With the end of Moore's Law and Dennard scaling, system developers have turned to parallel architectures and languages to continue to improve performance. Memory consistency models (MCMs) specify the ordering requirements for memory operations used for synchronization in these parallel systems, so MCM verification is critical to overall system correctness. My work enables efficient formal MCM modelling and verification across the stack, from high-level languages down to Verilog RTL.

In this talk, I will discuss two components of my thesis: PipeProof and RTLCheck. PipeProof offers the first-ever automated verification of a hardware design specification against its instruction-level MCM across all possible programs (an infinite space). PipeProof uses a combination of abstraction refinement and happens-before graphs that are checked using an SMT (Satisfiability Modulo Theories) solver, and enables hardware architects to automatically ensure that their design respects its MCM before even a line of RTL (Register Transfer Language) is implemented.

Once the processor's low-level Verilog RTL exists, the RTLCheck approach I developed can automatically check this Verilog against the hardware specification verified by PipeProof for a set of test programs. A key contribution of RTLCheck is its set of novel algorithms for connecting the temporal execution of RTL to the axiomatic happens-before graphs used by PipeProof. The composition of PipeProof and RTLCheck allows designers to automatically check their low-level RTL against an instruction-level MCM specification.