Hi All,
I have the following assertion:
assert property (@(posedge clk) (sig==1) |-> 2==3)
The above assertion doesn’t return a failure. Does this mean the signal sig have never been ‘1’?
Will the above assertion be checked till end of simulation or just on the nearest posedge clk?
Thank you!
In reply to ldm_as:
I strongly suggest that you study the meaning of vacuity in assertions.
In addition, you need to study the samplings and clocking events in assertions.
On that last point on various SV evaluation regions., see my replies at
https://verificationacademy.com/forums/systemverilog/sampling-point-assertions
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
Ben, could you explain in short why the below both expressions are evaluated as TRUE? What’s wrong?
assert property (@(posedge clk) (sig==1));
assert property (@(posedge clk) (sig==1) |-> 2==3);
I understand that you are promoting your book, but anyway…
P.S. I already have your book, but still don’t understand how this may happen… If the first expression is evaluated to TRUE, how the second one might be also TRUE???
In reply to ldm_as:
I you read my book and you still fail to understand this, then my book failed you;
try another book or do Google searched on SystemVerilog assertions; there is lot of free material.
assert property (@(posedge clk) (sig==1));
// sig==1 is a sequence that is a property the way it applied.
// At every clocking event , if sig==1, the assertion is a success, else a failure
assert property (@(posedge clk) (sig==1) |-> 2==3);
// if sig==0, the assertion is vacuously true, meaning not of interest
// if sig==1, then in the same cycle (because of the |->) 2==3) the 1st term of the
// consequent sequence is evaluated. Since 2==3 is false, the assertion is false.
// Thus, this assertion is either vacuously true or is false (a failure).
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr