[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:

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

--Michael