mirror of
https://github.com/lowRISC/ibex.git
synced 2025-06-27 17:00:41 -04:00
cea3d04caf
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>
67 lines
2.3 KiB
Makefile
67 lines
2.3 KiB
Makefile
IBEX_ROOT=../..
|
|
|
|
SAIL=sail
|
|
|
|
SAIL_RISCV_MODEL_DIR=${LOWRISC_SAIL_RISCV_SRC}/model
|
|
|
|
include Sources.mk
|
|
|
|
PSGEN_SRCS=thm/btype.proof thm/ibex.proof thm/mem.proof thm/riscv.proof
|
|
PSGEN_FLAGS=-root riscv -task
|
|
|
|
SAIL_EXTRA_SRCS=../spec/main.sail
|
|
|
|
SAIL_SV_FLAGS=-sv -sv-comb -sv-inregs -sv-outregs -sv-nostrings -sv-nopacked -sv-nomem -Oconstant_fold -memo-z3 \
|
|
-sv-unreachable translate -sv-unreachable lookup_TLB -sv-unreachable translate_tlb_miss -sv-unreachable translate_tlb_hit -sv-unreachable pt_walk \
|
|
-sv-fun2wires 2:read_ram \
|
|
-sv-fun2wires 2:write_ram \
|
|
-sv-fun2wires wX \
|
|
-sv-fun2wires 2:rX \
|
|
|
|
# Use fusesoc to resolve the tree of components, copy all resolved source files into the build/ directory,
|
|
# and then generate a filelist for jasper to ingest.
|
|
# Finally, apply a number of small RTL patches necessary to make the formal flow work. (see files in patches/)
|
|
# (Only patch the duplicated source files that fusesoc has copied into build/fusesoc/src, not the version-controlled originals)
|
|
# - Note. we use the 'vcs' fusesoc backend flow to generate the filelist. This is because fusesoc does not currently implement a
|
|
# JasperGold backend, but this is not an issue as the file-format generated by the vcs flow is compatible with jasper.
|
|
.PHONY: fusesoc
|
|
fusesoc:
|
|
mkdir -p build/fusesoc
|
|
fusesoc \
|
|
--cores-root $(IBEX_ROOT) \
|
|
run \
|
|
--build-root build/fusesoc \
|
|
--tool vcs \
|
|
--setup \
|
|
lowrisc:ibex:ibex_formal:0.1
|
|
patch -p0 < patches/ibex_top.diff
|
|
|
|
.PHONY: sv
|
|
sv:
|
|
mkdir -p build
|
|
python3 buildspec.py header > build/ibexspec_instrs.sv
|
|
cd build && $(SAIL) $(SAIL_SRCS) $(SAIL_EXTRA_SRCS) $(SAIL_SV_FLAGS) `cd .. && python3 buildspec.py unreachables` -o ibexspec
|
|
python3 spec/fix_pmp_bug.py
|
|
python3 buildspec.py unreachable_loc_hack
|
|
|
|
.PHONY: psgen
|
|
psgen:
|
|
mkdir -p build
|
|
psgen $(addprefix -path ,$(PSGEN_SRCS)) $(PSGEN_FLAGS) -sv-out build/psgen.sv -tcl-out build/psgen.tcl
|
|
|
|
.PHONY: jg
|
|
jg: fusesoc psgen sv
|
|
jg verify.tcl -allow_unsupported_OS -acquire_proj
|
|
|
|
# The following default target is intended for regressions / unattended runs.
|
|
.PHONY: all
|
|
all: fusesoc psgen sv
|
|
jg verify.tcl -allow_unsupported_OS -acquire_proj -no_gui --- "prove_no_liveness"
|
|
|
|
################################################################################
|
|
|
|
.PHONY: clean
|
|
clean:
|
|
rm -rf build/
|
|
rm -rf jgproject/
|
|
rm -rf jgproofs/
|