Index: vis_dev/vis-2.3/Makefile.in =================================================================== --- vis_dev/vis-2.3/Makefile.in (revision 27) +++ vis_dev/vis-2.3/Makefile.in (revision 28) @@ -96,5 +96,5 @@ ALL_PKGS = abs amc baig bmc cmd ctlp ctlsp eqv fsm rob grab hrc imc img io ltl \ maig mark mc mvf mvfaig ntk ntm ntmaig ord part puresat rst res restr \ - rt sat sim spfd synth tbl truesim tst var vm + rt sat sim spfd synth tbl truesim tst debug var vm # Generate the list of all packages NOT in the PKGS list Index: vis_dev/vis-2.3/models/arbiter/3_faulty.mv =================================================================== --- vis_dev/vis-2.3/models/arbiter/3_faulty.mv (revision 28) +++ vis_dev/vis-2.3/models/arbiter/3_faulty.mv (revision 28) @@ -0,0 +1,989 @@ +# vl2mv 3_faulty.v +# version: 2.1 +# date: 10:35:53 11/22/2010 (CET) +.model concret +# I/O ports +.outputs p +.outputs q +.inputs i +.inputs j +# p = 1 +.names p$raw_n0 +1 +# q = 1 +.names q$raw_n1 +1 +# state = 0 +.names state$raw_n2<0> +0 +.names state$raw_n2<1> +0 +.names state$raw_n2<2> +0 +.names state$raw_n2<3> +0 +# non-blocking assignments for initial +.names _n5<0> +0 +.names _n5<1> +0 +.names _n5<2> +0 +.names _n5<3> +0 +.names state<0> _n5<0> _n6<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n5<1> _n6<1> +.def 0 +0 1 1 +1 0 1 +.names state<2> _n5<2> _n6<2> +.def 0 +0 1 1 +1 0 1 +.names state<3> _n5<3> _n6<3> +.def 0 +0 1 1 +1 0 1 +.names _n6<0> _n6<1> _n6<2> _n6<3> _n7 +.def 1 +0 0 0 0 0 +.names _n7 _n4 +0 1 +1 0 +.names _n4 _n3 +.def 1 +0 0 +.names _n9 +1 +# j == 1 +.names j _n9 _na +.def 0 +0 1 1 +1 0 1 +.names _na _n8 +0 1 +1 0 +.names _n8 _nc +- =_n8 +# state = 3 +.names state$_n8_nd$true<0> +1 +.names state$_n8_nd$true<1> +1 +.names state$_n8_nd$true<2> +0 +.names state$_n8_nd$true<3> +0 +# p = 0 +.names p$_n8_ne$true +0 +# q = 1 +.names q$_n8_nf$true +1 +.names _n11 +1 +# i == 1 +.names i _n11 _n12 +.def 0 +0 1 1 +1 0 1 +.names _n12 _n10 +0 1 +1 0 +.names _n10 _n14 +- =_n10 +# state = 5 +.names state$_n10_n15$true<0> +1 +.names state$_n10_n15$true<1> +0 +.names state$_n10_n15$true<2> +1 +.names state$_n10_n15$true<3> +0 +# p = 1 +.names p$_n10_n16$true +1 +# q = 0 +.names q$_n10_n17$true +0 +# state = 1 +.names state$_n10_n18$false<0> +1 +.names state$_n10_n18$false<1> +0 +.names state$_n10_n18$false<2> +0 +.names state$_n10_n18$false<3> +0 +# p = 1 +.names p$_n10_n19$false +1 +# q = 1 +.names q$_n10_n1a$false +1 +# if/else (i == 1) +.names _n10 p$_n10_n16$true p$_n10_n19$false p$_n10$raw_n1e +.def 0 +1 1 - 1 +0 - 1 1 +.names _n10 q$_n10_n17$true q$_n10_n1a$false q$_n10$raw_n20 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n10 state$_n10_n15$true<0> state$_n10_n18$false<0> state$_n10$raw_n22<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n10 state$_n10_n15$true<1> state$_n10_n18$false<1> state$_n10$raw_n22<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n10 state$_n10_n15$true<2> state$_n10_n18$false<2> state$_n10$raw_n22<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n10 state$_n10_n15$true<3> state$_n10_n18$false<3> state$_n10$raw_n22<3> +.def 0 +1 1 - 1 +0 - 1 1 +# if/else (j == 1) +.names _n8 p$_n8_ne$true p$_n10$raw_n1e p$_n8$raw_n30 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n8 q$_n8_nf$true q$_n10$raw_n20 q$_n8$raw_n32 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n8 state$_n8_nd$true<0> state$_n10$raw_n22<0> state$_n8$raw_n34<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n8 state$_n8_nd$true<1> state$_n10$raw_n22<1> state$_n8$raw_n34<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n8 state$_n8_nd$true<2> state$_n10$raw_n22<2> state$_n8$raw_n34<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n8 state$_n8_nd$true<3> state$_n10$raw_n22<3> state$_n8$raw_n34<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n41<0> +1 +.names _n41<1> +0 +.names _n41<2> +0 +.names _n41<3> +0 +.names state<0> _n41<0> _n42<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n41<1> _n42<1> +.def 0 +0 1 1 +1 0 1 +.names state<2> _n41<2> _n42<2> +.def 0 +0 1 1 +1 0 1 +.names state<3> _n41<3> _n42<3> +.def 0 +0 1 1 +1 0 1 +.names _n42<0> _n42<1> _n42<2> _n42<3> _n43 +.def 1 +0 0 0 0 0 +.names _n43 _n40 +0 1 +1 0 +.names _n40 _n3f +.def 1 +0 0 +# state = 2 +.names state$_n3f_n44$true<0> +0 +.names state$_n3f_n44$true<1> +1 +.names state$_n3f_n44$true<2> +0 +.names state$_n3f_n44$true<3> +0 +# p = 1 +.names p$_n3f_n45$true +1 +# q = 0 +.names q$_n3f_n46$true +0 +.names _n49<0> +0 +.names _n49<1> +1 +.names _n49<2> +0 +.names _n49<3> +0 +.names state<0> _n49<0> _n4a<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n49<1> _n4a<1> +.def 0 +0 1 1 +1 0 1 +.names state<2> _n49<2> _n4a<2> +.def 0 +0 1 1 +1 0 1 +.names state<3> _n49<3> _n4a<3> +.def 0 +0 1 1 +1 0 1 +.names _n4a<0> _n4a<1> _n4a<2> _n4a<3> _n4b +.def 1 +0 0 0 0 0 +.names _n4b _n48 +0 1 +1 0 +.names _n48 _n47 +.def 1 +0 0 +# state = 8 +.names state$_n47_n4c$true<0> +0 +.names state$_n47_n4c$true<1> +0 +.names state$_n47_n4c$true<2> +0 +.names state$_n47_n4c$true<3> +1 +# p = 1 +.names p$_n47_n4d$true +1 +# q = 1 +.names q$_n47_n4e$true +1 +.names _n51<0> +1 +.names _n51<1> +1 +.names _n51<2> +0 +.names _n51<3> +0 +.names state<0> _n51<0> _n52<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n51<1> _n52<1> +.def 0 +0 1 1 +1 0 1 +.names state<2> _n51<2> _n52<2> +.def 0 +0 1 1 +1 0 1 +.names state<3> _n51<3> _n52<3> +.def 0 +0 1 1 +1 0 1 +.names _n52<0> _n52<1> _n52<2> _n52<3> _n53 +.def 1 +0 0 0 0 0 +.names _n53 _n50 +0 1 +1 0 +.names _n50 _n4f +.def 1 +0 0 +# state = 4 +.names state$_n4f_n54$true<0> +0 +.names state$_n4f_n54$true<1> +0 +.names state$_n4f_n54$true<2> +1 +.names state$_n4f_n54$true<3> +0 +# p = 1 +.names p$_n4f_n55$true +1 +# q = 0 +.names q$_n4f_n56$true +0 +.names _n59<0> +0 +.names _n59<1> +0 +.names _n59<2> +1 +.names _n59<3> +0 +.names state<0> _n59<0> _n5a<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n59<1> _n5a<1> +.def 0 +0 1 1 +1 0 1 +.names state<2> _n59<2> _n5a<2> +.def 0 +0 1 1 +1 0 1 +.names state<3> _n59<3> _n5a<3> +.def 0 +0 1 1 +1 0 1 +.names _n5a<0> _n5a<1> _n5a<2> _n5a<3> _n5b +.def 1 +0 0 0 0 0 +.names _n5b _n58 +0 1 +1 0 +.names _n58 _n57 +.def 1 +0 0 +# state = 4 +.names state$_n57_n5c$true<0> +0 +.names state$_n57_n5c$true<1> +0 +.names state$_n57_n5c$true<2> +1 +.names state$_n57_n5c$true<3> +0 +# p = 1 +.names p$_n57_n5d$true +1 +# q = 0 +.names q$_n57_n5e$true +0 +.names _n61<0> +1 +.names _n61<1> +0 +.names _n61<2> +1 +.names _n61<3> +0 +.names state<0> _n61<0> _n62<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n61<1> _n62<1> +.def 0 +0 1 1 +1 0 1 +.names state<2> _n61<2> _n62<2> +.def 0 +0 1 1 +1 0 1 +.names state<3> _n61<3> _n62<3> +.def 0 +0 1 1 +1 0 1 +.names _n62<0> _n62<1> _n62<2> _n62<3> _n63 +.def 1 +0 0 0 0 0 +.names _n63 _n60 +0 1 +1 0 +.names _n60 _n5f +.def 1 +0 0 +.names _n65 +0 +# j == 0 +.names j _n65 _n66 +.def 0 +0 1 1 +1 0 1 +.names _n66 _n64 +0 1 +1 0 +.names _n64 _n68 +- =_n64 +# state = 6 +.names state$_n64_n69$true<0> +0 +.names state$_n64_n69$true<1> +1 +.names state$_n64_n69$true<2> +1 +.names state$_n64_n69$true<3> +0 +# p = 1 +.names p$_n64_n6a$true +1 +# q = 1 +.names q$_n64_n6b$true +1 +# state = 2 +.names state$_n64_n6c$false<0> +0 +.names state$_n64_n6c$false<1> +1 +.names state$_n64_n6c$false<2> +0 +.names state$_n64_n6c$false<3> +0 +# p = 1 +.names p$_n64_n6d$false +1 +# q = 0 +.names q$_n64_n6e$false +0 +# if/else (j == 0) +.names _n64 p$_n64_n6a$true p$_n64_n6d$false p$_n64$raw_n72 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n64 q$_n64_n6b$true q$_n64_n6e$false q$_n64$raw_n74 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n64 state$_n64_n69$true<0> state$_n64_n6c$false<0> state$_n64$raw_n76<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n64 state$_n64_n69$true<1> state$_n64_n6c$false<1> state$_n64$raw_n76<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n64 state$_n64_n69$true<2> state$_n64_n6c$false<2> state$_n64$raw_n76<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n64 state$_n64_n69$true<3> state$_n64_n6c$false<3> state$_n64$raw_n76<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n83<0> +0 +.names _n83<1> +1 +.names _n83<2> +1 +.names _n83<3> +0 +.names state<0> _n83<0> _n84<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n83<1> _n84<1> +.def 0 +0 1 1 +1 0 1 +.names state<2> _n83<2> _n84<2> +.def 0 +0 1 1 +1 0 1 +.names state<3> _n83<3> _n84<3> +.def 0 +0 1 1 +1 0 1 +.names _n84<0> _n84<1> _n84<2> _n84<3> _n85 +.def 1 +0 0 0 0 0 +.names _n85 _n82 +0 1 +1 0 +.names _n82 _n81 +.def 1 +0 0 +# state = 7 +.names state$_n81_n86$true<0> +1 +.names state$_n81_n86$true<1> +1 +.names state$_n81_n86$true<2> +1 +.names state$_n81_n86$true<3> +0 +# p = 0 +.names p$_n81_n87$true +0 +# q = 1 +.names q$_n81_n88$true +1 +.names _n8b<0> +1 +.names _n8b<1> +1 +.names _n8b<2> +1 +.names _n8b<3> +0 +.names state<0> _n8b<0> _n8c<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n8b<1> _n8c<1> +.def 0 +0 1 1 +1 0 1 +.names state<2> _n8b<2> _n8c<2> +.def 0 +0 1 1 +1 0 1 +.names state<3> _n8b<3> _n8c<3> +.def 0 +0 1 1 +1 0 1 +.names _n8c<0> _n8c<1> _n8c<2> _n8c<3> _n8d +.def 1 +0 0 0 0 0 +.names _n8d _n8a +0 1 +1 0 +.names _n8a _n89 +.def 1 +0 0 +# state = 8 +.names state$_n89_n8e$true<0> +0 +.names state$_n89_n8e$true<1> +0 +.names state$_n89_n8e$true<2> +0 +.names state$_n89_n8e$true<3> +1 +# p = 1 +.names p$_n89_n8f$true +1 +# q = 1 +.names q$_n89_n90$true +1 +.names _n93<0> +0 +.names _n93<1> +0 +.names _n93<2> +0 +.names _n93<3> +1 +.names state<0> _n93<0> _n94<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n93<1> _n94<1> +.def 0 +0 1 1 +1 0 1 +.names state<2> _n93<2> _n94<2> +.def 0 +0 1 1 +1 0 1 +.names state<3> _n93<3> _n94<3> +.def 0 +0 1 1 +1 0 1 +.names _n94<0> _n94<1> _n94<2> _n94<3> _n95 +.def 1 +0 0 0 0 0 +.names _n95 _n92 +0 1 +1 0 +.names _n92 _n91 +.def 1 +0 0 +# state = 9 +.names state$_n91_n96$true<0> +1 +.names state$_n91_n96$true<1> +0 +.names state$_n91_n96$true<2> +0 +.names state$_n91_n96$true<3> +1 +# p = 0 +.names p$_n91_n97$true +0 +# q = 0 +.names q$_n91_n98$true +0 +.names _n9b<0> +1 +.names _n9b<1> +0 +.names _n9b<2> +0 +.names _n9b<3> +1 +.names state<0> _n9b<0> _n9c<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n9b<1> _n9c<1> +.def 0 +0 1 1 +1 0 1 +.names state<2> _n9b<2> _n9c<2> +.def 0 +0 1 1 +1 0 1 +.names state<3> _n9b<3> _n9c<3> +.def 0 +0 1 1 +1 0 1 +.names _n9c<0> _n9c<1> _n9c<2> _n9c<3> _n9d +.def 1 +0 0 0 0 0 +.names _n9d _n9a +0 1 +1 0 +.names _n9a _n99 +.def 1 +0 0 +# state = 9 +.names state$_n99_n9e$true<0> +1 +.names state$_n99_n9e$true<1> +0 +.names state$_n99_n9e$true<2> +0 +.names state$_n99_n9e$true<3> +1 +# p = 0 +.names p$_n99_n9f$true +0 +# q = 0 +.names q$_n99_na0$true +0 +# case (state ) +.names _n99 p$_n99_n9f$true p p$_n99$raw_na7 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n99 q$_n99_na0$true q q$_n99$raw_na9 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n99 state$_n99_n9e$true<0> state<0> state$_n99$raw_nab<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n99 state$_n99_n9e$true<1> state<1> state$_n99$raw_nab<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n99 state$_n99_n9e$true<2> state<2> state$_n99$raw_nab<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n99 state$_n99_n9e$true<3> state<3> state$_n99$raw_nab<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n91 p$_n91_n97$true p$_n99$raw_na7 p$_n91$raw_nb0 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n91 q$_n91_n98$true q$_n99$raw_na9 q$_n91$raw_nb2 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n91 state$_n91_n96$true<0> state$_n99$raw_nab<0> state$_n91$raw_nb4<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n91 state$_n91_n96$true<1> state$_n99$raw_nab<1> state$_n91$raw_nb4<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n91 state$_n91_n96$true<2> state$_n99$raw_nab<2> state$_n91$raw_nb4<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n91 state$_n91_n96$true<3> state$_n99$raw_nab<3> state$_n91$raw_nb4<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n89 p$_n89_n8f$true p$_n91$raw_nb0 p$_n89$raw_nc2 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n89 q$_n89_n90$true q$_n91$raw_nb2 q$_n89$raw_nc4 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n89 state$_n89_n8e$true<0> state$_n91$raw_nb4<0> state$_n89$raw_nc6<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n89 state$_n89_n8e$true<1> state$_n91$raw_nb4<1> state$_n89$raw_nc6<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n89 state$_n89_n8e$true<2> state$_n91$raw_nb4<2> state$_n89$raw_nc6<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n89 state$_n89_n8e$true<3> state$_n91$raw_nb4<3> state$_n89$raw_nc6<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n81 p$_n81_n87$true p$_n89$raw_nc2 p$_n81$raw_nd4 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n81 q$_n81_n88$true q$_n89$raw_nc4 q$_n81$raw_nd6 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n81 state$_n81_n86$true<0> state$_n89$raw_nc6<0> state$_n81$raw_nd8<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n81 state$_n81_n86$true<1> state$_n89$raw_nc6<1> state$_n81$raw_nd8<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n81 state$_n81_n86$true<2> state$_n89$raw_nc6<2> state$_n81$raw_nd8<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n81 state$_n81_n86$true<3> state$_n89$raw_nc6<3> state$_n81$raw_nd8<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f p$_n64$raw_n72 p$_n81$raw_nd4 p$_n5f$raw_ne6 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f q$_n64$raw_n74 q$_n81$raw_nd6 q$_n5f$raw_ne8 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f state$_n64$raw_n76<0> state$_n81$raw_nd8<0> state$_n5f$raw_nea<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f state$_n64$raw_n76<1> state$_n81$raw_nd8<1> state$_n5f$raw_nea<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f state$_n64$raw_n76<2> state$_n81$raw_nd8<2> state$_n5f$raw_nea<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f state$_n64$raw_n76<3> state$_n81$raw_nd8<3> state$_n5f$raw_nea<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n57 p$_n57_n5d$true p$_n5f$raw_ne6 p$_n57$raw_nf8 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n57 q$_n57_n5e$true q$_n5f$raw_ne8 q$_n57$raw_nfa +.def 0 +1 1 - 1 +0 - 1 1 +.names _n57 state$_n57_n5c$true<0> state$_n5f$raw_nea<0> state$_n57$raw_nfc<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n57 state$_n57_n5c$true<1> state$_n5f$raw_nea<1> state$_n57$raw_nfc<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n57 state$_n57_n5c$true<2> state$_n5f$raw_nea<2> state$_n57$raw_nfc<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n57 state$_n57_n5c$true<3> state$_n5f$raw_nea<3> state$_n57$raw_nfc<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4f p$_n4f_n55$true p$_n57$raw_nf8 p$_n4f$raw_n10a +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4f q$_n4f_n56$true q$_n57$raw_nfa q$_n4f$raw_n10c +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4f state$_n4f_n54$true<0> state$_n57$raw_nfc<0> state$_n4f$raw_n10e<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4f state$_n4f_n54$true<1> state$_n57$raw_nfc<1> state$_n4f$raw_n10e<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4f state$_n4f_n54$true<2> state$_n57$raw_nfc<2> state$_n4f$raw_n10e<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4f state$_n4f_n54$true<3> state$_n57$raw_nfc<3> state$_n4f$raw_n10e<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n47 p$_n47_n4d$true p$_n4f$raw_n10a p$_n47$raw_n11c +.def 0 +1 1 - 1 +0 - 1 1 +.names _n47 q$_n47_n4e$true q$_n4f$raw_n10c q$_n47$raw_n11e +.def 0 +1 1 - 1 +0 - 1 1 +.names _n47 state$_n47_n4c$true<0> state$_n4f$raw_n10e<0> state$_n47$raw_n120<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n47 state$_n47_n4c$true<1> state$_n4f$raw_n10e<1> state$_n47$raw_n120<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n47 state$_n47_n4c$true<2> state$_n4f$raw_n10e<2> state$_n47$raw_n120<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n47 state$_n47_n4c$true<3> state$_n4f$raw_n10e<3> state$_n47$raw_n120<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3f p$_n3f_n45$true p$_n47$raw_n11c p$_n3f$raw_n12e +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3f q$_n3f_n46$true q$_n47$raw_n11e q$_n3f$raw_n130 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3f state$_n3f_n44$true<0> state$_n47$raw_n120<0> state$_n3f$raw_n132<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3f state$_n3f_n44$true<1> state$_n47$raw_n120<1> state$_n3f$raw_n132<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3f state$_n3f_n44$true<2> state$_n47$raw_n120<2> state$_n3f$raw_n132<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3f state$_n3f_n44$true<3> state$_n47$raw_n120<3> state$_n3f$raw_n132<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3 p$_n8$raw_n30 p$_n3f$raw_n12e p$_n3$raw_n140 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3 q$_n8$raw_n32 q$_n3f$raw_n130 q$_n3$raw_n142 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3 state$_n8$raw_n34<0> state$_n3f$raw_n132<0> state$_n3$raw_n144<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3 state$_n8$raw_n34<1> state$_n3f$raw_n132<1> state$_n3$raw_n144<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3 state$_n8$raw_n34<2> state$_n3f$raw_n132<2> state$_n3$raw_n144<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3 state$_n8$raw_n34<3> state$_n3f$raw_n132<3> state$_n3$raw_n144<3> +.def 0 +1 1 - 1 +0 - 1 1 +# conflict arbitrators +.names _n3 _nc _n14 _n3f _n47 _n4f _n57 _n5f _n68 _n81 _n89 _n91 _n99 _n152 +.def 0 + 1 1 - - - - - - - - - - - 1 + 1 0 1 - - - - - - - - - - 1 + 1 0 0 - - - - - - - - - - 1 + 0 - - 1 - - - - - - - - - 1 + 0 - - 0 1 - - - - - - - - 1 + 0 - - 0 0 1 - - - - - - - 1 + 0 - - 0 0 0 1 - - - - - - 1 + 0 - - 0 0 0 0 1 1 - - - - 1 + 0 - - 0 0 0 0 1 0 - - - - 1 + 0 - - 0 0 0 0 0 - 1 - - - 1 + 0 - - 0 0 0 0 0 - 0 1 - - 1 + 0 - - 0 0 0 0 0 - 0 0 1 - 1 + 0 - - 0 0 0 0 0 - 0 0 0 1 1 +.names _n152 p$_n3$raw_n140 p _n153 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.names _n3 _nc _n14 _n3f _n47 _n4f _n57 _n5f _n68 _n81 _n89 _n91 _n99 _n154 +.def 0 + 1 1 - - - - - - - - - - - 1 + 1 0 1 - - - - - - - - - - 1 + 1 0 0 - - - - - - - - - - 1 + 0 - - 1 - - - - - - - - - 1 + 0 - - 0 1 - - - - - - - - 1 + 0 - - 0 0 1 - - - - - - - 1 + 0 - - 0 0 0 1 - - - - - - 1 + 0 - - 0 0 0 0 1 1 - - - - 1 + 0 - - 0 0 0 0 1 0 - - - - 1 + 0 - - 0 0 0 0 0 - 1 - - - 1 + 0 - - 0 0 0 0 0 - 0 1 - - 1 + 0 - - 0 0 0 0 0 - 0 0 1 - 1 + 0 - - 0 0 0 0 0 - 0 0 0 1 1 +.names _n154 q$_n3$raw_n142 q _n155 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.names _n3 _nc _n14 _n3f _n47 _n4f _n57 _n5f _n68 _n81 _n89 _n91 _n99 _n156 +.def 0 + 1 1 - - - - - - - - - - - 1 + 1 0 1 - - - - - - - - - - 1 + 1 0 0 - - - - - - - - - - 1 + 0 - - 1 - - - - - - - - - 1 + 0 - - 0 1 - - - - - - - - 1 + 0 - - 0 0 1 - - - - - - - 1 + 0 - - 0 0 0 1 - - - - - - 1 + 0 - - 0 0 0 0 1 1 - - - - 1 + 0 - - 0 0 0 0 1 0 - - - - 1 + 0 - - 0 0 0 0 0 - 1 - - - 1 + 0 - - 0 0 0 0 0 - 0 1 - - 1 + 0 - - 0 0 0 0 0 - 0 0 1 - 1 + 0 - - 0 0 0 0 0 - 0 0 0 1 1 +.names _n156 state$_n3$raw_n144<0> state$_n3$raw_n144<1> state$_n3$raw_n144<2> state$_n3$raw_n144<3> state<0> state<1> state<2> state<3> -> _n157<0> _n157<1> _n157<2> _n157<3> +1 - - - - - - - - =state$_n3$raw_n144<0> =state$_n3$raw_n144<1> =state$_n3$raw_n144<2> =state$_n3$raw_n144<3> +0 - - - - - - - - =state<0> =state<1> =state<2> =state<3> +# non-blocking assignments +# latches +.r p$raw_n0 p +0 0 +1 1 +.latch _n153 p +.r q$raw_n1 q +0 0 +1 1 +.latch _n155 q +.r state$raw_n2<0> state<0> +.def 0 +1 1 +.r state$raw_n2<1> state<1> +.def 0 +1 1 +.r state$raw_n2<2> state<2> +.def 0 +1 1 +.r state$raw_n2<3> state<3> +.def 0 +1 1 +.latch _n157<0> state<0> +.latch _n157<1> state<1> +.latch _n157<2> state<2> +.latch _n157<3> state<3> +# quasi-continuous assignment +.end Index: vis_dev/vis-2.3/models/arbiter/arbiter.mv =================================================================== --- vis_dev/vis-2.3/models/arbiter/arbiter.mv (revision 28) +++ vis_dev/vis-2.3/models/arbiter/arbiter.mv (revision 28) @@ -0,0 +1,504 @@ +# vl2mv arbiter.v +# version: 2.1 +# date: 10:46:52 03/10/2011 (CET) +.model main +# I/O ports +.outputs ackA +.outputs ackB +.outputs ackC +.mv sel 4 A B C X +# assign active = pass_tokenA || pass_tokenB || pass_tokenC +# pass_tokenA || pass_tokenB +.names pass_tokenA pass_tokenB _n1 +.def 1 +0 0 0 +# pass_tokenA || pass_tokenB || pass_tokenC +.names _n1 pass_tokenC _n2 +.def 1 +0 0 0 +.names _n2 active$raw_n0 +- =_n2 +.mv _n3 4 A B C X +.names _n3 +A +.subckt controller controllerA req=reqA ack=ackA sel=sel pass_token=pass_tokenA id=_n3 +.mv _n4 4 A B C X +.names _n4 +B +.subckt controller controllerB req=reqB ack=ackB sel=sel pass_token=pass_tokenB id=_n4 +.mv _n5 4 A B C X +.names _n5 +C +.subckt controller controllerC req=reqC ack=ackC sel=sel pass_token=pass_tokenC id=_n5 +.subckt arbiter arbiter sel=sel active=active +.subckt client clientA req=reqA ack=ackA +.subckt client clientB req=reqB ack=ackB +.subckt client clientC req=reqC ack=ackC +# conflict arbitrators +.names active$raw_n0 active +0 0 +1 1 +# non-blocking assignments +# latches +# quasi-continuous assignment +.end +.model controller +# I/O ports +.inputs sel +.inputs req +.outputs pass_token +.outputs ack +.inputs id +.mv sel 4 A B C X +.mv state 3 IDLE READY BUSY +.mv id 4 A B C X +# state = 0 +.mv state$raw_n6 3 IDLE READY BUSY +.names state$raw_n6 +IDLE +# non-blocking assignments for initial +# ack = 0 +.names ack$raw_n7 +0 +# non-blocking assignments for initial +# pass_token = 1 +.names pass_token$raw_n8 +1 +# non-blocking assignments for initial +# assign is_selected = (sel == id ) +# sel == id +.names sel id _na +.def 0 +- =sel 1 +.names _na is_selected$raw_n9 +- =_na +.mv _nd 3 IDLE READY BUSY +.names _nd +IDLE +.names state _nd _nc +.def 0 +- =state 1 +.names _nc _nb +.def 1 +0 0 +.names is_selected _ne +- =is_selected +.names req _nf +- =req +# state = 1 +.mv state$req_n10$true 3 IDLE READY BUSY +.names state$req_n10$true +READY +# pass_token = 0 +.names pass_token$req_n11$true +0 +# pass_token = 1 +.names pass_token$req_n12$false +1 +# if/else (req ) +.names req pass_token$req_n11$true pass_token$req_n12$false pass_token$req$raw_n15 +.def 0 +1 1 - 1 +0 - 1 1 +.mv state$req$raw_n19 3 IDLE READY BUSY +.names req state$req_n10$true state state$req$raw_n19 +0 - - =state +1 - - =state$req_n10$true +# pass_token = 0 +.names pass_token$is_selected_n1b$false +0 +# if/else (is_selected ) +.names is_selected pass_token$req$raw_n15 pass_token$is_selected_n1b$false pass_token$is_selected$raw_n1f +.def 0 +1 1 - 1 +0 - 1 1 +.mv state$is_selected$raw_n21 3 IDLE READY BUSY +.names is_selected state$req$raw_n19 state state$is_selected$raw_n21 +0 - - =state +1 - - =state$req$raw_n19 +.mv _n26 3 IDLE READY BUSY +.names _n26 +READY +.names state _n26 _n25 +.def 0 +- =state 1 +.names _n25 _n24 +.def 1 +0 0 +# state = 2 +.mv state$_n24_n27$true 3 IDLE READY BUSY +.names state$_n24_n27$true +BUSY +# ack = 1 +.names ack$_n24_n28$true +1 +.mv _n2b 3 IDLE READY BUSY +.names _n2b +BUSY +.names state _n2b _n2a +.def 0 +- =state 1 +.names _n2a _n29 +.def 1 +0 0 +.names req _n2c +0 1 +1 0 +.names _n2c _n2d +- =_n2c +# state = 0 +.mv state$_n2c_n2e$true 3 IDLE READY BUSY +.names state$_n2c_n2e$true +IDLE +# ack = 0 +.names ack$_n2c_n2f$true +0 +# pass_token = 1 +.names pass_token$_n2c_n30$true +1 +# if/else (!req ) +.names _n2c pass_token$_n2c_n30$true pass_token pass_token$_n2c$raw_n37 +.def 0 +1 1 - 1 +0 - 1 1 +.mv state$_n2c$raw_n39 3 IDLE READY BUSY +.names _n2c state$_n2c_n2e$true state state$_n2c$raw_n39 +0 - - =state +1 - - =state$_n2c_n2e$true +.names _n2c ack$_n2c_n2f$true ack ack$_n2c$raw_n3a +.def 0 +1 1 - 1 +0 - 1 1 +# case (state ) +.mv state$_n29$raw_n42 3 IDLE READY BUSY +.names _n29 state$_n2c$raw_n39 state state$_n29$raw_n42 +0 - - =state +1 - - =state$_n2c$raw_n39 +.names _n29 pass_token$_n2c$raw_n37 pass_token pass_token$_n29$raw_n43 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n29 ack$_n2c$raw_n3a ack ack$_n29$raw_n45 +.def 0 +1 1 - 1 +0 - 1 1 +.mv state$_n24$raw_n47 3 IDLE READY BUSY +.names _n24 state$_n24_n27$true state$_n29$raw_n42 state$_n24$raw_n47 +0 - - =state$_n29$raw_n42 +1 - - =state$_n24_n27$true +.names _n24 ack$_n24_n28$true ack$_n29$raw_n45 ack$_n24$raw_n48 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n24 pass_token pass_token$_n29$raw_n43 pass_token$_n24$raw_n4f +.def 0 +1 1 - 1 +0 - 1 1 +.mv state$_nb$raw_n52 3 IDLE READY BUSY +.names _nb state$is_selected$raw_n21 state$_n24$raw_n47 state$_nb$raw_n52 +0 - - =state$_n24$raw_n47 +1 - - =state$is_selected$raw_n21 +.names _nb pass_token$is_selected$raw_n1f pass_token$_n24$raw_n4f pass_token$_nb$raw_n53 +.def 0 +1 1 - 1 +0 - 1 1 +.names _nb ack ack$_n24$raw_n48 ack$_nb$raw_n5b +.def 0 +1 1 - 1 +0 - 1 1 +# conflict arbitrators +.names is_selected$raw_n9 is_selected +0 0 +1 1 +.names _nb _ne _nf _n24 _n29 _n2d _n5d +.def 0 + 1 1 1 - - - 1 + 0 - - 1 - - 1 + 0 - - 0 1 1 1 +.mv _n5e 3 IDLE READY BUSY +.names _n5d state$_nb$raw_n52 state _n5e +1 - - =state$_nb$raw_n52 +0 - - =state +.names _nb _ne _nf _n24 _n29 _n2d _n62 +.def 0 + 1 1 1 - - - 1 + 1 1 0 - - - 1 + 1 0 - - - - 1 + 0 - - 0 1 1 1 +.names _n62 pass_token$_nb$raw_n53 pass_token _n63 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.names _nb _n24 _n29 _n2d _n64 +.def 0 + 0 1 - - 1 + 0 0 1 1 1 +.names _n64 ack$_nb$raw_n5b ack _n65 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +# non-blocking assignments +# latches +.r pass_token$raw_n8 pass_token +0 0 +1 1 +.latch _n63 pass_token +.r state$raw_n6 state +- =state$raw_n6 +.latch _n5e state +.r ack$raw_n7 ack +0 0 +1 1 +.latch _n65 ack +# quasi-continuous assignment +.end +.model arbiter +# I/O ports +.outputs sel +.inputs active +.mv sel 4 A B C X +.mv state 4 A B C X +# state = 0 +.mv state$raw_n66 4 A B C X +.names state$raw_n66 +A +# non-blocking assignments for initial +# assign sel = active ? state : 3 +.mv sel$raw_n67 4 A B C X +.mv _n68 4 A B C X +.names _n68 +X +# active ? state : 3 +.mv _n69 4 A B C X +.names active state _n68 _n69 +0 - - =_n68 +1 - - =state +.names _n69 sel$raw_n67 +- =_n69 +.names active _n6a +- =active +.mv _n6d 4 A B C X +.names _n6d +A +.names state _n6d _n6c +.def 0 +- =state 1 +.names _n6c _n6b +.def 1 +0 0 +# state = 1 +.mv state$_n6b_n6e$true 4 A B C X +.names state$_n6b_n6e$true +B +.mv _n71 4 A B C X +.names _n71 +B +.names state _n71 _n70 +.def 0 +- =state 1 +.names _n70 _n6f +.def 1 +0 0 +# state = 2 +.mv state$_n6f_n72$true 4 A B C X +.names state$_n6f_n72$true +C +.mv _n75 4 A B C X +.names _n75 +C +.names state _n75 _n74 +.def 0 +- =state 1 +.names _n74 _n73 +.def 1 +0 0 +# state = 0 +.mv state$_n73_n76$true 4 A B C X +.names state$_n73_n76$true +A +# case (state ) +.mv state$_n73$raw_n79 4 A B C X +.names _n73 state$_n73_n76$true state state$_n73$raw_n79 +0 - - =state +1 - - =state$_n73_n76$true +.mv state$_n6f$raw_n7a 4 A B C X +.names _n6f state$_n6f_n72$true state$_n73$raw_n79 state$_n6f$raw_n7a +0 - - =state$_n73$raw_n79 +1 - - =state$_n6f_n72$true +.mv state$_n6b$raw_n7e 4 A B C X +.names _n6b state$_n6b_n6e$true state$_n6f$raw_n7a state$_n6b$raw_n7e +0 - - =state$_n6f$raw_n7a +1 - - =state$_n6b_n6e$true +# if/else (active ) +.mv state$active$raw_n84 4 A B C X +.names active state$_n6b$raw_n7e state state$active$raw_n84 +0 - - =state +1 - - =state$_n6b$raw_n7e +# conflict arbitrators +.names sel$raw_n67 sel +- =sel$raw_n67 +.names _n6a _n6b _n6f _n73 _n85 +.def 0 + 1 1 - - 1 + 1 0 1 - 1 + 1 0 0 1 1 +.mv _n86 4 A B C X +.names _n85 state$active$raw_n84 state _n86 +1 - - =state$active$raw_n84 +0 - - =state +# non-blocking assignments +# latches +.r state$raw_n66 state +- =state$raw_n66 +.latch _n86 state +# quasi-continuous assignment +.end +.model client +# I/O ports +.outputs req +.inputs ack +.mv state 3 NO_REQ REQ HAVE_TOKEN +# req = 0 +.names req$raw_n89 +0 +# non-blocking assignments for initial +# state = 0 +.mv state$raw_n8a 3 NO_REQ REQ HAVE_TOKEN +.names state$raw_n8a +NO_REQ +# non-blocking assignments for initial +# assign rand_choice = $ND ( 0,1 ) +.names rand_choice +0 +1 +.mv _n8f 3 NO_REQ REQ HAVE_TOKEN +.names _n8f +NO_REQ +.names state _n8f _n8e +.def 0 +- =state 1 +.names _n8e _n8d +.def 1 +0 0 +.names rand_choice _n90 +- =rand_choice +# req = 1 +.names req$rand_choice_n91$true +1 +# state = 1 +.mv state$rand_choice_n92$true 3 NO_REQ REQ HAVE_TOKEN +.names state$rand_choice_n92$true +REQ +# if/else (rand_choice ) +.names rand_choice req$rand_choice_n91$true req req$rand_choice$raw_n97 +.def 0 +1 1 - 1 +0 - 1 1 +.mv state$rand_choice$raw_n99 3 NO_REQ REQ HAVE_TOKEN +.names rand_choice state$rand_choice_n92$true state state$rand_choice$raw_n99 +0 - - =state +1 - - =state$rand_choice_n92$true +.mv _n9c 3 NO_REQ REQ HAVE_TOKEN +.names _n9c +REQ +.names state _n9c _n9b +.def 0 +- =state 1 +.names _n9b _n9a +.def 1 +0 0 +.names ack _n9d +- =ack +# state = 2 +.mv state$ack_n9e$true 3 NO_REQ REQ HAVE_TOKEN +.names state$ack_n9e$true +HAVE_TOKEN +# if/else (ack ) +.mv state$ack$raw_na1 3 NO_REQ REQ HAVE_TOKEN +.names ack state$ack_n9e$true state state$ack$raw_na1 +0 - - =state +1 - - =state$ack_n9e$true +.mv _na4 3 NO_REQ REQ HAVE_TOKEN +.names _na4 +HAVE_TOKEN +.names state _na4 _na3 +.def 0 +- =state 1 +.names _na3 _na2 +.def 1 +0 0 +.names rand_choice _na5 +- =rand_choice +# req = 0 +.names req$rand_choice_na6$true +0 +# state = 0 +.mv state$rand_choice_na7$true 3 NO_REQ REQ HAVE_TOKEN +.names state$rand_choice_na7$true +NO_REQ +# if/else (rand_choice ) +.names rand_choice req$rand_choice_na6$true req req$rand_choice$raw_nac +.def 0 +1 1 - 1 +0 - 1 1 +.mv state$rand_choice$raw_nae 3 NO_REQ REQ HAVE_TOKEN +.names rand_choice state$rand_choice_na7$true state state$rand_choice$raw_nae +0 - - =state +1 - - =state$rand_choice_na7$true +# case (state ) +.names _na2 req$rand_choice$raw_nac req req$_na2$raw_nb3 +.def 0 +1 1 - 1 +0 - 1 1 +.mv state$_na2$raw_nb5 3 NO_REQ REQ HAVE_TOKEN +.names _na2 state$rand_choice$raw_nae state state$_na2$raw_nb5 +0 - - =state +1 - - =state$rand_choice$raw_nae +.mv state$_n9a$raw_nb6 3 NO_REQ REQ HAVE_TOKEN +.names _n9a state$ack$raw_na1 state$_na2$raw_nb5 state$_n9a$raw_nb6 +0 - - =state$_na2$raw_nb5 +1 - - =state$ack$raw_na1 +.names _n9a req req$_na2$raw_nb3 req$_n9a$raw_nb9 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n8d req$rand_choice$raw_n97 req$_n9a$raw_nb9 req$_n8d$raw_nbc +.def 0 +1 1 - 1 +0 - 1 1 +.mv state$_n8d$raw_nbe 3 NO_REQ REQ HAVE_TOKEN +.names _n8d state$rand_choice$raw_n99 state$_n9a$raw_nb6 state$_n8d$raw_nbe +0 - - =state$_n9a$raw_nb6 +1 - - =state$rand_choice$raw_n99 +# conflict arbitrators +.names _n8d _n90 _n9a _na2 _na5 _nc5 +.def 0 + 1 1 - - - 1 + 0 - 0 1 1 1 +.names _nc5 req$_n8d$raw_nbc req _nc6 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.names _n8d _n90 _n9a _n9d _na2 _na5 _nc7 +.def 0 + 1 1 - - - - 1 + 0 - 1 1 - - 1 + 0 - 0 - 1 1 1 +.mv _nc8 3 NO_REQ REQ HAVE_TOKEN +.names _nc7 state$_n8d$raw_nbe state _nc8 +1 - - =state$_n8d$raw_nbe +0 - - =state +# non-blocking assignments +# latches +.r req$raw_n89 req +0 0 +1 1 +.latch _nc6 req +.r state$raw_n8a state +- =state$raw_n8a +.latch _nc8 state +# quasi-continuous assignment +.end Index: vis_dev/vis-2.3/models/arbiter/arbiter.script =================================================================== --- vis_dev/vis-2.3/models/arbiter/arbiter.script (revision 28) +++ vis_dev/vis-2.3/models/arbiter/arbiter.script (revision 28) @@ -0,0 +1,3 @@ +rlmv models/arbiter/arbiter.mv +init +set_init -v 1 -m usut Index: vis_dev/vis-2.3/models/arbiter/arbiter.v =================================================================== --- vis_dev/vis-2.3/models/arbiter/arbiter.v (revision 28) +++ vis_dev/vis-2.3/models/arbiter/arbiter.v (revision 28) @@ -0,0 +1,126 @@ +typedef enum {A, B, C, X} selection; +typedef enum {IDLE, READY, BUSY} controller_state; +typedef enum {NO_REQ, REQ, HAVE_TOKEN} client_state; + +module main(clk); +input clk; +output ackA, ackB, ackC; + +selection wire sel; +wire active; + +assign active = pass_tokenA || pass_tokenB || pass_tokenC; + +controller controllerA(clk, reqA, ackA, sel, pass_tokenA, A); +controller controllerB(clk, reqB, ackB, sel, pass_tokenB, B); +controller controllerC(clk, reqC, ackC, sel, pass_tokenC, C); +arbiter arbiter(clk, sel, active); + +client clientA(clk, reqA, ackA); +client clientB(clk, reqB, ackB); +client clientC(clk, reqC, ackC); + +endmodule + +module controller(clk, req, ack, sel, pass_token, id); +input clk, req, sel, id; +output ack, pass_token; + +selection wire sel, id; +reg ack, pass_token; +controller_state reg state; + +initial state = IDLE; +initial ack = 0; +initial pass_token = 1; + +wire is_selected; +assign is_selected = (sel == id); + +always @(posedge clk) begin + case(state) + IDLE: + if (is_selected) + if (req) + begin + state = READY; + pass_token = 0; /* dropping off this line causes a safety bug */ + end + else + pass_token = 1; + else + pass_token = 0; + READY: + begin + state = BUSY; + ack = 1; + end + BUSY: + if (!req) + begin + state = IDLE; + ack = 0; + pass_token = 1; + end + endcase +end +endmodule + +module arbiter(clk, sel, active); +input clk, active; +output sel; + +selection wire sel; +selection reg state; + +initial state = A; + +assign sel = active ? state: X; + +always @(posedge clk) begin + if (active) + case(state) + A: + state = B; + B: + state = C; + C: + state = A; + endcase +end +endmodule + +module client(clk, req, ack); +input clk, ack; +output req; + +reg req; +client_state reg state; + +wire rand_choice; + +initial req = 0; +initial state = NO_REQ; + +assign rand_choice = $ND(0,1); + +always @(posedge clk) begin + case(state) + NO_REQ: + if (rand_choice) + begin + req = 1; + state = REQ; + end + REQ: + if (ack) + state = HAVE_TOKEN; + HAVE_TOKEN: + if (rand_choice) + begin + req = 0; + state = NO_REQ; + end + endcase +end +endmodule Index: vis_dev/vis-2.3/models/arbiter/check_gcd =================================================================== --- vis_dev/vis-2.3/models/arbiter/check_gcd (revision 28) +++ vis_dev/vis-2.3/models/arbiter/check_gcd (revision 28) @@ -0,0 +1,3 @@ +rlmv gcd.mv +init +Test_rob3 Index: vis_dev/vis-2.3/models/arbiter/gcd.mv =================================================================== --- vis_dev/vis-2.3/models/arbiter/gcd.mv (revision 28) +++ vis_dev/vis-2.3/models/arbiter/gcd.mv (revision 28) @@ -0,0 +1,2248 @@ +# vl2mv gcd.v +# version: 2.1 +# date: 10:52:04 03/10/2011 (CET) +.model gcd +# I/O ports +.outputs o<0> o<1> o<2> o<3> o<4> o<5> o<6> o<7> +.outputs busy +.inputs a<0> a<1> a<2> a<3> a<4> a<5> a<6> a<7> +.inputs start +.inputs b<0> b<1> b<2> b<3> b<4> b<5> b<6> b<7> +# assign xy_lsb [1] = select (x ,lsb ) +.subckt select _n2 select<0>=_n1<0> z<0>=x<0> z<1>=x<1> z<2>=x<2> z<3>=x<3> z<4>=x<4> z<5>=x<5> z<6>=x<6> z<7>=x<7> lsb<0>=lsb<0> lsb<1>=lsb<1> lsb<2>=lsb<2> +.names _n1<0> xy_lsb$raw_n0<1> +- =_n1<0> +# assign xy_lsb [0] = select (y ,lsb ) +.subckt select _n5 select<0>=_n4<0> z<0>=y<0> z<1>=y<1> z<2>=y<2> z<3>=y<3> z<4>=y<4> z<5>=y<5> z<6>=y<6> z<7>=y<7> lsb<0>=lsb<0> lsb<1>=lsb<1> lsb<2>=lsb<2> +.names _n4<0> xy_lsb$raw_n3<0> +- =_n4<0> +# assign diff = x < y ? y - x : x - y +# x < y +.names _n9 +0 +.names x<0> y<0> _n9 _n8<0> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names _nb +0 +.names x<0> y<0> _nb _na +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<1> y<1> _na _n8<1> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<1> y<1> _na _nc +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<2> y<2> _nc _n8<2> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<2> y<2> _nc _nd +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<3> y<3> _nd _n8<3> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<3> y<3> _nd _ne +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<4> y<4> _ne _n8<4> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<4> y<4> _ne _nf +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<5> y<5> _nf _n8<5> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<5> y<5> _nf _n10 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<6> y<6> _n10 _n8<6> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<6> y<6> _n10 _n11 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<7> y<7> _n11 _n8<7> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<7> y<7> _n11 _n12 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names _n8<0> _n8<1> _n8<2> _n8<3> _n8<4> _n8<5> _n8<6> _n8<7> _n13 +.def 1 +0 0 0 0 0 0 0 0 0 +.names _n12 _n13 _n7 +.def 0 +1 1 1 +# y - x +.names _n15 +0 +.names y<0> x<0> _n15 _n14<0> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names _n17 +0 +.names y<0> x<0> _n17 _n16 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names y<1> x<1> _n16 _n14<1> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names y<1> x<1> _n16 _n18 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names y<2> x<2> _n18 _n14<2> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names y<2> x<2> _n18 _n19 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names y<3> x<3> _n19 _n14<3> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names y<3> x<3> _n19 _n1a +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names y<4> x<4> _n1a _n14<4> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names y<4> x<4> _n1a _n1b +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names y<5> x<5> _n1b _n14<5> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names y<5> x<5> _n1b _n1c +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names y<6> x<6> _n1c _n14<6> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names y<6> x<6> _n1c _n1d +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names y<7> x<7> _n1d _n14<7> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# x - y +.names _n1f +0 +.names x<0> y<0> _n1f _n1e<0> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names _n21 +0 +.names x<0> y<0> _n21 _n20 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<1> y<1> _n20 _n1e<1> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<1> y<1> _n20 _n22 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<2> y<2> _n22 _n1e<2> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<2> y<2> _n22 _n23 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<3> y<3> _n23 _n1e<3> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<3> y<3> _n23 _n24 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<4> y<4> _n24 _n1e<4> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<4> y<4> _n24 _n25 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<5> y<5> _n25 _n1e<5> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<5> y<5> _n25 _n26 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<6> y<6> _n26 _n1e<6> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<6> y<6> _n26 _n27 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<7> y<7> _n27 _n1e<7> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# x < y ? y - x : x - y +.names _n7 _n14<0> _n1e<0> _n28<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n7 _n14<1> _n1e<1> _n28<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n7 _n14<2> _n1e<2> _n28<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n7 _n14<3> _n1e<3> _n28<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n7 _n14<4> _n1e<4> _n28<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n7 _n14<5> _n1e<5> _n28<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n7 _n14<6> _n1e<6> _n28<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n7 _n14<7> _n1e<7> _n28<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n28<0> diff$raw_n6<0> +- =_n28<0> +.names _n28<1> diff$raw_n6<1> +- =_n28<1> +.names _n28<2> diff$raw_n6<2> +- =_n28<2> +.names _n28<3> diff$raw_n6<3> +- =_n28<3> +.names _n28<4> diff$raw_n6<4> +- =_n28<4> +.names _n28<5> diff$raw_n6<5> +- =_n28<5> +.names _n28<6> diff$raw_n6<6> +- =_n28<6> +.names _n28<7> diff$raw_n6<7> +- =_n28<7> +# busy = 0 +.names busy$raw_n31 +0 +# x = 0 +.names x$raw_n32<0> +0 +.names x$raw_n32<1> +0 +.names x$raw_n32<2> +0 +.names x$raw_n32<3> +0 +.names x$raw_n32<4> +0 +.names x$raw_n32<5> +0 +.names x$raw_n32<6> +0 +.names x$raw_n32<7> +0 +# y = 0 +.names y$raw_n33<0> +0 +.names y$raw_n33<1> +0 +.names y$raw_n33<2> +0 +.names y$raw_n33<3> +0 +.names y$raw_n33<4> +0 +.names y$raw_n33<5> +0 +.names y$raw_n33<6> +0 +.names y$raw_n33<7> +0 +# o = 0 +.names o$raw_n34<0> +0 +.names o$raw_n34<1> +0 +.names o$raw_n34<2> +0 +.names o$raw_n34<3> +0 +.names o$raw_n34<4> +0 +.names o$raw_n34<5> +0 +.names o$raw_n34<6> +0 +.names o$raw_n34<7> +0 +# lsb = 0 +.names lsb$raw_n35<0> +0 +.names lsb$raw_n35<1> +0 +.names lsb$raw_n35<2> +0 +# non-blocking assignments for initial +# assign done = ((x == y ) | (x == 0) | (y == 0)) & busy +# x == y +.names x<0> y<0> _n38<0> +.def 0 +0 1 1 +1 0 1 +.names x<1> y<1> _n38<1> +.def 0 +0 1 1 +1 0 1 +.names x<2> y<2> _n38<2> +.def 0 +0 1 1 +1 0 1 +.names x<3> y<3> _n38<3> +.def 0 +0 1 1 +1 0 1 +.names x<4> y<4> _n38<4> +.def 0 +0 1 1 +1 0 1 +.names x<5> y<5> _n38<5> +.def 0 +0 1 1 +1 0 1 +.names x<6> y<6> _n38<6> +.def 0 +0 1 1 +1 0 1 +.names x<7> y<7> _n38<7> +.def 0 +0 1 1 +1 0 1 +.names _n38<0> _n38<1> _n38<2> _n38<3> _n38<4> _n38<5> _n38<6> _n38<7> _n39 +.def 1 +0 0 0 0 0 0 0 0 0 +.names _n39 _n37 +0 1 +1 0 +.names _n3b<0> +0 +.names _n3b<1> +0 +.names _n3b<2> +0 +.names _n3b<3> +0 +.names _n3b<4> +0 +.names _n3b<5> +0 +.names _n3b<6> +0 +.names _n3b<7> +0 +# x == 0 +.names x<0> _n3b<0> _n3c<0> +.def 0 +0 1 1 +1 0 1 +.names x<1> _n3b<1> _n3c<1> +.def 0 +0 1 1 +1 0 1 +.names x<2> _n3b<2> _n3c<2> +.def 0 +0 1 1 +1 0 1 +.names x<3> _n3b<3> _n3c<3> +.def 0 +0 1 1 +1 0 1 +.names x<4> _n3b<4> _n3c<4> +.def 0 +0 1 1 +1 0 1 +.names x<5> _n3b<5> _n3c<5> +.def 0 +0 1 1 +1 0 1 +.names x<6> _n3b<6> _n3c<6> +.def 0 +0 1 1 +1 0 1 +.names x<7> _n3b<7> _n3c<7> +.def 0 +0 1 1 +1 0 1 +.names _n3c<0> _n3c<1> _n3c<2> _n3c<3> _n3c<4> _n3c<5> _n3c<6> _n3c<7> _n3d +.def 1 +0 0 0 0 0 0 0 0 0 +.names _n3d _n3a +0 1 +1 0 +# (x == y ) | (x == 0) +.names _n37 _n3a _n3e +.def 1 +0 0 0 +.names _n40<0> +0 +.names _n40<1> +0 +.names _n40<2> +0 +.names _n40<3> +0 +.names _n40<4> +0 +.names _n40<5> +0 +.names _n40<6> +0 +.names _n40<7> +0 +# y == 0 +.names y<0> _n40<0> _n41<0> +.def 0 +0 1 1 +1 0 1 +.names y<1> _n40<1> _n41<1> +.def 0 +0 1 1 +1 0 1 +.names y<2> _n40<2> _n41<2> +.def 0 +0 1 1 +1 0 1 +.names y<3> _n40<3> _n41<3> +.def 0 +0 1 1 +1 0 1 +.names y<4> _n40<4> _n41<4> +.def 0 +0 1 1 +1 0 1 +.names y<5> _n40<5> _n41<5> +.def 0 +0 1 1 +1 0 1 +.names y<6> _n40<6> _n41<6> +.def 0 +0 1 1 +1 0 1 +.names y<7> _n40<7> _n41<7> +.def 0 +0 1 1 +1 0 1 +.names _n41<0> _n41<1> _n41<2> _n41<3> _n41<4> _n41<5> _n41<6> _n41<7> _n42 +.def 1 +0 0 0 0 0 0 0 0 0 +.names _n42 _n3f +0 1 +1 0 +# (x == y ) | (x == 0) | (y == 0) +.names _n3e _n3f _n43 +.def 1 +0 0 0 +# ((x == y ) | (x == 0) | (y == 0)) & busy +.names _n43 busy _n44 +.def 0 +1 1 1 +.names _n44 done$raw_n36 +- =_n44 +.names load _n45 +- =load +# x = a +.names a<0> x$load_n46$true<0> +- =a<0> +.names a<1> x$load_n46$true<1> +- =a<1> +.names a<2> x$load_n46$true<2> +- =a<2> +.names a<3> x$load_n46$true<3> +- =a<3> +.names a<4> x$load_n46$true<4> +- =a<4> +.names a<5> x$load_n46$true<5> +- =a<5> +.names a<6> x$load_n46$true<6> +- =a<6> +.names a<7> x$load_n46$true<7> +- =a<7> +# y = b +.names b<0> y$load_n47$true<0> +- =b<0> +.names b<1> y$load_n47$true<1> +- =b<1> +.names b<2> y$load_n47$true<2> +- =b<2> +.names b<3> y$load_n47$true<3> +- =b<3> +.names b<4> y$load_n47$true<4> +- =b<4> +.names b<5> y$load_n47$true<5> +- =b<5> +.names b<6> y$load_n47$true<6> +- =b<6> +.names b<7> y$load_n47$true<7> +- =b<7> +# lsb = 0 +.names lsb$load_n48$true<0> +0 +.names lsb$load_n48$true<1> +0 +.names lsb$load_n48$true<2> +0 +.names done _n49 +0 1 +1 0 +# busy & ~done +.names busy _n49 _n4a +.def 0 +1 1 1 +.names _n4a _n4b +- =_n4a +.names _n4e<0> +0 +.names _n4e<1> +0 +.names xy_lsb<0> _n4e<0> _n4f<0> +.def 0 +0 1 1 +1 0 1 +.names xy_lsb<1> _n4e<1> _n4f<1> +.def 0 +0 1 1 +1 0 1 +.names _n4f<0> _n4f<1> _n50 +.def 1 +0 0 0 +.names _n50 _n4d +0 1 +1 0 +.names _n4d _n4c +.def 1 +0 0 +# lsb = lsb + 1 +.names _n52<0> +1 +.names _n52<1> +0 +.names _n52<2> +0 +# lsb + 1 +.names _n54 +0 +.names lsb<0> _n52<0> _n54 _n53<0> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names _n56 +0 +.names lsb<0> _n52<0> _n56 _n55 +.def 0 +- 1 1 1 +1 - 1 1 +1 1 - 1 +.names lsb<1> _n52<1> _n55 _n53<1> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names lsb<1> _n52<1> _n55 _n57 +.def 0 +- 1 1 1 +1 - 1 1 +1 1 - 1 +.names lsb<2> _n52<2> _n57 _n53<2> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +.names _n53<0> lsb$_n4c_n51$true<0> +- =_n53<0> +.names _n53<1> lsb$_n4c_n51$true<1> +- =_n53<1> +.names _n53<2> lsb$_n4c_n51$true<2> +- =_n53<2> +.names _n5a<0> +1 +.names _n5a<1> +0 +.names xy_lsb<0> _n5a<0> _n5b<0> +.def 0 +0 1 1 +1 0 1 +.names xy_lsb<1> _n5a<1> _n5b<1> +.def 0 +0 1 1 +1 0 1 +.names _n5b<0> _n5b<1> _n5c +.def 1 +0 0 0 +.names _n5c _n59 +0 1 +1 0 +.names _n59 _n58 +.def 1 +0 0 +# x [8 - 2 : 0] = x [8 - 1 : 1] +.names x<1> x$_n58_n5d$true<0> +- =x<1> +.names x<2> x$_n58_n5d$true<1> +- =x<2> +.names x<3> x$_n58_n5d$true<2> +- =x<3> +.names x<4> x$_n58_n5d$true<3> +- =x<4> +.names x<5> x$_n58_n5d$true<4> +- =x<5> +.names x<6> x$_n58_n5d$true<5> +- =x<6> +.names x<7> x$_n58_n5d$true<6> +- =x<7> +.names x<7> x$_n58_n5d$true<7> +- =x<7> +# x [8 - 1] = 0 +.names x$_n58_n5e$true<7> +0 +.names x$_n58_n5d$true<0> x$_n58_n5e$true<0> +- =x$_n58_n5d$true<0> +.names x$_n58_n5d$true<1> x$_n58_n5e$true<1> +- =x$_n58_n5d$true<1> +.names x$_n58_n5d$true<2> x$_n58_n5e$true<2> +- =x$_n58_n5d$true<2> +.names x$_n58_n5d$true<3> x$_n58_n5e$true<3> +- =x$_n58_n5d$true<3> +.names x$_n58_n5d$true<4> x$_n58_n5e$true<4> +- =x$_n58_n5d$true<4> +.names x$_n58_n5d$true<5> x$_n58_n5e$true<5> +- =x$_n58_n5d$true<5> +.names x$_n58_n5d$true<6> x$_n58_n5e$true<6> +- =x$_n58_n5d$true<6> +.names _n61<0> +0 +.names _n61<1> +1 +.names xy_lsb<0> _n61<0> _n62<0> +.def 0 +0 1 1 +1 0 1 +.names xy_lsb<1> _n61<1> _n62<1> +.def 0 +0 1 1 +1 0 1 +.names _n62<0> _n62<1> _n63 +.def 1 +0 0 0 +.names _n63 _n60 +0 1 +1 0 +.names _n60 _n5f +.def 1 +0 0 +# y [8 - 2 : 0] = y [8 - 1 : 1] +.names y<1> y$_n5f_n64$true<0> +- =y<1> +.names y<2> y$_n5f_n64$true<1> +- =y<2> +.names y<3> y$_n5f_n64$true<2> +- =y<3> +.names y<4> y$_n5f_n64$true<3> +- =y<4> +.names y<5> y$_n5f_n64$true<4> +- =y<5> +.names y<6> y$_n5f_n64$true<5> +- =y<6> +.names y<7> y$_n5f_n64$true<6> +- =y<7> +.names y<7> y$_n5f_n64$true<7> +- =y<7> +# y [8 - 1] = 0 +.names y$_n5f_n65$true<7> +0 +.names y$_n5f_n64$true<0> y$_n5f_n65$true<0> +- =y$_n5f_n64$true<0> +.names y$_n5f_n64$true<1> y$_n5f_n65$true<1> +- =y$_n5f_n64$true<1> +.names y$_n5f_n64$true<2> y$_n5f_n65$true<2> +- =y$_n5f_n64$true<2> +.names y$_n5f_n64$true<3> y$_n5f_n65$true<3> +- =y$_n5f_n64$true<3> +.names y$_n5f_n64$true<4> y$_n5f_n65$true<4> +- =y$_n5f_n64$true<4> +.names y$_n5f_n64$true<5> y$_n5f_n65$true<5> +- =y$_n5f_n64$true<5> +.names y$_n5f_n64$true<6> y$_n5f_n65$true<6> +- =y$_n5f_n64$true<6> +.names _n68<0> +1 +.names _n68<1> +1 +.names xy_lsb<0> _n68<0> _n69<0> +.def 0 +0 1 1 +1 0 1 +.names xy_lsb<1> _n68<1> _n69<1> +.def 0 +0 1 1 +1 0 1 +.names _n69<0> _n69<1> _n6a +.def 1 +0 0 0 +.names _n6a _n67 +0 1 +1 0 +.names _n67 _n66 +.def 1 +0 0 +# x < y +.names _n6d +0 +.names x<0> y<0> _n6d _n6c<0> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names _n6f +0 +.names x<0> y<0> _n6f _n6e +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<1> y<1> _n6e _n6c<1> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<1> y<1> _n6e _n70 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<2> y<2> _n70 _n6c<2> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<2> y<2> _n70 _n71 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<3> y<3> _n71 _n6c<3> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<3> y<3> _n71 _n72 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<4> y<4> _n72 _n6c<4> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<4> y<4> _n72 _n73 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<5> y<5> _n73 _n6c<5> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<5> y<5> _n73 _n74 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<6> y<6> _n74 _n6c<6> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<6> y<6> _n74 _n75 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<7> y<7> _n75 _n6c<7> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<7> y<7> _n75 _n76 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names _n6c<0> _n6c<1> _n6c<2> _n6c<3> _n6c<4> _n6c<5> _n6c<6> _n6c<7> _n77 +.def 1 +0 0 0 0 0 0 0 0 0 +.names _n76 _n77 _n6b +.def 0 +1 1 1 +.names _n6b _n78 +- =_n6b +# y [8 - 2 : 0] = diff [8 - 1 : 1] +.names diff<1> y$_n6b_n79$true<0> +- =diff<1> +.names diff<2> y$_n6b_n79$true<1> +- =diff<2> +.names diff<3> y$_n6b_n79$true<2> +- =diff<3> +.names diff<4> y$_n6b_n79$true<3> +- =diff<4> +.names diff<5> y$_n6b_n79$true<4> +- =diff<5> +.names diff<6> y$_n6b_n79$true<5> +- =diff<6> +.names diff<7> y$_n6b_n79$true<6> +- =diff<7> +.names y<7> y$_n6b_n79$true<7> +- =y<7> +# y [8 - 1] = 0 +.names y$_n6b_n7a$true<7> +0 +.names y$_n6b_n79$true<0> y$_n6b_n7a$true<0> +- =y$_n6b_n79$true<0> +.names y$_n6b_n79$true<1> y$_n6b_n7a$true<1> +- =y$_n6b_n79$true<1> +.names y$_n6b_n79$true<2> y$_n6b_n7a$true<2> +- =y$_n6b_n79$true<2> +.names y$_n6b_n79$true<3> y$_n6b_n7a$true<3> +- =y$_n6b_n79$true<3> +.names y$_n6b_n79$true<4> y$_n6b_n7a$true<4> +- =y$_n6b_n79$true<4> +.names y$_n6b_n79$true<5> y$_n6b_n7a$true<5> +- =y$_n6b_n79$true<5> +.names y$_n6b_n79$true<6> y$_n6b_n7a$true<6> +- =y$_n6b_n79$true<6> +# x [8 - 2 : 0] = diff [8 - 1 : 1] +.names diff<1> x$_n6b_n7b$false<0> +- =diff<1> +.names diff<2> x$_n6b_n7b$false<1> +- =diff<2> +.names diff<3> x$_n6b_n7b$false<2> +- =diff<3> +.names diff<4> x$_n6b_n7b$false<3> +- =diff<4> +.names diff<5> x$_n6b_n7b$false<4> +- =diff<5> +.names diff<6> x$_n6b_n7b$false<5> +- =diff<6> +.names diff<7> x$_n6b_n7b$false<6> +- =diff<7> +.names x<7> x$_n6b_n7b$false<7> +- =x<7> +# x [8 - 1] = 0 +.names x$_n6b_n7c$false<7> +0 +.names x$_n6b_n7b$false<0> x$_n6b_n7c$false<0> +- =x$_n6b_n7b$false<0> +.names x$_n6b_n7b$false<1> x$_n6b_n7c$false<1> +- =x$_n6b_n7b$false<1> +.names x$_n6b_n7b$false<2> x$_n6b_n7c$false<2> +- =x$_n6b_n7b$false<2> +.names x$_n6b_n7b$false<3> x$_n6b_n7c$false<3> +- =x$_n6b_n7b$false<3> +.names x$_n6b_n7b$false<4> x$_n6b_n7c$false<4> +- =x$_n6b_n7b$false<4> +.names x$_n6b_n7b$false<5> x$_n6b_n7c$false<5> +- =x$_n6b_n7b$false<5> +.names x$_n6b_n7b$false<6> x$_n6b_n7c$false<6> +- =x$_n6b_n7b$false<6> +# if/else (x < y ) +.names _n6b y$_n6b_n7a$true<0> y<0> y$_n6b$raw_n7f<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b y$_n6b_n7a$true<1> y<1> y$_n6b$raw_n7f<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b y$_n6b_n7a$true<2> y<2> y$_n6b$raw_n7f<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b y$_n6b_n7a$true<3> y<3> y$_n6b$raw_n7f<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b y$_n6b_n7a$true<4> y<4> y$_n6b$raw_n7f<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b y$_n6b_n7a$true<5> y<5> y$_n6b$raw_n7f<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b y$_n6b_n7a$true<6> y<6> y$_n6b$raw_n7f<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b y$_n6b_n7a$true<7> y<7> y$_n6b$raw_n7f<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b x<0> x$_n6b_n7c$false<0> x$_n6b$raw_n88<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b x<1> x$_n6b_n7c$false<1> x$_n6b$raw_n88<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b x<2> x$_n6b_n7c$false<2> x$_n6b$raw_n88<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b x<3> x$_n6b_n7c$false<3> x$_n6b$raw_n88<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b x<4> x$_n6b_n7c$false<4> x$_n6b$raw_n88<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b x<5> x$_n6b_n7c$false<5> x$_n6b$raw_n88<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b x<6> x$_n6b_n7c$false<6> x$_n6b$raw_n88<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n6b x<7> x$_n6b_n7c$false<7> x$_n6b$raw_n88<7> +.def 0 +1 1 - 1 +0 - 1 1 +# case (xy_lsb ) +.names _n66 y$_n6b$raw_n7f<0> y<0> y$_n66$raw_n95<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 y$_n6b$raw_n7f<1> y<1> y$_n66$raw_n95<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 y$_n6b$raw_n7f<2> y<2> y$_n66$raw_n95<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 y$_n6b$raw_n7f<3> y<3> y$_n66$raw_n95<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 y$_n6b$raw_n7f<4> y<4> y$_n66$raw_n95<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 y$_n6b$raw_n7f<5> y<5> y$_n66$raw_n95<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 y$_n6b$raw_n7f<6> y<6> y$_n66$raw_n95<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 y$_n6b$raw_n7f<7> y<7> y$_n66$raw_n95<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 x$_n6b$raw_n88<0> x<0> x$_n66$raw_n9e<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 x$_n6b$raw_n88<1> x<1> x$_n66$raw_n9e<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 x$_n6b$raw_n88<2> x<2> x$_n66$raw_n9e<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 x$_n6b$raw_n88<3> x<3> x$_n66$raw_n9e<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 x$_n6b$raw_n88<4> x<4> x$_n66$raw_n9e<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 x$_n6b$raw_n88<5> x<5> x$_n66$raw_n9e<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 x$_n6b$raw_n88<6> x<6> x$_n66$raw_n9e<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n66 x$_n6b$raw_n88<7> x<7> x$_n66$raw_n9e<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f y$_n5f_n65$true<0> y$_n66$raw_n95<0> y$_n5f$raw_na7<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f y$_n5f_n65$true<1> y$_n66$raw_n95<1> y$_n5f$raw_na7<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f y$_n5f_n65$true<2> y$_n66$raw_n95<2> y$_n5f$raw_na7<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f y$_n5f_n65$true<3> y$_n66$raw_n95<3> y$_n5f$raw_na7<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f y$_n5f_n65$true<4> y$_n66$raw_n95<4> y$_n5f$raw_na7<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f y$_n5f_n65$true<5> y$_n66$raw_n95<5> y$_n5f$raw_na7<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f y$_n5f_n65$true<6> y$_n66$raw_n95<6> y$_n5f$raw_na7<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f y$_n5f_n65$true<7> y$_n66$raw_n95<7> y$_n5f$raw_na7<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f x<0> x$_n66$raw_n9e<0> x$_n5f$raw_nb3<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f x<1> x$_n66$raw_n9e<1> x$_n5f$raw_nb3<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f x<2> x$_n66$raw_n9e<2> x$_n5f$raw_nb3<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f x<3> x$_n66$raw_n9e<3> x$_n5f$raw_nb3<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f x<4> x$_n66$raw_n9e<4> x$_n5f$raw_nb3<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f x<5> x$_n66$raw_n9e<5> x$_n5f$raw_nb3<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f x<6> x$_n66$raw_n9e<6> x$_n5f$raw_nb3<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n5f x<7> x$_n66$raw_n9e<7> x$_n5f$raw_nb3<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 x$_n58_n5e$true<0> x$_n5f$raw_nb3<0> x$_n58$raw_nbc<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 x$_n58_n5e$true<1> x$_n5f$raw_nb3<1> x$_n58$raw_nbc<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 x$_n58_n5e$true<2> x$_n5f$raw_nb3<2> x$_n58$raw_nbc<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 x$_n58_n5e$true<3> x$_n5f$raw_nb3<3> x$_n58$raw_nbc<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 x$_n58_n5e$true<4> x$_n5f$raw_nb3<4> x$_n58$raw_nbc<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 x$_n58_n5e$true<5> x$_n5f$raw_nb3<5> x$_n58$raw_nbc<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 x$_n58_n5e$true<6> x$_n5f$raw_nb3<6> x$_n58$raw_nbc<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 x$_n58_n5e$true<7> x$_n5f$raw_nb3<7> x$_n58$raw_nbc<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 y<0> y$_n5f$raw_na7<0> y$_n58$raw_nc7<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 y<1> y$_n5f$raw_na7<1> y$_n58$raw_nc7<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 y<2> y$_n5f$raw_na7<2> y$_n58$raw_nc7<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 y<3> y$_n5f$raw_na7<3> y$_n58$raw_nc7<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 y<4> y$_n5f$raw_na7<4> y$_n58$raw_nc7<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 y<5> y$_n5f$raw_na7<5> y$_n58$raw_nc7<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 y<6> y$_n5f$raw_na7<6> y$_n58$raw_nc7<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n58 y<7> y$_n5f$raw_na7<7> y$_n58$raw_nc7<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c lsb$_n4c_n51$true<0> lsb<0> lsb$_n4c$raw_nd3<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c lsb$_n4c_n51$true<1> lsb<1> lsb$_n4c$raw_nd3<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c lsb$_n4c_n51$true<2> lsb<2> lsb$_n4c$raw_nd3<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c y<0> y$_n58$raw_nc7<0> y$_n4c$raw_nd7<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c y<1> y$_n58$raw_nc7<1> y$_n4c$raw_nd7<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c y<2> y$_n58$raw_nc7<2> y$_n4c$raw_nd7<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c y<3> y$_n58$raw_nc7<3> y$_n4c$raw_nd7<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c y<4> y$_n58$raw_nc7<4> y$_n4c$raw_nd7<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c y<5> y$_n58$raw_nc7<5> y$_n4c$raw_nd7<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c y<6> y$_n58$raw_nc7<6> y$_n4c$raw_nd7<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c y<7> y$_n58$raw_nc7<7> y$_n4c$raw_nd7<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c x<0> x$_n58$raw_nbc<0> x$_n4c$raw_ne0<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c x<1> x$_n58$raw_nbc<1> x$_n4c$raw_ne0<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c x<2> x$_n58$raw_nbc<2> x$_n4c$raw_ne0<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c x<3> x$_n58$raw_nbc<3> x$_n4c$raw_ne0<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c x<4> x$_n58$raw_nbc<4> x$_n4c$raw_ne0<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c x<5> x$_n58$raw_nbc<5> x$_n4c$raw_ne0<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c x<6> x$_n58$raw_nbc<6> x$_n4c$raw_ne0<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4c x<7> x$_n58$raw_nbc<7> x$_n4c$raw_ne0<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names done _ne9 +- =done +# o = (x < y ) ? x : y +# x < y +.names _ned +0 +.names x<0> y<0> _ned _nec<0> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names _nef +0 +.names x<0> y<0> _nef _nee +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<1> y<1> _nee _nec<1> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<1> y<1> _nee _nf0 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<2> y<2> _nf0 _nec<2> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<2> y<2> _nf0 _nf1 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<3> y<3> _nf1 _nec<3> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<3> y<3> _nf1 _nf2 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<4> y<4> _nf2 _nec<4> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<4> y<4> _nf2 _nf3 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<5> y<5> _nf3 _nec<5> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<5> y<5> _nf3 _nf4 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<6> y<6> _nf4 _nec<6> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<6> y<6> _nf4 _nf5 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names x<7> y<7> _nf5 _nec<7> +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names x<7> y<7> _nf5 _nf6 +.def 0 +0 - 1 1 +0 1 - 1 +- 1 1 1 +.names _nec<0> _nec<1> _nec<2> _nec<3> _nec<4> _nec<5> _nec<6> _nec<7> _nf7 +.def 1 +0 0 0 0 0 0 0 0 0 +.names _nf6 _nf7 _neb +.def 0 +1 1 1 +# (x < y ) ? x : y +.names _neb x<0> y<0> _nf8<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _neb x<1> y<1> _nf8<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _neb x<2> y<2> _nf8<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _neb x<3> y<3> _nf8<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _neb x<4> y<4> _nf8<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _neb x<5> y<5> _nf8<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _neb x<6> y<6> _nf8<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _neb x<7> y<7> _nf8<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names _nf8<0> o$done_nea$true<0> +- =_nf8<0> +.names _nf8<1> o$done_nea$true<1> +- =_nf8<1> +.names _nf8<2> o$done_nea$true<2> +- =_nf8<2> +.names _nf8<3> o$done_nea$true<3> +- =_nf8<3> +.names _nf8<4> o$done_nea$true<4> +- =_nf8<4> +.names _nf8<5> o$done_nea$true<5> +- =_nf8<5> +.names _nf8<6> o$done_nea$true<6> +- =_nf8<6> +.names _nf8<7> o$done_nea$true<7> +- =_nf8<7> +# if/else (done ) +.names done o$done_nea$true<0> o<0> o$done$raw_n103<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names done o$done_nea$true<1> o<1> o$done$raw_n103<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names done o$done_nea$true<2> o<2> o$done$raw_n103<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names done o$done_nea$true<3> o<3> o$done$raw_n103<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names done o$done_nea$true<4> o<4> o$done$raw_n103<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names done o$done_nea$true<5> o<5> o$done$raw_n103<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names done o$done_nea$true<6> o<6> o$done$raw_n103<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names done o$done_nea$true<7> o<7> o$done$raw_n103<7> +.def 0 +1 1 - 1 +0 - 1 1 +# if/else (busy & ~done ) +.names _n4a y$_n4c$raw_nd7<0> y<0> y$_n4a$raw_n112<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a y$_n4c$raw_nd7<1> y<1> y$_n4a$raw_n112<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a y$_n4c$raw_nd7<2> y<2> y$_n4a$raw_n112<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a y$_n4c$raw_nd7<3> y<3> y$_n4a$raw_n112<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a y$_n4c$raw_nd7<4> y<4> y$_n4a$raw_n112<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a y$_n4c$raw_nd7<5> y<5> y$_n4a$raw_n112<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a y$_n4c$raw_nd7<6> y<6> y$_n4a$raw_n112<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a y$_n4c$raw_nd7<7> y<7> y$_n4a$raw_n112<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a lsb$_n4c$raw_nd3<0> lsb<0> lsb$_n4a$raw_n11b<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a lsb$_n4c$raw_nd3<1> lsb<1> lsb$_n4a$raw_n11b<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a lsb$_n4c$raw_nd3<2> lsb<2> lsb$_n4a$raw_n11b<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a x$_n4c$raw_ne0<0> x<0> x$_n4a$raw_n11f<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a x$_n4c$raw_ne0<1> x<1> x$_n4a$raw_n11f<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a x$_n4c$raw_ne0<2> x<2> x$_n4a$raw_n11f<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a x$_n4c$raw_ne0<3> x<3> x$_n4a$raw_n11f<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a x$_n4c$raw_ne0<4> x<4> x$_n4a$raw_n11f<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a x$_n4c$raw_ne0<5> x<5> x$_n4a$raw_n11f<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a x$_n4c$raw_ne0<6> x<6> x$_n4a$raw_n11f<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a x$_n4c$raw_ne0<7> x<7> x$_n4a$raw_n11f<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a o<0> o$done$raw_n103<0> o$_n4a$raw_n128<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a o<1> o$done$raw_n103<1> o$_n4a$raw_n128<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a o<2> o$done$raw_n103<2> o$_n4a$raw_n128<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a o<3> o$done$raw_n103<3> o$_n4a$raw_n128<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a o<4> o$done$raw_n103<4> o$_n4a$raw_n128<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a o<5> o$done$raw_n103<5> o$_n4a$raw_n128<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a o<6> o$done$raw_n103<6> o$_n4a$raw_n128<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4a o<7> o$done$raw_n103<7> o$_n4a$raw_n128<7> +.def 0 +1 1 - 1 +0 - 1 1 +# if/else (load ) +.names load y$load_n47$true<0> y$_n4a$raw_n112<0> y$load$raw_n134<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names load y$load_n47$true<1> y$_n4a$raw_n112<1> y$load$raw_n134<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names load y$load_n47$true<2> y$_n4a$raw_n112<2> y$load$raw_n134<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names load y$load_n47$true<3> y$_n4a$raw_n112<3> y$load$raw_n134<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names load y$load_n47$true<4> y$_n4a$raw_n112<4> y$load$raw_n134<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names load y$load_n47$true<5> y$_n4a$raw_n112<5> y$load$raw_n134<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names load y$load_n47$true<6> y$_n4a$raw_n112<6> y$load$raw_n134<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names load y$load_n47$true<7> y$_n4a$raw_n112<7> y$load$raw_n134<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names load lsb$load_n48$true<0> lsb$_n4a$raw_n11b<0> lsb$load$raw_n13d<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names load lsb$load_n48$true<1> lsb$_n4a$raw_n11b<1> lsb$load$raw_n13d<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names load lsb$load_n48$true<2> lsb$_n4a$raw_n11b<2> lsb$load$raw_n13d<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names load x$load_n46$true<0> x$_n4a$raw_n11f<0> x$load$raw_n141<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names load x$load_n46$true<1> x$_n4a$raw_n11f<1> x$load$raw_n141<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names load x$load_n46$true<2> x$_n4a$raw_n11f<2> x$load$raw_n141<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names load x$load_n46$true<3> x$_n4a$raw_n11f<3> x$load$raw_n141<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names load x$load_n46$true<4> x$_n4a$raw_n11f<4> x$load$raw_n141<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names load x$load_n46$true<5> x$_n4a$raw_n11f<5> x$load$raw_n141<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names load x$load_n46$true<6> x$_n4a$raw_n11f<6> x$load$raw_n141<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names load x$load_n46$true<7> x$_n4a$raw_n11f<7> x$load$raw_n141<7> +.def 0 +1 1 - 1 +0 - 1 1 +.names load o<0> o$_n4a$raw_n128<0> o$load$raw_n14e<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names load o<1> o$_n4a$raw_n128<1> o$load$raw_n14e<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names load o<2> o$_n4a$raw_n128<2> o$load$raw_n14e<2> +.def 0 +1 1 - 1 +0 - 1 1 +.names load o<3> o$_n4a$raw_n128<3> o$load$raw_n14e<3> +.def 0 +1 1 - 1 +0 - 1 1 +.names load o<4> o$_n4a$raw_n128<4> o$load$raw_n14e<4> +.def 0 +1 1 - 1 +0 - 1 1 +.names load o<5> o$_n4a$raw_n128<5> o$load$raw_n14e<5> +.def 0 +1 1 - 1 +0 - 1 1 +.names load o<6> o$_n4a$raw_n128<6> o$load$raw_n14e<6> +.def 0 +1 1 - 1 +0 - 1 1 +.names load o<7> o$_n4a$raw_n128<7> o$load$raw_n14e<7> +.def 0 +1 1 - 1 +0 - 1 1 +# assign load = start & ~busy +.names busy _n15a +0 1 +1 0 +# start & ~busy +.names start _n15a _n15b +.def 0 +1 1 1 +.names _n15b load$raw_n159 +- =_n15b +.names busy _n15c +0 1 +1 0 +.names _n15c _n15d +- =_n15c +.names start _n15e +- =start +# busy = 1 +.names busy$start_n15f$true +1 +# if/else (start ) +.names start busy$start_n15f$true busy busy$start$raw_n162 +.def 0 +1 1 - 1 +0 - 1 1 +.names done _n164 +- =done +# busy = 0 +.names busy$done_n165$true +0 +# if/else (done ) +.names done busy$done_n165$true busy busy$done$raw_n168 +.def 0 +1 1 - 1 +0 - 1 1 +# if/else (~busy ) +.names _n15c busy$start$raw_n162 busy$done$raw_n168 busy$_n15c$raw_n16b +.def 0 +1 1 - 1 +0 - 1 1 +# conflict arbitrators +.names _n45 _n4b _n4c _n58 _n5f _n66 _n78 _n16f +.def 0 + 1 - - - - - - 1 + 0 1 0 0 1 - - 1 + 0 1 0 0 1 - - 1 + 0 1 0 0 0 1 1 1 + 0 1 0 0 0 1 1 1 +.names _n16f y$load$raw_n134<0> y$load$raw_n134<1> y$load$raw_n134<2> y$load$raw_n134<3> y$load$raw_n134<4> y$load$raw_n134<5> y$load$raw_n134<6> y$load$raw_n134<7> y<0> y<1> y<2> y<3> y<4> y<5> y<6> y<7> -> _n170<0> _n170<1> _n170<2> _n170<3> _n170<4> _n170<5> _n170<6> _n170<7> +1 - - - - - - - - - - - - - - - - =y$load$raw_n134<0> =y$load$raw_n134<1> =y$load$raw_n134<2> =y$load$raw_n134<3> =y$load$raw_n134<4> =y$load$raw_n134<5> =y$load$raw_n134<6> =y$load$raw_n134<7> +0 - - - - - - - - - - - - - - - - =y<0> =y<1> =y<2> =y<3> =y<4> =y<5> =y<6> =y<7> +.names _n45 _n4b _ne9 _n171 +.def 0 + 0 0 1 1 +.names _n171 o$load$raw_n14e<0> o$load$raw_n14e<1> o$load$raw_n14e<2> o$load$raw_n14e<3> o$load$raw_n14e<4> o$load$raw_n14e<5> o$load$raw_n14e<6> o$load$raw_n14e<7> o<0> o<1> o<2> o<3> o<4> o<5> o<6> o<7> -> _n172<0> _n172<1> _n172<2> _n172<3> _n172<4> _n172<5> _n172<6> _n172<7> +1 - - - - - - - - - - - - - - - - =o$load$raw_n14e<0> =o$load$raw_n14e<1> =o$load$raw_n14e<2> =o$load$raw_n14e<3> =o$load$raw_n14e<4> =o$load$raw_n14e<5> =o$load$raw_n14e<6> =o$load$raw_n14e<7> +0 - - - - - - - - - - - - - - - - =o<0> =o<1> =o<2> =o<3> =o<4> =o<5> =o<6> =o<7> +.names load$raw_n159 load +0 0 +1 1 +.names _n45 _n4b _n4c _n173 +.def 0 + 1 - - 1 + 0 1 1 1 +.names _n173 lsb$load$raw_n13d<0> lsb$load$raw_n13d<1> lsb$load$raw_n13d<2> lsb<0> lsb<1> lsb<2> -> _n174<0> _n174<1> _n174<2> +1 - - - - - - =lsb$load$raw_n13d<0> =lsb$load$raw_n13d<1> =lsb$load$raw_n13d<2> +0 - - - - - - =lsb<0> =lsb<1> =lsb<2> +.names _n15d _n15e _n164 _n175 +.def 0 + 1 1 - 1 + 0 - 1 1 +.names _n175 busy$_n15c$raw_n16b busy _n176 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.names xy_lsb$raw_n3<0> xy_lsb<0> +- =xy_lsb$raw_n3<0> +.names xy_lsb$raw_n0<1> xy_lsb<1> +- =xy_lsb$raw_n0<1> +.names done$raw_n36 done +0 0 +1 1 +.names diff$raw_n6<0> diff<0> +- =diff$raw_n6<0> +.names diff$raw_n6<1> diff<1> +- =diff$raw_n6<1> +.names diff$raw_n6<2> diff<2> +- =diff$raw_n6<2> +.names diff$raw_n6<3> diff<3> +- =diff$raw_n6<3> +.names diff$raw_n6<4> diff<4> +- =diff$raw_n6<4> +.names diff$raw_n6<5> diff<5> +- =diff$raw_n6<5> +.names diff$raw_n6<6> diff<6> +- =diff$raw_n6<6> +.names diff$raw_n6<7> diff<7> +- =diff$raw_n6<7> +.names _n45 _n4b _n4c _n58 _n5f _n66 _n78 _n177 +.def 0 + 1 - - - - - - 1 + 0 1 0 1 - - - 1 + 0 1 0 1 - - - 1 + 0 1 0 0 0 1 0 1 + 0 1 0 0 0 1 0 1 +.names _n177 x$load$raw_n141<0> x$load$raw_n141<1> x$load$raw_n141<2> x$load$raw_n141<3> x$load$raw_n141<4> x$load$raw_n141<5> x$load$raw_n141<6> x$load$raw_n141<7> x<0> x<1> x<2> x<3> x<4> x<5> x<6> x<7> -> _n178<0> _n178<1> _n178<2> _n178<3> _n178<4> _n178<5> _n178<6> _n178<7> +1 - - - - - - - - - - - - - - - - =x$load$raw_n141<0> =x$load$raw_n141<1> =x$load$raw_n141<2> =x$load$raw_n141<3> =x$load$raw_n141<4> =x$load$raw_n141<5> =x$load$raw_n141<6> =x$load$raw_n141<7> +0 - - - - - - - - - - - - - - - - =x<0> =x<1> =x<2> =x<3> =x<4> =x<5> =x<6> =x<7> +# non-blocking assignments +# latches +.r y$raw_n33<0> y<0> +.def 0 +1 1 +.r y$raw_n33<1> y<1> +.def 0 +1 1 +.r y$raw_n33<2> y<2> +.def 0 +1 1 +.r y$raw_n33<3> y<3> +.def 0 +1 1 +.r y$raw_n33<4> y<4> +.def 0 +1 1 +.r y$raw_n33<5> y<5> +.def 0 +1 1 +.r y$raw_n33<6> y<6> +.def 0 +1 1 +.r y$raw_n33<7> y<7> +.def 0 +1 1 +.latch _n170<0> y<0> +.latch _n170<1> y<1> +.latch _n170<2> y<2> +.latch _n170<3> y<3> +.latch _n170<4> y<4> +.latch _n170<5> y<5> +.latch _n170<6> y<6> +.latch _n170<7> y<7> +.r o$raw_n34<0> o<0> +.def 0 +1 1 +.r o$raw_n34<1> o<1> +.def 0 +1 1 +.r o$raw_n34<2> o<2> +.def 0 +1 1 +.r o$raw_n34<3> o<3> +.def 0 +1 1 +.r o$raw_n34<4> o<4> +.def 0 +1 1 +.r o$raw_n34<5> o<5> +.def 0 +1 1 +.r o$raw_n34<6> o<6> +.def 0 +1 1 +.r o$raw_n34<7> o<7> +.def 0 +1 1 +.latch _n172<0> o<0> +.latch _n172<1> o<1> +.latch _n172<2> o<2> +.latch _n172<3> o<3> +.latch _n172<4> o<4> +.latch _n172<5> o<5> +.latch _n172<6> o<6> +.latch _n172<7> o<7> +.r busy$raw_n31 busy +0 0 +1 1 +.latch _n176 busy +.r lsb$raw_n35<0> lsb<0> +.def 0 +1 1 +.r lsb$raw_n35<1> lsb<1> +.def 0 +1 1 +.r lsb$raw_n35<2> lsb<2> +.def 0 +1 1 +.latch _n174<0> lsb<0> +.latch _n174<1> lsb<1> +.latch _n174<2> lsb<2> +.r x$raw_n32<0> x<0> +.def 0 +1 1 +.r x$raw_n32<1> x<1> +.def 0 +1 1 +.r x$raw_n32<2> x<2> +.def 0 +1 1 +.r x$raw_n32<3> x<3> +.def 0 +1 1 +.r x$raw_n32<4> x<4> +.def 0 +1 1 +.r x$raw_n32<5> x<5> +.def 0 +1 1 +.r x$raw_n32<6> x<6> +.def 0 +1 1 +.r x$raw_n32<7> x<7> +.def 0 +1 1 +.latch _n178<0> x<0> +.latch _n178<1> x<1> +.latch _n178<2> x<2> +.latch _n178<3> x<3> +.latch _n178<4> x<4> +.latch _n178<5> x<5> +.latch _n178<6> x<6> +.latch _n178<7> x<7> +# quasi-continuous assignment +.end +.model select +# I/O ports +.inputs z<0> z<1> z<2> z<3> z<4> z<5> z<6> z<7> +.inputs lsb<0> lsb<1> lsb<2> +.outputs select<0> +.names _n17a<0> +0 +.names _n17a<1> +0 +.names _n17a<2> +0 +# lsb == 'b000 +.names lsb<0> _n17a<0> _n17b<0> +.def 0 +0 1 1 +1 0 1 +.names lsb<1> _n17a<1> _n17b<1> +.def 0 +0 1 1 +1 0 1 +.names lsb<2> _n17a<2> _n17b<2> +.def 0 +0 1 1 +1 0 1 +.names _n17b<0> _n17b<1> _n17b<2> _n17c +.def 1 +0 0 0 0 +.names _n17c _n179 +0 1 +1 0 +.names _n179 _n17d +- =_n179 +# select = z [0] +.names z<0> select$_n179_n17e$true<0> +- =z<0> +.names _n180<0> +1 +.names _n180<1> +0 +.names _n180<2> +0 +# lsb == 'b001 +.names lsb<0> _n180<0> _n181<0> +.def 0 +0 1 1 +1 0 1 +.names lsb<1> _n180<1> _n181<1> +.def 0 +0 1 1 +1 0 1 +.names lsb<2> _n180<2> _n181<2> +.def 0 +0 1 1 +1 0 1 +.names _n181<0> _n181<1> _n181<2> _n182 +.def 1 +0 0 0 0 +.names _n182 _n17f +0 1 +1 0 +.names _n17f _n183 +- =_n17f +# select = z [1] +.names z<1> select$_n17f_n184$true<0> +- =z<1> +.names _n186<0> +0 +.names _n186<1> +1 +.names _n186<2> +0 +# lsb == 'b010 +.names lsb<0> _n186<0> _n187<0> +.def 0 +0 1 1 +1 0 1 +.names lsb<1> _n186<1> _n187<1> +.def 0 +0 1 1 +1 0 1 +.names lsb<2> _n186<2> _n187<2> +.def 0 +0 1 1 +1 0 1 +.names _n187<0> _n187<1> _n187<2> _n188 +.def 1 +0 0 0 0 +.names _n188 _n185 +0 1 +1 0 +.names _n185 _n189 +- =_n185 +# select = z [2] +.names z<2> select$_n185_n18a$true<0> +- =z<2> +.names _n18c<0> +1 +.names _n18c<1> +1 +.names _n18c<2> +0 +# lsb == 'b011 +.names lsb<0> _n18c<0> _n18d<0> +.def 0 +0 1 1 +1 0 1 +.names lsb<1> _n18c<1> _n18d<1> +.def 0 +0 1 1 +1 0 1 +.names lsb<2> _n18c<2> _n18d<2> +.def 0 +0 1 1 +1 0 1 +.names _n18d<0> _n18d<1> _n18d<2> _n18e +.def 1 +0 0 0 0 +.names _n18e _n18b +0 1 +1 0 +.names _n18b _n18f +- =_n18b +# select = z [3] +.names z<3> select$_n18b_n190$true<0> +- =z<3> +.names _n192<0> +0 +.names _n192<1> +0 +.names _n192<2> +1 +# lsb == 'b100 +.names lsb<0> _n192<0> _n193<0> +.def 0 +0 1 1 +1 0 1 +.names lsb<1> _n192<1> _n193<1> +.def 0 +0 1 1 +1 0 1 +.names lsb<2> _n192<2> _n193<2> +.def 0 +0 1 1 +1 0 1 +.names _n193<0> _n193<1> _n193<2> _n194 +.def 1 +0 0 0 0 +.names _n194 _n191 +0 1 +1 0 +.names _n191 _n195 +- =_n191 +# select = z [4] +.names z<4> select$_n191_n196$true<0> +- =z<4> +.names _n198<0> +1 +.names _n198<1> +0 +.names _n198<2> +1 +# lsb == 'b101 +.names lsb<0> _n198<0> _n199<0> +.def 0 +0 1 1 +1 0 1 +.names lsb<1> _n198<1> _n199<1> +.def 0 +0 1 1 +1 0 1 +.names lsb<2> _n198<2> _n199<2> +.def 0 +0 1 1 +1 0 1 +.names _n199<0> _n199<1> _n199<2> _n19a +.def 1 +0 0 0 0 +.names _n19a _n197 +0 1 +1 0 +.names _n197 _n19b +- =_n197 +# select = z [5] +.names z<5> select$_n197_n19c$true<0> +- =z<5> +.names _n19e<0> +0 +.names _n19e<1> +1 +.names _n19e<2> +1 +# lsb == 'b110 +.names lsb<0> _n19e<0> _n19f<0> +.def 0 +0 1 1 +1 0 1 +.names lsb<1> _n19e<1> _n19f<1> +.def 0 +0 1 1 +1 0 1 +.names lsb<2> _n19e<2> _n19f<2> +.def 0 +0 1 1 +1 0 1 +.names _n19f<0> _n19f<1> _n19f<2> _n1a0 +.def 1 +0 0 0 0 +.names _n1a0 _n19d +0 1 +1 0 +.names _n19d _n1a1 +- =_n19d +# select = z [6] +.names z<6> select$_n19d_n1a2$true<0> +- =z<6> +# select = z [7] +.names z<7> select$_n19d_n1a3$false<0> +- =z<7> +# if/else (lsb == 'b110) +.names _n19d select$_n19d_n1a2$true<0> select$_n19d_n1a3$false<0> select$_n19d$raw_n1a5<0> +.def 0 +1 1 - 1 +0 - 1 1 +# if/else (lsb == 'b101) +.names _n197 select$_n197_n19c$true<0> select$_n19d$raw_n1a5<0> select$_n197$raw_n1aa<0> +.def 0 +1 1 - 1 +0 - 1 1 +# if/else (lsb == 'b100) +.names _n191 select$_n191_n196$true<0> select$_n197$raw_n1aa<0> select$_n191$raw_n1af<0> +.def 0 +1 1 - 1 +0 - 1 1 +# if/else (lsb == 'b011) +.names _n18b select$_n18b_n190$true<0> select$_n191$raw_n1af<0> select$_n18b$raw_n1b4<0> +.def 0 +1 1 - 1 +0 - 1 1 +# if/else (lsb == 'b010) +.names _n185 select$_n185_n18a$true<0> select$_n18b$raw_n1b4<0> select$_n185$raw_n1b9<0> +.def 0 +1 1 - 1 +0 - 1 1 +# if/else (lsb == 'b001) +.names _n17f select$_n17f_n184$true<0> select$_n185$raw_n1b9<0> select$_n17f$raw_n1be<0> +.def 0 +1 1 - 1 +0 - 1 1 +# if/else (lsb == 'b000) +.names _n179 select$_n179_n17e$true<0> select$_n17f$raw_n1be<0> select$_n179$raw_n1c3<0> +.def 0 +1 1 - 1 +0 - 1 1 +# conflict arbitrators +.names select$_n179$raw_n1c3<0> select<0> +- =select$_n179$raw_n1c3<0> +.end + + Index: vis_dev/vis-2.3/models/arbiter/gcd.v =================================================================== --- vis_dev/vis-2.3/models/arbiter/gcd.v (revision 28) +++ vis_dev/vis-2.3/models/arbiter/gcd.v (revision 28) @@ -0,0 +1,118 @@ + +// GCD circuit for unsigned N-bit numbers +// a[0], b[0], and o[0] are the least significant bits +// +// Author: Fabio Somenzi +module gcd(clock,start,a,b,busy,o); + parameter N = 8; + parameter logN = 3; + input clock; + input start; + input [N-1:0] a; + input [N-1:0] b; + output busy; + output [N-1:0] o; + + reg [logN-1:0] lsb; + reg [N-1:0] x; + reg [N-1:0] y; + wire done; + wire load; + reg busy; + reg [N-1:0] o; + + wire [1:0] xy_lsb; + wire [N-1:0] diff; + + function select; + input [N-1:0] z; + input [logN-1:0] lsb; + begin: _select + if (lsb == 3'd0) + select = z[0]; + else if (lsb == 3'd1) + select = z[1]; + else if (lsb == 3'd2) + select = z[2]; + else if (lsb == 3'd3) + select = z[3]; + else if (lsb == 3'd4) + select = z[4]; + else if (lsb == 3'd5) + select = z[5]; + else if (lsb == 3'd6) + select = z[6]; + else + select = z[7]; + end // block: _select + endfunction // select + + assign xy_lsb[1] = select(x,lsb); + assign xy_lsb[0] = select(y,lsb); + assign diff = x < y ? y - x : x - y; + + initial begin + busy = 0; + x = 0; + y = 0; + o = 0; + lsb = 0; + end // initial begin + + assign done = ((x == y) | (x == 0) | (y == 0)) & busy; + + // Data path. + always @(posedge clock) begin + if (load) begin + x = a; + y = b; + lsb = 0; + end // if (load) + else if (busy & ~done) begin + case (xy_lsb) + 2'b00: + lsb = lsb + 1; + 2'b01: + begin + x[N-2:0] = x[N-1:1]; + x[N-1] = 0; + end + 2'b10: + begin + y[N-2:0] = y[N-1:1]; + y[N-1] = 0; + end + 2'b11: begin + if (x < y) begin + y[N-2:0] = diff[N-1:1]; + y[N-1] = 0; + end // if (x < y) + else begin + x[N-2:0] = diff[N-1:1]; + x[N-1] = 0; + end // else: !if(x < y) + end // case: 2b'11 + endcase // case (xy_lsb) + end // if (~done) + else if (done) begin + o = (x < y) ? x : y; + end // else: !if(~done) + end // always @ (posedge clock) + + assign load = start & ~busy; + + // Controller. + always @(posedge clock) begin + if (~busy) begin + if (start) begin + busy = 1; + end // if (start) + end // if (~busy) + else begin + if (done) begin + busy = 0; + end + end // else: !if(~busy) + end // always @ (posedge clock) + +endmodule // gcd Index: vis_dev/vis-2.3/models/counter/affalse =================================================================== --- vis_dev/vis-2.3/models/counter/affalse (revision 28) +++ vis_dev/vis-2.3/models/counter/affalse (revision 28) @@ -0,0 +1,1 @@ +AF FALSE; Index: vis_dev/vis-2.3/models/counter/check_result =================================================================== --- vis_dev/vis-2.3/models/counter/check_result (revision 28) +++ vis_dev/vis-2.3/models/counter/check_result (revision 28) @@ -0,0 +1,3 @@ +# MC: formula failed --- AF(FALSE) +# LE: language is not empty +# MC: formula passed --- AG(AF(bit2.carry_out=1)) Index: vis_dev/vis-2.3/models/counter/check_script =================================================================== --- vis_dev/vis-2.3/models/counter/check_script (revision 28) +++ vis_dev/vis-2.3/models/counter/check_script (revision 28) @@ -0,0 +1,7 @@ +read_blif_mv counter.mv +init_verify +model_check -d 0 affalse +lang_empty -d 0 +model_check -d 0 counter.ctl +time +quit -s Index: vis_dev/vis-2.3/models/counter/counter.ctl =================================================================== --- vis_dev/vis-2.3/models/counter/counter.ctl (revision 28) +++ vis_dev/vis-2.3/models/counter/counter.ctl (revision 28) @@ -0,0 +1,3 @@ +AG AF (bit2.carry_out=1) ; +AG (bit2.carry_out=1) ; + Index: vis_dev/vis-2.3/models/counter/counter.mv =================================================================== --- vis_dev/vis-2.3/models/counter/counter.mv (revision 28) +++ vis_dev/vis-2.3/models/counter/counter.mv (revision 28) @@ -0,0 +1,111 @@ +# vl2mv counter.v +# version: 2.1 +# date: 14:50:04 01/27/2010 (CET) +.model counter +# I/O ports +.names _n0 +1 +.subckt counter_cell bit0 carry_in=_n0 carry_out=out0 +.subckt counter_cell bit1 carry_in=out0 carry_out=out1 +.subckt counter_cell bit2 carry_in=out1 carry_out=out2 +# conflict arbitrators +# non-blocking assignments +# latches +# quasi-continuous assignment +.end +.model counter_cell +# I/O ports +.inputs carry_in +.outputs carry_out +# assign carry_out = value & carry_in +# value & carry_in +.names value carry_in _n2 +.def 0 +1 1 1 +.names _n2 carry_out$raw_n1 +- =_n2 +# value = 0 +.names value$raw_n3 +0 +# non-blocking assignments for initial +.names _n6 +0 +.names value _n6 _n7 +.def 0 +0 1 1 +1 0 1 +.names _n7 _n5 +0 1 +1 0 +.names _n5 _n4 +.def 1 +0 0 +# value = carry_in +.names carry_in value$_n4_n9$true +- =carry_in +.names _nc +1 +.names value _nc _nd +.def 0 +0 1 1 +1 0 1 +.names _nd _nb +0 1 +1 0 +.names _nb _na +.def 1 +0 0 +.names _n10 +0 +# carry_in == 0 +.names carry_in _n10 _n11 +.def 0 +0 1 1 +1 0 1 +.names _n11 _nf +0 1 +1 0 +.names _nf _n13 +- =_nf +# value = 1 +.names value$_nf_n14$true +1 +# value = 0 +.names value$_nf_n15$false +0 +# if/else (carry_in == 0) +.names _nf value$_nf_n14$true value$_nf_n15$false value$_nf$raw_n17 +.def 0 +1 1 - 1 +0 - 1 1 +# case (value ) +.names _na value$_nf$raw_n17 value value$_na$raw_n1d +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4 value$_n4_n9$true value$_na$raw_n1d value$_n4$raw_n1f +.def 0 +1 1 - 1 +0 - 1 1 +# conflict arbitrators +.names _n4 _na _n13 _n24 +.def 0 + 1 - - 1 + 0 1 1 1 + 0 1 0 1 +.names _n24 value$_n4$raw_n1f value _n25 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.names carry_out$raw_n1 carry_out +0 0 +1 1 +# non-blocking assignments +# latches +.r value$raw_n3 value +0 0 +1 1 +.latch _n25 value +# quasi-continuous assignment +.end Index: vis_dev/vis-2.3/models/counter/counter.v =================================================================== --- vis_dev/vis-2.3/models/counter/counter.v (revision 28) +++ vis_dev/vis-2.3/models/counter/counter.v (revision 28) @@ -0,0 +1,41 @@ +/* translation of counter.smv to verilog + + Sriram Krishnan 7/93. + + + +*/ + + + +module counter(clk); +input clk; + +wire out0, out1, out2; + +counter_cell bit0 (clk, 1, out0); +counter_cell bit1 (clk, out0, out1); +counter_cell bit2 (clk, out1, out2); +endmodule + +module counter_cell(clk, carry_in, carry_out); +input clk; +input carry_in; +output carry_out; +reg value; + +assign carry_out = value & carry_in; + +initial value = 0; + +always @(posedge clk) begin +// value = (value + carry_in) % 2; + case(value) + 0: value = carry_in; + 1: if (carry_in ==0) + value = 1; + else value = 0; + endcase +end +endmodule + Index: vis_dev/vis-2.3/models/counter/init.prop =================================================================== --- vis_dev/vis-2.3/models/counter/init.prop (revision 28) +++ vis_dev/vis-2.3/models/counter/init.prop (revision 28) @@ -0,0 +1,2 @@ +\define INIT (golden.bit0.value = 1 * (golden.bit1.value = 1 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * ( faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0))))+ golden.bit1.value = 0 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * ( faulty.bit2.value = 0))+ faulty.bit0.value = 0 * ( faulty.bit1.value = 0 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * ( faulty.bit1.value = 0 * ( faulty.bit2.value = 0)))))+ golden.bit0.value = 0 * (golden.bit1.value = 1 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * ( faulty.bit2.value = 0))))+ golden.bit1.value = 0 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * ( faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * ( faulty.bit2.value = 0)))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * ( faulty.bit1.value = 0 * ( faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 )))))) +\define GOLDEN (golden.bit0.value = 1 * (golden.bit1.value = 1 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * ( faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0))))+ golden.bit1.value = 0 * (golden.bit2.value = 1 * ( faulty.bit0.value = 0 * ( faulty.bit1.value = 0 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * ( faulty.bit0.value = 0 * ( faulty.bit1.value = 0 * ( faulty.bit2.value = 0)))))) Index: vis_dev/vis-2.3/models/counter/properties.ltl =================================================================== --- vis_dev/vis-2.3/models/counter/properties.ltl (revision 28) +++ vis_dev/vis-2.3/models/counter/properties.ltl (revision 28) @@ -0,0 +1,1 @@ +\define INIT (golden.bit0.value = 1 * (golden.bit1.value = 1 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * ( faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0))))+ golden.bit1.value = 0 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * ( faulty.bit2.value = 0))+ faulty.bit0.value = 0 * ( faulty.bit1.value = 0 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * ( faulty.bit1.value = 0 * ( faulty.bit2.value = 0)))))+ golden.bit0.value = 0 * (golden.bit1.value = 1 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * ( faulty.bit2.value = 0))))+ golden.bit1.value = 0 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * ( faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * ( faulty.bit2.value = 0)))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * ( faulty.bit1.value = 0 * ( faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * ( faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 )))))) Index: vis_dev/vis-2.3/models/counter/protect_golden.reg =================================================================== --- vis_dev/vis-2.3/models/counter/protect_golden.reg (revision 28) +++ vis_dev/vis-2.3/models/counter/protect_golden.reg (revision 28) @@ -0,0 +1,3 @@ +golden.bit0.value +golden.bit1.value +golden.bit2.value Index: vis_dev/vis-2.3/models/counter/rob.script =================================================================== --- vis_dev/vis-2.3/models/counter/rob.script (revision 28) +++ vis_dev/vis-2.3/models/counter/rob.script (revision 28) @@ -0,0 +1,6 @@ +rlmv counter.mv +compose_golden +init +set_init -v 1 -m usut -g protect_golden.reg + + Index: vis_dev/vis-2.3/models/transition/f.ctl =================================================================== --- vis_dev/vis-2.3/models/transition/f.ctl (revision 28) +++ vis_dev/vis-2.3/models/transition/f.ctl (revision 28) @@ -0,0 +1,1 @@ +!EX(state[1:0] = 1); Index: vis_dev/vis-2.3/models/transition/mc.html =================================================================== --- vis_dev/vis-2.3/models/transition/mc.html (revision 28) +++ vis_dev/vis-2.3/models/transition/mc.html (revision 28) @@ -0,0 +1,998 @@ + +/**Function******************************************************************** + + Synopsis [Check CTL formulas given in file are modeled by flattened network] + + CommandName [model_check] + + CommandSynopsis [perform fair CTL model checking on a flattened network] + + CommandArguments [ \[-b\] \[-c\] \[-d <dbg_level>\] + \[-f <dbg_file>\] \[-g <hints_file>\] \[-h\] \[-i\] \[-m\] \[-r\] + \[-t <time_out_period>\]\[-v <verbosity_level>\] + \[-D <dc_level>\] \[-F\] \[-S <schedule>\] \[-V\] \[-B\] \[-I\] + \[-C\] \[-w <node_file>\] \[-W\] \[-G\] <ctl_file>] + + CommandDescription [Performs fair CTL model checking on a flattened + network. Before calling this command, the user should have + initialized the design by calling the command init_verify. + Regardless of the options, no 'false positives' or 'false negatives' + will occur: the result is correct for the given circuit.

+ + Properties to be verified should be provided as CTL formulas in the + file ctl_file. Note that the support of any wire + referred to in a formula should consist only of latches. For the + precise syntax of CTL formulas, see the VIS CTL and LTL syntax manual.

+ + Properties of the form AG f, where f is a formula not + involving path quantifiers are referred to as invariants; for such properties + it may be substantially faster to use the + check_invariant command. +

+ + A fairness constraint can be specified by invoking the + read_fairness command; + if none is specified, all paths are taken to be fair. + If some initial states + do not lie on a fair path, the model checker prints a message to this effect. +

+ + A formula passes iff it is true for all initial states of the + system. Therefore, in the presence of multiple initial states, if a + formula fails, the negation of the formula may also fail.

+ + If a formula does not pass, a (potentially partial) proof of failure + (referred to as a debug trace) is demonstrated. Fair paths are + represented by a finite sequence of states (the stem) leading to a + fair cycle, i.e. a cycle on which there is a state from each + fairness condition. The level of detail of the proof can be + specified (see option -d).

+ + Both backward (future tense CTL formulas) and forward (past tense CTL + formulas) model checking can be performed. Forward model checking is + based on Iwashita's ICCAD96 paper. Future tense CTL formulas are + automatically converted to past tense ones as much as possible in + forward model checking.

+ + Command options: +

+ +

+ +
-b +
Use backward analysis when performing debugging; the default is + to use forward analysis. This should be tried when the debugger spends a + large amount of time when creating a path to a fair cycle. This option is not + compatible with forward model checking option (-F).

+ +

-c +
Use the formula tree so that there is no sharing of sub-formulae among + the formulae in the input file. This option is useful in the following + scenario - formulae A, B and C are being checked in order and there is + sub-formula sharing between A and C. If the BDDs corresponding to the shared + sub-formula is huge then computation for B might not be able to finish + without using this option. +

+ +

-d <dbg_level>
Specify the amount of + debugging performed when the system fails a formula being checked. + Note that it may not always be possible to give a simple + counter-example to show that a formula is false, since this may + require enumerating all paths from a state. In such a case the + model checker will print a message to this effect. This option is + incompatible with -F.

+

dbg_level must be one of the following: + +

0: No debugging performed. + dbg_level=0 is the default. + +

1: Debugging with minimal output: generate counter-examples + for universal formulas (formulas of the form AX|AF|AU|AG) and + witnesses for existential formulas (formulas of the form + EX|EF|EU|EG). States on a path are not further analyzed. + +

2: Same as dbg_level=1, but more + verbose. (The subformulas are printed, too.) + +

3: Maximal automatic debugging: as for level 1, + except that states occurring on paths will be recursively analyzed. + +

4: Manual debugging: at each state, the user is queried if + more feedback is desired. +

+ +

+ +

-f <dbg_file> +
Write the debugger output to dbg_file. + This option is incompatible with -F. + Notes: when you use -d4 (interactive mode), -f is not recommended, since you + can't see the output of vis on stdout.
+ +
-g <hints_file>
Use guided search. The file + hints_file contains a series of hints. A hint is a formula that + does not contain any temporal operators, so hints_file has the + same syntax as a file of invariants used for check_invariant. The hints are + used in the order given to change the transition relation. In the case of + least fixpoints (EF, EU), the transition relation is conjoined with the hint, + whereas for greatest fixpoints the transition relation is disjoined with the + negation of the hint. If the hints are cleverly chosen, this may speed up + the computation considerably, because a search with the changed transition + relation may be much simpler than one with the original transition relation, + and results obtained can be reused, so that we may never have to do a + complicated search with the original relation. Note: hints in terms of + primary inputs are not useful for greatest fixpoints. See also: Ravi and + Somenzi, Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and + Somenzi, Efficient Decision Procedures for Model Checking of Linear Time + Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search + for CTL Model Checking, DAC'00. + +

For formulae that contain both least and greatest fixpoints, the + behavior depends on the flag guided_search_hint_type. + If it is set to local (default) then every subformula is evaluated + to completion, using all hints in order, before the next subformula + is started. For pure ACTL or pure ECTL formulae, we can also set + guided_search_hint_type to global, in which case the entire formula + is evaluated for one hint before moving on to the next hint, using + underapproximations. The description of the options for guided + search can be found in the help page for + print_guided_search_options. + +

model_check will call reachability without any guided search, even + if -g is used. If you want to perform reachability with guided + search, call rch directly. + +

Incompatible with -F.

+ +
-h +
Print the command usage.
+

+ +

-i +
Print input values causing transitions between states during debugging. + Both primary and pseudo inputs are printed. + This option is incompatible with -F.
+

+ +

-m +
Pipe debugger output through the UNIX utility more. + This option is incompatible with -F.
+

+ +

-r +
Reduce the FSM derived from the flattened network with respect to each + formula being checked. By default, the FSM is reduced with respect to the + conjunction of the formulae in the input file. If this option is used and + don't cares are being used for simplification, then subformula sharing is + disabled (result might be incorrect otherwise).
+

+ +

The truth of a formula may be independent of parts of the network + (such as when wires have been abstracted; see + flatten_hierarchy). + These parts are effectively removed when this option is invoked; this may + result in more efficient model checking.
+

+ +

-t <timeOutPeriod> +
Specify the time out period (in seconds) after which the command + aborts. By default this option is set to infinity.
+

+ +

-v <verbosity_level> +
Specify verbosity level. This sets the amount of feedback on CPU usage + and code status. + +
verbosity_level must be one of the following:

+ + 0: No feedback provided. This is the default.

+ + 1: Feedback on code location.

+ + 2: Feedback on code location and CPU usage.

+ +

-B +
Check for vacuously passing formulae using the algorithm of Beer et al. + (CAV97). The algorithm applies to a subset of ACTL (w-ACTL) and replaces + the smallest important subformula of a passing property with either FALSE + or TRUE depending on its negation parity. It then applies model checking + to the resulting witness formula. If the witness formula also passes, then + the original formula is deemed to pass vacuously. If the witness formula + fails, a counterexample to it provides an interesting witness to the + original passing formula. See the CAV97 paper for the definitions of + w-ACTL, important subformula, and interesting witness. In short, one of the + operands of a binary operator in a w-ACTL formula must be a propositional + formula. See also the -V option. +

+ +

-C +
Compute coverage of all observable signals in a set of CTL formulae + using the algorithm of Hoskote, Kam, Ho, Zhao (DAC'99). If the verbosity + level (-v option) is equal to 0, only the coverage stats are printed. If + verbosity level is greater than zero, then detailed information of the + computation at each step of the algorithm is also provided. + Debug information is provided in the form of states not covered for each + observable signal if the dbg_level (-d option) is greater than 0. The number + of states printed is set by the vis environment variable + 'nr_uncoveredstates'. By default the number of states printed is 1. + The value of nr_uncoveredstates can be set using the set command. + See also the -I option.
+

+ +

-D <dc_level> + +
Specify extent to which don't cares are used to simplify MDDs in model + checking. Don't cares are minterms on which the values taken by functions + do not affect the computation; potentially, these minterms can be used to + simplify MDDs and reduce the time taken to perform model checking. The -g + flag for guided search does not affect the way in which the don't-care + conditions are computed. + +
+ dc_level must be one of the following: +

+ + 0 : No don't cares are used. + +

1 : Use unreachable states as don't cares. This is the + default. + +

2 : Use unreachable states as don't cares and in the EU + computation, use 'frontiers' for image computation.

+ + 3 : First compute an overapproximation of the reachable states + (ARDC), and use that as the cares set. Use `frontiers' for image + computation. For help on controlling options for ARDC, look up help on the + command: print_ardc_options. Refer + to Moon, Jang, Somenzi, Pixley, Yuan, "Approximate Reachability Don't Cares + for {CTL} Model Checking", ICCAD98, and to two papers by Cho et al, IEEE TCAD + December 1996: one is for State Space Decomposition and the other is for + Approximate FSM Traversal.

+

+ +

-F +
Use forward model checking based on Iwashita's method in ICCAD96. + Future tense CTL formulas are automatically converted to past tense + ones as much as possible. Converted forward formulas are printed when + verbosity is greater than 0. Debug options (-b, -d, -f, -i, and -m) + are ignored with this option. We have seen that forward model checking + was much faster than backward in many cases, also forward was much slower + than backward in many cases.
+

+ +

-I +
Compute coverage of all observable signals in a set of CTL formulae + using an improved algorithm of Jayakumar, Purandare, Somenzi (DAC'03). If + the verbosity level (-v option) is equal to 0, only the coverage stats are + printed. If verbosity level is greater than zero, then detailed information + of the computation at each step of the algorithm is also provided. + Debug information is provided in the form of states not covered for each + observable signal if the dbg_level (-d option) is greater than 0. The number + of states printed is set by the vis environment variable + 'nr_uncoveredstates'. By default the number of states printed is 1. + The value of nr_uncoveredstates can be set using the set command. + Compared to the -C option, this one produces more accurate results and deals + with a larger subset of CTL.
+

+ +

-S <schedule> + +
Specify schedule for GSH algorithm, which generalizes the + Emerson-Lei algorithm and is used to compute greatest fixpoints. + The choice of schedule affects the sequence in which EX and EU + operators are applied. It makes a difference only when fairness + constraints are specified. + +
+ <schedule> must be one of the following: + +

EL : EU and EX operators strictly alternate. This + is the default. + +

EL1 : EX is applied once for every application of all EUs. + +

EL2 : EX is applied repeatedly after each application of + all EUs. + +

budget : a hybrid of EL and EL2. + +

random : enabled operators are applied in + (pseudo-)random order. + +

off : GSH is disabled, and the old algorithm is + used instead. The old algorithm uses the EL schedule, but + the termination checks are less sophisticated than in GSH.

+

+ +

-V +
Check for vacuously passing formulae with the algorithm + of Purandare and Somenzi (CAV2002). The algorithm applies to all of + CTL, and to both passing and failing properties. It says whether a + passing formula may be strengthened and still pass, and whether a + failing formula may be weakened and still fail. It considers all + leaves of a formula that are under one negation parity (e.g., not + descendants of a XOR or EQ node) for replacement by either TRUE or + FALSE. See also the -B option. +

+ + +

-w <node_file> + + This option invoked the algorithm to generate an error trace divided + into fated and free segements. Fate represents the inevitability and + free is asserted when there is no inevitability. This can be formulated + as a two-player concurrent reachability game. The two players are + the environment and the system. The node_file is given to specify the + variables the are controlled by the system. + +
-W
+ + This option represents the case that all input variables are controlled + by system. + +
-G
+ + We proposed two algorithm to generate segemented counter example. + They are general and restrcited algorithm. Bu default we use restricted + algorithm. We can invoke general algorithm with -G option. + + For more information, please check the STTT'04 + paper of Jin et al., "Fate and Free Will in Error Traces"

+ +

<ctl_file> + +
File containing CTL formulas to be model checked. +
+ + Related "set" options: +
+
ctl_change_bracket <yes/no> +
Vl2mv automatically converts "\[\]" to "<>" in node names, + therefore CTL parser does the same thing. However, in some cases a user + does not want to change node names in CTL parsing. Then, use this set + option by giving "no". Default is "yes". +

+

guided_search_hint_type
Switches between local and + global hints (see the -g option, or the help page for set). +
+ + See also commands : approximate_model_check, incremental_ctl_verification + ] + + Description [First argument is a file containing a set of CTL formulas - see + ctlp package for grammar. Second argument is an FSM that we will check the + formulas on. Formulas are checked by calling the recursive function + Mc_ModelCheckFormula. When the formula fails, the debugger is invoked.] + + Comment [Ctlp creates duplicate formulas when converting to + existential form; e.g. when converting AaUb. We aren't using this + fact, which leads to some performance degradation. + + A system satisfies a formula if all its initial states are in the satisfying + set of the formula. Hence, we do not need to continue the computation if we + know that all initial states are in the satisfying set, or if there are + initial states that we are sure are not in the satisfying set. This is what + early termination does: it supplies an extra termination condition for the + fixpoints that kicks in when we can decide the truth of the formula. Note + that this leads to some nasty consequences in storing the satisfying sets. + A computation that has terminated early does not yield the exact satisfying + set, and hence we can not always reuse this result when there is subformula + sharing.] + + SideEffects [] + + SeeAlso [CommandInv] + +******************************************************************************/ +static int +CommandMc( + Hrc_Manager_t **hmgr, + int argc, + char **argv) +{ + /* options */ + McOptions_t *options; + Mc_VerbosityLevel verbosity; + Mc_DcLevel dcLevel; + FILE *ctlFile; + int timeOutPeriod = 0; + Mc_FwdBwdAnalysis traversalDirection; + int buildOnionRings = 0; + FILE *guideFile; + FILE *systemFile; + Mc_GuidedSearch_t guidedSearchType = Mc_None_c; + Ctlp_FormulaArray_t *hintsArray = NIL(Fsm_HintsArray_t); + array_t *hintsStatesArray = NIL(array_t); /* array of mdd_t* */ + st_table *systemVarBddIdTable; + boolean noShare = 0; + Mc_GSHScheduleType GSHschedule; + boolean checkVacuity; + boolean performCoverageHoskote; + boolean performCoverageImproved; + + /* CTL formulae */ + array_t *ctlArray; + array_t *ctlNormalFormulaArray; + int i; + int numFormulae; + /* FSM, network and image */ + Fsm_Fsm_t *totalFsm = NIL(Fsm_Fsm_t); + Fsm_Fsm_t *modelFsm = NIL(Fsm_Fsm_t); + Fsm_Fsm_t *reducedFsm = NIL(Fsm_Fsm_t); + Ntk_Network_t *network; + mdd_t *modelCareStates = NIL(mdd_t); + array_t *modelCareStatesArray = NIL(array_t); + mdd_t *modelInitialStates; + mdd_t *fairStates; + Fsm_Fairness_t *fairCond; + mdd_manager *mddMgr; + array_t *bddIdArray; + Img_ImageInfo_t *imageInfo; + Mc_EarlyTermination_t *earlyTermination; + /* Coverage estimation */ + mdd_t *totalcoveredstates = NIL(mdd_t); + array_t *signalTypeList = array_alloc(int,0); + array_t *signalList = array_alloc(char *,0); + array_t *statesCoveredList = array_alloc(mdd_t *,0); + array_t *newCoveredStatesList = array_alloc(mdd_t *,0); + array_t *statesToRemoveList = array_alloc(mdd_t *,0); + + /* Early termination is only partially implemented right now. It needs + distribution over all operators, including limited cases of temporal + operators. That should be relatively easy to implement. */ + + /* time keeping */ + long totalInitialTime; /* for model checking */ + long initialTime, finalTime; /* for model checking */ + + error_init(); + Img_ResetNumberOfImageComputation(Img_Both_c); + + /* read options */ + if (!(options = ParseMcOptions(argc, argv))) { + return 1; + } + verbosity = McOptionsReadVerbosityLevel(options); + dcLevel = McOptionsReadDcLevel(options); + ctlFile = McOptionsReadCtlFile(options); + timeOutPeriod = McOptionsReadTimeOutPeriod(options); + traversalDirection = McOptionsReadTraversalDirection(options); + buildOnionRings = + (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity); + noShare = McOptionsReadUseFormulaTree(options); + GSHschedule = McOptionsReadSchedule(options); + checkVacuity = McOptionsReadVacuityDetect(options); + /* for the command mc -C foo.ctl */ + performCoverageHoskote = McOptionsReadCoverageHoskote(options); + /* for the command mc -I foo.ctl */ + performCoverageImproved = McOptionsReadCoverageImproved(options); + + /* Check for incompatible options and do some option-specific + * intializations. + */ + + if (traversalDirection == McFwd_c) { + if (checkVacuity) { + fprintf(vis_stderr, "** mc error: -V and -B are incompatible with -F\n"); + McOptionsFree(options); + return 1; + } + if (performCoverageHoskote || performCoverageImproved) { + fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -F\n"); + McOptionsFree(options); + return 1; + } + } + + if (checkVacuity) { + if (performCoverageHoskote || performCoverageImproved) { + fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -V and -B\n"); + McOptionsFree(options); + return 1; + } + } + + guideFile = McOptionsReadGuideFile(options); + + if(guideFile != NIL(FILE) ){ + guidedSearchType = Mc_ReadGuidedSearchType(); + if(guidedSearchType == Mc_None_c){ /* illegal setting */ + fprintf(vis_stderr, "** mc error: Unknown hint type\n"); + fclose(guideFile); + McOptionsFree(options); + return 1; + } + + if(traversalDirection == McFwd_c){ /* illegal combination */ + fprintf(vis_stderr, "** mc error: -g is incompatible with -F\n"); + fclose(guideFile); + McOptionsFree(options); + return 1; + } + + if(Img_UserSpecifiedMethod() != Img_Iwls95_c && + Img_UserSpecifiedMethod() != Img_Monolithic_c && + Img_UserSpecifiedMethod() != Img_Mlp_c){ + fprintf(vis_stderr, "** mc error: -g only works with iwls95, MLP, or monolithic image methods.\n"); + fclose(guideFile); + McOptionsFree(options); + return 1; + } + + hintsArray = Mc_ReadHints(guideFile); + fclose(guideFile); guideFile = NIL(FILE); + if( hintsArray == NIL(array_t) ){ + McOptionsFree(options); + return 1; + } + + } /* if guided search */ + + /* If don't-cares are used, -r implies -c. Note that the satisfying + sets of a subformula are only in terms of propositions therein + and their cone of influence. Hence, we can share satisfying sets + among formulae. I don't quite understand what the problem with + don't-cares is (RB) */ + if (McOptionsReadReduceFsm(options)) + if (dcLevel != McDcLevelNone_c) + McOptionsSetUseFormulaTree(options, TRUE); + + if (traversalDirection == McFwd_c && + McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { + McOptionsSetDbgLevel(options, McDbgLevelNone_c); + (void)fprintf(vis_stderr, "** mc warning : option -d is ignored.\n"); + } + + /* Read CTL formulae */ + ctlArray = Ctlsp_FileParseCTLFormulaArray(ctlFile); + fclose(ctlFile); ctlFile = NIL(FILE); + if (ctlArray == NIL(array_t)) { + (void) fprintf(vis_stderr, + "** mc error: error in parsing formulas from file\n"); + McOptionsFree(options); + return 1; + } + + /* read network */ + network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); + if (network == NIL(Ntk_Network_t)) { + fprintf(vis_stdout, "%s\n", error_string()); + error_init(); + Ctlp_FormulaArrayFree(ctlArray); + McOptionsFree(options); + return 1; + } + + /* read fsm */ + totalFsm = Fsm_NetworkReadOrCreateFsm(network); + if (totalFsm == NIL(Fsm_Fsm_t)) { + fprintf(vis_stdout, "%s\n", error_string()); + error_init(); + Ctlp_FormulaArrayFree(ctlArray); + McOptionsFree(options); + return 1; + } + + /* Assign variables to system if doing FAFW */ + systemVarBddIdTable = NIL(st_table); + systemFile = McOptionsReadSystemFile(options); + if (systemFile != NIL(FILE)) { + systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile); + fclose(systemFile); systemFile = NIL(FILE); + if (systemVarBddIdTable == (st_table *)-1 ) { /* FS: error message? */ + Ctlp_FormulaArrayFree(ctlArray); + McOptionsFree(options); + return 1; + } + } /* if FAFW */ + + if(options->FAFWFlag && systemVarBddIdTable == 0) { + systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm); + } + + if (verbosity > McVerbosityNone_c) + totalInitialTime = util_cpu_time(); + else /* to remove uninitialized variable warning */ + totalInitialTime = 0; + + if(traversalDirection == McFwd_c){ + mdd_t *totalInitialStates; + double nInitialStates; + + totalInitialStates = Fsm_FsmComputeInitialStates(totalFsm); + nInitialStates = mdd_count_onset(Fsm_FsmReadMddManager(totalFsm), + totalInitialStates, + Fsm_FsmReadPresentStateVars(totalFsm)); + mdd_free(totalInitialStates); + + /* If the number of initial states is only one, we can use both + * conversion formulas(init ^ f != FALSE and init ^ !f == FALSE), + * however, if we have multiple initial states, we should use + * p0 ^ !f == FALSE. + */ + ctlNormalFormulaArray = + Ctlp_FormulaArrayConvertToForward(ctlArray, (nInitialStates == 1.0), + noShare); + /* end conversion for forward traversal */ + } else if (noShare) { /* conversion for backward, no sharing */ + ctlNormalFormulaArray = + Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray); + }else{ /* conversion for backward, with sharing */ + /* Note that converting to DAG after converting to existential form would + lead to more sharing, but it cannot be done since equal subformula that + are converted from different formulae need different pointers back to + their originals */ + if (checkVacuity) { + ctlNormalFormulaArray = + Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray); + } + else { + array_t *temp = Ctlp_FormulaArrayConvertToDAG( ctlArray ); + array_free( ctlArray ); + ctlArray = temp; + ctlNormalFormulaArray = + Ctlp_FormulaDAGConvertToExistentialFormDAG(ctlArray); + } + } + /* At this point, ctlNormalFormulaArray contains the formulas that are + actually going to be checked, and ctlArray contains the formulas from + which the conversion has been done. Both need to be kept around until the + end, for debugging purposes. */ + + numFormulae = array_n(ctlNormalFormulaArray); + + /* time out */ + if (timeOutPeriod > 0) { + /* Set the static variables used by the signal handler. */ + mcTimeOut = timeOutPeriod; + alarmLapTime = util_cpu_ctime(); + (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); + (void) alarm(timeOutPeriod); + if (setjmp(timeOutEnv) > 0) { + (void) fprintf(vis_stdout, + "# MC: timeout occurred after %d seconds.\n", timeOutPeriod); + (void) fprintf(vis_stdout, "# MC: data may be corrupted.\n"); + if (verbosity > McVerbosityNone_c) { + fprintf(vis_stdout, "-- total %d image computations and %d preimage computations\n", + Img_GetNumberOfImageComputation(Img_Forward_c), + Img_GetNumberOfImageComputation(Img_Backward_c)); + } + alarm(0); + return 1; + } + } + + /* Create reduced fsm, if necessary */ + if (!McOptionsReadReduceFsm(options)){ + /* We want to minimize only when "-r" option is not specified */ + /* reduceFsm would be NIL, if there is no reduction observed */ + assert (reducedFsm == NIL(Fsm_Fsm_t)); + reducedFsm = McConstructReducedFsm(network, ctlNormalFormulaArray); + if (reducedFsm != NIL(Fsm_Fsm_t) && verbosity != McVerbosityNone_c) { + mddMgr = Fsm_FsmReadMddManager(reducedFsm); + bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr, + Fsm_FsmReadPresentStateVars(reducedFsm)); + (void)fprintf(vis_stdout,"Local system includes "); + (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n", + array_n(Fsm_FsmReadPresentStateVars(reducedFsm)), + array_n(bddIdArray)); + array_free(bddIdArray); + } + } + + /************** for all formulae **********************************/ + for(i = 0; i < numFormulae; i++) { + int nImgComps, nPreComps; + boolean result; + Ctlp_Formula_t *ctlFormula = array_fetch(Ctlp_Formula_t *, + ctlNormalFormulaArray, i); + + modelFsm = NIL(Fsm_Fsm_t); + + /* do a check */ + if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) { + (void) fprintf(vis_stdout, + "** mc error: error in parsing Atomic Formula:\n%s\n", + error_string()); + error_init(); + Ctlp_FormulaFree(ctlFormula); + continue; + } + + /* Create reduced fsm */ + if (McOptionsReadReduceFsm(options)) { + /* We have not done top level reduction. */ + /* Using the same variable reducedFsm here */ + array_t *oneFormulaArray = array_alloc(Ctlp_Formula_t *, 1); + + assert(reducedFsm == NIL(Fsm_Fsm_t)); + array_insert_last(Ctlp_Formula_t *, oneFormulaArray, ctlFormula); + reducedFsm = McConstructReducedFsm(network, oneFormulaArray); + array_free(oneFormulaArray); + + if (reducedFsm && verbosity != McVerbosityNone_c) { + mddMgr = Fsm_FsmReadMddManager(reducedFsm); + bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr, + Fsm_FsmReadPresentStateVars(reducedFsm)); + (void)fprintf(vis_stdout,"Local system includes "); + (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n", + array_n(Fsm_FsmReadPresentStateVars(reducedFsm)), + array_n(bddIdArray)); + array_free(bddIdArray); + } + }/* if readreducefsm */ + + /* Let us see if we got any reduction via top level or via "-r" */ + if (reducedFsm == NIL(Fsm_Fsm_t)) + modelFsm = totalFsm; /* no reduction */ + else + modelFsm = reducedFsm; /* some reduction at some point */ + + /* compute initial states */ + modelInitialStates = Fsm_FsmComputeInitialStates(modelFsm); + if (modelInitialStates == NIL(mdd_t)) { + int j; + (void) fprintf(vis_stdout, + "** mc error: Cannot build init states (mutual latch dependency?)\n%s\n", + error_string()); + if (modelFsm != totalFsm) + Fsm_FsmFree(reducedFsm); + + alarm(0); + + for(j = i; j < numFormulae; j++) + Ctlp_FormulaFree( + array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) ); + array_free( ctlNormalFormulaArray ); + + Ctlp_FormulaArrayFree( ctlArray ); + + McOptionsFree(options); + + return 1; + } + + earlyTermination = Mc_EarlyTerminationAlloc(McAll_c, modelInitialStates); + + if(hintsArray != NIL(Ctlp_FormulaArray_t)) { + hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray); + if( hintsStatesArray == NIL(array_t) || + (guidedSearchType == Mc_Global_c && + Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)) { + int j; + + if( guidedSearchType == Mc_Global_c && + Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c) + fprintf(vis_stderr, "** mc error: global hints incompatible with " + "mixed formulae\n"); + + Mc_EarlyTerminationFree(earlyTermination); + mdd_free(modelInitialStates); + if (modelFsm != totalFsm) + Fsm_FsmFree(reducedFsm); + alarm(0); + for(j = i; j < numFormulae; j++) + Ctlp_FormulaFree( + array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) ); + array_free( ctlNormalFormulaArray ); + Ctlp_FormulaArrayFree( ctlArray ); + McOptionsFree(options); + return 1; + } /* problem with hints */ + } /* hints exist */ + + /* stats */ + if (verbosity > McVerbosityNone_c) { + initialTime = util_cpu_time(); + nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); + nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c); + } else { /* to remove uninitialized variable warnings */ + initialTime = 0; + nImgComps = 0; + nPreComps = 0; + } + mddMgr = Fsm_FsmReadMddManager(modelFsm); + + /* compute don't cares. */ + if (modelCareStatesArray == NIL(array_t)) { + long iTime; /* starting time for reachability analysis */ + if (verbosity > McVerbosityNone_c && i == 0) + iTime = util_cpu_time(); + else /* to remove uninitialized variable warnings */ + iTime = 0; + + /* ardc */ + if (dcLevel == McDcLevelArdc_c) { + Fsm_ArdcOptions_t *ardcOptions = McOptionsReadArdcOptions(options); + + modelCareStatesArray = Fsm_ArdcComputeOverApproximateReachableStates( + modelFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions); + if (verbosity > McVerbosityNone_c && i == 0) + Fsm_ArdcPrintReachabilityResults(modelFsm, util_cpu_time() - iTime); + + /* rch dc */ + } else if (dcLevel >= McDcLevelRch_c) { + modelCareStates = + Fsm_FsmComputeReachableStates(modelFsm, 0, 1, 0, 0, 0, 0, 0, + Fsm_Rch_Default_c, 0, 0, + NIL(array_t), FALSE, NIL(array_t)); + if (verbosity > McVerbosityNone_c && i == 0) { + Fsm_FsmReachabilityPrintResults(modelFsm, util_cpu_time() - iTime, + Fsm_Rch_Default_c); + } + + modelCareStatesArray = array_alloc(mdd_t *, 0); + array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates); + } else { + modelCareStates = mdd_one(mddMgr); + modelCareStatesArray = array_alloc(mdd_t *, 0); + array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates); + } + } + + Fsm_MinimizeTransitionRelationWithReachabilityInfo( + modelFsm, (traversalDirection == McFwd_c) ? Img_Both_c : Img_Backward_c, + verbosity > 1); + + /* fairness conditions */ + fairStates = Fsm_FsmComputeFairStates(modelFsm, modelCareStatesArray, + verbosity, dcLevel, GSHschedule, + McBwd_c, FALSE); + fairCond = Fsm_FsmReadFairnessConstraint(modelFsm); + + if (mdd_lequal(modelInitialStates, fairStates, 1, 0)) { + (void)fprintf(vis_stdout, + "** mc warning: There are no fair initial states\n"); + } + else if (!mdd_lequal(modelInitialStates, fairStates, 1, 1)) { + (void)fprintf(vis_stdout, + "** mc warning: Some initial states are not fair\n"); + } + + /* some user feedback */ + if (verbosity != McVerbosityNone_c) { + (void)fprintf(vis_stdout, "Checking formula[%d] : ", i + 1); + Ctlp_FormulaPrint(vis_stdout, + Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void)fprintf (vis_stdout, "\n"); + if (traversalDirection == McFwd_c) { + (void)fprintf(vis_stdout, "Forward formula : "); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + (void)fprintf(vis_stdout, "\n"); + } + } + + /************** the actual computation **********************************/ + if (checkVacuity) { + McVacuityDetection(modelFsm, ctlFormula, i, + fairStates, fairCond, modelCareStatesArray, + earlyTermination, hintsStatesArray, + guidedSearchType, modelInitialStates, + options); + } + else { /* Normal Model Checking */ + mdd_t *ctlFormulaStates = + Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates, + fairCond, modelCareStatesArray, + earlyTermination, hintsStatesArray, + guidedSearchType, verbosity, dcLevel, + buildOnionRings, GSHschedule); + + McEstimateCoverage(modelFsm, ctlFormula, i, fairStates, fairCond, + modelCareStatesArray, earlyTermination, + hintsStatesArray, guidedSearchType, verbosity, + dcLevel, buildOnionRings, GSHschedule, + traversalDirection, modelInitialStates, + ctlFormulaStates, &totalcoveredstates, + signalTypeList, signalList, statesCoveredList, + newCoveredStatesList, statesToRemoveList, + performCoverageHoskote, performCoverageImproved); + + Mc_EarlyTerminationFree(earlyTermination); + if(hintsStatesArray != NIL(array_t)) + mdd_array_free(hintsStatesArray); + /* Set up things for possible FAFW analysis of counterexample. */ + Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag); + Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable); + /* user feedback on succes/fail */ + result = McPrintPassFail(mddMgr, modelFsm, traversalDirection, + ctlFormula, ctlFormulaStates, + modelInitialStates, modelCareStatesArray, + options, verbosity); + Fsm_FsmSetFAFWFlag(modelFsm, 0); + Fsm_FsmSetSystemVariableFAFW(modelFsm, NULL); + mdd_free(ctlFormulaStates); + } + + if (verbosity > McVerbosityNone_c) { + finalTime = util_cpu_time(); + fprintf(vis_stdout, "-- mc time = %10g\n", + (double)(finalTime - initialTime) / 1000.0); + fprintf(vis_stdout, + "-- %d image computations and %d preimage computations\n", + Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps, + Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps); + } + mdd_free(modelInitialStates); + mdd_free(fairStates); + Ctlp_FormulaFree(ctlFormula); + + if ((McOptionsReadReduceFsm(options)) && + (reducedFsm != NIL(Fsm_Fsm_t))) { + /* + ** We need to free the reducedFsm only if it was created under "-r" + ** option and was non-NIL. + */ + Fsm_FsmFree(reducedFsm); + reducedFsm = NIL(Fsm_Fsm_t); + modelFsm = NIL(Fsm_Fsm_t); + if (modelCareStates) { + mdd_array_free(modelCareStatesArray); + modelCareStates = NIL(mdd_t); + modelCareStatesArray = NIL(array_t); + } else if (modelCareStatesArray) { + modelCareStatesArray = NIL(array_t); + } + } + }/* for all formulae */ + + if (verbosity > McVerbosityNone_c) { + finalTime = util_cpu_time(); + fprintf(vis_stdout, "-- total mc time = %10g\n", + (double)(finalTime - totalInitialTime) / 1000.0); + fprintf(vis_stdout, + "-- total %d image computations and %d preimage computations\n", + Img_GetNumberOfImageComputation(Img_Forward_c), + Img_GetNumberOfImageComputation(Img_Backward_c)); + /* Print tfm options if we have a global fsm. */ + if (!McOptionsReadReduceFsm(options) && modelFsm != NIL(Fsm_Fsm_t)) { + imageInfo = Fsm_FsmReadImageInfo(modelFsm); + if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c || + Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) { + Img_TfmPrintStatistics(imageInfo, Img_Both_c); + } + } + } + + /* Print results of coverage computation */ + McPrintCoverageSummary(modelFsm, dcLevel, + options, modelCareStatesArray, + modelCareStates, totalcoveredstates, + signalTypeList, signalList, statesCoveredList, + performCoverageHoskote, performCoverageImproved); + mdd_array_free(newCoveredStatesList); + mdd_array_free(statesToRemoveList); + array_free(signalTypeList); + array_free(signalList); + mdd_array_free(statesCoveredList); + if (totalcoveredstates != NIL(mdd_t)) + mdd_free(totalcoveredstates); + + if (modelCareStates) { + mdd_array_free(modelCareStatesArray); + } + + if(hintsArray) + Ctlp_FormulaArrayFree(hintsArray); + + if ((McOptionsReadReduceFsm(options) == FALSE) && + (reducedFsm != NIL(Fsm_Fsm_t))) { + /* If "-r" was not specified and we did some reduction at top + level, we need to free it */ + Fsm_FsmFree(reducedFsm); + reducedFsm = NIL(Fsm_Fsm_t); + modelFsm = NIL(Fsm_Fsm_t); + } + + if(systemVarBddIdTable) + st_free_table(systemVarBddIdTable); + array_free(ctlNormalFormulaArray); + (void) fprintf(vis_stdout, "\n"); + + Ctlp_FormulaArrayFree(ctlArray); + McOptionsFree(options); + alarm(0); + return 0; +} Index: vis_dev/vis-2.3/models/transition/mc.txt =================================================================== --- vis_dev/vis-2.3/models/transition/mc.txt (revision 28) +++ vis_dev/vis-2.3/models/transition/mc.txt (revision 28) @@ -0,0 +1,998 @@ + +/**Function******************************************************************** + + Synopsis [Check CTL formulas given in file are modeled by flattened network] + + CommandName [model_check] + + CommandSynopsis [perform fair CTL model checking on a flattened network] + + CommandArguments [ \[-b\] \[-c\] \[-d <dbg_level>\] + \[-f <dbg_file>\] \[-g <hints_file>\] \[-h\] \[-i\] \[-m\] \[-r\] + \[-t <time_out_period>\]\[-v <verbosity_level>\] + \[-D <dc_level>\] \[-F\] \[-S <schedule>\] \[-V\] \[-B\] \[-I\] + \[-C\] \[-w <node_file>\] \[-W\] \[-G\] <ctl_file>] + + CommandDescription [Performs fair CTL model checking on a flattened + network. Before calling this command, the user should have + initialized the design by calling the command init_verify. + Regardless of the options, no 'false positives' or 'false negatives' + will occur: the result is correct for the given circuit.

+ + Properties to be verified should be provided as CTL formulas in the + file ctl_file. Note that the support of any wire + referred to in a formula should consist only of latches. For the + precise syntax of CTL formulas, see the VIS CTL and LTL syntax manual.

+ + Properties of the form AG f, where f is a formula not + involving path quantifiers are referred to as invariants; for such properties + it may be substantially faster to use the + check_invariant command. +

+ + A fairness constraint can be specified by invoking the + read_fairness command; + if none is specified, all paths are taken to be fair. + If some initial states + do not lie on a fair path, the model checker prints a message to this effect. +

+ + A formula passes iff it is true for all initial states of the + system. Therefore, in the presence of multiple initial states, if a + formula fails, the negation of the formula may also fail.

+ + If a formula does not pass, a (potentially partial) proof of failure + (referred to as a debug trace) is demonstrated. Fair paths are + represented by a finite sequence of states (the stem) leading to a + fair cycle, i.e. a cycle on which there is a state from each + fairness condition. The level of detail of the proof can be + specified (see option -d).

+ + Both backward (future tense CTL formulas) and forward (past tense CTL + formulas) model checking can be performed. Forward model checking is + based on Iwashita's ICCAD96 paper. Future tense CTL formulas are + automatically converted to past tense ones as much as possible in + forward model checking.

+ + Command options: +

+ +

+ +
-b +
Use backward analysis when performing debugging; the default is + to use forward analysis. This should be tried when the debugger spends a + large amount of time when creating a path to a fair cycle. This option is not + compatible with forward model checking option (-F).

+ +

-c +
Use the formula tree so that there is no sharing of sub-formulae among + the formulae in the input file. This option is useful in the following + scenario - formulae A, B and C are being checked in order and there is + sub-formula sharing between A and C. If the BDDs corresponding to the shared + sub-formula is huge then computation for B might not be able to finish + without using this option. +

+ +

-d <dbg_level>
Specify the amount of + debugging performed when the system fails a formula being checked. + Note that it may not always be possible to give a simple + counter-example to show that a formula is false, since this may + require enumerating all paths from a state. In such a case the + model checker will print a message to this effect. This option is + incompatible with -F.

+

dbg_level must be one of the following: + +

0: No debugging performed. + dbg_level=0 is the default. + +

1: Debugging with minimal output: generate counter-examples + for universal formulas (formulas of the form AX|AF|AU|AG) and + witnesses for existential formulas (formulas of the form + EX|EF|EU|EG). States on a path are not further analyzed. + +

2: Same as dbg_level=1, but more + verbose. (The subformulas are printed, too.) + +

3: Maximal automatic debugging: as for level 1, + except that states occurring on paths will be recursively analyzed. + +

4: Manual debugging: at each state, the user is queried if + more feedback is desired. +

+ +

+ +

-f <dbg_file> +
Write the debugger output to dbg_file. + This option is incompatible with -F. + Notes: when you use -d4 (interactive mode), -f is not recommended, since you + can't see the output of vis on stdout.
+ +
-g <hints_file>
Use guided search. The file + hints_file contains a series of hints. A hint is a formula that + does not contain any temporal operators, so hints_file has the + same syntax as a file of invariants used for check_invariant. The hints are + used in the order given to change the transition relation. In the case of + least fixpoints (EF, EU), the transition relation is conjoined with the hint, + whereas for greatest fixpoints the transition relation is disjoined with the + negation of the hint. If the hints are cleverly chosen, this may speed up + the computation considerably, because a search with the changed transition + relation may be much simpler than one with the original transition relation, + and results obtained can be reused, so that we may never have to do a + complicated search with the original relation. Note: hints in terms of + primary inputs are not useful for greatest fixpoints. See also: Ravi and + Somenzi, Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and + Somenzi, Efficient Decision Procedures for Model Checking of Linear Time + Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search + for CTL Model Checking, DAC'00. + +

For formulae that contain both least and greatest fixpoints, the + behavior depends on the flag guided_search_hint_type. + If it is set to local (default) then every subformula is evaluated + to completion, using all hints in order, before the next subformula + is started. For pure ACTL or pure ECTL formulae, we can also set + guided_search_hint_type to global, in which case the entire formula + is evaluated for one hint before moving on to the next hint, using + underapproximations. The description of the options for guided + search can be found in the help page for + print_guided_search_options. + +

model_check will call reachability without any guided search, even + if -g is used. If you want to perform reachability with guided + search, call rch directly. + +

Incompatible with -F.

+ +
-h +
Print the command usage.
+

+ +

-i +
Print input values causing transitions between states during debugging. + Both primary and pseudo inputs are printed. + This option is incompatible with -F.
+

+ +

-m +
Pipe debugger output through the UNIX utility more. + This option is incompatible with -F.
+

+ +

-r +
Reduce the FSM derived from the flattened network with respect to each + formula being checked. By default, the FSM is reduced with respect to the + conjunction of the formulae in the input file. If this option is used and + don't cares are being used for simplification, then subformula sharing is + disabled (result might be incorrect otherwise).
+

+ +

The truth of a formula may be independent of parts of the network + (such as when wires have been abstracted; see + flatten_hierarchy). + These parts are effectively removed when this option is invoked; this may + result in more efficient model checking.
+

+ +

-t <timeOutPeriod> +
Specify the time out period (in seconds) after which the command + aborts. By default this option is set to infinity.
+

+ +

-v <verbosity_level> +
Specify verbosity level. This sets the amount of feedback on CPU usage + and code status. + +
verbosity_level must be one of the following:

+ + 0: No feedback provided. This is the default.

+ + 1: Feedback on code location.

+ + 2: Feedback on code location and CPU usage.

+ +

-B +
Check for vacuously passing formulae using the algorithm of Beer et al. + (CAV97). The algorithm applies to a subset of ACTL (w-ACTL) and replaces + the smallest important subformula of a passing property with either FALSE + or TRUE depending on its negation parity. It then applies model checking + to the resulting witness formula. If the witness formula also passes, then + the original formula is deemed to pass vacuously. If the witness formula + fails, a counterexample to it provides an interesting witness to the + original passing formula. See the CAV97 paper for the definitions of + w-ACTL, important subformula, and interesting witness. In short, one of the + operands of a binary operator in a w-ACTL formula must be a propositional + formula. See also the -V option. +

+ +

-C +
Compute coverage of all observable signals in a set of CTL formulae + using the algorithm of Hoskote, Kam, Ho, Zhao (DAC'99). If the verbosity + level (-v option) is equal to 0, only the coverage stats are printed. If + verbosity level is greater than zero, then detailed information of the + computation at each step of the algorithm is also provided. + Debug information is provided in the form of states not covered for each + observable signal if the dbg_level (-d option) is greater than 0. The number + of states printed is set by the vis environment variable + 'nr_uncoveredstates'. By default the number of states printed is 1. + The value of nr_uncoveredstates can be set using the set command. + See also the -I option.
+

+ +

-D <dc_level> + +
Specify extent to which don't cares are used to simplify MDDs in model + checking. Don't cares are minterms on which the values taken by functions + do not affect the computation; potentially, these minterms can be used to + simplify MDDs and reduce the time taken to perform model checking. The -g + flag for guided search does not affect the way in which the don't-care + conditions are computed. + +
+ dc_level must be one of the following: +

+ + 0 : No don't cares are used. + +

1 : Use unreachable states as don't cares. This is the + default. + +

2 : Use unreachable states as don't cares and in the EU + computation, use 'frontiers' for image computation.

+ + 3 : First compute an overapproximation of the reachable states + (ARDC), and use that as the cares set. Use `frontiers' for image + computation. For help on controlling options for ARDC, look up help on the + command: print_ardc_options. Refer + to Moon, Jang, Somenzi, Pixley, Yuan, "Approximate Reachability Don't Cares + for {CTL} Model Checking", ICCAD98, and to two papers by Cho et al, IEEE TCAD + December 1996: one is for State Space Decomposition and the other is for + Approximate FSM Traversal.

+

+ +

-F +
Use forward model checking based on Iwashita's method in ICCAD96. + Future tense CTL formulas are automatically converted to past tense + ones as much as possible. Converted forward formulas are printed when + verbosity is greater than 0. Debug options (-b, -d, -f, -i, and -m) + are ignored with this option. We have seen that forward model checking + was much faster than backward in many cases, also forward was much slower + than backward in many cases.
+

+ +

-I +
Compute coverage of all observable signals in a set of CTL formulae + using an improved algorithm of Jayakumar, Purandare, Somenzi (DAC'03). If + the verbosity level (-v option) is equal to 0, only the coverage stats are + printed. If verbosity level is greater than zero, then detailed information + of the computation at each step of the algorithm is also provided. + Debug information is provided in the form of states not covered for each + observable signal if the dbg_level (-d option) is greater than 0. The number + of states printed is set by the vis environment variable + 'nr_uncoveredstates'. By default the number of states printed is 1. + The value of nr_uncoveredstates can be set using the set command. + Compared to the -C option, this one produces more accurate results and deals + with a larger subset of CTL.
+

+ +

-S <schedule> + +
Specify schedule for GSH algorithm, which generalizes the + Emerson-Lei algorithm and is used to compute greatest fixpoints. + The choice of schedule affects the sequence in which EX and EU + operators are applied. It makes a difference only when fairness + constraints are specified. + +
+ <schedule> must be one of the following: + +

EL : EU and EX operators strictly alternate. This + is the default. + +

EL1 : EX is applied once for every application of all EUs. + +

EL2 : EX is applied repeatedly after each application of + all EUs. + +

budget : a hybrid of EL and EL2. + +

random : enabled operators are applied in + (pseudo-)random order. + +

off : GSH is disabled, and the old algorithm is + used instead. The old algorithm uses the EL schedule, but + the termination checks are less sophisticated than in GSH.

+

+ +

-V +
Check for vacuously passing formulae with the algorithm + of Purandare and Somenzi (CAV2002). The algorithm applies to all of + CTL, and to both passing and failing properties. It says whether a + passing formula may be strengthened and still pass, and whether a + failing formula may be weakened and still fail. It considers all + leaves of a formula that are under one negation parity (e.g., not + descendants of a XOR or EQ node) for replacement by either TRUE or + FALSE. See also the -B option. +

+ + +

-w <node_file> + + This option invoked the algorithm to generate an error trace divided + into fated and free segements. Fate represents the inevitability and + free is asserted when there is no inevitability. This can be formulated + as a two-player concurrent reachability game. The two players are + the environment and the system. The node_file is given to specify the + variables the are controlled by the system. + +
-W
+ + This option represents the case that all input variables are controlled + by system. + +
-G
+ + We proposed two algorithm to generate segemented counter example. + They are general and restrcited algorithm. Bu default we use restricted + algorithm. We can invoke general algorithm with -G option. + + For more information, please check the STTT'04 + paper of Jin et al., "Fate and Free Will in Error Traces"

+ +

<ctl_file> + +
File containing CTL formulas to be model checked. +
+ + Related "set" options: +
+
ctl_change_bracket <yes/no> +
Vl2mv automatically converts "\[\]" to "<>" in node names, + therefore CTL parser does the same thing. However, in some cases a user + does not want to change node names in CTL parsing. Then, use this set + option by giving "no". Default is "yes". +

+

guided_search_hint_type
Switches between local and + global hints (see the -g option, or the help page for set). +
+ + See also commands : approximate_model_check, incremental_ctl_verification + ] + + Description [First argument is a file containing a set of CTL formulas - see + ctlp package for grammar. Second argument is an FSM that we will check the + formulas on. Formulas are checked by calling the recursive function + Mc_ModelCheckFormula. When the formula fails, the debugger is invoked.] + + Comment [Ctlp creates duplicate formulas when converting to + existential form; e.g. when converting AaUb. We aren't using this + fact, which leads to some performance degradation. + + A system satisfies a formula if all its initial states are in the satisfying + set of the formula. Hence, we do not need to continue the computation if we + know that all initial states are in the satisfying set, or if there are + initial states that we are sure are not in the satisfying set. This is what + early termination does: it supplies an extra termination condition for the + fixpoints that kicks in when we can decide the truth of the formula. Note + that this leads to some nasty consequences in storing the satisfying sets. + A computation that has terminated early does not yield the exact satisfying + set, and hence we can not always reuse this result when there is subformula + sharing.] + + SideEffects [] + + SeeAlso [CommandInv] + +******************************************************************************/ +static int +CommandMc( + Hrc_Manager_t **hmgr, + int argc, + char **argv) +{ + /* options */ + McOptions_t *options; + Mc_VerbosityLevel verbosity; + Mc_DcLevel dcLevel; + FILE *ctlFile; + int timeOutPeriod = 0; + Mc_FwdBwdAnalysis traversalDirection; + int buildOnionRings = 0; + FILE *guideFile; + FILE *systemFile; + Mc_GuidedSearch_t guidedSearchType = Mc_None_c; + Ctlp_FormulaArray_t *hintsArray = NIL(Fsm_HintsArray_t); + array_t *hintsStatesArray = NIL(array_t); /* array of mdd_t* */ + st_table *systemVarBddIdTable; + boolean noShare = 0; + Mc_GSHScheduleType GSHschedule; + boolean checkVacuity; + boolean performCoverageHoskote; + boolean performCoverageImproved; + + /* CTL formulae */ + array_t *ctlArray; + array_t *ctlNormalFormulaArray; + int i; + int numFormulae; + /* FSM, network and image */ + Fsm_Fsm_t *totalFsm = NIL(Fsm_Fsm_t); + Fsm_Fsm_t *modelFsm = NIL(Fsm_Fsm_t); + Fsm_Fsm_t *reducedFsm = NIL(Fsm_Fsm_t); + Ntk_Network_t *network; + mdd_t *modelCareStates = NIL(mdd_t); + array_t *modelCareStatesArray = NIL(array_t); + mdd_t *modelInitialStates; + mdd_t *fairStates; + Fsm_Fairness_t *fairCond; + mdd_manager *mddMgr; + array_t *bddIdArray; + Img_ImageInfo_t *imageInfo; + Mc_EarlyTermination_t *earlyTermination; + /* Coverage estimation */ + mdd_t *totalcoveredstates = NIL(mdd_t); + array_t *signalTypeList = array_alloc(int,0); + array_t *signalList = array_alloc(char *,0); + array_t *statesCoveredList = array_alloc(mdd_t *,0); + array_t *newCoveredStatesList = array_alloc(mdd_t *,0); + array_t *statesToRemoveList = array_alloc(mdd_t *,0); + + /* Early termination is only partially implemented right now. It needs + distribution over all operators, including limited cases of temporal + operators. That should be relatively easy to implement. */ + + /* time keeping */ + long totalInitialTime; /* for model checking */ + long initialTime, finalTime; /* for model checking */ + + error_init(); + Img_ResetNumberOfImageComputation(Img_Both_c); + + /* read options */ + if (!(options = ParseMcOptions(argc, argv))) { + return 1; + } + verbosity = McOptionsReadVerbosityLevel(options); + dcLevel = McOptionsReadDcLevel(options); + ctlFile = McOptionsReadCtlFile(options); + timeOutPeriod = McOptionsReadTimeOutPeriod(options); + traversalDirection = McOptionsReadTraversalDirection(options); + buildOnionRings = + (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity); + noShare = McOptionsReadUseFormulaTree(options); + GSHschedule = McOptionsReadSchedule(options); + checkVacuity = McOptionsReadVacuityDetect(options); + /* for the command mc -C foo.ctl */ + performCoverageHoskote = McOptionsReadCoverageHoskote(options); + /* for the command mc -I foo.ctl */ + performCoverageImproved = McOptionsReadCoverageImproved(options); + + /* Check for incompatible options and do some option-specific + * intializations. + */ + + if (traversalDirection == McFwd_c) { + if (checkVacuity) { + fprintf(vis_stderr, "** mc error: -V and -B are incompatible with -F\n"); + McOptionsFree(options); + return 1; + } + if (performCoverageHoskote || performCoverageImproved) { + fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -F\n"); + McOptionsFree(options); + return 1; + } + } + + if (checkVacuity) { + if (performCoverageHoskote || performCoverageImproved) { + fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -V and -B\n"); + McOptionsFree(options); + return 1; + } + } + + guideFile = McOptionsReadGuideFile(options); + + if(guideFile != NIL(FILE) ){ + guidedSearchType = Mc_ReadGuidedSearchType(); + if(guidedSearchType == Mc_None_c){ /* illegal setting */ + fprintf(vis_stderr, "** mc error: Unknown hint type\n"); + fclose(guideFile); + McOptionsFree(options); + return 1; + } + + if(traversalDirection == McFwd_c){ /* illegal combination */ + fprintf(vis_stderr, "** mc error: -g is incompatible with -F\n"); + fclose(guideFile); + McOptionsFree(options); + return 1; + } + + if(Img_UserSpecifiedMethod() != Img_Iwls95_c && + Img_UserSpecifiedMethod() != Img_Monolithic_c && + Img_UserSpecifiedMethod() != Img_Mlp_c){ + fprintf(vis_stderr, "** mc error: -g only works with iwls95, MLP, or monolithic image methods.\n"); + fclose(guideFile); + McOptionsFree(options); + return 1; + } + + hintsArray = Mc_ReadHints(guideFile); + fclose(guideFile); guideFile = NIL(FILE); + if( hintsArray == NIL(array_t) ){ + McOptionsFree(options); + return 1; + } + + } /* if guided search */ + + /* If don't-cares are used, -r implies -c. Note that the satisfying + sets of a subformula are only in terms of propositions therein + and their cone of influence. Hence, we can share satisfying sets + among formulae. I don't quite understand what the problem with + don't-cares is (RB) */ + if (McOptionsReadReduceFsm(options)) + if (dcLevel != McDcLevelNone_c) + McOptionsSetUseFormulaTree(options, TRUE); + + if (traversalDirection == McFwd_c && + McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { + McOptionsSetDbgLevel(options, McDbgLevelNone_c); + (void)fprintf(vis_stderr, "** mc warning : option -d is ignored.\n"); + } + + /* Read CTL formulae */ + ctlArray = Ctlsp_FileParseCTLFormulaArray(ctlFile); + fclose(ctlFile); ctlFile = NIL(FILE); + if (ctlArray == NIL(array_t)) { + (void) fprintf(vis_stderr, + "** mc error: error in parsing formulas from file\n"); + McOptionsFree(options); + return 1; + } + + /* read network */ + network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); + if (network == NIL(Ntk_Network_t)) { + fprintf(vis_stdout, "%s\n", error_string()); + error_init(); + Ctlp_FormulaArrayFree(ctlArray); + McOptionsFree(options); + return 1; + } + + /* read fsm */ + totalFsm = Fsm_NetworkReadOrCreateFsm(network); + if (totalFsm == NIL(Fsm_Fsm_t)) { + fprintf(vis_stdout, "%s\n", error_string()); + error_init(); + Ctlp_FormulaArrayFree(ctlArray); + McOptionsFree(options); + return 1; + } + + /* Assign variables to system if doing FAFW */ + systemVarBddIdTable = NIL(st_table); + systemFile = McOptionsReadSystemFile(options); + if (systemFile != NIL(FILE)) { + systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile); + fclose(systemFile); systemFile = NIL(FILE); + if (systemVarBddIdTable == (st_table *)-1 ) { /* FS: error message? */ + Ctlp_FormulaArrayFree(ctlArray); + McOptionsFree(options); + return 1; + } + } /* if FAFW */ + + if(options->FAFWFlag && systemVarBddIdTable == 0) { + systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm); + } + + if (verbosity > McVerbosityNone_c) + totalInitialTime = util_cpu_time(); + else /* to remove uninitialized variable warning */ + totalInitialTime = 0; + + if(traversalDirection == McFwd_c){ + mdd_t *totalInitialStates; + double nInitialStates; + + totalInitialStates = Fsm_FsmComputeInitialStates(totalFsm); + nInitialStates = mdd_count_onset(Fsm_FsmReadMddManager(totalFsm), + totalInitialStates, + Fsm_FsmReadPresentStateVars(totalFsm)); + mdd_free(totalInitialStates); + + /* If the number of initial states is only one, we can use both + * conversion formulas(init ^ f != FALSE and init ^ !f == FALSE), + * however, if we have multiple initial states, we should use + * p0 ^ !f == FALSE. + */ + ctlNormalFormulaArray = + Ctlp_FormulaArrayConvertToForward(ctlArray, (nInitialStates == 1.0), + noShare); + /* end conversion for forward traversal */ + } else if (noShare) { /* conversion for backward, no sharing */ + ctlNormalFormulaArray = + Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray); + }else{ /* conversion for backward, with sharing */ + /* Note that converting to DAG after converting to existential form would + lead to more sharing, but it cannot be done since equal subformula that + are converted from different formulae need different pointers back to + their originals */ + if (checkVacuity) { + ctlNormalFormulaArray = + Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray); + } + else { + array_t *temp = Ctlp_FormulaArrayConvertToDAG( ctlArray ); + array_free( ctlArray ); + ctlArray = temp; + ctlNormalFormulaArray = + Ctlp_FormulaDAGConvertToExistentialFormDAG(ctlArray); + } + } + /* At this point, ctlNormalFormulaArray contains the formulas that are + actually going to be checked, and ctlArray contains the formulas from + which the conversion has been done. Both need to be kept around until the + end, for debugging purposes. */ + + numFormulae = array_n(ctlNormalFormulaArray); + + /* time out */ + if (timeOutPeriod > 0) { + /* Set the static variables used by the signal handler. */ + mcTimeOut = timeOutPeriod; + alarmLapTime = util_cpu_ctime(); + (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); + (void) alarm(timeOutPeriod); + if (setjmp(timeOutEnv) > 0) { + (void) fprintf(vis_stdout, + "# MC: timeout occurred after %d seconds.\n", timeOutPeriod); + (void) fprintf(vis_stdout, "# MC: data may be corrupted.\n"); + if (verbosity > McVerbosityNone_c) { + fprintf(vis_stdout, "-- total %d image computations and %d preimage computations\n", + Img_GetNumberOfImageComputation(Img_Forward_c), + Img_GetNumberOfImageComputation(Img_Backward_c)); + } + alarm(0); + return 1; + } + } + + /* Create reduced fsm, if necessary */ + if (!McOptionsReadReduceFsm(options)){ + /* We want to minimize only when "-r" option is not specified */ + /* reduceFsm would be NIL, if there is no reduction observed */ + assert (reducedFsm == NIL(Fsm_Fsm_t)); + reducedFsm = McConstructReducedFsm(network, ctlNormalFormulaArray); + if (reducedFsm != NIL(Fsm_Fsm_t) && verbosity != McVerbosityNone_c) { + mddMgr = Fsm_FsmReadMddManager(reducedFsm); + bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr, + Fsm_FsmReadPresentStateVars(reducedFsm)); + (void)fprintf(vis_stdout,"Local system includes "); + (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n", + array_n(Fsm_FsmReadPresentStateVars(reducedFsm)), + array_n(bddIdArray)); + array_free(bddIdArray); + } + } + + /************** for all formulae **********************************/ + for(i = 0; i < numFormulae; i++) { + int nImgComps, nPreComps; + boolean result; + Ctlp_Formula_t *ctlFormula = array_fetch(Ctlp_Formula_t *, + ctlNormalFormulaArray, i); + + modelFsm = NIL(Fsm_Fsm_t); + + /* do a check */ + if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) { + (void) fprintf(vis_stdout, + "** mc error: error in parsing Atomic Formula:\n%s\n", + error_string()); + error_init(); + Ctlp_FormulaFree(ctlFormula); + continue; + } + + /* Create reduced fsm */ + if (McOptionsReadReduceFsm(options)) { + /* We have not done top level reduction. */ + /* Using the same variable reducedFsm here */ + array_t *oneFormulaArray = array_alloc(Ctlp_Formula_t *, 1); + + assert(reducedFsm == NIL(Fsm_Fsm_t)); + array_insert_last(Ctlp_Formula_t *, oneFormulaArray, ctlFormula); + reducedFsm = McConstructReducedFsm(network, oneFormulaArray); + array_free(oneFormulaArray); + + if (reducedFsm && verbosity != McVerbosityNone_c) { + mddMgr = Fsm_FsmReadMddManager(reducedFsm); + bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr, + Fsm_FsmReadPresentStateVars(reducedFsm)); + (void)fprintf(vis_stdout,"Local system includes "); + (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n", + array_n(Fsm_FsmReadPresentStateVars(reducedFsm)), + array_n(bddIdArray)); + array_free(bddIdArray); + } + }/* if readreducefsm */ + + /* Let us see if we got any reduction via top level or via "-r" */ + if (reducedFsm == NIL(Fsm_Fsm_t)) + modelFsm = totalFsm; /* no reduction */ + else + modelFsm = reducedFsm; /* some reduction at some point */ + + /* compute initial states */ + modelInitialStates = Fsm_FsmComputeInitialStates(modelFsm); + if (modelInitialStates == NIL(mdd_t)) { + int j; + (void) fprintf(vis_stdout, + "** mc error: Cannot build init states (mutual latch dependency?)\n%s\n", + error_string()); + if (modelFsm != totalFsm) + Fsm_FsmFree(reducedFsm); + + alarm(0); + + for(j = i; j < numFormulae; j++) + Ctlp_FormulaFree( + array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) ); + array_free( ctlNormalFormulaArray ); + + Ctlp_FormulaArrayFree( ctlArray ); + + McOptionsFree(options); + + return 1; + } + + earlyTermination = Mc_EarlyTerminationAlloc(McAll_c, modelInitialStates); + + if(hintsArray != NIL(Ctlp_FormulaArray_t)) { + hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray); + if( hintsStatesArray == NIL(array_t) || + (guidedSearchType == Mc_Global_c && + Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)) { + int j; + + if( guidedSearchType == Mc_Global_c && + Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c) + fprintf(vis_stderr, "** mc error: global hints incompatible with " + "mixed formulae\n"); + + Mc_EarlyTerminationFree(earlyTermination); + mdd_free(modelInitialStates); + if (modelFsm != totalFsm) + Fsm_FsmFree(reducedFsm); + alarm(0); + for(j = i; j < numFormulae; j++) + Ctlp_FormulaFree( + array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) ); + array_free( ctlNormalFormulaArray ); + Ctlp_FormulaArrayFree( ctlArray ); + McOptionsFree(options); + return 1; + } /* problem with hints */ + } /* hints exist */ + + /* stats */ + if (verbosity > McVerbosityNone_c) { + initialTime = util_cpu_time(); + nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); + nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c); + } else { /* to remove uninitialized variable warnings */ + initialTime = 0; + nImgComps = 0; + nPreComps = 0; + } + mddMgr = Fsm_FsmReadMddManager(modelFsm); + + /* compute don't cares. */ + if (modelCareStatesArray == NIL(array_t)) { + long iTime; /* starting time for reachability analysis */ + if (verbosity > McVerbosityNone_c && i == 0) + iTime = util_cpu_time(); + else /* to remove uninitialized variable warnings */ + iTime = 0; + + /* ardc */ + if (dcLevel == McDcLevelArdc_c) { + Fsm_ArdcOptions_t *ardcOptions = McOptionsReadArdcOptions(options); + + modelCareStatesArray = Fsm_ArdcComputeOverApproximateReachableStates( + modelFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions); + if (verbosity > McVerbosityNone_c && i == 0) + Fsm_ArdcPrintReachabilityResults(modelFsm, util_cpu_time() - iTime); + + /* rch dc */ + } else if (dcLevel >= McDcLevelRch_c) { + modelCareStates = + Fsm_FsmComputeReachableStates(modelFsm, 0, 1, 0, 0, 0, 0, 0, + Fsm_Rch_Default_c, 0, 0, + NIL(array_t), FALSE, NIL(array_t)); + if (verbosity > McVerbosityNone_c && i == 0) { + Fsm_FsmReachabilityPrintResults(modelFsm, util_cpu_time() - iTime, + Fsm_Rch_Default_c); + } + + modelCareStatesArray = array_alloc(mdd_t *, 0); + array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates); + } else { + modelCareStates = mdd_one(mddMgr); + modelCareStatesArray = array_alloc(mdd_t *, 0); + array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates); + } + } + + Fsm_MinimizeTransitionRelationWithReachabilityInfo( + modelFsm, (traversalDirection == McFwd_c) ? Img_Both_c : Img_Backward_c, + verbosity > 1); + + /* fairness conditions */ + fairStates = Fsm_FsmComputeFairStates(modelFsm, modelCareStatesArray, + verbosity, dcLevel, GSHschedule, + McBwd_c, FALSE); + fairCond = Fsm_FsmReadFairnessConstraint(modelFsm); + + if (mdd_lequal(modelInitialStates, fairStates, 1, 0)) { + (void)fprintf(vis_stdout, + "** mc warning: There are no fair initial states\n"); + } + else if (!mdd_lequal(modelInitialStates, fairStates, 1, 1)) { + (void)fprintf(vis_stdout, + "** mc warning: Some initial states are not fair\n"); + } + + /* some user feedback */ + if (verbosity != McVerbosityNone_c) { + (void)fprintf(vis_stdout, "Checking formula[%d] : ", i + 1); + Ctlp_FormulaPrint(vis_stdout, + Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void)fprintf (vis_stdout, "\n"); + if (traversalDirection == McFwd_c) { + (void)fprintf(vis_stdout, "Forward formula : "); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + (void)fprintf(vis_stdout, "\n"); + } + } + + /************** the actual computation **********************************/ + if (checkVacuity) { + McVacuityDetection(modelFsm, ctlFormula, i, + fairStates, fairCond, modelCareStatesArray, + earlyTermination, hintsStatesArray, + guidedSearchType, modelInitialStates, + options); + } + else { /* Normal Model Checking */ + mdd_t *ctlFormulaStates = + Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates, + fairCond, modelCareStatesArray, + earlyTermination, hintsStatesArray, + guidedSearchType, verbosity, dcLevel, + buildOnionRings, GSHschedule); + + McEstimateCoverage(modelFsm, ctlFormula, i, fairStates, fairCond, + modelCareStatesArray, earlyTermination, + hintsStatesArray, guidedSearchType, verbosity, + dcLevel, buildOnionRings, GSHschedule, + traversalDirection, modelInitialStates, + ctlFormulaStates, &totalcoveredstates, + signalTypeList, signalList, statesCoveredList, + newCoveredStatesList, statesToRemoveList, + performCoverageHoskote, performCoverageImproved); + + Mc_EarlyTerminationFree(earlyTermination); + if(hintsStatesArray != NIL(array_t)) + mdd_array_free(hintsStatesArray); + /* Set up things for possible FAFW analysis of counterexample. */ + Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag); + Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable); + /* user feedback on succes/fail */ + result = McPrintPassFail(mddMgr, modelFsm, traversalDirection, + ctlFormula, ctlFormulaStates, + modelInitialStates, modelCareStatesArray, + options, verbosity); + Fsm_FsmSetFAFWFlag(modelFsm, 0); + Fsm_FsmSetSystemVariableFAFW(modelFsm, NULL); + mdd_free(ctlFormulaStates); + } + + if (verbosity > McVerbosityNone_c) { + finalTime = util_cpu_time(); + fprintf(vis_stdout, "-- mc time = %10g\n", + (double)(finalTime - initialTime) / 1000.0); + fprintf(vis_stdout, + "-- %d image computations and %d preimage computations\n", + Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps, + Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps); + } + mdd_free(modelInitialStates); + mdd_free(fairStates); + Ctlp_FormulaFree(ctlFormula); + + if ((McOptionsReadReduceFsm(options)) && + (reducedFsm != NIL(Fsm_Fsm_t))) { + /* + ** We need to free the reducedFsm only if it was created under "-r" + ** option and was non-NIL. + */ + Fsm_FsmFree(reducedFsm); + reducedFsm = NIL(Fsm_Fsm_t); + modelFsm = NIL(Fsm_Fsm_t); + if (modelCareStates) { + mdd_array_free(modelCareStatesArray); + modelCareStates = NIL(mdd_t); + modelCareStatesArray = NIL(array_t); + } else if (modelCareStatesArray) { + modelCareStatesArray = NIL(array_t); + } + } + }/* for all formulae */ + + if (verbosity > McVerbosityNone_c) { + finalTime = util_cpu_time(); + fprintf(vis_stdout, "-- total mc time = %10g\n", + (double)(finalTime - totalInitialTime) / 1000.0); + fprintf(vis_stdout, + "-- total %d image computations and %d preimage computations\n", + Img_GetNumberOfImageComputation(Img_Forward_c), + Img_GetNumberOfImageComputation(Img_Backward_c)); + /* Print tfm options if we have a global fsm. */ + if (!McOptionsReadReduceFsm(options) && modelFsm != NIL(Fsm_Fsm_t)) { + imageInfo = Fsm_FsmReadImageInfo(modelFsm); + if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c || + Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) { + Img_TfmPrintStatistics(imageInfo, Img_Both_c); + } + } + } + + /* Print results of coverage computation */ + McPrintCoverageSummary(modelFsm, dcLevel, + options, modelCareStatesArray, + modelCareStates, totalcoveredstates, + signalTypeList, signalList, statesCoveredList, + performCoverageHoskote, performCoverageImproved); + mdd_array_free(newCoveredStatesList); + mdd_array_free(statesToRemoveList); + array_free(signalTypeList); + array_free(signalList); + mdd_array_free(statesCoveredList); + if (totalcoveredstates != NIL(mdd_t)) + mdd_free(totalcoveredstates); + + if (modelCareStates) { + mdd_array_free(modelCareStatesArray); + } + + if(hintsArray) + Ctlp_FormulaArrayFree(hintsArray); + + if ((McOptionsReadReduceFsm(options) == FALSE) && + (reducedFsm != NIL(Fsm_Fsm_t))) { + /* If "-r" was not specified and we did some reduction at top + level, we need to free it */ + Fsm_FsmFree(reducedFsm); + reducedFsm = NIL(Fsm_Fsm_t); + modelFsm = NIL(Fsm_Fsm_t); + } + + if(systemVarBddIdTable) + st_free_table(systemVarBddIdTable); + array_free(ctlNormalFormulaArray); + (void) fprintf(vis_stdout, "\n"); + + Ctlp_FormulaArrayFree(ctlArray); + McOptionsFree(options); + alarm(0); + return 0; +} Index: vis_dev/vis-2.3/models/transition/relation.bdd =================================================================== --- vis_dev/vis-2.3/models/transition/relation.bdd (revision 28) +++ vis_dev/vis-2.3/models/transition/relation.bdd (revision 28) @@ -0,0 +1,4 @@ +\define TRANS (state<0> = 1 * (state<0>$NS = 1 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 )))+ state<1> = 0 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 ))+ state<1>$NS = 0 * ( p$NS = 0 * (q$NS = 1 ))))+ state<0>$NS = 0 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * ( q$NS = 0)))))+ state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 )))+ state<1> = 0 * ( state<1>$NS = 0 * ( p$NS = 0 * (q$NS = 1 ))))+ state<0>$NS = 0 * (state<1>$NS = 1 * (p$NS = 1 * ( q$NS = 0))))) +\define REACH (state<0> = 1 * (state<1> = 1 * (p = 1 * (q = 1 ))+ state<1> = 0 * ( p = 0 * (q = 1 )))+ state<0> = 0 * (state<1> = 1 * (p = 1 * ( q = 0))+ state<1> = 0 * ( p = 0 * ( q = 0)))) +\define REL (state<0> = 1 + state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 + state<1> = 0 * (state<1>$NS = 1 + state<1>$NS = 0 * (p = 1 + p = 0 * (q = 1 ))))+ state<0>$NS = 0)) +\define new_rel (state<0> = 1 * (state<0>$NS = 1 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 )))+ state<1> = 0 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 ))+ state<1>$NS = 0 * ( p$NS = 0 * (q$NS = 1 ))))+ state<0>$NS = 0 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * ( q$NS = 0)))))+ state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 )))+ state<1> = 0 * ( state<1>$NS = 0 * (p = 1 * ( p$NS = 0 * (q$NS = 1 ))+ p = 0 * ( p$NS = 0 * (q = 1 * (q$NS = 1 ))))))+ state<0>$NS = 0 * (state<1>$NS = 1 * (p$NS = 1 * ( q$NS = 0))))) Index: vis_dev/vis-2.3/models/transition/script =================================================================== --- vis_dev/vis-2.3/models/transition/script (revision 28) +++ vis_dev/vis-2.3/models/transition/script (revision 28) @@ -0,0 +1,4 @@ +rlmv simple.mv +init +compute_reach -v 1 +transition Index: vis_dev/vis-2.3/models/transition/simple.mv =================================================================== --- vis_dev/vis-2.3/models/transition/simple.mv (revision 28) +++ vis_dev/vis-2.3/models/transition/simple.mv (revision 28) @@ -0,0 +1,435 @@ +# vl2mv simple.v +# version: 2.1 +# date: 14:23:27 12/01/2011 (CET) +.model concret +# I/O ports +.inputs i +# p = 0 +.names p$raw_n0 +0 +# q = 0 +.names q$raw_n1 +0 +# state [1 : 0] = 0 +.names state$raw_n2<0> +0 +.names state$raw_n2<1> +0 +# non-blocking assignments for initial +.names _n5<0> +0 +.names _n5<1> +0 +.names state<0> _n5<0> _n6<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n5<1> _n6<1> +.def 0 +0 1 1 +1 0 1 +.names _n6<0> _n6<1> _n7 +.def 1 +0 0 0 +.names _n7 _n4 +0 1 +1 0 +.names _n4 _n3 +.def 1 +0 0 +.names _n9 +1 +# i == 1 +.names i _n9 _na +.def 0 +0 1 1 +1 0 1 +.names _na _n8 +0 1 +1 0 +.names _n8 _nc +- =_n8 +# state [1 : 0] = 1 +.names state$_n8_nd$true<0> +1 +.names state$_n8_nd$true<1> +0 +# p = 0 +.names p$_n8_ne$true +0 +# q = 1 +.names q$_n8_nf$true +1 +# state [1 : 0] = 2 +.names state$_n8_n10$false<0> +0 +.names state$_n8_n10$false<1> +1 +# p = 1 +.names p$_n8_n11$false +1 +# q = 0 +.names q$_n8_n12$false +0 +# if/else (i == 1) +.names _n8 p$_n8_ne$true p$_n8_n11$false p$_n8$raw_n16 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n8 q$_n8_nf$true q$_n8_n12$false q$_n8$raw_n18 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n8 state$_n8_nd$true<0> state$_n8_n10$false<0> state$_n8$raw_n1a<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n8 state$_n8_nd$true<1> state$_n8_n10$false<1> state$_n8$raw_n1a<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n25<0> +1 +.names _n25<1> +0 +.names state<0> _n25<0> _n26<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n25<1> _n26<1> +.def 0 +0 1 1 +1 0 1 +.names _n26<0> _n26<1> _n27 +.def 1 +0 0 0 +.names _n27 _n24 +0 1 +1 0 +.names _n24 _n23 +.def 1 +0 0 +.names _n29 +1 +# i == 1 +.names i _n29 _n2a +.def 0 +0 1 1 +1 0 1 +.names _n2a _n28 +0 1 +1 0 +.names _n28 _n2c +- =_n28 +# state [1 : 0] = 1 +.names state$_n28_n2d$true<0> +1 +.names state$_n28_n2d$true<1> +0 +# p = 0 +.names p$_n28_n2e$true +0 +# q = 1 +.names q$_n28_n2f$true +1 +# state [1 : 0] = 3 +.names state$_n28_n30$false<0> +1 +.names state$_n28_n30$false<1> +1 +# p = 1 +.names p$_n28_n31$false +1 +# q = 1 +.names q$_n28_n32$false +1 +# if/else (i == 1) +.names _n28 p$_n28_n2e$true p$_n28_n31$false p$_n28$raw_n36 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n28 q$_n28_n2f$true q$_n28_n32$false q$_n28$raw_n38 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n28 state$_n28_n2d$true<0> state$_n28_n30$false<0> state$_n28$raw_n3a<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n28 state$_n28_n2d$true<1> state$_n28_n30$false<1> state$_n28$raw_n3a<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n45<0> +0 +.names _n45<1> +1 +.names state<0> _n45<0> _n46<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n45<1> _n46<1> +.def 0 +0 1 1 +1 0 1 +.names _n46<0> _n46<1> _n47 +.def 1 +0 0 0 +.names _n47 _n44 +0 1 +1 0 +.names _n44 _n43 +.def 1 +0 0 +.names _n49 +1 +# i == 1 +.names i _n49 _n4a +.def 0 +0 1 1 +1 0 1 +.names _n4a _n48 +0 1 +1 0 +.names _n48 _n4c +- =_n48 +# state [1 : 0] = 2 +.names state$_n48_n4d$true<0> +0 +.names state$_n48_n4d$true<1> +1 +# p = 1 +.names p$_n48_n4e$true +1 +# q = 0 +.names q$_n48_n4f$true +0 +# state [1 : 0] = 3 +.names state$_n48_n50$false<0> +1 +.names state$_n48_n50$false<1> +1 +# p = 1 +.names p$_n48_n51$false +1 +# q = 1 +.names q$_n48_n52$false +1 +# if/else (i == 1) +.names _n48 p$_n48_n4e$true p$_n48_n51$false p$_n48$raw_n56 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n48 q$_n48_n4f$true q$_n48_n52$false q$_n48$raw_n58 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n48 state$_n48_n4d$true<0> state$_n48_n50$false<0> state$_n48$raw_n5a<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n48 state$_n48_n4d$true<1> state$_n48_n50$false<1> state$_n48$raw_n5a<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n65<0> +1 +.names _n65<1> +1 +.names state<0> _n65<0> _n66<0> +.def 0 +0 1 1 +1 0 1 +.names state<1> _n65<1> _n66<1> +.def 0 +0 1 1 +1 0 1 +.names _n66<0> _n66<1> _n67 +.def 1 +0 0 0 +.names _n67 _n64 +0 1 +1 0 +.names _n64 _n63 +.def 1 +0 0 +.names _n69 +1 +# i == 1 +.names i _n69 _n6a +.def 0 +0 1 1 +1 0 1 +.names _n6a _n68 +0 1 +1 0 +.names _n68 _n6c +- =_n68 +# state [1 : 0] = 2 +.names state$_n68_n6d$true<0> +0 +.names state$_n68_n6d$true<1> +1 +# p = 1 +.names p$_n68_n6e$true +1 +# q = 0 +.names q$_n68_n6f$true +0 +# state [1 : 0] = 3 +.names state$_n68_n70$false<0> +1 +.names state$_n68_n70$false<1> +1 +# p = 1 +.names p$_n68_n71$false +1 +# q = 1 +.names q$_n68_n72$false +1 +# if/else (i == 1) +.names _n68 p$_n68_n6e$true p$_n68_n71$false p$_n68$raw_n76 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n68 q$_n68_n6f$true q$_n68_n72$false q$_n68$raw_n78 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n68 state$_n68_n6d$true<0> state$_n68_n70$false<0> state$_n68$raw_n7a<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n68 state$_n68_n6d$true<1> state$_n68_n70$false<1> state$_n68$raw_n7a<1> +.def 0 +1 1 - 1 +0 - 1 1 +# case (state ) +.names _n63 p$_n68$raw_n76 p p$_n63$raw_n89 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n63 q$_n68$raw_n78 q q$_n63$raw_n8b +.def 0 +1 1 - 1 +0 - 1 1 +.names _n63 state$_n68$raw_n7a<0> state<0> state$_n63$raw_n8d<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n63 state$_n68$raw_n7a<1> state<1> state$_n63$raw_n8d<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n43 p$_n48$raw_n56 p$_n63$raw_n89 p$_n43$raw_n90 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n43 q$_n48$raw_n58 q$_n63$raw_n8b q$_n43$raw_n92 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n43 state$_n48$raw_n5a<0> state$_n63$raw_n8d<0> state$_n43$raw_n94<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n43 state$_n48$raw_n5a<1> state$_n63$raw_n8d<1> state$_n43$raw_n94<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n23 p$_n28$raw_n36 p$_n43$raw_n90 p$_n23$raw_na0 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n23 q$_n28$raw_n38 q$_n43$raw_n92 q$_n23$raw_na2 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n23 state$_n28$raw_n3a<0> state$_n43$raw_n94<0> state$_n23$raw_na4<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n23 state$_n28$raw_n3a<1> state$_n43$raw_n94<1> state$_n23$raw_na4<1> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3 p$_n8$raw_n16 p$_n23$raw_na0 p$_n3$raw_nb0 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3 q$_n8$raw_n18 q$_n23$raw_na2 q$_n3$raw_nb2 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3 state$_n8$raw_n1a<0> state$_n23$raw_na4<0> state$_n3$raw_nb4<0> +.def 0 +1 1 - 1 +0 - 1 1 +.names _n3 state$_n8$raw_n1a<1> state$_n23$raw_na4<1> state$_n3$raw_nb4<1> +.def 0 +1 1 - 1 +0 - 1 1 +# conflict arbitrators +.names _n3 _nc _n23 _n2c _n43 _n4c _n63 _n6c _nc0 +.def 0 + 1 1 - - - - - - 1 + 1 0 - - - - - - 1 + 0 - 1 1 - - - - 1 + 0 - 1 0 - - - - 1 + 0 - 0 - 1 1 - - 1 + 0 - 0 - 1 0 - - 1 + 0 - 0 - 0 - 1 1 1 + 0 - 0 - 0 - 1 0 1 +.names _nc0 p$_n3$raw_nb0 p _nc1 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.names _n3 _nc _n23 _n2c _n43 _n4c _n63 _n6c _nc2 +.def 0 + 1 1 - - - - - - 1 + 1 0 - - - - - - 1 + 0 - 1 1 - - - - 1 + 0 - 1 0 - - - - 1 + 0 - 0 - 1 1 - - 1 + 0 - 0 - 1 0 - - 1 + 0 - 0 - 0 - 1 1 1 + 0 - 0 - 0 - 1 0 1 +.names _nc2 q$_n3$raw_nb2 q _nc3 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.names _n3 _nc _n23 _n2c _n43 _n4c _n63 _n6c _nc4 +.def 0 + 1 1 - - - - - - 1 + 1 0 - - - - - - 1 + 0 - 1 1 - - - - 1 + 0 - 1 0 - - - - 1 + 0 - 0 - 1 1 - - 1 + 0 - 0 - 1 0 - - 1 + 0 - 0 - 0 - 1 1 1 + 0 - 0 - 0 - 1 0 1 +.names _nc4 state$_n3$raw_nb4<0> state$_n3$raw_nb4<1> state<0> state<1> -> _nc5<0> _nc5<1> +1 - - - - =state$_n3$raw_nb4<0> =state$_n3$raw_nb4<1> +0 - - - - =state<0> =state<1> +# non-blocking assignments +# latches +.r p$raw_n0 p +0 0 +1 1 +.latch _nc1 p +.r q$raw_n1 q +0 0 +1 1 +.latch _nc3 q +.r state$raw_n2<0> state<0> +.def 0 +1 1 +.r state$raw_n2<1> state<1> +.def 0 +1 1 +.latch _nc5<0> state<0> +.latch _nc5<1> state<1> +# quasi-continuous assignment +.end Index: vis_dev/vis-2.3/models/transition/simple.v =================================================================== --- vis_dev/vis-2.3/models/transition/simple.v (revision 28) +++ vis_dev/vis-2.3/models/transition/simple.v (revision 28) @@ -0,0 +1,76 @@ +//typedef enum {ZERO,UN,DEUX} state_t; + +module concret(clk,i); +input clk; + +reg p; +reg q; +input i; +reg[1:0] state; + +initial +begin +p = 0; +q = 0; +state[1:0] = 0; +end + +always @(posedge clk) +begin +case(state) + 0 : + if(i == 1) + begin + state[1:0] = 1; + p = 0; + q = 1; + end + else + begin + state[1:0] = 2; + p = 1; + q = 0; + end + 1 : if(i == 1) + begin + state[1:0] = 1; + p = 0; + q = 1; + end + else + begin + state[1:0] = 3; + p = 1; + q = 1; + end + 2 : if(i == 1) + begin + state[1:0] = 2; + p = 1; + q = 0; + end + else + begin + state[1:0] = 3; + p = 1; + q = 1; + end + 3 : if(i == 1) + begin + state[1:0] = 2; + p = 1; + q = 0; + end + else + begin + state[1:0] = 3; + p = 1; + q = 1; + end + +endcase + +end + + +endmodule Index: vis_dev/vis-2.3/models/transition/testons.mv =================================================================== --- vis_dev/vis-2.3/models/transition/testons.mv (revision 28) +++ vis_dev/vis-2.3/models/transition/testons.mv (revision 28) @@ -0,0 +1,391 @@ +.model concret +.root concret +.inputs i +.latch _nc5<0> state<0> +.reset state$raw_n2<0> ->state<0> +.default 0 +1 1 +.latch _nc1 p +.reset p$raw_n0 ->p +0 0 +1 1 +.latch _nc3 q +.reset q$raw_n1 ->q +0 0 +1 1 +.latch _nc5<1> state<1> +.reset state$raw_n2<1> ->state<1> +.default 0 +1 1 +.table ->p$raw_n0 +0 +.table ->q$raw_n1 +0 +.table ->state$raw_n2<0> +0 +.table ->state$raw_n2<1> +0 +.table ->_n5<0> +0 +.table ->_n5<1> +0 +.table state<0> _n5<0> ->_n6<0> +.default 0 +0 1 1 +1 0 1 +.table state<1> _n5<1> ->_n6<1> +.default 0 +0 1 1 +1 0 1 +.table _n6<0> _n6<1> ->_n7 +.default 1 +0 0 0 +.table _n7 ->_n4 +0 1 +1 0 +.table _n4 ->_n3 +.default 1 +0 0 +.table ->_n9 +1 +.table i _n9 ->_na +.default 0 +0 1 1 +1 0 1 +.table _na ->_n8 +0 1 +1 0 +.table _n8 ->_nc +- =_n8 +.table ->state$_n8_nd$true<0> +1 +.table ->state$_n8_nd$true<1> +0 +.table ->p$_n8_ne$true +0 +.table ->q$_n8_nf$true +1 +.table ->state$_n8_n10$false<0> +0 +.table ->state$_n8_n10$false<1> +1 +.table ->p$_n8_n11$false +1 +.table ->q$_n8_n12$false +0 +.table _n8 p$_n8_ne$true p$_n8_n11$false ->p$_n8$raw_n16 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n8 q$_n8_nf$true q$_n8_n12$false ->q$_n8$raw_n18 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n8 state$_n8_nd$true<0> state$_n8_n10$false<0> ->state$_n8$raw_n1a<0> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n8 state$_n8_nd$true<1> state$_n8_n10$false<1> ->state$_n8$raw_n1a<1> +.default 0 +1 1 - 1 +0 - 1 1 +.table ->_n25<0> +1 +.table ->_n25<1> +0 +.table state<0> _n25<0> ->_n26<0> +.default 0 +0 1 1 +1 0 1 +.table state<1> _n25<1> ->_n26<1> +.default 0 +0 1 1 +1 0 1 +.table _n26<0> _n26<1> ->_n27 +.default 1 +0 0 0 +.table _n27 ->_n24 +0 1 +1 0 +.table _n24 ->_n23 +.default 1 +0 0 +.table ->_n29 +1 +.table i _n29 ->_n2a +.default 0 +0 1 1 +1 0 1 +.table _n2a ->_n28 +0 1 +1 0 +.table _n28 ->_n2c +- =_n28 +.table ->state$_n28_n2d$true<0> +1 +.table ->state$_n28_n2d$true<1> +0 +.table ->p$_n28_n2e$true +0 +.table ->q$_n28_n2f$true +1 +.table ->state$_n28_n30$false<0> +1 +.table ->state$_n28_n30$false<1> +1 +.table ->p$_n28_n31$false +1 +.table ->q$_n28_n32$false +1 +.table _n28 p$_n28_n2e$true p$_n28_n31$false ->p$_n28$raw_n36 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n28 q$_n28_n2f$true q$_n28_n32$false ->q$_n28$raw_n38 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n28 state$_n28_n2d$true<0> state$_n28_n30$false<0> ->state$_n28$raw_n3a<0> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n28 state$_n28_n2d$true<1> state$_n28_n30$false<1> ->state$_n28$raw_n3a<1> +.default 0 +1 1 - 1 +0 - 1 1 +.table ->_n45<0> +0 +.table ->_n45<1> +1 +.table state<0> _n45<0> ->_n46<0> +.default 0 +0 1 1 +1 0 1 +.table state<1> _n45<1> ->_n46<1> +.default 0 +0 1 1 +1 0 1 +.table _n46<0> _n46<1> ->_n47 +.default 1 +0 0 0 +.table _n47 ->_n44 +0 1 +1 0 +.table _n44 ->_n43 +.default 1 +0 0 +.table ->_n49 +1 +.table i _n49 ->_n4a +.default 0 +0 1 1 +1 0 1 +.table _n4a ->_n48 +0 1 +1 0 +.table _n48 ->_n4c +- =_n48 +.table ->state$_n48_n4d$true<0> +0 +.table ->state$_n48_n4d$true<1> +1 +.table ->p$_n48_n4e$true +1 +.table ->q$_n48_n4f$true +0 +.table ->state$_n48_n50$false<0> +1 +.table ->state$_n48_n50$false<1> +1 +.table ->p$_n48_n51$false +1 +.table ->q$_n48_n52$false +1 +.table _n48 p$_n48_n4e$true p$_n48_n51$false ->p$_n48$raw_n56 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n48 q$_n48_n4f$true q$_n48_n52$false ->q$_n48$raw_n58 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n48 state$_n48_n4d$true<0> state$_n48_n50$false<0> ->state$_n48$raw_n5a<0> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n48 state$_n48_n4d$true<1> state$_n48_n50$false<1> ->state$_n48$raw_n5a<1> +.default 0 +1 1 - 1 +0 - 1 1 +.table ->_n65<0> +1 +.table ->_n65<1> +1 +.table state<0> _n65<0> ->_n66<0> +.default 0 +0 1 1 +1 0 1 +.table state<1> _n65<1> ->_n66<1> +.default 0 +0 1 1 +1 0 1 +.table _n66<0> _n66<1> ->_n67 +.default 1 +0 0 0 +.table _n67 ->_n64 +0 1 +1 0 +.table _n64 ->_n63 +.default 1 +0 0 +.table ->_n69 +1 +.table i _n69 ->_n6a +.default 0 +0 1 1 +1 0 1 +.table _n6a ->_n68 +0 1 +1 0 +.table _n68 ->_n6c +- =_n68 +.table ->state$_n68_n6d$true<0> +0 +.table ->state$_n68_n6d$true<1> +1 +.table ->p$_n68_n6e$true +1 +.table ->q$_n68_n6f$true +0 +.table ->state$_n68_n70$false<0> +1 +.table ->state$_n68_n70$false<1> +1 +.table ->p$_n68_n71$false +1 +.table ->q$_n68_n72$false +1 +.table _n68 p$_n68_n6e$true p$_n68_n71$false ->p$_n68$raw_n76 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n68 q$_n68_n6f$true q$_n68_n72$false ->q$_n68$raw_n78 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n68 state$_n68_n6d$true<0> state$_n68_n70$false<0> ->state$_n68$raw_n7a<0> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n68 state$_n68_n6d$true<1> state$_n68_n70$false<1> ->state$_n68$raw_n7a<1> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n63 p$_n68$raw_n76 p ->p$_n63$raw_n89 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n63 q$_n68$raw_n78 q ->q$_n63$raw_n8b +.default 0 +1 1 - 1 +0 - 1 1 +.table _n63 state$_n68$raw_n7a<0> state<0> ->state$_n63$raw_n8d<0> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n63 state$_n68$raw_n7a<1> state<1> ->state$_n63$raw_n8d<1> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n43 p$_n48$raw_n56 p$_n63$raw_n89 ->p$_n43$raw_n90 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n43 q$_n48$raw_n58 q$_n63$raw_n8b ->q$_n43$raw_n92 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n43 state$_n48$raw_n5a<0> state$_n63$raw_n8d<0> ->state$_n43$raw_n94<0> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n43 state$_n48$raw_n5a<1> state$_n63$raw_n8d<1> ->state$_n43$raw_n94<1> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n23 p$_n28$raw_n36 p$_n43$raw_n90 ->p$_n23$raw_na0 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n23 q$_n28$raw_n38 q$_n43$raw_n92 ->q$_n23$raw_na2 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n23 state$_n28$raw_n3a<0> state$_n43$raw_n94<0> ->state$_n23$raw_na4<0> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n23 state$_n28$raw_n3a<1> state$_n43$raw_n94<1> ->state$_n23$raw_na4<1> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n3 p$_n8$raw_n16 p$_n23$raw_na0 ->p$_n3$raw_nb0 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n3 q$_n8$raw_n18 q$_n23$raw_na2 ->q$_n3$raw_nb2 +.default 0 +1 1 - 1 +0 - 1 1 +.table _n3 state$_n8$raw_n1a<0> state$_n23$raw_na4<0> ->state$_n3$raw_nb4<0> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n3 state$_n8$raw_n1a<1> state$_n23$raw_na4<1> ->state$_n3$raw_nb4<1> +.default 0 +1 1 - 1 +0 - 1 1 +.table _n3 _nc _n23 _n2c _n43 _n4c _n63 _n6c ->_nc0 +.default 0 +1 1 - - - - - - 1 +1 0 - - - - - - 1 +0 - 1 1 - - - - 1 +0 - 1 0 - - - - 1 +0 - 0 - 1 1 - - 1 +0 - 0 - 1 0 - - 1 +0 - 0 - 0 - 1 1 1 +0 - 0 - 0 - 1 0 1 +.table _nc0 p$_n3$raw_nb0 p ->_nc1 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.table _n3 _nc _n23 _n2c _n43 _n4c _n63 _n6c ->_nc2 +.default 0 +1 1 - - - - - - 1 +1 0 - - - - - - 1 +0 - 1 1 - - - - 1 +0 - 1 0 - - - - 1 +0 - 0 - 1 1 - - 1 +0 - 0 - 1 0 - - 1 +0 - 0 - 0 - 1 1 1 +0 - 0 - 0 - 1 0 1 +.table _nc2 q$_n3$raw_nb2 q ->_nc3 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.table _n3 _nc _n23 _n2c _n43 _n4c _n63 _n6c ->_nc4 +.default 0 +1 1 - - - - - - 1 +1 0 - - - - - - 1 +0 - 1 1 - - - - 1 +0 - 1 0 - - - - 1 +0 - 0 - 1 1 - - 1 +0 - 0 - 1 0 - - 1 +0 - 0 - 0 - 1 1 1 +0 - 0 - 0 - 1 0 1 +.table _nc4 state$_n3$raw_nb4<0> state$_n3$raw_nb4<1> state<0> state<1> ->_nc5<0> _nc5<1> +1 - - - - =state$_n3$raw_nb4<0> =state$_n3$raw_nb4<1> +0 - - - - =state<0> =state<1> +.end