Overview

Data memcheck is a verification check used in the riscv-formal framework to validate the data memory portion of a RISC‑V core. It is part of the suite of "other checks" that are not yet managed by genchecks.py and that cannot be implemented using the standard RVFI wrapper interface alone.

Mechanism

The check works by instantiating a small memory abstraction that emulates only a single word of memory. The address of that word is left unconstrained, and the word itself is read/write (in contrast with the read‑only word used by the related instruction memcheck). With only this minimal memory in the model, any data‑path transactions the core issues necessarily hit the modeled word, allowing the check to focus on the load/store logic in isolation.

The role of the check is to test whether writes to and reads from the memory location, as reported through RVFI, are consistent. By comparing the data written to the modeled word against the data later read back (as observed on the RVFI signals), the check can detect mismatches between the core's view of memory and the abstract model's view of memory.

Reference implementation

A canonical implementation of the check is provided in the riscv-formal examples:

• dmemcheck.sv in cores/picorv32/

This file is referenced in the riscv-formal documentation as "one possible implementation of this test."

Status and relationship to the standard bus check

The data memcheck is now considered a legacy check: it has been superseded by the equivalent standard bus check described elsewhere in the riscv-formal procedure documentation. The standard bus check provides a more general and reusable mechanism for the same class of consistency verification, and the single‑word data memcheck is retained primarily as historical context and as a worked example.

Use of RVFI

The check relies on RVFI (the RISC‑V Formal Interface) to observe the loads and stores issued by the core and to determine whether the data values flowing through those transactions are coherent with the abstract memory model. RVFI is therefore an essential input to the consistency comparison that the check performs.

See also

• Instruction memcheck — the read‑only analogue that targets the instruction fetch path instead of the data path.
• Bus memcheck — the standard successor check that supersedes data memcheck.
• Memory abstraction — the underlying modeling primitive that data memcheck instantiates.
• RVFI — the formal interface through which loads and stores are observed.