core-v-verif icon indicating copy to clipboard operation
core-v-verif copied to clipboard

Published 20 hours ago • verified publisher icon openhwgroup

Formal: Roadmap

Open silabs-robin opened this issue 3 years ago • 2 comments

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:

  • https://github.com/openhwgroup/core-v-verif/issues/2411
  • https://github.com/openhwgroup/core-v-verif/issues/1406
  • https://github.com/openhwgroup/core-v-verif/issues/1384

Fixed:

  • https://github.com/openhwgroup/core-v-verif/issues/1996
  • https://github.com/openhwgroup/core-v-verif/issues/1498
  • https://github.com/openhwgroup/core-v-verif/issues/1458

silabs-robin avatar Oct 27 '22 13:10 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 avatar Nov 18 '22 08:11 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?

silabs-robin avatar Apr 13 '23 09:04 silabs-robin