| Summary: | Formal verification of fadd for just round-nearest-ties-to-even 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, lkcl, programmerjake |
| Priority: | --- | ||
| Version: | unspecified | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| 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 implemented correct NaN propagation for the fadd pipeline, so this task is complete. considering that this whole task was only 2 days of work, I think eur 1500 is probably too much, lkcl, I'll let you change it to a more suitable value. I switched to bitwuzla for the smt solver, which made it run *much* faster than z3 for this particular test, fast enough that I can run the f32 formal proof too. on my computer: f16 takes 11s f32 takes 3m15s f64 takes >15m so I set it to be skipped (In reply to Jacob Lifshay from comment #1) > I implemented correct NaN propagation for the fadd pipeline, so this task is > complete. considering that this whole task was only 2 days of work, I think > eur 1500 is probably too much, no, it really isn't. you find these "easy" but they're extremely challenging, and we lost a contributor two years ago because of underpayment. please don't publicly devalue the work that you're doing. i was quoted around EUR 80,000 for a formal correctness proof of IEEE754FP from an Industry source at market rates. |
Steps: * f16: * DONE: formal verification of fadd for just round-nearest-ties-to-even where NaNs are not distinguished from each other and exception flags/traps aren't checked * DONE: formal verification of correct NaN propagation/generation * f32: * DONE: formal verification of fadd for just round-nearest-ties-to-even where NaNs are not distinguished from each other and exception flags/traps aren't checked * DONE: formal verification of correct NaN propagation/generation * f64 -- determined that running the tests is too slow, but should be done. https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/fpadd/test/test_add_formal.py;h=2d3584d26c7f2b9c98ea7d95d0a79b4730cd83dd;hb=HEAD