Below are equivalent assertions:
// a |=> ##v b) // v is a module variable
property p_delay_equivalent; // Am producing an equivalent implementation
int local_v; // this is an internal local variable defined by the tool
a |=> (1, local_v = v)
##0 (1, local_v=local_v - 1'b1)[*0:$]
##1 local_v<0
##0 b;
endproperty
ap_delay_equivalent: assert property(@(posedge clk)ap_delay_equivalent);
// a |=> ##[0:v] ##1 b)
property p_range_equivalent; // Am producing an equivalent implementation
int local_v; // this is an internal local variable defined by the tool
a |=> (1, local_v = v)
##0 (local_v<0, local_v=local_v - 1'b1)[*0:$] ##1 b;
endproperty
ap_range_equivalent: assert property(@(posedge clk)ap_range_equivalent);
BTW, you’ll be able to use variables in delays and repeat operators in the next release of 1800 (maybe by end of 2015 or early 2016; that is in the plans.
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