Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make basedir overridable, add incdir optional harg #46

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

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