Ip Rocev Mini Run

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.