Implication Operator

sequence seq;
  @(posedge clk) a ##2 b;
endsequence

In the above sequence, we can observe that sequence starts on every positive edge of the clock and it looks for “a” to be high on every positive clock edge. If the signal “a” is not high on any given positive clock edge, an error is issued by the checker.

If we want the sequence to be checked only after “a” is high, this can be achieved by using the implication operator.

The implication is equivalent to an if-then structure. The left-hand side of the implication is called the “antecedent” and the right-hand side is called the “consequent.” The antecedent is the gating condition. If the antecedent succeeds, then the consequent is evaluated.

The implication construct can be used only with property definitions. It cannot be used in sequences.

There are 2 types of implication:

• Overlapped implication
• Non-overlapped implication

Overlapped implication

The overlapped implication is denoted by the symbol |->.

If there is a match on the antecedent, then the consequent expression is evaluated in the same clock cycle.

Below property checks that, if signal “a” is high on a given positive clock edge, then signal “b” should also be high on the same clock edge.

property p;
  @(posedge clk) a |-> b;
endproperty
a: assert property(p);

Click to execute on   

Non-overlapped implication

The non-overlapped implication is denoted by the symbol |=>.

If there is a match on the antecedent, then the consequent expression is evaluated in the next clock cycle.

Below property checks that, if signal “a” is high on a given positive clock edge, then signal “b” should be high on the next clock edge.

property p;
  @(posedge clk) a |=> b;
endproperty
a: assert property(p);

Click to execute on   

The implication with a fixed delay on the consequent

Below property checks that, if signal “a” is high on a given positive clock edge, then signal “b” should be high after 2 clock cycles.

property p;
  @(posedge clk) a |-> ##2 b;
endproperty
a: assert property(p);

Click to execute on   

The implication with a sequence as an antecedent

Below property checks that, if the sequence seq_1 is true on a given positive edge of the clock, then start checking the seq_2 (“d” should be low, 2 clock cycles after seq_1 is true).

sequence seq_1;
 (a && b) ##1 c;
endsequence

sequence seq_2;
  ##2 !d;
endsequence

property p;
  @(posedge clk) seq_1 |-> seq_2;
endpeoperty
a: assert property(p);

Click to execute on   

Timing windows in SVA Checkers

Below property checks that, if signal “a” is high on a given positive clock edge, then within 1 to 4 clock cycles, the signal “b” should be high.

property p;
  @(posedge clk) a |-> ##[1:4] b;
endproperty
a: assert property(p);

Click to execute on   

Overlapping timing window

Below property checks that, if signal “a” is high on a given positive clock edge, then signal “b” should be high in the same clock cycle or within 4 clock cycles.

property p;
  @(posedge clk) a |-> ##[0:4] b;
endproperty
a: assert property(p);

Click to execute on   

Indefinite timing window

The upper limit of the timing window specified in the right-hand side can be defined with a “$” sign which implies that there is no upper bound for timing. This is called the “eventuality” operator. The checker will keep checking for a match until the end of the simulation.

Below property checks that, if signal “a” is high on a given positive clock edge, then signal “b” will be high eventually starting from the next clock cycle.

property p;
  @(posedge clk) a |-> ##[1:$] b;
endproperty
a: assert property(p);

Click to execute on   

❮ Previous Next ❯