Skip to content

Commit

Permalink
[prim,dv] Fix a failure mode for ASSERT_FPV_LINEAR_FSM
Browse files Browse the repository at this point in the history
I tweaked this assertion in commit b5b4087 (to allow a formal tool to
see the assertion run to completion). But that caused failures in a
chip-level test. The test resets the block (which causes the FSM state
to go back to its initial value) but the "until" operator doesn't
complete for some reason.

Tweaking the "until" so that it waits until the condition above gets
cleared seems to work. This seems surprising to me (since I would
expect the difference to be the other way around) but it seems to
solve the problem.

Signed-off-by: Rupert Swarbrick <[email protected]>
  • Loading branch information
rswarbrick committed Nov 18, 2024
1 parent a3bf859 commit 64353cf
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion hw/ip/prim/rtl/prim_assert.sv
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,7 @@
property __name``_p; \
__type initial_state; \
(!$stable(__state) & __name``_cond, initial_state = $past(__state)) |-> \
(__state != initial_state) until (__rst == 1'b1); \
(__state != initial_state) until !(__name``_cond); \
endproperty \
`ASSERT(__name, __name``_p, __clk, 0) \
`endif
Expand Down

0 comments on commit 64353cf

Please sign in to comment.