Contract-first verification — walkthrough

You have an IP. You have HDL. You want the tool to tell you when the shape of your IP drifts from what you intended, not just when the tests you remembered to write still pass.

This guide walks one IP from "scaffold the contract" to "CI gate on every push". ~15 steps, each with a command you run. Every command is one we ran while adopting contract-first on a real crossbar + PULP wrapper IPs.

0. Starting state

You have something that looks like:

hw/ip/<name>/
├── ip.yml
└── hdl/
    └── <name>.{sv,vhd}

No requirements.yml yet. That's what we're adding.

1. Scaffold the contract

rr sim contract-init hw/ip/<name>/hdl/<name>.sv

This writes hw/ip/<name>/requirements.yml from the current HDL. Pay attention to the banner at the top:

⚠️ This scaffold reflects the CURRENT HDL implementation — not necessarily the INTENDED contract. Review before committing.

Scaffold ≠ contract. The scaffold is a starting point; the contract is what you decide the IP should be.

2. Review port_contract:

Open requirements.yml. The port_contract: block has four sub-lists:

• slaves: — AXI/AXIS/Avalon bundles flowing into the IP.
• masters: — bundles flowing out.
• scalars: — single-bit or small ports (sel, enable, valid, one-shot irq, etc.).
• clocks: / resets: — self-explanatory.

Bundle detection isn't perfect yet. An indexed AXIS bundle (m00_axis_tdata, m01_axis_tdata) may land in masters: as one bundle or split into scalars. Fix by hand — the requirements.yml is the source of truth from here on, not the parser.

Example (AXIS 1→2 demux):

port_contract:
  slaves:
    - { name: s_axis,   protocol: axi-stream }
  masters:
    - { name: m00_axis, protocol: axi-stream }
    - { name: m01_axis, protocol: axi-stream }
  scalars:
    - { name: sel, dir: in, width: 1 }
  clocks:  [{ name: aclk }]
  resets:  [{ name: aresetn, polarity: active_low }]

3. Declare functional requirements

Every behavioural property your IP must honour becomes a REQ. Examples from the 2→1 AXIS mux:

functional_contract:
  - { id: REQ-1, kind: behavioral, desc: "m_axis.tdata == sN_axis.tdata when sel=N" }
  - { id: REQ-2, kind: behavioral, desc: "tvalid flows through the selected slave only" }
  - { id: REQ-3, kind: behavioral, desc: "backpressure: tready from master forwards to selected slave" }
  - { id: REQ-4, kind: negative,   desc: "unselected slave's tvalid does NOT appear on master" }
  - { id: REQ-5, kind: behavioral, desc: "sel change between frames does not corrupt an in-flight tlast" }

Rules of thumb:

• kind: behavioral — "when X, the IP does Y."
• kind: negative — "when X, the IP does NOT do Y." (attack surface)
• desc: must be concrete enough that a future test author can write assert statements from it. "works correctly" is not a REQ.

Aim for 3–10 REQs for a typical AXI-wrapper IP. More if the IP has ordering or CDC guarantees.

4. Wire requirements.yml into ip.yml

Opt into contract-first by adding one line:

# hw/ip/<name>/ip.yml
name: my_ip
requirements: requirements.yml   # ← add this
# ...rest of ip.yml unchanged

Absence = no contract declared, tooling stays silent. Presence = the gates below activate for this IP.

5. Run contract-check

rr sim contract-check

You should see:

ip:      [OK] my_ip
contract-check passed: 1 contract(s) OK.

If the declared shape diverges from the HDL, every mismatch is enumerated:

ip:      [FAIL] my_ip  (.../requirements.yml)
  ! [master-count] master count mismatch: declared 2 (m00_axis, m01_axis), actual 3 (m00_axis, m01_axis, m02_axis)

That's the "wrong shape" signal your unit tests won't give you.

6. Generate test stubs

rr sim scaffold hw/ip/<name>

Emits tests/test_<name>.py with one @cocotb.test per REQ, each tagged with @requires("REQ-N") and a NotImplementedError body.

Every scaffold is a vacuous placeholder — coverage-map will flag it as such until you fill in real assertions.

7. Fill in a test body (adversarial stance)

Every test is an attack on the DUT, not a confirmation. If your test can't fail when the DUT is wrong, it isn't a test — it's a lie-in-waiting.

Example — REQ-1 (mux pass-through):

@cocotb.test()
@requires("REQ-1")
async def test_mux_pass_through(dut):
    await setup_clock(dut.aclk, 10)
    await reset(dut.aresetn)
    dut.sel.value = 0
    drive_axis(dut.s00_axis, tdata=0xDEADBEEF, tvalid=1)
    await RisingEdge(dut.aclk)
    await ReadOnly()
    # Adversarial: if the mux is wired wrong, this fires.
    assert dut.m_axis_tdata.value == 0xDEADBEEF, \
        f"expected DEADBEEF, got {int(dut.m_axis_tdata.value):#x}"

Example — REQ-4 (negative: silence on unselected):

@cocotb.test()
@requires("REQ-4")
async def test_unselected_slave_is_silent(dut):
    await setup_clock(dut.aclk, 10); await reset(dut.aresetn)
    dut.sel.value = 0
    drive_axis(dut.s01_axis, tdata=0x12345678, tvalid=1)  # unselected
    await RisingEdge(dut.aclk); await ReadOnly()
    assert dut.m_axis_tvalid.value == 0, \
        "leak: unselected slave's tvalid reached the master"

Negative tests earn their keep when someone "simplifies" the mux into a straight OR gate.

8. Pick a simulator

Declare it once in ip.yml so rr sim run --ip picks the right backend:

# hw/ip/<name>/ip.yml
build:
  simulation:
    simulator: verilator
    test_dir: tests

9. Run the tests standalone

rr sim run --ip hw/ip/<name>

No wrapping project.yml needed. The command resolves top, sources, simulator, and test dir from ip.yml alone.

Break the DUT (e.g. swap s00_axis ↔ s01_axis), re-run, confirm the test fails loudly. A test that stays green when the DUT is wrong is not a test.

10. Verify coverage

rr sim coverage-map

You should see every REQ marked ✓ with the test that anchors it:

ip:      [OK] my_ip: covered=5/5
  ✓ REQ-1: test_mux_pass_through
  ✓ REQ-2: test_tvalid_selected
  ...
coverage-map passed: 1 contract(s) fully covered.

Common failure signals:

• ✗ REQ-N: (uncovered) — you declared a REQ with no test tag.
• ∅ REQ-N: test_x (no assertions — vacuous tag) — tag without assert statements; write a real assertion.
• ? REQ-ORPHAN — test tags a REQ that doesn't exist in requirements.yml (typo or REQ deleted, tag forgotten).

All three are CI-fail-worthy.

11. Wire into CI

# .github/workflows/contract-gate.yml
jobs:
  contract-first:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - run: pip install routertl
      - run: rr sim contract-check
      - run: rr sim coverage-map

Both commands exit non-zero on any failure. Gate is the tree-shaped report: project + every IP, union exit code.

12. Optional: standalone synth-smoke

Registry publishers who want a synth-pass guarantee before push can declare build.hardware.* in ip.yml and run:

rr synth run --ip hw/ip/<name>

Today this validates readiness (vendor, part, top module, sources) and prints the plan; the full Vivado/Quartus spawn via --ip is coming. The readiness gate alone catches ~80% of registry-push regressions.

13. Migration notes

Contract-first adoption is gradual. The pattern we used on sdi_claude:

1. Ship requirements.yml for every IP (Phase 1 — 20 min each).
2. Gate contract-check in CI (Phase 2 — one PR).
3. Fill in real test bodies REQ-by-REQ as the IPs get touched (Phase 3 — ongoing, paired with bug-fix work).
4. Gate coverage-map once every IP is non-vacuous (Phase 4).

You don't need to solve Phase 3 before opting in — an empty functional_contract: [] is valid.

14. Pitfalls

• Indexed AXIS bundles — the SV parser sometimes splits m00_axis_t* + m01_axis_t* into loose scalars instead of two bundles. Hand-correct requirements.yml until the parser fix lands.
• Mixed-language on GHDL — if compile fails, either switch simulator (riviera-pro) or add a VHDL shim around the SV core.
• Scaffold-test lying — a @requires("REQ-N") tag on a test with assert True or no asserts is vacuous. coverage-map flags it; do not suppress. See ASSERT_QUALITY.md for the full catalogue of patterns that are classified as trivial vs substantive, with DUT-observable examples.
• requirements: pointing at a missing file — hard error, not silent skip. Fix the path or remove the declaration.

15. What this buys you

• A declarative shape the IP promises to honour.
• A gate that catches "wrong shape" before it hits integration.
• A test suite where every REQ is earned by at least one assertion.
• An IP that can be verified in isolation — rr sim contract-check, rr sim coverage-map, rr sim run --ip, rr synth run --ip — no wrapping project.yml needed.

Unit tests confirm the DUT does what it does. The contract is what forces you to decide what it should do.