3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-12-27 07:17:08 +00:00

Use labels to be more like SCY

This commit is contained in:
Gus Smith 2025-12-15 17:36:36 -08:00
parent 7c66b2d132
commit e904e88fc9
2 changed files with 9 additions and 12 deletions

View file

@ -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

View file

@ -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
--