From 81a0af362abfa270b1011d62ff59a5032d86b178 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Tue, 13 Jan 2026 08:12:22 -0800
Subject: [PATCH 01/12] Widen signal

---
 tests/staged_sim_and_verif/Req_Ack.sv | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv
index e1fd0e0..f94b018 100644
--- a/tests/staged_sim_and_verif/Req_Ack.sv
+++ b/tests/staged_sim_and_verif/Req_Ack.sv
@@ -12,8 +12,8 @@ module DUT (
 
         // Deterministic initial state
         initial begin
-                reqs_seen = 2'b0;
-                acks_seen = 2'b0;
+                reqs_seen = 32'b0;
+                acks_seen = 32'b0;
                 cycle_count = 32'b0;
         end
 

From d6252f7ee5bb07cafbe58d1ff78e9aca8b7b19e8 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Tue, 13 Jan 2026 08:17:00 -0800
Subject: [PATCH 02/12] Change comments and labels

---
 tests/staged_sim_and_verif/Req_Ack.sv | 39 +++++++++++++++------------
 1 file changed, 22 insertions(+), 17 deletions(-)

diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv
index f94b018..a0ea09f 100644
--- a/tests/staged_sim_and_verif/Req_Ack.sv
+++ b/tests/staged_sim_and_verif/Req_Ack.sv
@@ -50,26 +50,31 @@ module DUT (
                 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
+        // In phase 2, cover that the first ack arrives within a bounded window
+        // after the first req + another req arrives.
+        phase2_cover_ack_and_new_req: cover property (@(posedge clk)
+                $rose(ack) ##[1:$] (reqs_seen == 3)
         );
-        always @(posedge clk) begin
-                phase2b_assert_ack_stable: assert(acks_seen <= 2);
+
+
+        // In phase 3, assume that there's no more reqs.
+        always @ (posedge clk) begin
+                phase3_shared_no_new_req: assume(!req);
         end
 
+        // In phase 3a, cover the second ack arriving eventually.
+        always @(posedge clk) begin
+                phase3a_cover_ack: cover(ack);
+        end
+
+        // Assert the second ack arrives within a bounded window after beginning
+        // phase 3, and furthermore after that point no further acks arrive.
+        property p_acks_seen_hits_3_and_stays;
+                @(posedge clk) ##[0:8] $rose(acks_seen == 3) ##1 (acks_seen == 3)[*0:$];
+        endproperty
+
+        phase3b_acks_seen_hits_3_and_stays: assert property (p_acks_seen_hits_3_and_stays);
+
 
 `endif
 

From d82ef4daf93a40c2c1568360167b6af52a109509 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Tue, 13 Jan 2026 08:17:17 -0800
Subject: [PATCH 03/12] Update sby file for new stages

---
 .../staged_sim_and_verif/skip_staged_flow.sby | 104 +++++++++++-------
 1 file changed, 63 insertions(+), 41 deletions(-)

diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby
index 12a011e..8db258a 100644
--- a/tests/staged_sim_and_verif/skip_staged_flow.sby
+++ b/tests/staged_sim_and_verif/skip_staged_flow.sby
@@ -1,78 +1,100 @@
 [tasks]
-stage_1_init init
-stage_1_cover cover
-stage_2_init init
-stage_2a_cover cover
-stage_2b_assert assert
+stage_1
+stage_2
+stage_3_init
+stage_3a_cover
+stage_3b_assert
 
 [options]
-init:
-mode prep
-
-cover:
+stage_1:
+mode cover
+
+stage_2:
 mode cover
-depth 40
 skip_prep on
 
-assert:
+stage_3_init:
+mode prep
+skip_prep on
+
+stage_3a_cover:
+mode cover
+skip_prep on
+
+stage_3b_assert:
 mode prove
-depth 40
 skip_prep on
 
 --
 
 [engines]
-init: none
-cover: smtbmc
-assert: smtbmc
+smtbmc
+
+stage_3_init:
+none
+
+--
 
 [script]
-stage_1_init:
+stage_1:
 verific -formal Req_Ack.sv
 hierarchy -top DUT
 prep
 
-stage_1_cover:
-read_rtlil design_prep.il
+# Write checkpoint file.
+write_rtlil stage_1_init.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
+select */c:phase* */c:phase1* %d
 delete
 
-stage_2_init:
-read_rtlil design_prep.il
+stage_2:
+read_rtlil stage_1_init.il
+# Note that, in stage 2, we do not use -noinitstate, as this first simulation
+# begins at t=0. All future calls to sim should include -noinitstate.
 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
+write_rtlil stage_2_init.il
+select */c:phase* */c:phase2* %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
+stage_3_init:
+read_rtlil stage_2_init.il
+
+# Use -noinitstate, as this simulation does not begin at t=0.
+sim -a -w -scope DUT -r trace0.yw -noinitstate
+
+write_rtlil stage_3_init.il
+
+stage_3a_cover:
+read_rtlil stage_3_init.il
+select */c:phase* */c:phase3_shared* */c:phase3a* %u %d
 delete
 
+stage_3b_assert:
+read_rtlil stage_3_init.il
+select */c:phase* */c:phase3_shared_* */c:phase3b* %u %d
+delete
+
+
 --
 
 [files]
 
-stage_1_init:
+stage_1:
 Req_Ack.sv
 
-stage_1_cover:
-skip_staged_flow_stage_1_init/model/design_prep.il
+stage_2:
+skip_staged_flow_stage_1/src/stage_1_init.il
+skip_staged_flow_stage_1/engine_0/trace0.yw
 
-stage_2_init:
-skip_staged_flow_stage_1_init/model/design_prep.il
-skip_staged_flow_stage_1_cover/engine_0/trace0.yw
+stage_3_init:
+skip_staged_flow_stage_2/src/stage_2_init.il
+skip_staged_flow_stage_2/engine_0/trace0.yw
 
-stage_2a_cover:
-skip_staged_flow_stage_2_init/model/design_prep.il
+stage_3a_cover:
+skip_staged_flow_stage_3_init/src/stage_3_init.il
 
-stage_2b_assert:
-skip_staged_flow_stage_2_init/model/design_prep.il
+stage_3b_assert:
+skip_staged_flow_stage_3_init/src/stage_3_init.il

From 9389f3a7d6a903bc0ed970e38c37d4a20dcb8d2c Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Tue, 13 Jan 2026 08:18:54 -0800
Subject: [PATCH 04/12] Update script

---
 tests/staged_sim_and_verif/staged_sim_and_verif.sh | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/tests/staged_sim_and_verif/staged_sim_and_verif.sh b/tests/staged_sim_and_verif/staged_sim_and_verif.sh
index a7426b8..100e98b 100755
--- a/tests/staged_sim_and_verif/staged_sim_and_verif.sh
+++ b/tests/staged_sim_and_verif/staged_sim_and_verif.sh
@@ -7,8 +7,8 @@ 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
+run_task stage_1
+run_task stage_2
+run_task stage_3_init
+run_task stage_3a_cover
+run_task stage_3b_assert

From 022323bd71d6a62683b998acaa0aa8fafa49f64f Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Tue, 13 Jan 2026 09:40:14 -0800
Subject: [PATCH 05/12] Revive an independent prep stage

---
 .../staged_sim_and_verif/skip_staged_flow.sby | 35 ++++++++++++++++---
 .../staged_sim_and_verif.sh                   |  1 +
 2 files changed, 31 insertions(+), 5 deletions(-)

diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby
index 8db258a..613da42 100644
--- a/tests/staged_sim_and_verif/skip_staged_flow.sby
+++ b/tests/staged_sim_and_verif/skip_staged_flow.sby
@@ -1,4 +1,5 @@
 [tasks]
+prep
 stage_1
 stage_2
 stage_3_init
@@ -6,8 +7,12 @@ stage_3a_cover
 stage_3b_assert
 
 [options]
+prep:
+mode prep
+
 stage_1:
 mode cover
+skip_prep on
 
 stage_2:
 mode cover
@@ -30,17 +35,31 @@ skip_prep on
 [engines]
 smtbmc
 
+prep:
+none
+
 stage_3_init:
 none
 
 --
 
 [script]
-stage_1:
+
+# This separate prep step generates model_prep.il, which is our ground-truth
+# design file from which all other checkpoints are derived. It is essential
+# to have at least one prep step in `mode prep`, as we must produce a .il file
+# which has had the SBY-internal prep routine run on it. Any file written
+# in the user-provided script below will represent the state of the design 
+# *before* the SBY prep routine. (Note that the `prep` pass below is *not*
+# the SBY prep routine, but just the Yosys synthesis pass.)
+prep:
 verific -formal Req_Ack.sv
 hierarchy -top DUT
 prep
 
+stage_1:
+read_rtlil design_prep.il
+
 # Write checkpoint file.
 write_rtlil stage_1_init.il
 
@@ -50,12 +69,15 @@ select */c:phase* */c:phase1* %d
 delete
 
 stage_2:
+# Read the stage 1 checkpoint, and then use the stage 1 trace to simulate up
+# to the end of stage 1.
+# Note that, in stage 2, we do not use -noinitstate on sim, as this first 
+# simulation begins at t=0 and thus $initstate cells should be active. All 
+# future calls to sim should include -noinitstate.
 read_rtlil stage_1_init.il
-# Note that, in stage 2, we do not use -noinitstate, as this first simulation
-# begins at t=0. All future calls to sim should include -noinitstate.
 sim -a -w -scope DUT -r trace0.yw
-
 write_rtlil stage_2_init.il
+
 select */c:phase* */c:phase2* %d
 delete
 
@@ -82,9 +104,12 @@ delete
 
 [files]
 
-stage_1:
+prep:
 Req_Ack.sv
 
+stage_1:
+skip_staged_flow_prep/model/design_prep.il
+
 stage_2:
 skip_staged_flow_stage_1/src/stage_1_init.il
 skip_staged_flow_stage_1/engine_0/trace0.yw
diff --git a/tests/staged_sim_and_verif/staged_sim_and_verif.sh b/tests/staged_sim_and_verif/staged_sim_and_verif.sh
index 100e98b..720865b 100755
--- a/tests/staged_sim_and_verif/staged_sim_and_verif.sh
+++ b/tests/staged_sim_and_verif/staged_sim_and_verif.sh
@@ -7,6 +7,7 @@ run_task() {
     python3 "$SBY_MAIN" -f "$FLOW_FILE" "$1"
 }
 
+run_task prep
 run_task stage_1
 run_task stage_2
 run_task stage_3_init

From b23e01c2a13f67d9bd13c8ce70be8ad61f928f37 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Tue, 13 Jan 2026 09:53:09 -0800
Subject: [PATCH 06/12] Fix comment

---
 tests/staged_sim_and_verif/Req_Ack.sv | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv
index a0ea09f..52e38aa 100644
--- a/tests/staged_sim_and_verif/Req_Ack.sv
+++ b/tests/staged_sim_and_verif/Req_Ack.sv
@@ -67,7 +67,7 @@ module DUT (
                 phase3a_cover_ack: cover(ack);
         end
 
-        // Assert the second ack arrives within a bounded window after beginning
+        // Assert the third ack arrives within a bounded window after beginning
         // phase 3, and furthermore after that point no further acks arrive.
         property p_acks_seen_hits_3_and_stays;
                 @(posedge clk) ##[0:8] $rose(acks_seen == 3) ##1 (acks_seen == 3)[*0:$];

From fcba8d378054fb62390f34f4971e119431f9c2d6 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Tue, 13 Jan 2026 09:53:16 -0800
Subject: [PATCH 07/12] Change select to match other select

---
 tests/staged_sim_and_verif/skip_staged_flow.sby | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby
index 613da42..026fc22 100644
--- a/tests/staged_sim_and_verif/skip_staged_flow.sby
+++ b/tests/staged_sim_and_verif/skip_staged_flow.sby
@@ -96,7 +96,7 @@ delete
 
 stage_3b_assert:
 read_rtlil stage_3_init.il
-select */c:phase* */c:phase3_shared_* */c:phase3b* %u %d
+select */c:phase* */c:phase3_shared* */c:phase3b* %u %d
 delete
 
 

From 5e6e984a67cb48f0c79a3e0ec9e0fc7b63c34a5f Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Wed, 21 Jan 2026 08:20:00 -0800
Subject: [PATCH 08/12] Fix bitwidths

---
 tests/staged_sim_and_verif/Req_Ack.sv | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv
index 52e38aa..c6bd496 100644
--- a/tests/staged_sim_and_verif/Req_Ack.sv
+++ b/tests/staged_sim_and_verif/Req_Ack.sv
@@ -6,8 +6,8 @@ module DUT (
 
 `ifdef FORMAL
 
-        logic [1:0] reqs_seen;
-        logic [1:0] acks_seen;
+        logic [31:0] reqs_seen;
+        logic [31:0] acks_seen;
         logic [31:0] cycle_count;
 
         // Deterministic initial state

From 501a054731512acba1826da87961958120c83718 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Wed, 21 Jan 2026 08:20:24 -0800
Subject: [PATCH 09/12] Change stage 3 assertion

---
 tests/staged_sim_and_verif/Req_Ack.sv | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv
index c6bd496..b18e060 100644
--- a/tests/staged_sim_and_verif/Req_Ack.sv
+++ b/tests/staged_sim_and_verif/Req_Ack.sv
@@ -67,14 +67,10 @@ module DUT (
                 phase3a_cover_ack: cover(ack);
         end
 
-        // Assert the third ack arrives within a bounded window after beginning
-        // phase 3, and furthermore after that point no further acks arrive.
-        property p_acks_seen_hits_3_and_stays;
-                @(posedge clk) ##[0:8] $rose(acks_seen == 3) ##1 (acks_seen == 3)[*0:$];
-        endproperty
-
-        phase3b_acks_seen_hits_3_and_stays: assert property (p_acks_seen_hits_3_and_stays);
-
+        // In phase 3b, assert that once we've seen 3 acks, we stay at 3 acks.
+        phase3b_acks_remains_3: assert property (
+                @(posedge clk) $rose(acks_seen == 3) |-> (acks_seen == 3)[*1:$]
+        );
 
 `endif
 

From b66bbe4503dc5a5d5459ea604f0ecffe0056ce97 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Wed, 21 Jan 2026 08:22:19 -0800
Subject: [PATCH 10/12] Use tags

---
 .../staged_sim_and_verif/skip_staged_flow.sby | 23 ++++++++-----------
 1 file changed, 10 insertions(+), 13 deletions(-)

diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby
index 026fc22..a16bfe1 100644
--- a/tests/staged_sim_and_verif/skip_staged_flow.sby
+++ b/tests/staged_sim_and_verif/skip_staged_flow.sby
@@ -1,20 +1,16 @@
 [tasks]
 prep
-stage_1
-stage_2
+stage_1 cover
+stage_2 cover
 stage_3_init
-stage_3a_cover
+stage_3a_cover cover
 stage_3b_assert
 
 [options]
 prep:
 mode prep
 
-stage_1:
-mode cover
-skip_prep on
-
-stage_2:
+cover:
 mode cover
 skip_prep on
 
@@ -22,10 +18,6 @@ stage_3_init:
 mode prep
 skip_prep on
 
-stage_3a_cover:
-mode cover
-skip_prep on
-
 stage_3b_assert:
 mode prove
 skip_prep on
@@ -33,14 +25,19 @@ skip_prep on
 --
 
 [engines]
-smtbmc
 
 prep:
 none
 
+cover:
+smtbmc
+
 stage_3_init:
 none
 
+stage_3b_assert:
+smtbmc
+
 --
 
 [script]

From e89f71b3cbc8b201fa5d8aaca2dd9b406c9fe984 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Wed, 21 Jan 2026 08:30:03 -0800
Subject: [PATCH 11/12] phase->stage

---
 tests/staged_sim_and_verif/Req_Ack.sv          | 18 +++++++++---------
 .../staged_sim_and_verif/skip_staged_flow.sby  | 12 ++++++------
 2 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv
index b18e060..145dd97 100644
--- a/tests/staged_sim_and_verif/Req_Ack.sv
+++ b/tests/staged_sim_and_verif/Req_Ack.sv
@@ -47,28 +47,28 @@ 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, cover that the first ack arrives within a bounded window
+        // In stage 2, cover that the first ack arrives within a bounded window
         // after the first req + another req arrives.
-        phase2_cover_ack_and_new_req: cover property (@(posedge clk)
+        stage2_cover_ack_and_new_req: cover property (@(posedge clk)
                 $rose(ack) ##[1:$] (reqs_seen == 3)
         );
 
 
-        // In phase 3, assume that there's no more reqs.
+        // In stage 3, assume that there's no more reqs.
         always @ (posedge clk) begin
-                phase3_shared_no_new_req: assume(!req);
+                stage3_shared_no_new_req: assume(!req);
         end
 
-        // In phase 3a, cover the second ack arriving eventually.
+        // In stage 3a, cover the second ack arriving eventually.
         always @(posedge clk) begin
-                phase3a_cover_ack: cover(ack);
+                stage3a_cover_ack: cover(ack);
         end
 
-        // In phase 3b, assert that once we've seen 3 acks, we stay at 3 acks.
-        phase3b_acks_remains_3: assert property (
+        // 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:$]
         );
 
diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby
index a16bfe1..41b575a 100644
--- a/tests/staged_sim_and_verif/skip_staged_flow.sby
+++ b/tests/staged_sim_and_verif/skip_staged_flow.sby
@@ -60,9 +60,9 @@ read_rtlil design_prep.il
 # Write checkpoint file.
 write_rtlil stage_1_init.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
+# This selection computes (all stage-labeled things) - (all stage-1-labeled
+# things) to remove all stage-tagged SVA constructs not intended for stage 1.
+select */c:stage* */c:stage1* %d
 delete
 
 stage_2:
@@ -75,7 +75,7 @@ read_rtlil stage_1_init.il
 sim -a -w -scope DUT -r trace0.yw
 write_rtlil stage_2_init.il
 
-select */c:phase* */c:phase2* %d
+select */c:stage* */c:stage2* %d
 delete
 
 stage_3_init:
@@ -88,12 +88,12 @@ write_rtlil stage_3_init.il
 
 stage_3a_cover:
 read_rtlil stage_3_init.il
-select */c:phase* */c:phase3_shared* */c:phase3a* %u %d
+select */c:stage* */c:stage3_shared* */c:stage3a* %u %d
 delete
 
 stage_3b_assert:
 read_rtlil stage_3_init.il
-select */c:phase* */c:phase3_shared* */c:phase3b* %u %d
+select */c:stage* */c:stage3_shared* */c:stage3b* %u %d
 delete
 
 

From 551d8df2a913cf59b2b5aa8514560aceb78cc1a6 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Wed, 18 Feb 2026 08:20:51 -0800
Subject: [PATCH 12/12] Remove comments and point to appnote

Instead of duplicating editorial comments in the test, we should just
point to the appnote where the comments are already made in a more
substantive way.
---
 tests/staged_sim_and_verif/README.md            |  3 +++
 tests/staged_sim_and_verif/skip_staged_flow.sby | 16 ----------------
 2 files changed, 3 insertions(+), 16 deletions(-)

diff --git a/tests/staged_sim_and_verif/README.md b/tests/staged_sim_and_verif/README.md
index 6cb81e8..e47f8a9 100644
--- a/tests/staged_sim_and_verif/README.md
+++ b/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.
diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby
index 41b575a..da94b05 100644
--- a/tests/staged_sim_and_verif/skip_staged_flow.sby
+++ b/tests/staged_sim_and_verif/skip_staged_flow.sby
@@ -42,13 +42,6 @@ smtbmc
 
 [script]
 
-# This separate prep step generates model_prep.il, which is our ground-truth
-# design file from which all other checkpoints are derived. It is essential
-# to have at least one prep step in `mode prep`, as we must produce a .il file
-# which has had the SBY-internal prep routine run on it. Any file written
-# in the user-provided script below will represent the state of the design 
-# *before* the SBY prep routine. (Note that the `prep` pass below is *not*
-# the SBY prep routine, but just the Yosys synthesis pass.)
 prep:
 verific -formal Req_Ack.sv
 hierarchy -top DUT
@@ -57,20 +50,12 @@ prep
 stage_1:
 read_rtlil design_prep.il
 
-# Write checkpoint file.
 write_rtlil stage_1_init.il
 
-# This selection computes (all stage-labeled things) - (all stage-1-labeled
-# things) to remove all stage-tagged SVA constructs not intended for stage 1.
 select */c:stage* */c:stage1* %d
 delete
 
 stage_2:
-# Read the stage 1 checkpoint, and then use the stage 1 trace to simulate up
-# to the end of stage 1.
-# Note that, in stage 2, we do not use -noinitstate on sim, as this first 
-# simulation begins at t=0 and thus $initstate cells should be active. All 
-# future calls to sim should include -noinitstate.
 read_rtlil stage_1_init.il
 sim -a -w -scope DUT -r trace0.yw
 write_rtlil stage_2_init.il
@@ -81,7 +66,6 @@ delete
 stage_3_init:
 read_rtlil stage_2_init.il
 
-# Use -noinitstate, as this simulation does not begin at t=0.
 sim -a -w -scope DUT -r trace0.yw -noinitstate
 
 write_rtlil stage_3_init.il