SVA with multiple clocks

SystemVerilog
,
1

Hi Forum ,
Having established a basic understanding of SV assertions I decided to delve into multi-clocked assertions .
I started referring to book by author Ashok Mehta where I read the following quote

“There are differences in the way a ‘sequence’ behaves for multiple clocks and the way property behaves”

Since the book doesn’t elaborate further on it I decided to start trying out examples in the book.
One such example where I observe a difference in sequence and property behavior is :


  property  multiclocks ;
    @(posedge clk2) y and @(posedge clk3) z ; 
  endproperty
  try1:assert property ( @(posedge clk1)  x  |=>  multiclocks );

The above code executes whereas on changing it to :


  sequence  multiclocks ;
    @(posedge clk2) y and @(posedge clk3) z ; 
  endsequence
  try2:assert property ( @(posedge clk1)  x  |=>  multiclocks );

In this case I observe tools start throwing compilation errors like


(tool1) Error-[SVA-CMISO] Clocks mismatch in sequence operator.
(tool2) Sequence/SERE 'multiclocks' declared in 'top' has multiple leading clocks. Such sequence/SERE cannot be instanced as maximal property of a directive.

I tried searching the System Verilog LRM for the same but wasn’t successful :(
Would like to hear from the forum members and moderators on the above scenario .
Why do ‘sequences’ behave differently than ‘property’ for multiple clocks ?
I was under the impression that both ‘sequence’ and ‘property’ are valid as consequent.
Does the LRM have an example on the it ? If yes, could someone please point to the same

Regards,
Md. Waqar

2

/* 1800: 16.13.1: Differently clocked or multiclocked sequence operands cannot be combined with any
sequence operators other than ##1 and ##0.
For example, if clk1 and clk2 are not identical, then the following are illegal:
@(posedge clk1) s1 ##2 @(posedge clk2) s2
@(posedge clk1) s1 intersect @(posedge clk2) s2 */
This is why the sequence declaration sequence multiclocks_err fails to compile.
However, if the leading clock is unique, a property can change clocks on all ops.

Test I conducted: The following code compiled and simmed OK by all.
However if I include try2:assert property ( @(posedge clk1) x |=> multiclocks_err );
then all 3 vendors flagged the sequence as an error.

module test(); 
  bit clk1, clk2, clk3, x, y, z;
  property  multiclocks ;
    @(posedge clk2) y and @(posedge clk3) z ;
  endproperty
  try1:assert property ( @(posedge clk1)  x  |=>  multiclocks );
  //The above code executes whereas on changing it to :

 /* sequence  multiclocks_err ;
    @(posedge clk2) y and @(posedge clk3) z ;
  endsequence
    try2:assert property ( @(posedge clk1)  x  |=>  multiclocks_err ); */
    initial #100;
endmodule

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

3

In reply to ben@SystemVerilog.us:

Hi Sir ,
As the above quote specifically says "sequence operands " , it makes sense that the following is illegal :


 sequence diff_clocks_seq ;   
   @(posedge clk0) x ##2 @(posedge clk1) y;  // Invalid operator and/or operands in multi-clock context.  
 endsequence  
  assert property ( diff_clocks_seq );

However on declaring it as property the same error exists :


 property diff_clocks_prop ;   
   @(posedge clk0) x ##2 @(posedge clk1) y;  // Invalid operator and/or operands in multi-clock context.  
 endproperty
  assert property ( diff_clocks_prop );

This means that 1800: 16.13.1 is applicable to property expressions as well as sequence expressions.

I am still unclear on why is it that in my initial code , declaring ‘multiclocks’ as a property is legal whereas as a sequence it’s illegal ?

4

In reply to mohabhat:

For multiclocking you can only use ##0 or ##1 to switch the clocks.
Thus, this is illegal
@(posedge clk0) x ##2 @(posedge clk1) y;

(9) - EDA Playground // is OK

property diff_clocks_prop ;   
    @(posedge clk0) x ##1 @(posedge clk1) y;  // line 15 
  endproperty
  assert property ( diff_clocks_prop );

Ben

5

In reply to ben@SystemVerilog.us:

I am still not clear on my original doubt. In your earlier reply you commented :

However, if the leading clock is unique, a property can change clocks on all ops.

Could you please elaborate on this ? Why is it applicable for only property and not for a sequence ?

1800: 16.13.1: Differently clocked or multiclocked sequence operands cannot be combined with any sequence operators other than ##1 and ##0.
For example, if clk1 and clk2 are not identical, then the following are illegal:
@(posedge clk1) s1 ##2 @(posedge clk2) s2
@(posedge clk1) s1 intersect @(posedge clk2) s2

The above applies to both property as well as sequences , right ?

So why is it that the following is legal


  property  multiclocks ;
    @(posedge clk2) y and @(posedge clk3) z ;   // Legal
  endproperty
  try1:assert property ( @(posedge clk1)  x  |=>  multiclocks );

whereas the following is illegal


  sequence  multiclocks ;
    @(posedge clk2) y and @(posedge clk3) z ;   // Illegal
  endsequence
  try2:assert property ( @(posedge clk1)  x  |=>  multiclocks );
6

In reply to mohabhat:
In summary,

  1. You can only switch clocks in sequences with the ##0 or the ##1
  2. The clock flow cannot change in the RHS of ‘and’ operator.
    ILLEGALS
   try2:assert property ( @(posedge clk1) 1 ##0  @(posedge clk2) y and
1 ##0 @(posedge clk3) z );
//  The clock flow cannot change in the RHS of 'and' operator.
try3:assert property ( @(posedge clk1) 1 ##0  @(posedge clk2) y and @(posedge clk3) z );
  1. You can also switch clocks between a sequence and a property with the |-> or the |=>
  2. If the leading clock is unique, a property can change clocks on all ops.
property  multiclocks ;
@(posedge clk2) y and @(posedge clk3) z ;
endproperty
//try1:assert property ( @(posedge clk1)  multiclocks ); // illegal
try1:assert property ( @(posedge clk1) 1 |->  multiclocks ); // Legal

Another example:
(12) - EDA Playground // code
EPWave Waveform Viewer // wave


   function void f(bit a); 
      if(a) Y=Y+1; 
      else Z=Z+1;
    endfunction
  
    try2: assert property ( @(posedge clk1) 1 |->  // leading clock
                          (@(posedge clk2) (y, f(1))) and
                          (@(posedge clk3) (z, f(0))) ) pass=pass+1;

Ben