Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations

Abstract

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 Check-based verification of the four-core RISC-V V-scale (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 SystemVerilog design of the multi-V-scale processor in 6.84 minutes. Subsequent Check-based MCM verification of the synthesized μspec model takes less than one second per litmus test.