source init-dat.tcl
set model "rejective"
pa_encode_process "inv1ab0-$model"
pa_encode_process "fork1abc0-$model"
pa_encode_process "and2abc00-$model"
pa_encode_process "or2abc00-$model"
pa_encode_process "nand2abc00-$model"
pa_encode_process "nor2abc00-$model"
pa_encode_process "c2abc00-$model"
pa_encode_process "me2abcd00-$model"
pa_encode_process "mez3abcde000-$model"
pa_encode_process "rsqb2abcd0001-$model"

set dir [pwd]; cd ../circuits; source init.tcl; cd $dir
ccs_read test-gates.ccs
pa_encode_process "INV"
pa_encode_process "FORK"
pa_encode_process "AND-00"
pa_encode_process "OR-00"
pa_encode_process "NAND-00"
pa_encode_process "NOR-00"
pa_encode_process "C-00"
pa_encode_process "ME-00"
pa_encode_process "MEZ-000"
pa_encode_process "RSQB-000"

outline "COMPARE NEW AND OLD MODELS OF BASIC GATES"

out "INV ([pa_state_number INV] st, [pa_transition_number INV] tr, [bdd_node_number D_INV] n); "
out "INV_MIN ([pa_state_number INV_MIN] st, [pa_transition_number INV_MIN] tr, [bdd_node_number D_INV_MIN] n); "
outline "inv1ab0-$model ([pa_state_number inv1ab0-$model] st, [pa_transition_number inv1ab0-$model] tr, [bdd_node_number D_inv1ab0-$model] n)"
versis_strong_equivalence 0 INV 0 INV_MIN
versis_strong_equivalence 0 INV 0 "inv1ab0-$model"

out "FORK ([pa_state_number FORK] st, [pa_transition_number FORK] tr, [bdd_node_number D_FORK] n); "
out "FORK_MIN ([pa_state_number FORK_MIN] st, [pa_transition_number FORK_MIN] tr, [bdd_node_number D_FORK_MIN] n); "
outline "inv1ab0-$model ([pa_state_number fork1abc0-$model] st, [pa_transition_number fork1abc0-$model] tr, [bdd_node_number D_fork1abc0-$model] n)"
versis_strong_equivalence 0 FORK 0 FORK_MIN
versis_strong_equivalence 0 FORK 0 "fork1abc0-$model"

out "AND-00 ([pa_state_number AND-00] st, [pa_transition_number AND-00] tr, [bdd_node_number D_AND-00] n); "
out "AND_MIN ([pa_state_number AND_MIN] st, [pa_transition_number AND_MIN] tr, [bdd_node_number D_AND_MIN] n); "
outline "and2abc00-$model ([pa_state_number and2abc00-$model] st, [pa_transition_number and2abc00-$model] tr, [bdd_node_number D_and2abc00-$model] n)"
versis_strong_equivalence 0 AND-00 0 AND_MIN
versis_strong_equivalence 0 AND-00 0 "and2abc00-$model"

out "OR-00 ([pa_state_number OR-00] st, [pa_transition_number OR-00] tr, [bdd_node_number D_OR-00] n); "
out "OR_MIN ([pa_state_number OR_MIN] st, [pa_transition_number OR_MIN] tr, [bdd_node_number D_OR_MIN] n); "
outline "or2abc00-$model ([pa_state_number or2abc00-$model] st, [pa_transition_number or2abc00-$model] tr, [bdd_node_number D_or2abc00-$model] n)"
versis_strong_equivalence 0 OR-00 0 OR_MIN
versis_strong_equivalence 0 OR-00 0 "or2abc00-$model"

out "NAND-00 ([pa_state_number NAND-00] st, [pa_transition_number NAND-00] tr, [bdd_node_number D_NAND-00] n); "
out "NAND_MIN ([pa_state_number NAND_MIN] st, [pa_transition_number NAND_MIN] tr, [bdd_node_number D_NAND_MIN] n); "
outline "nand2abc00-$model ([pa_state_number nand2abc00-$model] st, [pa_transition_number nand2abc00-$model] tr, [bdd_node_number D_nand2abc00-$model] n)"
versis_strong_equivalence 0 NAND-00 0 NAND_MIN
versis_strong_equivalence 0 NAND-00 0 "nand2abc00-$model"

out "NOR-00 ([pa_state_number NOR-00] st, [pa_transition_number NOR-00] tr, [bdd_node_number D_NOR-00] n); "
out "NOR_MIN ([pa_state_number NOR_MIN] st, [pa_transition_number NOR_MIN] tr, [bdd_node_number D_NOR_MIN] n); "
outline "nor2abc00-$model ([pa_state_number nor2abc00-$model] st, [pa_transition_number nor2abc00-$model] tr, [bdd_node_number D_nor2abc00-$model] n)"
versis_strong_equivalence 0 NOR-00 0 NOR_MIN
versis_strong_equivalence 0 NOR-00 0 "nor2abc00-$model"

out "C-00 ([pa_state_number C-00] st, [pa_transition_number C-00] tr, [bdd_node_number D_C-00] n); "
out "C_MIN ([pa_state_number C_MIN] st, [pa_transition_number C_MIN] tr, [bdd_node_number D_C_MIN] n); "
outline "c2abc00-$model ([pa_state_number c2abc00-$model] st, [pa_transition_number c2abc00-$model] tr, [bdd_node_number D_c2abc00-$model] n)"
versis_strong_equivalence 0 C-00 0 C_MIN
versis_strong_equivalence 0 C-00 0 "c2abc00-$model"

out "ME-00 ([pa_state_number ME-00] st, [pa_transition_number ME-00] tr, [bdd_node_number D_ME-00] n); "
out "ME_MIN ([pa_state_number ME_MIN] st, [pa_transition_number ME_MIN] tr, [bdd_node_number D_ME_MIN] n); "
outline "me2abcd00-$model ([pa_state_number me2abcd00-$model] st, [pa_transition_number me2abcd00-$model] tr, [bdd_node_number D_me2abcd00-$model] n)"
versis_strong_equivalence 0 ME-00 0 ME_MIN
versis_strong_equivalence 0 ME-00 0 "me2abcd00-$model"

out "MEZ-000 ([pa_state_number MEZ-000] st, [pa_transition_number MEZ-000] tr, [bdd_node_number D_MEZ-000] n); "
out "MEZ_MIN ([pa_state_number MEZ_MIN] st, [pa_transition_number MEZ_MIN] tr, [bdd_node_number D_MEZ_MIN] n); "
outline "mez3abcde000-$model ([pa_state_number mez3abcde000-$model] st, [pa_transition_number mez3abcde000-$model] tr, [bdd_node_number D_mez3abcde000-$model] n)"
versis_strong_equivalence 0 MEZ-000 0 MEZ_MIN
versis_strong_equivalence 0 MEZ-000 0 "mez3abcde000-$model"

out "RSQB-000 ([pa_state_number RSQB-000] st, [pa_transition_number RSQB-000] tr, [bdd_node_number D_RSQB-000] n); "
out "RSQB_MIN ([pa_state_number RSQB_MIN] st, [pa_transition_number RSQB_MIN] tr, [bdd_node_number D_RSQB_MIN] n); "
outline "rsqb2abcd0001-$model ([pa_state_number rsqb2abcd0001-$model] st, [pa_transition_number rsqb2abcd0001-$model] tr, [bdd_node_number D_rsqb2abcd0001-$model] n)"
versis_strong_equivalence 0 RSQB-000 0 RSQB_MIN
versis_strong_equivalence 0 RSQB-000 0 "rsqb2abcd0001-$model"
