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

Luke Kenneth Casson Leighton lkcl at lkcl.net
Wed Feb 5 16:30:47 GMT 2020

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.


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

More information about the libre-riscv-dev mailing list