| Summary: | NLNet 2019 Formal Correctness Proofs toplevel 2019-10-032 | ||
|---|---|---|---|
| Product: | Libre-SOC's first SoC | Reporter: | Luke Kenneth Casson Leighton <lkcl> |
| Component: | Milestones | Assignee: | 2019-10P |
| Status: | RESOLVED FIXED | ||
| Severity: | enhancement | CC: | 2019-10P, addw, dan, danleighton, joost, libre-soc-bugs |
| Priority: | --- | ||
| Version: | unspecified | ||
| Hardware: | Other | ||
| OS: | Linux | ||
| URL: | https://libre-soc.org/nlnet_2019_formal/ | ||
| NLnet milestone: | NLNet.2019.10.032.Formal | total budget (EUR) for completion of task and all subtasks: | 51460 |
| budget (EUR) for this task, excluding subtasks' budget: | 0 | parent task for budget allocation: | |
| child tasks for budget allocation: | 194 195 196 197 198 577 941 | The table of payments (in EUR) for this task; TOML format: | |
| Bug Depends on: | 211, 195, 196, 197, 198, 577 | ||
| Bug Blocks: | 80, 938 | ||
|
Description
Luke Kenneth Casson Leighton
2020-01-23 18:56:58 GMT
the nmigen riscv-formal task (as well as the openpower one) can be general purpose and applicable to any core. the other tasks - OoO proof and FPU proof - are very specific to the libre soc. The detailed tasks and budget division look good, I will send you the necessary documentation to finalize this phase. Software Dependencies Installation instructions are here: https://libre-riscv.org/HDL_workflow/ we use: * nmigen * yosys * Symbiyosys * SAT Solver dependencies of Symbiyosys (yices2, z3, etc.) for formal proofs we do *not* use softfloat-3 or sfpy because those are for *standard* (non-formal, non-mathematical) unit tests of the IEEE754 FPU. # Schedule A to be attached to MoU List of tasks, plus description, bugtracker URL and budget # A nmigen-based RISC-V Formal correctness proof suite is needed A general-purpose Formal correctness test suite is needed for RISC-V, improving on https://github.com/SymbioticEDA/riscv-formal URL: http://bugs.libre-riscv.org/show_bug.cgi?id=194 Budget: EUR 12000 # A POWER-ISA-based Formal correctness proof suite is needed A general-purpose Formal correctness test suite is needed for Power ISA, similar in characteristics to bug #194. A good first processor to try testing is Microwatt: https://github.com/antonblanchard/microwatt/ URL: http://bugs.libre-riscv.org/show_bug.cgi?id=195 Budget: EUR 12000 # IEEE754 FPU Formal correctness proof suite is needed 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 URL: http://bugs.libre-riscv.org/show_bug.cgi?id=196 Budget: EUR 12000 # Formal correctness proof needed of the 6600-style OoO execution engine A formal proof is needed which demonstrates the effectiveness and correctness of the out-of-order execution engine: register dependencies, memory dependencies, and the use of a "revolving door" set of SR Latches. This is tricky because SR NOR Latches are not normally used in "industry" designs. Consequently we need to formally prove that the HDL functions correctly. https://git.libre-riscv.org/?p=soc.git;a=summary URL: http://bugs.libre-riscv.org/show_bug.cgi?id=197 Budget: EUR 5000 # Formal correctness proofs are needed for low-level libraries in LibreSOC 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 URL: http://bugs.libre-riscv.org/show_bug.cgi?id=198 Budget: EUR 9000 Joost, hi, please see in http://bugs.libre-riscv.org/show_bug.cgi?id=158#c4 the "Schedule A" to be attached to the Memorandum of Understanding for the Formal Correctness Proofs Proposal, 2019-10-032 many thanks. signed, received from Bob Goudriaan. |