#!/bin/bash

# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0

# Script to run fpv (formal property verification) using Jasper Gold
#
# Usage: To run fpv on module foo, type
#   fpv foo
#
# Here are some examples:
#   fpv rv_plic_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 -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
      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

echo "-------------------------------------------------------------------------"
echo "-- Generate file list using FuseSoC"
echo "-------------------------------------------------------------------------"
echo ""
echo "Top: $FPV_TOP"
echo ""

\rm -Rf build jgproject
# we just run the setup for the default target in order to generate the filelist
if [ "${CORE_PATH}" == "" ]; then
  if [[ $FPV_TOP == *"_fpv" ]]; then
    CORE_PATH="fpv:${FPV_TOP}"
  else
    CORE_PATH="ip:${FPV_TOP}"
  fi
fi
echo "core_file path: lowrisc:${CORE_PATH}"

fusesoc --cores-root ../.. run --tool=icarus --target=formal --setup "lowrisc:${CORE_PATH}"

echo "-------------------------------------------------------------------------"
echo "-- Run JasperGold"
echo "-------------------------------------------------------------------------"

cd build/*${FPV_TOP}*/formal-icarus

if [ "${gui}" == "1" ]; then
  jg ../../../fpv.tcl \
     -proj ../../../jgproject \
     -allow_unsupported_OS \
     | tee ../../../fpv.log
else
  jg -batch \
    ../../../fpv.tcl \
    -proj ../../../jgproject \
    -allow_unsupported_OS \
    -command exit \
    | tee ../../../fpv.log
fi

cd -

echo "-------------------------------------------------------------------------"
echo "-- Done"
echo "-------------------------------------------------------------------------"