// Two problems with
assert property (@(posedge clk) disable iff (!reset_n) $fell(a) ##[0:$] $fell(a) |-> $stable(dist_value))
1) $fell(a) ##[0:$] $fell(a) // is same as
$fell(a) ##0 $fell(a) or $fell(a) ##1 $fell(a) or ...
// Thus, upon the first $fell(a) the $fell(a) ##0 $fell(a) is satisfied.
// However, the other problem is that
2) the antecedent has multiple matches, and all matches must be evaluated
// before the property succeeds.
//You can do one of the following solutions:
assert property (@(posedge clk) disable iff (!reset_n)
first_match($fell(a) ##[1:$] $fell(a)) |-> $stable(dist_value));
assert property (@(posedge clk) disable iff (!reset_n)
$fell(a) ##1 $fell(a)[->1] |-> $stable(dist_value));
// Note: : b [->m] is equivalent to ( !b [*0:$] ##1 b)[*m]
// NOTE: The following assertion, though more brief, is NOT recommended
// because it is inefficient because multiple threads are started when !$fell(a)
ap_VERY_BAD_STYLE: assert property (@(posedge clk) disable iff (!reset_n)
$fell(a)[->2] |-> $stable(dist_value)); // INEFFICIENT!!!
// b[->2] is equivalent to:
// !b[*0:$] ##1 b ##1 !b[*0:$] ##1 b
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