[libre-riscv-dev] [Bug 165] New: Formally verify the FPCMP (FEQ, FLE, FLT) module

[Michael Nolan]

Luke Kenneth Casson Leighton <lkcl at lkcl.net> writes:

>
> wanna give it a shot?

Yup.

I was taking a look at integrating my chain/tree solution with the
existing equals module, it looks like the tree solution is a good bit smaller
than the original. Generating ilang for both with dynamic partition
points at positions 8, 16, and 24 for a 32 bit input and having yosys
synthesize them, I get the following:

New:
=== design hierarchy ===

   top                               1
     mux1                            1
     mux2                            1
     mux3                            1

   Number of wires:                 65
   Number of wire bits:            137
   Number of public wires:          36
   Number of public wire bits:     108
   Number of memories:               0
   Number of memory bits:            0
   Number of processes:              0
   Number of cells:                 45
     $_MUX_                          6
     $_NOR_                          1
     $_NOT_                          3
     $_OR_                          16
     $_XOR_                         19


Original:
=== top ===

   Number of wires:                157
   Number of wire bits:            234
   Number of public wires:          16
   Number of public wire bits:      93
   Number of memories:               0
   Number of memory bits:            0
   Number of processes:              0
   Number of cells:                145
     $_ANDNOT_                      33
     $_AND_                          7
     $_MUX_                          4
     $_NAND_                         1
     $_NOR_                          2
     $_NOT_                          1
     $_ORNOT_                        6
     $_OR_                          59
     $_XNOR_                         1
     $_XOR_                         31


I wanted to try 7 partition points for a 64 bit input, but the original
python seems to hang when I have it generate rtlil.

--Michael