In reply to MICRO_91:
The and, or sequence operators require that both sequence be true and start at the same time.
sequence mclocks ;
@(posedge clk1) B and @(posedge clk2) C ; // Could be "or" operator as well
endsequence
ap0:assert property ( mclocks ) ; // Illegal , but why ?
// Here the leading clocking event is not clearly defined.
// Is it @(posedge clk1), or is it @(posedge clk2)
// However, with
ap1:assert property ( @(posedge clk0) A |=> mclocks ) ; // Legal
// It is equivalent to
ap1:assert property ( @(posedge clk0) A |=> @(posedge clk1) B and @(posedge clk2) C);
// @(posedge clk0) flows into both "and" sequences, thus equivalent to
ap1:assert property ( @(posedge clk0) A |=>
@(posedge clk0) ##0 @(posedge clk1) B and
@(posedge clk0) ##0 @(posedge clk2) C);
// BTW, this would have been legal too.
ap0:assert property ( @(posedge clk0) mclocks );
ap0:assert property ( @(posedge clk1) mclocks );
ap0:assert property ( @(posedge clk2) mclocks );
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
Hi Ben ,
(1) I am intrigued by the concept of leading clock in a multi clocked sequence and seek your assistance for the same .
Here’s what I have noted via various trial and error :
The and, or sequence operators require that both sequence start at the same time
Generally when we write :
assert property ( @( posedge clk ) B and C ) ;
Here both B and C are evaluated on each posedge of clk i.e both sequence start at the same time i.e on posedge of clk
Whereas in the top multi clocked sequence :
assert property ( @(posedge clk1) B and @(posedge clk2) C ) ;
Here there exists ambiguity whether the variables B and C start evaluation on posedge of clk1 OR at posedge of clk2
**i.e sequence don't necessarily start at the same time**
On changing code to :
ap1:assert property ( @(posedge clk0) A |=> mclocks ) ;
Now variables B and C start at the same time i.e subsequent posedge of clk1 and clk2 respectively **after the antecedent is True on leading clock ( clk0 )**
I still observe Compilation Error : [edalink](https://www.edaplayground.com/x/Vnr9)
I believe this is due to the clk0 / clk1 / clk2 ( mentioned in the assert property ) getting overridden by clk1 for B and clk2 for C ( within the sequence ) .
So the equivalent expression remains the same :
In reply to MICRO_91:
The key to understanding multiclocking is to understand that a clock flow into a parenthesized (or declared) sequence, but it does not flow out of it. I explain clock flow in my book. Here is a section of it.
ap1a:assert property ( @(posedge clk0) A |=> mclocks ) ; // *** ILLegal
// ILLEGAL by tool vendors. I thought that the clock would flow into the sequence
//BUT the following is OK
ap1b:assert property ( @(posedge clk0) A |=> (@(posedge clk1) B and @(posedge clk2) C));
Thus,
module lce;
bit clk, clk0, clk1, clk2, a, b, c, d, e;
initial forever #10 clk=!clk;
// Illegal, no leading clocking event
ap_and2_seq_ERROR: assert property(
(@ (posedge clk) a ##1 b) and
(c ##2 d) // illegal
);
// Illegal, no leading clocking event
// both sequences start concurrently
ap_and2_seq_ERROR2: assert property(
(@ (posedge clk) a ##1 b) and
(@ (posedge clk2) c ##2 d)
); // has multiple leading clocks for its maximal property
// OK, one leading clocking event
ap_and2ab: assert property(@ (posedge clk0) 1|->
(@ (posedge clk) a ##1 b) and
(@ (posedge clk2) c ##2 d)
);
// Illegal, no leading clocking event
// both properties start concurrently
ap_and2_Prop_ERROR: assert property(
(@ (posedge clk) 1 |-> a ##1 b) and
(@ (posedge clk2) 1 |-> c ##2 d)
);
// OK, Same leading clocking event
// both properties start concurrently
ap_and2_Prop_OK_same_clk: assert property(
(@ (posedge clk) 1 |-> a ##1 b) and
(@ (posedge clk) 1 |-> c ##2 d)
);
ap_and2_Prop_OK: assert property(@ (posedge clk0) 1 |->
(@ (posedge clk) 1 |-> a ##1 b) and
(@ (posedge clk2) 1 |-> c ##2 d)
);
ap_mult_clk: assert property(
@ (posedge clk1) a [*0:1] ##1 // illegal a[*0] is empty
@ (posedge clk2) b[*0:2] ##1 c); // illegal b[*0] is empty
endmodule : lce
The key to understanding multiclocking is to understand that a clock flow into a parenthesized (or declared) sequence, but it does not flow out of it. I explain clock flow in my book.
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 ?
(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
(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 .
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!
:)
Have a question regarding the consequent as mclocks.
When mclocks is declared as a property it works whereas there is a compilation error on declaring mclocks as a sequence : edalink
This an interesting difference between sequence and a property , however I am not clear on the reason behind it .
In reply to MICRO_91:
Good question!
I modified your code to include the qmclocs for sequence, and pclocks for property.
The key as to why comes from the following warning given by a tool:
*** Warning: testbench.sv(6): (vlog-2047) Sequence/SERE ‘qclocks’ declared in ‘property_VS_Seq’ has multiple leading clocks. Such
sequence/SERE cannot be instanced asmaximal property of a directive.*
The key as to why if provided by this tool warning:
** Warning: testbench.sv(6): (vlog-2047) Sequence/SERE ‘qclocks’ declared in ‘property_VS_Seq’ has multiple leading clocks. Such sequence/SERE cannot be instanced as [b]maximal property of a directive.[/b]
1800’2017: the term maximal property, used in the rules below, is defined as the unique flattened property contained in the assertion statement and obtained by applying the rewriting algorithm in F.4.1 a)
labeled page 376: A multiclocked sequence or property can inherit the default clocking event as its leading clocking event. If a multiclocked property is the maximal property of a concurrent assertion statement, then the property shall have a unique semantic leading clock (see 16.16.1 ). 16.16.1 Semantic leading clocks for multiclocked sequences and properties.
Throughout this subclause, s, s1, and s2 denote sequences without clocking events; p, p1, and p2 denote properties without clocking events; m, m1, and m2 denote multiclocked sequences, q, q1, and q2 denote multiclocked properties; and c, c1, and c2 denote nonidentical clocking event expressions.
A multiclocked sequence has a unique semantic leading clock, defined inductively as follows:
…
— The semantic leading clock of (m) is equal to the semantic leading clock of m.
— The semantic leading clock of m1 ##1 m2 is equal to the semantic leading clock of m1.
— The semantic leading clock of m1 ##0 m2 is equal to the semantic leading clock of m1.
[Ben] I still don’t see the answer here. I am asking the question to some 1800 colleagues and to one vendor. I’ll get back to you when I get an answer.
Obviously this is getting into the deeper definitions and restrictions of 1800…
… an interesting world!
:)
Another way of thinking is considering that assertion expressions are made from building up three layers of abstractions: booleans, sequences, and properties. When parsing the syntax of an expression, it starts at the top level looking a property, then sequence and finally a boolean expression. Note that a boolean expression by itself can be used as a single cycle sequence, and a sequence by itself can be used as a property, but the reverse is not always possible.
The and and or operators can be used for both property and sequence expressions. If one or both operands of these operators are properties, then it is considered a property operator. However, the body of a named sequence cannot contain any properties. As a result, the compiler immediately considers these as operations on sequences.
The and and or operators can be used for both property and sequence expressions. If one or both operands of these operators are properties, then it is considered a property operator. However, the body of a named sequence cannot contain any properties. As a result, the compiler considers these as operations on sequences and will not allow operands with leading clocked edges as operands to the and and or sequence operators.
In reply to ben@SystemVerilog.us:
… However, the body of a named sequence cannot contain any properties. As a result, the compiler considers these as operations on sequences and will not allow operands with leading clocked edges as operands to the and and or sequence operators.
I am still puzzled because ap_qclocks is identical to ap_qclocks_expanded
Yet the compiler (all vendors) accepts ap_qclocks_expanded but not ap_qclocks.
From what you say, ap_qclocks considers the qclocks as a property though it is
specified as a sequence from its declaration. COrrect me if I am wrong,
ap_qclocks_expanded: assert property ( @( posedge clk0 ) A |=>
(@(posedge clk1) B and @(posedge clk2) C))
// IS EXPANDED AS
ap_qclocks_expanded_compiler: assert property ( @( posedge clk0 ) A |=>
(@(posedge clk0) @(posedge clk1) B and @( posedge clk0 ) @(posedge clk2) C))
// Thus ONE leading clocking event (LCE).
// My question to you, why does the compiler NOT expand or flatten ap_qclocks to be ap_qclocks_expanded.
// Yet in
ap_pclocks: assert property ( @( posedge clk0 ) A |=> pclocks )
$display("TIME:%2t Assertion ap_pcloks PASSes" , $time);
// the compiler expands or flattens the pclocks as a sequence that is a property.
Please clarify “As a result, the compiler considers these as operations on sequences and will not allow operands with leading clocked edges as operands to the and and or sequence operators.” OK on ap_qclocks_expanded but not OK on ap_qclocks?
Also OK on ap_pclocks: assert property ( @( posedge clk0 ) A |=> pclocks )
???
One more Q: Where in 1800 does it address this?
16.16.1 Semantic leading clocks for multiclocked sequences and properties.
does not address this.
Thanks,
Ben
