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 [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
discussion thread: http://lists.libre-riscv.org/pipermail/libre-riscv-dev/2019-April/001108.html
https://github.com/daniellustig/riscv-memory-model/blob/master/riscv.als#L312
https://github.com/whitequark/Boneless-CPU/commit/6fd5f1a863a18678104be4a0a31a189459537033
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