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: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: Highest enhancement
Assignee: Jacob Lifshay
URL:
Depends on: 211 901 902 903 904 909
Blocks: 158
  Show dependency treegraph
 
Reported: 2020-03-02 13:25 GMT by Luke Kenneth Casson Leighton
Modified: 2022-09-07 12:52 BST (History)
3 users (show)

See Also:
NLnet milestone: NLNet.2019.10.032.Formal
total budget (EUR) for completion of task and all subtasks: 9000
budget (EUR) for this task, excluding subtasks' budget: 8850
parent task for budget allocation: 158
child tasks for budget allocation: 312
The table of payments (in EUR) for this task; TOML format:
jacob = { amount = 3850, submitted = 2022-08-29, paid = 2022-09-03 } red = { amount = 5000, submitted = 2022-08-26, paid = 2022-08-31 }


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

nmutil:

* DONE picker    #901
* DONE byterev   #902
* DONE plru      #909
* DONE queue     #903
* DONE lut       already done as part of bug #745
* DONE pop-count #904

clz already has one

soc:

* identify any lowlevel modules and move them to nmutil
 (popcount to be left in soc due to PowerISA-specificity)
* https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/logical/formal/proof_main_stage.py;hb=HEAD

also update,Copyright, Trademark, and Grant notices.
all files.
Comment 1 Luke Kenneth Casson Leighton 2022-07-08 13:19:52 BST
https://gitlab.com/nmigen/nmigen/-/blob/master/nmigen/lib/fifo.py#L177
https://gitlab.com/nmigen/nmigen/-/blob/master/tests/test_lib_fifo.py#L240

these are the formal proofs of SyncFIFO and Queue is literally and exactly
compliant in almost all its modes (i.e. Queue provides more modes than SyncFIFO)
Comment 2 Jacob Lifshay 2022-08-03 05:15:56 BST
lut formal proof was already completed months ago as part of:
https://bugs.libre-soc.org/show_bug.cgi?id=745
Comment 3 Luke Kenneth Casson Leighton 2022-08-26 14:30:54 BST
correctness proofs of nmutil lowlevel all good.
Comment 4 Jacob Lifshay 2022-08-26 17:55:12 BST
lkcl: please explain why red gets more than I did even though iirc i did >90% of the work...marking as in-progress because this needs to be addressed before you try and submit RFPs
Comment 5 Jacob Lifshay 2022-08-26 19:54:14 BST
(In reply to Jacob Lifshay from comment #4)
> lkcl: please explain why red gets more than I did even though iirc i did
> >90% of the work...marking as in-progress because this needs to be addressed
> before you try and submit RFPs

lkcl explained this to me privately.