Bug 158 - NLNet 2019 Formal Correctness Proofs toplevel 2019-10-032
Summary: NLNet 2019 Formal Correctness Proofs toplevel 2019-10-032
Status: IN_PROGRESS
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Milestones (show other bugs)
Version: unspecified
Hardware: Other Linux
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
URL:
Depends on: 194 195 196 197 198 211
Blocks: 80
  Show dependency treegraph
 
Reported: 2020-01-23 18:56 GMT by Luke Kenneth Casson Leighton
Modified: 2020-04-10 15:16 BST (History)
6 users (show)

See Also:
NLnet milestone: NLNet.2019.10.Formal
total budget (EUR) for completion of task and all subtasks: 50000
budget (EUR) for this task, excluding subtasks' budget: 0
parent task for budget allocation:
child tasks for budget allocation: 194 195 196 197 198
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-01-23 18:56:58 GMT
https://libre-riscv.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.

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).

* nmigen riscv-formal EUR 12000
* nmigen powerisa-formal EUR 12000
* IEEE754 FPU formal EUR 12000
* 6600 out of order formal EUR 5000
* low level libraries formal EUR 9000
Comment 1 Luke Kenneth Casson Leighton 2020-01-23 19:07:46 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.
Comment 2 joost 2020-02-25 09:02:29 GMT
The detailed tasks and budget division look good, I will send you the necessary documentation to finalize this phase.
Comment 3 Luke Kenneth Casson Leighton 2020-02-25 10:37:49 GMT
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.
Comment 4 Luke Kenneth Casson Leighton 2020-03-02 13:31:36 GMT
# 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
Comment 5 Luke Kenneth Casson Leighton 2020-03-12 14:39:45 GMT
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.
Comment 6 Luke Kenneth Casson Leighton 2020-04-10 15:16:29 BST
signed, received from Bob Goudriaan.