# if you have tcl 8.6 you can use this:
# file tempfile tmpccs
set tmpccs "tmpccs.ccs"

# known model checker's settings
global mc_diagnostic
global mc_explain
global mc_tracepath
global mc_automaton
global mc_minimize
global mc_progress

# set parameters for model checking
set MCPAR [expr $mc_diagnostic]

set dir [pwd]; cd ../circuits; source init.tcl; cd $dir

ccs_convert_verilog c17.v $tmpccs
ccs_read $tmpccs
file delete $tmpccs

ccs_read c17-abstract.ccs
versis_strong_equivalence 0 c17 0 C17
versis_strong_equivalence 0 c17-G16 0 C17-G16-V1
versis_strong_equivalence 0 c17-G16 0 C17-G16-V2
versis_strong_equivalence 0 c17-G16 0 C17-G16-V3
versis_strong_equivalence 0 c17-G17 0 C17-G17-V1
versis_strong_equivalence 0 c17-G17 0 C17-G17-V2
versis_strong_equivalence 0 c17-G17 0 C17-G17-V3

outline ""

mc_read_actl_file "c17.actl"
mc_check_actl 0 C17 c17_F1 $MCPAR
mc_check_actl 0 C17-G16-V1 c17_F1 $MCPAR
mc_check_actl 0 C17-G16-V2 c17_F1 $MCPAR
mc_check_actl 0 C17-G16-V3 c17_F1 $MCPAR

mc_check_actl 0 C17 c17_F2 $MCPAR
mc_check_actl 0 C17-G17-V1 c17_F2 $MCPAR
mc_check_actl 0 C17-G17-V2 c17_F2 $MCPAR
mc_check_actl 0 C17-G17-V3 c17_F2 $MCPAR
