Assertions: Using 2 clocks within a sequence to sample $rose and $fell

SystemVerilog
1

Hi,

This is a question regarding system verilog assertions, namely concurrent assertions.
The question is, there is a situation where I have to check 1 condition, if it matches, then I have to check for 2 different sequences sampling signals at 2 different clock edges.
So, can I use theses 2 sequences in a single consequent with boolean operator between them?

Let me display a sample code that I have coded:

module m1;

sequence s1;
@(posedge clk1) ( $rose(a1) && $fell(b1) );//here the $rose/$fell should be sampled @(posedge clk1)
endsequence

sequence s2;
@(posedge clk2) ( $rose(a1) && $fell(b1) );//here the $rose/$fell should be sampled @(posedge clk2)
endsequence

property p1;
@(posedge clk1)
disable iff reset;
($rose(c1) && d1) |-> s1 or s2;
endproperty

assert property (p1);

endmodule;

However, this is not giving me the desired output.

After going through System Verilog LRM 1800-2012, I found this:
"
The following example shows a combination of differently clocked properties using both implication and
Boolean property operators:
@(posedge clk0) s0 |=> (@(posedge clk1) s1) and (@(posedge clk2) s2)
The multiclocked overlapping implication |-> has the following meaning: at the end of the antecedent the
nearest tick of the consequent clock is awaited. If the consequent clock happens at the end of the antecedent,
the consequent is started checking immediately. Otherwise, the meaning of the multiclocked overlapping
implication is the same as the meaning of the multiclock nonoverlapping implication.
"

2

In reply to NIDHI MAKWANA:
Everything you wrote is correct, even the assertion.
Question: Why are you saying "However, this is not giving me the desired output."
You need to clarify what you are really looking for.
With your assertion, if the antecedent passes, then in the same cyle (since same clock) the assertion succeeds if ( $rose(a1) && $fell(b1) ) matches. Else, the consequent will wait for the nearest @(posedge clk2) and then check if ( $rose(a1) && $fell(b1) ) matches. If it does the assertion is true.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

3

In reply to ben@SystemVerilog.us:

Hi ben,

As I did not “Previewed” it, so edited it now…

Elaborating on

However, this is not giving me the desired output.

With reference to the above code, let

sequence s0;
  @(posedge clk1)
  ($rose(c1) && d1);
endsequence

What I want to check is,

                                (consequent 1)
                          ----> s1 starts(at clk1) ----------------------||
                          |        [slower clock]                      {**assertion fails here}
s0(if this passes) -------|
(antecedent)              |     (consequent 2)
                          ----> s2 starts(at clk2) ----||
                                   [faster clock]       {*s2 condition meets here}

*  Condition meets for sequence "s2" w.r.t. clk2, but still
** the assertion fails for not meeting the sequence s1 w.r.t. clk1.

In my case, the clk1 is slower than clk2. So, when the antecedent condition is met, there are 2 threads(s1, s2) that will start at the same time, and they will be sampled at 2 different clocks(please correct if my understanding is wrong). As, there is an “or” operator used in between “s1” and “s2”, so, “s1” and “s2” will be checked parallelly.

However, I again went through the SystemVerilog LRM 1800-2012, and I found in Table 16-3, the precedence order of sequence and property operators.

[“and” is of higher precedence than “|->”]

What I understand from that table is, the operator with higher precedence should be evaluated first; i.e. w.r.t. p1,

property p1;
  @(posedge clk1)
  disable iff reset;
  (    s0        |->        (s1 or s2)     )  ;
                  ^              ^
                  |              |
                  |          1. evaluated first
                  |
            2. then implication
 
endproperty

So, “s0” is an antecedent, and “s1” and “s2” are 2 parallel consequents with different clocks.

Now according to your description,

property p1;
  disable iff reset;
  (   (s0  |-> s1)          or           s2  );
            ^               ^
            |               |
       1. This is           |
     evaluated first        |
                            |
                      2. Then this will be checked.

endproperty

This is not what I want to check through this check.

So, can you correct me and provide me a wiser way to implement this?

PS: Please correct if my understanding is wrong.

4

In reply to NIDHI MAKWANA:
Your understanding of the following is correct:

property p1;
  @(posedge clk1)
  disable iff reset;
  (    s0        |->        (s1 or s2)     )  ;
                  ^              ^
                  |              |
                  |          1. evaluated first
                  |
            2. then implication
 
endproperty

I ran the following model http://systemverilog.us/vf/twosq.sv
and got the following results

1085×472 34 KB


// ap1, ap2, and ap2c are all equivalent
ap1: assert property (p1);
ap2: assert property (@(posedge clk1) $rose(c1) && d1 |-> (s1 or s2) );
ap2a: assert property (@(posedge clk1) $rose(c1) && d1 |-> s1);
ap2b: assert property (@(posedge clk1) $rose(c1) && d1 |-> s2);
ap2c: assert property ( (@(posedge clk1) $rose(c1) && d1 |-> s1) or 
         	        (@(posedge clk1) $rose(c1) && d1 |-> s2)); 

// Was puzzled by the following though because the leading clock is in from the antecedent 
sequence s1s2; s1 or s2; endsequence
// Directive 'ap3' has property instances with multiple leading clocks.
 ap3_BAD: assert property (@(posedge clk1) $rose(c1) && d1 |-> @(posedge clk1) s1s2);
 ap3: assert property (@(posedge clk1) $rose(c1) && d1 |->  s1s2);
// Directive 'ap3a' has property instances with multiple leading clocks.
 ap3a: assert property (@(posedge clk1) $rose(c1) && d1 |->  (1|-> s1s2));
//** HOWEVER, a tool gave me the explanation
                 s1 or s2;
		    |
" Invalid operator and/or operands in multi-clock context."
// This is probably somewhere in 1800

Best advice, keep it simple; use something like ap2c

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us