Regarding 'followed by' property #=#

SystemVerilog
,
1

Consider the following SVA:


  bit clk , a , b ;
  
  always #5 clk = !clk;
  
  property prop;
    @(posedge clk)  a #=# b ;
  endproperty
  
  assert property( prop );

For assertion to pass , a should be sampled true at T:5 and then at next posedge at T:15 , b should be true.
If a is false at T:5 the assertion fails at T:5.
If a is true at T:5 and b is false at T:15, the assertion fails at T:15

I am trying to understand the difference between above code and the following:


  property prop_alt;
    @(posedge clk)  a ##1 b ;
  endproperty
2

In reply to MICRO_91:
The followed-by operators #-# and #=# concatenate a sequence and a property. The followed-by operators are of the following forms for the definition of a property:


property_expr ::=  
 ...
 | sequence_expr |-> property_expr  // same cycle 
 | sequence_expr #-# property_expr  // same cycle 

 | sequence_expr |=> property_expr  // next cycle  
 | sequence_expr #=# property_expr  // next cycle 

// Example from my SVA book: 
property p_BusAccess (bus_req, bus_ack);    
  (bus_req  |-> ##[1:7]  bus_ack); 
endproperty : p_BusAccess         
ap_DMA_BusAccess : assert property(@ (posedge clk) 
           $rose(dma_command) |=> (dma_req ##[1:3] dma_ack) // sequence 
                                      #=#  p_BusAccess(req, ack)); // property

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

3

In reply to ben@SystemVerilog.us:

The followed-by operators #-# and #=# concatenate a sequence and a property.

I was trying to understand the meaning/interpretation of your above quote.
One application I could think of is that property is illegal in RHS of ‘##’ ( clock delay ) expression


  property p1;
    d ##1 e ;  
  endproperty    
  property prop;
    @(posedge clk) a |=> (b ##1 c) ##0 p1 ; // .. ##0 p1 / .. ##1 p1 are both Illegal
  endproperty  
  assert property( prop );

whereas if I were to write ::


  property p1;
    d ##1 e ;  
  endproperty    
  property prop;
    @(posedge clk) a |=> (b ##1 c) #-# p1 ; // .. #-# p1 / .. #=# p1 are both legal
  endproperty  
  assert property( prop );

So the clock delay ‘##’ property restriction can be bypassed using ‘followed_by’ property.
However for ##2/##3/## N property, I would need to split it to ##( N-1) 1 #=# property / ##N 1 #-# property

[Q1] Is there anything else might be missing out on (from your above quote) ?


LRM 16.12.9 :: A followed-by operator is especially convenient for specifying a cover property directive over a sequence followed by a property.

[Q2] Could you elaborate on this please ?

4

In reply to MICRO_91:
If you want to follow the end point of a sequence by a property, then you nee the followed-by operator; it’s that simple.
seq1 #-# prop says that at the endpoint of seq1 you start prop in the same cycle.
seq1 #=# prop says that at the endpoint of seq1 you start prop in the next cycle.
If you want prop to start 10 cycles after the endpoint of seq1, you would need to extend the endpoint of seq1 by 10 cycles.
seq1 ##10 1 #-# prop says that at the endpoint of the sequence
(seq1 ##10 1) you start prop in the same cycle.
You can think of it as a sort of concatenation of a sequence and a property.
Something like (by syntactically incorrect) {seq1, prop}
Ben