#!/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
# -t: choose which formal tool to use, default using jaspergold, also support
# vcf(VC Formal)
#
# Example:
#   fpv pinmux_fpv -p vip:pinmux_fpv -gui -cov -t jg
#
# Note that the module to be tested needs to have an _fpv testbench
# and a corresponding core file for this to work.

set -e

export DUT_TOP=$1
shift
gui=0
tool="jg"
flag="fileset_top"
export COV=0
export CHECK=0
export COMMON_MSG_TCL_PATH=$(readlink -f tools/jaspergold/jaspergold_common_message_process.tcl)

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"
      ;;
    "-t")
      shift
      tool=$1
      echo "running in tool: $tool"
      ;;
    "-flag")
      shift
      flag=$1
      echo "flag is set to: $flag"
      ;;
  esac
  shift
done

echo "-------------------------------------------------------------------------"
echo "-- Generate file list using FuseSoC"
echo "-------------------------------------------------------------------------"
echo ""
echo "Top: $DUT_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 [[ $DUT_TOP == *"_fpv" ]]; then
    CORE_PATH="fpv:${DUT_TOP}"
  else
    CORE_PATH="dv:${DUT_TOP}_sva"
  fi
fi
echo "core_file path: lowrisc:${CORE_PATH}"

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

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

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

if [ "${tool}" == "jg" ]; then
  if [ "${gui}" == "1" ]; then
    jg ../../../tools/jaspergold/fpv.tcl \
       -proj ../../../jgproject \
       -allow_unsupported_OS \
       | tee ../../../fpv.log
  else
    jg -batch \
      ../../../tools/jaspergold/fpv.tcl \
      -proj ../../../jgproject \
      -allow_unsupported_OS \
      -command exit \
      | tee ../../../fpv.log
  fi
elif [ "${tool}" == "vcf" ]; then
  vcf -f fpv_vcf.tcl
fi
cd -

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