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

SystemVerilog
, ,
1

Hey All ,
I am having some trouble understanding why we would use the implication operator which can lead to vacuous passess when instead we have the ollowed by operator in SVA ? Isn’t the whole point of adding an assertion is to check for both antecedent & consequents to be satisfied in the assertion? Why is implication still used ?

EDIT: I think I should also add on to the point that this is specifically in a properly where we check for the antecdent to be true to evaluate the consequent shouldn’t =-= be the default usage instead of !-> ? Will be there any performance penalties for waiting on both consequence & antecedent to be true ?

2

In reply to pkumar16:

You need to understand that an assertion attempts to satisfy a property every clock cycle.

If you just had

assert property (@(posedge clk) A ##1 B;)

This says on every clock edge A must be true AND B must be true the next cycle. So effectively A must be true EVERY clock cycle, and B must be true EVERY. clock cycle except for the first.

By using an implication, you are saying that it’s OK that A is true or false any clock cycle, but on the cases when it’s true, B must be true the next clock cycle.

assert property (@(posedge clk) A |=> B;)

It’s possible that A was never true, and you would need to write another kind of assertion to make sure that it does, if that is your requirement. When you collect coverage, you can also detect that the consequent never passed.

3

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
4

Hi @pkumar16 ,
followed-by operators #-#, #=# don’t mean implication. That is, signals’ behavior is evaluated at each cycle unless implication operators are added before them. Moreover, they don’t have strong attribute. Refer to the following post.

1 Like