[fpv/script] Update tcl script

This PR updates fpv.tcl script with some latest jaspergold changes.

Signed-off-by: Cindy Chen <chencindy@opentitan.org>

hw/formal/tools/jaspergold/fpv.tcl

diff --git a/hw/formal/tools/jaspergold/fpv.tcl b/hw/formal/tools/jaspergold/fpv.tcl
index 21ab0b2..4df1900 100644
--- a/hw/formal/tools/jaspergold/fpv.tcl
+++ b/hw/formal/tools/jaspergold/fpv.tcl
@@ -9,10 +9,8 @@
 
 if {$env(COV) == 1} {
   check_cov -init -model {branch statement functional} \
-  -enable_prove_based_proof_core
+  -exclude_bind_hierarchies
 }
-set_task_compile_time_limit 1000s
-set_property_compile_time_limit 1000s
 
 #-------------------------------------------------------------------------
 # read design
@@ -24,13 +22,13 @@
   -f [glob *.scr]
 
 if {$env(DUT_TOP) == "prim_count_tb"} {
-  elaborate -bbox_a 4320 \
-            -top $env(DUT_TOP) \
+  elaborate -top $env(DUT_TOP) \
             -enable_sva_isunknown \
+            -disable_auto_bbox \
             -param OutSelDnCnt $OutSelDnCnt \
             -param CntStyle $CntStyle
 } else {
-  elaborate -bbox_a 4320 -top $env(DUT_TOP) -enable_sva_isunknown
+  elaborate -top $env(DUT_TOP) -enable_sva_isunknown -disable_auto_bbox
 }
 
 #-------------------------------------------------------------------------
@@ -155,16 +153,18 @@
   }
 }
 
+# Uncomment "jg_auto_coi_cov_waivers" to automatically waive out COI cover items which cannot
+# propagate to "relevant signals" (by default, top instance outputs). If you need to specify
+# include/exclude relevant signals manually, run "jg_auto_coi_cov_waivers -help" for more
+# options.
+jg_auto_coi_cov_waivers
+
 #-------------------------------------------------------------------------
 # configure proofgrid
 #-------------------------------------------------------------------------
 
 set_proofgrid_per_engine_max_local_jobs 2
 
-# Uncomment below 2 lines when using LSF:
-# set_proofgrid_mode lsf
-# set_proofgrid_per_engine_max_jobs 16
-
 #-------------------------------------------------------------------------
 # prove all assertions & report
 #-------------------------------------------------------------------------

hw/formal/tools/jaspergold/jaspergold.hjson

diff --git a/hw/formal/tools/jaspergold/jaspergold.hjson b/hw/formal/tools/jaspergold/jaspergold.hjson
index c403009..279bbd0 100644
--- a/hw/formal/tools/jaspergold/jaspergold.hjson
+++ b/hw/formal/tools/jaspergold/jaspergold.hjson
@@ -3,10 +3,9 @@
 // SPDX-License-Identifier: Apache-2.0
 {
   build_cmd: "{job_prefix} jg"
-  build_opts: ["{batch_mode_prefix} {formal_root}/tools/{tool}/{sub_flow}.tcl",
+  build_opts: ["-batch {formal_root}/tools/{tool}/{sub_flow}.tcl",
                "-proj jgproject",
-               "-allow_unsupported_OS",
-               "-command exit"]
+               "-allow_unsupported_OS"]
 
   exports: [
     {COMMON_MSG_TCL_PATH: "{formal_root}/tools/{tool}/jaspergold_common_message_process.tcl"}

hw/formal/tools/jaspergold/jaspergold_common_message_process.tcl

diff --git a/hw/formal/tools/jaspergold/jaspergold_common_message_process.tcl b/hw/formal/tools/jaspergold/jaspergold_common_message_process.tcl
index d08102f..97f557a 100644
--- a/hw/formal/tools/jaspergold/jaspergold_common_message_process.tcl
+++ b/hw/formal/tools/jaspergold/jaspergold_common_message_process.tcl
@@ -36,3 +36,4 @@
 # "initial construct ignored"
 set_message -disable VERI-1060
 
+set_prove_verbosity 4