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