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

[Luke Kenneth Casson Leighton]

On Monday, February 3, 2020, Michael Nolan <mtnolan2640 at gmail.com> wrote:

> 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.


yes to be expected


>
>    Number of cells:                 45
>      $_MUX_                          6
>      $_NOR_                          1
>      $_NOT_                          3
>      $_OR_                          16
>      $_XOR_                         19


niice


>
>    Number of cells:                145
>
>
> 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.


haha noo, it's just going mental.  O(N^3).

good job you came up with that.  will take a look later, looking forward to
it.

formal proof again, same story with the bugreport?

l.



-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68