Synthesizing Formal Models of Hardware from RTL for Efficient Hardware Memory Model and Security Verification
Speaker: Caroline Trippel, Assistant Professor of Computer Science and Electrical Engineering, Stanford University
Date: October 14, 2021
Modern hardware complexity makes it challenging to determine if a given microarchitecture adheres to a particular memory consistency model (MCM), This observation inspired the Check tools, which formally check that a specific microarchitecture correctly implements an MCM with respect to a suite of litmus test programs. Unfortunately, despite their effectiveness and efficiency, the Check tools must be supplied a microarchitecture in the guise of a manually constructed axiomatic specification, called a 𝜇spec model. To facilitate MCM verification---and enable the Check tools to consume processor RTL directly---we introduce a methodology and associated tool, rtl2𝜇spec for automatically synthesizing 𝜇spec models from processor designs written in Verilog or SystemVerilog, with the help of modest user-provided design metadata.
As a case study, we use rtl2𝜇spec to facilitate the (efficient) Check-based verification of the four-core RISC-V V-scale (multi-V-scale) processor's MCM implementation. Beyond MCM verification, we plan to use rtl2𝜇spec to support verification of RTL designs with CheckMate, a recently developed tool in the Check suite which conducts hardware security verification.