# SVA Repetition operator \[= **URL:** \ **Category:** SystemVerilog\ **Tags:** SystemVerilog\ **Created:** [February 23, 2015, 4:16pm UTC](https://verificationacademy.com/forums/t/sva-repetition-operator/30391 "2015-02-23T16:16:41Z")\ **Posts on this page:** 8\ **Page:** 1
**Author:** ![Jartar](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/j/ccd318/32.png) [@Jartar](https://verificationacademy.com/forums/u/Jartar)\ **Post date:** [February 23, 2015, 4:16pm UTC](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/1 "2015-02-23T16:16:41Z")
I am trying to implement this check: between two consecutive asserts of signal A separated by any no of clock cycles signal B should be asserted only once. i.e. A cannot be asserted without B received for previous A. I tried to use the repetition operator for this [= Sequence: A |-\> (B[=1]) ## [1:$] A; I’ve tried to introduce a bug and get this assertion to fire. But not sure if this will work. any thoughts ? ---
**Author:** ![user49](https://verificationacademy.com/forums/user_avatar/verificationacademy.com/user49/32/1084_2.png) [@user49](https://verificationacademy.com/forums/u/user49)\ **Post date:** [February 24, 2015, 4:25pm UTC](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/2 "2015-02-24T16:25:13Z")
In property (A |-\> (B[=1]) ## [1:] A) you need to understand the equivalents for the [=m] and [-\>m] b[=m] is equivalent to ( b [-\>m] ##1 !b [\*0:] ) b[-\>m] is equivalent to ( !b [\*0:] ##1 b)[\*m] Thus, what you wrote is equivalent to (A |-\> B [-\>1] ##1 !B [\*0:] ## [1:$] A) and the following thread would pass the property, something you may not want (A |-\> B [-\>1] ##1 A) // because (!b[\*0] ##1 A) is same as (A) Also, because of the implication operator, this sequence would succeed: A ##0 B ##1 A // Not what you want. I suggest you change it to: ```auto $rose(A) |=> (B[=1]) ##1 A // same as $rose(A) |=> B[->1] ##1 !B[*0:$]##1 A // This would be satisfied by any of the following sequences A ##1 B ##1 A or A ##1 !B ##1B ##1 !B ##1A // --- If you want a !B separation between B and A, then this would work $rose(A) |=> (B[->1]) ##1 !B[*1:$] ##1 A // This would be satisfied by any of the following sequences A ##1 B ##1 !B ##1 A or A ##1 !B ##1B ##1 !B ##1A ``` * * * Ben Cohen [http://www.systemverilog.us/](http://www.systemverilog.us/) [ben@systemverilog.us](mailto: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 * * * ---
**Author:** ![Jartar](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/j/ccd318/32.png) [@Jartar](https://verificationacademy.com/forums/u/Jartar)\ **Post date:** [February 25, 2015, 7:25pm UTC](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/3 "2015-02-25T19:25:54Z")
_In reply to [ben@SystemVerilog.us](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/2):_ Thanks very much. will try it out. ---
**Author:** ![lilyding](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/l/919ad9/32.png) [@lilyding](https://verificationacademy.com/forums/u/lilyding)\ **Post date:** [February 27, 2015, 5:09am UTC](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/4 "2015-02-27T05:09:19Z")
_In reply to [Jartar](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/3):_ Hi Ben/Jartar, I have something similar to your case. In the following code, I intend to implement there is only one outstanding request, i.e. After A&&B , it has to wait response C && D asserted, and the next A&&B has to be presented after C && D have already de-asserted, but the cycles in-between could be any number of cycle, does the following implementation make sense? Thanks. sequence request; ##[1:$] A && B; endsequence sequence response; ##[1:] C && D ##[1:] !C[\*1:] ##[1:] A && B ; endsequence property outstanding\_req; @(posedge clk) request |-\> response; endproperty assert property (outstanding\_req); ---
**Author:** ![lilyding](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/l/919ad9/32.png) [@lilyding](https://verificationacademy.com/forums/u/lilyding)\ **Post date:** [February 27, 2015, 6:01am UTC](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/5 "2015-02-27T06:01:29Z")
_In reply to [ben@SystemVerilog.us](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/4):_ Thanks Ben for the correction. The operand after intersect is to make sure there is no A&&B occurring at the same time, right? This is actually a checker on an AXI read interface, A&B is like ARREADY \* ARVALID, C&D is like RREADY & RVALID. So from protocol wise, would this assertion also make sense? Thanks much for your insight! ---
**Author:** ![lilyding](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/l/919ad9/32.png) [@lilyding](https://verificationacademy.com/forums/u/lilyding)\ **Post date:** [February 27, 2015, 6:16am UTC](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/6 "2015-02-27T06:16:58Z")
_In reply to [nickbayshore](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/5):_ Also, what’s that label ap\_abcdab for? I didn’t see a label from this assertion tutorial website: [http://www.doulos.com/knowhow/sysverilog/tutorial/assertions/](http://www.doulos.com/knowhow/sysverilog/tutorial/assertions/) Thanks ---
**Author:** ![user49](https://verificationacademy.com/forums/user_avatar/verificationacademy.com/user49/32/1084_2.png) [@user49](https://verificationacademy.com/forums/u/user49)\ **Post date:** [February 27, 2015, 6:33am UTC](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/7 "2015-02-27T06:33:04Z")
_In reply to [nickbayshore](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/6):_ The operand after intersect is to make sure there is no A&&B occurring at the same time, right? [Ben] Correct This is actually a checker on an AXI read interface, A&B is like ARREADY \* ARVALID, C&D is like RREADY & RVALID. So from protocol wise, would this assertion also make sense? Thanks much for your insight! [Ben] Makes sense; keep in mind that I am not familiar with that protocol. In any case, an assertion reflects the requirements, and they should express the intent (what is desired) and they should be accurate; thus, they should includes assumptions tha may be in your head. In this case you have something like: X … Y … X. What happens between X and Y? BTW, I made a mistake in the request and response Code should be: ```auto sequence request; A && B; // DOn't need the ##[1:$] <------ // Do you need a $rose? endsequence sequence response; ( (##[1:$] C && D ##[1:$] !(C && D)[*1:$]) intersect (1 ##1 !(A && B)[*1:$]) ) // <-- added the 1 ##1 because both sequences start at same time as the antecedent ##[1:$] A && B ; endsequence ap_abcdab: assert property(@(posedge clk) request |-> response); sequence response2; // Another option ( (##[0:$] C && D ##[1:$] !(C && D)[*1:$]) intersect // <<-- ##[0:$ insteas of ##[1:$ (!(A && B)[*1:$]) ) ##[1:$] A && B ; endsequence ap_abcdab2: assert property(@(posedge clk) request |=> response2); // |=> instead of |-> ``` what’s that label ap\_abcdab for? I didn’t see a label from this assertion tutorial website: [Ben] I strongly recommend that every assertion statement have a label; it makes debugging far easier. Otherwise, the tool will generate a funky, nonsense label for you. ---
**Author:** ![user49](https://verificationacademy.com/forums/user_avatar/verificationacademy.com/user49/32/1084_2.png) [@user49](https://verificationacademy.com/forums/u/user49)\ **Post date:** [February 27, 2015, 6:36am UTC](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/8 "2015-02-27T06:36:13Z")
_In reply to [nickbayshore](https://verificationacademy.com/forums/t/sva-repetition-operator/30391/7):_ // [Ben] How do you detect that A&&B does not occur while you wait for C&&D? ```auto sequence request; // ##[1:$] A && B; // Update: change to A && B; // may need a $rose, check requirements endsequence sequence response; ( (##[1:$] C && D ##[1:$] !(C && D)[*1:$]) intersect // (!(A && B)[*1:$]) ) // need a ##1 (1 ##1 !(A && B)[*1:$]) ) // Updated ##[1:$] A && B ; endsequence ap_abcdab: assert property(@(posedge clk) request |-> response); ``` Ben [SystemVerilog.us](http://SystemVerilog.us)