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

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

ccs_read dme-martin.ccs
ccs_read dme-smv.ccs

ccs_convert_verilog dme-martin.v $tmpccs
ccs_read $tmpccs
file delete $tmpccs

ccs_convert_verilog dme-smv.v $tmpccs
ccs_read $tmpccs
file delete $tmpccs

versis_trace_equivalence 0 DME-MARTIN-FALSE 0 DME-MARTIN
versis_testing_equivalence 0 DME-MARTIN-FALSE 0 DME-MARTIN
versis_strong_equivalence 0 DME-MARTIN-FALSE 0 DME-MARTIN
versis_trace_equivalence 0 DME-SMV-FALSE 0 DME-SMV
versis_testing_equivalence 0 DME-SMV-FALSE 0 DME-SMV
versis_strong_equivalence 0 DME-SMV-FALSE 0 DME-SMV

versis_trace_equivalence 0 DME-MARTIN-TRUE 0 DME-MARTIN
versis_testing_equivalence 0 DME-MARTIN-TRUE 0 DME-MARTIN
versis_strong_equivalence 0 DME-MARTIN-TRUE 0 DME-MARTIN
versis_trace_equivalence 0 DME-SMV-TRUE 0 DME-SMV
versis_testing_equivalence 0 DME-SMV-TRUE 0 DME-SMV
versis_strong_equivalence 0 DME-SMV-TRUE 0 DME-SMV
