Overview

The next_state macro is an architectural-style ITL macro used to describe the state transition semantics of a processor instruction set. In the cited ISS-generation flow, an architectural-style formulation requires an explicit next_state macro that captures the effects of instructions and interrupts on the architectural state. [C1]

The macro’s return value is the architectural state after execution of the current instruction. The paper describes this as the architectural state “modified by the execution of the current instruction,” and states that next_state forms the core of the ISA. [C2]

Role in the ISA property

In the architectural-style property, the current instruction is decoded, the current architectural state is obtained, and the next architectural state is computed with:

nstate = next_state(isa_state, instr) @ t;

The property then proves that the architectural state at the next time step matches this computed nstate when the processor is ready to start an instruction. This places next_state at the center of the formally checkable ISA description used for equivalence checking and ISS generation. [C3]

State and instruction inputs

The macro operates on an architectural state record, described in the evidence as a user-defined VHDL record data type that combines architectural components such as the register file, status flags, and program counter. In the example, state has type state_t and holds all elements of the architectural state. [C4]

The current instruction is represented by a decoded instruction record. The evidence describes iw of type instruction_t as holding decoded fields of the current instruction word; keeping these decoded fields can avoid repeated decoding of the same instruction in the generated simulator. [C5]

Instruction semantics

Instruction execution inside next_state is modeled with a case block. The cited example states that when the opcode denotes an ADD instruction, the register file in the current architectural state is updated with the sum of the source operands. [C6]

The modeling uses the ITL update keyword, which explicitly defines a write access to an array or record data structure. This is used for architectural-state updates such as writing a destination register. [C7]

Use in ISS generation

The reformulated architectural-style property captures the verified design behavior using next_state, yielding a formally checkable ISA description that serves as the starting point for generating a C++ instruction set simulator. [C8]

During generation, the flow creates public C++ functions for next_state, decode, and interface macros; private functions are generated for remaining macros. The generated simulator core is a C++ class, Sim, containing the instruction-execution code and the architectural state. [C9]

The generated C++ code replaces ITL/HDL data types and operations with C++ types and operations, and replaces update expressions with direct array or struct overwrites. [C10]

Verification and generation workflow

The evidence distinguishes ISS generation from the full RTL/ISA equivalence proof. It states that generating the ISS does not require completing the full equivalence proof or identifying mapping functions between ISA and RTL states up front. Instead, the ISA can be developed in ITL early in the design process and used to generate an ISS; the ISS needs regeneration when the ISA changes. [C11]

Related concepts

• The next_state macro implements the next-state function of the ISA-level model.
• The architectural isa property uses next_state to compute nstate and prove correspondence with the next architectural state.