SVA Repetition operator [=

SystemVerilog
1

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 ?

2

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:

$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/ 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
3

In reply to ben@SystemVerilog.us:

Thanks very much. will try it out.

4

In reply to Jartar:

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);

5

In reply to ben@SystemVerilog.us:

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!

6

In reply to nickbayshore:

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/

Thanks

7

In reply to nickbayshore:

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:

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.

8

In reply to nickbayshore:

// [Ben] How do you detect that A&&B does not occur while you wait for C&&D?

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