Generating an Efficient Instruction Set Simulator from a Complete Property Suite
PaperThe paper describes a method for generating a C++ instruction set simulator (ISS) from a gap-free, complete property suite written in an architectural style. The approach treats the verified property suite as a formally checkable ISA description and translates it into simulator code, applying optimizations such as native C++ type/operator mapping, shared-expression caching, and decode-result caching. Experiments on a small pipelined processor and an industrial DLX-based processor show generated simulator performance of 7.0 MIPS and 1.2 MIPS, respectively.
First seen 5/26/2026
Last seen 5/29/2026
Evidence 13 chunks
Wiki v1
WIKI
Overview
Generating an Efficient Instruction Set Simulator from a Complete Property Suite presents an approach for generating a C++ instruction set simulator (ISS) from a gap-free, complete property suite formulated in an architectural style. The paper argues that, after successful formal verification, such a property suite forms an architectural model of the verified design; therefore, the generated ISS is equivalent to the design by construction. [C1]
The method is intended to use the formal property suite as a single source of specification for both verification and instruction-set simulation. The authors state that this supports correct early software development based on instruction set simulation and allows the simulator to be automatically adapted when the design or specification changes late in the design process. [C2]
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
20 connectionsThe paper uses ITL (Interval Temporal Logic) as the property specification language.
The paper presents an approach to automatically generate a C++ instruction set simulator from a complete property suite.
The paper uses a pipelined processor as the evaluation target for ISS generation.
Pipelined processors are the evaluation targets in the paper's experiments.
The paper's approach relies on a complete property suite as the basis for generating the ISS.
Sven Beyer is listed as an author of the paper.
Christian Pichler is listed as an author of the paper.
Ulrich Kühne is listed as an author of the paper.
The paper introduces an approach to generate a C++ instruction set simulator from a complete property suite.
The paper uses Interval Property Checking as the formal verification technique.
The paper describes the equivalence proof between the ISA and RTL as part of the verification.
The paper mentions RTL description as the design representation used in verification.
The paper discusses formal verification as the foundation for obtaining the complete property suite.
The paper mentions gate-level simulation as an alternative but slow simulation approach.
The paper mentions ADL-based approaches and their limitations compared to the proposed method.
The paper mentions pre-silicon software development as a major use case for ISS.
The paper evaluates the generated ISS in terms of simulation performance in MIPS.
The paper compares the generated ISS performance against interpretive simulation.
The paper compares the generated ISS performance against JIT compiled simulation.
The paper uses the OneSpin IPC verification tool for completeness analysis.
CITATIONS
21 sources21 citations — click to expand
[1] C1: The paper presents an approach for generating a C++ ISS from a complete architectural-style property suite, with equivalence to the verified design by construction after successful formal verification. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[2] C2: The formal property suite is used as a single specification source, enabling automatic simulator adaptation and correct early software development through ISS. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[3] C3: Architectural-style reformulation includes explicit architectural state and interfaces, a next_state macro, interface macros, and reset-state definition. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[4] C4: The architectural state is represented as a user-defined VHDL record containing elements such as register file, status flags, and program counter; interfaces are modeled with similar data types. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[5] C5: The update keyword models writes to arrays or records, and the example next_state function updates registers for an ADD instruction using decoded instruction fields. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[6] C6: The equivalence proof uses vstate to map implementation state to ISA state and checks correspondence between the CPU transition relation and next_state, including interface and reset behavior. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[7] C7: Full ISA/RTL equivalence proof and mapping-function identification are not required before ISS generation; an ITL ISA can be used to generate an ISS early, with full confidence obtained after verification. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[8] C8: The architectural-style reformulation yields a single property using next_state, described as a formally checkable ISA description and used as the starting point for C++ ISS generation. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[9] C9: The generated simulator core is a C++ Sim class and translation steps include public/private function generation, architectural-state member generation, ITL/HDL to C++ replacement, and update-expression replacement. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[10] C10: A wrapper must call generated functions for instruction execution and connect the simulator core to peripherals; integration with commercial simulation/debugging tools is possible. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[11] C11: Code-generation optimizations map fitting bit-vector types and basic operations to native C++ constructs and use optimized libraries for complex operations and large bit vectors. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[12] C12: The generator analyzes macro data dependencies to find shared expressions and cache temporary or intermediate computation results. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[13] C13: Decode-result caching avoids repeated decoding of the same instruction and is presented as effective due to software locality such as loops. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[14] C14: The first experiment used a small pipelined processor with eight 16-bit registers, an interrupt-return-vector register, a five-stage pipeline, simple data-memory interface, and seven instructions. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[15] C15: For the small processor, interpretive, JIT-CS, and generated simulators achieved 0.22, 14.0, and 7.0 MIPS respectively, with the generated ISS reaching about 50% of JIT-CS performance. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[16] C16: The second experiment used an industrial processor with 64 32-bit registers in multiple hardware contexts, a seven-stage pipeline, memory and bus interfaces, and 88 DLX-based instructions; the core had about 10,000 VHDL lines and the property suite 2,000 ITL lines. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[17] C17: The industrial property suite and its completeness were checked against the processor design using OneSpin Verification Solutions and considered a correct and complete specification. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[18] C18: For the industrial processor, the JIT-CS simulator averaged 2.5 MIPS and the generated ISS reached 1.2 MIPS, which the paper describes as comparable to modern custom-made ISS performance. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[19] C19: The paper attributes performance differences to optimization maturity of commercial tools and to hardware and pipeline effects captured by generated properties. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[20] C20: The conclusion states that optimized generated C++ simulators can be comparable to state-of-the-art commercial tools and that the method provides a practical way to obtain a proven-correct, efficient ISS. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[21] C21: The research was supported by BMBF in the HERKULES project under contract number 01M3082. Generating an Efficient Instruction Set Simulator from a Complete Property Suite