hw/formal/fpv

#!/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 pinmux_fpv
#
# 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

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
fusesoc --cores-root ../.. run --setup "lowrisc:fpv:${FPV_TOP}"

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

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

jg -batch \
  ../../../fpv.tcl \
  -proj ../../../jgproject \
  -allow_unsupported_OS \
  -command exit \
  | tee ../../../fpv.log

cd -

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