Hi ,
I am trying to understand the difference in following 2 codes :
// CODE 1 : Using Non-Overlapping Implication
property multi_clocks1 ;
@(posedge clk0) A |=> ##0 @(posedge clk1) B ;
endproperty
V/S
// CODE 2 : Using Overlapping Implication
property multi_clocks2 ;
@(posedge clk0) A |-> ##0 @(posedge clk1) B ;
endproperty
Consider the following 2 cases :
(a) posedge of clk0 occurs at t0 whereas posedge of clk1 is false at t0 :
If ‘A’ is true at T:t0 , when would ‘B’ be evaluated ?
(b) Both posedge of clk0 and clk1 overlap at t1 :
If ‘A’ is true at T:t1 , when would ‘B’ be evaluated ?
From the output I observe , can I state that the 2 property expressions are equivalent to :
// CODE 1 : Using Non-Overlapping Implication :
@(posedge clk0) A |=> @(posedge clk1) B;
// CODE 2 : Using Overlapping Implication :
@(posedge clk0) A |-> @(posedge clk1) B;
In reply to MICRO_91:
Consider the following 2 cases :
// CODE 1 : Using Non-Overlapping Implication :
@(posedge clk0) A |=> @(posedge clk1) B;
// CODE 2 : Using Overlapping Implication :
@(posedge clk0) A |-> @(posedge clk1) B;
// **** (a) posedge of clk0 occurs at t0 whereas posedge of clk1 is false at t0 :
// If 'A' is true at T:t0 , when would 'B' be evaluated ?
// [Ben] Code 1: B is evaluated at the next posedge clk1
// Code 2: B is evaluated at the next posedge clk1
// **** (b) Both posedge of clk0 and clk1 overlap at t1 :
// If 'A' is true at T:t1 , when would 'B' be evaluated ?
// [Ben] Code 1: B is evaluated at the next posedge clk1
// Code 2: B is evaluated at the current posedge clk1, which is
// the same time step as posedge clk0
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
Hi Ben ,
I do understand the working without using ##0 in the consequent . Does the addition of ##0 change the behavior compared to without it ?
Can I say that the below property expressions are equivalent ?
property multi_clocks1 ;
@(posedge clk0) A |=> ##0 @(posedge clk1) B;
endproperty
property multi_clocks2 ;
@(posedge clk0) A |=> @(posedge clk1) B; // Without ##0 in consequent
endproperty
// [Q1] Are multi_clocks1 and multi_clocks2 equivalent ?
Similarly
property multi_clocks3 ;
@(posedge clk0) A |-> ##0 @(posedge clk1) B;
endproperty
property multi_clocks4 ;
@(posedge clk0) A |-> @(posedge clk1) B; // Without ##0 in consequent
endproperty
// [Q2] Are multi_clocks3 and multi_clocks4 equivalent ?
1800 is clear on multi_clocks2 and multi_clocks4.
1800 pg 446
Example 2: @(posedge clk0) sig0 ##0 @(posedge clk1) sig1
A match of this sequence starts with a match of sig0 at posedge clk0. Then ##0 moves the time to the nearest possibly overlapping posedge clk1, and the match of the sequence ends at that point with a match of sig1: if posedge clk0 and posedge clk1 happen simultaneously then the time does not move at ##0, otherwise, it behaves as ##1.
If clk0 and clk1 are not identical, then the clocking event for the sequence changes after ##0. If clk0 and clk1 are identical, then the clocking event does not change after ##0, and the preceding sequence is equivalent to the following singly clocked sequence: @(posedge clk0) sig0 ##0 sig1 which is equivalent to the following: @(posedge clk0) sig0 && sig1
1800 pg 448
For example, if s0 and s1 are sequences with no clocking events, then
@(posedge clk0) s0 |-> @(posedge clk1) s1
means the following: at each match of s0 the nearest posedge clk1 is awaited. If it happens immediately then s1 is checked without delay, otherwise its check starts at the next posedge clk1 as in case with |=>. In both cases the evaluation of s1 is controlled by posedge clk1.
On property multi_clocks1 ;
@(posedge clk0) A |=> ##0 @(posedge clk1) B;
endproperty
property multi_clocks3 ;
@(posedge clk0) A |-> ##0 @(posedge clk1) B;
endproperty
There is a discrepancy among tool vendors as to how this is processed.
I strongly believe that
A |=> ##0 @(posedge clk1) B; // should be interpreted as
A |=> 1 ##0 @(posedge clk1) B;
In my model, which I’ll share a bit later,
B==1, A==1 at t5, clk0 goes to 1 at t6 and at t13
clk1 goes to 1 at t8 and at t13.
At 13, the next posedge clk0, it processes the “1” (because of the |=> 1).
Since posedge also occurred at t13, the ##0 @(posedge clk1) B causes the evaluation of B at t13.
Another tool behaves as if it interpreted
A |=> ##0 @(posedge clk1) B; as
A |=> @(posedge clk1) B; // thus evaluated B at t8, the next posedge clk1 after posedge of clk0.
I am currently in discussion with a colleague on this. Obviously, one (or more) of the vendors
has it wrong. Stay tuned …
Ben
In reply to ben@SystemVerilog.us:
My above understanding is correct. Let’s have a reiteration:
@(posedge clk0) A |=> ##0 @(posedge clk1) B;
is similar to writing @(posedge clk0) A |=> ##0 s; // where s is some sequence.
The ##0 is still on clk0 and is equivalent to @(posedge clk0) A |=> 1 ##0 s;[b]
I.e.,
@(posedge clk0) A |=> 1 ##0 @(posedge clk1) B;[/b]
There is a one clock cycle of clk0 before it starts searching for a tick of clk1,
which due to ##0 can occur at the same time as the 2nd tick of clk0.
@(posedge clk0) A |=> ##0 @(posedge clk1) B; // (multi_clocks1) k0n01+=1;
@(posedge clk0) A |=> @(posedge clk1) B; // (multi_clocks2) k0n1+=1;
@(posedge clk0) A |-> ##0 @(posedge clk1) B; //(multi_clocks3) k001+=1;
@(posedge clk0) A |-> @(posedge clk1) B; //(multi_clocks2) k01+=1;
multi_clocks1 and multi_clocks2 are not equivalent
multi_clocks3 and multi_clocks4 are not equivalent
I observe that all tools agree that these two are indeed equivalent ( tested for both non-overlapping as well as overlapping clocks ) :
property multi_clocks3 ;
@(posedge clk0) A |-> ##0 @(posedge clk1) B;
endproperty
property multi_clocks4 ;
@(posedge clk0) A |-> @(posedge clk1) B; // Without ##0 in consequent
endproperty
The discrepancy lies with multi_clocks1 and multi_clocks2 . Some tools agree with your explanation while others treat multi_clocks1 and multi_clocks2 as equivalent
The expected output would be clearer had the LRM discussed it. Hopefully it gets resolved in future versions of the LRM.
CORRECT BEHAVIOR: in the expressions below,
seq1: @(posedge clk0) A |=> ##0 @(posedge clk1) B
// same as
seq1_equiv: @(posedge clk0) A |=> @(posedge clk0) 1 ##0 @(posedge clk1) B
Question: when are these 2 assertions equivalent?
k0n01: @(posedge clk0) A |=> ##0 @(posedge clk1) B // is equivalent to
k0n01: @(posedge clk0) A |=> @(posedge clk0) 1 ##0 @(posedge clk1) B
k0n1 : @(posedge clk0) A |=> @(posedge clk1) B
k0n01 and kn01 would behave the same if the clocking event floowing the
first @(posedge clk0) is
@(posedge clk0 ) and then @(posedge clk1) or
@(posedge clk0) simulataneously with @(posedge clk1)
The reason: |=> @(posedge clk0) 1 ##0 @(posedge clk1) B
Following the |=> we’re waiting for(posedge clk0) followed by @(posedge clk1) B
A |=> ##0 @(posedge clk1) B; // should be interpreted as
A |=> 1 ##0 @(posedge clk1) B;
Then why is it that :
@(posedge clk0) A |=> @(posedge clk1) B; // 'B" evaluated on subsequent posedge of clk1
// Why is above not interpreted as
@(posedge clk0) A |=> 1 @(posedge clk1) B;
i.e in the latter case why doesn’t consequent evaluation wait for next posedge of clk0 before checking ‘B’ ?
Non-Overlapping Implication ( |=> ) is equivalent to ( |-> ##1 ) , right ?
