.triggered and .matched of SVA sequence in multi clock property

SystemVerilog
, ,
1

Hi forum members,

I have a question about .triggered and .matched of SVA sequence.

In my understanding, the following properties are equivalent. At rising edge of s1, a sequence that s2 is kept high for 3 cycle’s and goes down low ends. Each of s1 and s2 is driven by different clock.

//----             _.__________
//s1 :  ________._|@             (clocked by clk1)
//----        _._._            
//s2 :  ___._|1 2 3|_._________  (clocked by clk2)
//----      >-------^   

property prop_1;
  @(posedge clk1) $rose(s1) |=>
  @(posedge clk2) ( !$past(s2,4) && $past(s2,3) && $past(s2,2) &&  $past(s2,1) && $fell(s2) );
endproperty

sequence seq_3high();
  @(posedge clk2) $rose(s2) ##0 s2[*3] ##1 $fell(s2);
endsequence

property prop_2;
  @(posedge clk1) $rose(s1) |=>
  @(posedge clk2) seq_3high().triggered;
endproperty

property prop_3;
  @(posedge clk1) $rose(s1) |->
  @(posedge clk2) seq_3high().matched;
endproperty

.matched implies synchronization between source clock and destination clock. So, I think it is same as synchronization by using |=> for .triggered and $past().

However, the property with .matched gives different results from others when they are examined by the followings tests.

===================================================
TEST 0 : FAIL is expected.
----             _.__________
s1 :    ______._|@           
----    _._._                
s2 :  _|1 2 3|_._____________
----  >-------^              
===================================================
TEST 1 : FAIL is expected.
----             _.__________
s1 :  ________._|@           
----      _._._              
s2 :  _._|1 2 3|_.___________
----    >-------^            
===================================================
TEST 2 : PASS is expected.
----             _.__________
s1 :  ________._|@           
----        _._._            
s2 :  ___._|1 2 3|_._________
----      >-------^          
===================================================
TEST 3 : FAIL is expected.
----             _.__________
s1 :  ______._._|@           
----          _._._          
s2 :  _____._|1 2 3|_._______
----        >-------^        
===================================================

prop_1, prop_2
TEST 0 : FAIL
TEST 1 : FAIL
TEST 2 : PASS
TEST 3 : FAIL

prop_3
TEST 0 : FAIL
TEST 1 : PASS
TEST 2 : FAIL
TEST 3 : FAIL

Here is a link to EDA Playground triggered and matched.

The results of prop_3(ast_3) are unexpected. Why are they different? Is my understanding wrong? Or, is this a tool issue?

Other simulators than QuestaSim give different results regarding prop_3(ast_3) and they are also unexpected. But I don’t mean to discuss it here.

2

rose(s1) at t305.
seq3high endpoint at 300
@(posedge clk2) after rose(s1) at t310
at t310 seq_3high().triggered ==0
The .matched extends to the next posedge clk
from 300 to 310
end point to be synchronized to clk2 (t300,
then at next cycle test for done with clk2
(at t310).

matched
matched1296×896 85.8 KB

An example from my SVA book:

sequence get_mem1;
     @(posedge clk1) rd ##1 valid[->1];
endsequence
ap_req2done: assert property(@(posedge clk) bus_req |-> ack[->1] // clocked with clk
##0 get_mem1.matched ##1 done); // end point to be synchronized to clk,
// then at next cycle test for done with clk

Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf

1 Like
3

Hi @ben2,

Thank your for your kind reply.
O.K. I understand my understanding was wrong. Extra 1 cycle extension is added at the end of the sequence in case of .matched. So, prop_1/2 and prop_3 is not equivalent.
I guess .matched is originally for asynchronous sequence inside another sequence. Therefore, extra 1 cycle extension is automatically added to sync back to original clock.

ack[->1] ##0      // synch to clk
get_mem1.matched  // synch to clk1, synch back to clk
##1 done          // synch to clk

Then, following
prop_2 <=> prop_3m
prop_2p <=> prop_3,
are equivalent respectively, aren’t they?

// Sequences
sequence seq_3high();
  @(posedge clk2) $rose(s2) ##0 s2[*3] ##1 $fell(s2);
endsequence

sequence seq_3high_plus(); // Added 1 cycle
  @(posedge clk2) $rose(s2) ##0 s2[*3] ##1 $fell(s2) ##1 1;
endsequence

sequence seq_3high_minus(); // Removed 1 cycle
  @(posedge clk2) $rose(s2) ##0 s2[*3];
endsequence

property prop_2;
  @(posedge clk1) $rose(s1) |=>
  @(posedge clk2) seq_3high().triggered;
endproperty

property prop_3m;  
  @(posedge clk1) $rose(s1) |->
  @(posedge clk2) seq_3high_minus().matched ##0 $fell(s2);
property

property prop_2p;
  @(posedge clk1) $rose(s1) |=>
  @(posedge clk2) seq_3high_plus().triggered;
endproperty;

property prop_3;
  @(posedge clk1) $rose(s1) |->
  @(posedge clk2) seq_3high().matched;
endproperty

I added ast_3m and ast_2p to my EDA Playground.
triggered and matched of SVA sequence
They work as expected.

4

I did not checkout your code. However, from my SVA book, the folowing explains the .matched

matched_rule
matched_rule990×785 174 KB

5

Thanks @ben2 ,

It looks it align with my understanding.

$rose(mreq0.req0r) |-> // Sync to clk0
qack1.matched          // Sync to clk1 (t39) and sync back to clk0 (t40)
##[1:2] mreq0.ack0r    // Sync to clk0