diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ac0a58d0..83da121b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -72,4 +72,30 @@ jobs: . venv/bin/activate python3 -m pip install --upgrade pip python3 -m pip install -e .[test] - pytest -m "not switchboard and not cocotb" -n logical --verbose + pytest -m "not switchboard and not cocotb and not formal" -n logical --verbose + + + formal_ci: + name: "Formal CI" + runs-on: ubuntu-latest + container: + image: ghcr.io/siliconcompiler/sc_tools:latest + timeout-minutes: 45 + + steps: + - name: Checkout repository + uses: actions/checkout@v7 + with: + fetch-depth: 0 + + # the sc_tools image already ships yosys + sby + boolector, so the + # formal lane runs here with no extra tool-install step; z3 and + # bitwuzla are absent, so those local-evidence rows skip cleanly + - name: pytest + run: | + git config --global --add safe.directory "$GITHUB_WORKSPACE" + python3 -m venv venv + . venv/bin/activate + python3 -m pip install --upgrade pip + python3 -m pip install -e .[test] + pytest -m "formal" --durations=0 diff --git a/pyproject.toml b/pyproject.toml index 619c7e4f..d91be80a 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -56,7 +56,8 @@ ignore = [ markers = [ "eda: this test requires EDA tools installed to run", "switchboard: this test requires switchboard to run", - "cocotb: this test requires cocotb to run" + "cocotb: this test requires cocotb to run", + "formal: this test requires SymbiYosys (sby) to run" ] pythonpath = [ "tests" diff --git a/tests/sumi/test_formal.py b/tests/sumi/test_formal.py new file mode 100644 index 00000000..70c63e16 --- /dev/null +++ b/tests/sumi/test_formal.py @@ -0,0 +1,115 @@ +"""Formal property proofs (SymbiYosys) as a pytest lane. + +Each proof under umi/formal/ is a harness (fv_.sv) plus a job +file (fv_.sby). This runner shells out to sby: ordinary tasks +must PASS, fault_* tasks inject a bug and must FAIL. Skips unless the +formal toolchain is on PATH, so other CI lanes are unaffected. +""" +import shutil +import subprocess +from pathlib import Path + +import pytest + +FORMAL_SUMI = Path(__file__).resolve().parents[2] / "umi" / "formal" / "sumi" + +# sby drives yosys; the green tasks run the boolector engine, which is +# always present in the sc_tools CI container. z3 and bitwuzla are extra +# solvers used only for the local dual-solver evidence and are skipped +# per-row (see below) when the solver is not on PATH. +_TOOLS = ("sby", "yosys", "boolector") +# the prove_z3 rows need z3 and the two fv_umi_txn *_bw rows need +# bitwuzla; skip just those rows when the solver is absent so the rest of +# the lane still runs on boolector alone +_HAVE_BITWUZLA = shutil.which("bitwuzla") is not None +_needs_bitwuzla = pytest.mark.skipif(not _HAVE_BITWUZLA, + reason="bitwuzla not on PATH") +_HAVE_Z3 = shutil.which("z3") is not None +_needs_z3 = pytest.mark.skipif(not _HAVE_Z3, + reason="z3 not on PATH") + +pytestmark = [ + pytest.mark.formal, + pytest.mark.skipif(any(shutil.which(t) is None for t in _TOOLS), + reason="formal toolchain (sby/yosys/boolector) " + "not on PATH"), +] + +GREEN_TASKS = [ + ("fv_umi_codec", "prove"), + pytest.param("fv_umi_codec", "prove_z3", marks=_needs_z3), + ("fv_umi_codec", "cover"), + ("fv_umi_buffer", "prove"), + pytest.param("fv_umi_buffer", "prove_z3", marks=_needs_z3), + ("fv_umi_buffer", "bypass"), + ("fv_umi_buffer", "cover"), + ("fv_umi_buffer", "rule5"), + ("fv_umi_cmd", "prove"), + pytest.param("fv_umi_cmd", "prove_z3", marks=_needs_z3), + ("fv_umi_cmd", "prove_dw64"), + ("fv_umi_cmd", "cover"), + ("fv_umi_cmd", "cover_sa"), + ("fv_umi_txn", "prove"), + pytest.param("fv_umi_txn", "prove_bw", marks=_needs_bitwuzla), + ("fv_umi_txn", "prove_deep"), + pytest.param("fv_umi_txn", "prove_deep_bw", marks=_needs_bitwuzla), + ("fv_umi_txn", "cover"), + ("fv_umi_txn", "cover_boundary"), +] + +FAULT_TASKS = [ + ("fv_umi_codec", "fault_eom"), + ("fv_umi_buffer", "fault_valid"), + ("fv_umi_buffer", "fault_data"), + ("fv_umi_buffer", "fault_rule5"), + ("fv_umi_cmd", "fault_opcode"), + ("fv_umi_cmd", "fault_atype"), + ("fv_umi_cmd", "fault_align_da"), + ("fv_umi_cmd", "fault_align_sa"), + ("fv_umi_cmd", "fault_fullbyte"), + ("fv_umi_cmd", "fault_ex"), + ("fv_umi_cmd", "fault_errsize"), + ("fv_umi_cmd", "fault_cap"), + ("fv_umi_cmd", "fault_respdata"), + ("fv_umi_cmd", "fault_sa_reserved"), + ("fv_umi_txn", "fault_wrongda"), + ("fv_umi_txn", "fault_size"), + ("fv_umi_txn", "fault_eom_early"), + ("fv_umi_txn", "fault_eom_missing"), + ("fv_umi_txn", "fault_msgbytes"), + ("fv_umi_txn", "fault_err_len"), + ("fv_umi_txn", "fault_orphan"), + ("fv_umi_txn", "fault_occ"), +] + + +def _sby(proof, task): + # sby resolves [files] against its working directory, so run from + # the proof's own directory (same as running it by hand) + return subprocess.run( + ["sby", "-f", f"{proof}.sby", task], + cwd=FORMAL_SUMI, capture_output=True, text=True, timeout=600) + + +def _tid(entry): + # entry is a (proof, task) tuple or a pytest.param wrapping the same + # two values; render the shared "proof:task" id either way + proof, task = getattr(entry, "values", entry) + return f"{proof}:{task}" + + +@pytest.mark.parametrize("proof,task", GREEN_TASKS, + ids=[_tid(e) for e in GREEN_TASKS]) +def test_proof(proof, task): + r = _sby(proof, task) + assert r.returncode == 0 and "DONE (PASS" in r.stdout, r.stdout[-800:] + + +@pytest.mark.parametrize("proof,task", FAULT_TASKS, + ids=[f"{p}:{t}" for p, t in FAULT_TASKS]) +def test_fault_must_fail(proof, task): + """Each proof's own regression: with the fault injected the proof + must FAIL on an assertion. DONE (FAIL is a counterexample; anything + else (ERROR, TIMEOUT) is a broken setup and stays red.""" + r = _sby(proof, task) + assert r.returncode != 0 and "DONE (FAIL" in r.stdout, r.stdout[-800:] diff --git a/tests/sumi/test_formal_sc.py b/tests/sumi/test_formal_sc.py new file mode 100644 index 00000000..b0c1d0bc --- /dev/null +++ b/tests/sumi/test_formal_sc.py @@ -0,0 +1,158 @@ +"""Formal property proofs as SiliconCompiler flows (the SC lane). + +The same proofs as tests/sumi/test_formal.py (the .sby task matrix), +launched here through siliconcompiler's PropertyCheckFlow. +Each proof family is a Design: the harness fv_.sv on top, the +DUT and property blocks (Buffer, Checker, Pack, Unpack) pulled in as +depfilesets -- so the sby job is GENERATED from the same fileset graph +the rest of the repo builds from. Include dirs, defines and top-level +params ride in from the Design objects; sources are read in place. + +Green rows must prove/cover clean: project.run() completes and the sby +errors metric is 0. fault_* rows inject a bug via a define and must +FAIL on a counterexample: run() raises naming the bmc node AND sby's +own verdict is FAIL (a tool/setup ERROR stays red here too). + +Engine note: this lane runs boolector, the engine the sby task offers +in the siliconcompiler 0.38.x releases; bitwuzla support is already +merged in siliconcompiler main, so this lane gains a second engine on +the next release. Until then the .sby lane (test_formal.py) remains +the dual-solver evidence (z3 / bitwuzla alongside boolector). + +Skips cleanly when sby/yosys/boolector or the SC formal flow are +missing, so other CI lanes are unaffected. +""" +import shutil +from pathlib import Path + +import pytest + +try: + from siliconcompiler import Design, Project + from siliconcompiler.flows.formalflow import PropertyCheckFlow, PropertyCheckMode + from siliconcompiler.tools.sby import SBYTask + _HAVE_SC_FORMAL = True +except ImportError: # pragma: no cover -- pre-formal-flow siliconcompiler + _HAVE_SC_FORMAL = False + +from umi.sumi import Buffer, Checker, Pack, Unpack + +REPO = Path(__file__).resolve().parents[2] +FORMAL_SUMI = REPO / "umi" / "formal" / "sumi" +SUMI_INCLUDE = REPO / "umi" / "sumi" / "include" + +_TOOLS = ("sby", "yosys", "boolector") + +pytestmark = [ + pytest.mark.formal, + pytest.mark.skipif(any(shutil.which(t) is None for t in _TOOLS), + reason="formal toolchain (sby/yosys/boolector) " + "not on PATH"), + pytest.mark.skipif(not _HAVE_SC_FORMAL, + reason="siliconcompiler PropertyCheckFlow/sby " + "not available"), +] + +if _HAVE_SC_FORMAL: + _MODES = { + "prove": PropertyCheckMode.PROVE, + "bmc": PropertyCheckMode.BMC, + "cover": PropertyCheckMode.COVER, + } + +# One entry per proof family: the dependency blocks (DUT + property +# modules), top-level harness params, and the unrolling depth -- the +# same depths as the equivalent .sby tasks. +FAMILIES = { + "fv_umi_codec": dict(deps=lambda: [Pack(), Unpack()], + depth=4, params=()), + "fv_umi_buffer": dict(deps=lambda: [Buffer(), Checker()], + depth=12, params=()), + # DW=64 (the hand lane's prove_dw64) keeps CI runtime down; the + # DW=256 face and the per-rule fault matrix stay on the .sby lane + "fv_umi_cmd": dict(deps=lambda: [Checker()], + depth=6, params=(("DW", "64"),)), + # the fast MAXLEN=1 configuration (the hand lane's prove); the + # MAXLEN=3 deep face stays on the .sby lane + "fv_umi_txn": dict(deps=lambda: [Checker()], + depth=20, params=()), +} + +# (id, family, mode, defines) -- id names the equivalent .sby task +GREEN_RUNS = [ + ("codec:prove", "fv_umi_codec", "prove", ()), + ("buffer:prove", "fv_umi_buffer", "prove", ()), + # rule 4.2.5 witness (README.md section 4.2 rule 5): out_ready + # ASSUMED stuck low, cover out_valid asserting-and-held anyway; + # FV_NO_WITNESS drops the handshake checker's own transaction + # covers, unreachable under stuck-low ready + ("buffer:rule5", "fv_umi_buffer", "cover", + ("FV_RULE5_READYLOW", "FV_NO_WITNESS")), + ("cmd:prove_dw64", "fv_umi_cmd", "prove", ()), + ("txn:prove", "fv_umi_txn", "prove", ()), +] + +# (id, family, defines) -- all run as bmc at the family depth +FAULT_RUNS = [ + ("codec:fault_eom", "fv_umi_codec", ("FV_FAULT_EOM",)), + ("buffer:fault_valid", "fv_umi_buffer", ("FV_FAULT_VALID",)), + # runs at the family's DW=64; the reserved-opcode fault (CMD1) is + # width-independent + ("cmd:fault_opcode", "fv_umi_cmd", ("FV_FAULT_OPCODE",)), + ("txn:fault_orphan", "fv_umi_txn", ("FV_FAULT_ORPHAN",)), +] + + +def _harness(family, defines): + """The proof-family Design: harness on top, repo blocks as deps.""" + spec = FAMILIES[family] + design = Design(family) + design.set_dataroot("umi_formal_sumi", str(FORMAL_SUMI)) + with design.active_fileset("rtl"): + design.set_topmodule(family) + design.add_file(f"{family}.sv") + design.add_idir(str(SUMI_INCLUDE)) + for dep in spec["deps"](): + design.add_depfileset(dep, "rtl") + for define in defines: + design.add_define(define) + for name, value in spec["params"]: + design.set_param(name, value) + return design + + +def _project(design, mode, depth, builddir): + proj = Project(design) + proj.add_fileset("rtl") + proj.set_flow(PropertyCheckFlow(f"formal_{mode}", modes=_MODES[mode])) + proj.option.set_builddir(str(builddir)) + # gate on the proof, not the tool version string: OSS CAD Suite sby + # builds answer --version with strings PEP-440 cannot parse (the + # local build prints a bare "SBY") + proj.option.set_novercheck(True) + SBYTask.find_task(proj).set_sby_depth(depth) + return proj + + +@pytest.mark.parametrize("tid,family,mode,defines", GREEN_RUNS, + ids=[r[0] for r in GREEN_RUNS]) +def test_sc_proof(tid, family, mode, defines, tmp_path): + proj = _project(_harness(family, defines), mode, + FAMILIES[family]["depth"], tmp_path) + hist = proj.run() + assert hist.get("metric", "errors", step=mode, index="0") == 0 + + +@pytest.mark.parametrize("tid,family,defines", FAULT_RUNS, + ids=[r[0] for r in FAULT_RUNS]) +def test_sc_fault_must_fail(tid, family, defines, tmp_path): + """With the fault injected the bmc node must fail the run (the + match pins the failure to the bmc node, not tool setup), and sby's + own verdict must be FAIL -- a counterexample, not an ERROR.""" + proj = _project(_harness(family, defines), "bmc", + FAMILIES[family]["depth"], tmp_path) + with pytest.raises(RuntimeError, match=r"bmc"): + proj.run() + status = (tmp_path / family / "job0" / "bmc" / "0" / + "sby" / "status").read_text() + assert status.startswith("FAIL"), status diff --git a/umi/formal/.gitignore b/umi/formal/.gitignore new file mode 100644 index 00000000..781ab4f6 --- /dev/null +++ b/umi/formal/.gitignore @@ -0,0 +1,2 @@ +# sby work directories (build products; recreated on every run) +*/fv_*_*/ diff --git a/umi/formal/README.md b/umi/formal/README.md new file mode 100644 index 00000000..758ea418 --- /dev/null +++ b/umi/formal/README.md @@ -0,0 +1,163 @@ +# Formal property proofs + +Machine-checked proofs of UMI spec properties against the RTL in this +repo, run with [SymbiYosys](https://symbiyosys.readthedocs.io) +(yosys + SMT solvers). + +Each proof is two files. No generators, no copied RTL: + + /fv_.sv harness: instantiates the shipped RTL, + constrains inputs, states the properties + /fv_.sby the sby job, one task per question + +`[files]` paths reference the RTL in place. Shared property modules +(the checkers themselves) are normal blocks under `umi/sumi/`, e.g. +`umi/sumi/umi_checker/`. The directories sby creates during a run +(`fv_*_/`) are build products: gitignored, never committed. + +## Run + +Two pytest entry points, both under the `formal` marker: + + # the .sby lane: the full dual-solver matrix, every .sby task + # (ordinary tasks must pass, fault_* tasks must fail) + pytest -m formal tests/sumi/test_formal.py + + # the SiliconCompiler lane: the same proofs launched as + # PropertyCheckFlow runs -- the sby jobs are GENERATED from the + # repo's own Design filesets (harness on top, DUT and checker + # blocks as depfilesets; include dirs, defines and params ride in + # from the Design objects) + pytest -m formal tests/sumi/test_formal_sc.py + + # one task by hand, from the proof's directory + cd umi/formal/sumi && sby -f fv_umi_codec.sby prove + +CI runs both entry points in the "Formal CI" job +(`.github/workflows/ci.yml`) inside SiliconCompiler's `sc_tools` +container (`ghcr.io/siliconcompiler/sc_tools:latest`, the same image the +Python CI lane uses). That image ships yosys, sby and boolector -- the +released SiliconCompiler 0.38.x engine -- and the job runs +`pytest -m "formal" --durations=0`. The formal lane runs the proofs +serially -- sby keeps a per-proof status database that is not safe to +share across the concurrent tasks of one proof, so this lane does not +add pytest-xdist (`-n`) here; the full set still finishes in a few +minutes. One solver is +all CI needs to gate the proofs; z3 and bitwuzla are the local dual-solver +evidence (see Engines), are absent from the container, and so their +rows skip cleanly there. Without the tools the formal tests skip, so no +other lane can be broken by this one. + +Engines: CI and the SC lane run boolector, the engine siliconcompiler's +sby task offers in the released 0.38.x versions; bitwuzla engine support +is already merged in siliconcompiler main, so the SC lane gains a second +engine on the next release. z3 and bitwuzla are used only in the local +`.sby` lane as independent-solver evidence (z3 and bitwuzla +alongside boolector); where those solvers are absent -- notably the CI +container -- their rows skip cleanly and boolector alone gates the lane. + +## Tools + +`sby`, `yosys`, and `boolector` on PATH (add `z3` and `bitwuzla` for the +full local dual-solver matrix; their rows skip when absent). Easiest +source is the +[OSS CAD Suite](https://github.com/YosysHQ/oss-cad-suite-build/releases): + + source /oss-cad-suite/environment + +Plus the repo's python environment for the pytest lane; the test-tree +conftests import switchboard/cocotb, so collection fails without it: + + python3 -m venv .venv + source .venv/bin/activate + pip install -e .[test] + +Without the tools on PATH the formal tests skip; they never break +other CI lanes. + +## Conventions + +* Tasks named `fault_*` inject a bug and must FAIL; all other tasks + must PASS. The pytest lane enforces both directions (a fault task + that passes is reported as the error it is). +* `prove` tasks are k-induction: a PASS is unbounded, not a bounded + search. Every `cover` witness must be REACHED, or the environment + is over-constrained. +* `prove` runs boolector and must pass; `prove_z3` runs the same proof + under z3 where z3 is on PATH and skips otherwise (local evidence only). + +## Adding a proof + +1. Add `fv_.sv` + `fv_.sby` under the layer directory, + with at least one `fault_*` task and covers for assumed corners. +2. Add its tasks to the lists in `tests/sumi/test_formal.py`. +3. Add a family entry (deps, depth, params) plus one green and one + fault row in `tests/sumi/test_formal_sc.py` so the proof also rides + the SiliconCompiler lane. + +## Proofs + +| proof | property module | claim | green tasks | fault tasks | +|---|---|---|---|---| +| `sumi/fv_umi_codec` | (umi_pack / umi_unpack) | CMD codec round-trips over the 13 structured opcodes | prove, prove_z3, cover | fault_eom | +| `sumi/fv_umi_buffer` | `umi_checker/rtl/umi_handshake_checker.sv` | umi_buffer obeys the README 4.2 ready/valid handshake, including rule 5 (VALID must not wait for READY) | prove, prove_z3, bypass, cover, rule5 | fault_valid, fault_data, fault_rule5 | +| `sumi/fv_umi_cmd` | `umi_checker/rtl/umi_cmd_checker.sv` | CMD-word legality: the assume face (legal-traffic generator) and assert face of the checker agree, at DW=256 and DW=64, and every legal opcode plus a full-capacity beat is reachable | prove, prove_z3, prove_dw64, cover, cover_sa | fault_opcode, fault_atype, fault_align_da, fault_align_sa, fault_fullbyte, fault_ex, fault_errsize, fault_cap, fault_respdata, fault_sa_reserved | +| `sumi/fv_umi_txn` | `umi_checker/rtl/umi_txn_checker.sv` | response-side transaction / framing: against a perfect in-order responder every response beat pairs with its request (kind/field-copy), the split-response DA follows the continuation law, EOM lands exactly on the closing beat, an error reply is one length-echoing beat, and the FRM-4 per-message byte total and the outstanding-request tracker stay bounded | prove, prove_bw, prove_deep, prove_deep_bw, cover, cover_boundary | fault_wrongda, fault_size, fault_eom_early, fault_eom_missing, fault_msgbytes, fault_err_len, fault_orphan, fault_occ | + +`fv_umi_buffer` additionally answers README section 4.2 rule 5 +(README.md:462): *"The assertion of VALID must not depend on the +assertion of READY. In other words, it is not legal for the VALID +assertion to wait for the READY assertion."* This is a structural rule +a cycle-sampled bind-in monitor can not assert (the handshake checker's +header says so); the complete method is +harness-level, on the DUT being proven, in three parts. `rule5` (cover) +assumes out_ready stuck low for the entire trace (`FV_RULE5_READYLOW`), +keeps the upstream driver legal, and reaches a cover of out_valid +asserting -- and holding -- anyway: VALID rises with zero help from +READY, the literal negation of the illegal behavior. `a_rule5_state` +rides the prove/prove_z3/bypass tasks as the state-driven face +(a full, data-holding buffer always asserts VALID, read out at the +ports as `!in_ready |-> out_valid`; in bypass `in_valid |-> out_valid`). +`fault_rule5` is the teeth: `FV_FAULT_RULE5` models the illegal design +where VALID waits for READY (`out_valid & out_ready`), under which the +stuck-low cover can never be reached, so the task FAILs. The handshake +checker also carries a free per-bind `c_rule5` reachability witness +(VALID fires while READY is low). Both rule5 tasks add `-DFV_NO_WITNESS` +so the checker's own transaction covers -- unreachable under stuck-low +ready -- do not spuriously fail the cover task. + +`fv_umi_cmd` checks one rule per fault task (the label each must trip +is tabulated in `fv_umi_cmd.sby`); `cover_sa` and `fault_sa_reserved` +run with the opt-in strict profile `CHECK_SA_RESERVED=1` (request SA +reserved bits zero), which defaults off because the repo's own +reference traffic uses the high SA bytes as routing/control bits. + +`fv_umi_txn` is a stateful, response-side (L2) proof and carries three +scope notes. **Framing depth.** The split-response framing rules are +proven by k-induction over messages of bounded length: `prove` / +`prove_bw` run the fast **MAXLEN=1** regression (short messages -- up +to two beats, one continuation), which already exercises the +continuation-address, mid-message ERR/EOF stability, and +EOM-exactly-on-close rules, and `prove_deep` / `prove_deep_bw` raise the +harness request-LEN ceiling to **MAXLEN=3**, extending the frame depth +to four beats. A PASS at each depth is unbounded (induction, not +bounded search); the harness glue lemmas +(`a_glue_*`, the checker tracker == responder queue equality) are +ASSERTED, not assumed. **No interleave.** The proof holds under the +single-link, un-interleaved operating condition documented in the +checker header: one point-to-point link, responses in request order, so +the checker's in-order shadow FIFO matches the responder queue +entry-for-entry. Bind the checker BEFORE any response mux; per-key +(HOSTID / bridge-specific) folding downstream of a merge is deferred. +**Harness width.** The harness runs at **DW=64** (the checker ships +DW=256) to keep the SMT problem tractable; DW is a data-path width the +framing rules are agnostic to. **Solver note.** `prove` / `prove_deep` +use **boolector** (the primary unbounded engine); `prove_bw` / +`prove_deep_bw` run the same proof under **bitwuzla**, which closes the +txn induction in seconds where z3 does not within a reasonable budget -- +the same bitwuzla-alongside-boolector precedent used elsewhere in this +lane. A fault task may falsify several related rules on the same +beat and the reported label can be solver-dependent; the intended +label for each is tabulated in `fv_umi_txn.sby`. `cover_boundary` (chparam +`MAX_MSG_BYTES=256`) witnesses the FRM-4 byte accumulator reaching +exactly its ceiling. diff --git a/umi/formal/sumi/fv_umi_buffer.sby b/umi/formal/sumi/fv_umi_buffer.sby new file mode 100644 index 00000000..b82d5872 --- /dev/null +++ b/umi/formal/sumi/fv_umi_buffer.sby @@ -0,0 +1,82 @@ +# Formal proof: umi_buffer vs the README 4.2 handshake rules. +# +# Run from this directory (needs yosys + SymbiYosys + a solver, e.g. +# the OSS CAD Suite): +# +# sby -f fv_umi_buffer.sby prove # skid buffer: expect PASS +# sby -f fv_umi_buffer.sby prove_z3 # same proof, second solver +# sby -f fv_umi_buffer.sby bypass # MODE=0: expect PASS +# sby -f fv_umi_buffer.sby cover # witnesses: expect all reached +# sby -f fv_umi_buffer.sby rule5 # rule 4.2.5 witness: expect PASS +# sby -f fv_umi_buffer.sby fault_valid # checker teeth: expect FAIL +# sby -f fv_umi_buffer.sby fault_data # checker teeth: expect FAIL +# sby -f fv_umi_buffer.sby fault_rule5 # rule5 teeth: expect FAIL +# +# prove tasks use k-induction: a PASS is an unbounded proof, not a +# bounded search. The fault tasks corrupt the observed output and MUST +# fail -- they are the checker's own regression (a checker that cannot +# fail a broken design proves nothing about a working one). +# +# rule 4.2.5 (README.md:462) -- "the assertion of VALID must not depend +# on the assertion of READY" -- is proven on the DUT in three parts: +# rule5 cover: out_ready ASSUMED 0 every cycle (FV_RULE5_READYLOW), +# upstream stays legal, COVER out_valid asserting-and-held. +# Reaching it proves VALID rises with zero help from READY. +# a_rule5_state (occupancy => out_valid) also rides the +# prove/prove_z3/bypass tasks as the state-driven face. +# fault_rule5 teeth: FV_FAULT_RULE5 models the illegal design where +# VALID waits for READY (out_valid & out_ready). Under +# stuck-low ready the covered signal is 0 forever, so: +# c_rule5_valid_stuck_low UNREACHED (the tripped label) +# c_rule5_valid_held UNREACHED +# and the task FAILs -- the honest `rule5` cover has teeth. +# Both rule5 tasks pass -DFV_NO_WITNESS so the handshake checker's own +# transaction covers (valid & ready), unreachable under stuck-low ready, +# do not spuriously fail the cover task. + +[tasks] +prove +prove_z3 +bypass +cover +rule5 +fault_valid +fault_data +fault_rule5 + +[options] +prove: mode prove +prove_z3: mode prove +bypass: mode prove +cover: mode cover +rule5: mode cover +fault_valid: mode bmc +fault_data: mode bmc +fault_rule5: mode cover +depth 12 +timeout 300 + +[engines] +prove_z3: smtbmc z3 +~prove_z3: smtbmc boolector + +[script] +rule5: verilog_defines -DFV_NO_WITNESS +fault_rule5: verilog_defines -DFV_NO_WITNESS +read_verilog -formal -sv umi_handshake_checker.sv +read_verilog -sv umi_buffer.v +fault_valid: read_verilog -formal -sv -DFV_FAULT_VALID fv_umi_buffer.sv +fault_data: read_verilog -formal -sv -DFV_FAULT_DATA fv_umi_buffer.sv +rule5: read_verilog -formal -sv -DFV_RULE5_READYLOW fv_umi_buffer.sv +fault_rule5: read_verilog -formal -sv -DFV_RULE5_READYLOW -DFV_FAULT_RULE5 fv_umi_buffer.sv +prove: read_verilog -formal -sv fv_umi_buffer.sv +prove_z3: read_verilog -formal -sv fv_umi_buffer.sv +cover: read_verilog -formal -sv fv_umi_buffer.sv +bypass: read_verilog -formal -sv fv_umi_buffer.sv +bypass: chparam -set MODE 0 fv_umi_buffer +prep -top fv_umi_buffer + +[files] +../../sumi/umi_buffer/rtl/umi_buffer.v +../../sumi/umi_checker/rtl/umi_handshake_checker.sv +fv_umi_buffer.sv diff --git a/umi/formal/sumi/fv_umi_buffer.sv b/umi/formal/sumi/fv_umi_buffer.sv new file mode 100644 index 00000000..1c67dfae --- /dev/null +++ b/umi/formal/sumi/fv_umi_buffer.sv @@ -0,0 +1,261 @@ +/******************************************************************************* + * Copyright 2026 Zero ASIC Corporation + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * + * ---- + * + * Documentation: + * + * Formal harness: umi_buffer against the README 4.2 handshake rules. + * + * The assume/guarantee split in one picture: + * + * assumed legal asserted legal + * (free) --[ env_in ASSUME=1 ]--> umi_buffer --[ chk_out ASSUME=0 ]-- + * + * The input channel is free stimulus constrained to obey the rules + * (the solver may only drive legal traffic); the output channel is + * checked. Both directions use the SAME property file, so the + * requirement and the environment can never drift apart. + * + * umi_buffer is payload-generic (one DW-wide data port), so the four + * SUMI fields ride through it concatenated -- which also demonstrates + * that the checker attaches to any block with two or three wires of + * glue. + * + * Fault tasks (see fv_umi_buffer.sby): under FV_FAULT_VALID / + * FV_FAULT_DATA the harness lets the solver corrupt the observed + * output for one cycle. The proof must then FAIL, with a + * counterexample trace. A checker that cannot fail a broken design + * proves nothing about a working one; these tasks are the checker's + * own regression. + * + * Rule 5 (README 4.2 rule 5, README.md:462): "The assertion of VALID + * must not depend on the assertion of READY. In other words, it is not + * legal for the VALID assertion to wait for the READY assertion." A + * cycle-sampled bind-in monitor can not assert this structural rule + * (see umi_handshake_checker's header); the complete method is + * harness-level, on the DUT we prove, in three parts: + * 1. STUCK-LOW WITNESS (`rule5` task, FV_RULE5_READYLOW): out_ready is + * assumed 0 on EVERY cycle, the upstream driver stays legal, and we + * COVER out_valid asserting -- and, per rule 2, holding. Reaching + * the cover with ready nailed low is the literal negation of "valid + * waits for ready": valid rises with zero help from ready. + * 2. STATE-DRIVEN VALID (a_rule5_state, live in the prove tasks): + * out_valid is a pure function of internal occupancy, never of + * out_ready, read out at the ports. In the skid buffer the FULL + * state is port-visible as in_ready low, and `!in_ready |-> out_valid` + * says a full (data-holding) buffer always asserts VALID; in bypass + * `in_valid |-> out_valid`. Proven in both MODE=1 and MODE=0. + * 3. TEETH (`fault_rule5` task, FV_FAULT_RULE5): models the illegal + * design in which valid waits for ready (out_valid & out_ready); + * under stuck-low ready that can never be covered, so the `rule5` + * cover goes unreachable and the task FAILs -- the honest cover has + * teeth. + ******************************************************************************/ + +`default_nettype none + +module fv_umi_buffer #( + parameter CW = 32, + parameter AW = 64, + parameter DW = 64, + parameter MODE = 1 // 1: skid buffer, 0: bypass +) ( + input wire clk +); + + localparam PW = CW + AW + AW + DW; // packed SUMI packet + + // ---------------------------------------------------------------- + // reset: free, but asserted at time zero (grounds all history) + // ---------------------------------------------------------------- + (* anyseq *) wire nreset; + reg f_past_exists = 1'b0; + always @(posedge clk) + f_past_exists <= 1'b1; + always @(*) + if (!f_past_exists) + assume (!nreset); + + // ---------------------------------------------------------------- + // free stimulus (constrained only by the rules, via env_in below) + // ---------------------------------------------------------------- + (* anyseq *) wire in_valid; + (* anyseq *) wire [CW-1:0] in_cmd; + (* anyseq *) wire [AW-1:0] in_dstaddr; + (* anyseq *) wire [AW-1:0] in_srcaddr; + (* anyseq *) wire [DW-1:0] in_data; + (* anyseq *) wire out_ready; + + wire in_ready; + wire out_valid; + wire [PW-1:0] out_packet; + + // ---------------------------------------------------------------- + // the design under test, exactly as shipped + // ---------------------------------------------------------------- + umi_buffer #( + .DW (PW), + .MODE (MODE) + ) dut ( + .clk (clk), + .nreset (nreset), + .in_valid (in_valid), + .in_data ({in_cmd, in_dstaddr, in_srcaddr, in_data}), + .in_ready (in_ready), + .out_valid (out_valid), + .out_data (out_packet), + .out_ready (out_ready) + ); + + wire [CW-1:0] out_cmd = out_packet[PW-1 -: CW]; + wire [AW-1:0] out_dstaddr = out_packet[PW-CW-1 -: AW]; + wire [AW-1:0] out_srcaddr = out_packet[PW-CW-AW-1 -: AW]; + wire [DW-1:0] out_data = out_packet[DW-1 -: DW]; + + // ---------------------------------------------------------------- + // fault injection (formal known-answer tests -- see the .sby tasks) + // ---------------------------------------------------------------- +`ifdef FV_FAULT_VALID + // the solver may drop the observed valid at any moment + (* anyseq *) wire fault; + wire obs_valid = out_valid & ~fault; +`else + wire obs_valid = out_valid; +`endif + +`ifdef FV_FAULT_DATA + // the solver may flip the observed data lsb at any moment + (* anyseq *) wire fault; + wire [DW-1:0] obs_data = out_data ^ {{(DW-1){1'b0}}, fault}; +`else + wire [DW-1:0] obs_data = out_data; +`endif + + // ---------------------------------------------------------------- + // the same file, both directions + // ---------------------------------------------------------------- + umi_handshake_checker #( + .CW (CW), .AW (AW), .DW (DW), + .ASSUME (1) // environment: assume legal input + ) env_in ( + .clk (clk), + .nreset (nreset), + .valid (in_valid), + .ready (in_ready), + .cmd (in_cmd), + .dstaddr (in_dstaddr), + .srcaddr (in_srcaddr), + .data (in_data) + ); + + umi_handshake_checker #( + .CW (CW), .AW (AW), .DW (DW), + .ASSUME (0) // requirement: assert legal output + ) chk_out ( + .clk (clk), + .nreset (nreset), + .valid (obs_valid), + .ready (out_ready), + .cmd (out_cmd), + .dstaddr (out_dstaddr), + .srcaddr (out_srcaddr), + .data (obs_data) + ); + + // ---------------------------------------------------------------- + // Rule 5 (README 4.2 rule 5, README.md:462): the assertion of VALID + // must not depend on the assertion of READY -- it is not legal for + // the VALID assertion to wait for the READY assertion. See the file + // header for the three-part evidence; parts 1 and 3 live here under + // FV_RULE5_READYLOW / FV_FAULT_RULE5, part 2 is a_rule5_state below. + // ---------------------------------------------------------------- +`ifdef FV_RULE5_READYLOW +`ifdef FV_FAULT_RULE5 + // ILLEGAL design model: VALID gated by READY (valid waits for ready). + // Under stuck-low ready this is 0 forever, so the covers can not be + // reached -- the `fault_rule5` task must FAIL. + wire rule5_valid = out_valid & out_ready; +`else + // honest DUT: VALID is whatever the buffer drives + wire rule5_valid = out_valid; +`endif + + // pin the downstream ready low for the entire trace + always @(*) + assume (out_ready == 1'b0); + +`ifdef FORMAL + // asserted-then-held shadow register, initial-grounded (no $past) + reg r5_past = 1'b0; + always @(posedge clk) + r5_past <= rule5_valid; + + always @(posedge clk) begin + if (f_past_exists & nreset) begin + // VALID asserts even though READY has been low all along + c_rule5_valid_stuck_low : cover (rule5_valid); + // and, per rule 2, stays asserted with READY still low + c_rule5_valid_held : cover (rule5_valid & r5_past); + end + end +`endif +`endif + + // ---------------------------------------------------------------- + // Part 2: STATE-DRIVEN VALID. out_valid is a pure function of the + // buffer's internal occupancy, never of out_ready. Live in the prove + // tasks (in cover/bmc modes the assert is inert). Occupancy is read + // out at the ports -- no hierarchical peek into the DUT: + // + // MODE 1 (skid): the buffer has two registered status outs, both + // assigned from the SAME next_state each cycle -- + // out_valid == (state != EMPTY) (data present) + // in_ready == (state != FULL) (room upstream) + // in_ready low is the port-visible "FULL, i.e. holding data" flag. + // The FSM never rests in the (out_valid=0, in_ready=0) corner: that + // would be a full buffer withholding VALID -- the exact signature + // of "VALID waits for READY". So `!in_ready |-> out_valid`: when the + // buffer is occupied to the point of backpressuring the input, + // out_valid is asserted with no dependence on out_ready. Both outs + // fall out of one next_state, so they can never both be low -- the + // property is inductive without reaching into the FSM register. + // + // MODE 0 (bypass): the input payload is presented the same cycle, + // so in_valid implies out_valid; out_ready feeds only in_ready and + // can not gate out_valid. + // + // past_nreset gates out the reset edge, where both status outs are + // held low by the repo's reset convention (not a rule-5 violation). + // ---------------------------------------------------------------- + reg past_nreset = 1'b0; + always @(posedge clk) + past_nreset <= nreset; + + generate + if (MODE == 1) begin : g_rule5_skid + always @(posedge clk) + if (f_past_exists & nreset & past_nreset) + a_rule5_state : assert (in_ready || out_valid); + end else begin : g_rule5_bypass + always @(posedge clk) + if (f_past_exists & nreset) + a_rule5_state : assert (!in_valid || out_valid); + end + endgenerate + +endmodule + +`default_nettype wire diff --git a/umi/formal/sumi/fv_umi_cmd.sby b/umi/formal/sumi/fv_umi_cmd.sby new file mode 100644 index 00000000..7ef8e3ef --- /dev/null +++ b/umi/formal/sumi/fv_umi_cmd.sby @@ -0,0 +1,92 @@ +# CMD-word legality (umi_cmd_checker against itself, assume vs assert). +# +# sby -f fv_umi_cmd.sby prove # expect PASS (boolector) +# sby -f fv_umi_cmd.sby prove_z3 # expect PASS (z3) +# sby -f fv_umi_cmd.sby prove_dw64 # expect PASS (DW=64) +# sby -f fv_umi_cmd.sby cover # expect PASS, all covers reached +# sby -f fv_umi_cmd.sby cover_sa # expect PASS (CHECK_SA_RESERVED=1) +# sby -f fv_umi_cmd.sby fault_ # must FAIL (see table) +# +# Fault tasks and the assertion label each must trip: +# fault_opcode CMD1_opcode_legal reserved opcode hole 0x19 +# fault_atype CMD2_atype_legal REQ_ATOMIC ATYPE=0x09 +# fault_align_da CMD4_da_aligned REQ_RD SIZE=1, odd DA +# fault_align_sa CMD4_sa_aligned REQ_RD SIZE=1, odd SA +# fault_fullbyte CMD10_fullbyte_decode opcode5 0x0E, CMD[7:5]=1 +# fault_ex CMD11_ex_zero REQ_WRPOSTED with EX=1 +# fault_errsize CMD12_error_size opcode5 0x0F, CMD[7:5]=2 +# fault_cap CMD15_beat_capacity REQ_WR SIZE=7 (128B > DW/8) +# fault_respdata CMD16_err_data_zero NETERR RESP_RD, data lane 0 != 0 +# fault_sa_reserved CMD6_sa_reserved SA[44]=1 (CHECK_SA_RESERVED=1) +# fault_fullbyte and fault_errsize also trip CMD1_opcode_legal (and +# fault_errsize CMD10): a full-byte aliasing error is by construction +# outside the CMD-1 legal-opcode set. The intended label must appear +# in the log's failed-assertion list. + +[tasks] +prove +prove_z3 +prove_dw64 +cover +cover_sa +fault_opcode +fault_atype +fault_align_da +fault_align_sa +fault_fullbyte +fault_ex +fault_errsize +fault_cap +fault_respdata +fault_sa_reserved + +[options] +prove: mode prove +prove_z3: mode prove +prove_dw64: mode prove +cover: mode cover +cover_sa: mode cover +fault_opcode: mode bmc +fault_atype: mode bmc +fault_align_da: mode bmc +fault_align_sa: mode bmc +fault_fullbyte: mode bmc +fault_ex: mode bmc +fault_errsize: mode bmc +fault_cap: mode bmc +fault_respdata: mode bmc +fault_sa_reserved: mode bmc +depth 6 +timeout 300 + +[engines] +prove_z3: smtbmc z3 +~prove_z3: smtbmc boolector + +[script] +# -I. : umi_messages.vh is staged next to the sources by [files] +read_verilog -formal -sv -I. umi_cmd_checker.sv +prove: read_verilog -formal -sv fv_umi_cmd.sv +prove_z3: read_verilog -formal -sv fv_umi_cmd.sv +prove_dw64: read_verilog -formal -sv fv_umi_cmd.sv +cover: read_verilog -formal -sv fv_umi_cmd.sv +cover_sa: read_verilog -formal -sv fv_umi_cmd.sv +fault_opcode: read_verilog -formal -sv -DFV_FAULT_OPCODE fv_umi_cmd.sv +fault_atype: read_verilog -formal -sv -DFV_FAULT_ATYPE fv_umi_cmd.sv +fault_align_da: read_verilog -formal -sv -DFV_FAULT_ALIGN_DA fv_umi_cmd.sv +fault_align_sa: read_verilog -formal -sv -DFV_FAULT_ALIGN_SA fv_umi_cmd.sv +fault_fullbyte: read_verilog -formal -sv -DFV_FAULT_FULLBYTE fv_umi_cmd.sv +fault_ex: read_verilog -formal -sv -DFV_FAULT_EX fv_umi_cmd.sv +fault_errsize: read_verilog -formal -sv -DFV_FAULT_ERRSIZE fv_umi_cmd.sv +fault_cap: read_verilog -formal -sv -DFV_FAULT_CAP fv_umi_cmd.sv +fault_respdata: read_verilog -formal -sv -DFV_FAULT_RESPDATA fv_umi_cmd.sv +fault_sa_reserved: read_verilog -formal -sv -DFV_FAULT_SA_RESERVED fv_umi_cmd.sv +prove_dw64: chparam -set DW 64 fv_umi_cmd +cover_sa: chparam -set CHECK_SA_RESERVED 1 fv_umi_cmd +fault_sa_reserved: chparam -set CHECK_SA_RESERVED 1 fv_umi_cmd +prep -top fv_umi_cmd + +[files] +../../sumi/umi_checker/rtl/umi_cmd_checker.sv +../../sumi/include/umi_messages.vh +fv_umi_cmd.sv diff --git a/umi/formal/sumi/fv_umi_cmd.sv b/umi/formal/sumi/fv_umi_cmd.sv new file mode 100644 index 00000000..b0e25c2b --- /dev/null +++ b/umi/formal/sumi/fv_umi_cmd.sv @@ -0,0 +1,191 @@ +/******************************************************************************* + * Copyright 2026 Zero ASIC Corporation + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * + * ---- + * + * Documentation: + * + * Formal harness: umi_cmd_checker against itself, both directions. + * + * assumed legal asserted legal + * (free) --[ env_legal ASSUME=1 ]--+--[ chk_beat ASSUME=0 ]-- + * | + * (fault_* only: targeted corruption) + * + * One free SUMI channel feeds two instances of the SAME property + * file: env_legal (ASSUME=1) generates the legal command language, + * chk_beat (ASSUME=0) checks it. With no fault injected the prove + * tasks show the assume and assert faces can never drift apart, and + * the cover tasks show the assumed language is alive: all 13 + * structured opcodes and a full-capacity beat are reachable (a + * language that can not express them would make every downstream + * proof vacuous). + * + * Fault tasks (see fv_umi_cmd.sby): each FV_FAULT_* define replaces + * the beat chk_beat observes with a known-answer illegal beat while + * env_legal still sees the clean channel. Every fault task must FAIL + * with the intended assertion label -- the checker's own regression. + * The known answers are constants (not free corruptions) so each one + * trips exactly the rule under test; the two full-byte faults + * necessarily also trip CMD1_opcode_legal, because any full-byte + * aliasing error is also outside the legal opcode set (CMD-1 implies + * CMD-10/CMD-12 over the whole language -- see the checker header). + ******************************************************************************/ + +`default_nettype none + +module fv_umi_cmd #( + parameter CW = 32, + parameter AW = 64, + parameter DW = 256, + parameter CHECK_SA_RESERVED = 0 +) ( + input wire clk +); + + // ---------------------------------------------------------------- + // reset: free, but asserted at time zero (grounds the first cycle) + // ---------------------------------------------------------------- + (* anyseq *) wire nreset; + reg f_past_exists = 1'b0; + always @(posedge clk) + f_past_exists <= 1'b1; + always @(*) + if (!f_past_exists) + assume (!nreset); + + // ---------------------------------------------------------------- + // free stimulus (constrained only by the rules, via env_legal) + // ---------------------------------------------------------------- + (* anyseq *) wire valid; + (* anyseq *) wire ready; + (* anyseq *) wire [CW-1:0] in_cmd; + (* anyseq *) wire [AW-1:0] in_dstaddr; + (* anyseq *) wire [AW-1:0] in_srcaddr; + (* anyseq *) wire [DW-1:0] in_data; + + // ---------------------------------------------------------------- + // fault injection (formal known-answer tests -- one define per + // .sby fault task; every constant is analyzed in the task table + // of fv_umi_cmd.sby so it trips exactly the intended rule) + // ---------------------------------------------------------------- +`ifdef FV_FAULT_OPCODE + // reserved opcode hole 0x19; SIZE=0 keeps every other rule content + wire [CW-1:0] obs_cmd = 32'h0000_0019; + wire [AW-1:0] obs_dstaddr = {AW{1'b0}}; + wire [AW-1:0] obs_srcaddr = {AW{1'b0}}; + wire [DW-1:0] obs_data = in_data; +`elsif FV_FAULT_ATYPE + // REQ_ATOMIC with ATYPE=0x09 (one past ATOMICSWAP), SIZE=0 + wire [CW-1:0] obs_cmd = 32'h0000_0909; + wire [AW-1:0] obs_dstaddr = {AW{1'b0}}; + wire [AW-1:0] obs_srcaddr = {AW{1'b0}}; + wire [DW-1:0] obs_data = in_data; +`elsif FV_FAULT_ALIGN_DA + // REQ_RD SIZE=1 with an odd DA (SA kept aligned) + wire [CW-1:0] obs_cmd = 32'h0000_0021; + wire [AW-1:0] obs_dstaddr = {{(AW-1){1'b0}}, 1'b1}; + wire [AW-1:0] obs_srcaddr = {AW{1'b0}}; + wire [DW-1:0] obs_data = in_data; +`elsif FV_FAULT_ALIGN_SA + // REQ_RD SIZE=1 with an odd SA (DA kept aligned) + wire [CW-1:0] obs_cmd = 32'h0000_0021; + wire [AW-1:0] obs_dstaddr = {AW{1'b0}}; + wire [AW-1:0] obs_srcaddr = {{(AW-1){1'b0}}, 1'b1}; + wire [DW-1:0] obs_data = in_data; +`elsif FV_FAULT_FULLBYTE + // 5-bit opcode 0x0E extended with CMD[7:5]=1: not RESP_LINK, + // not anything -- the 0x0E-family aliasing error + wire [CW-1:0] obs_cmd = 32'h0000_002E; + wire [AW-1:0] obs_dstaddr = {AW{1'b0}}; + wire [AW-1:0] obs_srcaddr = {AW{1'b0}}; + wire [DW-1:0] obs_data = in_data; +`elsif FV_FAULT_EX + // REQ_WRPOSTED with EX=1 (bit 24), SIZE=LEN=0 + wire [CW-1:0] obs_cmd = 32'h0100_0005; + wire [AW-1:0] obs_dstaddr = {AW{1'b0}}; + wire [AW-1:0] obs_srcaddr = {AW{1'b0}}; + wire [DW-1:0] obs_data = in_data; +`elsif FV_FAULT_ERRSIZE + // 5-bit opcode 0x0F extended with CMD[7:5]=2: the REQ_ERROR + // family carrying SIZE=2 instead of 0 + wire [CW-1:0] obs_cmd = 32'h0000_004F; + wire [AW-1:0] obs_dstaddr = {AW{1'b0}}; + wire [AW-1:0] obs_srcaddr = {AW{1'b0}}; + wire [DW-1:0] obs_data = in_data; +`elsif FV_FAULT_CAP + // REQ_WR SIZE=7 LEN=0: one beat claims 128 bytes, over any + // DW <= 512 bus (the task runs the default DW=256 -> 32 bytes) + wire [CW-1:0] obs_cmd = 32'h0000_00E3; + wire [AW-1:0] obs_dstaddr = {AW{1'b0}}; + wire [AW-1:0] obs_srcaddr = {AW{1'b0}}; + wire [DW-1:0] obs_data = in_data; +`elsif FV_FAULT_RESPDATA + // RESP_RD with ERR=NETERR (CMD[26:25]=3) and a nonzero byte in + // the one relevant data lane (SIZE=LEN=0 -> lane 0) + wire [CW-1:0] obs_cmd = 32'h0600_0002; + wire [AW-1:0] obs_dstaddr = {AW{1'b0}}; + wire [AW-1:0] obs_srcaddr = in_srcaddr; + wire [DW-1:0] obs_data = {{(DW-1){1'b0}}, 1'b1}; +`elsif FV_FAULT_SA_RESERVED + // REQ_RD with SA bit 44 set: reserved SA[63:40] nonzero (the + // .sby task turns the gate on with chparam CHECK_SA_RESERVED=1) + wire [CW-1:0] obs_cmd = 32'h0000_0001; + wire [AW-1:0] obs_dstaddr = {AW{1'b0}}; + wire [AW-1:0] obs_srcaddr = 64'h0000_1000_0000_0000; + wire [DW-1:0] obs_data = in_data; +`else + wire [CW-1:0] obs_cmd = in_cmd; + wire [AW-1:0] obs_dstaddr = in_dstaddr; + wire [AW-1:0] obs_srcaddr = in_srcaddr; + wire [DW-1:0] obs_data = in_data; +`endif + + // ---------------------------------------------------------------- + // the same file, both directions + // ---------------------------------------------------------------- + umi_cmd_checker #( + .CW (CW), .AW (AW), .DW (DW), + .ASSUME (1), // environment: assume legal beats + .CHECK_SA_RESERVED (CHECK_SA_RESERVED) + ) env_legal ( + .clk (clk), + .nreset (nreset), + .valid (valid), + .ready (ready), + .cmd (in_cmd), + .dstaddr (in_dstaddr), + .srcaddr (in_srcaddr), + .data (in_data) + ); + + umi_cmd_checker #( + .CW (CW), .AW (AW), .DW (DW), + .ASSUME (0), // requirement: assert legal beats + .CHECK_SA_RESERVED (CHECK_SA_RESERVED) + ) chk_beat ( + .clk (clk), + .nreset (nreset), + .valid (valid), + .ready (ready), + .cmd (obs_cmd), + .dstaddr (obs_dstaddr), + .srcaddr (obs_srcaddr), + .data (obs_data) + ); + +endmodule + +`default_nettype wire diff --git a/umi/formal/sumi/fv_umi_codec.sby b/umi/formal/sumi/fv_umi_codec.sby new file mode 100644 index 00000000..22ee3f3b --- /dev/null +++ b/umi/formal/sumi/fv_umi_codec.sby @@ -0,0 +1,39 @@ +# CMD codec round-trip (umi_pack <-> umi_unpack). +# +# sby -f fv_umi_codec.sby prove # expect PASS (boolector) +# sby -f fv_umi_codec.sby prove_z3 # expect PASS (z3) +# sby -f fv_umi_codec.sby cover # expect PASS, all covers reached +# sby -f fv_umi_codec.sby fault_eom # must FAIL (EOM corrupted in transit) + +[tasks] +prove +prove_z3 +cover +fault_eom + +[options] +prove: mode prove +prove_z3: mode prove +cover: mode cover +fault_eom: mode bmc +depth 4 +timeout 300 + +[engines] +prove_z3: smtbmc z3 +~prove_z3: smtbmc boolector + +[script] +read_verilog -sv umi_decode.v +read_verilog -sv umi_pack.v +read_verilog -sv umi_unpack.v +fault_eom: read_verilog -formal -sv -DFV_FAULT_EOM fv_umi_codec.sv +~fault_eom: read_verilog -formal -sv fv_umi_codec.sv +prep -top fv_umi_codec + +[files] +../../sumi/umi_pack/rtl/umi_pack.v +../../sumi/umi_unpack/rtl/umi_unpack.v +../../sumi/umi_decode/rtl/umi_decode.v +../../sumi/include/umi_messages.vh +fv_umi_codec.sv diff --git a/umi/formal/sumi/fv_umi_codec.sv b/umi/formal/sumi/fv_umi_codec.sv new file mode 100644 index 00000000..388644e8 --- /dev/null +++ b/umi/formal/sumi/fv_umi_codec.sv @@ -0,0 +1,247 @@ +/******************************************************************************* + * Copyright 2026 Zero ASIC Corporation + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * + * ---- + * + * Documentation: + * + * - Proves the CMD codec round-trips over the 13 structured opcodes. + * FWD_*: unpack(pack(fields)) returns the fields, with the format's + * two aliases handled exactly: REQ_ATOMIC carries ATYPE in the LEN + * bit positions (LEN reads back 0), and CMD[26:25] is USER on + * requests / ERR on responses. + * REV_cmd: pack(unpack(word)) == word for structured words. + * - Full-byte opcodes (REQ_ERROR 0x0F, REQ_LINK 0x2F, RESP_LINK 0x0E) + * redefine the field layout and are excluded here. The whitelist + * also avoids opcode 5'h19, which the codec's 4-bit atomic compare + * (packet_cmd[3:0] == 4'h9) reads as an atomic. + * - Purely combinational, so induction closes immediately; the value + * of prove mode is the quantifier over all inputs. + * - fault_eom (see .sby) flips the EOM bit in transit; FWD_eom must + * fail. A proof that cannot fail proves nothing. + * + ******************************************************************************/ + +`default_nettype none + +module fv_umi_codec #( + parameter CW = 32 +) ( + input wire clk +); + +`include "umi_messages.vh" + + // ---------------------------------------------------------------- + // free field tuple + // ---------------------------------------------------------------- + (* anyseq *) wire [4:0] f_opcode; + (* anyseq *) wire [2:0] f_size; + (* anyseq *) wire [7:0] f_len; + (* anyseq *) wire [7:0] f_atype; + (* anyseq *) wire [3:0] f_qos; + (* anyseq *) wire [1:0] f_prot; + (* anyseq *) wire f_eom; + (* anyseq *) wire f_eof; + (* anyseq *) wire [1:0] f_user; + (* anyseq *) wire [1:0] f_err; + (* anyseq *) wire f_ex; + (* anyseq *) wire [4:0] f_hostid; + + // the thirteen structured opcodes (requests odd, responses even) + wire f_structured = + (f_opcode == UMI_REQ_READ) | (f_opcode == UMI_REQ_WRITE) | + (f_opcode == UMI_REQ_POSTED) | (f_opcode == UMI_REQ_RDMA) | + (f_opcode == UMI_REQ_ATOMIC) | (f_opcode == UMI_REQ_USER0) | + (f_opcode == UMI_REQ_FUTURE0) | + (f_opcode == UMI_RESP_READ) | (f_opcode == UMI_RESP_WRITE) | + (f_opcode == UMI_RESP_USER0) | (f_opcode == UMI_RESP_USER1) | + (f_opcode == UMI_RESP_FUTURE0)| (f_opcode == UMI_RESP_FUTURE1); + + wire f_is_atomic = (f_opcode == UMI_REQ_ATOMIC); + wire f_is_response = ~f_opcode[0]; + + always @(*) begin + legal_opcode : assume (f_structured); + // ATYPE is an 8-bit field but only ADD..SWAP are defined (WF-2) + legal_atype : assume (!f_is_atomic + || (f_atype <= UMI_REQ_ATOMICSWAP)); + end + + // ---------------------------------------------------------------- + // forward: fields -> pack -> unpack -> fields + // ---------------------------------------------------------------- + wire [CW-1:0] packed_cmd; + + umi_pack #(.CW(CW)) u_pack ( + .cmd_opcode (f_opcode), + .cmd_size (f_size), + .cmd_len (f_len), + .cmd_atype (f_atype), + .cmd_prot (f_prot), + .cmd_qos (f_qos), + .cmd_eom (f_eom), + .cmd_eof (f_eof), + .cmd_user (f_user), + .cmd_err (f_err), + .cmd_ex (f_ex), + .cmd_hostid (f_hostid), + .cmd_user_extended (24'd0), // structured opcodes only + .packet_cmd (packed_cmd) + ); + +`ifdef FV_FAULT_EOM + // the known-answer fault: EOM flipped in transit; FWD_eom must fail + wire [CW-1:0] wire_cmd = packed_cmd ^ (32'h1 << 22); +`else + wire [CW-1:0] wire_cmd = packed_cmd; +`endif + + wire [4:0] u_opcode; + wire [2:0] u_size; + wire [7:0] u_len; + wire [7:0] u_atype; + wire [3:0] u_qos; + wire [1:0] u_prot; + wire u_eom; + wire u_eof; + wire u_ex; + wire [1:0] u_user; + wire [23:0] u_user_extended; + wire [1:0] u_err; + wire [4:0] u_hostid; + + umi_unpack #(.CW(CW)) u_unpack ( + .packet_cmd (wire_cmd), + .cmd_opcode (u_opcode), + .cmd_size (u_size), + .cmd_len (u_len), + .cmd_atype (u_atype), + .cmd_qos (u_qos), + .cmd_prot (u_prot), + .cmd_eom (u_eom), + .cmd_eof (u_eof), + .cmd_ex (u_ex), + .cmd_user (u_user), + .cmd_user_extended (u_user_extended), + .cmd_err (u_err), + .cmd_hostid (u_hostid) + ); + + always @(*) begin + FWD_opcode : assert (u_opcode == f_opcode); + FWD_size : assert (u_size == f_size); + FWD_qos : assert (u_qos == f_qos); + FWD_prot : assert (u_prot == f_prot); + FWD_eom : assert (u_eom == f_eom); + FWD_eof : assert (u_eof == f_eof); + FWD_ex : assert (u_ex == f_ex); + FWD_hostid : assert (u_hostid == f_hostid); + // the LEN/ATYPE alias, exactly as the format defines it + FWD_len : assert (f_is_atomic ? (u_len == 8'd0) + : (u_len == f_len)); + FWD_atype : assert (!f_is_atomic || (u_atype == f_atype)); + // the USER/ERR alias: requests carry USER, responses carry ERR + FWD_user : assert (f_is_response || (u_user == f_user)); + FWD_err : assert (f_is_response ? (u_err == f_err) + : (u_err == 2'd0)); + end + + // ---------------------------------------------------------------- + // reverse: word -> unpack -> pack -> the same word + // ---------------------------------------------------------------- + (* anyseq *) wire [CW-1:0] r_cmd; + + wire r_structured = + (r_cmd[4:0] == UMI_REQ_READ) | (r_cmd[4:0] == UMI_REQ_WRITE) | + (r_cmd[4:0] == UMI_REQ_POSTED) | (r_cmd[4:0] == UMI_REQ_RDMA) | + (r_cmd[4:0] == UMI_REQ_ATOMIC) | (r_cmd[4:0] == UMI_REQ_USER0) | + (r_cmd[4:0] == UMI_REQ_FUTURE0) | + (r_cmd[4:0] == UMI_RESP_READ) | (r_cmd[4:0] == UMI_RESP_WRITE) | + (r_cmd[4:0] == UMI_RESP_USER0) | (r_cmd[4:0] == UMI_RESP_USER1) | + (r_cmd[4:0] == UMI_RESP_FUTURE0)| (r_cmd[4:0] == UMI_RESP_FUTURE1); + + always @(*) begin + legal_r_opcode : assume (r_structured); + end + + wire [4:0] r_opcode; + wire [2:0] r_size; + wire [7:0] r_len; + wire [7:0] r_atype; + wire [3:0] r_qos; + wire [1:0] r_prot; + wire r_eom; + wire r_eof; + wire r_ex; + wire [1:0] r_user; + wire [23:0] r_user_extended; + wire [1:0] r_err; + wire [4:0] r_hostid; + + umi_unpack #(.CW(CW)) r_unpack ( + .packet_cmd (r_cmd), + .cmd_opcode (r_opcode), + .cmd_size (r_size), + .cmd_len (r_len), + .cmd_atype (r_atype), + .cmd_qos (r_qos), + .cmd_prot (r_prot), + .cmd_eom (r_eom), + .cmd_eof (r_eof), + .cmd_ex (r_ex), + .cmd_user (r_user), + .cmd_user_extended (r_user_extended), + .cmd_err (r_err), + .cmd_hostid (r_hostid) + ); + + wire [CW-1:0] r_repacked; + + umi_pack #(.CW(CW)) r_pack ( + .cmd_opcode (r_opcode), + .cmd_size (r_size), + .cmd_len (r_len), + .cmd_atype (r_atype), + .cmd_prot (r_prot), + .cmd_qos (r_qos), + .cmd_eom (r_eom), + .cmd_eof (r_eof), + .cmd_user (r_user), + .cmd_err (r_err), + .cmd_ex (r_ex), + .cmd_hostid (r_hostid), + .cmd_user_extended (24'd0), + .packet_cmd (r_repacked) + ); + + always @(*) begin + REV_cmd : assert (r_repacked == r_cmd); + end + + // ---------------------------------------------------------------- + // vacuity witnesses: each interesting class is actually explored + // ---------------------------------------------------------------- +`ifdef FORMAL + always @(*) begin + SAW_read_req : cover (f_opcode == UMI_REQ_READ); + SAW_write_resp : cover (f_opcode == UMI_RESP_WRITE && f_err != 2'd0); + SAW_atomic : cover (f_is_atomic && f_atype == UMI_REQ_ATOMICSWAP); + end +`endif + +endmodule + +`default_nettype wire diff --git a/umi/formal/sumi/fv_umi_txn.sby b/umi/formal/sumi/fv_umi_txn.sby new file mode 100644 index 00000000..701c5b07 --- /dev/null +++ b/umi/formal/sumi/fv_umi_txn.sby @@ -0,0 +1,163 @@ +# Transaction / framing checker (umi_txn_checker) vs a perfect in-order +# responder model. Response-side L2 rules, NO-INTERLEAVE operating +# condition (single point-to-point link -- see umi/formal/README.md). +# +# sby -f fv_umi_txn.sby prove # expect PASS (boolector, k-induction) +# sby -f fv_umi_txn.sby prove_bw # expect PASS (bitwuzla) +# sby -f fv_umi_txn.sby cover # expect PASS, all covers reached +# sby -f fv_umi_txn.sby cover_boundary # expect PASS, FRM-4 boundary reached +# sby -f fv_umi_txn.sby fault_ # must FAIL (see table) +# +# prove tasks are k-induction: a PASS is unbounded. The checker is +# stateful, so induction is strengthened by the harness glue lemmas +# (a_glue_*), which are ASSERTED, not assumed. z3 is replaced by +# bitwuzla on this configuration (prove_bw): z3 is slow on this +# composition (minutes) and does not close the txn induction within a +# reasonable budget, while bitwuzla closes in ~30 s, so it is the second +# solver here (documented in umi/formal/README.md). boolector (prove) is +# the primary unbounded engine. +# +# Fault tasks and the assertion label each must trip. Every fault +# corrupts ONLY the checker's response view (fv_umi_txn.sv [corrupt] +# block) or shrinks a checker bound by chparam, so the responder and all +# glue lemmas stay clean. Each fault trips its INTENDED rule below. Some +# corruptions violate several related rules on the same beat, and which +# label BMC reports is solver-dependent -- smtbmc prints whichever rules +# its particular counterexample happens to falsify, so a different solver +# (or build) can report a different subset. The INTENDED label is the one +# guaranteed to appear in the log's failed-assertion list; the extra +# labels called out below are also legal and NOT a regression: +# fault_wrongda TXN_da_first first-beat DA off by 8 (sole, +# stable across solvers) +# fault_size TXN_size mid-message SIZE mutation. This +# also trips TXN_eom_iff_closed +# (always) and TXN_bytes_le (most +# solvers): one SIZE flip corrupts +# the byte-count arithmetic those +# rules share, so they fail together +# fault_eom_early TXN_eom_iff_closed EOM on a non-closing split beat +# fault_eom_missing TXN_eom_iff_closed EOM dropped on the closing beat. +# Solver-dependent: boolector/z3 +# report TXN_eom_iff_closed, +# bitwuzla reports TXN_err_eom when +# it models the beat as an error +# response -- a dropped EOM breaks +# whichever EOM-termination law +# the counterexample invokes +# fault_msgbytes TXN_msgbytes FRM-4 overrun (chparam MAX=64, +# FV_BIGMSG legal >64 B message) +# fault_err_len TXN_err_len error response LEN != request LEN +# fault_orphan TXN_p5_outstanding response into an empty tracker. +# An orphan beat violates SEVERAL +# rules at once: boolector/bitwuzla +# report TXN_p5_outstanding, but z3 +# also trips TXN_da_first and the +# field-match rules (TXN_kind, +# TXN_size, TXN_hostid, TXN_qos, +# TXN_prot, TXN_bytes_le, +# TXN_eom_iff_closed) at the same +# step -- BMC reports whichever +# subset its model trips first +# fault_occ TXN_occ_bound tracker overflow (chparam CAP=1, +# two legal outstanding requests) +# The intended label must appear in the log's failed-assertion list. + +[tasks] +prove +prove_bw +prove_deep +prove_deep_bw +cover +cover_boundary +fault_wrongda +fault_size +fault_eom_early +fault_eom_missing +fault_msgbytes +fault_err_len +fault_orphan +fault_occ + +[options] +prove: mode prove +prove_bw: mode prove +prove_deep: mode prove +prove_deep_bw: mode prove +prove: depth 20 +prove_bw: depth 20 +prove_deep: depth 20 +prove_deep_bw: depth 20 +cover: mode cover +cover: depth 22 +cover_boundary: mode cover +cover_boundary: depth 24 +fault_wrongda: mode bmc +fault_size: mode bmc +fault_eom_early: mode bmc +fault_eom_missing: mode bmc +fault_msgbytes: mode bmc +fault_err_len: mode bmc +fault_orphan: mode bmc +fault_occ: mode bmc +fault_wrongda: depth 20 +fault_size: depth 20 +fault_eom_early: depth 20 +fault_eom_missing: depth 20 +fault_msgbytes: depth 24 +fault_err_len: depth 20 +fault_orphan: depth 20 +fault_occ: depth 20 +timeout 1200 + +[engines] +prove: smtbmc boolector +prove_bw: smtbmc bitwuzla +prove_deep: smtbmc boolector +prove_deep_bw: smtbmc bitwuzla +cover: smtbmc boolector +cover_boundary: smtbmc boolector +fault_wrongda: smtbmc boolector +fault_size: smtbmc boolector +fault_eom_early: smtbmc boolector +fault_eom_missing: smtbmc boolector +fault_msgbytes: smtbmc boolector +fault_err_len: smtbmc boolector +fault_orphan: smtbmc boolector +fault_occ: smtbmc boolector + +[script] +# -I. : umi_messages.vh is staged next to the sources by [files] +# FORMAL_MSGBYTES_BOUNDARY guards the SAW_msgbytes_boundary cover, which +# lives in the CHECKER (umi_txn_checker.sv), not the harness. read_verilog +# -D is local to a single read command, so the define must be set as a +# PERSISTENT yosys define BEFORE the checker read below -- otherwise the +# checker is parsed without it and the boundary cover is silently dropped. +cover_boundary: verilog_defines -DFORMAL_MSGBYTES_BOUNDARY +read_verilog -formal -sv -I. umi_txn_checker.sv +prove: read_verilog -formal -sv -I. fv_umi_txn.sv +prove_bw: read_verilog -formal -sv -I. fv_umi_txn.sv +prove_deep: read_verilog -formal -sv -I. fv_umi_txn.sv +prove_deep_bw: read_verilog -formal -sv -I. fv_umi_txn.sv +cover: read_verilog -formal -sv -I. fv_umi_txn.sv +cover_boundary: read_verilog -formal -sv -I. fv_umi_txn.sv +fault_wrongda: read_verilog -formal -sv -I. -DFV_FAULT_WRONGDA fv_umi_txn.sv +fault_size: read_verilog -formal -sv -I. -DFV_FAULT_SIZE fv_umi_txn.sv +fault_eom_early: read_verilog -formal -sv -I. -DFV_FAULT_EOM_EARLY fv_umi_txn.sv +fault_eom_missing: read_verilog -formal -sv -I. -DFV_FAULT_EOM_MISSING fv_umi_txn.sv +fault_msgbytes: read_verilog -formal -sv -I. -DFV_BIGMSG fv_umi_txn.sv +fault_err_len: read_verilog -formal -sv -I. -DFV_FAULT_ERR_LEN fv_umi_txn.sv +fault_orphan: read_verilog -formal -sv -I. -DFV_FAULT_ORPHAN fv_umi_txn.sv +fault_occ: read_verilog -formal -sv -I. fv_umi_txn.sv +cover_boundary: chparam -set MAX_MSG_BYTES 256 fv_umi_txn +fault_msgbytes: chparam -set MAX_MSG_BYTES 64 fv_umi_txn +fault_occ: chparam -set CAP 1 fv_umi_txn +# deep proof: raise the request-LEN ceiling to 3 (messages up to 4 beats), +# DW kept at 64 (default) for tractability. MAXLEN is a HARNESS-only knob. +prove_deep: chparam -set MAXLEN 3 fv_umi_txn +prove_deep_bw: chparam -set MAXLEN 3 fv_umi_txn +prep -top fv_umi_txn + +[files] +../../sumi/umi_checker/rtl/umi_txn_checker.sv +../../sumi/include/umi_messages.vh +fv_umi_txn.sv diff --git a/umi/formal/sumi/fv_umi_txn.sv b/umi/formal/sumi/fv_umi_txn.sv new file mode 100644 index 00000000..17432287 --- /dev/null +++ b/umi/formal/sumi/fv_umi_txn.sv @@ -0,0 +1,671 @@ +/******************************************************************************* + * Copyright 2026 Zero ASIC Corporation + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * + * ---- + * + * Documentation: + * + * Formal harness: umi_txn_checker (response-side L2 / framing rules) + * driven by a small requester + responder model. + * + * (anyseq legal requests) --> fv_umi_responder --clean resp--> [corrupt] + * | | + * +--(hierarchical glue lemmas)--+ + * | v + * +----------------------> umi_txn_checker + * (ASSERT face) + * + * The requester builds LEGAL single-beat requests from anyseq fields + * (opcode in {READ,WRITE,ATOMIC}, legal ATYPE, EOM=1). The responder is + * a perfect in-order device model: it enqueues each request that + * expects a response, and emits the matching response -- splitting reads + * word-per-beat, choosing ERR/data freely (anyseq) -- HS-clean by + * construction. The checker observes both channels and must never fire. + * + * OPERATING CONDITION -- NO INTERLEAVE. This harness drives a SINGLE + * point-to-point link: one responder, responses in request order. That + * is exactly the condition umi_txn_checker assumes (see its header and + * umi/formal/README.md). Because there is no interleave, the checker's + * shadow FIFO equals the responder's queue ENTRY-FOR-ENTRY -- the glue + * lemmas below are a DIRECT equality, not a per-key subsequence. + * + * Why the glue lemmas. The checker is stateful; a bare k-induction step + * may place the checker's tracker out of sync with the responder and + * then "discover" a field-copy violation that no reachable trace + * exhibits. The glue lemmas (a_glue_*) are the inductive strengthening: + * (1) the checker's queue equals the responder's queue, and (2) the + * live response beat equals the responder's head. Together they discharge + * every checker assertion. They are ASSERTED (proven), never assumed. + * + * Fault tasks (see fv_umi_txn.sby). Each FV_FAULT_* corrupts ONLY the + * response view the CHECKER sees (the [corrupt] block), leaving the + * responder -- and therefore every glue lemma -- clean, so each fault + * trips its intended checker assertion. Some corruptions violate several + * related rules on the same beat, and which label BMC reports is + * solver-dependent (fv_umi_txn.sby tabulates the intended and alternate + * labels per fault). The + * two exceptions carry no corruption at all: fault_msgbytes shrinks the + * FRM-4 ceiling (chparam MAX_MSG_BYTES) under a legal over-long message, + * and fault_occ shrinks the tracker capacity (chparam CAP) under two + * legal outstanding requests -- the checker convicts its own bound. + * + * Decode note: the checker keeps its own module-local field decoders + * (portable subset, no package). This formal-only harness shares its + * decoders through the txf package, referenced by explicit scope + * (txf::op5 ...), which yosys read_verilog accepts (an in-module + * `import pkg::*` does not parse). Both slice identical umi_messages.vh + * positions. + ******************************************************************************/ + +`default_nettype none + +// Shared field kernels for the responder and the harness (formal-only). +package txf; +`include "umi_messages.vh" + function automatic logic [4:0] op5(input logic [31:0] c); + op5 = c[UMI_OPCODE_MSB:UMI_OPCODE_LSB]; endfunction + function automatic logic [7:0] opbyte(input logic [31:0] c); + opbyte = c[7:0]; endfunction + function automatic logic [2:0] size(input logic [31:0] c); + size = c[UMI_SIZE_MSB:UMI_SIZE_LSB]; endfunction + function automatic logic [7:0] len(input logic [31:0] c); + len = c[UMI_LEN_MSB:UMI_LEN_LSB]; endfunction + function automatic logic [3:0] qos(input logic [31:0] c); + qos = c[UMI_QOS_MSB:UMI_QOS_LSB]; endfunction + function automatic logic [1:0] prot(input logic [31:0] c); + prot = c[UMI_PROT_MSB:UMI_PROT_LSB]; endfunction + function automatic logic eom(input logic [31:0] c); + eom = c[UMI_EOM_BIT]; endfunction + function automatic logic eof(input logic [31:0] c); + eof = c[UMI_EOF_BIT]; endfunction + function automatic logic ex(input logic [31:0] c); + ex = c[UMI_EX_BIT]; endfunction + function automatic logic [1:0] user(input logic [31:0] c); + user = c[UMI_USER_MSB:UMI_USER_LSB]; endfunction + function automatic logic [4:0] hostid(input logic [31:0] c); + hostid = c[UMI_HOSTID_MSB:UMI_HOSTID_LSB]; endfunction + function automatic logic is_req(input logic [31:0] c); + is_req = c[0] && (opbyte(c) != UMI_INVALID); endfunction + function automatic logic is_resp(input logic [31:0] c); + is_resp = !c[0] && (opbyte(c) != UMI_INVALID); endfunction + function automatic logic is_link(input logic [31:0] c); + is_link = (opbyte(c) == UMI_REQ_LINK) || (opbyte(c) == UMI_RESP_LINK); + endfunction + function automatic logic is_fullbyte(input logic [31:0] c); + is_fullbyte = (opbyte(c) == UMI_REQ_ERROR) || (opbyte(c) == UMI_REQ_LINK) + || (opbyte(c) == UMI_RESP_LINK); endfunction + function automatic logic expects_resp(input logic [31:0] c); + expects_resp = is_req(c) && !is_fullbyte(c) + && ((op5(c) == UMI_REQ_READ) || (op5(c) == UMI_REQ_WRITE) + || (op5(c) == UMI_REQ_ATOMIC)); endfunction + function automatic logic [4:0] resp_op5(input logic [31:0] c); + resp_op5 = (op5(c) == UMI_REQ_WRITE) ? UMI_RESP_WRITE[4:0] + : UMI_RESP_READ[4:0]; endfunction + function automatic logic [15:0] bytes(input logic [31:0] c); + bytes = (16'd1 << size(c)) * ({8'd0, len(c)} + 16'd1); endfunction + function automatic logic has_data(input logic [31:0] c); + has_data = (op5(c) == UMI_REQ_WRITE) || (op5(c) == UMI_REQ_POSTED) + || (op5(c) == UMI_REQ_ATOMIC) || (op5(c) == UMI_REQ_USER0) + || (op5(c) == UMI_REQ_FUTURE0) || (op5(c) == UMI_RESP_READ) + || (op5(c) == UMI_RESP_USER1) || (op5(c) == UMI_RESP_FUTURE1); + endfunction + function automatic logic [15:0] bytes_rel(input logic [31:0] c); + bytes_rel = !has_data(c) ? 16'd0 + : (op5(c) == UMI_REQ_ATOMIC) ? (16'd1 << size(c)) + : bytes(c); endfunction +endpackage + +// --------------------------------------------------------------------------- +// Perfect in-order responder model. One HOSTID stream, responses in +// request order, reads split word-per-beat. Free choices are anyseq. +// Internal state (occ, q0/q1, got_m, first_m, err_lat, err_pick) is read +// hierarchically by the harness glue. +// --------------------------------------------------------------------------- +module fv_umi_responder #( + parameter CW = 32, + parameter AW = 64, + parameter DW = 64 +) ( + input wire clk, + input wire nreset, + input wire req_valid, + output wire req_ready, + input wire [CW-1:0] req_cmd, + input wire [AW-1:0] req_srcaddr, + input wire resp_ready, + output wire resp_valid, + output wire [CW-1:0] resp_cmd, + output wire [AW-1:0] resp_dstaddr, + output wire [DW-1:0] resp_data, + // observation outputs for the harness glue (same packing as the checker) + output wire [1:0] f_occ, + output wire [15:0] f_got, + output wire f_first, + output wire [1:0] f_errlat, + output wire f_errpick, + output wire [AW+43:0] f_q0, + output wire [AW+43:0] f_q1 +); + // verilator lint_off UNUSEDPARAM +`include "umi_messages.vh" + // verilator lint_on UNUSEDPARAM + localparam [1:0] ERR_OK = 2'd0, ERR_EXOK = 2'd1, + ERR_DEVERR = 2'd2, ERR_NETERR = 2'd3; + + (* anyseq *) wire [1:0] f_err_sel; + (* anyseq *) wire [DW-1:0] f_mem_data; + + wire req_beat = req_valid && req_ready; + wire push_req = req_beat && txf::expects_resp(req_cmd) && txf::eom(req_cmd); + wire [15:0] push_bytes = + (txf::op5(req_cmd) == UMI_REQ_WRITE) ? 16'd0 + : (txf::op5(req_cmd) == UMI_REQ_ATOMIC) ? (16'd1 << txf::size(req_cmd)) + : txf::bytes(req_cmd); + + reg [1:0] occ; + reg [4:0] q0_ropc, q1_ropc; + reg [2:0] q0_size, q1_size; + reg [7:0] q0_len, q1_len; + reg [3:0] q0_qos, q1_qos; + reg [1:0] q0_prot, q1_prot; + reg q0_ex, q1_ex; + reg [4:0] q0_hostid, q1_hostid; + reg [AW-1:0] q0_da, q1_da; + reg [15:0] q0_bytes, q1_bytes; + + // registered offer (HS-clean: held stable while stalled) + reg off_v; + reg [4:0] off_ropc; + reg [2:0] off_size; + reg [7:0] off_len; + reg [3:0] off_qos; + reg [1:0] off_prot; + reg [4:0] off_hostid; + reg off_eom; + reg [1:0] off_err; + reg [AW-1:0] off_da; + reg [DW-1:0] off_data; + reg [1:0] err_lat; + reg err_pick; + reg [15:0] got_m; + reg first_m; + + wire [15:0] step_bytes = (16'd1 << q0_size); // one word per split beat + + wire [1:0] err_choice = (f_err_sel == ERR_EXOK && !q0_ex) ? ERR_OK : f_err_sel; + wire [1:0] err_now = err_pick ? err_lat : err_choice; + wire err_now_is_err = (err_now == ERR_DEVERR) || (err_now == ERR_NETERR); + + wire accept = off_v && resp_ready; + wire pop_q = accept && off_eom; + + assign req_ready = (occ != 2'd2) || pop_q; // blocks only at CAP + + initial begin + occ = 2'd0; off_v = 1'b0; err_pick = 1'b0; got_m = 16'd0; first_m = 1'b1; + end + + always @(posedge clk) begin + if (!nreset) begin + occ <= 2'd0; off_v <= 1'b0; err_pick <= 1'b0; + got_m <= 16'd0; first_m <= 1'b1; + end else begin + case ({push_req, pop_q}) + 2'b10: begin + if (occ == 2'd0) begin + q0_ropc <= txf::resp_op5(req_cmd); q0_size <= txf::size(req_cmd); + q0_len <= txf::len(req_cmd); q0_qos <= txf::qos(req_cmd); + q0_prot <= txf::prot(req_cmd); q0_ex <= txf::ex(req_cmd); + q0_hostid <= txf::hostid(req_cmd); q0_da <= req_srcaddr; + q0_bytes <= push_bytes; + end else begin + q1_ropc <= txf::resp_op5(req_cmd); q1_size <= txf::size(req_cmd); + q1_len <= txf::len(req_cmd); q1_qos <= txf::qos(req_cmd); + q1_prot <= txf::prot(req_cmd); q1_ex <= txf::ex(req_cmd); + q1_hostid <= txf::hostid(req_cmd); q1_da <= req_srcaddr; + q1_bytes <= push_bytes; + end + occ <= occ + 2'd1; + end + 2'b01: begin + q0_ropc <= q1_ropc; q0_size <= q1_size; q0_len <= q1_len; + q0_qos <= q1_qos; q0_prot <= q1_prot; q0_ex <= q1_ex; + q0_hostid <= q1_hostid; q0_da <= q1_da; q0_bytes <= q1_bytes; + occ <= occ - 2'd1; + end + 2'b11: begin + if (occ == 2'd1) begin + q0_ropc <= txf::resp_op5(req_cmd); q0_size <= txf::size(req_cmd); + q0_len <= txf::len(req_cmd); q0_qos <= txf::qos(req_cmd); + q0_prot <= txf::prot(req_cmd); q0_ex <= txf::ex(req_cmd); + q0_hostid <= txf::hostid(req_cmd); q0_da <= req_srcaddr; + q0_bytes <= push_bytes; + end else begin + q0_ropc <= q1_ropc; q0_size <= q1_size; q0_len <= q1_len; + q0_qos <= q1_qos; q0_prot <= q1_prot; q0_ex <= q1_ex; + q0_hostid <= q1_hostid; q0_da <= q1_da; q0_bytes <= q1_bytes; + q1_ropc <= txf::resp_op5(req_cmd); q1_size <= txf::size(req_cmd); + q1_len <= txf::len(req_cmd); q1_qos <= txf::qos(req_cmd); + q1_prot <= txf::prot(req_cmd); q1_ex <= txf::ex(req_cmd); + q1_hostid <= txf::hostid(req_cmd); q1_da <= req_srcaddr; + q1_bytes <= push_bytes; + end + end + default: ; + endcase + + if (accept) begin + off_v <= 1'b0; + if (off_eom) begin + err_pick <= 1'b0; got_m <= 16'd0; first_m <= 1'b1; + end else begin + got_m <= got_m + txf::bytes_rel(resp_cmd); first_m <= 1'b0; + end + end else if (!off_v && occ != 2'd0) begin + off_v <= 1'b1; + off_ropc <= q0_ropc; + off_size <= q0_size; + off_qos <= q0_qos; + off_prot <= q0_prot; + off_hostid <= q0_hostid; + off_err <= err_now; + off_data <= f_mem_data; + off_len <= err_now_is_err ? q0_len + : ((q0_ropc == UMI_RESP_WRITE[4:0]) ? q0_len : 8'd0); + off_eom <= (q0_ropc == UMI_RESP_WRITE[4:0]) || err_now_is_err + || ((q0_bytes - got_m) <= step_bytes); + off_da <= q0_da + {{(AW-16){1'b0}}, got_m}; + if (!err_pick) begin + err_lat <= err_choice; err_pick <= 1'b1; + end + end + end + end + + assign resp_valid = off_v; + assign resp_cmd = + {27'd0, off_ropc} + | ({29'd0, off_size} << UMI_SIZE_LSB) + | ({24'd0, off_len} << UMI_LEN_LSB) + | ({28'd0, off_qos} << UMI_QOS_LSB) + | ({30'd0, off_prot} << UMI_PROT_LSB) + | ({31'd0, off_eom} << UMI_EOM_BIT) + | (32'd1 << UMI_EOF_BIT) + | ({30'd0, off_err} << UMI_USER_LSB) + | ({27'd0, off_hostid} << UMI_HOSTID_LSB); + assign resp_dstaddr = off_da; + assign resp_data = err_now_is_err ? {DW{1'b0}} : off_data; + + assign f_occ = occ; + assign f_got = got_m; + assign f_first = first_m; + assign f_errlat = err_lat; + assign f_errpick = err_pick; + assign f_q0 = {q0_bytes, q0_da, q0_hostid, q0_ex, q0_prot, q0_qos, + q0_len, q0_size, q0_ropc}; + assign f_q1 = {q1_bytes, q1_da, q1_hostid, q1_ex, q1_prot, q1_qos, + q1_len, q1_size, q1_ropc}; +endmodule + +// --------------------------------------------------------------------------- +// The harness top. +// --------------------------------------------------------------------------- +module fv_umi_txn #( + parameter CW = 32, + parameter AW = 64, + parameter DW = 64, + parameter CAP = 2, + parameter [31:0] MAX_MSG_BYTES = 32768, + parameter [7:0] MAXLEN = 8'd1 // request LEN ceiling (shallow proof) +) ( + input wire clk +); + // verilator lint_off UNUSEDPARAM +`include "umi_messages.vh" + // verilator lint_on UNUSEDPARAM + localparam [1:0] ERR_OK = 2'd0, ERR_EXOK = 2'd1, + ERR_DEVERR = 2'd2, ERR_NETERR = 2'd3; + + // Effective request-LEN ceiling: this MUST match the m_len assumption + // below so the byte-bound glue lemmas (a_glue_e0_bytes/e1_bytes) stay + // TRUE for the legal environment. FV_BIGMSG (fault_msgbytes) relaxes the + // ceiling to 7 words; a MAXLEN-only bound would falsely fire at the + // enqueue and mask the intended TXN_msgbytes conviction. +`ifdef FV_BIGMSG + localparam [7:0] LEN_CEIL = 8'd7; +`else + localparam [7:0] LEN_CEIL = MAXLEN; +`endif + + // ---- reset: free, but asserted at time zero (grounds induction) ---- + (* anyseq *) wire nreset; + reg f_past = 1'b0; + always @(posedge clk) f_past <= 1'b1; + always @(*) if (!f_past) assume (!nreset); + + // ---- requester: LEGAL single-beat requests from anyseq fields ---- + (* anyseq *) wire [1:0] a_opsel; + (* anyseq *) wire [2:0] a_size; + (* anyseq *) wire [7:0] a_len; + (* anyseq *) wire [3:0] a_qos; + (* anyseq *) wire [1:0] a_prot; + (* anyseq *) wire a_ex; + (* anyseq *) wire [4:0] a_hostid; + (* anyseq *) wire [AW-1:0] a_srcaddr; + (* anyseq *) wire req_valid; + (* anyseq *) wire resp_ready; + + wire [4:0] req_op5 = (a_opsel == 2'd1) ? UMI_REQ_WRITE[4:0] + : (a_opsel == 2'd2) ? UMI_REQ_ATOMIC[4:0] + : UMI_REQ_READ[4:0]; + wire is_atomic = (req_op5 == UMI_REQ_ATOMIC[4:0]); + // ATYPE (rides LEN) legal 0..8; other requests take the free LEN + wire [7:0] len_use = is_atomic ? {5'd0, a_len[2:0]} : a_len; + wire ex_use = is_atomic ? 1'b0 : a_ex; + + wire [CW-1:0] req_cmd = + {27'd0, req_op5} + | ({29'd0, a_size} << UMI_SIZE_LSB) + | ({24'd0, len_use} << UMI_LEN_LSB) + | ({28'd0, a_qos} << UMI_QOS_LSB) + | ({30'd0, a_prot} << UMI_PROT_LSB) + | (32'd1 << UMI_EOM_BIT) + | (32'd1 << UMI_EOF_BIT) + | ({31'd0, ex_use} << UMI_EX_BIT) + | ({27'd0, a_hostid} << UMI_HOSTID_LSB); + + // ---- responder ---- + wire req_ready; + wire rsp_valid; + wire [CW-1:0] rsp_cmd; + wire [AW-1:0] rsp_dstaddr; + wire [DW-1:0] rsp_data; + // responder shadow state (glue) + wire [1:0] rsp_occ; + wire [15:0] rsp_got; + wire rsp_first; + wire [1:0] rsp_errlat; + wire rsp_errpick; + wire [AW+43:0] rq0, rq1; + + fv_umi_responder #(.CW(CW), .AW(AW), .DW(DW)) u_rsp ( + .clk(clk), .nreset(nreset), + .req_valid(req_valid), .req_ready(req_ready), + .req_cmd(req_cmd), .req_srcaddr(a_srcaddr), + .resp_ready(resp_ready), + .resp_valid(rsp_valid), .resp_cmd(rsp_cmd), + .resp_dstaddr(rsp_dstaddr), .resp_data(rsp_data), + .f_occ(rsp_occ), .f_got(rsp_got), .f_first(rsp_first), + .f_errlat(rsp_errlat), .f_errpick(rsp_errpick), + .f_q0(rq0), .f_q1(rq1)); + + // head field accessors on the responder's packed queue entries + wire [4:0] rq0_ropc = rq0[4:0]; + wire [2:0] rq0_size = rq0[7:5]; + wire [7:0] rq0_len = rq0[15:8]; + wire rq0_ex = rq0[22]; + wire [AW-1:0] rq0_da = rq0[AW+27:28]; + wire [15:0] rq0_bytes = rq0[AW+43:AW+28]; + + // ---- fault injection: corrupt ONLY the checker's response view ---- + // The responder outputs (rsp_*) stay clean, so every glue lemma holds + // and each fault trips its intended checker assertion. A given fault + // may also falsify several related rules on the same beat, and which + // label the solver reports can vary; fv_umi_txn.sby tabulates the + // intended label and the extra/alternate labels for each fault. + localparam [CW-1:0] SPUR_RESP = {27'd0, UMI_RESP_READ[4:0]} + | (32'd1 << UMI_EOM_BIT) + | (32'd1 << UMI_EOF_BIT); // idle-orphan beat + (* anyseq *) wire fault_go; + + wire c_valid; + wire [CW-1:0] c_cmd; + wire [AW-1:0] c_dstaddr; + wire [DW-1:0] c_data; + +`ifdef FV_FAULT_WRONGDA + // first-beat DA off by 8 (every beat, but the first-beat law fires first) + assign c_valid = rsp_valid; + assign c_cmd = rsp_cmd; + assign c_dstaddr = rsp_dstaddr + 64'd8; + assign c_data = rsp_data; +`elsif FV_FAULT_SIZE + // mid-message SIZE mutation: flip SIZE only on a continuation beat + assign c_valid = rsp_valid; + assign c_cmd = rsp_cmd + ^ ((rsp_valid && !rsp_first) ? (32'd1 << UMI_SIZE_LSB) : 32'd0); + assign c_dstaddr = rsp_dstaddr; + assign c_data = rsp_data; +`elsif FV_FAULT_EOM_EARLY + // EOM asserted on a split first beat that has more to come + assign c_valid = rsp_valid; + assign c_cmd = rsp_cmd + | ((rsp_valid && rsp_first && !rsp_cmd[UMI_EOM_BIT]) + ? (32'd1 << UMI_EOM_BIT) : 32'd0); + assign c_dstaddr = rsp_dstaddr; + assign c_data = rsp_data; +`elsif FV_FAULT_EOM_MISSING + // EOM never reaches the checker: the closing beat looks unterminated + assign c_valid = rsp_valid; + assign c_cmd = rsp_cmd & ~(32'd1 << UMI_EOM_BIT); + assign c_dstaddr = rsp_dstaddr; + assign c_data = rsp_data; +`elsif FV_FAULT_ERR_LEN + // error response with a mangled LEN (!= the request LEN it must copy) + assign c_valid = rsp_valid; + assign c_cmd = rsp_cmd + ^ (((txf::user(rsp_cmd) == ERR_DEVERR) + || (txf::user(rsp_cmd) == ERR_NETERR)) + ? (32'd1 << UMI_LEN_LSB) : 32'd0); + assign c_dstaddr = rsp_dstaddr; + assign c_data = rsp_data; +`elsif FV_FAULT_ORPHAN + // a spurious response beat while the tracker is empty + wire spur = fault_go && (rsp_occ == 2'd0) && !rsp_valid; + assign c_valid = rsp_valid | spur; + assign c_cmd = spur ? SPUR_RESP : rsp_cmd; + assign c_dstaddr = rsp_dstaddr; + assign c_data = spur ? {DW{1'b0}} : rsp_data; +`else + // clean: the checker sees exactly what the responder emits + assign c_valid = rsp_valid; + assign c_cmd = rsp_cmd; + assign c_dstaddr = rsp_dstaddr; + assign c_data = rsp_data; +`endif + + // ---- the checker under test (ASSERT face) ---- + wire [1:0] chk_occ; + wire [15:0] chk_got; + wire chk_first; + wire [AW-1:0] chk_next_da; + wire [CW-1:0] chk_last; + wire [AW+43:0] chk_e0, chk_e1; + + umi_txn_checker #( + .CW(CW), .AW(AW), .DW(DW), + .CAP(CAP), .MAX_MSG_BYTES(MAX_MSG_BYTES), .ASSUME(0) + ) u_chk ( + .clk(clk), .nreset(nreset), + .req_valid(req_valid), .req_ready(req_ready), .req_cmd(req_cmd), + .req_dstaddr({AW{1'b0}}), .req_srcaddr(a_srcaddr), .req_data({DW{1'b0}}), + .resp_valid(c_valid), .resp_ready(resp_ready), .resp_cmd(c_cmd), + .resp_dstaddr(c_dstaddr), .resp_srcaddr({AW{1'b0}}), .resp_data(c_data), + .f_occ(chk_occ), .f_got(chk_got), .f_first(chk_first), + .f_next_da(chk_next_da), .f_last_cmd(chk_last), + .f_e0(chk_e0), .f_e1(chk_e1)); + + // ---- environment discipline + witnesses ---- + reg seen_reset = 1'b0; + always @(posedge clk) if (!nreset) seen_reset <= 1'b1; + reg guard = 1'b0; + always @(posedge clk) if (!nreset) guard <= 1'b0; else guard <= seen_reset; + + always @(posedge clk) begin + // shallow proof: bound request length (relaxed by FV_BIGMSG) +`ifdef FV_BIGMSG + m_len : assume (!req_valid || len_use <= 8'd7); +`else + m_len : assume (!req_valid || len_use <= MAXLEN); +`endif + end + + // ---- glue lemmas: the checker's tracker equals the responder's queue + // ---- (direct equality: NO INTERLEAVE), and the live beat equals the + // ---- responder head. Asserted, not assumed -- the induction scaffold. + wire [15:0] rsp_beat_bytes = txf::bytes_rel(rsp_cmd); + // Gate the glue lemmas on nreset -- the SAME condition under which the + // checker fires its own TXN_* assertions -- not on the 2-cycle `guard`. + // The checker rules constrain an INPUT response stream, so they can never + // be self-inductive: the strengthening glue must be part of the induction + // hypothesis in every cycle the checker asserts. Gating glue on `guard` + // let k-induction pick an unreachable start state (seen_reset=0, guard=0, + // nreset=1 forever) in which the glue was disabled while the checker rules + // still fired -- an unclosable step. All glue lemmas provably hold from + // the first post-reset cycle (occ/got/first are reset-synced and the + // shadow-entry lemmas are vacuous while occ==0), so nreset gating is + // sound; the basecase confirms it. + always @(posedge clk) begin + if (nreset) begin + a_glue_occ : assert (chk_occ == rsp_occ); + a_glue_first : assert (chk_first == rsp_first); + a_glue_got : assert (chk_got == rsp_got); + if (rsp_occ != 2'd0) + a_glue_e0 : assert (chk_e0 == rq0); + if (rsp_occ == 2'd2) + a_glue_e1 : assert (chk_e1 == rq1); + // Every occupied responder queue entry carries a RESPONSE opcode + // (RESP_READ/RESP_WRITE): the queue is only ever loaded from + // txf::resp_op5. Without this, an induction start state can seat + // an odd (request-shaped) opcode in the head, so the beat the + // checker sees fails f_is_resp -- the checker does not pop while + // the responder does, desyncing chk_occ/chk_e0 from the model. + if (rsp_occ != 2'd0) + a_glue_rq0_ropc : assert (rq0_ropc == UMI_RESP_READ[4:0] + || rq0_ropc == UMI_RESP_WRITE[4:0]); + if (rsp_occ == 2'd2) + a_glue_rq1_ropc : assert (rq1[4:0] == UMI_RESP_READ[4:0] + || rq1[4:0] == UMI_RESP_WRITE[4:0]); + // A write-ack head carries zero data bytes (push_bytes==0 for a + // WRITE request). Without this an induction start state can seat a + // nonzero byte count on a RESP_WRITE head; the responder then + // offers it as a non-EOM (split) beat that advances the message + // (first->0) while adding bytes_rel==0 -- an impossible open + // message with got==0, which breaks a_glue_mid_got/a_glue_next_da. + if (rsp_occ != 2'd0 && rq0_ropc == UMI_RESP_WRITE[4:0]) + a_glue_rq0_wr0 : assert (rq0_bytes == 16'd0); + if (rsp_occ == 2'd2 && rq1[4:0] == UMI_RESP_WRITE[4:0]) + a_glue_rq1_wr0 : assert (rq1[AW+43:AW+28] == 16'd0); + // A read/atomic head expects a whole, positive number of words: + // rq0_bytes = (2^size)*(len+1) (read) or 2^size (atomic), both + // positive multiples of the word step 2^size. The accumulator + // advances exactly one word (2^size) per split beat, so it too + // stays a multiple of the step. Together they keep the responder's + // word-per-beat split landing EXACTLY on rq0_bytes: an unaligned + // byte count would over/undershoot the closing beat and break + // a_glue_off_ok (got + step <= rq0_bytes, EOM iff exactly equal). + if (rsp_occ != 2'd0 && rq0_ropc == UMI_RESP_READ[4:0]) + a_glue_rq0_words : assert (rq0_bytes >= (16'd1 << rq0_size) + && ((rq0_bytes >> rq0_size) << rq0_size) == rq0_bytes); + if (rsp_occ == 2'd2 && rq1[4:0] == UMI_RESP_READ[4:0]) + a_glue_rq1_words : assert (rq1[AW+43:AW+28] >= (16'd1 << rq1[7:5]) + && ((rq1[AW+43:AW+28] >> rq1[7:5]) << rq1[7:5]) + == rq1[AW+43:AW+28]); + if (rsp_occ != 2'd0) + a_glue_got_align : assert (((rsp_got >> rq0_size) << rq0_size) + == rsp_got); + + // responder-internal invariants (make the head well-formed) + a_glue_rsp_occ : assert (rsp_occ <= 2'd2); + a_glue_rsp_base : assert (!rsp_first || rsp_got == 16'd0); + a_glue_rsp_idle : assert ((rsp_occ != 2'd0) || rsp_first); + if (!rsp_first) begin + a_glue_mid_occ : assert (rsp_occ != 2'd0); + a_glue_mid_pick : assert (rsp_errpick); + a_glue_mid_got : assert (rsp_got != 16'd0 && rsp_got < rq0_bytes); + end + if (rsp_errpick) begin + a_glue_lat_occ : assert (rsp_occ != 2'd0); + a_glue_lat_exok : assert ((rsp_errlat != ERR_EXOK) || rq0_ex); + if ((rsp_errlat == ERR_DEVERR) || (rsp_errlat == ERR_NETERR)) + a_glue_lat_first : assert (rsp_first); + end + // the head byte total never exceeds LEN_CEIL+1 words at push time + // (env LEN_CEIL keeps split messages short -- LEN<=1 -> <=2 words; + // LEN<=7 -> <=8 words under FV_BIGMSG). LEN_CEIL tracks m_len so + // this bound is TRUE for the legal environment in every task. + if (rsp_occ != 2'd0) + a_glue_e0_bytes : assert (rq0_bytes + <= (16'd1 << rq0_size) * ({8'd0, LEN_CEIL} + 16'd1)); + if (rsp_occ == 2'd2) + a_glue_e1_bytes : assert (rq1[AW+43:AW+28] + <= (16'd1 << rq1[7:5]) * ({8'd0, LEN_CEIL} + 16'd1)); + + // continuation-address / framing carry (checker next_da,last_cmd) + if (!chk_first) begin + a_glue_next_da : assert (chk_next_da + == rq0_da + {{(AW-16){1'b0}}, rsp_got}); + a_glue_last_err : assert (txf::user(chk_last) == rsp_errlat); + a_glue_last_eof : assert (txf::eof(chk_last)); + end + + // offer coherence: the live response beat IS the responder head + if (rsp_valid) begin + a_glue_off_occ : assert (rsp_occ != 2'd0); + a_glue_off_kind : assert (txf::op5(rsp_cmd) == rq0_ropc); + a_glue_off_size : assert (txf::size(rsp_cmd) == rq0_size); + a_glue_off_qos : assert (txf::qos(rsp_cmd) == rq0[19:16]); + a_glue_off_prot : assert (txf::prot(rsp_cmd) == rq0[21:20]); + a_glue_off_hid : assert (txf::hostid(rsp_cmd) == rq0[27:23]); + a_glue_off_eof : assert (txf::eof(rsp_cmd)); + a_glue_off_lat : assert (rsp_errpick && txf::user(rsp_cmd) == rsp_errlat); + a_glue_off_exok : assert ((txf::user(rsp_cmd) != ERR_EXOK) || rq0_ex); + if (rsp_first) + a_glue_off_da : assert (rsp_dstaddr == rq0_da); + else + a_glue_off_da2 : assert (rsp_dstaddr + == rq0_da + {{(AW-16){1'b0}}, rsp_got}); + if ((txf::user(rsp_cmd) == ERR_DEVERR) || (txf::user(rsp_cmd) == ERR_NETERR)) + a_glue_off_err : assert (txf::len(rsp_cmd) == rq0_len + && rsp_first && txf::eom(rsp_cmd)); + else + a_glue_off_ok : assert (({16'd0, rsp_got} + {16'd0, rsp_beat_bytes}) + <= {16'd0, rq0_bytes} + && txf::eom(rsp_cmd) == (({16'd0, rsp_got} + + {16'd0, rsp_beat_bytes}) + == {16'd0, rq0_bytes})); + end + end + end + + // ---- witnesses (formal-only): the assumed language is alive ---- +`ifdef FORMAL + always @(posedge clk) begin + if (guard) begin + c_journey : cover (c_valid && resp_ready && txf::eom(c_cmd) + && txf::op5(c_cmd) == UMI_RESP_READ[4:0]); + c_multibeat: cover (c_valid && resp_ready && !txf::eom(c_cmd)); + c_close : cover (c_valid && resp_ready && txf::eom(c_cmd) && !chk_first); + c_wr_ack : cover (c_valid && resp_ready + && txf::op5(c_cmd) == UMI_RESP_WRITE[4:0]); + c_err : cover (c_valid && resp_ready && txf::user(c_cmd) == ERR_DEVERR); + c_backtoback : cover (c_valid && resp_ready && rsp_occ == 2'd2); + end + end +`endif + +endmodule + +`default_nettype wire diff --git a/umi/sumi/__init__.py b/umi/sumi/__init__.py index e2573098..6e2477ee 100644 --- a/umi/sumi/__init__.py +++ b/umi/sumi/__init__.py @@ -1,5 +1,6 @@ from .umi_arbiter.umi_arbiter import Arbiter from .umi_buffer.umi_buffer import Buffer +from .umi_checker.umi_checker import Checker from .umi_crossbar.umi_crossbar import Crossbar from .umi_decode.umi_decode import Decode from .umi_endpoint.umi_endpoint import Endpoint @@ -24,6 +25,7 @@ __all__ = ['Arbiter', 'Buffer', + 'Checker', 'Crossbar', 'Decode', 'Endpoint', diff --git a/umi/sumi/umi_checker/rtl/umi_cmd_checker.sv b/umi/sumi/umi_checker/rtl/umi_cmd_checker.sv new file mode 100644 index 00000000..bd86c3bf --- /dev/null +++ b/umi/sumi/umi_checker/rtl/umi_cmd_checker.sv @@ -0,0 +1,418 @@ +/******************************************************************************* + * Copyright 2026 Zero ASIC Corporation + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * + * ---- + * + * Documentation: + * + * Passive protocol checker for SUMI command-word (CMD) legality. + * Attach one instance per SUMI channel, exactly like the handshake + * checker in this directory; it drives nothing and never interferes + * with the design. Every rule is a same-cycle predicate over the + * OFFERED beat (checked whenever VALID is high out of reset): a beat + * that is never accepted must still be a legal beat, so READY is + * deliberately not consulted. + * + * The rules, with their README (UMI spec) anchors: + * + * CMD1_opcode_legal OPCODE is one of the 13 structured opcodes or + * the 3 full-byte specials REQ_ERROR/REQ_LINK/ + * RESP_LINK (README 3.2.3 message-types table). + * INVALID (CMD[7:0]==0x00) and the reserved + * opcode holes are rejected on an offered beat. + * CMD2_atype_legal REQ_ATOMIC carries ATYPE in the LEN bit + * positions; only 0x00..0x08 (ADD..SWAP) are + * defined (README 3.3.9 ATYPE table). + * CMD4_da_aligned DA aligned to 2^SIZE whenever the message has + * CMD4_sa_aligned a DA (everything but LINK); SA aligned on + * requests (README 3.1 "Device and source + * addresses must be aligned to the native word + * size"). Response SA is undefined by README + * 3.3.1 and never checked. + * CMD6_sa_reserved (gated by CHECK_SA_RESERVED, default OFF, see + * below) request SA reserved bits are zero: + * SA[63:40] for AW>=64, SA[31:24] otherwise + * (README 3.3.1 SA bit map, 3.3.12 "R ... shall + * be set to zero"). + * CMD10_fullbyte_decode the full-byte opcode family is unambiguous: + * a 5-bit opcode of 0x0F must extend to + * REQ_ERROR (CMD[7:5]==0) or REQ_LINK + * (CMD[7:5]==1); 0x0E must extend to RESP_LINK + * (CMD[7:5]==0) (README 3.2.3 rows REQ_ERROR / + * REQ_LINK / RESP_LINK). + * CMD11_ex_zero EX==0 for REQ_WRPOSTED / REQ_RDMA / + * REQ_ATOMIC (README 3.2.3: bit 24 is "0" in + * those rows). + * CMD12_error_size the REQ_ERROR family (5-bit opcode 0x0F, not + * the REQ_LINK extension) carries SIZE==0 + * (README 3.2.3 REQ_ERROR row, SIZE column + * 0x0). NOTE: classified by the 5-bit opcode, + * not CMD[7:0]==0x0F -- the full-byte + * classification makes the rule a tautology + * (0x0F in [7:0] already forces [7:5]==0), i.e. + * unfalsifiable. The 5-bit form is falsifiable; + * the set of beats accepted by the checker as a + * whole is unchanged (every CMD-12 violation is + * also outside the CMD-1 legal-opcode set). + * Exhaustively: the per-rule extra rejects are + * exactly opbyte in {0x4F,0x6F,0x8F,0xAF,0xCF, + * 0xEF}, each already rejected by CMD-1 (not + * structured, not a legal full-byte), so the + * ten-rule conjunction accepts the identical + * language. + * CMD15_beat_capacity the bytes implied by SIZE/LEN for one beat -- + * (LEN+1)*2^SIZE, or 2^SIZE for atomics, or 0 + * for no-data messages -- fit the data bus: + * <= DW/8 (README 3.3.2 SIZE, 3.3.3 LEN; a SUMI + * packet is a complete routable mini-message, + * README 4.1). EXEMPTION: responses with + * ERR==DEVERR or ERR==NETERR are not convicted. + * An error response echoes the SIZE/LEN of a + * request that may span several beats, and by + * CMD16 it carries no data -- convicting a + * NETERR reply to a multi-beat read would be a + * spec-plausible false positive. + * CMD16_err_data_zero a response with ERR==DEVERR or ERR==NETERR + * carries no data: the byte lanes SIZE/LEN + * declare relevant must be zero (README 3.3.9 + * ERR codes; data-carrying rows in 3.2.3). + * + * ASSUME parameter: identical contract to umi_handshake_checker. + * ASSUME=0 (default): assert the rules -- attach to any channel the + * design under test drives (simulation or formal). + * ASSUME=1: assume the rules. Formal-only: constrains free inputs of + * a harness to legal command traffic. The same file is both + * the requirement and the environment, so the two can never + * drift apart. + * + * CHECK_SA_RESERVED parameter (default 0 = OFF): README 3.3.1 marks + * SA[63:40] (64b mode) reserved and 3.3.12 requires reserved bits to + * be zero -- but README 3.3.1 equally allows SA to be "a partial + * routing address and a set of optional UMI signal layer controls", + * and this repository's own reference traffic and bus adapters carry + * routing/implementation bits in the high SA bytes. Shipping the rule + * hard-on would convict the reference RTL and push adopters to turn + * the whole checker off, so the strict reserved-zero profile is opt-in + * (CHECK_SA_RESERVED=1). + * + * Implementation notes (same portable subset as umi_handshake_checker): + * - Field positions and opcode values come from umi_messages.vh, the + * repo's single source of truth. The only locally declared + * constants are the ERR codes, which umi_messages.vh does not + * define (README 3.3.9). + * - Named immediate assertions inside always blocks; each assert is + * paired with an `ifndef FORMAL $error twin whose !== comparison + * also catches X in 4-state simulation. Cover statements are + * formal-only (`ifdef FORMAL). + * - No $past, no sequences, no bind, no packages: the same file works + * under yosys/SymbiYosys (read_verilog -formal), Verilator + * (--assert), slang lint, and Icarus Verilog. + ******************************************************************************/ + +`default_nettype none + +module umi_cmd_checker #( + parameter CW = 32, // command width + parameter AW = 64, // address width + parameter DW = 256, // data width + parameter ASSUME = 0, // 0: assert the rules, 1: assume them + parameter CHECK_SA_RESERVED = 0 // 1: also require request SA reserved bits zero +) ( + input wire clk, + input wire nreset, + input wire valid, + input wire ready, + input wire [CW-1:0] cmd, + input wire [AW-1:0] dstaddr, + input wire [AW-1:0] srcaddr, + input wire [DW-1:0] data +); + + // the shared header declares every UMI constant; a checker uses + // only the command-legality subset, so the unused ones are waived + // verilator lint_off UNUSEDPARAM +`include "umi_messages.vh" + // verilator lint_on UNUSEDPARAM + + // ERR codes on the response USER/ERR field (README 3.3.9). These + // are the one set of constants not present in umi_messages.vh. + localparam [1:0] UMI_ERR_DEVERR = 2'd2; + localparam [1:0] UMI_ERR_NETERR = 2'd3; + + localparam [15:0] BEAT_BYTES = DW / 8; // data-bus capacity of one beat + + // beat legality is a property of the OFFERED beat, so READY is + // unused (kept so handshake- and cmd-checker binds look alike); + // QOS/PROT/EOM/EOF/HOSTID carry no per-beat legality obligation + wire unused_ok = &{1'b1, ready, + cmd[UMI_HOSTID_MSB:UMI_HOSTID_LSB], + cmd[UMI_EOF_BIT], + cmd[UMI_EOM_BIT], + cmd[UMI_PROT_MSB:UMI_PROT_LSB], + cmd[UMI_QOS_MSB:UMI_QOS_LSB]}; + + // ################################################################# + // # Field extraction (umi_messages.vh bit positions) + // ################################################################# + + wire [4:0] dec_op5 = cmd[UMI_OPCODE_MSB:UMI_OPCODE_LSB]; + wire [7:0] dec_opbyte = cmd[7:0]; // opcode + extension + wire [2:0] dec_size = cmd[UMI_SIZE_MSB:UMI_SIZE_LSB]; + wire [7:0] dec_len = cmd[UMI_LEN_MSB:UMI_LEN_LSB]; // ATYPE on REQ_ATOMIC + wire dec_ex = cmd[UMI_EX_BIT]; + wire [1:0] dec_userr = cmd[UMI_USER_MSB:UMI_USER_LSB]; // USER on req / ERR on resp + + // ################################################################# + // # Decode (message classes per README 3.2.3) + // ################################################################# + + // the thirteen structured opcodes (requests odd, responses even) + wire dec_structured = + (dec_op5 == UMI_REQ_READ) | (dec_op5 == UMI_REQ_WRITE) | + (dec_op5 == UMI_REQ_POSTED) | (dec_op5 == UMI_REQ_RDMA) | + (dec_op5 == UMI_REQ_ATOMIC) | (dec_op5 == UMI_REQ_USER0) | + (dec_op5 == UMI_REQ_FUTURE0) | + (dec_op5 == UMI_RESP_READ) | (dec_op5 == UMI_RESP_WRITE) | + (dec_op5 == UMI_RESP_USER0) | (dec_op5 == UMI_RESP_USER1) | + (dec_op5 == UMI_RESP_FUTURE0)| (dec_op5 == UMI_RESP_FUTURE1); + + // the three full-byte specials (opcode field spans CMD[7:0]) + wire dec_fullbyte = (dec_opbyte == UMI_REQ_ERROR) + | (dec_opbyte == UMI_REQ_LINK) + | (dec_opbyte == UMI_RESP_LINK); + + wire dec_is_link = (dec_opbyte == UMI_REQ_LINK) + | (dec_opbyte == UMI_RESP_LINK); + + // requests odd / responses even; INVALID (0x00) is neither + wire dec_is_req = cmd[0] & (dec_opbyte != UMI_INVALID); + wire dec_is_resp = ~cmd[0] & (dec_opbyte != UMI_INVALID); + + // field applicability (README 3.2.3 DATA/SA/DA columns): + // DA everywhere but LINK; SA on requests only (README 3.3.1 leaves + // response SA undefined, so it is never an obligation) + wire dec_has_da = ~dec_is_link; + wire dec_has_sa = dec_is_req & ~dec_is_link; + wire dec_has_data = (dec_op5 == UMI_REQ_WRITE) + | (dec_op5 == UMI_REQ_POSTED) + | (dec_op5 == UMI_REQ_ATOMIC) + | (dec_op5 == UMI_REQ_USER0) + | (dec_op5 == UMI_REQ_FUTURE0) + | (dec_op5 == UMI_RESP_READ) + | (dec_op5 == UMI_RESP_USER1) + | (dec_op5 == UMI_RESP_FUTURE1); + + // bytes carried by ONE beat of this message (relevance-aware): + // no-data messages carry 0; atomics carry 2^SIZE (LEN aliases + // ATYPE, the LEN formula never applies); else (LEN+1)*2^SIZE + // (README 3.3.2 / 3.3.3) + wire [15:0] dec_words = {8'd0, dec_len} + 16'd1; + wire [15:0] dec_bytes = (16'd1 << dec_size) * dec_words; + wire [15:0] dec_bytes_rel = ~dec_has_data ? 16'd0 + : (dec_op5 == UMI_REQ_ATOMIC) ? (16'd1 << dec_size) + : dec_bytes; + + // alignment kernel (README 3.1): low SIZE bits of an address zero + localparam [AW-1:0] ADDR_ONE = {{(AW-1){1'b0}}, 1'b1}; + wire [AW-1:0] dec_align_mask = (ADDR_ONE << dec_size) - ADDR_ONE; + wire dec_da_aligned = ((dstaddr & dec_align_mask) == {AW{1'b0}}); + wire dec_sa_aligned = ((srcaddr & dec_align_mask) == {AW{1'b0}}); + + // request SA reserved bits (README 3.3.1 SA bit map) + wire dec_sa_res_zero; + generate + if (AW >= 64) begin : g_sa_64b + assign dec_sa_res_zero = (srcaddr[63:40] == 24'd0); + end else begin : g_sa_32b + assign dec_sa_res_zero = (srcaddr[AW-1:AW-8] == 8'd0); + end + endgenerate + + // byte-lane relevance mask for CMD16: lane i is relevant when + // i < bytes carried by the beat + wire [BEAT_BYTES-1:0] dec_rel_lane; + wire [DW-1:0] dec_rel_mask; + genvar gi; + generate + for (gi = 0; gi < DW/8; gi = gi + 1) begin : g_rel + // gi is an elaboration constant; the sized localparam keeps + // the lane compare pure 16-bit unsigned + localparam [15:0] GLANE = gi[15:0]; + assign dec_rel_lane[gi] = (GLANE < dec_bytes_rel); + assign dec_rel_mask[8*gi +: 8] = {8{dec_rel_lane[gi]}}; + end + endgenerate + + // ################################################################# + // # The rules (one wire per rule; the same wire is asserted or + // # assumed depending on ASSUME) + // ################################################################# + + wire dec_cmd1_ok = dec_structured | dec_fullbyte; + + wire dec_cmd2_ok = (dec_op5 != UMI_REQ_ATOMIC) + | (dec_len <= UMI_REQ_ATOMICSWAP); + + wire dec_cmd4a_ok = ~dec_has_da | dec_da_aligned; + wire dec_cmd4b_ok = ~dec_has_sa | dec_sa_aligned; + + wire dec_cmd6_ok = ~dec_has_sa | dec_sa_res_zero; + + // 5-bit opcode 0x0F is REQ_ERROR/REQ_LINK territory, 0x0E is + // RESP_LINK territory; any other extension is an aliasing error + wire dec_cmd10_ok = ((dec_op5 != UMI_REQ_ERROR[4:0]) + | (cmd[7:5] == 3'd0) | (cmd[7:5] == 3'd1)) + & ((dec_op5 != UMI_RESP_LINK[4:0]) + | (cmd[7:5] == 3'd0)); + + wire dec_cmd11_ok = ~(((dec_op5 == UMI_REQ_POSTED) + | (dec_op5 == UMI_REQ_RDMA) + | (dec_op5 == UMI_REQ_ATOMIC)) & dec_ex); + + // REQ_ERROR family by 5-bit opcode, REQ_LINK extension exempt -- + // see the CMD12 header note on falsifiability + wire dec_cmd12_ok = (dec_op5 != UMI_REQ_ERROR[4:0]) + | (cmd[7:5] == 3'd1) + | (dec_size == 3'd0); + + // DEVERR/NETERR response: exempt from beat capacity (CMD15, see + // header) and must carry all-zero relevant data lanes (CMD16) + wire dec_err_resp = dec_is_resp & ((dec_userr == UMI_ERR_DEVERR) + | (dec_userr == UMI_ERR_NETERR)); + + wire dec_cmd15_ok = dec_err_resp | (dec_bytes_rel <= BEAT_BYTES); + + wire dec_cmd16_ok = ~(dec_err_resp & dec_has_data) + | ((data & dec_rel_mask) == {DW{1'b0}}); + + // ################################################################# + // # Assert or assume (one generate arm per direction) + // ################################################################# + + generate + if (ASSUME == 0) begin : g_assert + + always @(posedge clk) begin + if (nreset & valid) begin + CMD1_opcode_legal : assert (dec_cmd1_ok); +`ifndef FORMAL + if ((dec_cmd1_ok) !== 1'b1) + $error("UMI-CMD CMD-1 %m: illegal OPCODE on a valid beat (README 3.2.3 message-types table)"); +`endif + CMD2_atype_legal : assert (dec_cmd2_ok); +`ifndef FORMAL + if ((dec_cmd2_ok) !== 1'b1) + $error("UMI-CMD CMD-2 %m: REQ_ATOMIC with ATYPE above ATOMICSWAP (README 3.3.9 ATYPE table)"); +`endif + CMD4_da_aligned : assert (dec_cmd4a_ok); +`ifndef FORMAL + if ((dec_cmd4a_ok) !== 1'b1) + $error("UMI-CMD CMD-4 %m: DSTADDR not aligned to 2^SIZE (README 3.1)"); +`endif + CMD4_sa_aligned : assert (dec_cmd4b_ok); +`ifndef FORMAL + if ((dec_cmd4b_ok) !== 1'b1) + $error("UMI-CMD CMD-4 %m: request SRCADDR not aligned to 2^SIZE (README 3.1)"); +`endif + if (CHECK_SA_RESERVED != 0) begin + CMD6_sa_reserved : assert (dec_cmd6_ok); +`ifndef FORMAL + if ((dec_cmd6_ok) !== 1'b1) + $error("UMI-CMD CMD-6 %m: request SRCADDR reserved bits nonzero (README 3.3.1/3.3.12)"); +`endif + end + CMD10_fullbyte_decode : assert (dec_cmd10_ok); +`ifndef FORMAL + if ((dec_cmd10_ok) !== 1'b1) + $error("UMI-CMD CMD-10 %m: full-byte opcode family aliased outside REQ_ERROR/REQ_LINK/RESP_LINK (README 3.2.3)"); +`endif + CMD11_ex_zero : assert (dec_cmd11_ok); +`ifndef FORMAL + if ((dec_cmd11_ok) !== 1'b1) + $error("UMI-CMD CMD-11 %m: EX set on REQ_WRPOSTED/REQ_RDMA/REQ_ATOMIC (README 3.2.3)"); +`endif + CMD12_error_size : assert (dec_cmd12_ok); +`ifndef FORMAL + if ((dec_cmd12_ok) !== 1'b1) + $error("UMI-CMD CMD-12 %m: REQ_ERROR with SIZE != 0 (README 3.2.3 REQ_ERROR row)"); +`endif + CMD15_beat_capacity : assert (dec_cmd15_ok); +`ifndef FORMAL + if ((dec_cmd15_ok) !== 1'b1) + $error("UMI-CMD CMD-15 %m: SIZE/LEN imply more bytes than one DW-bit beat carries (README 3.3.2/3.3.3)"); +`endif + CMD16_err_data_zero : assert (dec_cmd16_ok); +`ifndef FORMAL + if ((dec_cmd16_ok) !== 1'b1) + $error("UMI-CMD CMD-16 %m: DEVERR/NETERR response carrying nonzero data in relevant byte lanes (README 3.3.9)"); +`endif + end + end + + end else begin : g_assume +`ifdef FORMAL + always @(posedge clk) begin + if (nreset & valid) begin + CMD1_opcode_legal : assume (dec_cmd1_ok); + CMD2_atype_legal : assume (dec_cmd2_ok); + CMD4_da_aligned : assume (dec_cmd4a_ok); + CMD4_sa_aligned : assume (dec_cmd4b_ok); + if (CHECK_SA_RESERVED != 0) + CMD6_sa_reserved : assume (dec_cmd6_ok); + CMD10_fullbyte_decode : assume (dec_cmd10_ok); + CMD11_ex_zero : assume (dec_cmd11_ok); + CMD12_error_size : assume (dec_cmd12_ok); + CMD15_beat_capacity : assume (dec_cmd15_ok); + CMD16_err_data_zero : assume (dec_cmd16_ok); + end + end +`endif + end + endgenerate + + // ################################################################# + // # Vacuity witnesses (formal-only) + // ################################################################# + // A command-legality proof over an environment that can not reach + // every legal opcode -- or a full-capacity beat -- proves nothing. + // These covers fail loudly (unreached) if a harness or a bind + // over-constrains the channel. + +`ifdef FORMAL + always @(posedge clk) begin + if (nreset & valid) begin + SAW_req_read : cover (dec_op5 == UMI_REQ_READ); + SAW_req_write : cover (dec_op5 == UMI_REQ_WRITE); + SAW_req_posted : cover (dec_op5 == UMI_REQ_POSTED); + SAW_req_rdma : cover (dec_op5 == UMI_REQ_RDMA); + SAW_req_atomic : cover (dec_op5 == UMI_REQ_ATOMIC); + SAW_req_user0 : cover (dec_op5 == UMI_REQ_USER0); + SAW_req_future0 : cover (dec_op5 == UMI_REQ_FUTURE0); + SAW_resp_read : cover (dec_op5 == UMI_RESP_READ); + SAW_resp_write : cover (dec_op5 == UMI_RESP_WRITE); + SAW_resp_user0 : cover (dec_op5 == UMI_RESP_USER0); + SAW_resp_user1 : cover (dec_op5 == UMI_RESP_USER1); + SAW_resp_future0 : cover (dec_op5 == UMI_RESP_FUTURE0); + SAW_resp_future1 : cover (dec_op5 == UMI_RESP_FUTURE1); + SAW_full_capacity : cover (dec_bytes_rel == BEAT_BYTES); + if (CHECK_SA_RESERVED != 0) + SAW_sa_checked : cover (dec_has_sa & dec_cmd6_ok); + end + end +`endif + +endmodule + +`default_nettype wire diff --git a/umi/sumi/umi_checker/rtl/umi_handshake_checker.sv b/umi/sumi/umi_checker/rtl/umi_handshake_checker.sv new file mode 100644 index 00000000..fb83728e --- /dev/null +++ b/umi/sumi/umi_checker/rtl/umi_handshake_checker.sv @@ -0,0 +1,230 @@ +/******************************************************************************* + * Copyright 2026 Zero ASIC Corporation + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * + * ---- + * + * Documentation: + * + * Passive protocol checker for the SUMI ready/valid handshake + * (README section 4.2). Attach one instance per SUMI channel; it + * drives nothing and never interferes with the design. + * + * README 4.2 defines six rules. This module enforces the two that are + * runtime obligations of the transmitter, witnesses two more, and + * documents the remaining two, which are structural: + * + * Rule 1 (a transaction occurs when READY and VALID are both + * asserted on a rising clock edge) is a definition. The + * RULE1_* cover properties witness that transactions, + * stalls, and stall-then-complete sequences are all + * reachable, so a formal proof of the other rules can not + * pass vacuously. + * Rule 2 (once VALID is asserted, it must not be de-asserted until + * a transaction completes) -> RULE2_valid_hold. + * Rule 3 (while VALID is asserted, the packet fields CMD, DSTADDR, + * SRCADDR, DATA must remain stable until the transaction + * completes) -> RULE3_cmd_stable / RULE3_dstaddr_stable / + * RULE3_srcaddr_stable / RULE3_data_stable. + * Rule 4 (READY may be de-asserted before a transaction completes) + * is a permission for the receiver, not an obligation: there + * is nothing to assert. The RULE1_stall cover witnesses that + * the surrounding environment actually exercises it. + * Rules 5/6 (VALID must not depend on READY; READY may depend on + * VALID but not combinationally) constrain the DESIGN + * STRUCTURE, not the waveform: a legal trace can be produced + * by an illegal circuit. A cycle-sampled monitor therefore can + * not ASSERT them, so they remain out of scope for this + * bind-in checker. What it does contribute is the c_rule5 + * cover below: a free per-bind reachability witness that VALID + * fires while READY is low (README 4.2 rule 5, README.md:462). + * The COMPLETE method for rule 5 is harness-level, on the DUT + * being proven -- umi/formal/sumi/fv_umi_buffer.sby task + * `rule5` assumes READY stuck low for the whole trace and + * covers VALID asserting anyway, the literal negation of + * "VALID waits for READY". + * + * ASSUME parameter: the same properties can face two directions. + * ASSUME=0 (default): assert the rules. Use on any channel the + * design under test drives (its outputs) -- in simulation + * or formal. + * ASSUME=1: assume the rules. Formal-only: use on free inputs of a + * formal harness so the solver only explores legal + * stimulus. This is the standard assume/guarantee split; + * the same file is both the requirement and the + * environment, so the two can never drift apart. + * + * CHECK_RESET parameter: README 4.2 says nothing about reset. Every + * block in this repository holds VALID low while nreset is asserted, + * and the checker's history must be grounded somewhere, so RESET_ + * valid_low (VALID low during reset) is enforced by default. Set + * CHECK_RESET=0 if a design legitimately asserts VALID during reset. + * + * Implementation notes: + * - Written in the portable synthesizable-plus-assertions subset: + * named immediate assertions inside always blocks, no $past, no + * sequences, no bind, no packages. The same file works under + * yosys/SymbiYosys (read_verilog -formal), Verilator (--assert), + * and slang lint. Cover statements are formal-only (`ifdef FORMAL, + * which SymbiYosys defines automatically). + * - Each assert is paired with an `ifndef FORMAL $error twin: yosys's + * frontend does not parse the assert-else form, and the twin's !== + * comparison also catches X propagating into a rule in 4-state + * simulation, which a plain boolean assert would wave through. + * - History is kept in explicit shadow registers rather than $past + * so the file also runs under simulators without $past support. + ******************************************************************************/ + +`default_nettype none + +module umi_handshake_checker #( + parameter CW = 32, // command width + parameter AW = 64, // address width + parameter DW = 256, // data width + parameter ASSUME = 0, // 0: assert the rules, 1: assume them (formal env) + parameter CHECK_RESET = 1 // 1: also require VALID low during reset +) ( + input wire clk, + input wire nreset, + input wire valid, + input wire ready, + input wire [CW-1:0] cmd, + input wire [AW-1:0] dstaddr, + input wire [AW-1:0] srcaddr, + input wire [DW-1:0] data +); + + // ################################################################# + // # History (shadow registers) + // ################################################################# + + // one full clock has elapsed: nothing can be checked at time zero + reg past_exists; + // last cycle was an incomplete offer: valid, not accepted, not in reset + reg past_stalled; + reg [CW-1:0] past_cmd; + reg [AW-1:0] past_dstaddr; + reg [AW-1:0] past_srcaddr; + reg [DW-1:0] past_data; + + initial begin + past_exists = 1'b0; + past_stalled = 1'b0; + end + + always @(posedge clk) begin + past_exists <= 1'b1; + past_stalled <= nreset & valid & ~ready; + past_cmd <= cmd; + past_dstaddr <= dstaddr; + past_srcaddr <= srcaddr; + past_data <= data; + end + + // ################################################################# + // # The rules (one generate arm per direction) + // ################################################################# + + generate + if (ASSUME == 0) begin : g_assert + + always @(posedge clk) begin + if (past_exists & nreset & past_stalled) begin + RULE2_valid_hold : assert (valid); +`ifndef FORMAL + if ((valid) !== 1'b1) + $error("UMI-HS RULE2 %m: VALID de-asserted before the transaction completed (README 4.2 rule 2)"); +`endif + RULE3_cmd_stable : assert (cmd == past_cmd); +`ifndef FORMAL + if ((cmd == past_cmd) !== 1'b1) + $error("UMI-HS RULE3 %m: CMD changed while VALID was waiting for READY (README 4.2 rule 3)"); +`endif + RULE3_dstaddr_stable : assert (dstaddr == past_dstaddr); +`ifndef FORMAL + if ((dstaddr == past_dstaddr) !== 1'b1) + $error("UMI-HS RULE3 %m: DSTADDR changed while VALID was waiting for READY (README 4.2 rule 3)"); +`endif + RULE3_srcaddr_stable : assert (srcaddr == past_srcaddr); +`ifndef FORMAL + if ((srcaddr == past_srcaddr) !== 1'b1) + $error("UMI-HS RULE3 %m: SRCADDR changed while VALID was waiting for READY (README 4.2 rule 3)"); +`endif + RULE3_data_stable : assert (data == past_data); +`ifndef FORMAL + if ((data == past_data) !== 1'b1) + $error("UMI-HS RULE3 %m: DATA changed while VALID was waiting for READY (README 4.2 rule 3)"); +`endif + end + if (CHECK_RESET != 0) begin + if (past_exists & ~nreset) begin + RESET_valid_low : assert (~valid); +`ifndef FORMAL + if ((~valid) !== 1'b1) + $error("UMI-HS RESET %m: VALID asserted while nreset is active (repo convention, not README 4.2)"); +`endif + end + end + end + + end else begin : g_assume +`ifdef FORMAL + always @(posedge clk) begin + if (past_exists & nreset & past_stalled) begin + RULE2_valid_hold : assume (valid); + RULE3_cmd_stable : assume (cmd == past_cmd); + RULE3_dstaddr_stable : assume (dstaddr == past_dstaddr); + RULE3_srcaddr_stable : assume (srcaddr == past_srcaddr); + RULE3_data_stable : assume (data == past_data); + end + if (CHECK_RESET != 0) begin + if (past_exists & ~nreset) + RESET_valid_low : assume (~valid); + end + end +`endif + end + endgenerate + + // ################################################################# + // # Vacuity witnesses (formal-only) + // ################################################################# + // A handshake proof over an environment that never stalls, or + // never completes a transaction, proves nothing. These covers + // fail loudly (unreached) if the harness is over-constrained. + +`ifdef FORMAL +`ifndef FV_NO_WITNESS + always @(posedge clk) begin + if (past_exists & nreset) begin + RULE1_transaction : cover (valid & ready); + RULE1_stall : cover (valid & ~ready); + RULE1_stall_then_complete : cover (past_stalled & valid & ready); + // README 4.2 rule 5 (README.md:462): VALID must not wait for + // READY. This monitor can not ASSERT that structural rule + // (see header), but every bind gets this free witness that + // VALID does fire while READY is low. The complete proof is + // the harness-level fv_umi_buffer `rule5` task. FV_NO_WITNESS + // drops all covers for the stuck-low-ready harness task, + // where the transaction covers above are unreachable by + // construction. + c_rule5 : cover (valid & ~ready); + end + end +`endif +`endif + +endmodule + +`default_nettype wire diff --git a/umi/sumi/umi_checker/rtl/umi_txn_checker.sv b/umi/sumi/umi_checker/rtl/umi_txn_checker.sv new file mode 100644 index 00000000..0667e632 --- /dev/null +++ b/umi/sumi/umi_checker/rtl/umi_txn_checker.sv @@ -0,0 +1,684 @@ +/******************************************************************************* + * Copyright 2026 Zero ASIC Corporation + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * + * ---- + * + * Documentation: + * + * Passive transaction / framing checker for the SUMI RESPONSE stream + * (README section 3, "Transaction Layer", and section 4.1 "Signal UMI + * / packet splitting"). The checker observes BOTH channels of one + * point-to-point link -- the request channel to learn what responses + * are owed, the response channel to convict every response beat that + * breaks a transaction- or framing-level rule. It drives nothing and + * never interferes with the design; attach it exactly like the + * handshake and command checkers in this directory. + * + * This is the L2 (response-side) partner of umi_cmd_checker (L1, + * per-beat CMD legality). Where umi_cmd_checker judges a single beat in + * isolation, umi_txn_checker judges a beat AGAINST THE REQUEST IT + * ANSWERS and against the framing history of the message it belongs to. + * + * OPERATING CONDITION -- NO INTERLEAVE (read this first). This checker + * assumes a SINGLE, UN-INTERLEAVED response stream: the point-to-point + * link BEFORE any mux/merge, where responses return in the same order + * as the requests that elicited them. It tracks outstanding requests in + * a small in-order shadow FIFO and matches each response beat against + * the queue HEAD. It does NOT fold responses by HOSTID (or by any other + * routing key), so it must NOT be bound downstream of a mux that + * interleaves responses from several devices -- there it would convict + * legal merged traffic (the correct fold key is bridge-dependent -- TL + * carries source in SA[7:0], not HOSTID -- so per-key folding is + * deferred). Bind it on the un-merged link segment. + * + * SCOPE -- RESPONSE-SIDE FRAMING ONLY. Every asserted rule is a property + * of a RESPONSE beat. Request beats are observed (to populate the + * tracker) but their intra-message framing is NOT asserted here: + * request-side framing assertion is future work -- a host emitting + * broken multi-beat requests is not caught by this module. + * + * The rules, with their README (UMI spec) anchors: + * + * TXN_p5_outstanding every response beat has a matching outstanding + * request: the tracker is non-empty (README 3: + * a response answers a request). + * TXN_kind the response OPCODE is the kind the request + * maps to: REQ_RD/REQ_ATOMIC -> RESP_RD, + * REQ_WR -> RESP_WR (README 3.2.3). + * TXN_size / TXN_qos / TXN_prot / TXN_hostid + * the response copies the request's SIZE, QOS, + * PROT and HOSTID fields (README 3.2.3 field + * columns). HOSTID is checked here (not used as a + * fold key -- see NO INTERLEAVE). + * TXN_exok an EXOK (ERR==0b01) response is returned only + * for a request that carried EX (README 3.3.8 + * exclusive-access sequence, 3.3.9 EXOK). + * TXN_da_first the FIRST response beat's DA equals the + * request's SA ("For responses, the DA field + * returned is a copy of the requester SA field", + * README 3.3.1). + * TXN_da_cont a CONTINUATION beat's DA equals the running + * address: prev DA + (2^SIZE)*(LEN+1) of the + * previous beat (README 3.3.3 ADDR_i law, 4.1 + * split example "only DA increments"). Computed + * modulo 2^AW -- the wrap boundary is an open + * question (README 4.1 gives a safe-bit rule + * A[n-1:0]+(2^SIZE)(LEN+1) < 2^n but does not + * define behaviour past the wrap; this checker + * follows modular wrap). + * FRM2_err / FRM2_eof ERR and EOF are stable across the beats of one + * message: a split response does not change its + * error status or frame membership mid-message + * (README 3.3.7 EOF, 3.3.9 ERR). + * TXN_err_len an error response (DEVERR/NETERR) copies the + * TXN_err_first request LEN, is the FIRST beat, is single-beat + * TXN_err_eom (EOM), and carries zero data in the relevant + * TXN_err_zero lanes (README 3.3.9 error semantics; an error + * reply is one terminating beat that echoes the + * request length and returns no data). + * TXN_bytes_le a non-error response never returns more bytes + * than the request asked for: the running total + * got + this-beat-bytes <= expected message bytes + * (README 3.3.2/3.3.3). + * TXN_eom_iff_closed EOM is set on a non-error beat IFF that beat + * closes the message exactly (running total == + * expected) -- EOM neither early nor missing + * (README 3.3.6 EOM, 4.1 "EOM indicates the last + * packet"). + * TXN_msgbytes (FRM-4) the accumulated data bytes of the in-flight + * response message never exceed MAX_MSG_BYTES + * (default 32768 = the spec bound 128 B/word * + * 256 words, README 3.3.2 SIZE, 3.3.3 LEN). + * This is a per-message byte accumulator: a + * single beat's 16-bit (2^SIZE)*(LEN+1) cannot + * exceed 32768, so a per-beat check would be + * vacuous (no counterexample exists). The + * accumulator instead sums the ACTUAL response + * stream across beats and IS falsifiable: a + * responder that returns more bytes than the + * bound trips it. + * TXN_occ_bound the outstanding-request tracker never exceeds + * its capacity CAP: tracker overflow is REPORTED, + * never silent (a bound checker must announce + * when it can no longer track). + * TXN_reconcile an idle link (nothing outstanding) reconciles + * to a fresh framing state (no half-received + * message left dangling) -- an inductive + * invariant that also documents the idle + * contract. + * + * DEFERRED: a bounded-response LIVENESS rule ("the head is answered + * within LIV_MAX cycles") is NOT included. It needs a fairness + * assumption on resp_ready and an age counter whose progress tie is not + * inductive in the portable subset without harness support. Liveness is + * left to a dedicated watchdog. The occupancy bound above is the safety + * half that this checker does make precise. + * + * ASSUME parameter: identical contract to the other checkers in this + * directory. + * ASSUME=0 (default): assert the rules -- attach to the response + * channel a design under test drives (simulation or formal). + * ASSUME=1: assume the rules (formal-only) -- constrain the free + * response channel of a harness to legal response traffic. + * The same file is both requirement and environment, so the + * two can never drift apart. + * + * Parameters: + * CW / AW / DW command / address / data bus widths. + * CAP outstanding-request tracker capacity (the overflow + * report threshold for a_txn_occ_bound). The shadow + * storage is two deep (head e0 + next e1) -- the small + * window a point-to-point link needs; CAP in {1,2} is + * meaningful (CAP=1 models a single-outstanding link; + * a deeper store is future work). Default 2. + * MAX_MSG_BYTES FRM-4 per-message byte ceiling (default 32768, the + * spec maximum). Lower it (e.g. 256) to make the + * accumulator boundary observable at shallow depth. + * ASSUME assert (0) vs assume (1) the rules. + * + * Bind guidance: instantiate one per point-to-point UMI link, wiring + * the request channel to the host->device path and the response channel + * to the device->host path. Bind it BEFORE any response mux (see NO + * INTERLEAVE). Response SRCADDR is undefined by README 3.3.1 and is + * observed-but-never-checked; request DATA is not judged by an L2 + * pairing checker and is likewise waived. + * + * Implementation notes (same portable subset as the other checkers): + * - Field positions and opcode values come from umi_messages.vh, the + * repo's single source of truth. Decode is done through module-local + * `function automatic`s in the name-assignment form (no 'return', no + * 'inside', no packages) so the same file parses under slang, yosys + * (read_verilog -formal), Verilator and Icarus. The only locally + * declared constants are the ERR codes, which umi_messages.vh does + * not define (README 3.3.9). + * - Named immediate assertions inside always blocks; each assert is + * paired with an `ifndef FORMAL $error twin whose !== comparison also + * catches X in 4-state simulation. Cover statements are formal-only + * (`ifdef FORMAL). + * - No $past: the framing history is kept in explicit shadow registers + * grounded in an initial block, so the file runs under simulators + * without $past support and is Verilator -Wall clean. + ******************************************************************************/ + +`default_nettype none + +module umi_txn_checker #( + parameter CW = 32, // command width + parameter AW = 64, // address width + parameter DW = 256, // data width + parameter CAP = 2, // outstanding-tracker report threshold + parameter [31:0] MAX_MSG_BYTES = 32768, // FRM-4 per-message byte ceiling + parameter ASSUME = 0 // 0: assert the rules, 1: assume them +) ( + input wire clk, + input wire nreset, + // request channel (observed to learn what responses are owed) + input wire req_valid, + input wire req_ready, + input wire [CW-1:0] req_cmd, + input wire [AW-1:0] req_dstaddr, + input wire [AW-1:0] req_srcaddr, + input wire [DW-1:0] req_data, + // response channel (checked) + input wire resp_valid, + input wire resp_ready, + input wire [CW-1:0] resp_cmd, + input wire [AW-1:0] resp_dstaddr, + input wire [AW-1:0] resp_srcaddr, + input wire [DW-1:0] resp_data, + // ---- formal observation outputs (tracker / framing shadow state) ---- + // These expose the internal shadow registers so a formal HARNESS can + // write glue lemmas that tie this checker's tracker to a reference + // model (see umi/formal/sumi/fv_umi_txn.sv). They carry NO functional + // obligation: leave them UNCONNECTED in every simulation or formal + // bind, where they are optimized away. Entry packing (LSB first): + // {bytes[15:0], da[AW-1:0], hostid[4:0], ex, prot[1:0], qos[3:0], + // len[7:0], size[2:0], ropc[4:0]} = AW+44 bits. + output wire [1:0] f_occ, + output wire [15:0] f_got, + output wire f_first, + output wire [AW-1:0] f_next_da, + output wire [CW-1:0] f_last_cmd, + output wire [AW+43:0] f_e0, + output wire [AW+43:0] f_e1 +); + + // the shared header declares every UMI constant; a checker uses only + // a subset, so the unused ones are waived + // verilator lint_off UNUSEDPARAM +`include "umi_messages.vh" + // verilator lint_on UNUSEDPARAM + + // ERR codes on the response USER/ERR field (README 3.3.9). These are + // the one set of constants not present in umi_messages.vh; the + // sibling umi_cmd_checker declares them the same way. + localparam [1:0] UMI_ERR_EXOK = 2'd1; + localparam [1:0] UMI_ERR_DEVERR = 2'd2; + localparam [1:0] UMI_ERR_NETERR = 2'd3; + + // request DATA and request DSTADDR (the target of the request, not + // needed to judge a response) are not L2 obligations; response + // SRCADDR is undefined (README 3.3.1) -- observe, but never convict + wire unused_ok = &{1'b1, req_data, req_dstaddr, resp_srcaddr}; + + // ################################################################# + // # Field decode (umi_messages.vh bit positions) -- portable + // # name-assignment functions, callable on req_cmd or resp_cmd. Each + // # function slices its wide CMD argument, so its unused bits are + // # waived (a generic decoder over the whole command word). + // ################################################################# + + // verilator lint_off UNUSEDSIGNAL + function automatic [4:0] f_op5(input [CW-1:0] c); + f_op5 = c[UMI_OPCODE_MSB:UMI_OPCODE_LSB]; endfunction + function automatic [7:0] f_opbyte(input [CW-1:0] c); + f_opbyte = c[7:0]; endfunction + function automatic [2:0] f_size(input [CW-1:0] c); + f_size = c[UMI_SIZE_MSB:UMI_SIZE_LSB]; endfunction + function automatic [7:0] f_len(input [CW-1:0] c); + f_len = c[UMI_LEN_MSB:UMI_LEN_LSB]; endfunction + function automatic [3:0] f_qos(input [CW-1:0] c); + f_qos = c[UMI_QOS_MSB:UMI_QOS_LSB]; endfunction + function automatic [1:0] f_prot(input [CW-1:0] c); + f_prot = c[UMI_PROT_MSB:UMI_PROT_LSB]; endfunction + function automatic f_eom(input [CW-1:0] c); + f_eom = c[UMI_EOM_BIT]; endfunction + function automatic f_eof(input [CW-1:0] c); + f_eof = c[UMI_EOF_BIT]; endfunction + function automatic f_ex(input [CW-1:0] c); + f_ex = c[UMI_EX_BIT]; endfunction + function automatic [1:0] f_user(input [CW-1:0] c); + f_user = c[UMI_USER_MSB:UMI_USER_LSB]; endfunction + function automatic [4:0] f_hostid(input [CW-1:0] c); + f_hostid = c[UMI_HOSTID_MSB:UMI_HOSTID_LSB]; endfunction + + function automatic f_is_req(input [CW-1:0] c); + f_is_req = c[0] & (f_opbyte(c) != UMI_INVALID); endfunction + function automatic f_is_resp(input [CW-1:0] c); + f_is_resp = ~c[0] & (f_opbyte(c) != UMI_INVALID); endfunction + function automatic f_is_link(input [CW-1:0] c); + f_is_link = (f_opbyte(c) == UMI_REQ_LINK) + | (f_opbyte(c) == UMI_RESP_LINK); endfunction + function automatic f_is_fullbyte(input [CW-1:0] c); + f_is_fullbyte = (f_opbyte(c) == UMI_REQ_ERROR) + | (f_opbyte(c) == UMI_REQ_LINK) + | (f_opbyte(c) == UMI_RESP_LINK); endfunction + + // which requests elicit a response, and of which kind (README 3.2.3; + // POSTED/RDMA/ERROR/LINK elicit nothing, USER/FUTURE excluded) + function automatic f_expects_resp(input [CW-1:0] c); + f_expects_resp = f_is_req(c) & ~f_is_fullbyte(c) + & ((f_op5(c) == UMI_REQ_READ) + | (f_op5(c) == UMI_REQ_WRITE) + | (f_op5(c) == UMI_REQ_ATOMIC)); endfunction + function automatic [4:0] f_resp_op5(input [CW-1:0] c); + f_resp_op5 = (f_op5(c) == UMI_REQ_WRITE) + ? UMI_RESP_WRITE[4:0] : UMI_RESP_READ[4:0]; endfunction + + // raw byte count (2^SIZE)*(LEN+1) -- NOT relevance-aware + function automatic [15:0] f_bytes(input [CW-1:0] c); + f_bytes = (16'd1 << f_size(c)) * ({8'd0, f_len(c)} + 16'd1); + endfunction + // does this opcode carry DATA (README 3.2.3 DATA column) + function automatic f_has_data(input [CW-1:0] c); + f_has_data = (f_op5(c) == UMI_REQ_WRITE) + | (f_op5(c) == UMI_REQ_POSTED) + | (f_op5(c) == UMI_REQ_ATOMIC) + | (f_op5(c) == UMI_REQ_USER0) + | (f_op5(c) == UMI_REQ_FUTURE0) + | (f_op5(c) == UMI_RESP_READ) + | (f_op5(c) == UMI_RESP_USER1) + | (f_op5(c) == UMI_RESP_FUTURE1); endfunction + // relevance-aware byte count: none if no data; 2^SIZE for atomics + // (LEN aliases ATYPE); else (2^SIZE)*(LEN+1) + function automatic [15:0] f_bytes_rel(input [CW-1:0] c); + f_bytes_rel = ~f_has_data(c) ? 16'd0 + : (f_op5(c) == UMI_REQ_ATOMIC) ? (16'd1 << f_size(c)) + : f_bytes(c); endfunction + // verilator lint_on UNUSEDSIGNAL + + // ################################################################# + // # Beat / pairing events + // ################################################################# + + wire req_beat = req_valid & req_ready; + // enqueue a response obligation at the request's EOM beat (the whole + // request message maps to one response message) + wire req_qual = req_beat & f_expects_resp(req_cmd); + wire push = req_qual & f_eom(req_cmd); + + // NO INTERLEAVE: every response beat matches the queue head -- no + // HOSTID (or other key) filtering + wire resp_beat = resp_valid & resp_ready; + wire resp_hit = resp_beat & f_is_resp(resp_cmd) & ~f_is_link(resp_cmd); + wire resp_err = (f_user(resp_cmd) == UMI_ERR_DEVERR) + | (f_user(resp_cmd) == UMI_ERR_NETERR); + wire pop = resp_hit & f_eom(resp_cmd); + wire [15:0] rbytes = f_bytes_rel(resp_cmd); + + // expected response bytes for the request being enqueued: WR acks + // carry none; atomics return 2^SIZE (LEN is ATYPE); reads return the + // full (2^SIZE)*(LEN+1) + wire [15:0] push_bytes = + (f_op5(req_cmd) == UMI_REQ_WRITE) ? 16'd0 + : (f_op5(req_cmd) == UMI_REQ_ATOMIC) ? (16'd1 << f_size(req_cmd)) + : f_bytes(req_cmd); + + // ################################################################# + // # Outstanding-request tracker: in-order shadow FIFO (head e0, + // # next e1). occ is the count; CAP is the report threshold. + // ################################################################# + + reg [1:0] occ; + reg [4:0] e0_ropc, e1_ropc; + reg [2:0] e0_size, e1_size; + reg [7:0] e0_len, e1_len; + reg [3:0] e0_qos, e1_qos; + reg [1:0] e0_prot, e1_prot; + reg e0_ex, e1_ex; + reg [4:0] e0_hostid, e1_hostid; + reg [AW-1:0] e0_da, e1_da; + reg [15:0] e0_bytes, e1_bytes; + + reg [15:0] got; // data bytes received for the head message so far + reg first; // next response beat is the head's first beat + reg [AW-1:0] next_da; // running continuation address (DA law) + reg [CW-1:0] last_cmd; // previous response beat's cmd (FRM-2, no $past) + + initial begin + occ = 2'd0; + got = 16'd0; + first = 1'b1; + next_da = {AW{1'b0}}; + last_cmd = {CW{1'b0}}; + end + + always @(posedge clk) begin + if (!nreset) begin + occ <= 2'd0; + got <= 16'd0; + first <= 1'b1; + end else begin + // ---- queue update (head-shift register, depth 2) ---- + case ({push, pop}) + 2'b10: begin // push only + if (occ == 2'd0) begin + e0_ropc <= f_resp_op5(req_cmd); + e0_size <= f_size(req_cmd); + e0_len <= f_len(req_cmd); + e0_qos <= f_qos(req_cmd); + e0_prot <= f_prot(req_cmd); + e0_ex <= f_ex(req_cmd); + e0_hostid <= f_hostid(req_cmd); + e0_da <= req_srcaddr; + e0_bytes <= push_bytes; + end else begin + e1_ropc <= f_resp_op5(req_cmd); + e1_size <= f_size(req_cmd); + e1_len <= f_len(req_cmd); + e1_qos <= f_qos(req_cmd); + e1_prot <= f_prot(req_cmd); + e1_ex <= f_ex(req_cmd); + e1_hostid <= f_hostid(req_cmd); + e1_da <= req_srcaddr; + e1_bytes <= push_bytes; + end + occ <= occ + 2'd1; + end + 2'b01: begin // pop only + e0_ropc <= e1_ropc; + e0_size <= e1_size; + e0_len <= e1_len; + e0_qos <= e1_qos; + e0_prot <= e1_prot; + e0_ex <= e1_ex; + e0_hostid <= e1_hostid; + e0_da <= e1_da; + e0_bytes <= e1_bytes; + occ <= occ - 2'd1; + end + 2'b11: begin // push + pop + if (occ == 2'd1) begin + e0_ropc <= f_resp_op5(req_cmd); + e0_size <= f_size(req_cmd); + e0_len <= f_len(req_cmd); + e0_qos <= f_qos(req_cmd); + e0_prot <= f_prot(req_cmd); + e0_ex <= f_ex(req_cmd); + e0_hostid <= f_hostid(req_cmd); + e0_da <= req_srcaddr; + e0_bytes <= push_bytes; + end else begin + e0_ropc <= e1_ropc; + e0_size <= e1_size; + e0_len <= e1_len; + e0_qos <= e1_qos; + e0_prot <= e1_prot; + e0_ex <= e1_ex; + e0_hostid <= e1_hostid; + e0_da <= e1_da; + e0_bytes <= e1_bytes; + e1_ropc <= f_resp_op5(req_cmd); + e1_size <= f_size(req_cmd); + e1_len <= f_len(req_cmd); + e1_qos <= f_qos(req_cmd); + e1_prot <= f_prot(req_cmd); + e1_ex <= f_ex(req_cmd); + e1_hostid <= f_hostid(req_cmd); + e1_da <= req_srcaddr; + e1_bytes <= push_bytes; + end + end + default: ; // idle + endcase + + // ---- framing progress on the response head ---- + if (resp_hit) begin + last_cmd <= resp_cmd; + if (f_eom(resp_cmd)) begin + got <= 16'd0; // message closed + first <= 1'b1; + end else begin + got <= got + rbytes; // FRM-4 accumulate + first <= 1'b0; + // continuation address: prev DA + prev-beat bytes, + // modulo 2^AW (wrap boundary undefined by the spec) + next_da <= resp_dstaddr + + {{(AW-16){1'b0}}, f_bytes(resp_cmd)}; + end + end + end + end + + // ################################################################# + // # Error-branch DATA==0 lane check (rel-masked over the beat) + // ################################################################# + + integer li; + reg lanes_zero; + always @(*) begin + lanes_zero = 1'b1; + for (li = 0; li < DW/8; li = li + 1) + if ({16'd0, li[15:0]} < {16'd0, rbytes} + && resp_data[8*li +: 8] != 8'd0) + lanes_zero = 1'b0; + end + + // running / next byte totals for the head message + wire [31:0] tot_bytes = {16'd0, got} + {16'd0, rbytes}; + + // formal observation taps (see port comment) + assign f_occ = occ; + assign f_got = got; + assign f_first = first; + assign f_next_da = next_da; + assign f_last_cmd = last_cmd; + assign f_e0 = {e0_bytes, e0_da, e0_hostid, e0_ex, e0_prot, e0_qos, + e0_len, e0_size, e0_ropc}; + assign f_e1 = {e1_bytes, e1_da, e1_hostid, e1_ex, e1_prot, e1_qos, + e1_len, e1_size, e1_ropc}; + + // ################################################################# + // # The rules (one generate arm per direction) + // ################################################################# + + generate + if (ASSUME == 0) begin : g_assert + + always @(posedge clk) begin + if (nreset) begin + if (resp_hit) begin + TXN_p5_outstanding : assert (occ != 2'd0); +`ifndef FORMAL + if ((occ != 2'd0) !== 1'b1) + $error("UMI-TXN p5 %m: response beat with nothing outstanding (README 3: a response answers a request)"); +`endif + TXN_kind : assert (f_op5(resp_cmd) == e0_ropc); +`ifndef FORMAL + if ((f_op5(resp_cmd) == e0_ropc) !== 1'b1) + $error("UMI-TXN kind %m: response OPCODE does not match the request's response kind (README 3.2.3)"); +`endif + TXN_size : assert (f_size(resp_cmd) == e0_size); +`ifndef FORMAL + if ((f_size(resp_cmd) == e0_size) !== 1'b1) + $error("UMI-TXN size %m: response SIZE != request SIZE (README 3.2.3)"); +`endif + TXN_qos : assert (f_qos(resp_cmd) == e0_qos); +`ifndef FORMAL + if ((f_qos(resp_cmd) == e0_qos) !== 1'b1) + $error("UMI-TXN qos %m: response QOS != request QOS (README 3.2.3)"); +`endif + TXN_prot : assert (f_prot(resp_cmd) == e0_prot); +`ifndef FORMAL + if ((f_prot(resp_cmd) == e0_prot) !== 1'b1) + $error("UMI-TXN prot %m: response PROT != request PROT (README 3.2.3)"); +`endif + TXN_hostid : assert (f_hostid(resp_cmd) == e0_hostid); +`ifndef FORMAL + if ((f_hostid(resp_cmd) == e0_hostid) !== 1'b1) + $error("UMI-TXN hostid %m: response HOSTID != request HOSTID (README 3.2.3)"); +`endif + TXN_exok : assert ((f_user(resp_cmd) != UMI_ERR_EXOK) || e0_ex); +`ifndef FORMAL + if (((f_user(resp_cmd) != UMI_ERR_EXOK) || e0_ex) !== 1'b1) + $error("UMI-TXN exok %m: EXOK response to a non-exclusive request (README 3.3.8/3.3.9)"); +`endif + if (first) begin + TXN_da_first : assert (resp_dstaddr == e0_da); +`ifndef FORMAL + if ((resp_dstaddr == e0_da) !== 1'b1) + $error("UMI-TXN da_first %m: first response DA != request SA (README 3.3.1)"); +`endif + end else begin + TXN_da_cont : assert (resp_dstaddr == next_da); +`ifndef FORMAL + if ((resp_dstaddr == next_da) !== 1'b1) + $error("UMI-TXN da_cont %m: split-response DA breaks the continuation law (README 3.3.3/4.1)"); +`endif + TXN_frm2_err : assert (f_user(resp_cmd) == f_user(last_cmd)); +`ifndef FORMAL + if ((f_user(resp_cmd) == f_user(last_cmd)) !== 1'b1) + $error("UMI-TXN frm2 %m: ERR changed mid-message (README 3.3.9)"); +`endif + TXN_frm2_eof : assert (f_eof(resp_cmd) == f_eof(last_cmd)); +`ifndef FORMAL + if ((f_eof(resp_cmd) == f_eof(last_cmd)) !== 1'b1) + $error("UMI-TXN frm2 %m: EOF changed mid-message (README 3.3.7)"); +`endif + end + if (resp_err) begin + TXN_err_len : assert (f_len(resp_cmd) == e0_len); +`ifndef FORMAL + if ((f_len(resp_cmd) == e0_len) !== 1'b1) + $error("UMI-TXN err_len %m: error response LEN != request LEN (README 3.3.9)"); +`endif + TXN_err_first : assert (first); +`ifndef FORMAL + if ((first) !== 1'b1) + $error("UMI-TXN err_first %m: error response beat mid-message (README 3.3.9)"); +`endif + TXN_err_eom : assert (f_eom(resp_cmd)); +`ifndef FORMAL + if ((f_eom(resp_cmd)) !== 1'b1) + $error("UMI-TXN err_eom %m: error response not single-beat (README 3.3.9)"); +`endif + TXN_err_zero : assert (lanes_zero); +`ifndef FORMAL + if ((lanes_zero) !== 1'b1) + $error("UMI-TXN err_zero %m: DEVERR/NETERR response carries nonzero data (README 3.3.9)"); +`endif + end else begin + TXN_bytes_le : assert (tot_bytes[15:0] <= e0_bytes + && tot_bytes[31:16] == 16'd0); +`ifndef FORMAL + if ((tot_bytes <= {16'd0, e0_bytes}) !== 1'b1) + $error("UMI-TXN bytes_le %m: response over-returns bytes (README 3.3.2/3.3.3)"); +`endif + TXN_eom_iff_closed : assert (f_eom(resp_cmd) + == (tot_bytes == {16'd0, e0_bytes})); +`ifndef FORMAL + if ((f_eom(resp_cmd) == (tot_bytes == {16'd0, e0_bytes})) !== 1'b1) + $error("UMI-TXN eom_iff_closed %m: EOM not exactly on the closing beat (README 3.3.6/4.1)"); +`endif + // FRM-4: real per-message byte accumulator + // (a per-beat check would be vacuous) + TXN_msgbytes : assert (tot_bytes <= MAX_MSG_BYTES); +`ifndef FORMAL + if ((tot_bytes <= MAX_MSG_BYTES) !== 1'b1) + $error("UMI-TXN msgbytes %m: message byte total exceeds MAX_MSG_BYTES (FRM-4, README 3.3.2/3.3.3)"); +`endif + end + end + TXN_occ_bound : assert (occ <= CAP); +`ifndef FORMAL + if ((occ <= CAP) !== 1'b1) + $error("UMI-TXN occ_bound %m: outstanding-request tracker overflow (> CAP)"); +`endif + TXN_reconcile : assert ((occ != 2'd0) || (got == 16'd0 && first)); +`ifndef FORMAL + if (((occ != 2'd0) || (got == 16'd0 && first)) !== 1'b1) + $error("UMI-TXN reconcile %m: idle link left a dangling half-message"); +`endif + end + end + + end else begin : g_assume +`ifdef FORMAL + always @(posedge clk) begin + if (nreset) begin + if (resp_hit) begin + TXN_p5_outstanding : assume (occ != 2'd0); + TXN_kind : assume (f_op5(resp_cmd) == e0_ropc); + TXN_size : assume (f_size(resp_cmd) == e0_size); + TXN_qos : assume (f_qos(resp_cmd) == e0_qos); + TXN_prot : assume (f_prot(resp_cmd) == e0_prot); + TXN_hostid : assume (f_hostid(resp_cmd) == e0_hostid); + TXN_exok : assume ((f_user(resp_cmd) != UMI_ERR_EXOK) || e0_ex); + if (first) begin + TXN_da_first : assume (resp_dstaddr == e0_da); + end else begin + TXN_da_cont : assume (resp_dstaddr == next_da); + TXN_frm2_err : assume (f_user(resp_cmd) == f_user(last_cmd)); + TXN_frm2_eof : assume (f_eof(resp_cmd) == f_eof(last_cmd)); + end + if (resp_err) begin + TXN_err_len : assume (f_len(resp_cmd) == e0_len); + TXN_err_first : assume (first); + TXN_err_eom : assume (f_eom(resp_cmd)); + TXN_err_zero : assume (lanes_zero); + end else begin + TXN_bytes_le : assume (tot_bytes <= {16'd0, e0_bytes}); + TXN_eom_iff_closed : assume (f_eom(resp_cmd) + == (tot_bytes == {16'd0, e0_bytes})); + TXN_msgbytes : assume (tot_bytes <= MAX_MSG_BYTES); + end + end + TXN_occ_bound : assume (occ <= CAP); + TXN_reconcile : assume ((occ != 2'd0) || (got == 16'd0 && first)); + end + end +`endif + end + endgenerate + + // ################################################################# + // # Vacuity witnesses (formal-only) + // ################################################################# + // A transaction proof over an environment that never completes a + // message, never splits one, never returns an error, or never fills + // the tracker proves little. These covers fail loudly (unreached) if + // a harness or a bind over-constrains the channels. + +`ifdef FORMAL + always @(posedge clk) begin + if (nreset) begin + SAW_complete : cover (pop); + SAW_split : cover (resp_hit & ~f_eom(resp_cmd)); + SAW_journey : cover (pop & ~first); // multi-beat msg closes + SAW_err : cover (resp_hit & resp_err); + SAW_full : cover (occ == CAP); +`ifdef FORMAL_MSGBYTES_BOUNDARY + // FRM-4 accumulator reaches EXACTLY the ceiling (run with a + // small chparam MAX_MSG_BYTES so the boundary is shallow) + SAW_msgbytes_boundary : + cover (resp_hit & ~resp_err & (tot_bytes == MAX_MSG_BYTES)); +`endif + end + end +`endif + +endmodule + +`default_nettype wire diff --git a/umi/sumi/umi_checker/testbench/tb_umi_cmd_checker.sv b/umi/sumi/umi_checker/testbench/tb_umi_cmd_checker.sv new file mode 100644 index 00000000..107fb1ab --- /dev/null +++ b/umi/sumi/umi_checker/testbench/tb_umi_cmd_checker.sv @@ -0,0 +1,171 @@ +/******************************************************************************* + * Self-test for umi_cmd_checker in SIMULATION (no formal tools). + * + * The testbench drives one SUMI channel directly -- the checker is a + * passive observer, so no DUT is needed to demonstrate it. Two runs: + * + * clean (default) : legal beats -- write, read, read-response with + * data, atomic, RESP_LINK, REQ_ERROR -- each with + * legal alignment and capacity. + * Expect: "TB PASS", exit 0, no UMI-CMD text. + * +inject : one beat with the reserved opcode 0x19 (a CMD-1 + * violation). + * Expect: one UMI-CMD CMD-1 error, nonzero exit. + * + * The verdict is self-checking: the tb reads the checker's per-rule + * dec_*_ok verdict wires hierarchically and compares them against its + * own expectation for every beat; any mismatch prints "TB FAIL" and + * ends in $fatal. Exit codes gate pass/fail, but the exit code alone + * cannot distinguish a working checker from a broken one: an inject + * run whose checker missed the beat also exits nonzero, through the + * $fatal mismatch path. The grader must check the output text -- a + * working inject run prints the UMI-CMD $error line and no "TB FAIL" + * line; a missed detection prints "TB FAIL" before the nonzero exit. + * + * Run (Icarus, from this directory): + * iverilog -g2012 -I ../../include -o tb_umi_cmd_checker.vvp \ + * tb_umi_cmd_checker.sv ../rtl/umi_cmd_checker.sv + * vvp tb_umi_cmd_checker.vvp # expect: TB PASS, exit 0 + * vvp tb_umi_cmd_checker.vvp +inject # expect: CMD-1 error, exit 1 + ******************************************************************************/ + +`timescale 1ns / 1ps +`default_nettype none + +module tb_umi_cmd_checker; + + localparam CW = 32; + localparam AW = 64; + localparam DW = 64; + + reg clk = 1'b0; + reg nreset = 1'b0; + reg valid = 1'b0; + reg ready = 1'b0; + reg [CW-1:0] cmd = '0; + reg [AW-1:0] dstaddr = '0; + reg [AW-1:0] srcaddr = '0; + reg [DW-1:0] data = '0; + + reg inject = 1'b0; + integer tb_errors = 0; + + always #5 clk = ~clk; + + umi_cmd_checker #( + .CW (CW), .AW (AW), .DW (DW) + ) chk ( + .clk (clk), + .nreset (nreset), + .valid (valid), + .ready (ready), + .cmd (cmd), + .dstaddr (dstaddr), + .srcaddr (srcaddr), + .data (data) + ); + + // the checker's own per-rule verdicts, observed hierarchically + // (CMD6 is parameter-gated off in this instance and not sampled) + wire beat_ok = chk.dec_cmd1_ok & chk.dec_cmd2_ok + & chk.dec_cmd4a_ok & chk.dec_cmd4b_ok + & chk.dec_cmd10_ok & chk.dec_cmd11_ok + & chk.dec_cmd12_ok & chk.dec_cmd15_ok + & chk.dec_cmd16_ok; + + // drive one beat and require the checker's verdict to match + task drive_beat(input [CW-1:0] t_cmd, + input [AW-1:0] t_da, + input [AW-1:0] t_sa, + input [DW-1:0] t_data, + input t_legal); + begin + valid = 1'b1; + ready = 1'b1; + cmd = t_cmd; + dstaddr = t_da; + srcaddr = t_sa; + data = t_data; + @(negedge clk); // the posedge in between samples the beat + if (beat_ok !== t_legal) begin + tb_errors = tb_errors + 1; + $display("TB FAIL: cmd=%h expected %s, checker says %s", + t_cmd, t_legal ? "legal" : "ILLEGAL", + (beat_ok === 1'b1) ? "legal" : "ILLEGAL"); + end + end + endtask + + initial begin + if ($test$plusargs("inject")) + inject = 1'b1; + + // reset: no beats offered, nothing may fire + repeat (2) @(negedge clk); + nreset = 1'b1; + @(negedge clk); + + // REQ_WR SIZE=2 LEN=1 (8 bytes: exactly one DW=64 beat), EOM + drive_beat(32'h0040_0143, + 64'h0000_0000_1000_0100, + 64'h0000_0010_0000_1004, + 64'hDEAD_BEEF_CAFE_F00D, 1'b1); + + // REQ_RD SIZE=1 LEN=0 (no data relevance on a read request) + drive_beat(32'h0000_0021, + 64'h0000_0000_1000_0002, + 64'h0000_0010_0000_1006, + 64'h0, 1'b1); + + // RESP_RD SIZE=3 LEN=0 with ERR=OK carrying data (SA is + // undefined on responses -- deliberately unaligned here) + drive_beat(32'h0000_0062, + 64'h0000_0000_1000_0108, + 64'hFFFF_FFFF_FFFF_FFFF, + 64'h0123_4567_89AB_CDEF, 1'b1); + + // REQ_ATOMIC ADD SIZE=2 (ATYPE rides the LEN field) + drive_beat(32'h0000_0049, + 64'h0000_0000_1000_0200, + 64'h0000_0010_0000_1008, + 64'h0000_0000_0000_0001, 1'b1); + + // RESP_LINK: CMD-only, no DA/SA/DATA obligations + drive_beat(32'h0000_000E, + 64'hAAAA_AAAA_AAAA_AAAA, + 64'h5555_5555_5555_5555, + 64'h0, 1'b1); + + // REQ_ERROR: full-byte special, SIZE field 0 by encoding + drive_beat(32'h0000_000F, + 64'h0000_0000_1000_0300, + 64'h0000_0010_0000_100C, + 64'h0, 1'b1); + + // the injected violation: reserved opcode hole 0x19 + if (inject) + drive_beat(32'h0000_0019, + 64'h0000_0000_1000_0400, + 64'h0000_0010_0000_1010, + 64'h0, 1'b0); + + // idle down + valid = 1'b0; + ready = 1'b0; + repeat (2) @(negedge clk); + + if (tb_errors != 0) begin + $display("TB FAIL: %0d mismatch(es) between tb and checker", tb_errors); + $fatal(0, "tb/checker mismatch"); + end + if (!inject) begin + $display("TB PASS: legal sequence, checker silent"); + $finish; + end + $display("TB DONE: inject run complete (the UMI-CMD CMD-1 error above is the expected result)"); + $fatal(0, "expected-violation run: nonzero exit by design"); + end + +endmodule + +`default_nettype wire diff --git a/umi/sumi/umi_checker/testbench/tb_umi_handshake_checker.sv b/umi/sumi/umi_checker/testbench/tb_umi_handshake_checker.sv new file mode 100644 index 00000000..e58dd466 --- /dev/null +++ b/umi/sumi/umi_checker/testbench/tb_umi_handshake_checker.sv @@ -0,0 +1,101 @@ +/******************************************************************************* + * Self-test for umi_handshake_checker in SIMULATION (no formal tools). + * + * The testbench drives one SUMI channel directly -- the checker is a + * passive observer, so no DUT is needed to demonstrate it. Two runs: + * + * clean (default) : a legal sequence -- reset, a stalled offer held + * stable, completion, a back-to-back beat. + * Expect: "TB PASS", exit 0. + * +inject : same sequence, but CMD is changed in the middle + * of the stall (a rule 3 violation). + * Expect: one UMI-HS RULE3 error, nonzero exit. + * + * Run (Verilator): + * verilator --binary --assert --timing -o tb tb_umi_handshake_checker.sv \ + * ../rtl/umi_handshake_checker.sv && ./obj_dir/tb + * ./obj_dir/tb +inject # must report the RULE3 violation + ******************************************************************************/ + +`timescale 1ns / 1ps +`default_nettype none + +module tb_umi_handshake_checker; + + localparam CW = 32; + localparam AW = 64; + localparam DW = 64; + + reg clk = 1'b0; + reg nreset = 1'b0; + reg valid = 1'b0; + reg ready = 1'b0; + reg [CW-1:0] cmd = '0; + reg [AW-1:0] dstaddr = '0; + reg [AW-1:0] srcaddr = '0; + reg [DW-1:0] data = '0; + + reg inject = 1'b0; + + always #5 clk = ~clk; + + umi_handshake_checker #( + .CW (CW), .AW (AW), .DW (DW) + ) chk ( + .clk (clk), + .nreset (nreset), + .valid (valid), + .ready (ready), + .cmd (cmd), + .dstaddr (dstaddr), + .srcaddr (srcaddr), + .data (data) + ); + + initial begin + if ($test$plusargs("inject")) + inject = 1'b1; + + // reset (checker: VALID must stay low here) + repeat (2) @(negedge clk); + nreset = 1'b1; + @(negedge clk); + + // offer a beat into backpressure: hold everything (rules 2+3) + valid = 1'b1; + cmd = 32'h0000_0621; // an arbitrary, held command + dstaddr = 64'h0000_0000_1234_5678; + srcaddr = 64'h0000_1100_0000_0000; + data = 64'hDEAD_BEEF_CAFE_F00D; + ready = 1'b0; + @(negedge clk); + + // mid-stall: the injected violation changes CMD while waiting + if (inject) + cmd = 32'h0000_0721; + @(negedge clk); + + // the receiver wakes up; the transaction completes (rule 1) + ready = 1'b1; + @(negedge clk); + + // back-to-back second beat, accepted immediately + cmd = 32'h0000_0631; + data = 64'h0123_4567_89AB_CDEF; + @(negedge clk); + + // idle down + valid = 1'b0; + ready = 1'b0; + repeat (2) @(negedge clk); + + if (!inject) + $display("TB PASS: legal sequence, checker silent"); + else + $display("TB DONE: inject run complete (a RULE3 error above is the expected result)"); + $finish; + end + +endmodule + +`default_nettype wire diff --git a/umi/sumi/umi_checker/testbench/tb_umi_txn_checker.sv b/umi/sumi/umi_checker/testbench/tb_umi_txn_checker.sv new file mode 100644 index 00000000..3607927e --- /dev/null +++ b/umi/sumi/umi_checker/testbench/tb_umi_txn_checker.sv @@ -0,0 +1,222 @@ +/******************************************************************************* + * Self-test for umi_txn_checker in SIMULATION (no formal tools). + * + * The testbench drives BOTH channels of one point-to-point SUMI link -- + * the checker is a passive observer of a request/response pair, so no DUT + * is needed to demonstrate it. It plays one whole transaction: a + * multi-word READ request, then that request's framed multi-beat response + * split word-per-beat with EOM only on the closing beat. Two runs: + * + * clean (default) : REQ_RD (SIZE=3, LEN=1 -> 16 bytes, EOM) followed by + * a two-beat RESP_RD: beat1 (first, 8 bytes, EOM=0, + * DA = request SA) then beat2 (continuation, 8 bytes, + * EOM=1, DA = request SA + 8 = the continuation law). + * Expect: "TB PASS", exit 0, no UMI-TXN text. + * +inject : the same transaction, but the CONTINUATION beat's + * DSTADDR is corrupted (breaks the ADDR_i running + * address law -- a TXN_da_cont violation). + * Expect: one UMI-TXN da_cont error, nonzero exit. + * + * The verdict is self-checking: for every response beat the tb + * reconstructs the checker's OWN address verdict from the checker's + * exposed shadow state (f_first selects the reference -- the first beat + * checks DA == request SA held in f_e0's DA field, a continuation checks + * DA == f_next_da, the running address) and compares it against the tb's + * independent legal/illegal expectation for that beat. Any mismatch + * prints "TB FAIL" and ends in $fatal. + * + * Exit codes gate pass/fail, but the exit code alone cannot distinguish a + * working checker from a broken one: an inject run whose checker missed + * the beat also exits nonzero, through the $fatal mismatch path. The + * grader must ALSO check the output text -- a working inject run prints + * the UMI-TXN da_cont $error line and no "TB FAIL" line; a missed + * detection prints "TB FAIL" before the nonzero exit. + * + * Run (Icarus, from this directory): + * iverilog -g2012 -I ../../include -o tb_umi_txn_checker.vvp \ + * tb_umi_txn_checker.sv ../rtl/umi_txn_checker.sv + * vvp tb_umi_txn_checker.vvp # expect: TB PASS, exit 0 + * vvp tb_umi_txn_checker.vvp +inject # expect: da_cont error, exit 1 + ******************************************************************************/ + +`timescale 1ns / 1ps +`default_nettype none + +module tb_umi_txn_checker; + + localparam CW = 32; + localparam AW = 64; + localparam DW = 64; // 8 bytes/beat: SIZE=3 gives exactly one word/beat + + reg clk = 1'b0; + reg nreset = 1'b0; + + // request channel (observed to learn what responses are owed) + reg req_valid = 1'b0; + reg req_ready = 1'b0; + reg [CW-1:0] req_cmd = '0; + reg [AW-1:0] req_dstaddr = '0; + reg [AW-1:0] req_srcaddr = '0; + reg [DW-1:0] req_data = '0; + + // response channel (checked) + reg resp_valid = 1'b0; + reg resp_ready = 1'b0; + reg [CW-1:0] resp_cmd = '0; + reg [AW-1:0] resp_dstaddr = '0; + reg [AW-1:0] resp_srcaddr = '0; + reg [DW-1:0] resp_data = '0; + + reg inject = 1'b0; + integer tb_errors = 0; + + always #5 clk = ~clk; + + umi_txn_checker #( + .CW (CW), .AW (AW), .DW (DW) + ) chk ( + .clk (clk), + .nreset (nreset), + .req_valid (req_valid), + .req_ready (req_ready), + .req_cmd (req_cmd), + .req_dstaddr (req_dstaddr), + .req_srcaddr (req_srcaddr), + .req_data (req_data), + .resp_valid (resp_valid), + .resp_ready (resp_ready), + .resp_cmd (resp_cmd), + .resp_dstaddr (resp_dstaddr), + .resp_srcaddr (resp_srcaddr), + .resp_data (resp_data), + // formal observation taps -- read here to reconstruct verdicts + .f_occ (), + .f_got (), + .f_first (), + .f_next_da (), + .f_last_cmd (), + .f_e0 (), + .f_e1 () + ); + + // the checker's OWN shadow state, observed hierarchically. The DA law + // reference for a response beat is e0_da (packed in f_e0's DA field) + // on the first beat, or f_next_da (running address) on a continuation. + wire [AW-1:0] tap_e0_da = chk.f_e0[AW+27:28]; + wire [AW-1:0] tap_next_da = chk.f_next_da; + wire tap_first = chk.f_first; + + // drive one request beat (host->device); pushes a response obligation + task drive_req(input [CW-1:0] t_cmd, + input [AW-1:0] t_da, + input [AW-1:0] t_sa, + input [DW-1:0] t_data); + begin + // entered at a negedge + req_valid = 1'b1; + req_ready = 1'b1; + req_cmd = t_cmd; + req_dstaddr = t_da; + req_srcaddr = t_sa; + req_data = t_data; + resp_valid = 1'b0; + resp_ready = 1'b0; + @(posedge clk); // the request is sampled / enqueued here + @(negedge clk); + req_valid = 1'b0; + req_ready = 1'b0; + end + endtask + + // drive one response beat (device->host) and require the checker's own + // address verdict to match the tb's expectation for this beat + task drive_resp(input [CW-1:0] t_cmd, + input [AW-1:0] t_da, + input [AW-1:0] t_sa, + input [DW-1:0] t_data, + input t_legal); + reg [AW-1:0] ref_da; + reg beat_ok; + begin + // entered at a negedge: the checker's shadow registers still + // hold the values its NEXT posedge assertion will read + resp_valid = 1'b1; + resp_ready = 1'b1; + resp_cmd = t_cmd; + resp_dstaddr = t_da; + resp_srcaddr = t_sa; + resp_data = t_data; + req_valid = 1'b0; + req_ready = 1'b0; + // reconstruct exactly what the checker's DA rule will decide + ref_da = tap_first ? tap_e0_da : tap_next_da; + beat_ok = (t_da === ref_da); + if (beat_ok !== t_legal) begin + tb_errors = tb_errors + 1; + $display("TB FAIL: response DA verdict mismatch: da=%h ref=%h (%s beat) checker says %s, expected %s", + t_da, ref_da, tap_first ? "first" : "cont", + beat_ok ? "legal" : "ILLEGAL", + t_legal ? "legal" : "ILLEGAL"); + end + @(posedge clk); // checker samples the beat and asserts + @(negedge clk); + resp_valid = 1'b0; + resp_ready = 1'b0; + end + endtask + + initial begin + if ($test$plusargs("inject")) + inject = 1'b1; + + // reset: no beats offered, nothing may fire + repeat (2) @(negedge clk); + nreset = 1'b1; + @(negedge clk); + + // REQ_RD SIZE=3 (8 B/word), LEN=1 (2 words = 16 B), EOM. The + // request SA (0x1000) is the DA the first response beat must copy + // (README 3.3.1). DA/DATA of a request are not L2 obligations. + drive_req(32'h0040_0161, + 64'h0000_0000_2000_0000, + 64'h0000_0000_0000_1000, + 64'h0); + + // RESP_RD beat 1 (FIRST): SIZE=3 LEN=0 (8 B), EOM=0 (message not + // yet closed), DA = request SA = 0x1000. + drive_resp(32'h0000_0062, + 64'h0000_0000_0000_1000, + 64'hFFFF_FFFF_FFFF_FFFF, // response SA undefined (waived) + 64'h0123_4567_89AB_CDEF, 1'b1); + + // RESP_RD beat 2 (CONTINUATION, closes): SIZE=3 LEN=0 (8 B), + // EOM=1, DA = 0x1000 + 8 = 0x1008 (the ADDR_i continuation law). + // +inject corrupts this DA, breaking the continuation address. + drive_resp(32'h0040_0062, + inject ? 64'hDEAD_BEEF_0000_0000 : 64'h0000_0000_0000_1008, + 64'hFFFF_FFFF_FFFF_FFFF, + 64'hFEDC_BA98_7654_3210, + inject ? 1'b0 : 1'b1); + + // idle down + req_valid = 1'b0; + req_ready = 1'b0; + resp_valid = 1'b0; + resp_ready = 1'b0; + repeat (2) @(negedge clk); + + if (tb_errors != 0) begin + $display("TB FAIL: %0d verdict mismatch(es) between tb and checker", tb_errors); + $fatal(0, "tb/checker mismatch"); + end + if (!inject) begin + $display("TB PASS: legal request/response transaction, checker silent"); + $finish; + end + $display("TB DONE: inject run complete (the UMI-TXN da_cont error above is the expected result)"); + $fatal(0, "expected-violation run: nonzero exit by design"); + end + +endmodule + +`default_nettype wire diff --git a/umi/sumi/umi_checker/umi_checker.py b/umi/sumi/umi_checker/umi_checker.py new file mode 100644 index 00000000..1be7cb07 --- /dev/null +++ b/umi/sumi/umi_checker/umi_checker.py @@ -0,0 +1,28 @@ +from umi.common import UMI + + +class Checker(UMI): + """The UMI verification IP: passive protocol checkers. + + One block, one fileset, growing by files -- never by folders: + rtl/umi_handshake_checker.sv README 4.2 ready/valid handshake + rtl/umi_cmd_checker.sv CMD-word (command field) legality + rtl/umi_txn_checker.sv request/response pairing + framing + """ + def __init__(self): + super().__init__('umi_checker', + files=['rtl/umi_handshake_checker.sv', + 'rtl/umi_cmd_checker.sv', + 'rtl/umi_txn_checker.sv'], + deps=[]) + # the block name is the family home, not a module. test_lint + # elaborates this fileset under a single top, so point it at the + # handshake checker; umi_cmd_checker and umi_txn_checker ship in + # the same fileset and are elaborated as tops by the formal lane. + with self.active_fileset('rtl'): + self.set_topmodule('umi_handshake_checker') + + +if __name__ == "__main__": + d = Checker() + d.write_fileset(f"{d.name}.f", fileset="rtl")