| Summary: | Implementation and Formal verification of fadd for all rounding modes but without exception flags/traps | ||
|---|---|---|---|
| Product: | Libre-SOC's first SoC | Reporter: | Jacob Lifshay <programmerjake> |
| Component: | Formal Verification | Assignee: | Jacob Lifshay <programmerjake> |
| Status: | RESOLVED FIXED | ||
| Severity: | enhancement | CC: | libre-soc-bugs, programmerjake |
| Priority: | --- | ||
| Version: | unspecified | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| See Also: | https://bugs.libre-soc.org/show_bug.cgi?id=877 | ||
| NLnet milestone: | NLNet.2019.10.032.Formal | total budget (EUR) for completion of task and all subtasks: | 1500 |
| budget (EUR) for this task, excluding subtasks' budget: | 1500 | parent task for budget allocation: | 196 |
| child tasks for budget allocation: | The table of payments (in EUR) for this task; TOML format: |
[jacob]
amount = 1500
submitted = 2022-07-06
paid = 2022-07-21
|
|
| Bug Depends on: | 835 | ||
| Bug Blocks: | 868 | ||
I finished implementing and formally proving fadd for f16/f32 and for all rounding modes in the OpenPower spec. https://git.libre-soc.org/?p=ieee754fpu.git;a=commit;h=78bc58e1e6031a81620ced176b798f2e9e4703d1 Copied the same amount of payment as for #869, lkcl let me know if you think that's fine. |
* f16: * DONE: implement other rounding modes in the fadd pipeline * DONE: formal verification of all rounding modes * f32 (if smt solver can handle it): * DONE: implement other rounding modes in the fadd pipeline * DONE: formal verification of all rounding modes * f64 (if smt solver can handle it): * DONE: implement other rounding modes in the fadd pipeline * REMOVED: formal verification of all rounding modes smt solver can't handle it in a reasonably short amount of time, I gave up after 15min, as mentioned in https://bugs.libre-soc.org/show_bug.cgi?id=869#c1 If anyone wants to try running it longer, I expect the formal proof to succeed if the smt solver actually finishes.