CODEWITHSUNDEEP
system-verilogverificationsystem-verilog-assertions
Shuaiyu Jiang
Shuaiyu Jiang

Reputation: 239

SystemVerilog Assertions: Once A is asserted, A remains high until B is de-asserted, and after that A will finally be low

I tried to write a assertion:

Once A is asserted, A remains HIGH until B is de-asserted. After that, A will finally de-asserted.

The assertion I wrote was:

my_assertion : assert property(
    @(posedge clk) disable iff(reset)
    $rose(A) |-> A throughout !B [->1] ## [0:$] !A) 
else $display("Assertion failed")

The assertion failed at the time when A is de-asserted. Guys, can you please tell me where I did wrong in my_assertion? Was " [0:$] " not used correctly?

Upvotes: 2

Views: 2913

Answers (2)

Matthew
Matthew

Reputation: 13937

I think you're problem is due to operator precedence. This does not fail when A is deasserted:

$rose(A) |-> (A throughout !B [->1]) ## [0:$] !A

whereas what you have written is the same as:

$rose(A) |-> A throughout (!B [->1] ## [0:$] !A)

which can never pass, because A cannot be true and false at the same time.

https://www.edaplayground.com/x/4Vv9

Upvotes: 3

Greg
Greg

Reputation: 19094

## has a higher priority than throughout; See IEEE1800-2012 § 16.9 Sequence operations Table 16-1.

Therefore A throughout !B [->1] ## [0:$] !A is the sample a A throughout (!B [->1] ## [0:$] !A). This fails because A is required be high (left side of throughout) and low (right side of throughout) for the last cycle, which will always evaluate as false.

I believe the desired behavior is: (A throughout !B [->1]) ## [0:$] !A

Upvotes: 4

Related Questions