Evaluation of following Multi-clocked sequence

SystemVerilog
, ,
1

Hi All ,
Syntax 16-16 of the LRM tells us that a sequence expression is by default a property expression.

eg1:assert property( @(posedge clk) sig1 ##1 sig2 );

The above is an example of a sequence that is used as a property

LRM 16.13.2 states Multiclocked sequences are themselves multiclocked properties.

eg2:assert property( @(posedge clk1) sig1 ##1 @(posedge clk2) sig2 );

[Q1] Can I state that eg2 is an example of multi-clocked sequence that is used as a multi-clocked property ?

On trying the following multiclocked expression

//  What is the LHS of 'and' ? Is it @(posedge clk1) b [ OR ] @(posedge clk0) a ##1 @(posedge clk1) b  ?
eg3:assert property( @(posedge clk0) a ##1 @(posedge clk1) b  and @(posedge clk2) c );

I expected that leading clock would be clk0 and then at the nearest subsequence posedge of clk1 / clk2 there would be an ‘and’ operation, however I observe a compilation error.

[Q2] Is the error because the LHS of ‘and’ operator is @(posedge clk0) a ## 1 @(posedge clk1) b ?
Since ‘and’ / ‘or’ / ‘intersect’ operators are illegal for multiclocked sequences , the code is termed illegal.

Note : One solution for eg3 is to replace ## 1 with followed-by property operator ( #=# / #-# )

2 
eg2:assert property( @(posedge clk1) sig1 ##1 @(posedge clk2) sig2 );

[Q1] Can I state that eg2 is an example of multi-clocked sequence that is used as a multi-clocked property ?
[Ben] YES

[Q1] On trying the following multiclocked expression
eg3:assert property( @(posedge clk0) a ##1 @(posedge clk1) b and @(posedge clk2) c );
// What is the LHS of ‘and’ ? Is it @(posedge clk1) b [ OR ]
// @(posedge clk0) a ##1 @(posedge clk1) b ?
I expected that leading clock would be clk0 and then at the nearest
subsequence posedge of clk1 / clk2 there would be an ‘and’ operation, however I observe a compilation error.
[Ben] I see it as
(@(posedge clk0) a ##1 @(posedge clk1) b) and
(@(posedge clk2) c );
There is no singly clock to both properties that must start at the same leading clocking event.

[Q2] Is the error because the LHS of ‘and’ operator is @(posedge clk0) a ## 1 @(posedge clk1) b ?
Since ‘and’ / ‘or’ / ‘intersect’ operators are illegal for multiclocked sequences , the code is termed illegal.

Note : One solution for eg3 is to replace ## 1 with followed-by property operator ( #=# / #-# )
[Ben] The following works

 // ( @(posedge clk0) a ##1 @(posedge clk1) b  and @(posedge clk2) c );
  eg3_ok:assert property(@(posedge clk0) 1 |-> 
   (@(posedge clk0) a ##1 @(posedge clk1) b) and 
   (@(posedge clk2) c)); 
    
  eg3:assert property( 
   (@(posedge clk0) a ##1 @(posedge clk1) b) and 
   (@(posedge clk0) 1 ##0 @(posedge clk2) c));
3

Thanks Ben.

There is no singly clock to both properties that must start at the same leading clocking event.

The error message differs across tools. Some treat it as multi-clocked sequence and throw an error for invalid ‘and’ operator used in a multi-clocked sequence while only one tool correctly identifies the issue as absence of leading clock.