[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