Skip to content
STIMSMITH

ITL

Tool WIKI v1 · 5/26/2026

ITL is a verification language used to express formally checkable processor properties and ISA-style descriptions. In the cited ISS-generation flow, ITL property suites model architectural state, instruction effects, interfaces, and reset behavior, and can be translated into C++ instruction set simulators.

Overview

ITL is used as a verification language for processor property suites. In the cited work, properties written in ITL describe design transitions and output behavior; when verification and completeness checking succeed, the property suite forms a model of the verified design. This model can be exploited to generate an executable simulator.[C1]

Property structure and abstraction

ITL properties are organized around constructs such as freeze, assume, and prove, and can use macros to capture recurring behavior. An example ADD-instruction property decomposes an instruction word into opcode and register fields, assumes that the processor is ready to execute the ADD instruction, and proves the corresponding architectural register-file update.[C2]

The processor state described by these properties is an abstract or architectural state corresponding to the programmer-visible view of the processor. Mapping functions can hide implementation details such as pipeline forwarding logic while keeping the properties compact and readable.[C3]

Architectural-style ITL for ISS generation

For automatic instruction set simulator generation, the cited method reformulates properties in an architectural style. This style explicitly models the architectural state and memory/port interfaces, defines a next_state macro for instruction and interrupt effects, defines interface-behavior macros, and defines the architectural reset state.[C4]

In this style, the architectural state is represented using user-defined VHDL record data types, typically including elements such as a register file, status flags, and a program counter. ITL also introduces an update keyword for explicitly defining writes to array or record data structures.[C5]

The resulting architectural-style property captures the behavior of the verified design through next_state, yielding a formally checkable ISA description. That description is used as the starting point for generating a C++ instruction set simulator.[C6]

Translation to C++

The generated simulator core is a C++ class, named Sim in the cited work. It contains instruction-execution code and stores the architectural state. Translation from ITL to C++ includes generating public functions for next_state, decode, and interface macros; generating private functions for other macros; creating a member variable for architectural state; replacing ITL/HDL data types and operations with C++ equivalents; and replacing update expressions with direct array or struct overwrites.[C7]

The generated C++ core must be connected to its environment through a wrapper. The wrapper calls the generated public functions to execute individual instructions and connects the simulator core to peripheral components such as external memories or buses. The cited experiments also integrated the generated core with commercial simulation and debugging tools.[C8]

Optimizations

Several optimizations are applied during C++ generation to improve simulator performance. ITL/HDL data types whose bit sizes fit the host machine are mapped to native C++ types such as unsigned integers, while larger bit vectors use dedicated data structures. Basic operations are mapped to native C++ operations, and more complex operations such as bit slicing, bit rotation, and operations on large bit vectors use optimized library functions.[C9]

The generator also analyzes data dependencies in macro functions to identify shared expressions, enabling the simulator class to store temporary and intermediate results. Decoded instruction fields can be cached so that repeated decoding of the same instruction is avoided, which is effective for software with locality such as loops.[C10]

Verification-flow role

A full equivalence proof between ISA and RTL is not required before generating the ISS. The ISA can be developed in ITL early in the design process and used to generate an ISS; the ISS only needs regeneration when the ISA changes. Full confidence that the generated ISS complies with the design is obtained later through verification.[C11]

Reported evaluation

In one experiment, an ISS was generated from an ITL property suite for a small 5-stage pipelined processor with eight 16-bit registers, an interrupt-return-vector register, and seven instructions. The generated simulator reached 7 MIPS, compared with 0.22 MIPS for an interpretive simulator and 14 MIPS for a just-in-time compiled simulator built with a commercial tool.[C12]

In a second experiment, an ISS was generated for an industrial processor design with 64 32-bit registers in multiple hardware contexts, a 7-stage pipeline, memory and bus interfaces, and 88 instructions based on the DLX instruction set architecture. The processor core had about 10,000 lines of VHDL, while the final reformulated property suite had about 2,000 lines of ITL. The generated simulator reached 1.2 MIPS, while a commercial just-in-time compiled simulator reached 2.5 MIPS.[C13]

LINKED ENTITIES

2 links
Instruction Set Simulator generated_from
RTL verified_against

CITATIONS

13 sources
13 citations
[1] ITL property suites can form a model of a verified design and be exploited to obtain a simulator. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[2] ITL properties use freeze, assume, prove, and macros; an ADD example decodes instruction fields and proves register updates. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[3] ITL processor properties describe architectural state and use mapping functions to abstract implementation details such as pipeline forwarding. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[4] Architectural-style ITL explicitly models architectural state, interfaces, next_state, interface behavior, and reset state. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[5] Architectural state is represented with user-defined VHDL record data types and ITL provides an update keyword for array or record writes. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[6] The architectural-style ITL property yields a formally checkable ISA description used as the starting point for C++ ISS generation. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[7] The generated C++ simulator class contains instruction execution code and architectural state, and translation includes generating public/private functions, state variables, C++ type substitutions, and update replacements. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[8] A wrapper calls generated simulator functions, connects the core to memories or buses, and can integrate it with commercial simulation/debugging tools. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[9] C++ generation optimizes ITL/HDL types and operations by using native C++ types and operations where possible, with optimized libraries for complex or large-bit-vector operations. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[10] The generator caches shared intermediate results and decoded instruction fields to reduce simulation runtime. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[11] ISS generation from ITL does not require a full ISA/RTL equivalence proof upfront; full confidence is achieved later through verification. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[12] For a small 5-stage pipelined processor, the generated ITL-based ISS reached 7 MIPS versus 0.22 MIPS interpretive and 14 MIPS JIT-CS. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[13] For an industrial processor design, the final property suite had 2,000 lines of ITL and the generated ISS reached 1.2 MIPS versus 2.5 MIPS for a commercial JIT-CS simulator. Generating an Efficient Instruction Set Simulator from a Complete Property Suite