Bug 61 - Evaluate and research Formal Mathematical Proofs
Summary: Evaluate and research Formal Mathematical Proofs
Status: CONFIRMED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Source Code (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
URL:
Depends on:
Blocks: 80
  Show dependency treegraph
 
Reported: 2019-04-15 12:52 BST by Luke Kenneth Casson Leighton
Modified: 2020-09-21 16:35 BST (History)
1 user (show)

See Also:
NLnet milestone: NLnet.2019.02
total budget (EUR) for completion of task and all subtasks: 1000
budget (EUR) for this task, excluding subtasks' budget: 1000
parent task for budget allocation: 191
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:


Attachments
modified version of nmigen.test.tools.py (3.21 KB, text/x-python)
2019-05-01 23:14 BST, Luke Kenneth Casson Leighton
Details
version of mstatus_formal.v in nmigen (2.42 KB, text/x-python)
2019-05-01 23:18 BST, Luke Kenneth Casson Leighton
Details
show graphviz a mess, make test temp variable (2.57 KB, text/x-python)
2019-05-01 23:34 BST, Luke Kenneth Casson Leighton
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2019-04-15 12:52:21 BST
Formal mathematical proofs of correctness are needed for the
components and the overall system.
Comment 1 Luke Kenneth Casson Leighton 2019-04-17 08:10:42 BST
From what I saw, verific is an optional requirement. According to [1],
only Yosys, SymbiYosys, and Z3 are required.

[1]: https://github.com/YosysHQ/SymbiYosys/blob/master/docs/source/quickstart.rst#installing
Comment 2 Luke Kenneth Casson Leighton 2019-04-17 08:11:12 BST
found a tutorial which makes mention of the different options, such as
bounded model check and prove mode, which does k-induction checks.

https://symbiyosys.readthedocs.io/en/latest/quickstart.html

https://tomverbeure.github.io/rtl/2019/01/04/Under-the-Hood-of-Formal-Verification.html
Comment 3 Luke Kenneth Casson Leighton 2019-04-17 08:12:03 BST
discussion thread:
http://lists.libre-riscv.org/pipermail/libre-riscv-dev/2019-April/001108.html
Comment 6 Luke Kenneth Casson Leighton 2019-05-01 20:54:46 BST
https://github.com/m-labs/nmigen/blob/master/nmigen/test/test_lib_fifo.py

tracking through from there is something called FHDLTestCase.assertFormal
which calls the prerequisite sby proof, creating the sby config file
in the process.
Comment 7 Luke Kenneth Casson Leighton 2019-05-01 23:14:59 BST
Created attachment 9 [details]
modified version of nmigen.test.tools.py
Comment 8 Luke Kenneth Casson Leighton 2019-05-01 23:18:03 BST
Created attachment 10 [details]
version of mstatus_formal.v in nmigen

redid this:
http://chiselapp.com/user/kc5tja/repository/kestrel-3/artifact/6a73cad59a4fe513

into nmigen, as a standard python unit test, to see if it could be done.
(it can)
Comment 9 Luke Kenneth Casson Leighton 2019-05-01 23:34:01 BST
Created attachment 11 [details]
show graphviz a mess, make test temp variable