ITL

Tool

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.

First seen 5/26/2026

Last seen 5/29/2026

Evidence 7 chunks

Wiki v1

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

7 connections

Generating an Efficient Instruction Set Simulator from a Complete Property Suite ← uses 100% 4e

The paper uses ITL (Interval Temporal Logic) as the property specification language.

Architectural Style Properties ← uses 100% 2e

Architectural style properties are formulated in the ITL language.

VHDL uses → 95% 2e

ITL supports the use of VHDL operators in temporal expressions.

Interval Property Checking ← uses 100% 1e

ITL is the language used to express properties in interval property checking.

Temporal Logic implements → 100% 1e

ITL implements temporal logic for describing synchronous system behavior.

Freeze Variable uses → 100% 1e

ITL uses freeze variables to capture signal values at specific time points.

Verilog uses → 95% 1e

ITL supports the use of Verilog operators in temporal expressions.

LINKED ENTITIES

2 links

Instruction Set Simulator generated_from The evidence repeatedly describes generating an ISS from ITL property suites and ISA descriptions.

RTL verified_against The evidence says reformulated ITL properties are checked against RTL and discusses ISA/RTL equivalence proof.

CITATIONS

13 sources

13 citations — click to expand

[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