From a missed timer interrupt to a verified fix
A RISC-V machine timer with a seeded bug, taken from failing test to counterexample, root cause, proven fix, and closed coverage holes.
Public demonstration
This is not a client result. The recorded command and check status appear below.
Recorded outcome
Before the fix, 2 of 5 tests fail and formal returns a counterexample. After the fix, 7 of 7 tests pass and the property is proven for every reachable state. Of four coverage holes, two are reached by new tests, one is proven unreachable, and one is waived with a checked constraint.
What was checked
- Problem
- A bug report says the timer interrupt is sometimes missed when the core has interrupts disabled. The RISC-V privileged specification requires the interrupt to stay pending while mtime is at or past mtimecmp. The existing regression passed.
- Scope
- One machine timer block with mtime and mtimecmp registers, a clock prescaler, and a debug halt input. The bug is seeded on purpose. The work covers the bug report and the coverage holes the old regression left.
- Approach
- Two tests written from the specification reproduce the failure in simulation. A formal property stating the same requirement returns a counterexample on the buggy RTL. After the fix, four coverage holes are each reached by a directed test, proven unreachable, or waived with a z3 check of the firmware limits.
- Evidence
- Committed in the repository: simulation logs before and after the fix, the counterexample trace, coverage reports before and after, the proof log, cover results showing every property is exercised, a check that each assertion fails when the design is wrong, and the z3 waiver results.
Scope and limits
What these checks do not establish.
- The block is small and the bug was seeded on purpose. It shows the method, not a result on a production RISC-V core.
- The waiver holds only if the firmware driver is the only code that writes the prescaler register and every board stays inside the stated clock limits.
- Line coverage shows which lines ran, not that their behaviour was checked. The checking comes from the tests and the properties.
- The property excludes the wrap of mtime from all ones to zero, which takes 2^64 counts.
Reproduce and inspect
Recorded verification status
We ran scripts/reproduce.sh from a fresh clone on 13 September 2026: 23 of 23 checks passed, with SymbiYosys git b1a1e98, Yosys 0.67+post, z3 4.16.0, Verilator 5.050, and cocotb 2.1.0.
pip install -r requirements.txt
scripts/reproduce.shrtl/mtimer.svdesign, +define+SEEDED_BUG selects the bugformal/mtimer_props.svhproperties and cover checksformal/mtimer.sbybug_bmc, prove, cover tasks with z3tb/test_bug_report.pytests written from the bug reportwaiver/div_never_zero.smt2 z3 check behind the waiverscripts/reproduce.shreruns every step, checks 23 resultsevidence/logs and trace from a fresh clone runWant this method on your design?
Share the problem in a few lines. We will discuss the scope before any confidential project material changes hands.
Discuss a verification problem