Bug 877 - implementation and formal correctness proof for fp fused-mul-add pipeline excluding ieee754 exception flags
Summary: implementation and formal correctness proof for fp fused-mul-add pipeline exc...
Status: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Jacob Lifshay
URL:
: 123 (view as bug list)
Depends on: 835
Blocks: 196
  Show dependency tree / graph
 
Reported: 2022-07-01 08:40 BST by Luke Kenneth Casson Leighton
Modified: 2022-07-22 05:10 BST (History)
2 users (show)

See Also:
NLnet milestone: NLNet.2019.10.032.Formal
total budget (EUR) for completion of task and all subtasks: 1650
budget (EUR) for this task, excluding subtasks' budget: 1650
parent task for budget allocation: 196
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:
[jacob] amount = 1650 submitted = 2022-07-06 paid = 2022-07-21

Attachments
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2022-07-01 08:40:13 BST 
similar to bug #869 a formal correctness proof is needed for
fused-mul-add

* f8 (non-standard -- 5 exponent bits, 2 bits in mantissa field, 3-bit mantissa value):
    * DONE: implement other rounding modes in the fmadd pipeline
    * DONE: implement fmsub, fnmadd, fnmsub
    * DONE: formal verification
* f16:
    * DONE: implement other rounding modes in the fmadd pipeline
    * DONE: implement fmsub, fnmadd, fnmsub
    * REMOVED: formal verification -- didn't complete after >8hr
* f32 (if smt solver can handle it):
    * DONE: implement other rounding modes in the fmadd pipeline
    * DONE: implement fmsub, fnmadd, fnmsub
    * REMOVED: formal verification -- f16 is too slow, didn't attempt f32
* f64 (if smt solver can handle it):
    * DONE: implement other rounding modes in the fmadd pipeline
    * DONE: implement fmsub, fnmadd, fnmsub
    * REMOVED: formal verification -- f16 is too slow, didn't attempt f64
Comment 1 Jacob Lifshay 2022-07-04 12:03:40 BST 
I implemented fmadd, fmsub, fnmadd, and fnmsub and now just have to work out the remaining bugs.

https://git.libre-soc.org/?p=ieee754fpu.git;a=commit;h=449176c8896dd13ae80130a3a0c8fc88026a2499

I probably got fmadd and fnmsub to work for all rounding modes, I'm currently running the formal proofs overnight -- hopefully they won't take too long to run.

fmsub and fnmadd have a bug which I'll debug tomorrow.
Comment 2 Jacob Lifshay 2022-07-04 12:34:48 BST 
(In reply to Jacob Lifshay from comment #1)
> fmsub and fnmadd have a bug which I'll debug tomorrow.

i think i found the bug by reading the diff:
i forgot to flip `b`'s sign when `negate_addend` is set in the `0 + x` special case:
https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/fpfma/special_cases.py;h=826c32a8e80f2a121a585d7c83bb65e436e97d50;hb=449176c8896dd13ae80130a3a0c8fc88026a2499#l247

i'll fix it tomorrow when it's not 4:30am
Comment 3 Jacob Lifshay 2022-07-05 00:45:01 BST 
(In reply to Jacob Lifshay from comment #2)
> (In reply to Jacob Lifshay from comment #1)
> > fmsub and fnmadd have a bug which I'll debug tomorrow.

I fixed the bug.

Since the formal proofs for f16 fma didn't finish after >8hr, I disabled f16 formal proofs by default and added f8 formal proofs:
I added support for non-standard floating-point types so we can test f8 (eb=5, sb=3), all those passed without issue.

https://git.libre-soc.org/?p=ieee754fpu.git;a=commit;h=a434759860b4e6a92c4c46d4842e767ae5b680e3

I also finished cleaning up all the remaining fixmes, and optimized the amount of padding needed in the intermediate sum.

https://git.libre-soc.org/?p=ieee754fpu.git;a=commit;h=80f6d6471d627c1af572d37b99643c66bbe8be67

I'm considering this completed.
Comment 4 Jacob Lifshay 2022-07-05 00:46:31 BST 
*** Bug 123 has been marked as a duplicate of this bug. ***