ip-rocev-mini-run

name	ip-rocev-mini-run
description	Walk through any hardware IP using ROCEV. Use for seminar demos or short explanations of Requirement, Obligation, Contract, Evidence, and Validation.

IP ROCEV Mini Run

Use this for any IP directory. Replace <ip>, <case>, and <obligation> with the current block and behavior.

For a fully filled local example, read:

.cursor_new/examples/pwm-gen-cx1-rocev-worked-example.md

Step 1 - Requirement

<ip> must handle <case> correctly.

Examples:

fifo_sync: preserves push/pop order
timer: interrupt pulse is exactly one cycle
register_block: W1C bits clear only on write-one
packet_parser: invalid header is rejected
bridge: backpressure does not drop a transaction

Step 2 - Obligation

O1: when <condition> occurs, DUT must produce <expected behavior>.
O2: no unintended side effect occurs.

Step 3 - Contract

Use at least one dynamic contract and, if available, one static/formal contract:

Dynamic:
  expected model/checker defines <expected behavior>
  scoreboard compares RTL observed vs expected
  coverage includes <case>

Static/formal:
  SVA states that <bad condition> cannot produce <forbidden output/state>

Step 4 - Evidence

Check the evidence bundle:

IP=<ip>
ls -lh "$IP/rtl/rtl_compile.json"
ls -lh "$IP/lint/dut_lint.json"
ls -lh "$IP/sim/results.xml"
ls -lh "$IP/sim/scoreboard_events.jsonl"
ls -lh "$IP/cov/coverage.json"
ls -lh "$IP/sim/"*.vcd
ls -lh "$IP/verify/formal_status.json"

Optional targeted search:

IP=<ip>
rg -n "<case>|<obligation>|scoreboard|coverage|formal|VCD" "$IP" doc/wiki

Step 5 - Validation

Say exactly what is closed:

Closed:
  <obligation> dynamic simulation evidence

Evidence:
  results.xml passed
  scoreboard row exists
  coverage bin hit
  VCD exists for debug

Not claimed:
  full formal proof unless formal_status.json proves the matching property

Filled-in quick examples

FIFO:
  Requirement: FIFO preserves order.
  Obligation: first pushed item is first popped item.
  Contract: reference queue model + scoreboard.
  Evidence: results.xml, scoreboard_events.jsonl, coverage for push/pop patterns.
  Validation: closed for ordering if all evidence passes.

Register block:
  Requirement: W1C status bits clear only on write-one.
  Obligation: write-zero leaves status bit unchanged.
  Contract: register model/checker + readback scoreboard.
  Evidence: APB/AHB sim result, scoreboard row, W1C coverage bin.
  Validation: closed for write-zero behavior.