Skip to content

Commit

Permalink
PSL assertions should not be postponed
Browse files Browse the repository at this point in the history
  • Loading branch information
nickg committed Nov 2, 2024
1 parent 84a79d2 commit c16d2ae
Show file tree
Hide file tree
Showing 6 changed files with 6 additions and 7 deletions.
2 changes: 1 addition & 1 deletion src/rt/model.c
Original file line number Diff line number Diff line change
Expand Up @@ -535,7 +535,7 @@ static void scope_for_block(rt_model_t *m, tree_t block, rt_scope_t *parent)

p->wakeable.kind = W_PROPERTY;
p->wakeable.pending = false;
p->wakeable.postponed = true;
p->wakeable.postponed = false;
p->wakeable.delayed = false;

APUSH(s->properties, p);
Expand Down
2 changes: 1 addition & 1 deletion test/regress/psl13.vhd
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ begin
cgen: c <= seq_c(clk);
dgen: d <= seq_d(clk);

-- psl default clock is clk'event;
-- psl default clock is clk'delayed(0 ns)'event;

-- Should fail at: 3 ns and 7 ns
-- psl asrt_1 : assert always {a;b} |=> {c;d};
Expand Down
3 changes: 1 addition & 2 deletions test/regress/psl2.vhd
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,7 @@ architecture psl of psl2 is
signal clk : natural;

-- All is sensitive to rising edge of clk
-- psl default clock is clk'event;

-- psl default clock is clk'delayed(0 ns)'event;
begin

clkgen: clk <= clk + 1 after 1 ns when clk < 5;
Expand Down
2 changes: 1 addition & 1 deletion test/regress/psl3.vhd
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ architecture psl of psl3 is
signal clk : natural;

-- All is sensitive to rising edge of clk
default clock is clk'event;
default clock is clk'delayed(0 ns)'event;

begin

Expand Down
2 changes: 1 addition & 1 deletion test/regress/psl5.vhd
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ architecture psl of psl5 is
signal clk : natural;

-- All is sensitive to rising edge of clk
-- psl default clock is clk'event;
-- psl default clock is clk'delayed(0 ns)'event;

begin

Expand Down
2 changes: 1 addition & 1 deletion test/regress/psl6.vhd
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ architecture psl of psl6 is
signal clk : natural;

-- All is sensitive to rising edge of clk
-- psl default clock is clk'event;
-- psl default clock is clk'delayed(0 ns)'event;

begin

Expand Down

0 comments on commit c16d2ae

Please sign in to comment.