Hi,
My original assertion is as following:
property p_test;
@(posedge i_cpu_clock) disable iff (!i_rst_n)
a ##[0:1] (b && tag1==1)[->1] ##1 (c && tag2==1)[->1] |-> d;
endproperty: p_test;
AST_p_test: assert property (p_test);
It works fine in formal verification, the witness status is green and the assertion passes.
However, because the signal tag1/2 may vary from 1 to 7, I tried to use local variable to extend the assertion in some way, so I rewrote this assertions as following:
property p_test;
reg [3:0] tmp_tag;
@(posedge i_cpu_clock) disable iff (!i_rst_n)
a ##[0:1] (b && tag1!=0, tmp_tag=tag1)[->1] ##1 (d && tag2==tmp_tag)[->1] |-> f;
endproperty: p_test;
AST_p_test: assert property (p_test);
However, the formal tool shows it’s vacuity.
I don’t understand why local variable will impact the status? Any one konws the reason? Thanks in advance!
In reply to wangjiawen:
The following comment may not fix your issue, but you need to consider the following:
1800’2017: From a given start point, evaluation of the implication succeeds and returns true if, and only if, for every match of the antecedent sequence_expr beginning at the start point, the evaluation of the consequent property_expr beginning at the end point of the match succeeds and returns true.
Translation: If an assertion of a property has a multi-threaded sequence used as an antecedent, then all threads must be exercised in search of a matched antecedent with a first match of the consequent, unless the assertion fails. In that case, the search is short-circuited (i.e., stopped).
Your assertion has 2 threads
a ##[0:1] (b && tag1==1)[->1] ##1 (c && tag2==1)[->1] |-> d;
// equivalent to
(a ##0 (b && tag1==1)[->1] ##1 (c && tag2==1)[->1]) or
(a ##1 (b && tag1==1)[->1] ##1 (c && tag2==1)[->1]) |-> d;
// Use the first_match()
first_match(a ##[0:1] (b && tag1==1)[->1] ##1 (c && tag2==1)[->1]) |-> d;
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** 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:
- Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy - SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy - SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
Hi Ben,
Thanks a lot for the suggestion. I’m a little confused about “all threads must be exercised in search of a matched antecedent with a first match of the consequent, unless the assertion fails. In that case, the search is short-circuited”.
Let’s use the example
(a ##0 (b && tag1==1)[->1] ##1 (c && tag2==1)[->1]) or
(a ##1 (b && tag1==1)[->1] ##1 (c && tag2==1)[->1]) |-> d;
From my understanding, if (a ##0 (b && tag1==1)[->1] ##1 (c && tag2==1)[->1]) has been satisfied, then if d is asserted, this assertion should pass. If d is not asserted as expected, this assertion should fail. But before (a ##0 (b && tag1==1)[->1] ##1 (c && tag2==1)[->1]) is satisfied, if we detect (a ##1 (b && tag1==1)[->1] ##1 (c && tag2==1)[->1]) is satisfied, then we will check d’s behavior directly, we do not need to wait for (a ##0 (b && tag1==1)[->1] ##1 (c && tag2==1)[->1]) to be satisified. Is my understanding correct? Or you mean, unless ##0 and ##1 are both satisfied, the assertion won’t show the final status?
BTW, to eliminate the potential impact of this multi threads style, I rewrote my two assertions as following:
a ##1 (b && tag1==1)[->1] ##1 (c && tag2==1)[->1] |-> d;
a ##1 (b && tag1!=0, tmp_tag=tag1)[->1] ##1 (c && tag2==tmp_tag)[->1] |-> d;
However, the status does not change. The 1st one still could pass while the 2nd one is still recognized as vacuity… Really weird.
In reply to wangjiawen:
YES, I mean "unless ##0 and ##1 are both satisfied, the assertion won’t show finish because all threads of the antecedent must be tested, and for success, each thread must pass.
If a thread fails, then the assertion fails.
Below is a simple case that will never succeed (testbench below):
ap_no_pass: assert property(@(posedge clk)
(1'b1, $display("%t Start", $realtime)) ##[1:$] 1'b1
|-> 1'b1) $display("%t PASS", $realtime);
// Sim results
# KERNEL: 10 Start
# KERNEL: 3990 END
# RUNTIME: Info: RUNTIME_0068 testbench.sv (13): $finish called.
module top;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, a, b;
initial forever #10 clk=!clk;
initial begin
ap_no_pass: assert property(@(posedge clk)
(1'b1, $display("%t Start", $realtime)) ##[1:$] 1'b1
|-> 1'b1) $display("%t PASS", $realtime);
end
initial begin
repeat(200) @(posedge clk);
$display ("%t END", $realtime);
$finish;
end
endmodule
On your other question, the 2 assertions are not the same unless tag1==1
property p_test;
logic[3:0] tmp_tag;
@(posedge i_cpu_clock) disable iff (!i_rst_n)
// a ##1 (b && tag1==1)[->1] ##1 (c && tag2==1)[->1] |-> d; // one version
a ##1 (b && tag1!=0, tmp_tag=tag1)[->1] ##1 (c && tag2==tmp_tag)[->1] |-> d;
// if(tag1==4'b0100) tmp_tag=4'b0100
// That is different than
// a ##1 (b && tag1==1)[->1] ##1 (c && tag2==1)[->1] |-> d;
// unless tag1==1
endproperty: p_test;
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** 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 - SystemVerilog - Verification Academy
- Free books: Component Design by Example https://rb.gy/9tcbhl
Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com - Papers:
- Understanding the SVA Engine,
Verification Horizons - SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue - SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
In reply to ben@SystemVerilog.us:
Hi Ben,
Thanks a lot for the example. I’m clear now.
But for the 2nd question, yes, I know they’re different, in fact that’s why I used local variables. Since tag1 and tag2 may vary from 1 to 7, my intent is to cover 7 different scenarios:
(a ##1 (b && tag1==1)[->1] ##1 (c && tag2==1)[->1]) |-> d;
(a ##1 (b && tag1==2)[->1] ##1 (c && tag2==2)[->1]) |-> d;
(a ##1 (b && tag1==3)[->1] ##1 (c && tag2==3)[->1]) |-> d;
…
(a ##1 (b && tag1==7)[->1] ##1 (c && tag2==7)[->1]) |-> d;
I tried to use only one assertion to cover all these 7 scenarios, that’s why I tried to use local variable to capture the tag infromation. For now, since local variable does not work as expected, I have to use “generate” to generate 7 assertions.
In reply to wangjiawen:
Could it be that the assertion with the variable is correct with no issue, but the design has an issue with some combinations of the values of tag?
You blame the assertion, but I see nothing wrong with the structure.
Ben
In reply to ben@SystemVerilog.us:
Hi Ben,
Yes, there may be something wrong with the design, but since tag1==1 could pass, at least we should be able to capture the same scenario when I used tmp_tag, as a result, at least one antecedent(where tag1=1) could be satisfied, hence the status of tmp_tag should not be vacuity. That’s what I think is wired. I suspect there is some tool issue here, I also talked to the vendor’s AE team, but they don’t have idea either…
In reply to wangjiawen:
If I understand you correctly, you are addressing formal verification and not simulation. with
a ##1 (b && tag1!=0, tmp_tag=tag1)[->1] ##1 (c && tag2==tmp_tag)[->1] |-> d;
since tag1 is a 4-bit vector, tmp_tag=tag1 will take 15 possible values for the value of tag1 module variable (not the zero value).
thus, it seems to me that formal will consider these situations.
a ##1 (b && tag1!=0, tmp_tag=1)[->1] ##1 (c && tag2==1)[->1] |-> d;
a ##1 (b && tag1!=0, tmp_tag=2)[->1] ##1 (c && tag2==2)[->1] |-> d;
..
a ##1 (b && tag1!=0, tmp_tag=15)[->1] ##1 (c && tag2==15)[->1] |-> d;
// and I believe that all of these properties must be satisficed.
Does this make sense? BTW, if you and your vendor figure it out, I would like to know.
I am always open to learning.
In reply to ben@SystemVerilog.us:
Hi Ben,
Yes, I’m doing formal verification, not simulation.
In the design, tag will only vary from 1-7, but as you said, the formal tool may extend this to 15 assertions. Not sure how do they define vacuity, if all 15 antecedents have to be satisfied, then this can explain the behavior we saw becauwe 8-15 will never be triggered in RTL.
Sure, if I get any further feedback from them, I will let you know. Really glad to have this opportunity to discuss with you and learn from you:)
In reply to wangjiawen:
I believe that you are correct, all 15 antecedents have to be satisfied, then this can explain the behavior
Try adding the following:
ap_tag4: assume property(@(posedge clk) tag1[3]==0 );
That limits the range. Play with more assumptions until you reseolve the issues.
Ben
In reply to ben@SystemVerilog.us:
Also, consider the restrict.
In formal verification, for the tool to converge on a proof of a property or to initialize the design to a specific state, it is often necessary to constrain the state space. For this purpose, the assertion statement restrict property is introduced. It has the same semantics as assume property, however, in contrast to that statement, the restrict property statement is not verified in simulation and has no action block.
The difference between the restrict statement and the assume statement is that the restrict is used to limit scenarios to converge on a proof, whereas the assume defines legal input states
In reply to ben@SystemVerilog.us:
Hi Ben,
Seems it does not work. I added the assumption, but nothing changed. Then I changed the assumption to be tag<2, so it could only be 0 and 1. But the assertion is still vacuity. I also used the analysis tool provided by the formal tool to analyze this vacuity, but it reported: no constraint is related to this.
In reply to wangjiawen:
let us know when you figure it out.
Play with different ranges. The [->1] is a large space, try things like
instead of expr[->1] ##1 w
!expr[*0:10] ##1 expr ##1 w
In reply to ben@SystemVerilog.us:
Hi Ben,
I guess it’s not related to ranges. Because if it’s vacuity due to large ranges, it takes time to verify this. But in fact, the passed assertion took about 30 seconds to finish and the other one only takes 2-3 seconds to show the vacuity status.
In reply to ben@SystemVerilog.us:
Hi Ben,
I guess it’s formal tool issue. I found several interesting results:
- Once I added new assumption as we discussed, e.g. tag<8, then though the vacuity assertion does not change, even the passed assertion(where local variable is not used) became vacuity.
- I noticed that the formal engine used for passed assertion and vacuity assertion was different, if I forced the formal tool to use the same formal engine to run the local variable assertion, then it took hours and just could not finish.