diff --git a/hw/formal/formal.core b/hw/formal/formal.core
index e5222a7..369aa4c 100644
--- a/hw/formal/formal.core
+++ b/hw/formal/formal.core
@@ -10,21 +10,30 @@
 filesets:
   files_rtl_generic:
     depend:
-      - lowrisc:fpv:prim_lfsr_fpv
-      - lowrisc:fpv:prim_alert_rxtx_fpv
-      - lowrisc:fpv:prim_esc_rxtx_fpv
       - lowrisc:ip:rv_timer
       - lowrisc:ip:hmac
       - lowrisc:systems:top_earlgrey
-      - lowrisc:fpv:rv_plic_fpv
       - lowrisc:ip:usbuart
       - lowrisc:ip:usbdev
       - lowrisc:ip:usbfs_nb_pe
-      - lowrisc:tlul:adapter_sram
-      - lowrisc:tlul:socket_1n
-      - lowrisc:tlul:socket_m1
+      # files with dedicated fpv tb
+      - lowrisc:fpv:prim_lfsr_fpv
+      - lowrisc:fpv:prim_alert_rxtx_fpv
+      - lowrisc:fpv:prim_esc_rxtx_fpv
       - lowrisc:fpv:pinmux_fpv
       - lowrisc:fpv:padctrl_fpv
+      - lowrisc:fpv:rv_plic_fpv
+    files:
+      - ../ip/gpio/dv/tb/gpio_bind.sv
+      - ../ip/hmac/dv/tb/hmac_bind.sv
+      - ../ip/rv_timer/dv/tb/rv_timer_bind.sv
+      - ../ip/rv_core_ibex/dv/tb/core_ibex_bind.sv
+      - ../ip/rv_dm/dv/tb/rv_dm_bind.sv
+      - ../ip/uart/dv/tb/uart_bind.sv
+      - ../ip/flash_ctrl/dv/tb/flash_ctrl_bind.sv
+      - ../ip/usbuart/dv/tb/usbuart_bind.sv
+      - ../ip/usbdev/dv/tb/usbdev_bind.sv
+    file_type: systemVerilogSource
 
 targets:
   sim:
diff --git a/hw/formal/fpv.tcl b/hw/formal/fpv.tcl
index 3bdbf5c..9524f92 100644
--- a/hw/formal/fpv.tcl
+++ b/hw/formal/fpv.tcl
@@ -22,6 +22,9 @@
 
 elaborate -top $env(FPV_TOP)
 
+check_assumptions -conflict
+check_assumptions -live
+check_assumptions -dead_end
 #-------------------------------------------------------------------------
 # specify clock(s) and reset(s)
 #-------------------------------------------------------------------------
@@ -52,8 +55,7 @@
 } elseif {$env(FPV_TOP) == "top_earlgrey"} {
   clock clk_i -both_edges
   clock jtag_tck_i
-  clock cio_spi_device_sck_p2d_i
-  reset -expr {!rst_ni !jtag_trst_ni cio_spi_device_csb_p2d_i}
+  reset -expr {!rst_ni !jtag_trst_ni}
 } elseif {$env(FPV_TOP) == "xbar_main"} {
   clock clk_main_i -both_edges
   reset -expr {!rst_main_ni}
@@ -154,6 +156,7 @@
 #-------------------------------------------------------------------------
 # prove all assertions & report
 #-------------------------------------------------------------------------
+# time limit set to 2 hours
 get_reset_info -x_value -with_reset_pin
-prove -all
+prove -all -time_limit 120m
 report
diff --git a/hw/formal/fpv_all b/hw/formal/fpv_all
index af67f96..f26dec5 100755
--- a/hw/formal/fpv_all
+++ b/hw/formal/fpv_all
@@ -10,7 +10,6 @@
   "gpio"
   "rv_core_ibex"
   "rv_dm"
-  "rv_plic"
   "spi_device"
   "rv_timer"
   "uart"
@@ -19,19 +18,21 @@
   "usbuart"
   "usbdev"
   # "usb_fs_nb_pe" This module doesn't have any assertions yet
-  "tlul_adapter_sram"
-  "tlul_socket_1n"
-  "tlul_socket_m1"
-  "sram2tlul"
-  "xbar_main"
+  # TODO: bind files are deleted
+  # "tlul_adapter_sram"
+  # "tlul_socket_1n"
+  # "tlul_socket_m1"
+  # "sram2tlul"
+  # "xbar_main"
   "top_earlgrey"
   # run formal on dedicated FPV testbenches
-  "prim_lfsr_tb"
-  "prim_alert_rxtx_tb"
-  "prim_alert_rxtx_async_tb"
-  "prim_esc_rxtx_tb"
-  "pinmux_tb"
-  "padctrl_tb"
+  "prim_lfsr_fpv"
+  "prim_alert_rxtx_fpv"
+  "prim_alert_rxtx_async_fpv"
+  "prim_esc_rxtx_fpv"
+  "pinmux_fpv"
+  "padctrl_fpv"
+  "rv_plic_fpv"
 )
 
 #-------------------------------------------------------------------------