A brief halt request is lost at a control boundary

Ordinary tests pass, but requests arriving during a stall, exception flush, or debug return expose seeded faults in a real RISC-V controller.

Open the repository on GitHub

Checks passed

Public demonstration

This is not a client result. The recorded command and check status appear below.

Recorded outcome

All five variants pass the ordinary suite. The original controller passes the temporal suite and all ten timing cases. Four synthetic faults fail their targeted checks while passing ordinary and adjacent timing controls. The full matrix requires thirty expected outcomes.

What was checked

Problem: A one-cycle halt request must survive until the controller can service it. Qualifying its storage with the wrong instruction or debug state can lose it, allowing another event to take priority.
Scope: The actual pinned CV32E40P controller with default feature parameters. The matrix varies decode stalls of 0, 1, and 3 cycles and halt pulses before, during, and after exception flush and debug return. It checks request retention, causes, redirects, restore, and interrupt priority.
Approach: The original ordinary regression runs on unchanged RTL and four synthetic variants. All pass it. Targeted temporal checks then expose validity gating, exception-flush gating, and debug-return gating errors. The runner requires the exact intended diagnostic and rejects unrelated or duplicate failures.
Evidence: The repository retains ordinary and temporal logs, exact source and mutant hashes, log hashes, compile commands, and durations. The upstream checkout remains unchanged. The mutations are synthetic controls, not discovered CV32E40P defects.

Scope and limits

What these checks do not establish.

This is controller-level simulation, not execution of software on a complete processor or a formal proof.
The interrupt is already qualified by external logic. CSR masking, pending-latch implementation, and trap storage are not verified.
Pipeline signals are driven at the module boundary with one shared clock. The recorded progress assumptions are part of the result.
Fetch faults are supplied as inputs. The detector and complete exception return are outside these checks.
JTAG, DMI, nested traps, gated-clock behaviour, nondefault feature branches, and architecture compliance are outside this example.

Reproduce and inspect

Recorded verification status

Implementation 996cb0d uses unchanged OpenHW CV32E40P source 6033d2b. Independent reproduction on 15 September 2026 checks fifteen builds and thirty simulation outcomes, including twenty boundary cases. Eleven runner regression tests pass. Exact commands, observations, and source and log hashes are recorded.

Recorded commandriscv-debug-interrupt-verification

git clone https://github.com/Rivoryxa-Technologies/riscv-debug-interrupt-verification
cd riscv-debug-interrupt-verification
# Requires Python 3, Git, Verilator, make, and a C++ compiler.
./setup.sh
python3 tools/test_runner.py

Filestb/controller_debug_irq_smoke_tb.svretained ordinary baselinetb/controller_debug_irq_tb.svtemporal interactionstb/controller_boundary_matrix_tb.svstall and pulse-position matrixtools/run.pyexact outcomes and observed metadata validationrecorded/2026-09-15-temporal-v3/reviewed source and result hashes

Next steps

Service: RISC-V verification Service: Debug, interrupt, and exception verification Other examples

Want 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