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

> 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?

Thanks,
Michael

> l.
>
>
> On Sunday, February 2, 2020, <bugzilla-daemon at libre-riscv.org> wrote:
>
>> http://bugs.libre-riscv.org/show_bug.cgi?id=165
>>
>>             Bug ID: 165
>>            Summary: Formally verify the FPCMP (FEQ, FLE, FLT) module
>>            Product: Libre Shakti M-Class
>>            Version: unspecified
>>           Hardware: PC
>>                 OS: Windows
>>             Status: CONFIRMED
>>           Severity: enhancement
>>           Priority: ---
>>          Component: Formal Verification
>>           Assignee: lkcl at lkcl.net
>>           Reporter: mtnolan2640 at gmail.com
>>                 CC: libre-riscv-dev at lists.libre-riscv.org
>>    NLnet milestone: ---
>>
>> A formal proof for the fpcmp module can be found here:
>> https://git.libre-riscv.org/?p=ieee754fpu.git;a=blob;f=src/
>> ieee754/fpcmp/formal/proof_fpcmp_mod.py;h=4f3d273ebbff4ea2c5133134383600
>> d14e8c2683;hb=HEAD
>>
>> --
>> You are receiving this mail because:
>> You are on the CC list for the bug.
>> _______________________________________________
>> libre-riscv-dev mailing list
>> libre-riscv-dev at lists.libre-riscv.org
>> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
>>