isa property

CodeArtifact

The `isa` property is an architectural-style ITL property used as the starting point for automatic generation of a C++ instruction set simulator. It freezes the decoded instruction, current and next architectural states, and the result of `next_state`, then proves that the next abstract ISA state equals the state computed by the ISA transition model when the processor is not stalled.

First seen 5/29/2026

Last seen 5/29/2026

Evidence 1 chunks

Wiki v1

WIKI

Overview

The isa property is an architectural-style property used in the Complete Property Suite flow for generating an instruction set simulator (ISS). In the cited ISS-generation approach, the ISA description is the starting point for automatic generation of a C++ simulator core; the property is translated into simulator functionality rather than requiring a completed RTL/ISA equivalence proof first. [1]

Structure

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

3 connections

decode macro uses → 100% 1e

The isa property uses the decode macro to extract instruction fields.

Complete Property Suite part of → 95% 1e

The isa property is the top-level equivalence property in the property suite.

next_state macro uses → 100% 1e

The isa property uses the next_state macro to capture the state transition.

LINKED ENTITIES

3 links

Complete Property Suite PART_OF Extracted graph relationship

next_state macro USES Extracted graph relationship

decode macro USES Extracted graph relationship

CITATIONS

6 sources

6 citations — click to expand

[1] The `isa` property is used as the ISA description that starts automatic generation of a C++ instruction set simulator, and ISS generation can occur before a full RTL/ISA equivalence proof. Generating an Efficient Instruction Set Simulator from a Complete Property Suite

[2] The `isa` property freezes `instr`, `isa_state`, `isa_state_p`, and `nstate`, assumes `not stall` at time `t`, and proves `isa_state_p = nstate` at time `t+1`. Generating an Efficient Instruction Set Simulator from a Complete Property Suite

[3] `decode(instruction)` provides decoded fields of the current instruction word, and retaining decoded fields can avoid repeated decoding of the same instruction. Generating an Efficient Instruction Set Simulator from a Complete Property Suite

[4] `next_state` returns the architectural state modified by executing the current instruction and forms the core of the ISA model. Generating an Efficient Instruction Set Simulator from a Complete Property Suite

[5] The ISA can be developed early in ITL and used for early ISS generation; the ISS must be regenerated when the ISA changes. Generating an Efficient Instruction Set Simulator from a Complete Property Suite

[6] The generated C++ `Sim` class contains instruction-execution code and architectural state, while a user wrapper calls public functions and connects peripherals such as memories or buses. Generating an Efficient Instruction Set Simulator from a Complete Property Suite