Search code examples
verilogsystem-verilogassertionhdlsystem-verilog-assertions

Assertion fails despite equality being true


I am getting a bizarre failure of an assertion. It fails although the equality is true, as shown in the error messages. I am doing a simple sum of the 4 inputs of the u2 module and confirming that the sum is equal to the sum of the two outputs.

property CSA_add;
    @(posedge clk) disable iff(reset) (u2.VS + u2.VC)&'hFFFF == (u2.VS_x + u2.VS_y + u2.VC_x + u2.VC_y)&'hFFFF;
endproperty 

assert property (CSA_add)
       error <= 1'b0; 
    else begin
       $warning("%x result != %x  cheat\n",(u2.VS_x + u2.VS_y + u2.VC_x + u2.VC_y)&'hFFFF
                                       ,(u2.VS + u2.VC)&'hFFFF );
       error <= 1'b1;
    end

I get these error messages:

** Warning: 0000049d result != 0000049d  cheat
Time: 3 ns Started: 3 ns  Scope: tb_shift File: C::....../tb_shift.sv Line: 29<br>
** Warning: 00000163 result != 00000163  cheat
Time: 5 ns Started: 5 ns  Scope: tb_shift File: C::....../tb_shift.sv Line: 29<br>
** Warning: 000000a4 result != 000000a4  cheat
Time: 7 ns Started: 7 ns  Scope: tb_shift File: C::....../tb_shift.sv Line: 29<br>
** Warning: 000006b3 result != 000006b3  cheat
Time: 9 ns Started: 9 ns  Scope: tb_shift File: C:....../tb_shift.sv Line: 29<br>
** Warning: 00000580 result != 00000580  cheat
Time: 11 ns Started: 11 ns  Scope: tb_shift File: C:/Users/John/Dropbox/University/3rd_year/ELEC3017/tb_shift.sv Line: 29

Solution

  • When there is a discrepancy between displayed messages and checking code, it is often the result of a race condition. In this case, the signals being compared were changing at the same time as the sampling clock.

    One remedy is to change the sample point for the assertion. For example, change

    @(posedge clk) 
    

    to:

    @(negedge clk)