# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# Original author: Louis-Emile Ploix
# SPDX-License-Identifier: Apache-2.0

IBEX_ROOT=../..

SAIL=$(shell which sail)
PSGEN=$(shell which psgen)

SAIL_RISCV_MODEL_DIR=${LOWRISC_SAIL_RISCV_SRC}/model

include sail-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

# -sv, use the SystemVerilog backend
# --sv-comb, generate a always_comb instead of an initial block
# --sv-inregs --sv-outregs, produce inputs and outputs for every Sail register
# --sv-nostrings, --sv-nopacked, --sv-nomem, avoid generating some things Jasper doesn't like (FIXME: --sv-nopacked might be better removed?)
# -Oconstrant_fold, do basic optimisation
# -memo-z3, resolving types requires a sat solver, this helps speed up those queries
# --sv-unreachable, remove the implementations of functions to either make the design smaller or avoid recursion loops (FIXME: Still necessary?)
# --sv-fun2wires (n:)?f, transform a function into ports, with n (or 1) slots
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

# 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.
# - 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 both jasper and
#   yosys-slang.
build/fusesoc: $(IBEX_ROOT)/rtl $(IBEX_ROOT)/vendor
	mkdir -p build/fusesoc
	fusesoc \
	  --cores-root $(IBEX_ROOT) \
	  run \
	  --build-root build/fusesoc \
	  --tool vcs \
	  --setup \
	  lowrisc:ibex:ibex_formal:0.1
	touch build/fusesoc # Fix timestamps for Makefile

# The sail spec module, constructed from LOWRISC_SAIL_RISCV_SRC, compiled by our fork of the sail compiler
build/ibexspec.sv: $(SAIL) $(SAIL_SRCS) $(SAIL_EXTRA_SRCS) sail-sources.mk Makefile spec/fix_bugs.py
	mkdir -p build
	cd build && $(SAIL) $(SAIL_SRCS) $(addprefix ../,$(SAIL_EXTRA_SRCS)) $(SAIL_SV_FLAGS) $(addprefix -sv_unreachable execute_,$(COMPRESSED_INSTRS)) -o ibexspec
	python3 spec/fix_bugs.py

# The compiled property structure, and the associated TCL
build/psgen-jg.sv: $(PSGEN) $(PSGEN_SRCS) Makefile
	mkdir -p build
	$(PSGEN) $(addprefix -path ,$(PSGEN_SRCS)) $(PSGEN_FLAGS) -sv-out build/psgen-jg.sv -tcl-out build/psgen.tcl

# Same as above, but generate our own covers, and tweak for consumption by our tools
build/psgen-yosys.sv: $(PSGEN) $(PSGEN_SRCS) Makefile
	mkdir -p build
	$(PSGEN) $(addprefix -path ,$(PSGEN_SRCS)) $(PSGEN_FLAGS) -sv-out build/psgen-yosys.sv -clocking -covers -cover-assert -step-prefix

# The aiger file for the OSS flow, using the yosys_formal/* plugins. The main yosys script is in build_all.ys
build/all.aig: build/psgen-yosys.sv build/fusesoc build/ibexspec.sv check build_all.ys $(LOWRISC_YOSYS_SLANG) build/yosys_formal.so
	yosys -m $(LOWRISC_YOSYS_SLANG) -m build/yosys_formal.so -v 1 -s <(cat ./build_all.ys | sed "s|LOWRISC_SAIL_SRC|$(LOWRISC_SAIL_SRC)|g")

# Build the custom yosys plugins
build/yosys_formal.so: yosys_formal/global_clock.cc yosys_formal/write_aiger.cc yosys_formal/opt_muxtree.cc
	yosys-config --build build/yosys_formal.so yosys_formal/global_clock.cc yosys_formal/write_aiger.cc yosys_formal/opt_muxtree.cc

# Build the aig-manip Rust tool
build/aig-manip: aig-manip/src/main.rs
	mkdir -p build
	cd aig-manip && cargo build --release
	cp aig-manip/target/release/aig-manip build/

# Run the jasper environment in interactive mode
.PHONY: jg
jg: build/fusesoc build/psgen-jg.sv build/ibexspec.sv
	jg verify.tcl -allow_unsupported_OS -acquire_proj

# Jasper environment for regression and unattended runs
.PHONY: all
all: build/fusesoc build/psgen-jg.sv build/ibexspec.sv
	jg verify.tcl -allow_unsupported_OS -acquire_proj -no_gui --- "prove_no_liveness"

################################################################################

.PHONY: clean
clean:
	rm -rf build/ aig-manip/target
	rm -rf jgproject/ jgproofs/

