Formal mathematical proofs of correctness are needed for the
components and the overall system.
From what I saw, verific is an optional requirement. According to ,
only Yosys, SymbiYosys, and Z3 are required.
found a tutorial which makes mention of the different options, such as
bounded model check and prove mode, which does k-induction checks.
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
into nmigen, as a standard python unit test, to see if it could be done.
Created attachment 11 [details]
show graphviz a mess, make test temp variable