[fpv] Fix fusesoc dependecy issue
When CSR assertions can be generated automatically, we encountered some
fusesoc dependency issue. Because CSR auto-gen assertions depend on
RTL(reg core file), for most of IPs, there isn't an independent reg file
core, thus the auto-gen file directly used the rtl core file. And formal
target is build on the default RTL core file. Now we try to import the
CSR auto-gen core file, and this creates a dependency issue.
To solve this issue, the new formal core file is built on IP_sva.core
instead of RTL core file.
Signed-off-by: Cindy Chen <chencindy@google.com>
diff --git a/hw/ip/aes/aes.core b/hw/ip/aes/aes.core
index d5fcdef..2586fde 100644
--- a/hw/ip/aes/aes.core
+++ b/hw/ip/aes/aes.core
@@ -60,11 +60,6 @@
- lowrisc:lint:common
- lowrisc:lint:comportable
- files_formal:
- files:
- - dv/tb/aes_bind.sv
- file_type: systemVerilogSource
-
parameters:
SYNTHESIS:
datatype: bool
@@ -77,13 +72,6 @@
- tool_verilator ? (files_verilator_waiver)
- tool_ascentlint ? (files_ascentlint_waiver)
- tool_veriblelint ? (files_veriblelint_waiver)
- - target_formal ? (files_formal)
- - files_rtl
- toplevel: aes
-
- formal:
- filesets:
- - files_formal
- files_rtl
toplevel: aes
diff --git a/hw/ip/aes/dv/sva/aes_sva.core b/hw/ip/aes/dv/sva/aes_sva.core
index 674f2f6..18e4569 100644
--- a/hw/ip/aes/dv/sva/aes_sva.core
+++ b/hw/ip/aes/dv/sva/aes_sva.core
@@ -13,6 +13,10 @@
- aes_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:aes
+
generate:
csr_assert_gen:
generator: csr_assert_gen
@@ -21,8 +25,15 @@
depend: lowrisc:ip:aes
targets:
- default:
+ default: &default_target
filesets:
- files_dv
generate:
- csr_assert_gen
+
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: aes
diff --git a/hw/ip/alert_handler/alert_handler.core b/hw/ip/alert_handler/alert_handler.core
index 3ff7156..c83489d 100644
--- a/hw/ip/alert_handler/alert_handler.core
+++ b/hw/ip/alert_handler/alert_handler.core
@@ -11,11 +11,6 @@
- lowrisc:ip:alert_handler_reg
- lowrisc:ip:alert_handler_component
- files_formal:
- files:
- - dv/tb/alert_handler_bind.sv
- file_type: systemVerilogSource
-
parameters:
SYNTHESIS:
datatype: bool
@@ -25,16 +20,9 @@
targets:
default: &default_target
filesets:
- - target_formal ? (files_formal)
- files_rtl
toplevel: alert_handler
- formal:
- filesets:
- - files_rtl
- - files_formal
- toplevel: alert_handler
-
lint:
<<: *default_target
default_tool: verilator
diff --git a/hw/ip/alert_handler/dv/sva/alert_handler_sva.core b/hw/ip/alert_handler/dv/sva/alert_handler_sva.core
index fb88846..2899f19 100644
--- a/hw/ip/alert_handler/dv/sva/alert_handler_sva.core
+++ b/hw/ip/alert_handler/dv/sva/alert_handler_sva.core
@@ -13,6 +13,10 @@
- alert_handler_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:alert_handler
+
generate:
csr_assert_gen:
generator: csr_assert_gen
@@ -21,8 +25,15 @@
depend: lowrisc:ip:alert_handler_reg
targets:
- default:
+ default: &default_target
filesets:
- files_dv
generate:
- csr_assert_gen
+
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: alert_handler
diff --git a/hw/ip/entropy_src/dv/sva/entropy_src_sva.core b/hw/ip/entropy_src/dv/sva/entropy_src_sva.core
index 35a447d..224f26c 100644
--- a/hw/ip/entropy_src/dv/sva/entropy_src_sva.core
+++ b/hw/ip/entropy_src/dv/sva/entropy_src_sva.core
@@ -13,6 +13,10 @@
- entropy_src_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:entropy_src
+
generate:
csr_assert_gen:
generator: csr_assert_gen
@@ -21,8 +25,15 @@
depend: lowrisc:ip:entropy_src
targets:
- default:
+ default: &default_target
filesets:
- files_dv
generate:
- csr_assert_gen
+
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: entropy_src
diff --git a/hw/ip/flash_ctrl/dv/sva/flash_ctrl_sva.core b/hw/ip/flash_ctrl/dv/sva/flash_ctrl_sva.core
index 63a52a4..a4eb36d 100644
--- a/hw/ip/flash_ctrl/dv/sva/flash_ctrl_sva.core
+++ b/hw/ip/flash_ctrl/dv/sva/flash_ctrl_sva.core
@@ -13,6 +13,10 @@
- flash_ctrl_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:flash_ctrl
+
generate:
csr_assert_gen:
generator: csr_assert_gen
@@ -21,8 +25,15 @@
depend: lowrisc:ip:flash_ctrl
targets:
- default:
+ default: &default_target
filesets:
- files_dv
generate:
- csr_assert_gen
+
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: flash_ctrl
diff --git a/hw/ip/flash_ctrl/flash_ctrl.core b/hw/ip/flash_ctrl/flash_ctrl.core
index 1363bfa..e2bd570 100644
--- a/hw/ip/flash_ctrl/flash_ctrl.core
+++ b/hw/ip/flash_ctrl/flash_ctrl.core
@@ -59,11 +59,6 @@
- lowrisc:lint:common
- lowrisc:lint:comportable
- files_formal:
- files:
- - dv/tb/flash_ctrl_bind.sv
- file_type: systemVerilogSource
-
parameters:
SYNTHESIS:
datatype: bool
@@ -76,16 +71,9 @@
- tool_verilator ? (files_verilator_waiver)
- tool_ascentlint ? (files_ascentlint_waiver)
- tool_veriblelint ? (files_veriblelint_waiver)
- - target_formal ? (files_formal)
- files_rtl
toplevel: flash_ctrl
- formal:
- filesets:
- - files_rtl
- - files_formal
- toplevel: flash_ctrl
-
lint:
<<: *default_target
default_tool: verilator
diff --git a/hw/ip/gpio/dv/sva/gpio_sva.core b/hw/ip/gpio/dv/sva/gpio_sva.core
index a2837c6..0fb097c 100644
--- a/hw/ip/gpio/dv/sva/gpio_sva.core
+++ b/hw/ip/gpio/dv/sva/gpio_sva.core
@@ -13,6 +13,10 @@
- gpio_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:gpio
+
generate:
csr_assert_gen:
generator: csr_assert_gen
@@ -21,8 +25,15 @@
depend: lowrisc:ip:gpio
targets:
- default:
+ default: &default_target
filesets:
- files_dv
generate:
- csr_assert_gen
+
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: gpio
diff --git a/hw/ip/gpio/gpio.core b/hw/ip/gpio/gpio.core
index a6533e1..0517262 100644
--- a/hw/ip/gpio/gpio.core
+++ b/hw/ip/gpio/gpio.core
@@ -39,11 +39,6 @@
- lowrisc:lint:common
- lowrisc:lint:comportable
- files_formal:
- files:
- - dv/tb/gpio_bind.sv
- file_type: systemVerilogSource
-
parameters:
SYNTHESIS:
datatype: bool
@@ -56,16 +51,9 @@
- tool_verilator ? (files_verilator_waiver)
- tool_ascentlint ? (files_ascentlint_waiver)
- tool_veriblelint ? (files_veriblelint_waiver)
- - target_formal ? (files_formal)
- files_rtl
toplevel: gpio
- formal:
- filesets:
- - files_rtl
- - files_formal
- toplevel: gpio
-
lint:
<<: *default_target
default_tool: verilator
@@ -80,5 +68,3 @@
mode: lint-only
verilator_options:
- "-Wall"
-
-
diff --git a/hw/ip/hmac/dv/sva/hmac_sva.core b/hw/ip/hmac/dv/sva/hmac_sva.core
index a7b4b98..d5754c9 100644
--- a/hw/ip/hmac/dv/sva/hmac_sva.core
+++ b/hw/ip/hmac/dv/sva/hmac_sva.core
@@ -13,6 +13,10 @@
- hmac_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:hmac
+
generate:
csr_assert_gen:
generator: csr_assert_gen
@@ -21,8 +25,15 @@
depend: lowrisc:ip:hmac
targets:
- default:
+ default: &default_target
filesets:
- files_dv
generate:
- csr_assert_gen
+
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: hmac
diff --git a/hw/ip/hmac/hmac.core b/hw/ip/hmac/hmac.core
index 9488395..58a9560 100644
--- a/hw/ip/hmac/hmac.core
+++ b/hw/ip/hmac/hmac.core
@@ -43,11 +43,6 @@
- lowrisc:lint:common
- lowrisc:lint:comportable
- files_formal:
- files:
- - dv/tb/hmac_bind.sv
- file_type: systemVerilogSource
-
parameters:
SYNTHESIS:
datatype: bool
@@ -60,16 +55,9 @@
- tool_verilator ? (files_verilator_waiver)
- tool_ascentlint ? (files_ascentlint_waiver)
- tool_veriblelint ? (files_veriblelint_waiver)
- - target_formal ? (files_formal)
- files_rtl
toplevel: hmac
- formal:
- filesets:
- - files_rtl
- - files_formal
- toplevel: hmac
-
lint:
<<: *default_target
default_tool: verilator
@@ -84,5 +72,3 @@
mode: lint-only
verilator_options:
- "-Wall"
-
-
diff --git a/hw/ip/i2c/dv/sva/i2c_sva.core b/hw/ip/i2c/dv/sva/i2c_sva.core
index c1774f6..a492097 100644
--- a/hw/ip/i2c/dv/sva/i2c_sva.core
+++ b/hw/ip/i2c/dv/sva/i2c_sva.core
@@ -13,6 +13,10 @@
- i2c_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:i2c
+
generate:
csr_assert_gen:
generator: csr_assert_gen
@@ -21,8 +25,15 @@
depend: lowrisc:ip:i2c
targets:
- default:
+ default: &default_target
filesets:
- files_dv
generate:
- csr_assert_gen
+
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: i2c
diff --git a/hw/ip/i2c/i2c.core b/hw/ip/i2c/i2c.core
index 64d8936..972aacf 100644
--- a/hw/ip/i2c/i2c.core
+++ b/hw/ip/i2c/i2c.core
@@ -42,11 +42,6 @@
- lowrisc:lint:common
- lowrisc:lint:comportable
- files_formal:
- files:
- - dv/tb/i2c_bind.sv
- file_type: systemVerilogSource
-
parameters:
SYNTHESIS:
datatype: bool
@@ -59,16 +54,9 @@
- tool_verilator ? (files_verilator_waiver)
- tool_ascentlint ? (files_ascentlint_waiver)
- tool_veriblelint ? (files_veriblelint_waiver)
- - target_formal ? (files_formal)
- files_rtl
toplevel: i2c
- formal:
- filesets:
- - files_rtl
- - files_formal
- toplevel: i2c
-
lint:
<<: *default_target
default_tool: verilator
@@ -83,5 +71,3 @@
mode: lint-only
verilator_options:
- "-Wall"
-
-
diff --git a/hw/ip/keymgr/dv/sva/keymgr_sva.core b/hw/ip/keymgr/dv/sva/keymgr_sva.core
index 4f4ba7e..bab8b47 100644
--- a/hw/ip/keymgr/dv/sva/keymgr_sva.core
+++ b/hw/ip/keymgr/dv/sva/keymgr_sva.core
@@ -13,6 +13,10 @@
- keymgr_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:keymgr
+
generate:
csr_assert_gen:
generator: csr_assert_gen
@@ -21,8 +25,15 @@
depend: lowrisc:ip:keymgr
targets:
- default:
+ default: &default_target
filesets:
- files_dv
generate:
- csr_assert_gen
+
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: keymgr
diff --git a/hw/ip/keymgr/keymgr.core b/hw/ip/keymgr/keymgr.core
index b81e0a7..fd7ae4d 100644
--- a/hw/ip/keymgr/keymgr.core
+++ b/hw/ip/keymgr/keymgr.core
@@ -41,11 +41,6 @@
- lint/keymgr.waiver
file_type: waiver
- files_formal:
- files:
- - dv/tb/keymgr_bind.sv
- file_type: systemVerilogSource
-
parameters:
SYNTHESIS:
datatype: bool
@@ -57,16 +52,9 @@
filesets:
- tool_verilator ? (files_verilator_waiver)
- tool_ascentlint ? (files_ascentlint_waiver)
- - target_formal ? (files_formal)
- files_rtl
toplevel: keymgr
- formal:
- filesets:
- - files_rtl
- - files_formal
- toplevel: keymgr
-
lint:
<<: *default_target
default_tool: verilator
diff --git a/hw/ip/otp_ctrl/dv/sva/otp_ctrl_sva.core b/hw/ip/otp_ctrl/dv/sva/otp_ctrl_sva.core
index e362fab..91b96b5 100644
--- a/hw/ip/otp_ctrl/dv/sva/otp_ctrl_sva.core
+++ b/hw/ip/otp_ctrl/dv/sva/otp_ctrl_sva.core
@@ -13,6 +13,10 @@
- otp_ctrl_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:otp_ctrl
+
generate:
csr_assert_gen:
generator: csr_assert_gen
@@ -21,8 +25,15 @@
depend: lowrisc:ip:otp_ctrl_pkg
targets:
- default:
+ default: &default_target
filesets:
- files_dv
generate:
- csr_assert_gen
+
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: otp_ctrl
diff --git a/hw/ip/otp_ctrl/otp_ctrl.core b/hw/ip/otp_ctrl/otp_ctrl.core
index 9bb0deb..5925fb3 100644
--- a/hw/ip/otp_ctrl/otp_ctrl.core
+++ b/hw/ip/otp_ctrl/otp_ctrl.core
@@ -47,11 +47,6 @@
- lint/otp_ctrl.waiver
file_type: waiver
- files_formal:
- files:
- - dv/tb/otp_ctrl_bind.sv
- file_type: systemVerilogSource
-
parameters:
SYNTHESIS:
datatype: bool
@@ -63,16 +58,9 @@
filesets:
- tool_verilator ? (files_verilator_waiver)
- tool_ascentlint ? (files_ascentlint_waiver)
- - target_formal ? (files_formal)
- files_rtl
toplevel: otp_ctrl
- formal:
- filesets:
- - files_rtl
- - files_formal
- toplevel: otp_ctrl
-
lint:
<<: *default_target
default_tool: verilator
diff --git a/hw/ip/rv_timer/dv/sva/rv_timer_sva.core b/hw/ip/rv_timer/dv/sva/rv_timer_sva.core
index 6f3cd33..2b67caa 100644
--- a/hw/ip/rv_timer/dv/sva/rv_timer_sva.core
+++ b/hw/ip/rv_timer/dv/sva/rv_timer_sva.core
@@ -13,6 +13,10 @@
- rv_timer_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:rv_timer
+
generate:
csr_assert_gen:
generator: csr_assert_gen
@@ -21,8 +25,15 @@
depend: lowrisc:ip:rv_timer
targets:
- default:
+ default: &default_target
filesets:
- files_dv
generate:
- csr_assert_gen
+
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: rv_timer
diff --git a/hw/ip/rv_timer/rv_timer.core b/hw/ip/rv_timer/rv_timer.core
index 24b5a9a..014023b 100644
--- a/hw/ip/rv_timer/rv_timer.core
+++ b/hw/ip/rv_timer/rv_timer.core
@@ -40,33 +40,20 @@
- lowrisc:lint:common
- lowrisc:lint:comportable
- files_formal:
- files:
- - dv/tb/rv_timer_bind.sv
- file_type: systemVerilogSource
-
parameters:
SYNTHESIS:
datatype: bool
paramtype: vlogdefine
-
targets:
default: &default_target
filesets:
- tool_verilator ? (files_verilator_waiver)
- tool_ascentlint ? (files_ascentlint_waiver)
- tool_veriblelint ? (files_veriblelint_waiver)
- - target_formal ? (files_formal)
- files_rtl
toplevel: rv_timer
- formal:
- filesets:
- - files_rtl
- - files_formal
- toplevel: rv_timer
-
lint:
<<: *default_target
default_tool: verilator
@@ -81,5 +68,3 @@
mode: lint-only
verilator_options:
- "-Wall"
-
-
diff --git a/hw/ip/spi_device/dv/sva/spi_device_sva.core b/hw/ip/spi_device/dv/sva/spi_device_sva.core
index 23cdd99..69193c9 100644
--- a/hw/ip/spi_device/dv/sva/spi_device_sva.core
+++ b/hw/ip/spi_device/dv/sva/spi_device_sva.core
@@ -13,6 +13,10 @@
- spi_device_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:spi_device
+
generate:
csr_assert_gen:
generator: csr_assert_gen
@@ -21,8 +25,15 @@
depend: lowrisc:ip:spi_device
targets:
- default:
+ default: &default_target
filesets:
- files_dv
generate:
- csr_assert_gen
+
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: spi_device
diff --git a/hw/ip/spi_device/spi_device.core b/hw/ip/spi_device/spi_device.core
index 72e2dd9..f5b0d63 100644
--- a/hw/ip/spi_device/spi_device.core
+++ b/hw/ip/spi_device/spi_device.core
@@ -48,11 +48,6 @@
- lowrisc:lint:common
- lowrisc:lint:comportable
- files_formal:
- files:
- - dv/tb/spi_device_bind.sv
- file_type: systemVerilogSource
-
parameters:
SYNTHESIS:
datatype: bool
@@ -65,16 +60,9 @@
- tool_verilator ? (files_verilator_waiver)
- tool_ascentlint ? (files_ascentlint_waiver)
- tool_veriblelint ? (files_veriblelint_waiver)
- - target_formal ? (files_formal)
- files_rtl
toplevel: spi_device
- formal:
- filesets:
- - files_rtl
- - files_formal
- toplevel: spi_device
-
lint:
<<: *default_target
default_tool: verilator
@@ -89,5 +77,3 @@
mode: lint-only
verilator_options:
- "-Wall"
-
-
diff --git a/hw/ip/uart/dv/sva/uart_sva.core b/hw/ip/uart/dv/sva/uart_sva.core
index 9b397e8..73c14bc 100644
--- a/hw/ip/uart/dv/sva/uart_sva.core
+++ b/hw/ip/uart/dv/sva/uart_sva.core
@@ -13,6 +13,10 @@
- uart_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:uart
+
generate:
csr_assert_gen:
generator: csr_assert_gen
@@ -21,8 +25,15 @@
depend: lowrisc:ip:uart
targets:
- default:
+ default: &default_target
filesets:
- files_dv
generate:
- csr_assert_gen
+
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: uart
diff --git a/hw/ip/uart/uart.core b/hw/ip/uart/uart.core
index 75bf2e2..0405cbf 100644
--- a/hw/ip/uart/uart.core
+++ b/hw/ip/uart/uart.core
@@ -43,11 +43,6 @@
- lowrisc:lint:common
- lowrisc:lint:comportable
- files_formal:
- files:
- - dv/tb/uart_bind.sv
- file_type: systemVerilogSource
-
parameters:
SYNTHESIS:
datatype: bool
@@ -60,16 +55,9 @@
- tool_verilator ? (files_verilator_waiver)
- tool_ascentlint ? (files_ascentlint_waiver)
- tool_veriblelint ? (files_veriblelint_waiver)
- - target_formal ? (files_formal)
- files_rtl
toplevel: uart
- formal:
- filesets:
- - files_rtl
- - files_formal
- toplevel: uart
-
lint:
<<: *default_target
default_tool: verilator
diff --git a/hw/top_earlgrey/fpv/top_earlgrey_fpv_cfgs.hjson b/hw/top_earlgrey/fpv/top_earlgrey_fpv_cfgs.hjson
index 6b268a3..6a7dabf 100644
--- a/hw/top_earlgrey/fpv/top_earlgrey_fpv_cfgs.hjson
+++ b/hw/top_earlgrey/fpv/top_earlgrey_fpv_cfgs.hjson
@@ -18,71 +18,160 @@
name: prim_arbiter_ppc_fpv
fusesoc_core: lowrisc:fpv:prim_arbiter_ppc_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: prim_arbiter_tree_fpv
fusesoc_core: lowrisc:fpv:prim_arbiter_tree_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: prim_arbiter_fixed_fpv
fusesoc_core: lowrisc:fpv:prim_arbiter_fixed_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: prim_lfsr_fpv
fusesoc_core: lowrisc:fpv:prim_lfsr_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: prim_fifo_sync_fpv
fusesoc_core: lowrisc:fpv:prim_fifo_sync_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: prim_alert_rxtx_fpv
fusesoc_core: lowrisc:fpv:prim_alert_rxtx_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: prim_alert_rxtx_async_fpv
fusesoc_core: lowrisc:fpv:prim_alert_rxtx_async_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: prim_esc_rxtx_fpv
fusesoc_core: lowrisc:fpv:prim_esc_rxtx_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: prim_packer_fpv
fusesoc_core: lowrisc:fpv:prim_packer_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: padctrl_fpv
fusesoc_core: lowrisc:fpv:padctrl_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: pinmux_fpv
fusesoc_core: lowrisc:fpv:pinmux_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: rv_plic_fpv
fusesoc_core: lowrisc:fpv:rv_plic_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: rv_plic_generic_fpv
fusesoc_core: lowrisc:fpv:rv_plic_generic_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
}
{
name: sha3pad_fpv
fusesoc_core: lowrisc:fpv:sha3pad_fpv
import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: true
+ }
+ // Below are IPs that already has a DV testbench,
+ // FPV only verifies TLUL interface and build-in assertions,
+ // so will not collect FPV coverage.
+ {
+ name: aes
+ fusesoc_core: lowrisc:dv:aes_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: false
+ }
+ {
+ name: alert_handler
+ fusesoc_core: lowrisc:dv:alert_handler_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: false
+ }
+ {
+ name: entropy_src
+ fusesoc_core: lowrisc:dv:entropy_src_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: false
+ }
+ {
+ name: flash_ctrl
+ fusesoc_core: lowrisc:dv:flash_ctrl_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: false
+ }
+ {
+ name: gpio
+ fusesoc_core: lowrisc:dv:gpio_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: false
+ }
+ {
+ name: hmac
+ fusesoc_core: lowrisc:dv:hmac_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: false
+ }
+ {
+ name: i2c
+ fusesoc_core: lowrisc:dv:i2c_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: false
+ }
+ {
+ name: keymgr
+ fusesoc_core: lowrisc:dv:keymgr_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: false
+ }
+ {
+ name: otp_ctrl
+ fusesoc_core: lowrisc:dv:otp_ctrl_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: false
+ }
+ {
+ name: rv_timer
+ fusesoc_core: lowrisc:dv:rv_timer_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: false
+ }
+ {
+ name: spi_device
+ fusesoc_core: lowrisc:dv:spi_device_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: false
+ }
+ {
+ name: uart
+ fusesoc_core: lowrisc:dv:uart_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ cov: false
}
]
}
diff --git a/util/uvmdvgen/sva.core.tpl b/util/uvmdvgen/sva.core.tpl
index 89863d7..3324369 100644
--- a/util/uvmdvgen/sva.core.tpl
+++ b/util/uvmdvgen/sva.core.tpl
@@ -15,6 +15,10 @@
- ${name}_bind.sv
file_type: systemVerilogSource
+ files_formal:
+ depend:
+ - lowrisc:ip:${name}
+
% if has_ral:
generate:
csr_assert_gen:
@@ -25,10 +29,16 @@
% endif
targets:
- default:
+ default: &default_target
filesets:
- files_dv
% if has_ral:
generate:
- csr_assert_gen
+ formal:
+ <<: *default_target
+ filesets:
+ - files_formal
+ - files_dv
+ toplevel: ${name}
% endif
