Definition

Architectural state is the processor state visible at the instruction-set architecture (ISA) or programmer level. In the RISC-V verification evidence, this state includes the program counter (PC), general-purpose registers (GPRs), control and status registers (CSRs), and memory contents relevant to execution. [C1]

At instruction retirement, an instruction has completed execution and its results have been committed to architectural state. Retirement is therefore a natural observation point for checking architecturally visible behavior rather than transient implementation behavior. [C2]

Role in retirement-level lockstep co-simulation

In retirement-level lockstep co-simulation, the RTL design and a validated reference model run the same program under a co-simulation harness. At each retire event, architectural state is captured and compared immediately. If the states diverge, the flow reports the retire index and expected-versus-actual values, allowing debug at the point of failure. [C3]

Because comparison is performed at retirement rather than against transient pipeline states, the debug process focuses on architecturally visible behavior and reduces false positives caused by intermediate implementation states. [C4]

Some lockstep flows make the compared subset configurable. The cited flow describes starting with PC-only checks, expanding to PC plus GPRs, adding CSRs for privilege and exception behavior, and finally comparing selected memory regions or the complete architectural state for sign-off confidence. [C5]

Role in XiangShan difftest and co-simulation

XiangShan's difftest framework implements a co-simulation approach in which the XiangShan design (the design under test, DUT) runs in lockstep with a golden reference model, comparing architectural state at commit points to detect discrepancies. [C6]

Two golden reference models are supported:

• NEMU (NJU Emulator): a fast functional RISC-V simulator used as the primary golden model, supporting all privilege modes (M/H/S/U) and virtual memory, with native checkpoint/restore via .zstd or .gz files. [C7]
• Spike: the official RISC-V ISA simulator maintained by RISC-V International, selected via the --spike flag. [C8]

The difftest interface exports several categories of signals for verification:

1. Architectural State: PC, GPRs, floating-point registers (FPRs), and vector registers. [C9]
2. CSRs: machine, supervisor, and hypervisor mode registers. [C9]
3. Memory Operations: load/store addresses and data for memory consistency checks. [C9]
4. Exceptions: exception cause and PC to verify trap handling logic. [C9]

The interface is checked during CI using difftest/scripts/st_tools/interface.py to ensure SimTop.sv matches the expected difftest-interface.sv. [C10]

By verifying at instruction-commit boundaries against a golden model, difftest provides cycle-accurate validation of architectural state, detection of implementation bugs, and automated regression testing across workloads. The infrastructure supports Verilator and VCS simulation backends and integrates with NEMU and Spike as functional reference simulators. [C11]

Role in EPEX

EPEX treats architectural state as the equivalence boundary for processor verification at the ISA level. The EPEX paper defines processing an instruction as transforming an architectural state s, described as the state visible to the programmer, into a new architectural state s'. [C12]

EPEX uses this abstraction to synthesize equivalent programs. For an instruction from a test program that starts in s and leads to s', EPEX uses a formal ISA model and SMT-based automated reasoning to find a different instruction that, when executed from the same s, reaches the same s'. Repeating this for each instruction transforms the original program P into a program P̂ whose behavior is equivalent on architectural states, while potentially exercising different data and control paths. [C13]

Practical interpretation

Across the provided evidence, architectural state functions as the externally meaningful state of the processor:

• it is the state committed at instruction retirement;
• it includes PC, GPRs, CSRs, and relevant memory contents (and, in XiangShan's difftest, FPRs and vector registers);
• it is the state compared between RTL and reference models in lockstep verification (e.g., NEMU or Spike in XiangShan difftest);
• it is the state over which EPEX defines instruction and program equivalence.

This makes architectural state a key boundary between ISA-level correctness and implementation-level behavior.