System verilog Assertion with throughout operation

SystemVerilog
, ,
1

Hi ,
I am trying to verify 1 scenario from SVA with throughout OPERATOR.
Below is my design requirement.

Once the fifo_empty_o signal assert, it should not be de-assert with below condition
1. fifo_empty_o will not de-assert till the occ_cnt_o is less than fifo_empty_th.
OR
2. It will de-assert only when occ_cnt_o is 0.
I have wrote below assertion for above requirement but it is passing with failing cases also.
Please let me know where I am doing wrong.

    property almost_empty_status ;
      @(posedge u_dma_ctrl.clk_i ) disable iff (!(u_dma_ctrl.rst_n_i)) 
    $rose(u_dma_ctrl.fifo_empty_o) |-> u_dma_ctrl.fifo_empty_o throughout (((u_dma_ctrl.occ_cnt_o)<=(u_dma_ctrl.fifo_empty_th))|| (u_dma_ctrl.occ_cnt_o==0))[->1];
    endproperty
2

In reply to kuldeep sharma:
You need the sequential ORing instead of the logical ORing. Thus,


property almost_empty_status ;
    @(posedge u_dma_ctrl.clk_i ) disable iff (!(u_dma_ctrl.rst_n_i)) 
    $rose(u_dma_ctrl.fifo_empty_o) |->
      u_dma_ctrl.fifo_empty_o throughout (u_dma_ctrl.occ_cnt_o <=u_dma_ctrl.fifo_empty_th)[->1]
    or (u_dma_ctrl.occ_cnt_o==0))[->1];
endproperty

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

** 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:
3

In reply to ben@SystemVerilog.us:

Your original assertion looks OK from a construction view.
I prefer the use of the sequence “or”, as it expresses your requirements in a clearer way. It is also easier to debug with a thread viewer.

If your assertion passes unexpectedly, I would question your requirements.
Ben systemverilog.us

4

In reply to ben@SystemVerilog.us:
Hi Ben,

Thanks for the update.It is working in my case.
I am getting confusion to print Assertion pass/fail info in report summary.

Pass info is coming only once when antecedent {$rose or $fell} is asserting for the first time.
Pass Info is not coming when antecedent is true for next time .Only this is happening with pass info
But Error info is coming whenever antecedent { $rose or $fell} is true but consequent is not true.
I am writing assertion as below
property valid_assert ;
@(posedge clk_i ) disable iff (!(rst_n_i))
$rose(valid |-> ((valid_cnt <=valid_in) && (valid_cnt>0));
endproperty

  valid_assert_check : assert property (valid_assert)
 `uvm_info("QAU0:: PASS VALID ASSERT", $psprintf("Valid asserted Correctly  inp_register= %d valid_cnt=%d",valid_in,valid_cnt),UVM_HIGH)
 else
 `uvm_error("QAU0:: FAIL PASS VALID ASSERT", $psprintf("Valid asserted Correctly  inp_register= %d valid_cnt=%d",valid_in,valid_cnt))

In my simulation valid is asserting twice or thrice. In report summary it print it is asserting only once.
[QAU0:: PASS VALID ASSERT] 1

Is there any issue in my assertion ?

5

In reply to kuldeep sharma:

Because of the way SystemVerilog evaluates items in specific zones, you have to use the $sampled(variable) in the action block. Thus,

.. 
$psprintf("Valid asserted Correctly inp_register= %d valid_cnt=%d",$sampled (valid_in) , $sampled(valid_cnt) ),UVM_HIGH)

Reverify your assertion now.
Ben systemverilog.us