mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-02-22 03:07:38 +00:00
Code Activity

phase->stage

Browse source
This commit is contained in:
Gus Smith 2026-01-21 08:30:03 -08:00
parent b66bbe4503
commit e89f71b3cb
2 changed files with 15 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

18
tests/staged_sim_and_verif/Req_Ack.sv
View file

@ -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:$]
);

12
tests/staged_sim_and_verif/skip_staged_flow.sby
View file

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