Merge pull request #349 from YosysHQ/gus/update-sim-and-verif-test

Update staged verification test

tests/staged_sim_and_verif/README.md

@@ -1,4 +1,7 @@
 Staged simulation + verification example demonstrating staged verification using simulation and writeback via `sim -w` pass.
+
+This test mirrors what is described in <https://yosyshq.readthedocs.io/projects/ap130/en/latest/>, and should be kept up to date with that appnote.
+
 - 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.

tests/staged_sim_and_verif/Req_Ack.sv

@@ -6,14 +6,14 @@ module DUT (
 
 `ifdef FORMAL
 
-        logic [1:0] reqs_seen;
+        logic [31:0] reqs_seen;
-        logic [1:0] acks_seen;
+        logic [31:0] acks_seen;
         logic [31:0] cycle_count;
 
         // Deterministic initial state
         initial begin
-                reqs_seen = 2'b0;
+                reqs_seen = 32'b0;
-                acks_seen = 2'b0;
+                acks_seen = 32'b0;
                 cycle_count = 32'b0;
         end
 
@@ -47,29 +47,30 @@ module DUT (
         // 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);
+                stage1_reqs_seen: cover(reqs_seen == 2);
         end
 
-        // In phase 2, assume that there's no more reqs; cover that an ack will
+        // In stage 2, cover that the first ack arrives within a bounded window
-        // eventually come for the second req, and separately prove bounded
+        // after the first req + another req arrives.
-        // counts for reqs/acks.
+        stage2_cover_ack_and_new_req: cover property (@(posedge clk)
-        always @ (posedge clk) begin
+                $rose(ack) ##[1:$] (reqs_seen == 3)
-                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);
+
+        // In stage 3, assume that there's no more reqs.
+        always @ (posedge clk) begin
+                stage3_shared_no_new_req: assume(!req);
         end
 
+        // In stage 3a, cover the second ack arriving eventually.
+        always @(posedge clk) begin
+                stage3a_cover_ack: cover(ack);
+        end
+
+        // In stage 3b, assert that once we've seen 3 acks, we stay at 3 acks.
+        stage3b_acks_remains_3: assert property (
+                @(posedge clk) $rose(acks_seen == 3) |-> (acks_seen == 3)[*1:$]
+        );
 
 `endif
 

tests/staged_sim_and_verif/skip_staged_flow.sby

@@ -1,78 +1,106 @@
 [tasks]
-stage_1_init init
+prep
-stage_1_cover cover
+stage_1 cover
-stage_2_init init
+stage_2 cover
-stage_2a_cover cover
+stage_3_init
-stage_2b_assert assert
+stage_3a_cover cover
+stage_3b_assert
 
 [options]
-init:
+prep:
 mode prep
 
 cover:
 mode cover
-depth 40
 skip_prep on
 
-assert:
+stage_3_init:
+mode prep
+skip_prep on
+
+stage_3b_assert:
 mode prove
-depth 40
 skip_prep on
 
 --
 
 [engines]
-init: none
+
-cover: smtbmc
+prep:
-assert: smtbmc
+none
+
+cover:
+smtbmc
+
+stage_3_init:
+none
+
+stage_3b_assert:
+smtbmc
+
+--
 
 [script]
-stage_1_init:
+
+prep:
 verific -formal Req_Ack.sv
 hierarchy -top DUT
 prep
 
-stage_1_cover:
+stage_1:
 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.
+write_rtlil stage_1_init.il
-select */c:phase* */c:phase1_* %d
+
+select */c:stage* */c:stage1* %d
 delete
 
-stage_2_init:
+stage_2:
-read_rtlil design_prep.il
+read_rtlil stage_1_init.il
 sim -a -w -scope DUT -r trace0.yw
+write_rtlil stage_2_init.il
 
-stage_2a_cover:
+select */c:stage* */c:stage2* %d
-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:
+stage_3_init:
-read_rtlil design_prep.il
+read_rtlil stage_2_init.il
-# This selection computes (all phase-labeled things) - (phase2 shared + phase2b)
+
-# to remove all phase-tagged SVA constructs not intended for this branch.
+sim -a -w -scope DUT -r trace0.yw -noinitstate
-select */c:phase* */c:phase2_shared_* */c:phase2b_* %u %d
+
+write_rtlil stage_3_init.il
+
+stage_3a_cover:
+read_rtlil stage_3_init.il
+select */c:stage* */c:stage3_shared* */c:stage3a* %u %d
 delete
 
+stage_3b_assert:
+read_rtlil stage_3_init.il
+select */c:stage* */c:stage3_shared* */c:stage3b* %u %d
+delete
+
+
 --
 
 [files]
 
-stage_1_init:
+prep:
 Req_Ack.sv
 
-stage_1_cover:
+stage_1:
-skip_staged_flow_stage_1_init/model/design_prep.il
+skip_staged_flow_prep/model/design_prep.il
 
-stage_2_init:
+stage_2:
-skip_staged_flow_stage_1_init/model/design_prep.il
+skip_staged_flow_stage_1/src/stage_1_init.il
-skip_staged_flow_stage_1_cover/engine_0/trace0.yw
+skip_staged_flow_stage_1/engine_0/trace0.yw
 
-stage_2a_cover:
+stage_3_init:
-skip_staged_flow_stage_2_init/model/design_prep.il
+skip_staged_flow_stage_2/src/stage_2_init.il
+skip_staged_flow_stage_2/engine_0/trace0.yw
 
-stage_2b_assert:
+stage_3a_cover:
-skip_staged_flow_stage_2_init/model/design_prep.il
+skip_staged_flow_stage_3_init/src/stage_3_init.il
+
+stage_3b_assert:
+skip_staged_flow_stage_3_init/src/stage_3_init.il

tests/staged_sim_and_verif/staged_sim_and_verif.sh

@@ -7,8 +7,9 @@ run_task() {
     python3 "$SBY_MAIN" -f "$FLOW_FILE" "$1"
 }
 
-run_task stage_1_init
+run_task prep
-run_task stage_1_cover
+run_task stage_1
-run_task stage_2_init
+run_task stage_2
-run_task stage_2a_cover
+run_task stage_3_init
-run_task stage_2b_assert
+run_task stage_3a_cover
+run_task stage_3b_assert