Nested Implication

SystemVerilog
, , ,
1

This is question regarding an example cited in the book, [“Boolean Sequences.” SVA - the Power of Assertions in Systemverilog. 2nd ed. Springer, 2014.]

For a sequence if start is asserted, then 2 clocks later send is asserted, then 3 clocks after send, ack should be asserted, the book suggests 2 equivalent ways :

  1. Nested suffix implication
   assert property (@(posedge clk) 
       start |-> ##2 send |-> ##3 ack );
  1. Using single suffix implication
   assert property (@(posedge clk)
       start ##2 send |-> ##3 ack );

My doubt is, I dont think the 2 methods would be equivalent (or would they???). In the method 1, the assertion will fail, even if we don’t receive “send” 2 clk ticks after start while the condition is to only assert that ack is received 3 clk ticks after the condition (start ##2 send) is met. Using method 2 (single suffix implication) makes more sense, since the property would not fail even if send is not asserted 2 clk ticks after start.

Please let me know if this is wrong… Are the two methods equivalent?

Thanks,
Priyank

2

In both cases, after a successful attempt (i.e., start==1) if send is false 2 ticks later, the assertion is vacuous. In the 2nd case (start ##2 send |-> ##3 ack );the assertion is vacuous because the antecedent is a no match. In the 1st case, it is vacuous (true vacuously) because the property that follows the start is vacuous.
Ben Cohen systemverilog.us

3

In reply to ben@SystemVerilog.us:

Thanks for the response, Ben!

I understand the vacuousness in the 2nd assertion. But, unmatched antecedent won’t result in the “failure” of assertion.
Will the assertion in 1st case “fail” because property (consequent to first suffix implication) is failing?

Priyank

4

In reply to priyank87:

start |-> ##2 send |-> ##3 ack );

/Will the assertion in 1st case “fail” because property (consequent to first suffix implication) is failing?

The consequent to start is the property ##2 send |-> ##3 ack
If the antecedent to that property is false with send ==0, then that property is vacuous.
That makes start |-> ##2 send |-> ##3 ack vacuous.
This is also vacuous

 true|-> (false|-> true or false)

Ben Cohen systemverilog.us

5

In reply to ben@SystemVerilog.us:

Got it! Thanks, Ben!

6

In reply to priyank87:

Remember that for a property with an antecedent to succeed, all threads of that antecedent must be evaluated; thus the need for a first match.

start |-> ##[1:$] send |-> ##3 ack; // can never succeed
start |-> first_match (##[1:$] send) |-> ##3 ack; // can succeed
start |=>  send[->1] |-> ##3 ack; // can succeed
start |-> ##[1:$] send ##3 ack; // can succeed, is more efficient for sims

Ben

7

In reply to ben@SystemVerilog.us:

Remember that for a property with an antecedent to succeed, all threads of that antecedent must be evaluated; thus the need for a first match.

The above statement holds true only if there is a unbounded delay in the antecedant correct ?

8

In reply to diptishe:


// One attempt at every clocking event, assertion can fail but never succeed because for success 
// all threads of that antecedent must be evaluated (as you mentioned) 
ap_v0: assert property( @(posedge clk) 
          a ## [1:$] b |=> c); 

// One attempt at every clocking event, one unique match in antecedent 
ap_better: assert property( @(posedge clk) 
            first_match(a ## [1:$] b)|=> c); 

// One attempt at every clocking event, one unique match in antecedent 
ap__more_stylist: assert property( @(posedge clk) 
          a ##1 b[->1] |=> c);  // no first_match() because of the goto operator 

// One attempt at every clocking event, way way too many threads  
// assertion can fail but never succeed because for success 
// all threads of that antecedent must be evaluated (as you mentioned) 
// Very poor style. actually same as (a ## [1:$] b |=> c) 
ap_Discouraged: assert property( @(posedge clk) 
          ##[1;$] a ## [1:$] b |=> c);  //

ben ben@systemverilog.us

9

Hi Ben,

For the below property to be non vacuous what will be it changed too?
start |-> ##2 send |-> ##3 ack );

10

In reply to curious_verifier:

start |-> ##2 send |-> ##3 ack );
is vacuous when any of the antecedents of the 2 properties are a no-match.
start |-> ##2 send |-> ##3 ack ); is same as

property2: (##2 send |-> ##3 ack )
Property_top: start |-> property2

Thus, start |-> (##2 send |-> ##3 ack ) is nonvacuous if
start==1 and send==1

In general, I recommend avoiding multiple implication operators
Write instead
start ##2 send |-> ##3 ack );

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

11

Thank Ben!