Skip to main content Skip to secondary navigation

Synthesizing Formal Models of Hardware from RTL for Efficient Hardware Memory Model and Security Verification

Main content start

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.

Synthesizing Formal Models of Hardware from RTL for Efficient Hardware Memory Model and Security Verification (Caroline Trippel, Stanford University)