[SVA]Antecedent of the implication never satisfied-Issue

SystemVerilog
, ,
1

Hello Enthu’s,

I had created an assertion and found the result as Antecedent of implication never satisfied.

But I can see that signal there at antecedent is asserted,

//Antecedent of the implication never satisfied.

Below is my assertion code:

assert1: assert property (prop1(aggr_clkreq_imgpll,valid_imgpll,aggr_clkack_imgpll,force_on_imgpll,force_on_ack_imgpll))
$display(“at %t assertion passed”,$time);
else $display(“assertion failed”);
property chassis_force_on_prop(sig1,sig2,sig3);
//@(posedge test_clk)
disable iff(!global_rst_b)
$rose(sig1) /|->/ ##[0:max_index_check] $rose(sig2) |-> ##[0:max_index_check] $rose(sig3) |-> ##[0:max_index_check] $fell(sig1) |-> ##[0:max_index_check] $fell(sig2) |-> ##[0:max_index_check] $fell(sig3);
endproperty
assert2: assert property (@(posedge done) prop2(sig1,sig2,sig3))
$display(“at %t assertion passed”,$time);
else $display(“assertion failed”);

Regards
Bharath

2

In reply to BhaRath@Intel:
In my book and in my most recent paper I address the issue of multithreaded antecedent (see - Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy

From that paper: 1.3.1 Raw range. no single match
Consider the following property
$rose(a) ##[1:5] b |-> ##3 c;
It states that following each thread of the sequence ($rose(a) ##[1:5] b) the variable “c” will be true three cycles later for that thread. That antecedent sequence states that the rise of “a” is followed by the expression “b” within 1 to 5 cycles.

The issue that arises with users is that the antecedent is multithreaded, and that can causes unanticipated errors. SVA requires that each of the threads of that antecedent with a range or a repeat statement, must be tested with its appropriate consequent. Specifically, the property $rose(a) ##[1:5] b |-> ##3 c; is equivalent to
($rose(a) ##[1] b) or ($rose(a) ##[2] b) or …($rose(a) ##[5] b) |-> ##3 c;

This ORing in the antecedent creates multiple threads, something like:
($rose(a) ##[1] b |-> ##3 c) and
($rose(a) ##[2] b |-> ##3 c) and
…
($rose(a) ##[5] b |-> ##3 c);

Note: Any non-matched thread of the antecedent (when b==0) creates a vacuously true property result for that thread, meaning that though TRUE, it is of no significance. However, any failure of one of those property threads causes the assertion to fail. That would occur if one of the treads of the antecedent is a match and its corresponding consequent is not a match (when c==0). For true property success, there can be no property failure (vacuity is considered a vacuous true), and at least one thread of the antecedent matches along with a match of its corresponding consequent.

Now, looking at your assertion, it presents many of those issues, including the use of multiple antecedents/consequents. This is a good example of a very POORLY WRITTEN __property. I would rewrite your property as:


  property chassis_force_on_prop(sig1,sig2,sig3); // max_index_check must be a static number
  @(posedge test_clk) disable iff(!global_rst_b)
  first_match($rose(sig1) ##[0:max_index_check] $rose(sig2) 
                          ##[0:max_index_check] $rose(sig3)) 
    |-> strong(##[0:max_index_check] $fell(sig1) 
               ##[0:max_index_check] $fell(sig2) 
               ##[0:max_index_check] $fell(sig3));
endproperty
// An assertion of this property can never FAIL if max_index_check is replaced with $

This property has a different interpretation than the one you expressed. However, you need to understand and appreciate the significance of vacuity. What are your requirements expressed in English?

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
3

In reply to ben@SystemVerilog.us:

Thank you Ben for clarifying on this assertion writing.

So far I was assuming each signal check should be associated with an Implication operator.

your explanation clarified me two things 1. Why we are using Implication operator. 2. How the assertion behaves if we have $ in the range.

4

In reply to BhaRath@Intel:

So far I was assuming each signal check should be associated with an Implication operator.

True for most cases, but not always. For example

 assume property(@(posedge clk) mode==low_power);
assert property(@(posedge clk) not(pop && fifo_state==empty);

How the assertion behaves if we have $ in the range.

that is true for a range; the $ is a special case for an infinite range.