Overview
Generated C++ ISS refers to the automatically generated C++ instruction set simulator described in Generating an Efficient Instruction Set Simulator from a Complete Property Suite. The simulator is generated from the same complete property suite used for formal processor verification, rather than from a separately hand-written simulator model or an architecture-description-language reimplementation. This addresses a key risk of traditional ISS development: a simulator independently reimplementing the ISA can diverge from the actual design or ISA. [C1]
The paper presents this artifact as a way to obtain a provably correct simulator with relatively small effort. Because the property suite is used in the formal verification of the processor, the generated simulator is constructed from the ISA model that is checked against the RTL design. [C2]
Source model
The generation flow starts from an ISA description written in the ITL verification language. In the architectural-style property shown in the paper, an instruction is decoded, the current architectural state is read, next_state computes the architectural state after executing the instruction, and the proof obligation relates that next state to the implementation state after one step. The paper states that the next_state function forms the core of the ISA. [C3]
A complete property suite is important because completeness means the properties capture the design behavior uniquely for every possible combination of states and inputs. After formal verification, the set of properties forms a functionally equivalent model of the verified design; any two designs satisfying all properties of a complete property suite are formally equivalent. [C4]
Generated C++ structure
The generated simulator core is a C++ class named Sim. This class contains the code for executing instructions and holds the architectural state. The generated class is not the entire simulation environment by itself: the user supplies a wrapper that calls the generated public functions to execute individual instructions and connects the simulation core to external components such as memories, buses, commercial simulation tools, or debugging tools. [C5]
The paper also describes an optimization in which decoded fields of the current instruction word are kept in an instruction_t structure. This avoids repeated decoding of the same instruction. The authors identify this as useful because software locality, such as loop execution, makes instruction reuse common and can reduce simulation runtime. [C6]
Verification and lifecycle
The ISS can be generated early from the ITL ISA description without first completing the full equivalence proof between the ISA and the RTL or identifying the mapping functions between architectural and implementation state. If the ISA is updated, for example after finding a bug during formal verification, the ISS must be generated again. The paper notes that the ISS is therefore available when verification starts, while full confidence that it complies with the design is obtained at the end of verification. [C7]
Evaluation
The authors report generating an ISS for a small pipelined processor as an initial evaluation, and the abstract states that the approach was shown feasible for an industrial design. The resulting simulator performance is reported as comparable to custom state-of-the-art simulators. [C8]