Hi,
I want to use an assertion to check the following scenario: signal A asserts for one cycle, then signal B asserts for one cycle and signal C asserts for one cycle(The problem here is: the order of B and C is arbitrary, so we don’t know when B and C will be asserted and who will be asserted first), then signal D should asserts right after the latter one of B/C. I used the following assertion:
(A==1) ##1 (B[->1] && C[->1]) |-> ##1 (D==1);
However the simulation tool reports syntax error about “&&”. I think that may be “&&” means happens simultaneously, so it could not be used with [->1]. But if that’s the case, how shall I write this assertion?
Thanks a lot!
In reply to wangjiawen:
- (B[->1] && C[->1]):
You need to use the sequential andoperator instead of the logical **&&**operator since B[->1] and C[->1] are sequences - You need to use an implication operator because at every clocking event you have an attempt. Using only a sequence as the property of an assertion the assertion fails when an element of the sequence is false. In this case, every time A==0 the assertion fails instead of being vacuous (your real intent).
/* signal A asserts for one cycle, then signal B asserts for one cycle and signal C
asserts for one cycle(The problem here is: the order of B and C is arbitrary,
so we don't know when B and C will be asserted and who will be asserted first),
then signal D should asserts right after the latter one of B/C */
module m;
bit clk, a, b, c, d;
ap_abc: assert property(@(posedge clk)
a |-> (b[->1] and c[->1]) ##1 d);
endmodule : m
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
In reply to ben@SystemVerilog.us:
Hi Ben,
Thanks a lot for the reply! I did not know the difference between “and” and “&&”. Really appreciate your help.
Regarding your second comment, I indeed used implication operator, but the position is different.
Mine: a ##1 (b[->1] and c[->1]) |-> ##1 d;
Yours: a |-> (b[->1] and c[->1]) ##1 d;
I guess the difference between yours and mine is that in my code the assertion won’t be checked until the whole sequence before the a implication operation is satisfied, but in your code, every time a is asserted, the assertion will start. In my opinion, there is some difference here, but for the current requirement, both should work. Not sure if I get your point correctly? Please correct me if I’m wrong.
Thanks again for your help!
In reply to wangjiawen:
You’re correct, it’s really a matter of the requirements. As you know, a non-matched antecedent is a vacuous assertion.
Note: b[->1] is equivalent to: !b[*0:] ##1 b
b[=1] is equivalent to: !b[*0:] ##1 b ##1 !b[*0:$]
If an antecedent is multithreaded, all threads must be tested with its corresponding consequent for success. b[->1] is single-threaded because it ends when b==1
b[=1] is multi-threaded because after b==1, there are other threads to be test (till infinity) for b==0. If in your case you want ONE “b” followed by ZEROs and ONE “c” followed by ZEROs until you match an intersect type of condition, then you’ll need a first_match() operator. See my example and the comments below:
/* signal A asserts for one cycle, then signal B asserts for one cycle and signal C
asserts for one cycle(The problem here is: the order of B and C is arbitrary,
so we don't know when B and C will be asserted and who will be asserted first),
then signal D should asserts right after the latter one of B/C */
module m;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, a, b, c, d;
initial forever #10 clk=!clk;
ap_abc: assert property(@(posedge clk) // A 2nd "b" could occur before a "c"
a ##1 (b[->1] and c[->1]) |-> d);
ap_abc2: assert property(@(posedge clk)
a ##1 (b[=1] and c[=1]) |-> d); // MULTI_THREADED !!!
ap_abc3: assert property(@(posedge clk)
first_match(a ##1 (b[=1] and c[=1])) |-> d); // BETTER
// vacuous if 2nd "b" occurs before a "c"
initial begin
repeat(200) begin
@(posedge clk);
if (!randomize(a, b, c, d) with
{ a dist {1'b1:=1, 1'b0:=7};
b dist {1'b1:=1, 1'b0:=2};
c dist {1'b1:=1, 1'b0:=3};
d dist {1'b1:=1, 1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule : m
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
In reply to ben@SystemVerilog.us:
Hi Ben,
Thanks a lot! Really appreciate your help! I think ap_abc3 is exactly what I want.
In reply to wangjiawen:
Sorry, but I made a mistake.
Assertions need to be tested!!!
we’re human :)
// ap_abc3 DOES NOT WORK as I expressed because
ap_abc3: assert property(@(posedge clk)
first_match(a ##1 (b[=1] and c[=1])) |-> d);
ap_abc3_equiv: assert property(@(posedge clk)
first_match(a ##1 (!b[*0:$] ##1 b ##1 !b[*0:$] and
!c[*0:$] ##1 c ##1 !c[*0:$])) |-> d);
// Then the !b[*0:$] gives you the option of a thread !b[*0],
// thus not a requirement for for a follow-up "b" to be equal to 0.
//----- WHAT IS NEEDED INSTEAD
ap_abc2_want: assert property(@(posedge clk)
first_match(a ##1 (!b[*0:$] ##1 b ##1 !b[*1:$] and
!c[*0:$] ##1 c ##1 !c[*1:$] )) |-> $past(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
In reply to ben@SystemVerilog.us:
Hi Ben,
Thanks a lot for the elaboration. Really learned a lot from you! I never notice there are so many subtle differences here.
In reply to wangjiawen:
ap_abc2_want: assert property(@(posedge clk)
first_match(a ##1 (!b[*0:$] ##1 b ##1 !b[*1:$] and
!c[*0:$] ##1 c ##1 !c[*1:$] )) |-> $past(d));
// is same as
ap_abc2_want2: assert property(@(posedge clk)
first_match(a ##1 (b[->1] ##1 !b[*1:$] and
c[->1] ##1 !c[*1:$])) |-> $past(d));
// Looks cleaner