can someone please explain the difference (if any) between the following 2 properties
@(posedge slow_clk_A) $changed(A)|->##1 @(posedge fast_clk_B) $changed(B)
When i wrote the cover properties in jasper tool, i see that the waves are exactly same.
When i try to compile the below property for simulation, it failed saying that there is some issue with the delay ##2, it is accepting only ##1 or ##0.
Is there a standard reason for this ?
@(posedge slow_clk_A) $changed(A)|-> ##2 @(posedge fast_clk_B) $changed(B)
Yes, there is a standard on that, and it is limited to ##0 or ##1. sv1800’2017 16.13.1 Multiclocked sequences
Multiclocked sequences are built by concatenating singly clocked subsequences using the single-delay concatenation operator ##1 or the zero-delay concatenation operator ##0. The single delay indicated by ##1 is understood to be from the end point of the first sequence, which occurs at a tick of the first clock, to the nearest strictly subsequent tick of the second clock, where the second sequence begins. The zero delay indicated by ##0 is understood to be from the end point of the first sequence, which occurs at a tick of the first clock, to the nearest possibly overlapping tick of the second clock, where the second sequence begins.
On your other question:
@(posedge slow_clk_A) $changed(A)|-> ##1 @(posedge fast_clk_B) $changed(B)
// is same as
@(posedge slow_clk_A) $changed(A)|->
@(posedge slow_clk_A) 1 ##1 @(posedge fast_clk_B) $changed(B)
// The sampling is at the nearest strictly subsequent tick of the second clock,
// vs
@(posedge slow_clk_A) $changed(A)|-> @(posedge fast_clk_B) ##1 $changed(B)
the nearest possibly overlapping tick of the second clock, where the second sequence begins.
In reply to ben@SystemVerilog.us:
Thanks for the reply ben,
Just a little more clarification that i want is:
In both the cases, ##1 will be always with respect to clock 2 only, is that correct understanding?
Is there a reasoning as to why the ##2 or above is not allowed after the implication in these cases ?
sequence_expr |=> property_expr // is equivalent to:
sequence_expr ##1 `true |-> property_expr
// Thus
ap1: assert property(@(posedge clk1) $rose(a) |=> @(posedge clk2) b); // equivalent to
ap1: assert property(@(posedge clk1) $rose(a) ##1 1'b1 |-> @(posedge clk2) b); // same as
ap1: assert property(@(posedge clk1) $rose(a) ##1 @(posedge clk1) 1'b1 // clock flow through
|-> @(posedge clk2) b);
/* 1800'2017 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
//[Ben] The following should be legal though
@(posedge clk1) s1 ##1 '1b1 ##1 @(posedge clk2) s2
// equivalent to
sequence s1b;
@(posedge clk1) s1 ##1 1'b1;
endsequence
@(posedge clk1) s1b ##1 @(posedge clk2) s2
As to why? Amybe to keep it simple as there are other ways to clearly express the intent.