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

Luke Kenneth Casson Leighton lkcl at lkcl.net
Mon Feb 3 03:16:00 GMT 2020

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?


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.


More information about the libre-riscv-dev mailing list