Merge e904e88fc9 into cc84339b37

tests/staged_sim_and_verif/README.md

@@ -0,0 +1,7 @@
+Staged simulation + verification example demonstrating staged verification using simulation and writeback via `sim -w` pass.
+- Stage 1: run cover to reach “req sent, ack pending”, producing `trace0.yw`.
+- Stage 2: replay the witness with `sim -w` to bake state, then run another cover that requires the ack.
+- Uses phased SVA (`(* phase = "1" *)`, `(* phase = "2" *)`) and a selector script to strip irrelevant properties per stage.
+- Needs Yosys with Verific (`verific -formal` in the scripts).
+
+Run via the wrapper: from the root directory, call `make -C tests staged_sim_and_verif/staged_sim_and_verif`, which calls `staged_sim_and_verif.sh` and exercises all four tasks in `skip_staged_flow.sby`. You may also run each task manually; simply ensure you run the tasks in the correct order shown in the `.sh` file.

tests/staged_sim_and_verif/Req_Ack.sv

@@ -0,0 +1,62 @@
+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
+                reqs_seen = 2'b0;
+                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
+                phase1_reqs_seen: 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
+                phase2_no_new_req: assume(!req);
+        end
+        always @(posedge clk) begin
+                phase2_ack_eventually: cover(ack);
+        end
+
+
+`endif
+
+endmodule

tests/staged_sim_and_verif/skip_staged_flow.sby

@@ -0,0 +1,59 @@
+[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
+
+stage_1_fv:
+read_rtlil design_prep.il
+# This selection computes (all phase-labeled things) - (all phase-1-labeled
+# things) to remove all phase-tagged SVA constructs not intended for phase 1.
+select */c:phase* */c:phase1_* %d
+delete
+
+stage_2_init:
+read_rtlil design_prep.il
+sim -a -w -scope DUT -r trace0.yw
+
+stage_2_fv:
+read_rtlil design_prep.il
+# This selection computes (all phase-labeled things) - (all phase-2-labeled
+# things) to remove all phase-tagged SVA constructs not intended for phase 2.
+select */c:phase* */c:phase2_* %d
+delete
+
+--
+
+[files]
+
+stage_1_init:
+Req_Ack.sv
+
+stage_1_fv:
+skip_staged_flow_stage_1_init/model/design_prep.il
+
+stage_2_init:
+skip_staged_flow_stage_1_init/model/design_prep.il
+skip_staged_flow_stage_1_fv/engine_0/trace0.yw
+
+stage_2_fv:
+skip_staged_flow_stage_2_init/model/design_prep.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,16 @@
+#!/bin/bash
+set -euo pipefail
+
+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