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

The property shown in the source is named isa and has three main sections: freeze, assume, and prove. [2]

property isa;
freeze:
  instr       = decode(instruction) @ t,
  isa_state   = vstate @ t,
  isa_state_p = vstate @ t+1,
  nstate      = next_state(isa_state, instr) @ t;
assume:
  at t: not stall; // ready to start instruction
prove:
  at t+1: isa_state_p = nstate;
[...]
end property;

In the freeze section, the current instruction is decoded with decode(instruction), the current and next architectural states are obtained via vstate, and the predicted next architectural state is computed with next_state(isa_state, instr). The assumption requires that the processor is not stalled at time t, meaning it is ready to start the instruction. The proof obligation states that at t+1, the next architectural state equals the state computed by next_state. [2]

Role of decode

The decode macro is used to derive the decoded instruction fields from the current instruction word. The generated simulator can keep these decoded fields in an instruction_t representation so repeated decoding of the same instruction can be avoided, which the source identifies as an efficient technique due to the locality of most software, such as loop behavior. [3]

Role of next_state

The next_state macro computes the architectural state modified by the execution of the current instruction. The source describes the instruction execution model as a case block; for example, when the opcode denotes an ADD instruction, the register file in the current architectural state is updated with the sum of the source operands. Because next_state models instruction execution and returns the modified architectural state, it forms the core of the ISA model used by the property. [4]

ISS generation context

The paper states that generating the ISS from this ISA description does not require completing the full equivalence proof between ISA and RTL in advance, nor does it require identifying the mapping functions between architectural and implementation state up front. Instead, the ISA can be developed early in the design process in ITL and used for early ISS generation. The ISS only needs to be regenerated when the ISA changes, for example after a bug is found during formal verification. [5]

The generated C++ class, named Sim in the source, forms the core simulator functionality. It contains the code for instruction execution and holds the architectural state. A user-provided wrapper is still needed to call the generated public simulator functions, trigger single-instruction execution, and connect the simulator core to peripherals such as external memories or buses. [6]