[libre-riscv-dev] [Bug 165] New: Formally verify the FPCMP (FEQ, FLE, FLT) module
mtnolan2640 at gmail.com
Mon Feb 3 03:27:49 GMT 2020
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
> 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.
More information about the libre-riscv-dev