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

> don't be put off by the Case being in a pyrhon for-loop! this is a
> weird sideeffect of how nmigen works.

Yep, it threw me a second until I thought about it and realized what was
going on.

> also deploy the "carry" trick being used in partitioned add.

I'll have to look at this tomorrow

> the only thing is, it might actually be better to get this code to do
> GT LT *and* eq all in one.
>
> they are so similar and use the same logic
>
> see wiki page gt is not that different from eq.

Yep, from what I understand it's ~(lt | eq). Of course as I learned with
the scalar comparisons, LT and EQ are not as straightforward as they
seem. Stupid -0.

--Michael