RTL verification for semiconductor and RISC-V teams. We investigate design bugs, coverage gaps, and design rules, with evidence your team can inspect and rerun.
We agree the question, inputs, deliverables, and completion criteria before work starts. When a check cannot establish an answer, we record the remaining uncertainty and the next step.
CORE-V investigation reports shows the method applied to real OpenHW CORE-V issues: sixteen public GitHub issues taken to a disposition, each with the evidence, the proof scope, and the limits written down.
Every report follows the clause order used in published silicon errata and anomaly reports: status, description, conditions, implications, action, evidence, limitations and scope, provenance. Where a field was not recorded, it says so rather than being filled in. Ten of the sixteen issues were still open upstream when the reports were published, and none of the reports has been submitted upstream.
Read issue 1010 first. It is three pages: a coverage hole proven unreachable, the two proofs that establish it, the cover that shows the proofs are not trivially true, the waiver text, and what the result does not establish.
These are public educational demonstrations, not client results or production IP. Each repository states its environment and limitations. A deliberately introduced bug is labelled as such.
| Problem to explore | Repository | Evidence to inspect |
|---|---|---|
| A timer write crosses the interrupt threshold at rollover | Historical upstream timer regression | Two ordinary cases pass before and after; five boundary cases fail before the upstream fix and pass after, including a spurious interrupt. Independent reproduction, not our discovery |
| Architectural tests must match the core configuration | RISC-V ACT4 integration | Fresh generation and 94 named RTL test results for pinned CV32E40P v2 RV32IMC; not general certification |
| FIFO pointers or synchronizer staging change incorrectly | Bound FIFO assertions | Concurrent traffic at depths 4/8 and widths 5/8/13; independent flag checks and a stale full-comparator defect; 28 expected outcomes |
| Debug halt and a qualified interrupt arrive together | RISC-V debug and interrupts | Real pinned CV32E40P controller; synthetic temporal faults pass the ordinary regression but fail checks around stalls, exception flush, and debug return |
| A regression reports success with incomplete evidence | Verification automation | Complete result matrices from three pinned RTL projects, source hashes, failure handling, and CI |
Start with the README in a repository. It explains the problem, reproduction command, recorded results, and limits. The repositories include automated runs, measured tool times, and contribution instructions. Tool runtimes are not client delivery estimates. Scenario counts are not code coverage or proof of all behaviour.
These compact teaching designs explain individual checks and testbench tools. They are not evidence of complex IP verification.
| Problem to explore | Repository | Evidence to inspect |
|---|---|---|
| A receiver pauses while data is waiting | Ready/valid buffer | Data stability, ordered transfers, backpressure, and a detected seeded defect |
| Reset arrives while requests are still pending | Reset recovery | Flush contract, recovery, and detection of a stale response |
| One requester keeps losing access to a shared resource | Round robin arbitration | Grant safety and bounded waiting in accepted grants, tested against a fixed priority mutant |
| A controller must keep two directions mutually exclusive | Formal FSM | Safety proof and reachability checks under the documented model |
| UVM classes need to run and detect a wrong result | Executed UVM ALU | Three seeds with 200 scoreboard matches each, plus a detected injected mismatch; no class-covergroup coverage claim |
| A testbench needs to predict the correct answer | Python ALU testbench | Reference model, directed and random tests, and operation counts |
| A timer interrupt disappears after its compare value | RISC-V machine timer | Seeded failure, simulation, formal counterexample, checked correction, and coverage dispositions |
| A random test misses corruption when a FIFO fills | Asynchronous FIFO | Directed failure on a seeded variant and passing functional tests at three clock pairs |
- RISC-V verification: investigate a defined architectural or subsystem requirement, with the tested configuration and limits recorded.
- RISC-V architectural tests (ACT4): pinned test generation, simulator integration, and a complete result matrix for the agreed core configuration.
- Debug, interrupt, and exception verification: directed checks of agreed control interactions. The public controller example does not establish whole-core debug compliance or CSR masking behaviour.
- Verification automation: reproducible regression execution and validation of complete, current evidence.
- Bug reproduction and root cause: a replayable failure when one can be found, a cause analysis, and checks of a proposed correction.
- Coverage closure: investigate gaps and record directed tests, proofs, supported waivers, or unresolved outcomes.
- Formal verification and SVA: design properties, assumptions, counterexamples, proof scope, and reachability checks.
- Simulation environments: cocotb or UVM stimulus, reference models, automatic checking, and supported coverage or scenario reports for an agreed scope.
- Asynchronous FIFO verification: functional checks for loss, duplication, and reordering across the tested clocks and reset conditions, plus bound pointer and synchronizer assertions where agreed. This does not replace structural CDC analysis or electrical sign off.
The SVA library remains a code reference with lint results, not a completed formal proof. The original UVM ALU source now links to the separate pinned execution runner above, which documents its simulator compatibility and coverage limitations.
Open an issue with the repository revision, tool versions, command, expected behaviour, and actual log. For a proposed correction, include a test that fails before the change and passes after it. Do not upload proprietary RTL or client information to these public repositories.
Confidential work begins with an agreed scope, NDA, and source exchange process.