Why can't we use followed by instead of implication operator in SVA as the default operator?

In reply to dave_59:
The Followed-by operators, #-#, #=#, allow ths concatenating a sequence and a property. It is useful in many cases. From my book SVA Handbook 4th Edition

The following represents an application example of the followed-by operator.
A processor needs to initiate the data transfer from an external bus onto its internal memory via DMA. The processor starts two consecutive actions: 1) a DMA request followed by a DMA acknowledge to get the memory transfer setup ready, and then 2) an optional external bus request followed by a bus acknowledge to start the data transfers over the bus interface. Thus, following the DMA acknowledge they may or may not be a bus request. If there is no bus request, then this might be because the processor is handling another higher priority process, and an assertion of this activity is vacuous.


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) |=>  // property antecedent and implication operator 
       (dma_req ##[1:3] dma_ack) // followed-by antecedent 
              #=# p_BusAccess(req, ack)); // followed-by consequent 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy