Bug 198 - Formal correctness proofs are needed for low-level libraries in LibreSOC
Summary: Formal correctness proofs are needed for low-level libraries in LibreSOC
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: 211
Blocks: 158
  Show dependency treegraph
 
Reported: 2020-03-02 13:25 GMT by Luke Kenneth Casson Leighton
Modified: 2020-05-21 14:01 BST (History)
1 user (show)

See Also:
NLnet milestone: NLNet.2019.10.Formal
total budget (EUR) for completion of task and all subtasks: 9000
budget (EUR) for this task, excluding subtasks' budget: 8650
parent task for budget allocation: 158
child tasks for budget allocation: 211 312
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:25:41 GMT
Formal proofs turn out to provide 100% code-coverage if written correctly,
whereas standard testbench units tests typically do not, even when dozens,
hundreds or tens of thousands are provided.  Therefore, to greatly simplify
the development and also increase effectiveness of unit tests, formal
proofs are to be written on the low-level HDL libraries used in Libre-SOC.
this includes nmutil and the SoC code itself.  This is *different* from
the *high-level* formal correctness proofs (bug #194 and bug #195)
https://git.libre-riscv.org/?p=nmutil.git;a=summary
https://git.libre-riscv.org/?p=soc.git;a=summary