SVA: Use of implication (|=>) vs sequence?

0
votes

SystemVerilog Assertion properties can be built with implication operators |=> and sequences ##1

For example :

property P1;
  @(posedge clk)
    A ##1 B |=> C ##1 D;
endproperty

Above we have used A ##1 B as an enabling sequence (antecedent) and C ##1 D as the fulfilling sequence (consequent).

I do not see why it could not be rewritten as :

property P2;
  @(posedge clk)
    A ##1 B ##1 C ##1 D;
endproperty

When and why would you choose implication |=> over a sequence ##1 ?

1
system-verilogverificationassertionssystem-verilog-assertions
This isn't Verilog - what's the etiquette around here for changing question tags? - EML
I think most people would just edit the question, and leave a clear 'edit summary'. Also not sure how much we distinguish between verilog and SystemVerilog these days since the LRMs were rolled in to one. - Morgan

1 Answers

1
votes

The above properties are the same for the sequence passing, however the failure conditions do not match.

If they are all 1's then A ##1 B ##1 C ##1 D; and A ##1 B |=> C ##1 D; are true.

If we have A as 1 then the rest 0's:

A ##1 B ##1 C ##1 D; fails and A ##1 B |=> C ##1 D; would pass.

The latter is not considered a failure due to the conditions of the enabling sequence not being met.