Progressive Automated Formal Verification of Memory Consistency in Parallel Processors

Abstract:

In recent years, single-threaded hardware performance has stagnated due to transistorlevel limitations stemming from the end of Moore’s Law and Dennard scaling. Instead,
today’s designs improve performance through heterogeneous parallelism: the use of
multiple distinct processing elements on a chip, many of which are specialised to run
specific workloads. The processing elements in such architectures often communicate
and synchronise with each other via loads and stores to shared memory. Memory
consistency models (MCMs) specify the ordering rules for such loads and stores. MCM
verification is thus critical to parallel system correctness, but is notoriously hard to
conduct and requires examining a vast number of scenarios.
Verification using formal methods can provide strong correctness guarantees based
on mathematical proofs, and is an excellent fit for MCM verification. This dissertation
makes several contributions to automated formal hardware MCM verification, bringing
such techniques much closer to being able to handle real-world architectures. Firstly,
my RTLCheck work enables the automatic linkage of formal models of design orderings
to RTL processor implementations. This linkage helps push the correctness guarantees
of design-time formal verification down to taped-out chips. The linkage doubles as a
method for verifying microarchitectural model soundness against RTL. Secondly, my
RealityCheck work enables scalable automated formal MCM verification of hardware
designs by leveraging their structural modularity. It also facilitates the modular
specification of design orderings by the various teams designing a processor. Thirdly,
my PipeProof work enables automated all-program hardware MCM verification. A
processor must respect its MCM for all possible programs, and PipeProof enables
designers to prove such results automatically.
This dissertation also proposes Progressive Automated Formal Verification, a novel
generic verification flow. Progressive verification emphasises the use of automated
formal verification at multiple points in system development—starting at early-stage
design—and the linkage of the various verification methods to each other. Progressive
verification has multiple benefits, including the earlier detection of bugs, reduced
verification overhead, and reduced development time. The combination of PipeProof,
RealityCheck, and RTLCheck enables the progressive verification of MCM properties
in parallel processors, and serves as a reference point for the development of future
progressive verification flows.