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
…
- SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
- 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
- Papers: