Implication Operator in Assertions

In SystemVerilog Assertions (SVA), the implication operator is a powerful construct used to establish a cause-and-effect relationship between conditions. It ensures that when a certain condition (antecedent) holds true, another condition (consequent) must follow, either immediately or after a delay. This article delves into the two types of implications—overlapped and non-overlapped—with detailed explanations and examples.

Implication in Assertions

The implication operator in SystemVerilog comes in two forms:

Overlapped Implication (|->): Indicates that the consequent condition must hold starting in the same clock cycle as the antecedent.
Non-Overlapped Implication (|=>): Indicates that the consequent condition must hold starting in the clock cycle immediately after the antecedent completes.

Syntax

antecedent |-> consequent; // Overlapped Implication
antecedent |=> consequent; // Non-Overlapped Implication

Overlapped Implication (`|->`)

The overlapped implication asserts that whenever the antecedent condition is true, the consequent condition must hold starting in the same clock cycle.

Example: Simple Overlapped Implication

property overlapped_implication_example;
  @(posedge clk) req |-> ack;
endproperty

In this example:

Antecedent (req): The request signal must be asserted.
Consequent (ack): The acknowledgment signal must also be true in the same cycle as the request signal.

If req is high at a rising edge of clk, the assertion checks that ack is also high in the same cycle.

Complete code:

module test;

  // Signals
  reg clk;
  reg req;
  reg ack;

  // Clock generation
  initial clk = 0;
  always #5 clk = ~clk; // 10ns clock period

  // Stimulus generation
  initial begin
    req = 0;
    ack = 0;

    // Apply stimulus
    #15 req = 1; ack = 1; //both asserted at 15ns
    #10 req = 0; 

    #20 req = 1; // req again asserted at time 45ns
    #10 ack = 0; // ack deasserted at time 65ns

    #20 $finish; // End simulation
  end

  // Property
  property overlapped_property;
    @(posedge clk) req |-> ack;
  endproperty

  // Assertion
  assert property (overlapped_property) $display("assertion got passed at %0t", $time);
    else $error("overlapped_property failed at time %0t", $time);
    
    initial begin
      $dumpfile("test.vcd");
      $dumpvars();
    end

endmodule

assertion is passing at 25 and 55ns as both are high at the same cycle in the waveform.

Waveform:

Non-Overlapped Implication (`|=>`)

The non-overlapped implication asserts that whenever the antecedent condition is true, the consequent condition must hold starting in the next clock cycle.

Example: Simple Non-Overlapped Implication

module test;

  // Signals
  reg clk;
  reg req;
  reg ack;

  // Clock generation
  initial clk = 0;
  always #5 clk = ~clk; // 10ns clock period

  // Stimulus generation
  initial begin
    req = 0;
    ack = 0;

    // Apply stimulus
    #15 req = 1;  
    #10 ack = 1; 

    #20 req = 0; // req deasserted at time 45ns
    #10 ack = 0; // ack deasserted at time 65ns

    #20 $finish; // End simulation
  end

  // Property
  property non_overlapped_property;
    @(posedge clk) req |=> ack;
  endproperty

  // Assertion
  assert property (non_overlapped_property) $display("assertion got passed at %0t", $time);
    else $error("non_overlapped_property failed at time %0t", $time);
    
    initial begin
      $dumpfile("test.vcd");
      $dumpvars();
    end

endmodule

Here assertion will pass at 35 and 45ns as ack is high after one clock cycle of req.

Waveform

Using Implications with Sequences

The implication operators can also work with sequences instead of simple conditions, enabling more complex temporal relationships.

Example: Overlapped Implication with a Sequence

sequence req_ack_sequence;
  req ##1 data_valid;
endsequence

property overlapped_sequence_example;
  @(posedge clk) req |-> req_ack_sequence;
endproperty

In this property:

If req is asserted, the sequence req_ack_sequence must hold, meaning req is followed by data_valid in the next cycle.

Example: Non-Overlapped Implication with a Sequence

sequence data_transfer_sequence;
  req ##1 grant ##1 data_transfer;
endsequence

property non_overlapped_sequence_example;
  @(posedge clk) start |=> data_transfer_sequence;
endproperty