In reply to ben@SystemVerilog.us:
If you don’t want to use the generate, you can do the following:
property p_delay;
int v;
($rose(a), v=delay+1'b1) |->
first_match((v>0 && !b, v=v-1'b1)[*0:$] ##1 v==0) ##0 $rose(b);
// New comment: No need for the first_match because of the v>0 test
// Need of first_match() if we use the following instead
// first_match((!b, v=v-1'b1)[*0:$] ##1 v==0) ##0 $rose(b);
endproperty
// You need the first_match() because without it, id no $rose(b)
// the repeats keeps on counting forever.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
- 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