This course built DCRouter's verification in the order a course teaches: stimulus, then checks, then coverage, then proofs. A real project would have started with the plan. This lesson writes that plan, using everything Parts 2 to 8 produced, and finds that writing it down shows two features nothing has verified.
What does a complete verification plan for DCRouter look like?
The obvious plan for a block that already catches all 24 planted bugs is "done". But the Bug Zoo is 24 bugs someone thought of; the plan is the list of everything the specification promises. Laying the evidence against the plan, feature by feature, is the only way to see what no planted bug happened to test.
Item | DCRouter |
|---|---|
Design | dcrouter.sv as of this course; Bug Zoo defines excluded |
Specification | Rules R1–R13 and the register table (docs/verification-fp-dcrouter.md) |
Level | Block; SoC concerns listed in Part 8 belong to the integration plan |
Methods | Constrained-random simulation with scoreboard, assertions and coverage; formal proofs for FIFO, arbiter and credits; directed tests for registers and reset |
Done criteria | Every feature has evidence; coverage holes hit, proved unreachable or waived; all 24 Bug Zoo bugs caught; formal properties proved |
ID | Feature | Rule | Risk | Check | Method / evidence | Coverage |
|---|---|---|---|---|---|---|
F1 | Forward whole packets to dst | R3 | High | Scoreboard (4.1) | Covered hunt | Header cross |
F2 | Per-flow order | R3 | High | Per-flow scoreboard | Covered hunt | Back-to-back bins |
F3 | Length 1–15 honoured | R4 | Medium | Scoreboard | Directed + random | len1, len15 bins |
F4 | Length 0 flagged and counted | R5 | Medium | Scoreboard, ERR_CNT read | Error injection | fault len0 bins |
F5 | CRC checked, out_err on tail | R8 | Medium | Scoreboard; out_err assertion | Error injection | fault bad CRC bins |
F6 | FIFO admission and full | R1 | High | Scoreboard; formal count bound | Back-pressure; formal | FIFO full bins |
F7 | Occupancy under push and pop together | R2 | High | Formal pointer invariant | Formal proof | - |
F8 | Round-robin rotation and fairness | R6 | High | Arbitration checker; formal rotation | Hot spot; formal | Contention events |
F9 | Priority when enabled | R6 | High | Arbitration checker; formal winner | Hot spot; formal | CTRL prio_en 1 |
F10 | Priority ignored when disabled | R6 | High | Arbitration checker; formal winner | Hot spot; formal | CTRL prio_en 0 |
F11 | Credits: start at 4, never lost | R7 | High | Formal conservation; credit audit | Formal; audit | out of credits bins |
F12 | Send and return in the same cycle | R7 | High | Formal conservation | Formal proof | - |
F13 | ERR_CNT per input, saturating | R9 | Medium | Read-backs | Error injection; close phase | saturated bins |
F14 | ERR_CNT clear isolation | R9 | Medium | Read-backs of all four | Close phase | cleared bins |
F15 | PKT_CNT per output, simultaneous tails | R10 | Medium | Read-backs | Random; directed | two tails bin |
F16 | PKT_CNT clear | R10 | Low | Read-back | Close phase | PKT_CNT cleared bins |
F17 | CTRL reset value | R11 | Medium | Read before write; register app | Directed | CTRL read before write |
F18 | Unmapped address answers pslverr | R12 | Low | Read and pslverr check | Directed | unmapped bin |
F19 | Disabled port never ready | R1 | High | R1 assertion | Close phase | port disabled bins |
F20 | Sleep after 8 idle cycles | R13 | High | Sleep assertion | Random with quiet gaps | sleep entered |
F21 | Asleep: nothing accepted or sent | R13 | High | Quiet assertion | Random | - |
F22 | Wake from any input | R13 | High | Wake assertion | Random | wake by input k alone |
F23 | Never sleep mid-packet | R13 | High | Mid-packet assertion | Back-pressure, random | - |
F24 | Credits counted while asleep | R13 | High | Formal conservation; audit | Formal; back-pressure | credit returned while asleep |
F25 | Low power disabled | R13 | Medium | Sleep assertion with lp_en 0 | Not yet done | CTRL lp_en 0 (hole) |
F26 | Throughput 1 flit per cycle per output | Perf | Medium | Throughput monitor (not built) | Partial: back-to-back flits in 4.1's waveform | - |
F27 | Bounded waiting (3 others) | Perf | High | Arbitration checker | Hot spot | - |
F28 | Reset mid-traffic | R11 | Medium | Scoreboard flush and reset values | Not yet done | - |
28 features, every one traced to a rule or a performance requirement.
Most high-risk features have two kinds of evidence: arbitration, credits and FIFOs are proved and also checked in simulation.
F25 (low power disabled) has no evidence: lesson 6.6 found "CTRL lp_en 0" as a hole; no test has run with low power off.
F28 (reset in the middle of traffic) has no evidence: no planted bug needed it, so no test was written. It appears only because the plan starts from the specification, not from the bugs.
F26 (throughput) has only partial evidence: lesson 4.1's waveform shows back-to-back flits, but no monitor measures throughput under saturation.
None of these gaps would show in any Bug Zoo result: 24 of 24 caught says nothing about features without planted bugs.
Action | Closes |
|---|---|
A phase with lp_en clear: idle for 50 cycles, assert never sleeping, then traffic | F25 |
A reset asserted mid-packet, then reset values, empty FIFOs, 4 credits and clean traffic | F28 |
A throughput monitor on a saturating test: every output must send one flit per cycle while credits allow | F26 |
Saturate ERR_CNT0, 1 and 3, or record the waiver of lesson 6.6 | F13's remaining holes |
Add these to the nightly regression tier | Keeping them closed (lesson 9.6) |
Practice | Purpose |
|---|---|
The plan as the review document for sign-off | Evidence judged feature by feature (Part 14) |
Evidence columns filled automatically from results | Status computed, not claimed |
Empty evidence cells as the team's task list | Effort aimed at the unproven |
The course itself is the example: four parts of increasingly strong verification, a testbench that catches every planted bug, and still two features nobody tested. A project that measured itself only by its planted bugs, or its coverage model, or its pass rate, would have signed off with both gaps open.
No planted bug involves reset in the middle of traffic, so no test ever needed to do it; only a plan written from the specification lists it.
FIFO occupancy, arbitration and credits: formal proves the rules for all inputs, and simulation exercises them in realistic traffic and catches anything outside the properties.
DCRouter's plan lists 28 features traced to the rules, each with risk, check, method and coverage.
Laying evidence against the plan found two untested features despite 24 of 24 planted bugs caught.
A plan written from the specification is the only place unverified behaviour becomes visible.