Skip to content
STIMSMITH

Bus memcheck

Concept WIKI v1 · 6/7/2026

Bus memcheck refers to a family of formal verification checks within the riscv-formal framework that validate a RISC-V core's behavior on its instruction and data memory buses. The family includes the data bus memcheck, the instruction bus fault memcheck, the data bus fault memcheck, and a set of data bus I/O checks. These bus-level checks supersede the earlier, equivalent instruction memcheck and data memcheck checks.

Overview

In the riscv-formal verification framework, a set of checks collectively referred to as bus memcheck validate how a RISC-V core interacts with the memory bus. Each check introduces a small, abstract memory model and observes bus traffic (via the RVFI bus interface) to confirm that the core's retired memory accesses, faults, and I/O behavior are consistent with what appears on the bus.

The bus memcheck checks are part of the broader memory abstraction machinery used by riscv-formal [evidence: 9adf98b4-b25d-4071-b16a-6d418db8e707]. The bus-level checks supersede the earlier, simpler instruction memcheck and data memcheck checks, which are no longer managed by genchecks.py and have been replaced by their standard bus-check equivalents [evidence: 9adf98b4-b25d-4071-b16a-6d418db8e707].

Data bus memcheck (bus_dmem)

The bus_dmem check adds a memory abstraction that emulates a single word of memory at an unconstrained address. The memory word is read/write. The check tests whether writes to and reads from the memory location, as reported via RVFI, are consistent. It additionally checks that an initial value as reported via RVFI matches the value fetched on the bus. The check does not require writes to appear on the bus, making it compatible with caches situated between the core and the observed bus.

When the granularity of access faults as observed from the core is coarser than the width of the bus, the macro RISCV_FORMAL_FAULT_WIDTH must be defined to the corresponding width in bytes (for example, the width of a cache line in bytes) [evidence: 583772cd-5bef-4004-8cd5-e8cf078bcb5f].

Instruction bus fault memcheck (bus_imem_fault)

The bus_imem_fault check adds a memory abstraction containing a single always-faulting word of memory at an unconstrained address. The check verifies that executing an instruction from this address raises an "instruction access fault" trap.

The RVFI signalling for the faulting fetch requires an all-zero rvfi_insn value with rvfi_trap set. When RISCV_FORMAL_MEM_FAULT is defined, the associated signals must also be set correctly [evidence: 583772cd-5bef-4004-8cd5-e8cf078bcb5f].

Data bus fault memcheck (bus_dmem_fault)

The bus_dmem_fault check adds a memory abstraction containing a single always-faulting word of memory at an unconstrained address. The check verifies that a read from this address causes a "load access fault" trap and a write causes a "store/AMO access fault" trap.

The RVFI signalling for an instruction causing either fault has rvfi_trap set and does not include a register update or memory write, even if the instruction would have performed one had the memory access not faulted. When RISCV_FORMAL_MEM_FAULT is defined, the associated signals must also be set correctly [evidence: 583772cd-5bef-4004-8cd5-e8cf078bcb5f].

Data bus I/O checks

These checks provide stronger guarantees on data bus accesses that need not hold in general, but typically should hold for I/O memory regions. Depending on the use case, only a subset may be applicable, or some may be applicable only for certain address ranges. The set of memory addresses for which these checks run can be configured using the RISCV_FORMAL_IOADDR(addr) macro [evidence: 583772cd-5bef-4004-8cd5-e8cf078bcb5f].

The data bus I/O checks include:

  • bus_dmem_io_read — Ensures that every retired non-faulting I/O memory read access appears as an individual read on the bus. The whole read must appear on its own in a single RVFI_BUS cycle, although reading adjacent bytes within the same RVFI_BUS cycle is permitted [evidence: 583772cd-5bef-4004-8cd5-e8cf078bcb5f].
  • bus_dmem_io_read_fault — Ensures that every retired faulting I/O memory read access appears as an individual faulting read on the bus [evidence: 583772cd-5bef-4004-8cd5-e8cf078bcb5f].
  • bus_dmem_io_write — Ensures that every retired non-faulting I/O memory write access appears as an individual write on the bus. The whole write must appear on its own in a single RVFI_BUS cycle and may not write any additional adjacent bytes [evidence: 583772cd-5bef-4004-8cd5-e8cf078bcb5f].
  • bus_dmem_io_write_fault — Ensures that every retired faulting I/O memory write access appears as an individual faulting write on the bus [evidence: 583772cd-5bef-4004-8cd5-e8cf078bcb5f].
  • bus_dmem_io_order — Ensures that all I/O memory accesses appear in order on the bus. The check verifies that every pair of adjacent I/O memory accesses (as observed via RVFI) corresponds to adjacent I/O memory accesses on the bus. Non-I/O accesses are ignored and may be arbitrarily reordered relative to I/O accesses and to each other [evidence: 583772cd-5bef-4004-8cd5-e8cf078bcb5f].

Relation to the superseded checks

The bus memcheck checks render the legacy instruction memcheck and data memcheck checks obsolete. The older instruction memcheck had added a memory abstraction that emulated a single read-only word of memory at an unconstrained address, verifying that instructions fetched from it were handled correctly and that data from that memory word propagated into rvfi_insn unchanged; the older data memcheck had added a similar read/write single-word abstraction, testing whether writes to and reads from the location (as reported via RVFI) were consistent. Both are explicitly noted as superseded by the equivalent standard bus checks [evidence: 9adf98b4-b25d-4071-b16a-6d418db8e707].

LINKED ENTITIES

3 links
memory abstraction PART_OF
instruction memcheck DERIVED_FROM
data memcheck DERIVED_FROM

CITATIONS

10 sources
10 citations
[1] Bus memcheck checks add a memory abstraction that emulates a single word of memory at an unconstrained address, and are part of the broader memory abstraction machinery used by riscv-formal. Verification procedure - RISC-V Formal documentation
[2] The earlier Instruction memcheck and Data memcheck checks are superseded by the equivalent standard bus checks. Verification procedure - RISC-V Formal documentation
[3] The bus_dmem check tests that writes and reads reported via RVFI are consistent with a single read/write word at an unconstrained address, that an initial value as reported via RVFI matches the fetched bus value, and that it does not require writes to appear on the bus, making it cache-compatible. Verification procedure - RISC-V Formal documentation
[4] The RISCV_FORMAL_FAULT_WIDTH macro must be defined when the granularity of access faults as observed from the core is coarser than the width of the bus (e.g., a cache-line granularity). Verification procedure - RISC-V Formal documentation
[5] The bus_imem_fault check adds a single always-faulting word of memory and verifies that executing from that address raises an 'instruction access fault' trap, with RVFI signaling rvfi_trap and an all-zero rvfi_insn. Verification procedure - RISC-V Formal documentation
[6] The bus_dmem_fault check verifies that a read from the faulting address causes a 'load access fault' and a write causes a 'store/AMO access fault', with RVFI signaling rvfi_trap and no register update or memory write. Verification procedure - RISC-V Formal documentation
[7] When RISCV_FORMAL_MEM_FAULT is defined, the bus_imem_fault and bus_dmem_fault checks require the associated fault signals to be set correctly. Verification procedure - RISC-V Formal documentation
[8] The data bus I/O checks (bus_dmem_io_read, bus_dmem_io_read_fault, bus_dmem_io_write, bus_dmem_io_write_fault, bus_dmem_io_order) provide stronger guarantees for I/O memory regions and can be configured for specific addresses via the RISCV_FORMAL_IOADDR(addr) macro. Verification procedure - RISC-V Formal documentation
[9] bus_dmem_io_read requires that every retired non-faulting I/O memory read appears as an individual read in a single RVFI_BUS cycle, and bus_dmem_io_write requires that every non-faulting I/O memory write appears individually in a single RVFI_BUS cycle without writing adjacent bytes. Verification procedure - RISC-V Formal documentation
[10] bus_dmem_io_order checks that every pair of adjacent I/O memory accesses observed via RVFI corresponds to adjacent I/O memory accesses on the bus, ignoring non-I/O accesses. Verification procedure - RISC-V Formal documentation