Why i am seeing assertion fail msg even when i have used implication operator for every clk.?

SystemVerilog
, ,
1 
//full_signal
sequence fifo_full;
   
  ( WR_EN && clear && (RD_EN ==0) )[*16] ;  

endsequence

property full_prop;
  @(posedge WR_CLK , RD_CLK)
  disable iff(!clear)
  fifo_full |-> FULL;
 
endproperty

full_check : assert property(full_prop)
               $info("[%0t] FULL_Property :::ASSERTED <<<<--------------------------------------------------------------------------------- ",$time);
             else
               $warning("[%0t] WARNING FULL_Property ::: NOT ASSERTED ",$time);
2

In reply to shakti meva:

Can you create a simple example that shows when you expect to see exactly one failure, but are seeing multiple failures?

3

In reply to dave_59:

In below example i am expecting when wr_en is high for 16 consecutive cycle then only full is going to be checked and if full is not high then only it should give a asssertion error not on every clk when it’s checking

//full_signal
sequence fifo_full;

( WR_EN )[*16] ;

endsequence

property full_prop;
@(posedge WR_CLK )
disable iff(!clear)
fifo_full |-> FULL;

endproperty

full_check : assert property(full_prop)
$info("[%0t] FULL_Property :::ASSERTED <<<<--------------------------------------------------------------------------------- “,$time);
else
$warning(”[%0t] WARNING FULL_Property ::: NOT ASSERTED ",$time);

4

In reply to shakti meva:

When wr_en is high for 16 consecutive cycle then only full is going to be checked
and if full is not high then only it should give a asssertion error not on every clk when it’s checking


ap_we_full: assert property(@ (posedge clk) ( WR_EN )[*16] |-> FULL );
// Above assertion states that at every attempt there is an evaluation of that assertion. 
// For every attempt, at the end point of 16 repeats of WR_EN, then FULL==1 else failure. 
// We need to see your testbench 
//  @cycle 0 1 2 3 4 5 6 7 8 9 A B C D 
//           <-------------16-------------->
//             <-------------16-------------->
//               <-------------16-------------->
WE_EN      0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
FULL       x x x x x x x x x x x x x x x x 1 1 0
Pass/Fail    <-------- active -----------> P     // thread for non vacuous attempt @1
               <-------- active -----------> P   // thread for non vacuous attempt @2
                 <-------- active -----------> F // thread for non vacuous attempt @3

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 - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:
5

In reply to ben@SystemVerilog.us:

Your assertion does meet the requirements for a fifo.
Also, the wr_en need not be conservative. Instead of [*16] you could use [->16] .
You’ll need some support logic to keep track of the state of the fifo as you have reads and writes.
Bottom line, your assertion does not meet your REQUIREMENTS, my opinion of course.
Ben