Instruction Set Architecture
ConceptAn Instruction Set Architecture (ISA) is a programmer-visible contract that can be represented as architectural state together with a next-state function describing the effect of each instruction and interrupt. Evidence from instruction-set simulator (ISS) generation, constrained-random verification (CRV) of microprocessors, FPGA-accelerated hardware fuzzing, and formally generated property suites (e.g., FISACO) centers on how an ISA is specified, abstracted, and exercised in modern processor verification.
First seen 5/25/2026
Last seen 6/9/2026
Evidence 60 chunks
Wiki v8
WIKI
Overview
An Instruction Set Architecture (ISA) can be represented as an architecture description for an instruction-set simulator (ISS). In the cited ISS-generation work, such a description mainly consists of architectural state plus a next_state function that describes the effect of each instruction and interrupt on that state.[1]
The same work describes processor properties at a high-level operation view: for a processor, an operation naturally corresponds to executing a single instruction, and each property describes the resulting change to internal state and output behavior.[2]
NEIGHBORHOOD
7 nodes · 11 edgesgraph · Instruction Set Architecture · depth=1
RELATIONSHIPS
28 connectionsRISC-V is a new instruction set architecture mentioned in the context of verification demands.
The paper mentions ISAs as a driver for new verification needs.
Spike is the official RISC-V ISA reference simulator implementing the RISC-V ISA.
The architecture description captures the ISA of the processor.
The VAMP has a formal ISA model.
The RTL design is compared with the ISA through formal equivalence proof.
The next state function forms the core of the ISA description, capturing instruction semantics.
The generated C++ ISS implements the ISA as derived from the complete property suite.
The architectural state is a key component of the ISA description.
Forvis is an ISS aiming to be a formal specification of the RISC-V ISA.
The RISC-V Virtual Prototype implements the RISC-V ISA.
Processor fuzzing requires inputs defined by an ISA
The paper targets instruction set architectures for rewrite rule synthesis.
Instruction Set Architecture (ISA) is discussed in the context of CHERI's implementation on RISC-V.
The ISA describes a sequential model of processing that SEQ implements as its reference.
Control-flow operations are part of the VAMP instruction set.
Abstract ISS are based on the instruction set architecture rather than gate-level implementation.
The generated C++ ISS implements the instruction set architecture captured in the complete property suite.
Arithmetic operations are part of the DLX/VAMP instruction set.
ISS are based on the ISA for their simulation model.
Logic operations are part of the VAMP instruction set.
The ISS simulates instruction set architecture behavior as a reference model.
Load and store operations are part of the DLX/VAMP instruction set.
The ISA includes condition codes as part of the architectural state.
Cross-level verification compares processor behavior against an ISA specification.
The ISA includes a register file as part of its architectural state.
Control and Status Registers are part of the RISC-V ISA.
CRV requires knowledge of the processor's instruction set architecture to generate effective stimuli.
LINKED ENTITIES
1 linksCITATIONS
20 sources20 citations — click to expand
[1] An ISA is captured as an architecture description consisting of architectural state plus a next_state function describing the effect of each instruction and interrupt. Automated Formal Verification of Processors
[2] FISACO's architecture description has a two-part structure: a components section listing architecture registers, flags, and memory/bus interfaces with transaction types, and an ISA description section defining each instruction's TRIGGER (execution condition), updates to PC and architecture registers/flags, and one transaction per interface. Automated Formal Verification of Processors
[3] An ADD-like instruction in the architecture description uses bit-fields IW[10:8], IW[7:5], IW[4:2] for two source operands and the destination, advances the PC by `(PC + 2)[7:0]`, computes the result and truncates to 16 bits, and issues a `DMEM_IDLE` transaction on the data-memory interface. Automated Formal Verification of Processors
[4] Mapping functions connect ISA-level concepts to the RTL implementation, with mapping of PC and IW typically pointing to dedicated RTL signals, while mapping the architecture register file requires a model of the pipelining because of forwarding mechanisms. Automated Formal Verification of Processors
[5] Pipeline hazards relevant to ISA-level verification include read-after-write conflicts requiring stalls and branch hazards requiring pipeline flushes on taken jumps. Automated Formal Verification of Processors
[6] The approach uses Interval Property Checking (IPC), a technique similar to Bounded Model Checking, together with the OneSpin 360 MV verification engine. Automated Formal Verification of Processors
[7] FISACO is a front-end for OneSpin 360 MV that takes an architecture description plus temporal-logic mapping information and automatically generates instruction properties and consistency assertions; the generated property suite covers all scenarios, but read transactions on interface signals are not checked, a gap that can be closed using OneSpin 360's automatic gap detection. Automated Formal Verification of Processors
[8] FISACO was demonstrated on the Peripheral Control Processor (PCP) by Infineon Technologies for embedded automotive use; the overall verification took about 5 person-months with an estimated 100% productivity gain, successfully verifying the PCP ISA except for two complex nested-loop bus instructions and three complex math instructions that did not fit the general pipeline model. Automated Formal Verification of Processors
[9] PCP verification results: 34 assertion properties (600 s total, 17.6 s avg, 937 MB), 15 arithmetic properties (18,788 s total, 1,252.5 s avg, 2,500 MB), 18 logic/bit properties (3,368 s total, 187.1 s avg, 2,500 MB), 7 jump properties (220 s total, 31.4 s avg, 2,500 MB), and 16 memory properties; most time was spent on arithmetic and bus (multicycle) instructions requiring long design unrollings. Automated Formal Verification of Processors
[10] Simulator/assembler/compiler generators such as Facile and LISA exist, but formal verification of processor functionality is not part of their tool chain; the cited approach adds the formal verification step starting from the same abstract architecture description. Automated Formal Verification of Processors
[11] CRV stimulus generation must be built with explicit knowledge of the processor's instruction set architecture and state, because pure random instructions rarely create useful stimulus for branches, jumps, and exceptions. Automated Formal Verification of Processors
[12] MIPS-I is partitioned into four functional classes — no operation, load and store, computational, and control — with an operation class encapsulating the operation kind, operands, and a `kind` enumerated type listing the supported opcodes defined by the ISA. Automated Formal Verification of Processors
[13] CRV models three levels of transaction abstraction in SystemVerilog — operations, instructions, and instruction scenarios — as classes with properties, constraints, and methods; for example, an ADD transaction can be packed into a binary representation such as `000000_00011_00101_01010_00000_100000`. Automated Formal Verification of Processors
[14] ISA rules are translated into SystemVerilog constraints, including: R1 (memory load/store only in slot 0), R2 (ERET must be in slot 0), R3 (ERET in slot 0 must be paired with NOP in slot 1), and R5 (no same-scalar-register write hazard in the two operations of the same instruction). Automated Formal Verification of Processors
[15] Exception conditions including illegal opcodes are first-class citizens in CRV: the operation class supports an `ILLEGAL` kind that, when randomized, uses a random unassigned opcode value; branch operations such as BEQ are modeled using `LABEL` kinds with `from`/`to` properties to check PC offsets and program-trace semantics against ISA-defined branch behavior. Automated Formal Verification of Processors
[16] The emergence of new ISAs such as RISC-V is driving demand for agile and efficient processor-verification methodologies with faster coverage convergence than simulation alone can provide. Automated Formal Verification of Processors
[17] TurboFuzz is an end-to-end hardware-accelerated verification framework that places the entire Test Generation–Simulation–Coverage Feedback loop on a single FPGA, using optimized seed control flow, inter-seed scheduling, and hybrid fuzzer integration, and reports up to 2.23x more coverage than software-based fuzzers in the same time budget and up to 571x speedup in detecting real-world issues. Automated Formal Verification of Processors
[18] An architectural-style property in the ISS-generation approach decodes instruction fields (e.g., the ADD instruction) and proves that one time step after the opcode is `ADD_op`, the destination register is updated with the sum of two source registers, and the ISS-generation approach reformulates properties into an architectural style that explicitly models state and interfaces and defines a `next_state` macro to capture the effect of instructions. Automated Formal Verification of Processors
[19] The generated C++ ISS exposes public functions `next_state` and `decode`, with remaining macros as private functions and a member variable holding the architectural state; the translation replaces ITL/HDL data types and update expressions with C++ types, operations, and direct array or structure overwrites. Automated Formal Verification of Processors
[20] Two ISS-generation evaluations are reported: a small pipelined processor with seven instructions spanning logic, arithmetic, memory-access, and jump classes, and an industrial processor capable of executing 88 instructions based on the DLX instruction set architecture. Automated Formal Verification of Processors