# Copyright lowRISC contributors.
# Copyright 2024 University of Oxford, see also CREDITS.md.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# The underlying commands and reports of this script are copyrighted by Cadence.
# We thank Cadence for granting permission to share our research to help
# promote and foster the next generation of innovators.
# Original author: Louis-Emile Ploix
# SPDX-License-Identifier: Apache-2.0

clear -all

set_prove_cache_path jgproofs
set_prove_cache on
set_prove_cache_mode coi

set_prove_per_property_time_limit 10s

# Load all Ibex RTL, using the filelist generated by fusesoc
analyze -sv12 +define+SYNTHESIS -f_relative_to_file_location build/fusesoc/lowrisc_ibex_ibex_formal_0.1/default-vcs/lowrisc_ibex_ibex_formal_0.1.scr

set sail_lib_dir $env(LOWRISC_SAIL_SRC)/lib/sv
analyze -sv12 -incdir $sail_lib_dir build/ibexspec.sv
analyze -sv12 spec/stub.sv

analyze -sv12 spec/spec_api.sv

# analyze -sv12 bound/binder.sv
# analyze -sv12 bound/if.sv
analyze -sv12 check/peek/alt_lsu.sv

analyze -sv12 check/top.sv

elaborate -top top -disable_auto_bbox
clock clk_i
reset ~rst_ni

set_proofgrid_max_local_jobs 10
set_proofgrid_per_engine_max_local_jobs 8

# AMcustom1
custom_engine -add -code hT3N1rhP11/52HrFRS21ROp2LOjVTgPvT8L8BGXHgLhaIuqtT4nARFjUqrBL+7pLmaTOzBepZW/Jm8SSrHDybSQtoNiO3y43wk+dEoWlsZizu97Fih6O6lPVG/LpWP5SsUPwlGagLNa1FKEFvwVXyX7//8prySbvSxIHXr5er+z4RAEA

# AMcustom2
custom_engine -add -code hT3Ng7hP/feYQOTDZ3qhYOwGAM51eA+J/FjkM5shLioAsqhgLR4Ft+O1BuKG6ilQ83B9tLXSmmqwm7g9AQA

# Ncustom3
custom_engine -add -code hT3OXrhPByJp3TrFSTLhUmMH4KVtJgmTCnNDF46yMXOKY48m4LS5nE7yBzFjA7kDuwO/GhGUpEPiky3p3wmPn3dJZHxFMsafSoObRzSC+tn7sEY0WbTdZ/FV4hL3MYH/b1CIUvXSWR4wqEoVLsmMOD4xIPT4lI1LO6ZCO7PnnWQuLwetnvKlrXx6wCW/A+x+enqslg1YPobi4wEF/EvbzOvcTYdJvl2s4H2yZg2b2ofAVN5WvhWk1HoBAA

# ADcustom4
custom_engine -add -code hT3Nv7hPv1752HrFRa2kROx2f/ECJeZB2AZsLdlO8VwmIuqtT4nIDFXclhg+O+o+DMmQCekbheGk0kK28laA9gaOFDXsQp29J3X615HY1IPHJWd6FUFvCHjO+p1k652b5JJvZlShNpGlGSXAiQe/mEAj6tEBAA

# Ncustom5
custom_engine -add -code hT3Ng7hPPfiYQOTDZ3qhYOwGAM51eA+J/FjkM5shLioAsqhgLR4Ft+O1BuKG6ilQ83B9tLXSl+CwjiTMAQA

# Mpcustom6
custom_engine -add -code hT3NZbhP9fmY2AbBQnsjfOxn6c+6e6yL+/e8fZFmaQrnlgEA

# prove -bg -all -covers

proc disable_mtypes {} {
	assert -disable {Step10::top.MType_*_Data}
}

proc prove_hps {task regex} {
	set props [get_property_list -task $task -include "disabled 0 type assert name $regex" -exclude "status proven"]
	set len [llength $props]
	for {set i 0} {$i <[llength $props]} {incr i 10} {
		for {set j 0} {$j < 10 && ($i + $j) < $len} {incr j} {
			set idx [expr {$i + $j}]
			prove -bg -property [lindex $props $idx] -engine_mode Hp
		}
		prove -wait
	}
}

# TODO: Add liveness checking
proc prove_no_liveness {} {
	disable_mtypes

	prove -task Step0
	prove -bg -task Step1
	prove -bg -task Step2
	prove -wait
	prove -bg -task Step3
	prove -bg -task Step4
	prove -wait
	prove -bg -property {Step5::*SpecStable*} -engine_mode Hp
	prove -bg -property {Step5::top.Ibex_FetchErrRoot} -engine_mode Hp
	prove -bg -property {Step5::top.Ibex_PreNextPcMatch}
	prove -wait
	prove -bg -task Step5
	prove -bg -task Step6
	prove -bg -task Step7
	prove -wait
	prove_hps Step8 *MemSpec*
	prove_hps Step8 *CapFsm*
	prove -property {Step8::*.Mem_*}
	prove -task Step8
	prove -property {Step9::*.BType_* Step9::*.JType_*}
	prove -property {Step9::*.Mem_*}
	prove -property {Step9::top.MType_Div*_Addr Step9::top.MType_Div*_CSR Step9::top.MType_Div*_PC Step9::top.MType_Rem*_Addr Step9::top.MType_Rem*_CSR Step9::top.MType_Rem*_PC}
	prove_hps Step9 *
	prove -property {Step10::*.BType_* Step10::*.JType_* Step10::*.Mem_*}
	prove_hps Step10 *
	prove -task Step11
	prove -task Step12
	prove_hps Step13 *BType*
	prove -task Step13
	prove_hps Step14 *JType*
	prove -task Step14
	prove -bg -task Step15
	prove -bg -task Step16
	prove -bg -task Step17
	prove -wait
	prove_hps Step18 *
	prove -task Step19
	prove_hps Step20 *
	prove -bg -task Step21
	prove -bg -task Step22
	prove -wait
}

source build/psgen.tcl
