hw/formal/fpv_all

#!/bin/bash

# to run JasperGold FPV on all modules, type
#   fpv_all

tool="jg"
while [ "$1" != "" ]; do
  case "$1" in
    "-t")
      shift
      tool=$1
      ;;
  esac
  shift
done

#-------------------------------------------------------------------------
# list all blocks
#-------------------------------------------------------------------------
declare -a blocks=(
  "alert_handler"
  "aes"
  "gpio"
  "flash_ctrl"
  "hmac"
  "otp_ctrl"
  "pwrmgr"
  "rv_core_ibex"
  "rv_dm"
  "rv_timer"
  "spi_device"
  "uart"
  "usbdev"
  "usbuart"
  #"top_earlgrey"
  # run formal on dedicated FPV testbenches
  "prim_arbiter_ppc_fpv"
  "prim_arbiter_tree_fpv"
  "prim_arbiter_fixed_fpv"
  "prim_alert_rxtx_fpv"
  "prim_alert_rxtx_async_fpv"
  "prim_esc_rxtx_fpv"
  "prim_lfsr_fpv"
  "prim_fifo_sync_fpv"
  "pinmux_fpv"
  "padctrl_fpv"
  "rv_plic_fpv"
  "rv_plic_generic_fpv"
)

#-------------------------------------------------------------------------
# print header
#-------------------------------------------------------------------------
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="%28s %10s %10s %10s \n"
format2="%28s %10s %9.0f%% %9.0f%% \n"
printf "${format1}" "Block" "Asserts" "Covered" "Proven"
echo "-----------------------------------------------------------------"

#-------------------------------------------------------------------------
# run fpv and summarize results
#-------------------------------------------------------------------------
\rm -Rf fpv_*.log

for block in "${blocks[@]}" ; do

  ./fpv $block -t ${tool} > /dev/null 2>&1
  cp fpv.log fpv_${block}.log

  # summarize results
  crash=`grep "ERROR" fpv.log`
  if [ $? -eq 0 ]; then
    printf "${format1}" $block "CRASH"
  else
    asserts=`grep "  assertions " fpv.log | cut -d":" -f2 | cut -d"(" -f1`
    covered=`grep "  - covered "  fpv.log | cut -d"(" -f2 | cut -d"%" -f1`
    proven=`grep  "  - proven "   fpv.log | cut -d"(" -f2 | cut -d"%" -f1`
    printf "${format2}" $block $asserts $covered $proven
  fi
done

#-------------------------------------------------------------------------
# print errors
#-------------------------------------------------------------------------
printf "\n\nLIST OF ERRORS AND UNPROVEN ASSERTIONS FOR EACH BLOCK:"
printf "\nNote: \"cex\" below indicates that JasperGold found a"
printf "\n\"counter example\", which could be caused by an RTL"
printf "\nbug or a missing assume property on an input."

for block in "${blocks[@]}" ; do
  printf "\n\n${block}\n"
  grep "ERROR" fpv_${block}.log

  # print uncovered and unproven assertions
  grep "^\[[1-9]" fpv_${block}.log | egrep -v " (proven|covered) "
done