I provide 2 solutions in my SVA Handbook 4th Edition, 2016
*Simple repeat (e.g., a[v]]
ap_repeat_fix: assert property( $rose(a) |-> b[*v] ##1 c); //1800'2018 property
// Above is illegal in 1800'2012
p_repeat_equivalent; // /11.4/m5067_gen_options.sv. works in 1800'2012
int local_v; //
$rose(a) |->
(1, local_v = v) ##0 first_match((b, local_v=local_v - 1)[*0:$] ##1 local_v<=0)
##0 c; //
endproperty
ap_repeat_equivalent: assert property(p_repeat_equivalent); // with default clocking
generate option
If the variable used to define the repeat has values that are within a constraint range, such as between 0 and 7 (or 15, or at most 32) one can use the generate statement, which appears much simpler than the use of local variables and the sequence_match_item.
generate for (genvar g_i=0; g_i<8; g_i++) begin
ap_repeat_gen: assert property (v==g_i && $rose(a) |-> b[*g_i] ##1 c);
end endgenerate
The generate
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA 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 978-1539769712
- 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