State the case, model subset, initial values, observation boundary and selected protocol/system rule.
List accepted requests, accepted data/responses, live queues and explicit cancellation. Distinguish an offered response from a handshake.
Mark the first observable divergence. Name the additional internal observation that would distinguish the leading implementation hypotheses.
Propose the smallest correction, state what legal behaviour it preserves and specify a negative stimulus that would detect recurrence.
Provide a clean control and the same failing replay after repair. Record real execution output, source revision, accepted work and remaining limitations.
Selection | Required harness result | What that does not mean |
|---|---|---|
CASE=0 | Nonzero baseline work, no diagnostic violation, queues drained or explicitly cancelled. | Not proof of a complete AXI implementation. |
CASE=1..5 (A..E) | Each selection produces its intended diagnostic only; harness checks the expected rejection. | A harness PASS does not mean a faulty selection was accepted as correct. |
Clean replay after each selection | The baseline with the mutation disabled passes for the same initial-data seed. | Not an automatic test of a learner's separate patch. |
Default campaign | All selections at three initial-data seeds, with nonzero work and clean replays. | Not exhaustive timing, concurrency, reset or CDC verification. |
A reviewer can provide the compiled bus-lab.vvp without the source. With that artefact, vvp bus-lab.vvp +CASE=0 selects the baseline and +CASE=1 through +CASE=5 select A through E. Detailed event logging uses the default initial-data seed; the harness also audits two changed-data seeds. Numeric diagnostic masks are implementation reports; make your diagnosis from the observed events first.
The executable source and build commands are deliberately on Solutions. Their presence does not imply execution has passed. A complete review must also compare the hand-constructed evidence fixtures with actual logged events.
The response and request accounting balances, including the cancelled pre-reset read.
Each case has a falsifiable rule and discriminator, rather than only a component name or a larger timeout.
Counterexamples are detected while legal W-before-AW, stalled offers, cross-ID returns and post-reset traffic remain legal.
Source compilation, execution and rendered-page checks have real recorded results; authored code is still pending until then.
Open Solutions only after completing the investigation — spoilers