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