mmu-verification

Verification of a three-port RISC-V Sv39 memory-management unit. The testbench is UVM on Verilator with a DPI-C reference model. Checking uses scoreboarding and concurrent assertions plus functional coverage. Formal sign-off comes from SymbiYosys k-induction proofs and directed bug injection.

DUT

rtl/ implements a small but real MMU.

• Three translation ports driven by UVM agents issuing mixed traffic.
• Sv39 address translation with canonical-address checking.
• A shared set-associative TLB (8 sets x 4 ways) with per-set tree PLRU. Every lookup probes leaf levels 0 through 2 in parallel. Entries carry ASID tags and a global bit.
• One hardware page-table walker per port (rtl/ptw.sv). Walkers share a single memory-read port behind a grant-locking round-robin arbiter (rtl/rr_arbiter.sv).
• sfence.vma-style invalidation over four shapes (all entries, VA only, ASID only, VA+ASID).
• U/S privilege checks plus sstatus.SUM and sstatus.MXR handling. Svade A/D semantics: a leaf with A=0, or a store to a leaf with D=0, raises a page fault. Hardware never writes PTEs back.
• Malformed PTEs (V=0, W without R, reserved bits set), misaligned superpages, and memory access faults surface as the correct fault response.

The design is self-contained. tb/mem_slave.sv serves walker page-table reads from a C++ memory image and can inject access faults per address.

Verification environment

• model/mmu_ref.cpp. DPI-C reference model. Every retired transaction is re-walked through the same image the hardware read. The scoreboard compares PA plus fault and cause fields.
• tb/classes/, the UVM environment. Agents drive and sample the ports. A scoreboard checks every transaction. A page-table generator builds a random image per test. The image holds mapped pages at all three Sv39 leaf sizes. It also holds malformed leaves and error-injection pages plus pools for unmapped or non-canonical VAs.
• sva/, bind files with concurrent assertions. Arbiter properties cover one-hot grants and grant-lock stability. TLB properties cover fill-visibility and invalidation. MMU-level properties cover response behavior.
• formal/. Yosys-friendly behavioral models of the arbiter and TLB with embedded properties, plus .sby files driving smtbmc z3 BMC and k-induction.
• tests/, six UVM tests named rand, warm, fault, bare, thrash, inv.
• scripts/, runner and report tooling.

Toolchain

• Verilator 5.053 (OSS CAD Suite 20261030) for simulation and coverage.
• The antmicro UVM-for-Verilator port (uvm-verilator, UVM 2017).
• Yosys 0.70 + SymbiYosys + Z3 for formal work.
• Python 3 for the runners.

scripts/toolchain.sh puts the suite on PATH. The sim binary shells out to z3 for constrained randomization at run time, so z3 must stay on PATH whenever a sim executes.

Reproduce

source scripts/toolchain.sh

# build + smoke test
scripts/build_sim.sh sim_build
./sim_build/mmu_sim +verilator+seed+1 +UVM_TESTNAME=mmu_rand_test

# regression: six tests x 100 seeds, per-run logs, merged coverage
python3 scripts/run_regression.py --seeds 100 --out results/regression

# formal: BMC + k-induction on the arbiter and TLB models
cd formal && sby -f arbiter.sby && sby -f tlb.sby

# bug injection: 12 RTL mutations x 6 tests x 5 seeds
python3 scripts/run_mutations.py --seeds 5 --out results/mutations

# coverage closure report from a merged .dat
python3 scripts/coverage_report.py results/regression/coverage_merged.dat \
    results/regression/coverage_report.md

Results

See results/ for the raw artifacts and docs/testplan.md for the feature matrix the numbers map onto.

• Simulation: six UVM tests x 100 seeds, summarized in results/regression/summary.txt. Each run ends with a RESULT checks=N failures=M line. Zero failures across the regression.
• Functional coverage: merged per-seed data meets the closure targets in docs/testplan.md. Per-coverpoint bins are listed in results/regression/coverage_report.md.
• Formal: formal/arbiter_prove and formal/tlb_prove pass k-induction under smtbmc z3 (logs under results/formal/). The TLB proof runs on a 4-set x 2-way instance of the same logic to keep the SMT state space tractable.
• Bug injection: results/mutations/ holds 12 targeted mutations. The suite kills the correctness-visible ones. Survivors are documented. Each is either fairness-only or stimulus-unreachable.

What the bug-injection study caught

Survivor analysis is part of the deliverable. Three mutations initially survived because the page-table generator packed PTE fields into the wrong bit positions. The DUT and the C++ model decoded the same nonstandard word, so walks agreed while never descending past the root level. Fixing the generator's make_pte packing made multi-level translation real. It turned previously surviving mutations into kills and exposed coverage bins that had been structurally unreachable. A scoreboard that only compares end-to-end results can ratify a degenerate environment. Mutation survivors are the cheapest place to notice.

Layout

rtl/        synthesizable DUT
tb/         UVM harness, interface, memory slave
tb/classes/ agents, driver, monitor, scoreboard, coverage, ptgen
tests/      UVM tests
sva/        bind files with concurrent assertions
formal/     Yosys-compatible models + .sby proofs
model/      DPI-C reference walker + memory image
scripts/    build, regression, mutation, coverage tooling
results/    captured regression, coverage, formal, and mutation artifacts
docs/       testplan and feature matrix

Known limits

• The formal TLB proof uses a reduced instance (4 sets x 2 ways). The logic is identical, but the largest configuration was not proved end-to-end.
• Unbounded liveness (no request starves forever) is unproven. The suite's AIGER liveness flow needs super_prove, which the installed toolchain lacks. A bounded starvation bound is proved instead, under a bounded-fairness assumption on the memory port.
• The equivalence build swaps the formal views in for the production modules and reruns the UVM suite. It is a smoke-level argument rather than a proof of translation between the two views.