[tool/fpv] add fpv to dvsim.py
Adding formal jaspergold tool flow to dvsim.py
Add hjson run files, mk files, and tool specific tcl and hjson files
Signed-off-by: Cindy Chen <chencindy@google.com>
diff --git a/hw/formal/data/common_fpv_cfg.hjson b/hw/formal/data/common_fpv_cfg.hjson
new file mode 100644
index 0000000..c8a06d5
--- /dev/null
+++ b/hw/formal/data/common_fpv_cfg.hjson
@@ -0,0 +1,41 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+{
+ flow: fpv
+ flow_makefile: "{proj_root}/hw/formal/data/fpv.mk"
+
+ import_cfgs: [// common server configuration for results upload
+ "{proj_root}/hw/data/common_project_cfg.hjson",
+ "{proj_root}/hw/formal/tools/{tool}/{tool}.hjson"]
+
+ // Default directory structure for the output
+ dut: "{name}"
+ build_dir: "{scratch_path}/{build_mode}"
+
+ // we rely on Fusesoc to generate the filelist for fpv
+ sv_flist_gen_cmd: fusesoc
+
+ // TODO: switch the tool to formal once the corresponding edalize backend is avaiable
+ sv_flist_gen_opts: ["--cores-root {proj_root}",
+ "run",
+ "--tool=icarus",
+ "--target=formal",
+ "--build-root={build_dir}",
+ "--setup {fusesoc_core}"]
+ sv_flist_gen_dir: "{build_dir}/formal-icarus"
+
+ // Indicate the tool specific helper sources
+ tool_srcs: ["{proj_root}/hw/formal/tools/{tool}/fpv.tcl"]
+
+ // Vars that need to exported to the env
+ exports: [
+ FPV_TOP: {dut}
+ COV: {cov}
+ ]
+ report_cmd: "python3 {proj_root}/hw/formal/tools/{tool}/parse-fpv-report.py"
+ report_opts: ["--logpath={build_dir}/fpv.log",
+ "--reppath={build_dir}/results.hjson",
+ "--cov={cov}"]
+}
+
diff --git a/hw/formal/data/fpv.mk b/hw/formal/data/fpv.mk
new file mode 100644
index 0000000..63fbe5b
--- /dev/null
+++ b/hw/formal/data/fpv.mk
@@ -0,0 +1,42 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+.DEFAULT_GOAL := all
+
+all: build
+
+###################
+## build targets ##
+###################
+build: compile_result
+
+gen_sv_flist:
+ @echo "[make]: gen_sv_flist"
+ cd ${build_dir} && ${sv_flist_gen_cmd} ${sv_flist_gen_opts}
+
+pre_compile: gen_sv_flist
+ @echo "[make]: pre_compile"
+ mkdir -p ${build_dir}
+ env | sort > ${build_dir}/env_vars
+ cp -Ru ${tool_srcs} ${sv_flist_gen_dir}
+
+compile: pre_compile
+ @echo "[make]: compile"
+ # we check the status in the parse script below
+ cd ${sv_flist_gen_dir} && ${build_cmd} ${build_opts} 2>&1 | tee ${build_dir}/fpv.log
+
+post_compile: compile
+ @echo "[make]: post_compile"
+
+# Parse out result
+compile_result: post_compile
+ @echo "[make]: compile_result"
+ ${report_cmd} ${report_opts}
+
+.PHONY: \
+ build \
+ run \
+ pre_compile \
+ compile \
+ post_compile \
+ compile_result
diff --git a/hw/formal/tools/jaspergold/fpv.tcl b/hw/formal/tools/jaspergold/fpv.tcl
index aca9d0d..8d8727c 100644
--- a/hw/formal/tools/jaspergold/fpv.tcl
+++ b/hw/formal/tools/jaspergold/fpv.tcl
@@ -111,10 +111,12 @@
}
# run once to check if assumptions have any conflict
-if {$env(CHECK) == 1} {
- check_assumptions -conflict
- check_assumptions -live
- check_assumptions -dead_end
+if {[info exists ::env(CHECK)]} {
+ if {$env(CHECK)} {
+ check_assumptions -conflict
+ check_assumptions -live
+ check_assumptions -dead_end
+ }
}
#-------------------------------------------------------------------------
diff --git a/hw/formal/tools/jaspergold/jaspergold.hjson b/hw/formal/tools/jaspergold/jaspergold.hjson
new file mode 100644
index 0000000..f6a2c44
--- /dev/null
+++ b/hw/formal/tools/jaspergold/jaspergold.hjson
@@ -0,0 +1,10 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+{
+ build_cmd: "{job_prefix} jg"
+ build_opts: ["-batch fpv.tcl",
+ "-proj jgproject",
+ "-allow_unsupported_OS",
+ "-command exit"]
+}
diff --git a/hw/top_earlgrey/fpv/top_earlgrey_fpv_cfgs.hjson b/hw/top_earlgrey/fpv/top_earlgrey_fpv_cfgs.hjson
new file mode 100644
index 0000000..57521e0
--- /dev/null
+++ b/hw/top_earlgrey/fpv/top_earlgrey_fpv_cfgs.hjson
@@ -0,0 +1,148 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+{
+
+ // This is the master cfg hjson for FPV. It imports ALL individual FPV
+ // cfgs of the IPs and the full chip used in top_earlgrey. This enables to run
+ // them all as a regression in one shot.
+ name: top_earlgrey_batch_fpv
+
+ import_cfgs: [// common server configuration for results upload
+ "{proj_root}/hw/data/common_project_cfg.hjson"]
+
+ use_cfgs: [// TODO: implement some switch to only select "_fpv" testbenches
+ // TODO: if we default "_fpv" cov to be on, and the rest of the tbs cov off, need a
+ // command-line switch to disable cov.
+ {
+ name: prim_arbiter_ppc_fpv
+ fusesoc_core: lowrisc:fpv:prim_arbiter_ppc_fpv
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: prim_arbiter_tree_fpv
+ fusesoc_core: lowrisc:fpv:prim_arbiter_tree_fpv
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: prim_lfsr_fpv
+ fusesoc_core: lowrisc:fpv:prim_lfsr_fpv
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: prim_fifo_sync_fpv
+ fusesoc_core: lowrisc:fpv:prim_fifo_sync_fpv
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: prim_alert_rxtx_fpv
+ fusesoc_core: lowrisc:fpv:prim_alert_rxtx_fpv
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: prim_alert_rxtx_async_fpv
+ fusesoc_core: lowrisc:fpv:prim_alert_rxtx_async_fpv
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: prim_esc_rxtx_fpv
+ fusesoc_core: lowrisc:fpv:prim_esc_rxtx_fpv
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: padctrl_fpv
+ fusesoc_core: lowrisc:fpv:padctrl_fpv
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: pinmux_fpv
+ fusesoc_core: lowrisc:fpv:pinmux_fpv
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: rv_plic_fpv
+ fusesoc_core: lowrisc:fpv:rv_plic_fpv
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: rv_plic_generic_fpv
+ fusesoc_core: lowrisc:fpv:rv_plic_generic_fpv
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: aes
+ fusesoc_core: lowrisc:ip:aes
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: alert_handler
+ fusesoc_core: lowrisc:ip:alert_handler
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: flash_ctrl
+ fusesoc_core: lowrisc:ip:flash_ctrl
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: gpio
+ fusesoc_core: lowrisc:ip:gpio
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: hmac
+ fusesoc_core: lowrisc:ip:hmac
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: i2c
+ fusesoc_core: lowrisc:ip:i2c
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: otp_ctrl
+ fusesoc_core: lowrisc:ip:otp_ctrl
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: pwrmgr
+ fusesoc_core: lowrisc:ip:pwrmgr
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: rv_core_ibex
+ fusesoc_core: lowrisc:ip:rv_core_ibex
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: rv_dm
+ fusesoc_core: lowrisc:ip:rv_dm
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: rv_timer
+ fusesoc_core: lowrisc:ip:rv_timer
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: spi_device
+ fusesoc_core: lowrisc:ip:spi_device
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: uart
+ fusesoc_core: lowrisc:ip:uart
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: usbdev
+ fusesoc_core: lowrisc:ip:usbdev
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ {
+ name: usbuart
+ fusesoc_core: lowrisc:ip:usbuart
+ import_cfgs: ["{proj_root}/hw/formal/data/common_fpv_cfg.hjson"]
+ }
+ ]
+}
