| Summary: | Evaluate and research Formal Mathematical Proofs | ||
|---|---|---|---|
| Product: | Libre-SOC's first SoC | Reporter: | Luke Kenneth Casson Leighton <lkcl> |
| Component: | Source Code | Assignee: | Luke Kenneth Casson Leighton <lkcl> |
| Status: | CONFIRMED --- | ||
| Severity: | enhancement | CC: | libre-soc-bugs |
| Priority: | --- | ||
| Version: | unspecified | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| NLnet milestone: | NLnet.2019.02.012 | total budget (EUR) for completion of task and all subtasks: | 0 |
| budget (EUR) for this task, excluding subtasks' budget: | 0 | parent task for budget allocation: | 191 |
| child tasks for budget allocation: | The table of payments (in EUR) for this task; TOML format: | ||
| Bug Depends on: | |||
| Bug Blocks: | 80 | ||
| Attachments: |
modified version of nmigen.test.tools.py
version of mstatus_formal.v in nmigen show graphviz a mess, make test temp variable |
||
|
Description
Luke Kenneth Casson Leighton
2019-04-15 12:52:21 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 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 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. Created attachment 9 [details]
modified version of nmigen.test.tools.py
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) Created attachment 11 [details]
show graphviz a mess, make test temp variable
|