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

[Luke Kenneth Casson Leighton]

On Wednesday, February 5, 2020, Michael Nolan <mtnolan2640 at gmail.com> wrote:

> Luke Kenneth Casson Leighton <lkcl at lkcl.net> writes:
>
> > It would almost work for eq as well. I think if the gt inputs are set to
> >> 0 and the right input to the crossbars is set to 1 it would be
> >> equivalent to the equals case. However, that would mean using actual
> >> crossbars.
> >
> >
> > wanna give it a shot?
>
> I've got something working in part_cmp/eq_gt_ge.py and
> gt_combiner.py. Turns out, not only does changing the other input to 1
> work for the equals case, but it also handles the greater than or equals
> case.


good god :)

i integrated eq_combiner into the partitioned signal and it's not having
any of it.

can you look into that by running ieee754/part/tests/test_sig.py?

ignore the (successful) test_add function.

line 105 is where the *single* bit (LSB) of each partition is set to
success/fail, *not* all bits in the partition.

https://git.libre-riscv.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/part/test/test_partsig.py;h=c312917f411ff7a8b1de41f5790bca3ca937e698;hb=419a7fce211635a7c21c58ab857a39f98a238572#l105




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