Merge pull request #1377 from silabs-robin/formal_nonhardcoded

Formal updates

cv32e40x/fv/Makefile

@@ -16,12 +16,31 @@
 # SPDX-License-Identifier:Apache-2.0 WITH SHL-2.0
 
 
-# TODO:silabs-robin  Move parts to `core-v-verif/mk/`, generalize for re-use.
+# Defines and includes
 
+CORE_V_VERIF ?= $(realpath ../..)
 
-# TODO:silabs-robin  No hardcoded paths.
-export DESIGN_RTL_DIR = ../../core-v-cores/cv32e40x/rtl/
+CV_CORE ?= cv32e40x
 
+CV_CORE_REPO   ?= https://github.com/openhwgroup/cv32e40x
+CV_CORE_BRANCH ?= master
+CV_CORE_TAG    ?= none
+CV_CORE_HASH   ?= head
 
-fv:
-	$(CV_SIM_PREFIX)  jaspergold  fv.tcl
+RISCVDV_REPO        ?= TODO_dontwanttodefinethis
+EMBENCH_REPO        ?= TODO_dontwanttodefinethis
+COMPLIANCE_REPO     ?= TODO_dontwanttodefinethis
+DPI_DASM_SPIKE_REPO ?= TODO_dontwanttodefinethis
+
+include  $(CORE_V_VERIF)/mk/fv/fv.mk
+
+
+# Make target
+
+ifndef  CV_SIM_PREFIX
+  $(warning  CV_SIM_PREFIX undefined)
+endif
+
+fv:  $(CV_CORE_PKG)
+	$(CV_SIM_PREFIX)  jaspergold  jg.tcl
+	# TODO:robin-silabs  Move to "mk/fv/jg.mk"?

cv32e40x/fv/fv.flist

@@ -0,0 +1,42 @@
+# Copyright 2022 Silicon Labs, Inc.
+# Copyright 2022 OpenHW Group
+#
+# SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1
+#
+# Licensed under the Solderpad Hardware License v 2.1 (the "License"); you may
+# not use this file except in compliance with the License, or, at your option,
+# the Apache License version 2.0.
+#
+# You may obtain a copy of the License at
+#
+# https://solderpad.org/licenses/SHL-2.1/
+#
+# Unless required by applicable law or agreed to in writing, any work
+# distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+# WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+
+./uvm_pkg.sv
+./defines.sv
+
+-f  ${CV_CORE_PKG}/cv32e40x_manifest.flist
+
++incdir+${CV_UVMT_PATH}
++incdir+${CV_UVMA_PATH}/uvma_rvfi
++incdir+${CV_UVMA_PATH}/uvma_fencei
+
+./dummy_pkg.sv
+
+${CV_UVMA_PATH}/uvma_fencei/uvma_fencei_if.sv
+${CV_UVMA_PATH}/uvma_rvfi/uvma_rvfi_instr_if.sv
+
+${CV_UVMT_PATH}/uvmt_cv32e40x_tb.sv
+${CV_UVMT_PATH}/uvmt_cv32e40x_dut_wrap.sv
+${CV_UVMT_PATH}/uvmt_cv32e40x_interrupt_assert.sv
+${CV_UVMT_PATH}/uvmt_cv32e40x_debug_assert.sv
+${CV_UVMT_PATH}/uvmt_cv32e40x_fencei_assert.sv
+${CV_UVMT_PATH}/uvmt_cv32e40x_integration_assert.sv
+${CV_UVMT_PATH}/uvmt_cv32e40x_tb_ifs.sv

cv32e40x/fv/jg.tcl

@@ -0,0 +1,32 @@
+# Copyright 2022 Silicon Labs, Inc.
+# Copyright 2022 OpenHW Group
+#
+# Licensed under the Solderpad Hardware Licence, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     https://solderpad.org/licenses/
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+#
+# SPDX-License-Identifier:Apache-2.0 WITH SHL-2.0
+
+
+# TODO:silabs-robin  No hardcoded paths, integrate with `mk/` definitions.
+
+
+proc cvfv_rerun {} {
+  clear  -all
+
+  analyze  -sv12  -f  fv.flist
+  elaborate  -top  uvmt_cv32e40x_tb
+
+  clock  clknrst_if.clk
+  reset  ~clknrst_if.reset_n
+}
+
+cvfv_rerun

mk/fv/fv.mk

@@ -0,0 +1,36 @@
+# Copyright 2022 Silicon Labs, Inc.
+# Copyright 2022 OpenHW Group
+# 
+# SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1
+# 
+# Licensed under the Solderpad Hardware License v 2.1 (the "License"); you may
+# not use this file except in compliance with the License, or, at your option,
+# the Apache License version 2.0.
+# 
+# You may obtain a copy of the License at
+# 
+# https://solderpad.org/licenses/SHL-2.1/
+# 
+# Unless required by applicable law or agreed to in writing, any work
+# distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+# WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# 
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+
+default_target:  fv
+
+
+export CV_CORE_PKG  ?= $(CORE_V_VERIF)/core-v-cores/$(CV_CORE)
+export CV_UVMT_PATH ?= $(CORE_V_VERIF)/$(CV_CORE)/tb/uvmt
+export CV_UVMA_PATH ?= $(CORE_V_VERIF)/lib/uvm_agents
+
+export DESIGN_RTL_DIR ?= $(CV_CORE_PKG)/rtl
+
+
+include $(CORE_V_VERIF)/mk/Common.mk
+
+
+$(CV_CORE_PKG):
+	$(CLONE_CV_CORE_CMD)