Help with assertion inside always@(*) combinational block alongside with for loop

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

  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: