Add formal verification for the handshake protocol and CMD codec

.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

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"

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_<name>.sv) plus a job
+file (fv_<name>.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:]

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_<name>.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

umi/formal/.gitignore

@@ -0,0 +1,2 @@
+# sby work directories (build products; recreated on every run)
+*/fv_*_*/