Systemverilog assertion

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

  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: