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]

Architectural state and instruction semantics

The architectural state is the programmer-visible view of the processor state, such as visible registers. In the cited approach, mapping functions connect this high-level state to implementation details such as pipeline forwarding logic, allowing properties to be written in a compact form instead of reimplementing circuit logic.^[3]

Instruction semantics can then be expressed as state transitions. For example, the evidence shows an ADD-instruction property that decodes fields from the instruction word, assumes the opcode is ADD_op, and proves that one time step later the destination register is updated with the sum of two source registers.^[4]

A more detailed instruction description in the formal-verification setting is a property whose structure follows three parts: first a trigger (TRIGGER) giving the execution condition; then updates of the program counter and the architecture registers/flags; finally one transaction per interface (e.g., DMEM_IDLE for the data-memory interface). The example bit-fields for an ADD-like instruction are IW[10:8], IW[7:5], and IW[4:2] for the two source operands and the destination, with the PC advance defined as (PC + 2)[7:0] and the result computed and truncated to 16 bits, e.g., UPDATE_1 := (VREGISTER_1 + VREGISTER_2)[15:0].^[5]

ISA descriptions as inputs to generated simulators

The ISS-generation paper reformulates properties into an architectural style to enable straightforward simulator generation. This style explicitly models architectural state and memory or port interfaces and explicitly defines a next_state macro that captures the effect of instructions.^[6]

The generated C++ simulator includes public functions such as next_state and decode, private functions for remaining macros, 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.^[7]

In the reported evaluations, one generated ISS targeted a small pipelined processor whose instruction set contained seven logic, arithmetic, memory-access, and jump instructions. A second generated ISS targeted an industrial processor capable of executing 88 instructions based on the DLX instruction set architecture.^[8]

Modeling an ISA in constrained-random verification

Constrained-random verification (CRV) of microprocessors requires stimulus-generation infrastructure that is built with explicit knowledge of the processor's instruction set architecture and state, because pure random instructions rarely create useful stimulus for important design features such as branches, jumps, and exceptions.^[9]

The MIPS-I ISA is given as the example design under test. The evidence describes MIPS-I as partitioned into four functional classes: no operation, load and store, computational, and control. The operation class encapsulates the operation kind, the list of operands, and other properties, with a kind enumerated type that lists the supported opcodes defined by the ISA.^[10]

CRV models three levels of transaction abstraction in SystemVerilog — operations, instructions, and instruction scenarios — as classes, with each transaction class containing properties, constraints, and methods. For example, a transaction can be an ADD operation with two source registers and the result placed into a destination register, and a method can pack the transaction into its binary representation (such as 000000_00011_00101_01010_00000_100000).^[11]

The evidence also illustrates how ISA rules are translated into SystemVerilog constraints, including:

• [R1] Memory load and store operations are in slot 0 only; otherwise an exception is to be detected.
• [R2] Return from Exception (ERET) must be in slot 0.
• [R3] ERET in slot 0 must be paired with NOP in slot 1; otherwise hardware behavior is undefined.
• [R5] Writing to the same scalar register in both operations of the same instruction is disallowed; otherwise hardware behavior is undefined.^[12]

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 to make the operation illegal for exception testing. The CRV methodology also models branch operations such as BEQ using added LABEL kinds and from/to properties so that program-counter offsets and program-trace semantics can be checked against the ISA-defined branch behavior.^[13]

ISA-level verification through hardware-accelerated fuzzing

The emergence of new ISAs such as RISC-V is cited as driving the demand for more agile and efficient processor-verification methodologies, especially faster coverage convergence than simulation-based approaches alone can provide.^[14]

TurboFuzz is described as an end-to-end hardware-accelerated verification framework that places the entire Test Generation–Simulation–Coverage Feedback loop on a single FPGA. It enhances test quality through optimized test-case seed control flow, efficient inter-seed scheduling, and hybrid fuzzer integration, and uses feedback-driven generation to accelerate coverage convergence. The reported results state that TurboFuzz collects up to 2.23x more coverage than software-based fuzzers in the same time budget and achieves up to 571x speedup when detecting real-world issues, with full visibility and debugging capabilities and moderate area overhead.^[15]

Formal verification of ISA conformance through property generation

Beyond simulation-based and CRV-based approaches, formal methods can be applied directly to an ISA specification by automatically generating a complete property suite from an architecture description. The cited work introduces this as a way to make the formal verification of processor functionality part of the same tool chain that already produces simulators, assemblers, or compilers, and notes that other tools such as Facile and LISA exist for the latter purpose but do not by themselves cover functional verification.^[16]

The starting point of the approach is an architecture description of the processor. By defining a number of mapping functions, the user captures how the abstract ISA-level concepts (such as the program counter, the instruction word, and the architecture register file) are mapped to the register-transfer level (RTL) implementation. Mapping functions refer to pipeline stages, stall and cancel signals, and similar objects that design and verification engineers are familiar with, so the specification is captured in a concise and readable form while the underlying general processor model enables verification of advanced features such as multicycle instructions, out-of-order termination, and exceptions.^[17]

Architecture description structure

The architecture description has a clear two-part structure:

• First section (components): lists all architecture registers and flags, plus the interfaces to memories and buses with their respective transaction types.
• Second section (ISA description): defines all instructions of the processor. For each instruction, the description gives the execution condition (TRIGGER), the updates of the program counter and the architecture registers and flags, and one transaction per interface. Registers in this section are referred to by their specification name.^[18]

The instructions are described on the architecture level; verifying them against the RTL implementation requires a user-supplied mapping. For the program counter (PC) and the instruction word (IW), the mapping function typically points to dedicated RTL signals. The mapping of the architecture register file, however, requires a model of the pipelining because every pipelined processor design includes forwarding mechanisms.^[19]

Pipeline model used in the formal verification

A pipeline overlaps the processing of instructions to speed up computation: a new instruction starts before the preceding one has terminated. A typical simple pipeline partitions an instruction into fetching the instruction word from memory, decoding it, executing logical and arithmetic operations, and writing the result back to the register file. The two principal pipeline hazards relevant to ISA-level verification are:

• Read-after-write conflicts (data hazards): when an instruction needs data being computed by a preceding instruction, requiring a stall mechanism.
• Branch hazards: when a taken jump is detected after subsequent sequential instructions have already been fetched, requiring the pipeline to be cleaned of wrongly fetched instructions.^[20]

The cited approach uses basic pipeline modeling for the control path to keep track of the different instructions in the pipeline; handling of forwarding is part of the data-path model and is treated separately.

Verification engine and property completeness

The chosen formal verification technique is Interval Property Checking (IPC), a technique similar to Bounded Model Checking. IPC is used to check whether a system satisfies a set of properties about the operations of a design — for example, the processing of a request in a bus bridge or, in this case, the execution of an instruction in a processor. The driving verification engine is OneSpin 360 MV, which offers the performance and capacity to formally verify whole processor designs.^[21]

The generation ensures that all possible scenarios are covered with properties, but not that all transactions verify all outputs. In particular, the interface signals are not checked at all for read transactions, leaving a gap in the verification. The automatic gap-detection feature of OneSpin 360 can be used to close these gaps as well.^[22]

FISACO tool and PCP case study

The above method is implemented as a front-end for OneSpin 360 MV called FISACO (Formal Instruction Set Architecture Compiler). FISACO takes an architecture description and automatically generates the instruction properties and the consistency assertions in a form readable for 360 MV. The mapping information must be supplied in a temporal logic format, and the combined processor model (architecture description plus mapping information) can then be verified and debugged using 360 MV.^[23]

The approach was demonstrated on an industrial control processor used in embedded automotive systems, the Peripheral Control Processor (PCP) by Infineon Technologies, a domain with particularly high quality requirements. Using the generated property suite and the mapping functions, the instruction set of the PCP could be successfully verified, except for two highly complex bus instructions involving nested loops and excluding three complex math instructions; for these, the PCP's control mechanisms did not match the general pipeline model, and the cited work judged it not useful to extend the model for these very design-specific cases. Additional functionality beyond the ISA, such as loading and storing full register contexts, was verified manually using the same defined functions. The overall verification took about 5 person-months, yielding an estimated 100% productivity gain over manual property coding.^[24]

The reported verification results (on a 2.2 GHz workstation with 16 GB memory) break down the property categories and per-property proof time and memory consumption as follows:

Most of the verification time was spent on arithmetic and bus instructions, with bus instructions being mostly multicycle and therefore requiring longer design unrollings.^[25]

References

^[1]: ISA description as architectural state plus next-state function. ^[2]: Processor operation properties describe single-instruction execution. ^[3]: Architectural state as programmer-visible state represented through mapping functions. ^[4]: ADD instruction property decodes instruction fields and updates the destination register. ^[5]: Per-instruction description with TRIGGER, register/PC updates, and one transaction per interface; ADD-like example uses IW[10:8], IW[7:5], IW[4:2] fields, PC advance (PC+2)[7:0], and result truncated to 16 bits. ^[6]: Architectural-style properties explicitly model state, interfaces, and next-state behavior. ^[7]: Generated C++ ISS contains next_state, decode, private macro functions, and architectural-state storage. ^[8]: Generated ISS evaluations for a seven-instruction processor and an 88-instruction DLX-based processor. ^[9]: CRV stimulus generation must encode knowledge of the processor's ISA and state. ^[10]: MIPS-I functional classes and operation-class kind enumeration. ^[11]: SystemVerilog transaction classes with properties, constraints, and methods for operations and instructions. ^[12]: MIPS-I architectural rules R1, R2, R3, and R5 expressed as SystemVerilog constraints. ^[13]: Illegal opcodes and branch labels modeled in CRV for exception testing. ^[14]: RISC-V and other new ISAs create demand for agile verification methodologies. ^[15]: TurboFuzz FPGA-accelerated fuzzing metrics and Test Generation–Simulation–Coverage Feedback loop. ^[16]: Simulator/assembler/compiler generators such as Facile and LISA exist, but formal verification of functionality is not part of their tool chain. ^[17]: Architecture description with mapping functions from abstract ISA concepts to RTL implementation, including pipeline stages, stall and cancel signals. ^[18]: Two-part architecture description: components (registers, flags, memory/bus interfaces with transaction types) and ISA description (TRIGGER, register/PC updates, transactions per interface). ^[19]: Mapping of PC and IW typically points to dedicated RTL signals; mapping of the architecture register file requires a pipeline model due to forwarding. ^[20]: Pipeline hazards include read-after-write conflicts (requiring stalls) and branch hazards (requiring pipeline flushes on taken jumps). ^[21]: Interval Property Checking (IPC) is used together with the OneSpin 360 MV verification engine for whole-processor formal verification. ^[22]: FISACO's generation covers all scenarios with properties, but read transactions on interface signals are not checked; OneSpin 360's automatic gap detection can close these gaps. ^[23]: FISACO (Formal Instruction Set Architecture Compiler) is a front-end for OneSpin 360 MV that generates instruction properties and consistency assertions from an architecture description and temporal-logic mapping information. ^[24]: FISACO demonstrated on Infineon's Peripheral Control Processor (PCP); ~5 person-months, ~100% productivity gain; PCP ISA verified except for two nested-loop bus instructions and three complex math instructions, with extra functionality (register contexts) verified manually. ^[25]: PCP verification results: 34 assertions (600 s, 17.6 s avg, 937 MB), 15 arithmetic (18,788 s, 1,252.5 s avg, 2,500 MB), 18 logic/bit (3,368 s, 187.1 s avg, 2,500 MB), 7 jump (220 s, 31.4 s avg, 2,500 MB), 16 memory properties.