Coherex

A four-layer verification environment for a 4-core snoopy MESI cache-coherence cluster: exhaustive protocol model checking before the RTL exists, cycle-accurate invariant checkers, litmus tests judged against an exhaustive sequential-consistency oracle, and mutation qualification that proves the whole thing can actually fail.

The design under test is a means to an end. The deliverable is the verification.

---

Why four layers

A coherence protocol has two kinds of bug, and they need opposite tools.

A specification bug means the state table itself is wrong — every faithful implementation of it is equally broken, and no amount of simulation will tell you so. An implementation bug means the table is right and the RTL does not follow it. Simulation cannot find the first and is the only thing that finds the second.

	Question	Method
Layer 0	Is the protocol correct?	exhaustive BFS over the state space, in Python, before any RTL
Layer 1	Does the RTL follow it?	invariant checkers reading cache state every cycle
Layer 2	Does the cluster implement SC?	litmus tests vs an exhaustive SC oracle + axiomatic graph check
Layer 3	Would any of this notice a bug?	mutation qualification against a catalog of real defects

Layer 3 is what makes the rest mean anything. Layers 0–2 going green proves the environment did not complain. Only Layer 3 shows it can.

The two arrows worth following are the dotted ones. mesi_spec.py is the only place a state is named, so the model checker, the RTL defines and the coverage report cannot drift apart without the encoding cross-check saying so. And Layer 3 points backwards: it breaks the RTL on purpose and re-runs Layers 1 and 2 against it, so a mutant that lives is a missing checker, not a tolerable score.

Results

Full breakdown — every test, bin and mutant — in docs/RESULTS.md. The summary below is the headline; that document has the per-test outcome diversity table, the per-mutant kill grades, and the counterexample lengths for all 10 Layer 0 defects.

Every number below is reproduced by make -C sim all, and by CI on every push. The three badges above are three separate workflows, one per layer, so a failure names itself without anyone opening a log. Coverage and mutation are gates, not reports: an uncovered required bin, a hit on a protocol-illegal bin, or a single surviving mutant fails the build.

Layer 0 — exhaustive protocol model check

Caches	Reachable states	Result
2	110	PASS
3	520	PASS
4	2,330	PASS

All 10 catalogued defects are rejected by the model's own invariants (10/10), with counterexample traces 3–7 steps long.

Layer 2 — litmus regression — 55/55 tests, 715 runs, 96,362 cycles, 3,411 bus transactions. 43 catalog tests (14 shapes × 3 address maps, plus a directed eviction race) and 12 randomly generated ones, each replayed across 13 stall/skew configurations and judged four independent ways.

Functional coverage — 81/82 legal bins, 98.8%, with group F (the transient-window corner events) at 12/12. No illegal bin was ever hit; the coverage model treats that as a failure, not a gap.

Layer 3 — mutation qualification — 11/11 mutants killed (100%), each facing the same regression the clean design passed. Two of them survived the first run, and neither was fixed by tuning stimulus: each survived because a property was not being checked at all, and each produced a new checker (bus fairness counted in grants rather than cycles, and rules R1/R2 checked directly rather than through their eventual data corruption).

A real bug, found

Not injected — found, by Layer 1's DV1 invariant:

A store that hits a line in M could commit on the same clock edge the bus latched that line's pre-store contents for a snoop. The bus carried the old value away, the cache array kept the new one, and the M→S demotion one cycle later left two caches sitting in S holding different data — with rule R3 having already written the stale copy back to memory.

The guard for this existed and covered PH_SNP, the cycle the snoop commits. The response is sampled a cycle earlier, in PH_REQ. Layer 0 could not have found it: in an atomic model there is no "same edge".

It only became reachable after the stimulus was fixed (below). A green regression was hiding a real data-corruption bug behind a stimulus bug.

Outcome diversity is a first-class metric

The regression reports seen/SC — how many distinct SC-legal outcomes a test's whole sweep actually produced, out of how many are legal. A litmus test whose sweep yields one outcome is not being raced, no matter how green it looks.

That metric earned its place twice:

1. All four cores were released from a single start signal, so every core issued its first request on the same cycle, the round-robin pointer resolved that tie identically every run, and the arbiter then forced strict alternation forever. 42 tests passed. Every one was exercising exactly one interleaving.
2. The fix — a seeded per-core start stagger — appeared to work and did not. Every seed in the sweep is 16-bit, and the stagger hash read bits above the seed's significant range, so core 1 led in every single run and the arbiter pointer seeding (seed[17:16]) was constantly zero.

Both were invisible to every pass/fail check in the project. Only the diversity column could see them.

Layout

model/    Layers 0, 2 and 3, plus the coverage model — all Python, no deps
  mesi_spec.py         the protocol as data; single source of truth
  mesi_model_check.py  Layer 0 exhaustive BFS + bug rejection
  litmus.py            test catalog, assembler, random generator
  sc_oracle.py         exhaustive SC enumeration + axiomatic po∪rf∪co∪fr check
  run_litmus.py        Layer 2 regression driver
  coverage.py          functional coverage model and report
  mutate.py            Layer 3 mutation qualification
  simrun.py            simulator plumbing (native or WSL Icarus)
rtl/      the DUT: 4 × MESI L1 + atomic snoop bus + memory (Verilog-2001)
tb/       BFMs, invariant checkers, coverage collector
  sva/    a SystemVerilog restatement of the rules (see the caveat below)
sim/      Makefile, Icarus script, ModelSim script
docs/     SPEC.md, VERIF_PLAN.md, RESULTS.md
  img/    the layer diagram: layers.mmd is the source, the two .svg files
          are what the README shows (light and dark)

Documentation

docs/RESULTS.md	Every measured result, with the reasoning behind each number — and the bugs, stimulus bugs and mutation survivors that were found on the way to them.
docs/SPEC.md	The protocol the RTL, the model checker and the checkers all implement: states, phases, the four rules, the invariants, and the memory model.
docs/VERIF_PLAN.md	What each layer is for, why there are four of them, what CI runs, and where the coverage is knowingly thin.

Running it

Needs Python 3.8+ and Icarus Verilog — no Python packages beyond the standard library. On Windows, model/simrun.py finds Icarus inside WSL automatically and translates the paths, so the Python drivers run natively from Windows while the simulator runs in WSL.

make -C sim all

Or one layer at a time:

make -C sim model      # Layer 0, no simulator needed
make -C sim litmus     # Layer 2 regression
make -C sim cov        # coverage report for the last regression
make -C sim mutate     # Layer 3 mutation qualification
make -C sim smoke      # fast subset

Git Bash on Windows has no make; run the targets from WSL, or call the drivers directly — which is how you debug a single point anyway:

cd model && python run_litmus.py -k MP --all

Honest limitations

• The SVA layer is not evaluated here. tb/sva/coherex_sva.sv compiles and elaborates clean, but ModelSim ASE reports "System Verilog assertions are supported only in Questasim" and never evaluates the properties. It is a formal-ready restatement of the rules; the procedural checkers are what carry the verification, and no reported result comes from the SVA.
• IRIW, QUAD and UPGRACE reach a minority of their legal outcomes (5/15, 7/15, 11/256). With four threads the SC-legal set grows factorially while the DUT's reachable schedules are bounded by a 3-cycle atomic bus. The numbers are printed rather than hidden.
• Layer 0 is atomic. It has no arbiter and no clock edges, so it structurally cannot model BUG_ARB_FIXED_PRIO or the same-edge bug described above.
• Only 3 of 11 mutants are killed black-box. Seven are killed only by white-box probes into cache arrays that real silicon does not have, and one is a pure liveness kill. mutate.py grades kills by class and reports them separately rather than averaging them into a single score.
• Five checks in bus_protocol_checker.v have never fired. PH (phase-sequence), ACT (bus_active consistency), GNT (grant validity), SUP (multiple simultaneous suppliers) and STRV (starvation) all have zero hits across every mutant and the whole litmus regression — confirmed by grepping results/mutation.json. For PH/ACT/GNT this is structural: no mutant in the catalog touches the phase FSM, bus_active, or the arbiter's request-wiring, so those checks currently audit logic nothing perturbs. SUP is a near-miss — the one mutant that duplicates a line (GETS_ALWAYS_E) puts the duplicate in E, which HAS_DATA excludes from supplying, so it trips EXCL/SWMR/DV1 instead. STRV's 2000-cycle threshold is simply longer than any run: the whole regression totals 96,362 cycles, roughly 170 per test, and ARB_FIXED_PRIO (the mutant built to starve a core) is caught by the bus checker's tighter FAIR bound (NCORE grants) long before age could climb that far. A targeted mutant for each — a stuck phase register, a bus_active stuck-at, two owners answering one snoop, a request that never clears — is the honest next step; inventing one badly risks a checker that looks qualified without being qualified, which is worse than leaving the gap named. HANG (op-count-not-retired) is in the same position for a different reason: mutate.py's docstring used to claim it was the only thing that could see ARB_FIXED_PRIO, but the recorded run shows FAIR catches it first every time, so HANG has never actually killed a mutant either.
• **NCORE=4 is a real define but not a real parameter.** The RTL, the checkers and Layer 0 are genuinely NCORE-generic — they loop 0..NCORE-1. tb_cluster.v's program-loading and result-dump tasks and the Python driver (litmus.py, run_litmus.py) are not: they are four hand-written cases, one per core, coupled to the RTL's core count only by everyone happening to write 4. Changing NCORE` would compile and simulate a cluster with a different core count and silently stop loading, or reporting, the results for whichever cores the testbench does not name.
• Two small infra gaps in model/simrun.py, both left as named gaps rather than fixed. _discard() kills the Windows-side wsl.exe front-end when a pooled shell times out or dies, but not whatever it was running inside WSL (e.g. a still-running vvp) — that child is orphaned, not reaped, because the pool does not track the WSL-side PID. And build()'s name parameter defaults to the same string for every caller that does not override it, so two concurrent builds left at the default could interleave writes to the same sim/build/coherex.vvp. Neither bites the project's own tooling — mutate.py always passes a per-mutant name, and shells are only discarded on rare timeout/death — so both are documented rather than fixed under time pressure that would not let either be verified properly.