Initial commit

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/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/staged.sh

@@ -0,0 +1,115 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+ROOT="$(cd "$(dirname "$0")" && pwd)"
+# Default to a Verific-enabled yosys; override with YOSYS env if needed.
+YOSYS=${YOSYS:-"$ROOT/../../yosys-private/install/bin/yosys"}
+# Default to the matching sby alongside the custom yosys; fall back to PATH.
+SBY=${SBY:-"$ROOT/../../yosys-private/install/bin/sby"}
+if [ ! -x "$SBY" ]; then
+  SBY=sby
+fi
+
+tmpdir="$(mktemp -d "${TMPDIR:-/tmp}/yosys-staged-XXXX")"
+trap 'rm -rf "$tmpdir"' EXIT
+
+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"
+
+# Convert the RTL once; both stages start from the same RTLIL.
+"$YOSYS" -q -l "$tmpdir/convert.log" -p "
+  verific -formal \"$ROOT/dut.sv\";
+  verific -import -all;
+  hierarchy -top dut;
+  prep -top dut;
+  flatten;
+  write_rtlil \"$stage1_init\";
+"
+
+# Filter to phase 1 properties.
+"$YOSYS" -q -l "$tmpdir/stage1_fv.log" -p "
+  read_rtlil \"$stage1_init\";
+  select */a:phase */a:phase=1 %d;
+  delete;
+  write_rtlil \"$stage1_fv\";
+"
+
+cat >"$stage1_sby" <<'EOF'
+[options]
+mode cover
+depth 24
+
+[engines]
+smtbmc
+
+[script]
+read_rtlil stage_1_fv.il
+
+[files]
+stage_1_fv.il
+EOF
+
+(
+  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.
+"$YOSYS" -q -l "$tmpdir/replay.log" -p "
+  read_rtlil \"$stage1_init\";
+  prep -top dut;
+  sim -w -a -scope dut -r \"$witness\";
+  write_rtlil \"$stage2_init\";
+"
+
+# Filter to phase 2 properties.
+"$YOSYS" -q -l "$tmpdir/stage2_fv.log" -p "
+  read_rtlil \"$stage2_init\";
+  select */a:phase */a:phase=2 %d;
+  delete;
+  write_rtlil \"$stage2_fv\";
+"
+
+cat >"$stage2_sby" <<'EOF'
+[options]
+mode cover
+depth 24
+
+[engines]
+smtbmc
+
+[script]
+read_rtlil stage_2_fv.il
+
+[files]
+stage_2_fv.il
+EOF
+
+(
+  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."