Skip to content

Conversation

@slan
Copy link

@slan slan commented Feb 24, 2021

During development, it is convenient to integrate formal verification in the build process rather than integrating the core to the verification framework.

This PR removes the restriction to generate and run verification inside the riscv-formal dev tree cores directory:

  • genchecks now accepts an additional argument to override basedir (a hard-coded reference to ../.. has been fixed too)
  • genchecks also provides a extra hargs: incdir that can be passed as 3rd command-line argument to define additional include path

In practice, this enables the following:

  • ${ROOT_PROJECT}/platform/formal contains checks.cfg and wrapper.sv
  • checks.cfg has a line read_verilog -sv @incdir@/wrapper.sv
    The following command will create a local, ready-to run directory structure:
mkdir -p build/formal&&cd build/formal&&cp ${ROOT_PROJECT}/platform/formal/checks.cfg .
python ${ROOT_RISCV_FORMAL}/checks/genchecks.py checks ${ROOT_RISCV_FORMAL} ${ROOT_PROJECT}/platform/formal

NOTE: genchecks is assuming cfgname is both the filename of the config file and the name of the target directory. This forces the config file to be copied in the build directory instead of just being referenced from the source directory. I couldn't find a way to do that in a backward-compatible way.

@stevehoover
Copy link

@clairexen I'm maintaining some really ugly hacks in https://github.com/stevehoover/warp-v to work around this. Any chance this (or #11) could be merged?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants