Assertions not triggering:

SystemVerilog
,
2

In reply to Bhaskar44:

I am writing an assertion to check the value of a signal from the DUT against a value I calculated in my assertions module.
On the waveform I see that both the signals do have similar values.
My problem is that the assertions aren’t even triggering!
The code that I have is :

cmd_10_chk: assert property (@(negedge act_vfy)
(1) |-> (enc_sva[8] == enc_dut_8[3:0])) 
else $error ("Error: encode failed for SVA, %d != %d", enc_sva[8], enc_dut_8 );

act_vfy is a flag, upon its negedge is when the assertion should trigger!
Similarly I have 16 assertions each to check for 16 values from the DUT which arrives as different signals.

[Ben] Your issue seems to be the sampling regions and when the signals are sampled.
From your description, I believe that you are using something like the following code:


always_ff  @(posedge clk)  
  if(some_condition) act_vfy <= 1'b0; 
  else act_vfy <= 1'b1;  
// act_vfy changes in the NBA region, see below for regions 
always_ff  @(posedge clk)
   if(some_situation) enc_sva <= some_value; 
// BAD STYLE because of triggering and sampling regions 
// ****
cmd_10_chk_VERY_BAD_STYLE: assert property (@(negedge act_vfy)(1) |-> 
  (enc_sva[8] == enc_dut_8[3:0]) ); 
// The sampling value for enc_sva[8] is one delta time (i.e., just before)  
// act_vfy is falling (i.e., when it was ==1'b1. 
// I believe that what you want to express is that 
// * When act_vfy went to a zero, then after enc_sva[8] settles, 
//  (enc_sva[8] == enc_dut_8[3:0])
// Your correct should should then look like this: 
always_ff  @(posedge clk)  
  if(some_condition) act_vfy <= 1'b0; 
  else act_vfy <= 1'b1;    
always_ff  @(posedge clk)
   if(some_situation) enc_sva <= some_value; 
// *****************************************
cmd_10_chk_better: assert property (@(posedge clk) $fell(act_vfy) |-> 
   (enc_sva[8] == enc_dut_8[3:0])) 
    else $error ("Error: encode failed for SVA, %d != %d", enc_sva[8], enc_dut_8 );
// *****************************************
// On a separate note, properties of the type 
   1'b1 |-> consequent // can be reduced to: 
            consequent // The 1'b1 antecedent is not needed. 
// Similarly I have 16 assertions each to check for 16 values 
// from the DUT which arrives as different signals.
// [Ben] Consider using the generate statement if it fits your needs. 
// Below is an example of a generate statement, from my SVA Handbook 4th Edition, 2016 
generate for (genvar g_i=0; (g_i<8); g_i++) begin
  if (g_i >= N)
    ap_range_gen: assert property (v==g_i && $rose(a) |-> ##[N:g_i] b);
end endgenerate

1008×627 444 KB

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us