In reply to foxtrot:
Your requirements are ambiguous.
Can you create a table or a better description of the requirements?
For example,
- If ref = 0 and ack = 0 then ..
// or is it "if($fell(ref) and ack", or is it "if($fell(ack) ..
- ....If(..) then ..
- ...
You need to clarify the antecedents. It is OK (or even better) to have multiple small assertions.
With
!refclk throughout (!refClkReq && !refClkAck) [*1:$];
are you trying to say
@(posedge sclk) $fell(req) |-> !refclk throughout (!Req ##[*1:$] !Ack);
The
throughout operator specifies that a signal (expression) must hold throughout a sequence.
( b throughout R ) is equivalent to ( b [*0:$] intersect R )
For example, in the following handshake example, a req is honored with an acknowledge within the next 4 cycles. The ack is then followed at a later time by a done control signal. However, there is one additional requirement that throughout the time between the ack and done an enable signal must be asserted to drive a tri-state bus. That assertion can be expressed as follows. Figure 2.4.6 demonstrates a timing diagram that satisfies an assertion of this property.
ap_handshake : assert property (
$rose(req) |-> ##[1:4] enable throughout (ack ##[1:$] done));
Ben Cohen
http://www.systemverilog.us/
For training, consulting, services: contact
http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats
https://rb.gy/a89jlh
2) Free books: Component Design by Example
https://rb.gy/9tcbhl
Real Chip Design and Verification Using Verilog and VHDL($3)
https://rb.gy/cwy7nb
3) Papers:
- Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment