In reply to cool_cake20:
What I initially wrote was correct for the original requirements:
“Pulse A should not fall between these two pulses(B and C). It be either before B or after C.”
meaning (my interpretation) that if A==0, it should fail.
ap_abc: assert property(reject_on (!a) // reject if a==0, since !a==1, and abort condition is true
@(posedge b) 1’b1 |-> @(posedge c) 1’b1); / is correct.
For this requirement
“If in between B and C there may be any number of clock cycles like [1:$] in a given simulation but A should not be become high(meaning must be 0, if 1 → fail) in between B and C.” then
ap_abc: assert property(reject_on (a)
@(posedge b) 1’b1 |-> @(posedge c) 1’b1); / is correct.
From the syntax of a property
property_expr ::= // includes
reject_on ( expression_or_dist ) property_expr
Thus,
assert property (@(posedge clk) rose(b) |-> (reject_on(a) ##[1:] c); // is correct
// The " c[1:]" is incorect, unless you mean c[*1:], which is a repeat operator
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115