In reply to feiphung:
you need to study the types of assertions.
Once the always_comb is triggered becuase of a change in any of the signals inside that construct, the
assert(a[i] > b[i]) else $display(“i a[i] b[i]”, i, a[i], b[i]);
is an immediate asn and checks he conditions described on the asn.
Also, the concurrent asd is triggered and at then next posedge of clk, the sampled variables are checked. In this case, if a[i] is true, then at the nect clk cycle b[i] must be true.
ap_ab: assert property(@ (posedge clk) a[i] |=> b[i]);
There is a lot more to assertions, and you need to study the SystemVerilog assertions described in 1800’17 chapter 16. Of course, my SVA book expands on SVA with lots of examples and text using knowledge got thru experience of 4 authors and providing examples of issues addressed by users on this forum.
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