##
* 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 signal "a" is not high on any given positive clock edge, an error is issued by the checker.

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

*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 *

*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.

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);

####
* Non-overlapped implication *

*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.

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);

__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);

__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 starts 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);

__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);

__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);

__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 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);