RISC-V verification
Turn an architectural requirement or failure report into checks your team can inspect and rerun.
How the check works
Start with one architectural question.
Define the rule
Identify the required behaviour and its configuration or software assumptions.
Exercise the RTL
Use tests or properties to expose a violating sequence.
Hand over the evidence
Record the result, proposed correction, and remaining limits.
Concept illustration. The public timer demonstration covers a small subsystem. Whole-core verification requires a separately agreed scope.
What you receive
- A test plan tied to the agreed architectural requirement.
- Reproduction scripts, run settings, and evidence for observed failures.
- Checks of the proposed correction and any remaining unknowns.
- A handover stating the tested revision, assumptions, and limits.
When this is useful
- A RISC-V subsystem behaves differently from the requirement or reference model.
- An interrupt or control sequence needs a short, reproducible test.
- You need evidence for a specific processor integration question.
Problem, approach, and required inputs
The problem
A processor can run software while still mishandling an interrupt, a register update, or an unusual control sequence. You need to separate what the architecture requires from the assumptions made by the testbench.
What we do
We define the architectural rule and its conditions, then exercise the relevant RTL using directed simulation or formal checks where appropriate. We investigate mismatches, check proposed corrections, and record the result and its limits. The agreed scope states whether the work covers a small subsystem, a controller, or an integrated processor.
Inputs agreed after scoping and NDA
- The core or subsystem revision, configuration, and relevant specification.
- A failure report or a defined behaviour to investigate.
- The simulator, testbench, and software environment available to the project.
Related public demonstration
Public demonstration, not a client result
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.
More problems you can reproduce
Technical details
How the result is checked
Our machine timer example follows a deliberately seeded interrupt bug through simulation, a formal counterexample, a checked correction, and coverage analysis. It demonstrates subsystem verification; it is not a claim that an entire RISC-V core is verified.
Tools used for this kind of work
- SystemVerilog
- Verilator
- cocotb
- SymbiYosys
- Yosys
- z3
Scripts are handed over as agreed in the scope. If we have not tested your simulator or flow, the scope says so.
Discuss this problem.
Tell us what you are trying to verify and what is blocking you. A person replies, and the scope comes back in writing after a call.
Discuss a verification problem