SystemVerilog Assertion for valid (request) - ack checking?

0
votes

I am studying SystemVerilog Assertion. I applied SVA to check valid-ack spec. Spec is as below:

When the valid is drived (0 to 1), the valid should be equal to 1 until the ack is drived (1). When the ack is de-asserted (1 to 0), the valid is also de-asserted (1 to 0).

To check this spec, I wrote two property (pr1 and pr2). You can see the SVA code from the below link. https://www.edaplayground.com/x/5gHd

I expected that two property works exactly same. However, pr2 does not work as I expected (I expected that the assertion might fail at 50ns since the valid is equal to 1 but ack is equal to 0 at the 50ns).

Waveform: https://www.edaplayground.com/w/x/u5

What is the wrong at the pr2 (at 50ns)?

Best regards,

1
system-verilogverificationsystem-verilog-assertions
pr1 appears correct at first glance. The first post-condition in pr2 will match as long as valid is asserted, regardless of what ack is doing. That is probably not what you want. - teadotjay

1 Answers

0
votes

According to the SystemVerilog LRM:

A repetition with a range of min minimum and max maximum number of iterations can be expressed with the consecutive repetition operator [* min:max].

In pr2 you have used repetition operator with max equal to $ which stands for finite, but unbounded number of iterations so sequencevalid[*1:$] will last as long as valid is asserted and ack will be checked only after valid goes down.