blob: 2c1ad61dd437de6ef9361e1922b858f0e3fb437c [file] [log] [blame]
#****************************************************************************
#* fwrisc_fetch_formal Makefile
#****************************************************************************
include $(PACKAGES_DIR)/packages.mk
include $(PACKAGES_DIR)/simscripts/mkfiles/plusargs.mk
CHECKER=$(call get_plusarg,CHECKER,$(PLUSARGS))
DEPTH=$(call get_plusarg,DEPTH,$(PLUSARGS))
MODE=$(call get_plusarg,MODE,$(PLUSARGS))
ifeq (,$(DEPTH))
DEPTH=32
endif
ifeq (,$(MODE))
MODE=bmc
endif
ifeq (sim,$(MODE))
RUN_TARGETS += run-sim
else
RUN_TARGETS += run-sby
endif
include $(PACKAGES_DIR)/simscripts/mkfiles/common_sim.mk
ifeq (true,$(QUIET))
REDIRECT= >simx.log 2>&1
else
REDIRECT= | tee simx.log 2>&1
endif
VE_DIR := $(abspath $(SIM_DIR)/..)
CORE_SRC_FILES += $(VE_DIR)/../../rtl/fwrisc_fetch.sv
CORE_SRC_FILES += $(VE_DIR)/tb/$(CHECKER).sv
CORE_SRC_FILES += $(VE_DIR)/tests/$(TESTNAME)_test.sv
CORE_SRC_FILES += $(VE_DIR)/tb/fwrisc_fetch_formal_tb.sv
IVL_FLAGS += -I $(VE_DIR)/../../rtl -I $(VE_DIR)/tb
# List of variables to substitute in the .sby file
SBY_VARS += CHECKER TESTNAME DEPTH MODE VE_DIR CORE_SRC_FILES
fwrisc_fetch_formal_tb_defines.svh :
$(Q)echo "\`define TEST_MODULE $(TESTNAME)_test" > $@
$(Q)echo "\`define CHECKER_MODULE $(CHECKER)" >> $@
run-sby : fwrisc_fetch_formal_tb_defines.svh
$(Q)sed $(SIM_DIR)/scripts/fwrisc_fetch_formal.sby \
$(foreach v,$(SBY_VARS),-e 's%{$(v)}%$($(v))%g') > fwrisc_fetch_formal.sby
$(Q)sby -f fwrisc_fetch_formal.sby $(REDIRECT)
run-sim : fwrisc_fetch_formal_tb_defines.svh
$(Q)iverilog $(IVL_FLAGS) $(CORE_SRC_FILES)
$(Q)vvp -l simx.log a.out
include $(PACKAGES_DIR)/packages.mk