Formal Properties In Requirements

requirements.yml can carry machine-checkable formal properties next to the human-readable requirement they prove. rr formal run --contract reads those blocks, generates an external PSL vunit, and proves the properties against the HDL without editing the DUT.

Schema

Attach formal: to a functional_contract: entry:

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

The block accepts:

At least one of psl or sva is required when formal: is present.

Two Checking Tiers

rr sim run --psl evaluates PSL assertions during simulation. This is a runtime check: it catches failures reached by the test stimulus and reset sequence you actually ran.

rr formal run --contract proves the formal.psl properties from requirements.yml with the open-source formal flow. This is an exhaustive proof over the reachable state space using k-induction. A passing run reports:

✅ PROVED — all properties hold for '<top>'.

Use simulation assertions for fast regression coverage and waveform-friendly debug. Use contract formal when the requirement is a protocol invariant that should hold for every legal input sequence, not just the sequences already in the cocotb test.

Counterexamples Name Requirements

The generated vunit labels each assertion with the requirement id. When the solver finds a failing trace, rr formal run --contract maps the failed label back to the contract:

❌ COUNTEREXAMPLE — contract violated: REQ-AXIS-TDATA-STABLE.

That makes the trace actionable: the failure is tied to the requirement that was violated, not just to an anonymous assertion in generated code.

Toolchain

The formal flow uses the vendored oss-cad-suite bundle:

• ghdl with PSL support
• yosys with the ghdl plugin
• sby / SymbiYosys
• SMT backends from the bundle

Install it with:

rr eda install formal

rr formal run --contract locates ~/.local/opt/oss-cad-suite automatically. No Vivado, Quartus, FPGA board, queue slot, or hardware lease is involved for an open-source formal host run.

AXI Handshake Patterns

AXI-style channels must keep xVALID asserted until the transfer is accepted:

formal:
  psl: "always ((valid = '1' and ready = '0') -> next(valid) = '1')"
  clock: "rising_edge(clk)"

Payload must also remain stable while the channel is stalled:

formal:
  psl: "always ((valid = '1' and ready = '0') -> next(stable(tdata)))"
  clock: "rising_edge(clk)"

The worked example in examples/formal_axi_handshake/ proves both properties with rr formal run --contract.

Multi-channel ordering properties use the same shape. For AXI write channels, write data must not be issued before the write address has been accepted:

formal:
  psl: "always ((wvalid = '1' and aw_seen = '0') -> awvalid = '1')"
  clock: "rising_edge(clk)"

In a real slave or bridge, aw_seen is the design-visible state that becomes true after awvalid = '1' and awready = '1', and is cleared when the write transaction completes.