Skip navigation
Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp01vq27zr48r
Title: Progressive Automated Formal Verification of Memory Consistency in Parallel Processors
Authors: Manerkar, Yatin
Advisors: Martonosi, Margaret
Contributors: Computer Science Department
Keywords: computer architecture
formal verification
memory consistency models
model checking
Subjects: Computer science
Issue Date: 2021
Publisher: Princeton, NJ : Princeton University
Abstract: 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.
URI: http://arks.princeton.edu/ark:/88435/dsp01vq27zr48r
Alternate format: The Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog: catalog.princeton.edu
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Computer Science

Files in This Item:
File Description SizeFormat 
Manerkar_princeton_0181D_13565.pdf3.93 MBAdobe PDFView/Download


Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.