From ad93d4fc4f74b91e6827c2c9faeadc177184a3b6 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 9 Dec 2025 11:17:33 -0800 Subject: [PATCH 01/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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 --