Bug 196 - Formal correctness proof needed for the IEEE754 FPU
Summary: Formal correctness proof needed for the IEEE754 FPU
Status: CONFIRMED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
URL:
Depends on: 162 163 165
Blocks: 158
  Show dependency treegraph
 
Reported: 2020-03-02 13:16 GMT by Luke Kenneth Casson Leighton
Modified: 2021-10-02 13:11 BST (History)
1 user (show)

See Also:
NLnet milestone: NLNet.2019.10.Formal
total budget (EUR) for completion of task and all subtasks: 12000
budget (EUR) for this task, excluding subtasks' budget: 3550
parent task for budget allocation: 158
child tasks for budget allocation: 162 163 165 565 596
The table of payments (in EUR) for this task; TOML format:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2020-03-02 13:16:21 GMT
The current unit tests are high-level, cumbersome and time-consuming to run
(and can never give 100% coverage).  Formal correctness proofs are needed
which at least cover the low-level components, and move up to the higher
levels - if practical.
https://git.libre-riscv.org/?p=ieee754fpu.git
Comment 1 Luke Kenneth Casson Leighton 2020-03-09 11:23:44 GMT
http://lists.libre-riscv.org/pipermail/libre-riscv-dev/2020-January/003658.html

make sure this is not lost.  james, thank you, i think this went to spam for most people