Working of Multiple edge in antecedent

SystemVerilog
,
1

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 ?

2

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.

3

In reply to iamyash1234:

@( posedge clk ) @( negedge clk )  |->  ...  is  Legal  and equivalent  to  :: @( negedge clk )  |->  ...
4

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.

5

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 !!

6

In reply to dave_59:

Hi Dave ,
As you pointed :

  1. Event controls can only be placed at the beginning of a sequence expression.
  2. 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 .

7

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.