Assertion Failing Because Signals Set to 'X'

Coverage
, , ,
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