From 3c1eaa3ec0492d183444b799c0d072a63f1f4ce4 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Tue, 2 Dec 2025 13:03:37 -0800
Subject: [PATCH] Split out scripts into their own files, fixup

---
 tests/formal_witness_replay/stage_1.sby     | 12 +++
 tests/formal_witness_replay/stage_1_fv.ys   |  4 +
 tests/formal_witness_replay/stage_1_init.ys |  6 ++
 tests/formal_witness_replay/stage_2.sby     | 12 +++
 tests/formal_witness_replay/stage_2_fv.ys   |  4 +
 tests/formal_witness_replay/stage_2_init.ys |  4 +
 tests/formal_witness_replay/staged.sh       | 87 +++++----------------
 7 files changed, 63 insertions(+), 66 deletions(-)
 create mode 100644 tests/formal_witness_replay/stage_1.sby
 create mode 100644 tests/formal_witness_replay/stage_1_fv.ys
 create mode 100644 tests/formal_witness_replay/stage_1_init.ys
 create mode 100644 tests/formal_witness_replay/stage_2.sby
 create mode 100644 tests/formal_witness_replay/stage_2_fv.ys
 create mode 100644 tests/formal_witness_replay/stage_2_init.ys

diff --git a/tests/formal_witness_replay/stage_1.sby b/tests/formal_witness_replay/stage_1.sby
new file mode 100644
index 000000000..19f3c1521
--- /dev/null
+++ b/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
diff --git a/tests/formal_witness_replay/stage_1_fv.ys b/tests/formal_witness_replay/stage_1_fv.ys
new file mode 100644
index 000000000..806fa9bdd
--- /dev/null
+++ b/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
diff --git a/tests/formal_witness_replay/stage_1_init.ys b/tests/formal_witness_replay/stage_1_init.ys
new file mode 100644
index 000000000..6a4ac2f28
--- /dev/null
+++ b/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
diff --git a/tests/formal_witness_replay/stage_2.sby b/tests/formal_witness_replay/stage_2.sby
new file mode 100644
index 000000000..24e276a0d
--- /dev/null
+++ b/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
diff --git a/tests/formal_witness_replay/stage_2_fv.ys b/tests/formal_witness_replay/stage_2_fv.ys
new file mode 100644
index 000000000..fa98b08fd
--- /dev/null
+++ b/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
diff --git a/tests/formal_witness_replay/stage_2_init.ys b/tests/formal_witness_replay/stage_2_init.ys
new file mode 100644
index 000000000..7e28612b7
--- /dev/null
+++ b/tests/formal_witness_replay/stage_2_init.ys
@@ -0,0 +1,4 @@
+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
diff --git a/tests/formal_witness_replay/staged.sh b/tests/formal_witness_replay/staged.sh
index 835d6386d..86cd9a52e 100644
--- a/tests/formal_witness_replay/staged.sh
+++ b/tests/formal_witness_replay/staged.sh
@@ -2,16 +2,17 @@
 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
+YOSYS=${YOSYS:-"yosys"}
+SBY=${SBY:-"sby"}
 
-tmpdir="$(mktemp -d "${TMPDIR:-/tmp}/yosys-staged-XXXX")"
-trap 'rm -rf "$tmpdir"' EXIT
+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"
@@ -26,39 +27,17 @@ 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\";
-"
+# 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"/
 
-# 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\";
-"
+# Generate the initial IL for stage 1.
+( cd "$tmpdir" && "$YOSYS" -q -l stage_1_init.log -s stage_1_init.ys )
 
-cat >"$stage1_sby" <<'EOF'
-[options]
-mode cover
-depth 24
-
-[engines]
-smtbmc
-
-[script]
-read_rtlil stage_1_fv.il
-
-[files]
-stage_1_fv.il
-EOF
+# 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"
@@ -71,36 +50,12 @@ if ! grep -qi "pass" "$stage1_dir/status"; then
 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\";
-"
+( cd "$tmpdir" && "$YOSYS" -q -l stage_2_init.log -s stage_2_init.ys )
 
 # 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" -q -l stage2_fv.log -s stage_2_fv.ys )
 
+# Run stage 2 formal verification.
 (
   cd "$tmpdir"
   YOSYS="$YOSYS" "$SBY" -f "$stage2_sby"