How to make sure assertion fails when expected Boolean expression did not happen in simulation?

SystemVerilog
,
1

Hi,

I have the following assert property. The intention is that if i_en is asserted, the condition data_wr =1 and data_en !==3 should happen for atleast once or more than once in simulation. (I am using the non-consecutive repetition operation because the condition can hold true spaced any number of clock cycles in the simulation).

property i_writes();
@(posedge clk) disable iff (!i_en || !rst_n)
(data_wr & (data_en !== 'h3))[=1:$];
endproperty

assert_i_writes : assert property(i_writes);

I was expecting the assertion to fail if the condition doesn’t happen even once in the entire simulation, but I don’t see the assertion fail.
How to I make it fail if the condition doesn’t even happen atleast once?

Thanks!

2

In reply to sunnikhanna:
1800’2017 16.12.2 Sequence property
If the strong or weak operator is omitted, then the evaluation of the sequence_expr depends on the assertion statement in which it is used. If the assertion statement is assert property or assume property, then the sequence_expr is evaluated as weak(sequence_expr). Otherwise, the sequence_expr is evaluated as strong(sequence_expr).
Thus, in your assertion the sequence (data_wr & (data_en !== 'h3))[=1:$]; is considered weak.
I would write the assertion in a manner that specifies the requirements; specifically,
if i_en is asserted, the condition data_wr =1 and data_en !==3 should happen for atleast once.
The way you wrote is a bit convoluted because it disables the assertion if i_en==0, thus not clearly making that signal as a precondition to the consequent. In addition, if i_en==0 at all cycles, the assertion is always disabled and is never attempted.


    property i_writes();
      @(posedge clk) disable iff (!rst_n)
      $rose(i_en) |-> strong(data_wr & data_en!== 'h3)[->1];
    endproperty
    assert_i_writes : assert property(i_writes);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** 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) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/