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

Modern hardware complexity makes it challenging to determine if a given microarchitecture adheres to a particular memory consistency model (or 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 microprocessor designs written in Verilog, with the help of modest user-provided design metadata. As a case study, we use rtl2𝜇spec to facilitate the Check-based verification of the four-core RISC-V V-scale (or multi-V-scale) processor's MCM implementation. We show that rtl2𝜇spec can synthesize a complete, and proven correct by construction, 𝜇spec model from the Verilog design of the multi-V-scale processor in 6.90 minutes. Subsequent Check-based MCM verification of the synthesized 𝜇spec model takes less than one second per litmus test.