Verification contracts

RouteRTL can treat verification as a traceable contract rather than a collection of tests that happen to pass. The project says what the design must do, each IP can carry its own requirements, and the checks connect those declarations to observable evidence.

specification and design intent
              ↓
project and IP requirements
              ↓
stimulus capabilities and test/property scaffolds
              ↓
cocotb observations · PSL/SVA properties · static analysis
              ↓
shape · stimulus · assertion quality · anti-vacuity · proof
              ↓
implementation and hardware evidence where required
              ↓
reproducible human report · JSON manifest · policy verdict

This structure is useful to engineers and coding agents for the same reason: a failed gate identifies the missing link instead of asking either one to infer intent from HDL and test names.

1. Declare intent at the right level

A project can declare system-level requirements, while an IP can reference its own requirements.yml from ip.yml. A contract records two different things:

• the interface shape: clocks, resets, scalar ports, and protocol endpoints;
• the functional behavior: positive, negative, ordering, reset, and error requirements.

Scaffolding starts from the HDL that exists today:

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

The result is a draft, not proof of intent. Port discovery can describe the current implementation, but only a reviewed requirement can say what the implementation should do. For a standardized interface, requirements can cite the source document and clause that define the expected behavior. A custom interface can declare that no public specification exists and record why.

Once the contract is referenced by the project or IP manifest, RouteRTL checks the declared shape against the parsed HDL:

rr sim contract-check

Added, removed, renamed, or reclassified interfaces then become explicit contract changes rather than integration surprises.

2. Scaffold tests without mistaking scaffolds for evidence

RouteRTL has two related starting points. rr testgen creates general cocotb boilerplate from a discovered HDL module. The contract-aware scaffold creates one placeholder per functional requirement:

rr testgen <module>
rr sim scaffold hw/ip/<name>

Tests from the contract-aware scaffold are linked to requirements with @requires("REQ-N"). A placeholder deliberately does not count as coverage. It must be replaced with a test that drives the DUT and contains an assertion capable of failing when the implementation is wrong.

A useful test follows a simple pattern:

@cocotb.test()
@requires("REQ-READY-1")
async def test_backpressure_holds_payload(dut):
    # Set up and drive a stalled transfer, then sample the DUT.
    assert int(dut.out_data.value) == 0x5A

The expected value should come from the requirement or specification, not from the same calculation as the DUT. The test is evidence only if a plausible broken implementation makes it fail.

Run an IP's testbench directly from its manifest:

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

3. Check traceability and assertion quality

The coverage map joins declared requirements to their verification evidence:

rr sim coverage-map

It reports more than whether a test name exists:

Trivial patterns such as assert True, constant truth tests, and self-comparison do not earn coverage. The checker also follows same-file assertion helpers, so moving an assertion into a local helper does not break the evidence chain.

For automation, the same matrix is available as structured output:

rr sim coverage-map --json

The command keeps the same exit-code semantics in human and JSON modes, which lets an agent inspect details while pre-commit and CI enforce the verdict.

4. Prove that the relevant stimulus happened

A test can name the right requirement and contain a real assertion while never driving the condition that matters. This is especially dangerous around backpressure, reset during traffic, boundary lengths, malformed input, overflow, and error recovery.

The complete evidence path is therefore longer than requirement-to-test traceability:

specification clause
        ↓
named requirement or feature arm
        ↓
BFM is capable of producing it
        ↓
the condition was produced in this run
        ↓
a monitor observed it at the DUT boundary
        ↓
the associated assertion evaluated

RouteRTL protocol BFMs can declare the corner cases they emit, and runtime stimulus ledgers record what monitors actually observed. Audit the latest run with:

rr sim stimulus-audit

This separates three failures that otherwise look like “missing coverage”:

• specification gap — no requirement represents a normative corner case;
• asset gap — no available BFM can generate the required condition;
• stimulus hole — the BFM supports it, but the suite never produced it.

For protocols with tables or enumerated modes, a feature matrix makes each arm visible. A broad requirement such as “all packet types decode correctly” should not conceal a packet type that never appears in the stimulus corpus.

5. Ask whether the test has teeth

Static assertion-quality checks reject obvious vacuity, but the strongest test question is still:

Would this test fail against a plausible broken implementation?

Useful confidence levels are:

RouteRTL simulation journals and audits preserve red-to-green history and can associate requirements with defect witnesses:

rr sim audit
rr sim attack-audit

A future mutation probe can strengthen this further, but mutation must remain independent of the expected-value logic. A mutation framework that changes both the DUT and its oracle would manufacture confidence rather than measure it.

6. Add properties where examples are not enough

A behavioral requirement can carry a PSL or SVA property beside its prose. RouteRTL generates an external verification unit from that property, so the requirement remains the source of truth and the DUT does not need generated assertion code mixed into it.

functional_contract:
    - id: REQ-VALID-STABLE
      kind: behavioral
      desc: "valid remains asserted while ready is low"
      formal:
          psl: "always ((valid = '1' and ready = '0') -> next(valid) = '1')"
          clock: "rising_edge(clk)"

There are two complementary ways to evaluate properties:

rr sim run --psl
rr formal run --contract

The first evaluates PSL along the paths reached in simulation. The second generates the contract property wrapper and proves it over the formal state space. When a formal implication passes, RouteRTL also covers its antecedent; an unreachable antecedent is reported as vacuous rather than accepted as a meaningful proof.

The property is only half of a formal contract. Clock, reset, legal-input, and environment assumptions determine which state space is being proved. Reviewers must be able to see those assumptions and tell whether they exclude behavior the real system can produce. Formal antecedent anti-vacuity is available today; complete environment over-constraint analysis is not yet an enforced RouteRTL gate.

7. Layer structural analysis around behavioral evidence

Requirements and simulation describe intended behavior. Language-aware lint and SV-Gap add structural evidence, including CDC/RDC analysis, clock and crossing coverage, and waiver validation. A project can select the profile in project.yml, keeping the same policy for engineers, agents, pre-commit, and CI:

rr linting --profile rr-cdc-structural-provisional --src src

Structural analysis is not a replacement for simulation or formal proof. It is another view of the same design, with its own stated coverage boundary, so a clean report is not mistaken for complete sign-off.

Waivers qualify evidence; they do not prove it

A waiver should identify the exact finding, its reason and owner, the scope it applies to, and an expiry or review condition. Reports should keep these states different:

• proven — the required evidence passed;
• waived — a reviewed exception suppresses a finding;
• unsupported — the selected backend cannot produce the evidence;
• not run — the check was available but absent from this verdict.

RouteRTL already has coverage and CDC waiver surfaces. A single waiver model shared by simulation coverage, formal, lint, timing, and hardware evidence is a target for the complete journey, not a released unified contract today.

8. Keep design documentation in the evidence chain

A good IP package includes a Firmware Design Document that explains the theory of operation and architectural choices that schemas cannot express. The requirements then point back to authoritative specifications or explicitly record why the behavior is project-specific.

RouteRTL can currently run a strict documentation build from pre-commit when a project enables hooks.pre_commit.check_docs and provides mkdocs.yml. It also validates requirement-level specification citations. It does not currently fail solely because an IP has no FDD, nor does the released CLI provide an rr fdd currentness gate. Treat the FDD as required engineering practice, but do not mistake that practice for an enforced RouteRTL check yet.

The intended relationship is:

engineer-authored rationale       declarative machine truth
Overview                          requirements and interfaces
Theory of Operation       ↔       registers and dependencies
Architecture                      generated block/decision views

Generated sections should be refreshable without rewriting the engineer's rationale. The document is an aggregate view over canonical configuration, not a second place to maintain register maps or port lists.

9. Compose contracts at project boundaries

An IP can be correct in isolation while the assembled project is wrong. At each connection, the project needs evidence that producer and consumer assumptions agree:

• data and address widths;
• protocol modes and optional signals;
• reset polarity, sequencing, and recovery;
• clock domains and intentional crossings;
• buffering, ordering, and backpressure expectations.

One project-level requirement may need evidence from several IP contracts and an integration test. A single @requires tag on one unit test should not be presented as proof of an end-to-end behavior.

The same graph enables change-impact analysis. If a requirement, port, register, dependency, specification citation, or policy changes, RouteRTL should be able to identify the tests, formal properties, FDD sections, targets, and earlier evidence that are now stale. Contract shape checking exists today; complete cross-artifact impact analysis does not.

10. Close selected requirements on hardware

Not every requirement needs a board. Pure transformations and protocol invariants often close in simulation or formal. Requirements involving external clocking, reset behavior, device primitives, physical interfaces, timing, or vendor integration may require implementation and hardware evidence.

Hardware evidence should bind together:

• the requirement being checked;
• the exact project and bitstream identity;
• the board and target configuration;
• the leased command or capture that produced the observation;
• measured values, logs, or ILA/REA captures;
• a timestamp and reproducibility information.

RouteRTL already provides provenance-aware build, programming, hardware, and capture commands. Those results are not yet generally joined to requirement IDs as one verification manifest. Until they are, record the relationship explicitly in the project's validation material.

11. Preserve one reproducible evidence manifest

A green result without its inputs is difficult to review later. A complete manifest should identify the HDL and configuration digests, tool versions, requirements, test and property results, coverage boundaries, waivers, FDD state, build identity, and any hardware observations.

The human view should be organized by requirement rather than by tool:

Machine-readable output must preserve the same distinctions. An agent can then find the missing link and propose work, while policy decides which states block pre-commit, CI, release, or registry promotion.

RouteRTL's individual commands already provide structured results in several of these areas. A unified rr verify requirement-centric report and versioned evidence manifest describe the target experience; they are not released CLI commands today.

12. Adopt the journey as a maturity ladder

Projects should not have to enable every strict gate at once. A practical adoption ladder is:

1. Declare — record reviewed project and IP requirements.
2. Anchor — cite specifications or declare why behavior is project-specific.
3. Exercise — show that required feature arms and corner cases reached the DUT.
4. Assert — link substantive, relevant observations to every requirement.
5. Prove — add formal properties and visible environment assumptions for invariants.
6. Inspect — run structural, CDC/RDC, and implementation checks with qualified waivers.
7. Document — keep the FDD present and current with declarative truth.
8. Integrate — prove compatibility and end-to-end behavior across IP boundaries.
9. Validate — attach implementation or hardware evidence where the requirement demands it.
10. Reproduce — preserve the inputs, evidence, and policy that produced the verdict.

Measurement can begin before enforcement. A team can first see missing or stale evidence as advisory, then promote selected maturity levels to strict policy once the project is ready.

13. Assemble today's gate

A practical verification gate runs the independent checks together:

rr sim contract-check
rr sim coverage-map
rr sim run --ip hw/ip/<name>
rr sim stimulus-audit
rr formal run --contract
rr linting

Projects can introduce the layers gradually. Start by declaring reviewed requirements and checking interface shape. Then replace scaffolds with substantive tests, add formal properties for invariants, and enable the appropriate lint profile. Once a layer is trusted, run the same command in pre-commit and CI.

The goal is not a longer checklist. It is a connected answer to four review questions:

1. What did the design promise?
2. Which test, assertion, or property supplies the evidence?
3. Did that evidence actually exercise something that could fail?
4. Can a human or agent reproduce the verdict from the project configuration?

These commands are intentionally independent today. Their separation keeps each failure honest, although it means the engineer still assembles the final review. The complete journey does not replace them; it joins their evidence without flattening “waived,” “unsupported,” “not run,” and “proven” into the same green status.