Adds a Nix environment which provides a development shell for the formal
verification flow. All dependencies are fetched and built upon entering the
shell (nix develop .#formal), except for the proprietary Cadence Jasper.
The dev shell (nix develop .#formal-dev) is identical to the normal
shell, but prints some information on how to swap out components. This
is also documented in the README.
Documentation on how to use this environment is added to the dv/formal/README.md
The provided Makefile/.tcl scripts make assumptions about the environment
they are run within which are provided by the Nix environment. Using Nix is
the recommended way to run this flow, but if you cannot do this, you will need
to duplicate the setup done by Nix in terms of environment variables and
provided dependencies.
Jasper Gold options:
- allow_unsupported_OS is required on both the machines I use.
- acquire_proj means that if JG is killed (which happens somewhat
often) the next it runs it will still be able to take ownership
of the project.
Co-authored-by: Louis-Emile Ploix <louis-emile.ploix@lowrisc.org>
Co-authored-by: Marno van der Maas <mvdmaas+git@lowrisc.org>
Co-authored-by: Gary Guo <gary.guo@lowrisc.org>
Signed-off-by: Harry Callahan <hcallahan@lowrisc.org>
