Add initial test impl

tests/staged_sim_and_verif/Req_Ack.sv

@@ -0,0 +1,65 @@
+module DUT (
+    input  logic clk,
+    output logic req,
+    output logic ack
+);
+
+`ifdef FORMAL
+
+  logic [1:0] reqs_seen;
+  logic [31:0] cycle_count;
+
+  // Deterministic initial state
+  initial begin
+    // req       = 1'b0;
+    reqs_seen = 2'b00;
+    cycle_count = 32'b0;
+  end
+
+  always @ (posedge clk) begin
+    if (req) reqs_seen <= reqs_seen + 1;
+    cycle_count <= cycle_count + 1;
+  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
+  );
+
+  // For the purpose of demonstration, stop exactly when second req pulse
+  // occurs. This leaves us in a state where we're waiting for the second ack.
+  always @(posedge clk) begin
+    (* phase = "1" *)
+    cover(reqs_seen == 2);
+  end
+
+  // In phase 2, assume that there's no more reqs; despite this, assert that
+  // an ack will eventually come for the second req.
+  always @ (posedge clk) begin
+    (* phase = "2" *)
+    assume(!req);
+  end
+  always @(posedge clk) begin
+    (* phase = "2" *)
+    cover(ack);
+  end
+
+
+`endif
+
+endmodule

tests/staged_sim_and_verif/skip_staged_flow.sby

@@ -0,0 +1,64 @@
+[tasks]
+stage_1_init init
+stage_1_fv fv
+stage_2_init init
+stage_2_fv fv
+
+[options]
+init:
+mode prep
+
+fv:
+mode cover
+depth 40
+
+--
+
+[engines]
+init: none
+fv: smtbmc
+
+[script]
+stage_1_init:
+verific -formal Req_Ack.sv
+hierarchy -top DUT
+setattr -set keep 1 w:\\*
+prep -top DUT
+flatten
+write_rtlil stage_1_init.il
+
+stage_1_fv:
+read_rtlil stage_1_init.il
+# This selection computes (all things with phase)-(all things with phase=1)
+# to remove all phased SVA constructs not intended for phase 1.
+select */a:phase */a:phase=1 %d
+delete
+
+stage_2_init:
+read_rtlil stage_1_init.il
+sim -a -w -scope DUT -r trace0.yw
+write_rtlil stage_2_init.il
+
+stage_2_fv:
+read_rtlil stage_2_init.il
+# This selection computes (all things with phase)-(all things with phase=2)
+# to remove all phased SVA constructs not intended for phase 2.
+select */a:phase */a:phase=2 %d
+delete
+
+--
+
+[files]
+
+stage_1_init:
+Req_Ack.sv
+
+stage_1_fv:
+skip_staged_flow_stage_1_init/src/stage_1_init.il
+
+stage_2_init:
+skip_staged_flow_stage_1_init/src/stage_1_init.il
+skip_staged_flow_stage_1_fv/engine_0/trace0.yw
+
+stage_2_fv:
+skip_staged_flow_stage_2_init/src/stage_2_init.il

tests/staged_sim_and_verif/staged_sim_and_verif.sby

@@ -0,0 +1,14 @@
+[options]
+mode cover
+depth 1
+
+[engines]
+smtbmc
+
+[script]
+# Minimal job so dumptaskinfo picks up the tools this flow requires.
+verific -formal Req_Ack.sv
+prep -top DUT
+
+[files]
+Req_Ack.sv

tests/staged_sim_and_verif/staged_sim_and_verif.sh

@@ -0,0 +1,19 @@
+#!/bin/bash
+set -euo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+cd "$SCRIPT_DIR"
+
+FLOW_FILE="skip_staged_flow.sby"
+
+# Clean previous runs so we always exercise the full staged flow.
+rm -rf skip_staged_flow_stage_1_init skip_staged_flow_stage_1_fv skip_staged_flow_stage_2_init skip_staged_flow_stage_2_fv
+
+run_task() {
+    python3 "$SBY_MAIN" -f "$FLOW_FILE" "$1"
+}
+
+run_task stage_1_init
+run_task stage_1_fv
+run_task stage_2_init
+run_task stage_2_fv