Merge pull request #347 from YosysHQ/gus/staged-sim-and-verif-test

Staged verification test

tests/staged_sim_and_verif/README.md

@@ -0,0 +1,14 @@
+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 2A (cover branch): replay the witness with `sim -w` to bake state, then run another cover that requires the ack.
+- Stage 2B (assert branch): replay the same baked state and assert there is at most one further ack after the second req.
+- Uses labeled properties (`phase1_*`, `phase2_shared_*`, `phase2a_*`, `phase2b_*`) 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 five 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.
+
+Design notes
+- Two-phase flow with a branch in phase 2: phase 1 reaches “two reqs seen” and emits a witness; phase 2 replays that witness with `sim -w` and then splits into a cover branch (ack) and an assert branch (single remaining ack). This covers both SCY-like sequential covers and an assertion path that goes beyond SCY’s current cover-only sequencing.
+- Phase separation uses labeled properties (`phase1_*`, `phase2_shared_*`, `phase2a_*`, `phase2b_*`), matching the SCY approach. Each branch prunes with `select */c:phase* ... %u %d` to keep only the shared + branch-specific labels for that task.
+- Tooling: needs Yosys with Verific (`verific -formal`) for SVA parsing. The minimal `staged_sim_and_verif.sby` exists just so the test harness discovers the Verific requirement.
+- Harness glue: the current make harness can’t express “run these SBY tasks sequentially from one .sby”; it spins each task as an independent target. We keep the multi-task config in `skip_staged_flow.sby` (prefixed so collect skips it) and use `staged_sim_and_verif.sh` to drive the five tasks in order. The tiny `staged_sim_and_verif.sby` is only there so collect/required_tools see the test and recognize that verific is required. The `.sh` is what actually runs and enforces ordering.

tests/staged_sim_and_verif/Req_Ack.sv

@@ -0,0 +1,76 @@
+module DUT (
+        input  logic clk,
+        output logic req,
+        output logic ack
+);
+
+`ifdef FORMAL
+
+        logic [1:0] reqs_seen;
+        logic [1:0] acks_seen;
+        logic [31:0] cycle_count;
+
+        // Deterministic initial state
+        initial begin
+                reqs_seen = 2'b0;
+                acks_seen = 2'b0;
+                cycle_count = 32'b0;
+        end
+
+        always @ (posedge clk) begin
+                if (req) reqs_seen <= reqs_seen + 1;
+                if (ack && !$past(ack)) acks_seen <= acks_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; cover that an ack will
+        // eventually come for the second req, and separately prove bounded
+        // counts for reqs/acks.
+        always @ (posedge clk) begin
+                phase2_shared_no_new_req: assume(!req);
+        end
+
+        always @(posedge clk) begin
+                phase2a_cover_ack: cover(ack);
+        end
+
+        // Assert the second ack arrives within a bounded window after the second
+        // request, and also that ack count never exceeds the expected two.
+        phase2b_assert_ack_reaches_two: assert property (@(posedge clk)
+                $rose(reqs_seen == 2) |-> ##[1:8] acks_seen == 2
+        );
+        always @(posedge clk) begin
+                phase2b_assert_ack_stable: assert(acks_seen <= 2);
+        end
+
+
+`endif
+
+endmodule

tests/staged_sim_and_verif/skip_staged_flow.sby

@@ -0,0 +1,78 @@
+[tasks]
+stage_1_init init
+stage_1_cover cover
+stage_2_init init
+stage_2a_cover cover
+stage_2b_assert assert
+
+[options]
+init:
+mode prep
+
+cover:
+mode cover
+depth 40
+skip_prep on
+
+assert:
+mode prove
+depth 40
+skip_prep on
+
+--
+
+[engines]
+init: none
+cover: smtbmc
+assert: smtbmc
+
+[script]
+stage_1_init:
+verific -formal Req_Ack.sv
+hierarchy -top DUT
+prep
+
+stage_1_cover:
+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_2a_cover:
+read_rtlil design_prep.il
+# This selection computes (all phase-labeled things) - (phase2 shared + phase2a)
+# to remove all phase-tagged SVA constructs not intended for this branch.
+select */c:phase* */c:phase2_shared_* */c:phase2a_* %u %d
+delete
+
+stage_2b_assert:
+read_rtlil design_prep.il
+# This selection computes (all phase-labeled things) - (phase2 shared + phase2b)
+# to remove all phase-tagged SVA constructs not intended for this branch.
+select */c:phase* */c:phase2_shared_* */c:phase2b_* %u %d
+delete
+
+--
+
+[files]
+
+stage_1_init:
+Req_Ack.sv
+
+stage_1_cover:
+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_cover/engine_0/trace0.yw
+
+stage_2a_cover:
+skip_staged_flow_stage_2_init/model/design_prep.il
+
+stage_2b_assert:
+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,14 @@
+#!/bin/bash
+set -euo pipefail
+
+FLOW_FILE="skip_staged_flow.sby"
+
+run_task() {
+    python3 "$SBY_MAIN" -f "$FLOW_FILE" "$1"
+}
+
+run_task stage_1_init
+run_task stage_1_cover
+run_task stage_2_init
+run_task stage_2a_cover
+run_task stage_2b_assert