[formal] cleanup fpv_all
Add env variable for 1."assumption and assertion checks"
2. "coverage"
Reduce the parallel engine number
Add back prim_alert_rxtx_async_fpv core file
Signed-off-by: Cindy Chen <chencindy@google.com>
diff --git a/hw/formal/fpv b/hw/formal/fpv
index 032b411..fbf5720 100755
--- a/hw/formal/fpv
+++ b/hw/formal/fpv
@@ -11,31 +11,44 @@
#
# Here are some examples:
# fpv rv_plic_fpv
-# fpv pinmux_fpv
+# fpv gpio
#
# More options:
# -p: provide core file path
# -gui: run JasperGold GUI
+# -cov: run coverage
+# -chk: run checks for assumptions: deadlock, conflict, live chks
#
# Example:
-# fpv pinmux_fpv -p vip:pinmux_fpv -gui
+# fpv pinmux_fpv -p vip:pinmux_fpv -gui -cov
#
# Note that the module to be tested needs to have an _fpv testbench
# and a corresponding core file for this to work.
+
export FPV_TOP=$1
shift
gui=0
+export COV=0
+export CHECK=0
while [ "$1" != "" ]; do
case "$1" in
"-p")
shift
- export CORE_PATH=$1
+ CORE_PATH=$1
;;
"-gui")
gui=1
echo "using jasper gold GUI"
;;
+ "-cov")
+ COV=1
+ echo "enable FPV coverage"
+ ;;
+ "-chk")
+ CHECK=1
+ echo "enable assumption checks"
+ ;;
esac
shift
done
diff --git a/hw/formal/fpv.tcl b/hw/formal/fpv.tcl
index ff5a4d5..399321c 100644
--- a/hw/formal/fpv.tcl
+++ b/hw/formal/fpv.tcl
@@ -11,6 +11,10 @@
# "parameter declared inside package XXX shall be treated as localparam".
set_message -disable VERI-2418
+if {$env(COV) == 1} {
+ check_cov -init -model {branch statement functional} \
+ -enable_prove_based_proof_core
+}
#-------------------------------------------------------------------------
# read design
@@ -142,14 +146,17 @@
assume {scanmode_i == 1}
}
-check_assumptions -conflict
-check_assumptions -live
-check_assumptions -dead_end
+# run once to check if assumptions have any conflict
+if {$env(CHECK) == 1} {
+ check_assumptions -conflict
+ check_assumptions -live
+ check_assumptions -dead_end
+}
#-------------------------------------------------------------------------
# configure proofgrid
#-------------------------------------------------------------------------
-set_proofgrid_per_engine_max_local_jobs 16
+set_proofgrid_per_engine_max_local_jobs 2
# Uncomment below 2 lines when using LSF:
# set_proofgrid_mode lsf
@@ -160,10 +167,13 @@
#-------------------------------------------------------------------------
# time limit set to 2 hours
get_reset_info -x_value -with_reset_pin
-prove -all -time_limit 24h
+prove -all -time_limit 4h
report
#-------------------------------------------------------------------------
# check coverage and report
#-------------------------------------------------------------------------
-
-
+if {$env(COV) == 1} {
+ check_cov -measure
+ check_cov -report -type all -no_return -report_file cover.html \
+ -html -force -exclude { reset waived }
+}
diff --git a/hw/formal/fpv_all b/hw/formal/fpv_all
index fe8feb3..65f2f04 100755
--- a/hw/formal/fpv_all
+++ b/hw/formal/fpv_all
@@ -47,7 +47,7 @@
format1="%28s %10s %10s %10s \n"
format2="%28s %10s %9.0f%% %9.0f%% \n"
printf "${format1}" "Block" "Asserts" "Covered" "Proven"
-echo "----------------------------------------------------"
+echo "-----------------------------------------------------------------"
#-------------------------------------------------------------------------
# run fpv and summarize results
diff --git a/hw/ip/prim/fpv/prim_alert_rxtx_async_fpv.core b/hw/ip/prim/fpv/prim_alert_rxtx_async_fpv.core
new file mode 100644
index 0000000..fbbc23b
--- /dev/null
+++ b/hw/ip/prim/fpv/prim_alert_rxtx_async_fpv.core
@@ -0,0 +1,25 @@
+CAPI=2:
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+name: "lowrisc:fpv:prim_alert_rxtx_async_fpv:0.1"
+description: "ALERT_HANDLER rxtx async FPV target"
+filesets:
+ files_fpv:
+ depend:
+ - lowrisc:prim:all
+ files:
+ - vip/prim_alert_rxtx_async_assert_fpv.sv
+ - tb/prim_alert_rxtx_async_fpv.sv
+ - tb/prim_alert_rxtx_async_bind_fpv.sv
+ file_type: systemVerilogSource
+
+targets:
+ default:
+ # note, this setting is just used
+ # to generate a file list for jg
+ default_tool: icarus
+ filesets:
+ - files_fpv
+ toplevel:
+ - prim_alert_rxtx_async_fpv
