In reply to ben@SystemVerilog.us:
Hi Ben ,
Quote:
16.13.1 Multiclocked sequences (Page 447)
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
This quote is specifically for a multiclocked sequence :
sequence mclocks_seq;
@(posedge clk0) a ##2 @(posedge clk1) B ; // This is a sequence_expression as property_expression is invalid within a sequence body
endsequence
assert property ( mclocks_seq ) ;
However if I were to declare 'mclocks_seq' as property , I observe it's also invalid
property mclocks_prop;
@(posedge clk0) a ##2 @(posedge clk1) B ; // This is a property_expression
endproperty
assert property ( mclocks_prop ) ;
I went through LRM for this and I noted the following . Please correct me if wrong :
(1) Syntax 16-16—Property construct syntax :
property_expr ::=
sequence_expr
[Q1]This means all sequence_expressions are implicitly property_expressions , right ?
(2) 16.13.1 Multiclocked sequences :
If s1, s2 are sequence expressions with no clocking events, then the multiclocked sequence
@(posedge clk1) s1 ##1 @(posedge clk2) s2
is legal only if neither s1 nor s2 can match the empty word.
(3) 16.13.2 Multiclocked properties :
Multiclocked sequences are themselves multiclocked properties. For example:
@(posedge clk0) sig0 ##1 @(posedge clk1) sig1
is a multiclocked property. If a multiclocked sequence is evaluated as a property starting at some point, the
evaluation returns true if, and only if, there is a match of the multiclocked sequence beginning at that point.
Via (2) and (3) :
@(posedge clk1) s1 ##1 @(posedge clk2) s2
This is a multiclocked sequence .
Since a sequence is also a property , it can also be said that it's a multiclocked property
Hence when 16.13.1 Multiclocked sequences says that :
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
So to summarize :
- Sequence concatenation operator '##' is used between two sequence_expressions.
It doesn't apply for only a sequence,it could be applied between 2 property_expression as well ( as a sequence_expr is also a property_expr by default )
- A multiclocked sequence has clocking event Eg. @( posedge clk1 ) / @( posedge clk2 ) at the start of the sequence_expression.
- Via (1) since a sequence_expression is also a property_expression , ##2 is illegal even for a property_expression
