https://libre-soc.org/nlnet_2019_formal/ todo, edit this comment and list a series of tasks to assign budgets to. then, create bugreports for each. see bug #48 for a template * bug #194 nmigen version of riscv-formal * bug #195 nmigen version of powerisa-formal (to be discussed, below, may need OpenPowerFoundation sponsorship) * bug #196 IEEE754 FPU formal correctness proofs * bug #197 6600 scoreboard (out of order execution) proof * bug #198 low level libraries (submodules) proofs. * bug #577 basic binutils, gcc and macro-assembler SimpleV support * bug #941 FOSDEM 2020 travel TODO, subdivide these down into smaller tasks (discuss below) so that reasonably accurate budgetary amounts can be assigned to them. slight overestimation (10 to 15% or so) is recommended (and acceptable). * CANCELLED 19jan2020 nmigen riscv-formal EUR 0 * nmigen powerisa-formal EUR 12000 * IEEE754 FPU formal EUR 12000 * 6600 out of order formal EUR 5000 * low level libraries formal EUR 9000 * ADDED 19jan2020 basic gcc binutils macros EUR 12000
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.
michiel, joost: we won't be doing RISC-V, but the MoU was signed before that decision. bug #194 is invalid. can we reassign its budget to bug #550 and to some basic gcc support bug #558