../

Fable Performance

performance of fable

sockit

==============================================================
SUMMARY
==============================================================
           Properties Considered              : 107
                 assertions                   : 64
                  - proven                    : 62 (96.875%)
                  - bounded_proven (user)     : 0 (0%)
                  - bounded_proven (auto)     : 0 (0%)
                  - marked_proven             : 0 (0%)
                  - cex                       : 2 (3.125%)
                  - ar_cex                    : 0 (0%)
                  - undetermined              : 0 (0%)
                  - unknown                   : 0 (0%)
                  - error                     : 0 (0%)
                 covers                       : 43
                  - unreachable               : 0 (0%)
                  - bounded_unreachable (user): 0 (0%)
                  - covered                   : 43 (100%)
                  - ar_covered                : 0 (0%)
                  - undetermined              : 0 (0%)
                  - unknown                   : 0 (0%)
                  - error                     : 0 (0%)

CEX

  • Even the too-dangerous-for-the-general-public model made 2 errors. Let us see if this was a actual CEX or a setup error on my part
a_owr_e_comb: assert property (owr_e == (owr_oen << 0)); // OWN==1: owr_sel== 0

<< by 0 should do nothing afaik. So this says that owr_e == owr_oen at all times.

Let us see what the RTL implements.

assign owr_e = owr_oen << owr_sel;

So the above assertion will be true only when owr_sel is always set to 0.

always @ (posedge clk, posedge rst)
if (rst)
	owr_sel <= {SDW{1'b0}}; 
else if
	(bus_wen_pwr_sel) owr_sel <= bus_wdt[(BDW==32 ? 8 : 0)+:SDW];

Clearly not the case as bus_wdt is an input signal.

Let us look at the other CEX

a_owr_iln: assert (owr_iln == owr_i[0])

RTL:

assign owr_iln = owr_i [ owr_sel ];

Again it’s the owr_sel signal. Claude assumes this is always 0. Why? It is clearly derived from an input signal.

sha3

sha3 doesn’t even compile. The following are the suspicious lines.

// rho rotation offsets, RHO[x][y]
   localparam int RHO [0:4][0:4] = '{
       '{ 0, 36,  3, 41, 18},   // x = 0
       '{ 1, 44, 10, 45,  2},   // x = 1
       '{62,  6, 43, 15, 61},   // x = 2
       '{28, 55, 25, 21, 56},   // x = 3
       '{27, 20, 39,  8, 14}    // x = 4
   };

I don’t think there is anything wrong with this. I ran it with verilator and it worked fine. I think it’s just claude not understanding data type widths and jasper being very strict with its conversions. The bottom line is that it doesn’t compile.