Overview

An Instruction Set Architecture (ISA) is the interface between hardware and software of a computing system and is therefore of central importance to the system architecture.^[1] A conventional way to represent an ISA is as an architecture description for an instruction-set simulator (ISS): it consists of architectural state plus a next_state function that describes the effect of each instruction and interrupt on that state.^[2]

The same architecture description can be interpreted 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.^[3]

CPUs are expected to faithfully implement their ISAs and to enforce strict isolation between processes; this expectation has been increasingly challenged by the discovery of architectural and microarchitectural-level vulnerabilities that can leak data, bypass protections, or undermine system integrity even when the software itself is secure.^[4] Modern processors, particularly in the x86 family, contain layers of undocumented behavior implemented in proprietary microcode, and as designs become more complex and opaque the risk of hardware-level security flaws continues to grow.^[4]

Architectural state and instruction semantics

The architectural state is the programmer-visible view of the processor state, such as visible registers. In the cited ISS-generation 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.^[5]

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.^[6]

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].^[7]

ISA encoding and density considerations

An ISA's encoding scheme determines how the binary bytestream maps to architectural operations. The RISC-V base integer ISA, for example, consists of a mandatory base (RV32I, RV64I, RV128I) plus optional extensions such as M (integer multiply/divide) and A (atomic); a non-compressed RISC-V instruction is 32 bits long and contains fields such as opcode, source and destination registers, and immediates whose presence and width depend on the instruction format (R, I, S, B, U, J).^[8]

A complete RISC-V instruction can be reorganized as a sequence of at most six 8-bit tokens, where each token represents a semantic field (Opcode, Funct7, Funct3, Rd, Rs1, Rs2, plus split immediate components ImmLo/ImmMi/ImmHi, or Shamt for shift forms). Because each format uniquely determines its required token set, the omitted-field convention introduces no ambiguity and the encoding forms a prefix code; this property makes the encoding directly usable as a vocabulary for token-based machine-learning models that generate instructions.^[9]

ISA design also involves trade-offs beyond correctness. Instruction density and encoding efficiency are directly affected by an ISA's design, in contrast to performance, power, and area which are largely influenced by the implementation. The Scry ISA is reported to achieve instruction-feature parity with RISC-V's RV64IMC using 2-byte instructions versus RISC-V's 4 bytes, and to occupy only 28% of the 2-byte encoding space compared to RV64IMC's 68% occupancy of the 4-byte space. Scry uses forward-temporal referencing (where instructions name the future instructions that consume their outputs) together with internal data-type tagging tracked by the processor.^[10]

ISA specialized for proof systems

A more recent class of ISA is defined by application-driven constraints. The Valida ISA is explicitly designed for implementation in zkVMs to optimize for fast, efficient execution proving. Its specification provides an unambiguous definition of Valida program semantics and is intended to guide implementors of zkVMs and compiler toolchains, and may serve as a starting point for formalization efforts.^[11]

Formal ISA models and ISS generation

An ISA description has many aspects—instruction semantics, memory and register behavior, interrupts, decoding, et cetera—and ISS-generation work in the cited literature focuses on instruction semantics in isolation, abstracting the rest behind an interface so that vendor-supplied components (memory, bus, peripherals) can be reused without replacement.^[12]

LIBRISCV as a formal ISA model

LIBRISCV is a formal model providing semantics for the 32-bit base instruction set of the RISC-V architecture. Unlike prior formal ISA work such as Sail, LIBRISCV focuses exclusively on describing user-level instruction semantics in isolation, without formally describing aspects such as the memory, and does not capture microarchitectural details such as pipelining or timing. This makes it well suited to integration with existing simulators by allowing re-use of vendor-supplied components such as memory implementations.^[1]

LIBRISCV describes the semantics of an individual RISC-V instruction through an embedded domain-specific language (EDSL) in Haskell. The EDSL consists of two components: (1) primitives for describing interactions with architectural-state components (e.g., the memory) and (2) an expression language for performing operations on memory/register values. A simplified LB (load byte) example illustrates the style: read the base register, perform loadByte at the sum of base and immediate, and write the sign-extended byte back through writeRegister.^[13]

Internally, the LIBRISCV EDSL is implemented in Haskell using free monads. Because the formal description is machine-processable, it can be mapped to C/C++ code via the 26 primitives and the expression language to produce ISS code automatically.^[14]

The EDSL-based approach allows minimally invasive ISS generation: the generated ISS can replace the manually written execution component of an existing SystemC-based virtual prototype (e.g., RISC-V VP) or reference ISS (e.g., Spike), while the existing memory, bus, and peripheral models remain unchanged. Reported experiments indicate that the generated ISS achieves similar simulation speed to a manually written one while still passing the official RISC-V ISA tests.^[15]

ISS generation from architecture descriptions

A separate, simulation-oriented approach reformulates properties into an architectural style that explicitly models architectural state, memory or port interfaces, and a next_state macro that captures the effect of instructions. The style enables straightforward generation of a C++ simulator with 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.^[16][17]

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.^[18]

Modeling an ISA in constrained-random verification

Constrained-random verification (CRV) of microprocessors requires stimulus-generation infrastructure 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.^[19]

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.^[20]

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).^[21]

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.^[22]

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.^[23]

Verifying ISAs through fuzzing of ISS implementations

Coverage-guided fuzzing (CGF) can be used to verify ISS implementations against each other, with the goal of detecting mismatches and crashes when ISSs are presented with the same sequences of instructions, including illegal instructions. A typical CGF approach is two-step: first generate a testset of ELF testcases via a fuzzer instrumented with custom coverage callbacks, then run the testset on the ISS under test (ISS-UT) and one or more reference ISSs, and report mismatches.^[24]

An ELF testcase embeds a binary bytestream (interpreted as an instruction sequence) into a pre-defined ELF template that provides a prefix to initialize all registers to a fixed pre-defined state, and a suffix that writes register values and selected memory contents back so results can be dumped and compared across ISSs.^[25]

Functional coverage metrics for ISS verification reason about both instruction structure and operand values. Structure metrics include R2: for every instruction with one source register RS1 and destination RD, the case RD = RS1 and the case RD ≠ RS1 should each be observed at least once. R3 extends this to three-register instructions, requiring observation of each of the four RD/RS1/RS2 equality cases.^[26]

A specialized mutator for ISS verification operates on the binary bytestream: starting at offset 0, it applies one of two local mutations at each step—(1) select a random instruction and inject its opcode bits at the current position (preserving randomized parameters and optionally injecting a special immediate), or (2) select a random constrained sequence of instructions and inject it. This constrains the fuzzer to use legal opcodes while still randomizing parameters, allowing it to discover and re-use specific instruction patterns through its own mutations and crossovers.^[27]

Post-silicon microcode-guided ISA fuzzing (Fuzzilicon)

Hardware-level vulnerability detection has traditionally relied on formal verification, runtime detection, information-flow tracking, and hardware fuzzing; among these, hardware fuzzing has emerged as a promising approach because of its scalability and adaptability to various designs.^[28]

Hardware fuzzing has evolved into two distinct approaches:

• Pre-silicon fuzzing, which targets Register-Transfer Level (RTL) models during hardware development.
• Post-silicon fuzzing, which evaluates manufactured processors under real execution conditions.^[29]

The cited Fuzzilicon work targets the post-silicon setting for x86 CPUs, where the processor's complexity and the layers of undocumented behavior implemented in proprietary microcode motivate new fuzzing approaches that are microcode-aware rather than treating the ISA surface alone.^[4]

ISA-aware generative-model verification on FPGA (Lyra)

The Lyra framework is a hardware-accelerated RISC-V verification framework that combines an ISA-aware generative model with FPGA-accelerated differential checking. Both the design under test (DUT) and a software ISA reference emulator are instantiated on the same FPGA following the Encore architecture; a software fuzzer running on a CPU connects to the DUT's main memory, continuously produces RISC-V instructions, and writes them into memory so that the DUT and reference model simultaneously fetch and execute each block.^[30]

Instead of creating stimuli by random generation or by simple semantic-blind mutations, Lyra trains a domain-specialized generative model (LyraGen) on the tokenized instruction encoding described above. The model learns the relationship between instruction tokens and the corresponding coverage vectors, and at inference time generates new tokens that can be reassembled into valid RISC-V instructions. Reported results indicate up to 1.27× higher coverage and end-to-end verification speedups of up to 107× to 3343× relative to state-of-the-art software fuzzers, with consistently lower convergence difficulty.^[30]

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.^[31]

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.23× more coverage than software-based fuzzers in the same time budget and achieves up to 571× speedup when detecting real-world issues, with full visibility and debugging capabilities and moderate area overhead.^[32]

Functional coverage for 100% RISC-V ISA coverage (RISCV-DV)

Functional-coverage definitions for RISC-V implementations must cover compliance to the ISA specification, ideally spanning all possible instruction combinations. This ideal is not achievable if one enumerates all possible sources, destinations, and data values; instead, a practical definition of "100% RISC-V ISA coverage" must be constructed.^[33]

For each RV32I instruction, it is mathematically possible to enumerate coverage points that cover all possible modes, register addresses, register contents, and immediate values. There are 32 possibilities for each register referenced in an instruction, and for an instruction with two source registers and one destination register that yields 32×32×32 = 2^15 combinations—within the practical realm for simulation. However, each 32-bit source register has one of 2^32 possible data values, which explodes the number of coverage points beyond all practical limits when combined with the register-value enumeration.^[34]

The cited methodology restricts coverage to all possible instruction modes, register addresses, and immediate values, but excludes the full space of register-content data values. With this restriction, the addition instruction ADD rd, rs1, rs2 yields 2^15 practical coverage points (32×32×32 register combinations) versus a mathematically possible 2^79 (register combinations multiplied by 2^32×2^32 source-data values), and the load-word instruction LW rd, rs1, imm yields 2^22 practical coverage points versus 2^54 mathematically possible.^[35]

The RISCV-DV environment supports this methodology by providing instruction-level, sequence-level, and program-level randomization to obtain good stimulus coverage for the ISA test suite, and converts the resulting assembly into binary executables of random valid instructions that can run on any core supporting the RISC-V ISA.^[36] Results are checked against a golden reference obtained by running the same generated tests on the Spike open-source RISC-V ISS; the merged functional-coverage (RISCV-DV) and code-coverage (RTL simulation) databases can be loaded into Synopsys Verdi Coverage for combined viewing.^[37][38]

Defining 100% RISC-V ISA coverage and sharpening the definition is treated as an iterative process of upgrading the definition and re-running the test suite to achieve the coverage goals, with methodology refinement described as an ongoing collaboration between Synopsys and Bluespec.^[39]

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.^[40]

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.^[41]

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.^[42]

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.^[43]

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.^[44]

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.^[45]

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.^[46]

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.^[47]

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.^[48]

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.^[49]

References

^[2]: ISA description as architectural state plus next-state function. ^[3]: Processor operation properties describe single-instruction execution. ^[5]: Architectural state as programmer-visible state represented through mapping functions. ^[6]: ADD instruction property decodes instruction fields and updates the destination register. ^[7]: 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. ^[1]: LIBRISCV provides formal semantics for the 32-bit base RISC-V instruction set, focused on user-level instruction semantics in isolation, without modeling memory or microarchitecture. ^[12]: ISS generation must integrate with vendor-supplied SystemC components; the approach targets minimally invasive ISS generation that preserves existing peripherals and bus models. ^[13]: LIBRISCV's Haskell EDSL provides primitives (e.g., readRegister, writeRegister, loadByte) and an expression language for describing RISC-V instruction semantics; the LB example is given. ^[14]: EDSL descriptions in Haskell can be mapped to C/C++ code via the 26 primitives and the expression language; the LIBRISCV EDSL is implemented using free monads. ^[15]: Generated ISS was integrated with Spike and RISC-V VP, achieving similar simulation speed to manually written ISSs while still passing the official RISC-V tests. ^[8]: RISC-V base ISAs (RV32I/RV64I/RV128I) and optional extensions M (multiply/divide) and A (atomic); 32-bit non-compressed instructions with up to two source registers RS1/RS2 and one destination register RD. ^[9]: Tokenized RISC-V instruction encoding: at most six 8-bit tokens per instruction, one per semantic field (Opcode, Funct7, Funct3, Rd, Rs1, Rs2, ImmLo, ImmMi, ImmHi, Shamt), forming a prefix code. ^[30]: Lyra is a heterogeneous RISC-V verification framework combining an ISA-aware generative model (LyraGen) with FPGA-accelerated differential checking; reported up to 1.27× higher coverage and 107×–3343× end-to-end speedups vs. state-of-the-art software fuzzers. ^[10]: Scry ISA uses forward-temporal referencing and internal data-type tagging to achieve RV64IMC feature parity with 2-byte instructions (28% encoding occupancy) versus RISC-V's 4-byte (68% occupancy). ^[11]: Valida ISA is designed for zkVM implementation to optimize fast, efficient execution proving; its specification is intended for zkVM and compiler toolchain implementors and may serve as a starting point for formalization. ^[16]: Architectural-style properties explicitly model state, interfaces, and next-state behavior. ^[17]: Generated C++ ISS contains next_state, decode, private macro functions, and architectural-state storage. ^[18]: Generated ISS evaluations for a seven-instruction processor and an 88-instruction DLX-based processor. ^[19]: CRV stimulus generation must encode knowledge of the processor's ISA and state. ^[20]: MIPS-I functional classes and operation-class kind enumeration. ^[21]: SystemVerilog transaction classes with properties, constraints, and methods for operations and instructions. ^[22]: MIPS-I architectural rules R1, R2, R3, and R5 expressed as SystemVerilog constraints. ^[23]: Illegal opcodes and branch labels modeled in CRV for exception testing. ^[24]: Two-step CGF for ISS verification: fuzzer generates an ELF testset, then testset is run on ISS-UT and reference ISSs with mismatches reported. ^[25]: ELF testcase embeds a binary bytestream between an initialization prefix and a result-collection suffix that writes register values and selected memory contents back. ^[26]: Functional structure metrics R2 (RD=RS1 and RD≠RS1 for two-register instructions) and R3 (four RD/RS1/RS2 equality cases for three-register instructions). ^[27]: ISS-fuzzing mutator injects opcode bits of a random instruction or a random constrained instruction sequence into the bytestream, optionally with a special immediate. ^[31]: RISC-V and other new ISAs create demand for agile verification methodologies. ^[32]: TurboFuzz FPGA-accelerated fuzzing metrics and Test Generation–Simulation–Coverage Feedback loop. ^[40]: Simulator/assembler/compiler generators such as Facile and LISA exist, but formal verification of functionality is not part of their tool chain. ^[41]: Architecture description with mapping functions from abstract ISA concepts to RTL implementation, including pipeline stages, stall and cancel signals. ^[42]: Two-part architecture description: components (registers, flags, memory/bus interfaces with transaction types) and ISA description (TRIGGER, register/PC updates, transactions per interface). ^[43]: Mapping of PC and IW typically points to dedicated RTL signals; mapping of the architecture register file requires a pipeline model due to forwarding. ^[44]: Pipeline hazards include read-after-write conflicts (requiring stalls) and branch hazards (requiring pipeline flushes on taken jumps). ^[45]: Interval Property Checking (IPC) is used together with the OneSpin 360 MV verification engine for whole-processor formal verification. ^[46]: 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. ^[47]: 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. ^[48]: 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. ^[49]: 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. ^[4]: CPUs are expected to faithfully implement their ISAs and enforce strict process isolation; this assumption is challenged by architectural and microarchitectural vulnerabilities that affect secure software; x86 processors contain layers of undocumented behavior in proprietary microcode. ^[28]: Hardware-level vulnerability detection techniques include formal verification, runtime detection, information-flow tracking, and hardware fuzzing; among them, hardware fuzzing is highlighted for scalability and adaptability to various designs. ^[29]: Hardware fuzzing has two distinct approaches: pre-silicon fuzzing of RTL models during hardware development, and post-silicon fuzzing of manufactured processors under real execution conditions. ^[33]: Functional-coverage definitions for RISC-V implementations must cover compliance to the ISA specification; ideal spanning of all instruction combinations is not achievable because of register-content data-value explosion. ^[34]: RV32I instructions enumerate 32 register choices per operand; an instruction with two source registers and one destination yields 32×32×32 = 2^15 combinations, but combining with 2^32 source-data values explodes the coverage space beyond practical simulation. ^[35]: Practical RISC-V ISA coverage restricts to instruction modes, register addresses, and immediate values; ADD rd,rs1,rs2 has 2^15 practical coverage points vs. 2^79 mathematically possible; LW rd,rs1,imm has 2^22 practical vs. 2^54 mathematically possible. ^[36]: RISCV-DV provides instruction-level, sequence-level, and program-level randomization, producing binary executables of random valid instructions that can run on any core supporting the RISC-V ISA. ^[37]: Spike is the open-source RISC-V ISS used as the golden reference; results from Spike are compared against the Bluespec RTL simulation. ^[38]: Synopsys VCS merges functional-coverage (RISCV-DV) and code-coverage (RTL) databases via URG or Verdi Coverage, and the merged VDB is loaded into Synopsys Verdi Coverage for combined viewing. ^[39]: Defining 100% RISC-V ISA coverage is treated as an iterative process of upgrading the definition and re-running the test suite; the methodology refinement is described as an ongoing collaboration between Synopsys and Bluespec.