hw/formal/fpv_all

#!/bin/bash

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

#-------------------------------------------------------------------------
# list all blocks
#-------------------------------------------------------------------------
declare -a blocks=(
  "gpio"
  "rv_core_ibex"
  "rv_dm"
  "rv_plic"
  "spi_device"
  "rv_timer"
  "uart"
  "hmac"
  "flash_ctrl"
  "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"
  "top_earlgrey"
)

#-------------------------------------------------------------------------
# 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="%18s %10s %10s %10s \n"
format2="%18s %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 > /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