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

[Luke Kenneth Casson Leighton]

moo? where did this come from, ha ha ok right michael i think i forgot to
put fcmp on #48 ay no it is there
http://bugs.libre-riscv.org/show_bug.cgi?id=129

frickin fantastic.  it passes the formal proof, right?

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?

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
>


-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68