Open
Description
I encountered some issues where assertions similar to the following are always refuted and I have tested it in several projects:
assert property(@(posedge PCLK) ((PADDR >= 1959869417) && (PADDR <= 2152689152) ##1 (PWDATA >= 1116873605) && (PWDATA <= 1290695065) ##2 1) |-> (WRITE_DATA_ON_TX >= 323527462) && (WRITE_DATA_ON_TX <= 4294534911));
assert property(@(posedge DEFAULT_CLOCK) (bitIn && bitOut ##1 bitN ##1 bitOut ##1 !bitN && !bitOut ##1 !bitIn) |-> bitOut);
In this assertion, there are delays like ##2 1
,##1 bitN ##1
, ##1 (PWDATA >= 1116873605) && (PWDATA <= 1290695065)
or other sequences. Any assertions similar to these are refuted and only assertions similar to this one can pass,
assert property(@(posedge DEFAULT_CLOCK) (bitOut) |-> bitOut);
even though they are passed by other formal verification tools.
Metadata
Metadata
Assignees
Labels
No labels