In reply to MICRO_91:
In reply to ben@SystemVerilog.us:
Hi Ben ,
I do understand this part .
However I am still not clear on the concept of missing leading clock for :
sequence mclocks ;
@(posedge clk1) B and @(posedge clk2) C ; // Could be "or" operator as well
endsequence
ap0:assert property ( mclocks ) ; // Compilation Error ::
// Tool1 => Error-[SVA-SLCE] Single leading clock expected
// Tool2 => xmvlog: *E,CLKSVA : The clock for a concurrent assert statement must be completely specified.
Please correct me if my following understanding in incorrect :
As you mentioned : " The and, or sequence operators require that both sequence start at the same time "
My confusion : Is above quote related to leading clock ?
[Ben] Yes, every assertion needs a unique leading clocking event
(1) Legal Case :
sequence mclocks1 ;
@(posedge clk1) B and C ; // Could be "or" operator as well
endsequence
ap1:assert property ( mclocks1 ) ;
Here both sequence starts at same time i.e on posedge of clk1 which is basically the leading clock
[Ben] YES
(2) Illegal Case :
sequence mclocks ;
@(posedge clk1) B and @(posedge clk2) C ; // Could be "or" operator as well
endsequence
ap0:assert property ( mclocks ) ;
Here both sequences don’t start at the same time i.e missing leading clock
Whereas when I write :
ap2:assert property ( @(posedge clk0) A |=> mclocks ) ; // posedge of clk0 is the leading clock
Here both sequences start at the same time i.e nearest posedge of clk1 and clk2 after the antecedent is True on posedge of clk0 .
[Ben] Still illegal
ap1a:assert property ( @(posedge clk0) A |=> mclocks ) ; // *** ILLegal Line 10
Error-[SVA-CMISO] Clocks mismatch in sequence operator
testbench.sv, 10
top
Clocks mismatch in 'and' sequence operator.
Leading clock: posedge clk1
Sequence: (B and @(posedge clk2) C)
[Ben] the reason @(posedge clk0) A |=> mclocks is illegal
is because mclocks is interpreted as a property and NOT as a SEQUENCE!
HOWEVER,
ap1b:assert property ( @(posedge clk0) A |=> // line 13
(@(posedge clk1) B and @(posedge clk2) C)); /
The (@(posedge clk1) B and @(posedge clk2) C) is interpreted as a sequence
and the (posedge clk0) flows thru each of the terms of the and
Question: WHY? Seems that since the sequence declaration is the same as the content when it is expanded is the same?
The only explanation I can get (from an 1800’2017 colleague is because of
the associative rules. 1800’2017 Table 16-3—Sequence and property operator precedence and associativity shows that sequences have higher priority than properties.
When I use as the consequent the named sequence declaration (i.e., the mclocks),
it is interpreted as a propertythat does not have a unique leading clocking event (LCE).
If I use the internals of mclocks as the consequent, (i.e., (@(posedge clk1) B and @(posedge clk2) C) ) then the compiler sees it as a sequence and LCE is @(posedge clk0) that flows into each of the and sequences.
BOTTOM LINE: Tricky? yes. Be practical, and make sure that properties have a unique LCE.
If you make a mistake, the compiler will tell you and then just fix it!
:)