If I were to write property as :
property multi_edge ;
@( posedge clk ) ( 1 , $display(" Tpos = " , $realtime ) ) ##0 @( negedge clk ) ( 1 , $display(" Tneg = " , $realtime ) )
|-> ( 1 , $display(" T = " , $realtime ) ) ;
endproperty
assert property ( multi_edge ) ;
(a) I notice that without ##0 between @( posedge clk ) and @( negedge clk ) a Compilation Error is observed .
[Q1] Without ##0 wouldn’t the meaning remain the same i.e wait till subsequent negedge of clk ?
(b) Since the last edge is @( negedge of clk ) the overlapping implication operator would ensure the consequent is evaluated on Same negedge of clk .
[Q2] So does this mean the last edge in the consequent decides when the consequent is evaluated ?
(c) On changing property expression to :
@( posedge clk ) ( 1 , $display(" Tpos = " , $realtime ) ) ##0 @( Sig ) ( 1 , $display(" Sig changes at " , $realtime ) )
|=> ( 1 , $display(" Next Sig changes at " , $realtime ) ) ;
Since the last edge is @( Sig ) this would mean the Consequent is evaluated whenever Sig changes for the 2nd time , right ?
In reply to hisingh:
For [Q1].,
Without ##0 , it is meaning as @(posedge clk) and @(negedge clk) at same time , which seems like contradiction statement.
For [Q2].,
Last edge in the anticedent decides when the consequent should be evaluted in assosiation with implication operator.
In reply to iamyash1234:
@( posedge clk ) @( negedge clk ) |-> ... is Legal and equivalent to :: @( negedge clk ) |-> ...
In reply to hisingh:
For Q1, This is more of a syntax issue. ##0 and ##1 are a sequence concatenation operators. Event controls can only be placed at the beginning of a sequence expression. Each each sequence expression can only have one clock. You need to use concatenation to have multiple clocks. In your example there is no difference between ##0 or ##1 because the posedge and negedge can never overlap.
For Q2, since you used the non-overlapping implication operator |=>, the consequent starts on the next @(Sig) event.
In reply to dave_59:
Thanks Dave .
Event controls can only be placed at the beginning of a sequence expression. Each each sequence expression can only have one clock. You need to use concatenation to have multiple clocks.
This answers [Q1].
There is no difference between ##0 or ##1 because the posedge and negedge can never overlap.
Thanks for pointing this as well !!
In reply to dave_59:
Hi Dave ,
As you pointed :
- Event controls can only be placed at the beginning of a sequence expression.
- Each each sequence expression can only have one clock.
Event control : @( posedge clk0 ) is placed at the beginning of sequence expression A whereas
event control : @( posedge clk1 ) is placed at the beginning of sequence expression B .
So why is sequence concatenation even required ? They are 2 separate sequence expressions , right ?
If I were to write :
@( posedge clk0 ) A ##2 B ;
Now there is only one event control i.e @( posedge clk0 ) whereas we have 2 sequence expressions A and B .
As a result we require sequence concatenation ##2 between the two sequences .
In reply to MICRO_91:
Because.
That is how the syntax is defined. You need some kind of sequence operator between two sequences. There is no implicit concatenation.