Document and regression-test staged/cosimulation-based verification

docs/source/using_yosys/more_scripting/index.rst

@@ -12,6 +12,7 @@ More scripting
    selections
    interactive_investigation
    model_checking
+   staged_formal_sim
    data_flow_tracking
 
 .. troubleshooting

docs/source/using_yosys/more_scripting/staged_formal_sim.rst

@@ -0,0 +1,80 @@
+Staged formal with witness replay
+=================================
+
+This guide documents a simple two-stage flow for chaining formal runs via a
+saved witness and replaying it into a new initial state. The example in
+``tests/formal_witness_replay`` uses the Verific frontend for SystemVerilog/SVA;
+set ``YOSYS`` to a Verific-enabled binary (for example
+``../yosys-private/install/bin/yosys``) when running the scripts.
+
+Overview
+--------
+
+- Stage 1: run a cover/BMC proof that reaches an interesting waypoint and dump a
+  Yosys witness (``.yw``).
+- Replay: use ``sim -w`` to apply the witness to the original design, writing a
+  new RTLIL with baked-in init values.
+- Stage 2: reload that RTLIL, activate a different set of properties, and
+  continue proving/covering from the saved state.
+
+Flow contract
+-------------
+
+- The RTL must stay identical across stages. Only the active property set and
+  INIT values may change.
+- Use phase (or other) attributes to drop properties not meant for a given
+  stage; e.g. ``select */a:phase */a:phase=1 %d; delete`` before Stage 1.
+- Prefer YW over VCD: YW records solver-provided data with ``hdlname`` mapping,
+  so signal names stay stable through flattening and ``prep``.
+- ``sim -w`` writes back flip-flop and memory state; ``-a`` can be added to
+  include internal ``$`` wires in generated traces, but it does not change how a
+  YW witness is applied.
+- Environment-controlled signals should be inputs or ``anyseq``; ``sim`` only
+  drives inputs, while the solver may assign ``anyseq`` nets.
+- For later stages consider ``sim -noinitstate`` if you do not want ``$initstate``
+  to fire again.
+
+Example commands (from tests/formal_witness_replay)
+---------------------------------------------------
+
+Stage 1 preparation and cover run::
+
+  yosys -p '
+    read_verilog -formal tests/formal_witness_replay/dut.sv;
+    prep -top dut; flatten;
+    write_rtlil stage_1_init.il'
+
+  yosys -p '
+    read_rtlil stage_1_init.il;
+    select */a:phase */a:phase=1 %d; delete;
+    write_rtlil stage_1_fv.il'
+
+  # stage_1.sby uses "mode cover" with smtbmc to produce stage_1/engine_0/trace0.yw
+
+Replay the witness into a new init-state IL::
+
+  yosys -p '
+    read_rtlil stage_1_init.il;
+    prep -top dut;
+    sim -w -a -scope dut -r stage_1/engine_0/trace0.yw;
+    write_rtlil stage_2_init.il'
+
+Stage 2 cover run (only phase 2 properties active)::
+
+  yosys -p '
+    read_rtlil stage_2_init.il;
+    select */a:phase */a:phase=2 %d; delete;
+    write_rtlil stage_2_fv.il'
+
+  # stage_2.sby then proves the pending ack cover starting from the baked state
+
+Notes and caveats
+-----------------
+
+- YW is input-only for ``sim``; the pass never writes a YW file. Use VCD/FST/AIW
+  output if you need a trace of the replay itself.
+- Cross-stage sequential assumptions may need care. If an assumption spans
+  cycles across the stage boundary, you may need to extend the witness during FV
+  and trim it before replay so the assumption is fully evaluated.
+- Keep a single RTL source with property guards so that signal names stay
+  stable; changing the HDL between stages will break witness replay.

tests/formal_witness_replay/config.sby

@@ -0,0 +1,34 @@
+[tasks]
+stage_1_init
+stage_1_fv
+stage_2_init
+stage_2_fv
+
+[options]
+stage_1_init:
+mode prep
+expect unknown
+make_model prep
+
+stage_1_fv:
+mode cover
+depth 24
+
+[engines]
+stage_1_init stage_2_init:
+none
+
+stage_1_fv stage_2_fv: 
+smtbmc
+
+[script]
+stage_1_init:
+verific -formal dut.sv
+
+
+[files]
+stage_1_init: dut.sv
+
+stage_2_init:
+stage_1/engine_0/trace0.yw
+stage_1_init.il

tests/formal_witness_replay/dut.sv

@@ -0,0 +1,47 @@
+module dut (
+    input  logic clk,
+    input  logic req,
+    input  logic ack
+);
+
+`ifdef FORMAL
+
+  logic [1:0] reqs_seen;
+
+  // Deterministic initial state for the internal counter.
+  initial reqs_seen = 2'b00;
+
+  always @ (posedge clk) begin
+    if (req)
+      reqs_seen <= reqs_seen + 1'b1;
+  end
+
+  // Req is only high for one cycle.
+  assume property (@(posedge clk) req |-> ##1 !req);
+
+  // Reqs are at least 8 cycles apart.
+  assume property (@(posedge clk) req |-> ##1 (!req [*7]));
+
+  // Ack comes exactly 4 cycles after req.
+  assume property (@(posedge clk) req |-> ##4 ack);
+
+  // Ack must remain low if no req 4 cycles ago.
+  assume property (@(posedge clk) !$past(req,4) |-> !ack);
+
+  // Phase 1: stop exactly when the second request is seen.
+  always @ (posedge clk) begin
+    (* phase = "1" *)
+    cover(reqs_seen == 2);
+  end
+
+  // Phase 2: forbid more reqs and cover the pending ack.
+  always @ (posedge clk) begin
+    (* phase = "2" *)
+    assume(!req);
+    (* phase = "2" *)
+    cover(ack);
+  end
+
+`endif
+
+endmodule

tests/formal_witness_replay/run-test.sh

@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+set -eu
+source ../gen-tests-makefile.sh
+generate_mk --bash
+exec ${MAKE:-make} -f run-test.mk

tests/formal_witness_replay/stage_1.sby

@@ -0,0 +1,12 @@
+[options]
+mode cover
+depth 24
+
+[engines]
+smtbmc
+
+[script]
+read_rtlil stage_1_fv.il
+
+[files]
+stage_1_fv.il

tests/formal_witness_replay/stage_1_fv.ys

@@ -0,0 +1,4 @@
+read_rtlil stage_1_init.il
+select */a:phase */a:phase=1 %d
+delete
+write_rtlil stage_1_fv.il

tests/formal_witness_replay/stage_1_init.ys

@@ -0,0 +1,6 @@
+verific -formal dut.sv
+verific -import -all
+hierarchy -top dut
+prep -top dut
+flatten
+write_rtlil stage_1_init.il

tests/formal_witness_replay/stage_2.sby

@@ -0,0 +1,12 @@
+[options]
+mode cover
+depth 24
+
+[engines]
+smtbmc
+
+[script]
+read_rtlil stage_2_fv.il
+
+[files]
+stage_2_fv.il

tests/formal_witness_replay/stage_2_fv.ys

@@ -0,0 +1,4 @@
+read_rtlil stage_2_init.il
+select */a:phase */a:phase=2 %d
+delete
+write_rtlil stage_2_fv.il

tests/formal_witness_replay/stage_2_init.ys

@@ -0,0 +1,4 @@
+read_rtlil stage_1_init.il
+prep -top dut
+sim -noinitstate -w -a -scope dut -r stage_1/engine_0/trace0.yw
+write_rtlil stage_2_init.il

tests/formal_witness_replay/staged.sh

@@ -0,0 +1,70 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+ROOT="$(cd "$(dirname "$0")" && pwd)"
+YOSYS=${YOSYS:-"yosys"}
+SBY=${SBY:-"sby"}
+
+if [ -z "${OUTPUT_DIR:-}" ]; then
+  tmpdir="$(mktemp -d "${TMPDIR:-/tmp}/yosys-staged-XXXX")"
+  trap 'rm -rf "$tmpdir"' EXIT
+else
+  tmpdir="$OUTPUT_DIR"
+  mkdir -p "$tmpdir"
+  tmpdir="$(cd "$tmpdir" && pwd)"
+fi
+
+stage1_init="$tmpdir/stage_1_init.il"
+stage1_fv="$tmpdir/stage_1_fv.il"
+stage1_sby="$tmpdir/stage_1.sby"
+stage1_dir="$tmpdir/stage_1"
+witness="$stage1_dir/engine_0/trace0.yw"
+
+stage2_init="$tmpdir/stage_2_init.il"
+stage2_fv="$tmpdir/stage_2_fv.il"
+stage2_sby="$tmpdir/stage_2.sby"
+stage2_dir="$tmpdir/stage_2"
+
+echo "Preparing staged formal witness replay test in $tmpdir"
+
+# Copy static assets into the temp dir.
+cp "$ROOT"/{dut.sv,stage_1_init.ys,stage_1_fv.ys,stage_2_init.ys,stage_2_fv.ys,stage_1.sby,stage_2.sby} "$tmpdir"/
+
+# Generate the initial IL for stage 1.
+( cd "$tmpdir" && "$YOSYS" -q -l stage_1_init.log -s stage_1_init.ys )
+
+# Filter to phase 1 properties to produce the final IL for stage 1, ready for
+# formal verification.
+( cd "$tmpdir" && "$YOSYS" -q -l stage1_fv.log -s stage_1_fv.ys )
+
+# Run stage 1 formal verification to produce a witness.
+(
+  cd "$tmpdir"
+  YOSYS="$YOSYS" "$SBY" -f "$stage1_sby"
+)
+
+if ! grep -qi "pass" "$stage1_dir/status"; then
+  echo "stage 1 did not pass"
+  cat "$stage1_dir/status" || true
+  exit 1
+fi
+
+# Replay the witness into a new init-state IL for stage 2.
+( cd "$tmpdir" && "$YOSYS" -q -l stage_2_init.log -s stage_2_init.ys )
+
+# Filter to phase 2 properties.
+( cd "$tmpdir" && "$YOSYS" -q -l stage2_fv.log -s stage_2_fv.ys )
+
+# Run stage 2 formal verification.
+(
+  cd "$tmpdir"
+  YOSYS="$YOSYS" "$SBY" -f "$stage2_sby"
+)
+
+if ! grep -qi "pass" "$stage2_dir/status"; then
+  echo "stage 2 did not pass"
+  cat "$stage2_dir/status" || true
+  exit 1
+fi
+
+echo "Staged witness replay test passed."