Assertion Failing Because Signals Set to 'X'

Coverage
, , ,
1
Hi, I am writing an assertion in SystemVerilog, and I am encountering an interesting problem. I am using the assertion to verify that some counters are only incrementing when the enable bit is set. Here is my code: 


generate
   begin genvar i;
      // Assertion - counters should only be incremented when enabled
      for (i=0; i<NUM_CNTRS; i++) begin

         property incr_cntrs_enabled_check;
         @ (posedge clk)
         disable iff(reset) (!(counter[i] != 12'b0 && i_enable_cntrs == 1'b0));          
         endproperty

         a_incr_cntrs_enabled_check: assert property (incr_cntrs_enabled_check) else $error($time, "Counters incremented when disabled. Cnt: %h", counter[i]);
      end      
   end    
endgenerate

When I run it, my assertion keeps resulting in an error because the counters are "not equal to 0", because they are equal to 'X'! Is there an easy way I can just delay the start of my assertion a certain number of clock cycles until the counters are initialized, or is there a better solution in my case?

Thanks

2

In reply to rachel.greenlee:
You could use supporting logic to add a “ready” signal, and use that in the antecedent.
Thus:


bit ready; 
initial begin 
 repeat(10) @(posedge clk); 
 ready <= 1'b1; 
end 

a_incr_cntrs_enabled_check: assert property (ready |-> incr_cntrs_enabled_check) else $error($time, "Counters incremented when disabled. Cnt: %h", counter[i]);

On you assertion, I have several comments:

  1. the way I read it, you basically state (ignoring the reset disable):
    There should never be the case when counter[i] is not 0 and it is not enabled.
  2. If this is really what you want to say, you should be using the “not” instead of the “!”
  3. Your assertion, the way you wrote DOES NOT fulfill your requirements of
    Assertion - counters should only be incremented when enabled

Instead of:


// Assertion - counters should only be incremented when enabled
       property incr_cntrs_enabled_check;
         @ (posedge clk)
         disable iff(reset) (!(counter[i] != 12'b0 && i_enable_cntrs == 1'b0));          
       endproperty

USE


// Assertion - counters should only be incremented when enabled
      property incr_cntrs_enabled_check;
         @ (posedge clk)
         disable iff(reset) ready && i_enable_cntrs == 1'b0 |=> $stable(counter[i]);  
       endproperty
   property incr_cntrs_enabled_check2;
         @ (posedge clk)
         disable iff(reset) ready && i_enable_cntrs == 1'b1 |=> counter[i]== counter[i] + 1'b1;  
       endproperty

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

3

In reply to rachel.greenlee:

Hi,

Why don’t you reset the counter and avoid 'X all along! If that is not possible, you can make use of $assertoff/$asserton untill counter resets/settles down to a known value.

Here advantage is, even if different counter takes different times to get known value, you can disable/enable each assertion separately accordingly.

Also, in Ben’s code the counter increment logic should look like this,

// Assertion - counters should only be incremented when enabled
property incr_cntrs_enabled_check2;
  @(posedge clk) disable iff(reset)
    ready && (i_enable_cntrs == 1'b1) |=> counter[i] == ($past(counter[i]) + 1'b1);  
endproperty
4

Thanks for the replies. I played around with this for a bit and the solution that ended up working was using $isunknown (which I did not know about at the time).


disable iff(reset) (!(counter[i] != 12'b0 && i_enable_cntrs == 1'b0) || $isunknown(counter[i])[*11]);
5

In reply to MayurKubavat:
Thanks for correcting my code. Shows you why assertions should be reviewed.
We’re human… and we make mistakes. In tis case, I meant to use the $past/
Ben

6

In reply to rachel.greenlee:

Thanks for the replies. I played around with this for a bit and the solution that ended up working was using $isunknown (which I did not know about at the time).


disable iff(reset) (!(counter*!= 12'b0 && i_enable_cntrs == 1'b0) || $isunknown(counter[i])[*11]);

Your assertion does NOT meet your requirements [i]“counters are only incrementing when the enable bit is set”*. What you have says " There should never be the case When not enable and counter[i] is not 0, or counter[i] is unknown". not(x && y) is same as !x or y, thus, you can say that what you wrote is same as
at every clock, !(counter[i] !=0) || ! enbale==0 || is unkown(counter).
I guess hat this means that at every clock, counter==0 || ebable ==1 || usunknown.

That does NOT meet your original requirements, sorry.

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
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115