[formal] support FPV_ALL
FPV_ALL script has been broken due to fusesoc optimzation from the fpv
script. Currently support fpv_all again
But exclude top_earlgrey and usbuart for compile and not converge issues
Signed-off-by: Cindy Chen <chencindy@google.com>
diff --git a/hw/formal/fpv b/hw/formal/fpv
index 7fcdc99..032b411 100755
--- a/hw/formal/fpv
+++ b/hw/formal/fpv
@@ -50,7 +50,11 @@
\rm -Rf build jgproject
# we just run the setup for the default target in order to generate the filelist
if [ "${CORE_PATH}" == "" ]; then
- CORE_PATH="fpv:${FPV_TOP}"
+ if [[ $FPV_TOP == *"_fpv" ]]; then
+ CORE_PATH="fpv:${FPV_TOP}"
+ else
+ CORE_PATH="ip:${FPV_TOP}:0.1"
+ fi
fi
echo "core_file path: lowrisc:${CORE_PATH}"
diff --git a/hw/formal/fpv_all b/hw/formal/fpv_all
index f26dec5..a240bb7 100755
--- a/hw/formal/fpv_all
+++ b/hw/formal/fpv_all
@@ -15,7 +15,7 @@
"uart"
"hmac"
"flash_ctrl"
- "usbuart"
+ #"usbuart"
"usbdev"
# "usb_fs_nb_pe" This module doesn't have any assertions yet
# TODO: bind files are deleted
@@ -24,9 +24,10 @@
# "tlul_socket_m1"
# "sram2tlul"
# "xbar_main"
- "top_earlgrey"
+ #"top_earlgrey"
# run formal on dedicated FPV testbenches
"prim_lfsr_fpv"
+ "prim_fifo_sync_fpv"
"prim_alert_rxtx_fpv"
"prim_alert_rxtx_async_fpv"
"prim_esc_rxtx_fpv"
@@ -41,8 +42,8 @@
printf "FPV RESULTS PER BLOCK\n"
printf "Below table shows the total number of assertions, and\n"
printf "the percentages of covered and proven assertions.\n\n"
-format1="%18s %10s %10s %10s \n"
-format2="%18s %10s %9.0f%% %9.0f%% \n"
+format1="%28s %10s %10s %10s \n"
+format2="%28s %10s %9.0f%% %9.0f%% \n"
printf "${format1}" "Block" "Asserts" "Covered" "Proven"
echo "----------------------------------------------------"
@@ -53,7 +54,7 @@
for block in "${blocks[@]}" ; do
- fpv $block > /dev/null 2>&1
+ ./fpv $block > /dev/null 2>&1
cp fpv.log fpv_${block}.log
# summarize results
