[libre-riscv-dev] [Bug 165] New: Formally verify the FPCMP (FEQ, FLE, FLT) module
Luke Kenneth Casson Leighton
lkcl at lkcl.net
Mon Feb 3 20:15:57 GMT 2020
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?
> 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
> than the original.
yes to be expected
> Number of cells: 45
> $_MUX_ 6
> $_NOR_ 1
> $_NOT_ 3
> $_OR_ 16
> $_XOR_ 19
> 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
formal proof again, same story with the bugreport?
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
More information about the libre-riscv-dev