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.