Book Description

In recent years, single-threaded hardware performance has stagnated due to transistor-level 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.