simulationsystem-verilogformal-verificationsystem-verilog-assertions

What is the difference between ##1 and |=> in System Verilog assertions and if statement vs assert statement?

Are there major differences between using ##1 and |=> in System Verilog assertions

A ##1 B and A => B. When do they behave similarly, and when do they differ? For example

property p_a_then_b;
  a ##1 b;  
endproperty

versus

property p_a_implies_b;
  a |=> b;  
endproperty

The second question is when to use an if statement vs an assert statement.

if (a==b)
 $display("pass");
else
$error("Error");

versus

assert(a == b);

All these questions are in the context of simulation-based verification. Would anything change if the context is Formal verification?

Solution

  • They are very different.

    ##1 is a sequence operator that joins two sequences between cycles.

    |=> is a property operator that joins a sequence (antecedent) conditionally with a property (consequence).

    With a ##1 b, b is restricted to being a sequence (or boolean expression). When used as an assertion, if a is false, the assertion fails.

    When used as an assertion a |=. b, if a is false, the assertion passes (vacuous success).

    Formal tools only try to prove assert statements, not if statements.