From ad93d4fc4f74b91e6827c2c9faeadc177184a3b6 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 9 Dec 2025 11:17:33 -0800 Subject: [PATCH 01/22] Add initial test impl --- tests/staged_sim_and_verif/Req_Ack.sv | 65 +++++++++++++++++++ .../staged_sim_and_verif/skip_staged_flow.sby | 64 ++++++++++++++++++ .../staged_sim_and_verif.sby | 14 ++++ .../staged_sim_and_verif.sh | 19 ++++++ 4 files changed, 162 insertions(+) create mode 100644 tests/staged_sim_and_verif/Req_Ack.sv create mode 100644 tests/staged_sim_and_verif/skip_staged_flow.sby create mode 100644 tests/staged_sim_and_verif/staged_sim_and_verif.sby create mode 100755 tests/staged_sim_and_verif/staged_sim_and_verif.sh diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv new file mode 100644 index 0000000..51f3ece --- /dev/null +++ b/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 diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby new file mode 100644 index 0000000..6625d3c --- /dev/null +++ b/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 diff --git a/tests/staged_sim_and_verif/staged_sim_and_verif.sby b/tests/staged_sim_and_verif/staged_sim_and_verif.sby new file mode 100644 index 0000000..76d9896 --- /dev/null +++ b/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 diff --git a/tests/staged_sim_and_verif/staged_sim_and_verif.sh b/tests/staged_sim_and_verif/staged_sim_and_verif.sh new file mode 100755 index 0000000..1ae5e81 --- /dev/null +++ b/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 From 4be8853a32c8d7ab751b37de878f6d70d479ca99 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 9 Dec 2025 11:20:27 -0800 Subject: [PATCH 02/22] Add readme --- tests/staged_sim_and_verif/README.md | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 tests/staged_sim_and_verif/README.md diff --git a/tests/staged_sim_and_verif/README.md b/tests/staged_sim_and_verif/README.md new file mode 100644 index 0000000..466c0a0 --- /dev/null +++ b/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: `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`).*** From a0ab7de28c9247db8cbcda0b5c9ec52f050ccb87 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 15 Dec 2025 12:27:24 -0800 Subject: [PATCH 03/22] Fix readme --- tests/staged_sim_and_verif/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/staged_sim_and_verif/README.md b/tests/staged_sim_and_verif/README.md index 466c0a0..8f9745b 100644 --- a/tests/staged_sim_and_verif/README.md +++ b/tests/staged_sim_and_verif/README.md @@ -4,4 +4,4 @@ Staged simulation + verification example demonstrating staged verification using - 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: `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`).*** +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`. From 358ccf3ab64803fc99ab60430c171a92f3ab9a9b Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 15 Dec 2025 12:30:06 -0800 Subject: [PATCH 04/22] Reindent --- tests/staged_sim_and_verif/Req_Ack.sv | 94 +++++++++++++-------------- 1 file changed, 47 insertions(+), 47 deletions(-) diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv index 51f3ece..b764540 100644 --- a/tests/staged_sim_and_verif/Req_Ack.sv +++ b/tests/staged_sim_and_verif/Req_Ack.sv @@ -1,63 +1,63 @@ module DUT ( - input logic clk, - output logic req, - output logic ack + input logic clk, + output logic req, + output logic ack ); `ifdef FORMAL - logic [1:0] reqs_seen; - logic [31:0] cycle_count; + 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 + // Deterministic initial state + initial begin + 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 + 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 - ); + // 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]) - ); + // 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 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 - ); + // 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 + // 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 + // 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 From 1ee552a50265a6f50c9c4ff583301045a08dabb6 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 15 Dec 2025 12:41:38 -0800 Subject: [PATCH 05/22] Syntax --- 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 b764540..b708caa 100644 --- a/tests/staged_sim_and_verif/Req_Ack.sv +++ b/tests/staged_sim_and_verif/Req_Ack.sv @@ -11,7 +11,7 @@ module DUT ( // Deterministic initial state initial begin - reqs_seen = 2'b00; + reqs_seen = 2'b0; cycle_count = 32'b0; end From 9779436d0bebe2e944eeaf42c9b81d0918597aaa Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 15 Dec 2025 12:41:47 -0800 Subject: [PATCH 06/22] Simplify script by relying on sby's prep routine --- tests/staged_sim_and_verif/skip_staged_flow.sby | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby index 6625d3c..505115c 100644 --- a/tests/staged_sim_and_verif/skip_staged_flow.sby +++ b/tests/staged_sim_and_verif/skip_staged_flow.sby @@ -22,25 +22,20 @@ fv: smtbmc 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 +read_rtlil design_prep.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 +read_rtlil design_prep.il sim -a -w -scope DUT -r trace0.yw -write_rtlil stage_2_init.il stage_2_fv: -read_rtlil stage_2_init.il +read_rtlil design_prep.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 @@ -54,11 +49,11 @@ stage_1_init: Req_Ack.sv stage_1_fv: -skip_staged_flow_stage_1_init/src/stage_1_init.il +skip_staged_flow_stage_1_init/model/design_prep.il stage_2_init: -skip_staged_flow_stage_1_init/src/stage_1_init.il +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/src/stage_2_init.il +skip_staged_flow_stage_2_init/model/design_prep.il From 8274979147d3d34d0690b8622191a285e13ac3bf Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 15 Dec 2025 12:47:36 -0800 Subject: [PATCH 07/22] Update readme --- tests/staged_sim_and_verif/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/staged_sim_and_verif/README.md b/tests/staged_sim_and_verif/README.md index 8f9745b..fe264b5 100644 --- a/tests/staged_sim_and_verif/README.md +++ b/tests/staged_sim_and_verif/README.md @@ -4,4 +4,4 @@ Staged simulation + verification example demonstrating staged verification using - 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`. +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. From 2b38c31936dfe5d51f8a5836a8440bde62c39fb6 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 15 Dec 2025 13:00:58 -0800 Subject: [PATCH 08/22] Rework file based on new understanding of make --- .../staged_sim_and_verif/skip_staged_flow.sby | 59 ------------------- .../staged_sim_and_verif.sby | 53 +++++++++++++++-- .../staged_sim_and_verif.sh | 4 +- 3 files changed, 51 insertions(+), 65 deletions(-) delete mode 100644 tests/staged_sim_and_verif/skip_staged_flow.sby diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby deleted file mode 100644 index 505115c..0000000 --- a/tests/staged_sim_and_verif/skip_staged_flow.sby +++ /dev/null @@ -1,59 +0,0 @@ -[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 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 design_prep.il -sim -a -w -scope DUT -r trace0.yw - -stage_2_fv: -read_rtlil design_prep.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/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 diff --git a/tests/staged_sim_and_verif/staged_sim_and_verif.sby b/tests/staged_sim_and_verif/staged_sim_and_verif.sby index 76d9896..1b3c48d 100644 --- a/tests/staged_sim_and_verif/staged_sim_and_verif.sby +++ b/tests/staged_sim_and_verif/staged_sim_and_verif.sby @@ -1,14 +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 1 +depth 40 + +-- [engines] -smtbmc +init: none +fv: smtbmc [script] -# Minimal job so dumptaskinfo picks up the tools this flow requires. +stage_1_init: verific -formal Req_Ack.sv -prep -top DUT +hierarchy -top DUT + +stage_1_fv: +read_rtlil design_prep.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 design_prep.il +sim -a -w -scope DUT -r trace0.yw + +stage_2_fv: +read_rtlil design_prep.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: +staged_sim_and_verif_stage_1_init/model/design_prep.il + +stage_2_init: +staged_sim_and_verif_stage_1_init/model/design_prep.il +staged_sim_and_verif_stage_1_fv/engine_0/trace0.yw + +stage_2_fv: +staged_sim_and_verif_stage_2_init/model/design_prep.il 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 1ae5e81..a83b62e 100755 --- a/tests/staged_sim_and_verif/staged_sim_and_verif.sh +++ b/tests/staged_sim_and_verif/staged_sim_and_verif.sh @@ -4,10 +4,10 @@ set -euo pipefail SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" cd "$SCRIPT_DIR" -FLOW_FILE="skip_staged_flow.sby" +FLOW_FILE="staged_sim_and_verif.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 +rm -rf staged_sim_and_verif_stage_1_init staged_sim_and_verif_stage_1_fv staged_sim_and_verif_stage_2_init staged_sim_and_verif_stage_2_fv run_task() { python3 "$SBY_MAIN" -f "$FLOW_FILE" "$1" From f9bee0464b9c55bbeae8b0fe29032e80475f7b3e Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 15 Dec 2025 13:04:25 -0800 Subject: [PATCH 09/22] Get rid of unnecessary file --- .../staged_sim_and_verif.sh | 19 ------------------- 1 file changed, 19 deletions(-) delete mode 100755 tests/staged_sim_and_verif/staged_sim_and_verif.sh diff --git a/tests/staged_sim_and_verif/staged_sim_and_verif.sh b/tests/staged_sim_and_verif/staged_sim_and_verif.sh deleted file mode 100755 index a83b62e..0000000 --- a/tests/staged_sim_and_verif/staged_sim_and_verif.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/bin/bash -set -euo pipefail - -SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" -cd "$SCRIPT_DIR" - -FLOW_FILE="staged_sim_and_verif.sby" - -# Clean previous runs so we always exercise the full staged flow. -rm -rf staged_sim_and_verif_stage_1_init staged_sim_and_verif_stage_1_fv staged_sim_and_verif_stage_2_init staged_sim_and_verif_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 From 36fcd8fbc873df402721383478c183e28b9af617 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 15 Dec 2025 13:20:28 -0800 Subject: [PATCH 10/22] Revert "Get rid of unnecessary file" This reverts commit f9bee0464b9c55bbeae8b0fe29032e80475f7b3e. --- .../staged_sim_and_verif.sh | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100755 tests/staged_sim_and_verif/staged_sim_and_verif.sh diff --git a/tests/staged_sim_and_verif/staged_sim_and_verif.sh b/tests/staged_sim_and_verif/staged_sim_and_verif.sh new file mode 100755 index 0000000..a83b62e --- /dev/null +++ b/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="staged_sim_and_verif.sby" + +# Clean previous runs so we always exercise the full staged flow. +rm -rf staged_sim_and_verif_stage_1_init staged_sim_and_verif_stage_1_fv staged_sim_and_verif_stage_2_init staged_sim_and_verif_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 From 07669fde927d271341b7bdd2eec2f4e0546783e0 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 15 Dec 2025 13:20:32 -0800 Subject: [PATCH 11/22] Revert "Rework file based on new understanding of make" This reverts commit 2b38c31936dfe5d51f8a5836a8440bde62c39fb6. --- .../staged_sim_and_verif/skip_staged_flow.sby | 59 +++++++++++++++++++ .../staged_sim_and_verif.sby | 53 ++--------------- .../staged_sim_and_verif.sh | 4 +- 3 files changed, 65 insertions(+), 51 deletions(-) create mode 100644 tests/staged_sim_and_verif/skip_staged_flow.sby diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby new file mode 100644 index 0000000..505115c --- /dev/null +++ b/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 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 design_prep.il +sim -a -w -scope DUT -r trace0.yw + +stage_2_fv: +read_rtlil design_prep.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/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 diff --git a/tests/staged_sim_and_verif/staged_sim_and_verif.sby b/tests/staged_sim_and_verif/staged_sim_and_verif.sby index 1b3c48d..76d9896 100644 --- a/tests/staged_sim_and_verif/staged_sim_and_verif.sby +++ b/tests/staged_sim_and_verif/staged_sim_and_verif.sby @@ -1,59 +1,14 @@ -[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 - --- +depth 1 [engines] -init: none -fv: smtbmc +smtbmc [script] -stage_1_init: +# Minimal job so dumptaskinfo picks up the tools this flow requires. verific -formal Req_Ack.sv -hierarchy -top DUT - -stage_1_fv: -read_rtlil design_prep.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 design_prep.il -sim -a -w -scope DUT -r trace0.yw - -stage_2_fv: -read_rtlil design_prep.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 - --- +prep -top DUT [files] - -stage_1_init: Req_Ack.sv - -stage_1_fv: -staged_sim_and_verif_stage_1_init/model/design_prep.il - -stage_2_init: -staged_sim_and_verif_stage_1_init/model/design_prep.il -staged_sim_and_verif_stage_1_fv/engine_0/trace0.yw - -stage_2_fv: -staged_sim_and_verif_stage_2_init/model/design_prep.il 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 a83b62e..1ae5e81 100755 --- a/tests/staged_sim_and_verif/staged_sim_and_verif.sh +++ b/tests/staged_sim_and_verif/staged_sim_and_verif.sh @@ -4,10 +4,10 @@ set -euo pipefail SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" cd "$SCRIPT_DIR" -FLOW_FILE="staged_sim_and_verif.sby" +FLOW_FILE="skip_staged_flow.sby" # Clean previous runs so we always exercise the full staged flow. -rm -rf staged_sim_and_verif_stage_1_init staged_sim_and_verif_stage_1_fv staged_sim_and_verif_stage_2_init staged_sim_and_verif_stage_2_fv +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" From 7c66b2d132c2550926318a32c719f8b628206697 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 15 Dec 2025 13:24:13 -0800 Subject: [PATCH 12/22] Remove redundant cd --- tests/staged_sim_and_verif/staged_sim_and_verif.sh | 3 --- 1 file changed, 3 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 1ae5e81..7cb867e 100755 --- a/tests/staged_sim_and_verif/staged_sim_and_verif.sh +++ b/tests/staged_sim_and_verif/staged_sim_and_verif.sh @@ -1,9 +1,6 @@ #!/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. From e904e88fc9716a589cca880c1feb5b105c2ee7d3 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 15 Dec 2025 17:36:36 -0800 Subject: [PATCH 13/22] Use labels to be more like SCY --- tests/staged_sim_and_verif/Req_Ack.sv | 9 +++------ tests/staged_sim_and_verif/skip_staged_flow.sby | 12 ++++++------ 2 files changed, 9 insertions(+), 12 deletions(-) diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv index b708caa..7886261 100644 --- a/tests/staged_sim_and_verif/Req_Ack.sv +++ b/tests/staged_sim_and_verif/Req_Ack.sv @@ -44,19 +44,16 @@ module DUT ( // 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); + 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 - (* phase = "2" *) - assume(!req); + phase2_no_new_req: assume(!req); end always @(posedge clk) begin - (* phase = "2" *) - cover(ack); + phase2_ack_eventually: cover(ack); end diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby index 505115c..f55a331 100644 --- a/tests/staged_sim_and_verif/skip_staged_flow.sby +++ b/tests/staged_sim_and_verif/skip_staged_flow.sby @@ -25,9 +25,9 @@ hierarchy -top DUT stage_1_fv: read_rtlil design_prep.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 +# 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: @@ -36,9 +36,9 @@ sim -a -w -scope DUT -r trace0.yw stage_2_fv: read_rtlil design_prep.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 +# 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 -- From 01f5c10cd71dfbeffde16a3638e582bedecc0ceb Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 29 Dec 2025 08:32:49 -0800 Subject: [PATCH 14/22] Adds notes to readme --- tests/staged_sim_and_verif/README.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tests/staged_sim_and_verif/README.md b/tests/staged_sim_and_verif/README.md index fe264b5..b4f6b4b 100644 --- a/tests/staged_sim_and_verif/README.md +++ b/tests/staged_sim_and_verif/README.md @@ -5,3 +5,9 @@ Staged simulation + verification example demonstrating staged verification using - 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. + +Design notes +- Two-phase flow: phase 1 reaches “two reqs seen” and emits a witness; phase 2 replays that witness with `sim -w` and covers the matching ack. +- Phase separation uses labeled properties (`phase1_*` / `phase2_*`), matching the SCY approach; each phase prunes with `select */c:phase* */c:phase1_* %d` (or `phase2_*`) then `delete`, leaving only the desired phase’s properties. +- 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 four tasks in order. The tiny `staged_sim_and_verif.sby` is only there so collect/required_tools see the test; the `.sh` enforces ordering. Set `SBY_MAIN` to your SBY entrypoint (e.g., `.../share/yosys/python3/sby_cmdline.py` from OSS CAD Suite) when running manually. From 889bfab8c94e6c6a10cef9b79b3a91e5538f5592 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 29 Dec 2025 09:07:11 -0800 Subject: [PATCH 15/22] Explicitly skip prep --- tests/staged_sim_and_verif/skip_staged_flow.sby | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby index f55a331..03f7001 100644 --- a/tests/staged_sim_and_verif/skip_staged_flow.sby +++ b/tests/staged_sim_and_verif/skip_staged_flow.sby @@ -11,6 +11,7 @@ mode prep fv: mode cover depth 40 +skip_prep on -- From 4a4d75df6a5411df5b3d610a620bbc45d972e978 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 29 Dec 2025 09:07:24 -0800 Subject: [PATCH 16/22] We still need to run the actual prep pass --- tests/staged_sim_and_verif/skip_staged_flow.sby | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby index 03f7001..9fef0fc 100644 --- a/tests/staged_sim_and_verif/skip_staged_flow.sby +++ b/tests/staged_sim_and_verif/skip_staged_flow.sby @@ -23,6 +23,7 @@ fv: smtbmc stage_1_init: verific -formal Req_Ack.sv hierarchy -top DUT +prep stage_1_fv: read_rtlil design_prep.il From 5abce0c9ee1faa8e7abe3c27069b39a4492e215a Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 29 Dec 2025 09:32:33 -0800 Subject: [PATCH 17/22] Update readme --- tests/staged_sim_and_verif/README.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/tests/staged_sim_and_verif/README.md b/tests/staged_sim_and_verif/README.md index b4f6b4b..6cb81e8 100644 --- a/tests/staged_sim_and_verif/README.md +++ b/tests/staged_sim_and_verif/README.md @@ -1,13 +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 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. +- 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 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. +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: phase 1 reaches “two reqs seen” and emits a witness; phase 2 replays that witness with `sim -w` and covers the matching ack. -- Phase separation uses labeled properties (`phase1_*` / `phase2_*`), matching the SCY approach; each phase prunes with `select */c:phase* */c:phase1_* %d` (or `phase2_*`) then `delete`, leaving only the desired phase’s properties. +- 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 four tasks in order. The tiny `staged_sim_and_verif.sby` is only there so collect/required_tools see the test; the `.sh` enforces ordering. Set `SBY_MAIN` to your SBY entrypoint (e.g., `.../share/yosys/python3/sby_cmdline.py` from OSS CAD Suite) when running manually. +- 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. From 531e328c3d5b53730c3773b9e3e22d70d5487797 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 29 Dec 2025 09:34:04 -0800 Subject: [PATCH 18/22] Update sby file --- .../staged_sim_and_verif/skip_staged_flow.sby | 39 +++++++++++++------ 1 file changed, 28 insertions(+), 11 deletions(-) diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby index 9fef0fc..88d2f5e 100644 --- a/tests/staged_sim_and_verif/skip_staged_flow.sby +++ b/tests/staged_sim_and_verif/skip_staged_flow.sby @@ -1,23 +1,30 @@ [tasks] stage_1_init init -stage_1_fv fv +stage_1_cover cover stage_2_init init -stage_2_fv fv +stage_2a_cover cover +stage_2b_assert assert [options] init: mode prep -fv: +cover: mode cover depth 40 skip_prep on +assert: +mode prove +depth 40 +skip_prep on + -- [engines] init: none -fv: smtbmc +cover: smtbmc +assert: smtbmc [script] stage_1_init: @@ -25,7 +32,7 @@ verific -formal Req_Ack.sv hierarchy -top DUT prep -stage_1_fv: +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. @@ -36,11 +43,18 @@ stage_2_init: read_rtlil design_prep.il sim -a -w -scope DUT -r trace0.yw -stage_2_fv: +stage_2a_cover: 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 +# 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 -- @@ -50,12 +64,15 @@ delete stage_1_init: Req_Ack.sv -stage_1_fv: +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_fv/engine_0/trace0.yw -stage_2_fv: +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 From 6c8a26eb86b948b67ae204b00e49d8cdea09132f Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 29 Dec 2025 09:34:18 -0800 Subject: [PATCH 19/22] Update script --- tests/staged_sim_and_verif/staged_sim_and_verif.sh | 8 +++----- 1 file changed, 3 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 7cb867e..a7426b8 100755 --- a/tests/staged_sim_and_verif/staged_sim_and_verif.sh +++ b/tests/staged_sim_and_verif/staged_sim_and_verif.sh @@ -3,14 +3,12 @@ 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_1_cover run_task stage_2_init -run_task stage_2_fv +run_task stage_2a_cover +run_task stage_2b_assert From 4decc31933d8939b9dbd2d2c4d167a7ddbefbe1b Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 29 Dec 2025 09:38:07 -0800 Subject: [PATCH 20/22] Split cover stage into two final stages --- tests/staged_sim_and_verif/Req_Ack.sv | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv index 7886261..581e4b9 100644 --- a/tests/staged_sim_and_verif/Req_Ack.sv +++ b/tests/staged_sim_and_verif/Req_Ack.sv @@ -7,16 +7,19 @@ module DUT ( `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 @@ -47,13 +50,20 @@ module DUT ( 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. + // 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_no_new_req: assume(!req); + phase2_shared_no_new_req: assume(!req); end + always @(posedge clk) begin - phase2_ack_eventually: cover(ack); + phase2a_cover_ack: cover(ack); + end + + always @(posedge clk) begin + phase2b_assert_req_count: assert(reqs_seen <= 2); + phase2b_assert_ack_count: assert(acks_seen <= 2); end From a41fdb67843fa1ec4a2daa276458877146144e31 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 29 Dec 2025 11:37:48 -0800 Subject: [PATCH 21/22] Fix: rename path --- 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 88d2f5e..12a011e 100644 --- a/tests/staged_sim_and_verif/skip_staged_flow.sby +++ b/tests/staged_sim_and_verif/skip_staged_flow.sby @@ -69,7 +69,7 @@ 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 +skip_staged_flow_stage_1_cover/engine_0/trace0.yw stage_2a_cover: skip_staged_flow_stage_2_init/model/design_prep.il From 0b88cdac90ecbd8de408ad3e5e663f893d2af181 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 29 Dec 2025 12:14:09 -0800 Subject: [PATCH 22/22] Remove req assertion; make assertion richer --- tests/staged_sim_and_verif/Req_Ack.sv | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv index 581e4b9..e1fd0e0 100644 --- a/tests/staged_sim_and_verif/Req_Ack.sv +++ b/tests/staged_sim_and_verif/Req_Ack.sv @@ -61,9 +61,13 @@ module DUT ( 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_req_count: assert(reqs_seen <= 2); - phase2b_assert_ack_count: assert(acks_seen <= 2); + phase2b_assert_ack_stable: assert(acks_seen <= 2); end