Merge 834c84f84d into e3db8fee6f

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."