[fpv/common] Fix fpv run files and dependency
Since fpv.tcl file deletes the statement to search all the bind files,
in the formal.core, I manually add the bind files.
Set time limit to FPV run files to 2 hours.
Temp delete the modules that do not have a bind file, added a TODO to
decide how to add them back.
Add liveness, deadend, and conflict check in fpv.tcl file
Signed-off-by: Cindy Chen <chencindy@google.com>
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"
)
#-------------------------------------------------------------------------
