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

[Luke Kenneth Casson Leighton]

On 2/3/20, Michael Nolan <mtnolan2640 at gmail.com> wrote:
> Luke Kenneth Casson Leighton <lkcl at lkcl.net> writes:
>
>> frickin fantastic.  it passes the formal proof, right?
>
> Yes it does
>>
>> i am just trying to do gt dynamic partitioned
>>
>> michael if you want something a bit challenging to do, could you see if
>> you
>> can optimise the part_cmp eq.py code?
>
> I'll give it a go. This is the sort of variable width SIMD thing you
> were talking about a while ago right? I seem to remember you mentioning
> writing a Switch() statement for each case of the mask, it looks like
> that's what is in equal.py right?

yehyeh.

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

the main problem is that just as jacob initially wrote, i *think* you
can do this purely as a cascade.

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

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.

l.