Formal: Roadmap

[silabs-robin]

Task Outcome

Formal support needs improvements, more features, better integration, etc.

Background information

Initial formal scripts for 40s/x has been implemented for Jasper, but there is still more to clean up.

Location Information

• Common files: mk/fv/
• 40s: cv32e40s/fv/
• 40x: cv32e40x/fv

Completion Criteria

TODO

Additional context

Ideas for improvement:

• Move common functionality to shared directory (e.g. mk/fv/)
• Make sure all assumes/etc are included, so assertions can be expected to pass
• Add tb for Onespin-specific assertions
• Support for more tools {Jasper, Questa, Onespin}

Known issues:

• Separate Binding of Assertions #2411
• e40x/s - Lump assert files together #1406
• Remove duplicate manifests #1384

Fixed:

• Formal - Use ExternalRepos #1996
• Formal: Add Assumes #1498
• Formal: Use correct prefix #1458

[silabs-robin]

History:

• Setup initial testbench-scripts
• Port from 40x to 40s
• Create future-plans github-issues
• Add "formal" github-label
• ?

(I might or might not maintain this list as we progress.)

[silabs-robin]

Idea: Before I forget, adding support for tests/cfg/*.yaml might be easy?

The formal makefile already sources some mk/* file(s)(?), so whatever is in there should be visible from the formal makefile.
And the cfgyaml2make script seems to just define some env variables like COMPILE_FLAGS.

Ergo, it should simply be a matter of 1) passing the appropriate env variable to the call to e.g. jasper, and then 2) use CFG=someconfig when calling make?