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

Michael Nolan mtnolan2640 at gmail.com
Wed Feb 5 16:07:49 GMT 2020

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


More information about the libre-riscv-dev mailing list