Support for JasperGold for Formal Property Verification

[msfschaffner]

It would be great if we had support for JasperGold as well. This can also be in the form of a minimal backend that accepts a tcl file.

Let me know if you need assistance with this.

The opentitan repository has an example flow in place, see the fpv and fpv.tcl files here: https://github.com/lowRISC/opentitan/tree/master/hw/formal

[olofk]

I would love to see a JasperGold backend too. From your example it seems that it should be quite straight-forward to have a minimal implementation. I would love some help here though, especially since I don't have access to the tool itself

[msfschaffner]

Ok so I think we could build this backend by reusing the AscentLint flow that is already in place.

It would be great if we could invoke the tool in GUI mode as well, meaning that the invocation of the tool could look something like this (where GUI is a fusesoc tool parameter):

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            \ # <- could be absorbed into runfile, see below
    | tee fpv.log
fi

fpv.tcl is the runfile that has to be provided to the tool. below is a sample with some inline comments:

# clear previous settings
clear -all

# this one is debatable. we get several warnings in our flow due to the
# the coding style that we use if we do not disable these warnings. could be absorbed
# into a tool parameter in fusesoc that contains a list of waived messages.
# disables "parameter declared inside package XXX shall be treated as localparam".
set_message -disable VERI-2418

# only needed if coverage is measured, see below
check_cov -init -model {branch statement functional} \
-enable_prove_based_proof_core

#-------------------------------------------------------------------------
# read design sources
#-------------------------------------------------------------------------

# source file must also contain defines known to fusesoc
# in +define format, e.g. +define+FPV_ON
# sv09 could be absorbed into a tool parameter
analyze -sv09 -f sources.f

elaborate -top ${TOP_LEVEL_NAME}

#-------------------------------------------------------------------------
# specify clock(s) and reset(s) and additional constraints
#-------------------------------------------------------------------------

# source any additional TCL sources specified in fusesoc in the same way as 
# waiver or policy files are sourced in the ascentlint flow.
# these tcl files may include:
# nonstandard clock definitions
# additional constraints per block
# demotions (assertions -> assumptions)

# if no additional TCL source defined, use this default:
clock clk_i -both_edges
reset -expr {!rst_ni}

# these assumptions are always good to check as well,
# but we could absorb these in the user TCL files above for simplicity
check_assumptions -conflict
check_assumptions -live
check_assumptions -dead_end

#-------------------------------------------------------------------------
# configure proofgrid
#-------------------------------------------------------------------------

# could be made a tool parameter
# need to uncomment when using LSF:
# set_proofgrid_mode lsf

# this should be made a tool parameters in fusesoc, and just default 
# to some value that is reasonable machine/license wise (something in the range 1-4).
set_proofgrid_per_engine_max_local_jobs 16

#-------------------------------------------------------------------------
# prove all assertions and report
#-------------------------------------------------------------------------

# time limit could be made a tool parameter, and default to 60m or
# something like that
get_reset_info -x_value -with_reset_pin
prove -all -time_limit 120m
report -all     \
       -summary \
       -file fpv.rpt

#-------------------------------------------------------------------------
# check coverage and report
#-------------------------------------------------------------------------

# this needs to take place after proving the assertions
# since this can use a considerable amount of time, I would make this optional
# by adding another tool parameter which is called check_cov
check_cov -measure
check_cov -report -type all -no_return -report_file cover.html \
    -html -force -exclude { reset waived }

# only add this in batch mode
exit

success can be tested by grepping fpv.log and fpv.rpt for errors and certain proof status messages. the following grep commands should not return anything if the run was successful:

grep 'ERROR' fpv.log

grep 'RESULTS' -A 100000000 fpv.rpt | \
grep 'cex\|ar_cex\|undetermined\|unreachable\|unknown\|error\|ERROR'

Let me know if you need more info or whether I should test something.