# /home/sharma/vl2mv/i586/bin/vl2mv 4-arbit.v # version: 0.2 # date: 20:34:06 07/21/96 (CDT) .model main # I/O ports .mv constFALSE 2 myTRUE myFALSE .mv sa 2 myTRUE myFALSE .mv ur1 4 idle request lock release .mv xa 2 myTRUE myFALSE .mv ur2 4 idle request lock release .mv yr 4 idle request lock release .mv ur3 4 idle request lock release .mv ua1 2 myTRUE myFALSE .mv ur4 4 idle request lock release .mv ua2 2 myTRUE myFALSE .mv sr 4 idle request lock release .mv ua3 2 myTRUE myFALSE .mv ua4 2 myTRUE myFALSE .mv xr 4 idle request lock release .mv ya 2 myTRUE myFALSE .mv constTRUE 2 myTRUE myFALSE # assign constTRUE = 0 .mv constTRUE$raw_n0 2 myTRUE myFALSE .names constTRUE$raw_n0 myTRUE # assign constFALSE = 1 .mv constFALSE$raw_n1 2 myTRUE myFALSE .names constFALSE$raw_n1 myFALSE # assign sa = constFALSE .mv sa$raw_n2 2 myTRUE myFALSE .names constFALSE sa$raw_n2 - =constFALSE .subckt arbitCell C0 topCell=constTRUE urLeft=xr urRight=yr uaLeft=xa uaRight=ya xr=sr xa=sa .subckt arbitCell C1 topCell=constFALSE urLeft=ur1 urRight=ur2 uaLeft=ua1 uaRight=ua2 xr=xr xa=xa .subckt arbitCell C2 topCell=constFALSE urLeft=ur3 urRight=ur4 uaLeft=ua3 uaRight=ua4 xr=yr xa=ya .subckt procModel P1 ack=ua1 req=ur1 .subckt procModel P2 ack=ua2 req=ur2 .subckt procModel P3 ack=ua3 req=ur3 .subckt procModel P4 ack=ua4 req=ur4 # conflict arbitrators .names constFALSE$raw_n1 constFALSE - =constFALSE$raw_n1 .names sa$raw_n2 sa - =sa$raw_n2 .names constTRUE$raw_n0 constTRUE - =constTRUE$raw_n0 # non-blocking assignments # latches # quasi-continuous assignment .end .model arbitCell # I/O ports .outputs uaLeft .inputs topCell .inputs xa .inputs urRight .inputs urLeft .outputs xr .outputs uaRight .mv processedLeft 2 myTRUE myFALSE .mv prevLeft 2 myTRUE myFALSE .mv holdToken 2 myTRUE myFALSE .mv processedRight 2 myTRUE myFALSE .mv uaLeft 2 myTRUE myFALSE .mv topCell 2 myTRUE myFALSE .mv xa 2 myTRUE myFALSE .mv urRight 4 idle request lock release .mv giveChild 2 myTRUE myFALSE .mv urLeft 4 idle request lock release .mv mustGiveParent 2 myTRUE myFALSE .mv xr 4 idle request lock release .mv uaRight 2 myTRUE myFALSE .mv childOwns 2 myTRUE myFALSE .mv prevRight 2 myTRUE myFALSE # prevLeft = 1 .mv prevLeft$raw_n3 2 myTRUE myFALSE .names prevLeft$raw_n3 myFALSE # non-blocking assignments for initial # prevRight = 0 .mv prevRight$raw_n4 2 myTRUE myFALSE .names prevRight$raw_n4 myTRUE # non-blocking assignments for initial # processedLeft = 1 .mv processedLeft$raw_n5 2 myTRUE myFALSE .names processedLeft$raw_n5 myFALSE # non-blocking assignments for initial # processedRight = 1 .mv processedRight$raw_n6 2 myTRUE myFALSE .names processedRight$raw_n6 myFALSE # non-blocking assignments for initial # assign mustGiveParent = (processedLeft == 0) && (processedRight == 0) && (!(topCell == 0)) ? 0 : 1 .mv mustGiveParent$raw_n7 2 myTRUE myFALSE .mv _n9 2 myTRUE myFALSE .names _n9 myTRUE # processedLeft == 0 .names processedLeft _n9 _n8 .def 0 - =processedLeft 1 .mv _nb 2 myTRUE myFALSE .names _nb myTRUE # processedRight == 0 .names processedRight _nb _na .def 0 - =processedRight 1 # (processedLeft == 0) && (processedRight == 0) .names _n8 _na _nc .def 0 1 1 1 .mv _ne 2 myTRUE myFALSE .names _ne myTRUE # topCell == 0 .names topCell _ne _nd .def 0 - =topCell 1 .names _nd _nf 0 1 1 0 # (processedLeft == 0) && (processedRight == 0) && (!(topCell == 0)) .names _nc _nf _n10 .def 0 1 1 1 .mv _n11 2 myTRUE myFALSE .names _n11 myTRUE .mv _n12 2 myTRUE myFALSE .names _n12 myFALSE # (processedLeft == 0) && (processedRight == 0) && (!(topCell == 0)) ? 0 : 1 .mv _n13 2 myTRUE myFALSE .names _n11 _n12 _n10 _n13 - - 0 =_n12 - - 1 =_n11 .names _n13 mustGiveParent$raw_n7 - =_n13 # holdToken = topCell .mv holdToken$raw_n14 2 myTRUE myFALSE .names topCell holdToken$raw_n14 - =topCell # non-blocking assignments for initial # assign childOwns = (urLeft == lock || urRight == lock ) ? 0 : 1 .mv childOwns$raw_n15 2 myTRUE myFALSE .mv _n17 4 idle request lock release .names _n17 lock # urLeft == 2 .names urLeft _n17 _n16 .def 0 - =urLeft 1 .mv _n19 4 idle request lock release .names _n19 lock # urRight == 2 .names urRight _n19 _n18 .def 0 - =urRight 1 # urLeft == 2 || urRight == 2 .names _n16 _n18 _n1a .def 1 0 0 0 .mv _n1b 2 myTRUE myFALSE .names _n1b myTRUE .mv _n1c 2 myTRUE myFALSE .names _n1c myFALSE # (urLeft == 2 || urRight == 2) ? 0 : 1 .mv _n1d 2 myTRUE myFALSE .names _n1b _n1c _n1a _n1d - - 0 =_n1c - - 1 =_n1b .names _n1d childOwns$raw_n15 - =_n1d # assign giveChild = (uaLeft == 0 || uaRight == 0) ? 0 : 1 .mv giveChild$raw_n1e 2 myTRUE myFALSE .mv _n20 2 myTRUE myFALSE .names _n20 myTRUE # uaLeft == 0 .names uaLeft _n20 _n1f .def 0 - =uaLeft 1 .mv _n22 2 myTRUE myFALSE .names _n22 myTRUE # uaRight == 0 .names uaRight _n22 _n21 .def 0 - =uaRight 1 # uaLeft == 0 || uaRight == 0 .names _n1f _n21 _n23 .def 1 0 0 0 .mv _n24 2 myTRUE myFALSE .names _n24 myTRUE .mv _n25 2 myTRUE myFALSE .names _n25 myFALSE # (uaLeft == 0 || uaRight == 0) ? 0 : 1 .mv _n26 2 myTRUE myFALSE .names _n24 _n25 _n23 _n26 - - 0 =_n25 - - 1 =_n24 .names _n26 giveChild$raw_n1e - =_n26 # assign uaLeft = (!(mustGiveParent == 0) && (holdToken == 0 && urLeft == request && (!(urRight == request ) || prevRight == 0))) ? 0 : 1 .mv uaLeft$raw_n27 2 myTRUE myFALSE .mv _n29 2 myTRUE myFALSE .names _n29 myTRUE # mustGiveParent == 0 .names mustGiveParent _n29 _n28 .def 0 - =mustGiveParent 1 .names _n28 _n2a 0 1 1 0 .mv _n2c 2 myTRUE myFALSE .names _n2c myTRUE # holdToken == 0 .names holdToken _n2c _n2b .def 0 - =holdToken 1 .mv _n2e 4 idle request lock release .names _n2e request # urLeft == 1 .names urLeft _n2e _n2d .def 0 - =urLeft 1 # holdToken == 0 && urLeft == 1 .names _n2b _n2d _n2f .def 0 1 1 1 .mv _n31 4 idle request lock release .names _n31 request # urRight == 1 .names urRight _n31 _n30 .def 0 - =urRight 1 .names _n30 _n32 0 1 1 0 .mv _n34 2 myTRUE myFALSE .names _n34 myTRUE # prevRight == 0 .names prevRight _n34 _n33 .def 0 - =prevRight 1 # !(urRight == 1) || prevRight == 0 .names _n32 _n33 _n35 .def 1 0 0 0 # holdToken == 0 && urLeft == 1 && (!(urRight == 1) || prevRight == 0) .names _n2f _n35 _n36 .def 0 1 1 1 # !(mustGiveParent == 0) && (holdToken == 0 && urLeft == 1 && (!(urRight == 1) || prevRight == 0)) .names _n2a _n36 _n37 .def 0 1 1 1 .mv _n38 2 myTRUE myFALSE .names _n38 myTRUE .mv _n39 2 myTRUE myFALSE .names _n39 myFALSE # (!(mustGiveParent == 0) && (holdToken == 0 && urLeft == 1 && (!(urRight == 1) || prevRight == 0))) ? 0 : 1 .mv _n3a 2 myTRUE myFALSE .names _n38 _n39 _n37 _n3a - - 0 =_n39 - - 1 =_n38 .names _n3a uaLeft$raw_n27 - =_n3a # assign uaRight = (!(mustGiveParent == 0) && (holdToken == 0 && urRight == request && (!(urLeft == request ) || prevLeft == 0))) ? 0 : 1 .mv uaRight$raw_n3b 2 myTRUE myFALSE .mv _n3d 2 myTRUE myFALSE .names _n3d myTRUE # mustGiveParent == 0 .names mustGiveParent _n3d _n3c .def 0 - =mustGiveParent 1 .names _n3c _n3e 0 1 1 0 .mv _n40 2 myTRUE myFALSE .names _n40 myTRUE # holdToken == 0 .names holdToken _n40 _n3f .def 0 - =holdToken 1 .mv _n42 4 idle request lock release .names _n42 request # urRight == 1 .names urRight _n42 _n41 .def 0 - =urRight 1 # holdToken == 0 && urRight == 1 .names _n3f _n41 _n43 .def 0 1 1 1 .mv _n45 4 idle request lock release .names _n45 request # urLeft == 1 .names urLeft _n45 _n44 .def 0 - =urLeft 1 .names _n44 _n46 0 1 1 0 .mv _n48 2 myTRUE myFALSE .names _n48 myTRUE # prevLeft == 0 .names prevLeft _n48 _n47 .def 0 - =prevLeft 1 # !(urLeft == 1) || prevLeft == 0 .names _n46 _n47 _n49 .def 1 0 0 0 # holdToken == 0 && urRight == 1 && (!(urLeft == 1) || prevLeft == 0) .names _n43 _n49 _n4a .def 0 1 1 1 # !(mustGiveParent == 0) && (holdToken == 0 && urRight == 1 && (!(urLeft == 1) || prevLeft == 0)) .names _n3e _n4a _n4b .def 0 1 1 1 .mv _n4c 2 myTRUE myFALSE .names _n4c myTRUE .mv _n4d 2 myTRUE myFALSE .names _n4d myFALSE # (!(mustGiveParent == 0) && (holdToken == 0 && urRight == 1 && (!(urLeft == 1) || prevLeft == 0))) ? 0 : 1 .mv _n4e 2 myTRUE myFALSE .names _n4c _n4d _n4b _n4e - - 0 =_n4d - - 1 =_n4c .names _n4e uaRight$raw_n3b - =_n4e # assign xr = (holdToken == myFALSE && (urLeft == 1 || urRight == 1)) ? 1 : (childOwns == myTRUE ) ? 2 : (holdToken == myTRUE && (((mustGiveParent == myTRUE ) || !((urLeft == 1 || urRight == 1))) && !(topCell == myTRUE ))) ? 3 : 0 .mv xr$raw_n4f 4 idle request lock release .mv _n51 2 myTRUE myFALSE .names _n51 myFALSE # holdToken == 1 .names holdToken _n51 _n50 .def 0 - =holdToken 1 .mv _n53 4 idle request lock release .names _n53 request # urLeft == 1 .names urLeft _n53 _n52 .def 0 - =urLeft 1 .mv _n55 4 idle request lock release .names _n55 request # urRight == 1 .names urRight _n55 _n54 .def 0 - =urRight 1 # urLeft == 1 || urRight == 1 .names _n52 _n54 _n56 .def 1 0 0 0 # holdToken == 1 && (urLeft == 1 || urRight == 1) .names _n50 _n56 _n57 .def 0 1 1 1 .mv _n59 2 myTRUE myFALSE .names _n59 myTRUE # childOwns == 0 .names childOwns _n59 _n58 .def 0 - =childOwns 1 .mv _n5b 2 myTRUE myFALSE .names _n5b myTRUE # holdToken == 0 .names holdToken _n5b _n5a .def 0 - =holdToken 1 .mv _n5d 2 myTRUE myFALSE .names _n5d myTRUE # mustGiveParent == 0 .names mustGiveParent _n5d _n5c .def 0 - =mustGiveParent 1 .mv _n5f 4 idle request lock release .names _n5f request # urLeft == 1 .names urLeft _n5f _n5e .def 0 - =urLeft 1 .mv _n61 4 idle request lock release .names _n61 request # urRight == 1 .names urRight _n61 _n60 .def 0 - =urRight 1 # urLeft == 1 || urRight == 1 .names _n5e _n60 _n62 .def 1 0 0 0 .names _n62 _n63 0 1 1 0 # (mustGiveParent == 0) || !((urLeft == 1 || urRight == 1)) .names _n5c _n63 _n64 .def 1 0 0 0 .mv _n66 2 myTRUE myFALSE .names _n66 myTRUE # topCell == 0 .names topCell _n66 _n65 .def 0 - =topCell 1 .names _n65 _n67 0 1 1 0 # ((mustGiveParent == 0) || !((urLeft == 1 || urRight == 1))) && !(topCell == 0) .names _n64 _n67 _n68 .def 0 1 1 1 # holdToken == 0 && (((mustGiveParent == 0) || !((urLeft == 1 || urRight == 1))) && !(topCell == 0)) .names _n5a _n68 _n69 .def 0 1 1 1 .mv _n6a 4 idle request lock release .names _n6a release .mv _n6b 4 idle request lock release .names _n6b idle # (holdToken == 0 && (((mustGiveParent == 0) || !((urLeft == 1 || urRight == 1))) && !(topCell == 0))) ? 3 : 0 .mv _n6c 4 idle request lock release .names _n6a _n6b _n69 _n6c - - 0 =_n6b - - 1 =_n6a .mv _n6d 4 idle request lock release .names _n6d lock # (childOwns == 0) ? 2 : (holdToken == 0 && (((mustGiveParent == 0) || !((urLeft == 1 || urRight == 1))) && !(topCell == 0))) ? 3 : 0 .mv _n6e 4 idle request lock release .names _n6d _n6c _n58 _n6e - - 0 =_n6c - - 1 =_n6d .mv _n6f 4 idle request lock release .names _n6f request # (holdToken == 1 && (urLeft == 1 || urRight == 1)) ? 1 : (childOwns == 0) ? 2 : (holdToken == 0 && (((mustGiveParent == 0) || !((urLeft == 1 || urRight == 1))) && !(topCell == 0))) ? 3 : 0 .mv _n70 4 idle request lock release .names _n6f _n6e _n57 _n70 - - 0 =_n6e - - 1 =_n6f .names _n70 xr$raw_n4f - =_n70 .mv _n72 2 myTRUE myFALSE .names _n72 myTRUE # xa == 0 .names xa _n72 _n71 .def 0 - =xa 1 .names _n71 _n73 - =_n71 # holdToken = 0 .mv holdToken$_n71_n74$true 2 myTRUE myFALSE .names holdToken$_n71_n74$true myTRUE .mv _n76 2 myTRUE myFALSE .names _n76 myTRUE # giveChild == 0 .names giveChild _n76 _n75 .def 0 - =giveChild 1 .names _n75 _n77 - =_n75 # holdToken = 1 .mv holdToken$_n75_n78$true 2 myTRUE myFALSE .names holdToken$_n75_n78$true myFALSE .mv _n7a 4 idle request lock release .names _n7a release # urLeft == 3 .names urLeft _n7a _n79 .def 0 - =urLeft 1 .mv _n7c 4 idle request lock release .names _n7c release # urRight == 3 .names urRight _n7c _n7b .def 0 - =urRight 1 # urLeft == 3 || urRight == 3 .names _n79 _n7b _n7d .def 1 0 0 0 .names _n7d _n7e - =_n7d # holdToken = 0 .mv holdToken$_n7d_n7f$true 2 myTRUE myFALSE .names holdToken$_n7d_n7f$true myTRUE .mv _n81 4 idle request lock release .names _n81 release # xr == 3 .names xr _n81 _n80 .def 0 - =xr 1 .names _n80 _n82 - =_n80 # holdToken = 1 .mv holdToken$_n80_n83$true 2 myTRUE myFALSE .names holdToken$_n80_n83$true myFALSE # if/else (xr == 3) .mv holdToken$_n80$raw_n86 2 myTRUE myFALSE .names holdToken$_n80_n83$true holdToken _n80 holdToken$_n80$raw_n86 - - 0 =holdToken - - 1 =holdToken$_n80_n83$true # if/else (urLeft == 3 || urRight == 3) .mv holdToken$_n7d$raw_n88 2 myTRUE myFALSE .names holdToken$_n7d_n7f$true holdToken$_n80$raw_n86 _n7d holdToken$_n7d$raw_n88 - - 0 =holdToken$_n80$raw_n86 - - 1 =holdToken$_n7d_n7f$true # if/else (giveChild == 0) .mv holdToken$_n75$raw_n8c 2 myTRUE myFALSE .names holdToken$_n75_n78$true holdToken$_n7d$raw_n88 _n75 holdToken$_n75$raw_n8c - - 0 =holdToken$_n7d$raw_n88 - - 1 =holdToken$_n75_n78$true # if/else (xa == 0) .mv holdToken$_n71$raw_n90 2 myTRUE myFALSE .names holdToken$_n71_n74$true holdToken$_n75$raw_n8c _n71 holdToken$_n71$raw_n90 - - 0 =holdToken$_n75$raw_n8c - - 1 =holdToken$_n71_n74$true .mv _n94 2 myTRUE myFALSE .names _n94 myTRUE # uaLeft == 0 .names uaLeft _n94 _n93 .def 0 - =uaLeft 1 .names _n93 _n95 - =_n93 # prevLeft = 0 .mv prevLeft$_n93_n96$true 2 myTRUE myFALSE .names prevLeft$_n93_n96$true myTRUE # prevRight = 1 .mv prevRight$_n93_n97$true 2 myTRUE myFALSE .names prevRight$_n93_n97$true myFALSE .mv _n99 2 myTRUE myFALSE .names _n99 myTRUE # uaRight == 0 .names uaRight _n99 _n98 .def 0 - =uaRight 1 .names _n98 _n9a - =_n98 # prevLeft = 1 .mv prevLeft$_n98_n9b$true 2 myTRUE myFALSE .names prevLeft$_n98_n9b$true myFALSE # prevRight = 0 .mv prevRight$_n98_n9c$true 2 myTRUE myFALSE .names prevRight$_n98_n9c$true myTRUE # if/else (uaRight == 0) .mv prevLeft$_n98$raw_na3 2 myTRUE myFALSE .names prevLeft$_n98_n9b$true prevLeft _n98 prevLeft$_n98$raw_na3 - - 0 =prevLeft - - 1 =prevLeft$_n98_n9b$true .mv prevRight$_n98$raw_na5 2 myTRUE myFALSE .names prevRight$_n98_n9c$true prevRight _n98 prevRight$_n98$raw_na5 - - 0 =prevRight - - 1 =prevRight$_n98_n9c$true # if/else (uaLeft == 0) .mv prevLeft$_n93$raw_naa 2 myTRUE myFALSE .names prevLeft$_n93_n96$true prevLeft$_n98$raw_na3 _n93 prevLeft$_n93$raw_naa - - 0 =prevLeft$_n98$raw_na3 - - 1 =prevLeft$_n93_n96$true .mv prevRight$_n93$raw_nac 2 myTRUE myFALSE .names prevRight$_n93_n97$true prevRight$_n98$raw_na5 _n93 prevRight$_n93$raw_nac - - 0 =prevRight$_n98$raw_na5 - - 1 =prevRight$_n93_n97$true .mv _nb4 4 idle request lock release .names _nb4 release # urLeft == 3 .names urLeft _nb4 _nb3 .def 0 - =urLeft 1 .names _nb3 _nb5 - =_nb3 # processedLeft = 0 .mv processedLeft$_nb3_nb6$true 2 myTRUE myFALSE .names processedLeft$_nb3_nb6$true myTRUE .mv _nb8 4 idle request lock release .names _nb8 release # urRight == 3 .names urRight _nb8 _nb7 .def 0 - =urRight 1 .names _nb7 _nb9 - =_nb7 # processedRight = 0 .mv processedRight$_nb7_nba$true 2 myTRUE myFALSE .names processedRight$_nb7_nba$true myTRUE .mv _nbc 2 myTRUE myFALSE .names _nbc myTRUE # processedLeft == 0 .names processedLeft _nbc _nbb .def 0 - =processedLeft 1 .mv _nbe 2 myTRUE myFALSE .names _nbe myTRUE # processedRight == 0 .names processedRight _nbe _nbd .def 0 - =processedRight 1 # (processedLeft == 0) && (processedRight == 0) .names _nbb _nbd _nbf .def 0 1 1 1 .names _nbf _nc0 - =_nbf # processedLeft = 1 .mv processedLeft$_nbf_nc1$true 2 myTRUE myFALSE .names processedLeft$_nbf_nc1$true myFALSE # processedRight = 1 .mv processedRight$_nbf_nc2$true 2 myTRUE myFALSE .names processedRight$_nbf_nc2$true myFALSE # if/else ((processedLeft == 0) && (processedRight == 0)) .mv processedLeft$_nbf$raw_ncd 2 myTRUE myFALSE .names processedLeft$_nbf_nc1$true processedLeft _nbf processedLeft$_nbf$raw_ncd - - 0 =processedLeft - - 1 =processedLeft$_nbf_nc1$true .mv processedRight$_nbf$raw_ncf 2 myTRUE myFALSE .names processedRight$_nbf_nc2$true processedRight _nbf processedRight$_nbf$raw_ncf - - 0 =processedRight - - 1 =processedRight$_nbf_nc2$true # if/else (urRight == 3) .mv processedRight$_nb7$raw_nda 2 myTRUE myFALSE .names processedRight$_nb7_nba$true processedRight$_nbf$raw_ncf _nb7 processedRight$_nb7$raw_nda - - 0 =processedRight$_nbf$raw_ncf - - 1 =processedRight$_nb7_nba$true .mv processedLeft$_nb7$raw_ne1 2 myTRUE myFALSE .names processedLeft processedLeft$_nbf$raw_ncd _nb7 processedLeft$_nb7$raw_ne1 - - 0 =processedLeft$_nbf$raw_ncd - - 1 =processedLeft # if/else (urLeft == 3) .mv processedLeft$_nb3$raw_nea 2 myTRUE myFALSE .names processedLeft$_nb3_nb6$true processedLeft$_nb7$raw_ne1 _nb3 processedLeft$_nb3$raw_nea - - 0 =processedLeft$_nb7$raw_ne1 - - 1 =processedLeft$_nb3_nb6$true .mv processedRight$_nb3$raw_nf4 2 myTRUE myFALSE .names processedRight processedRight$_nb7$raw_nda _nb3 processedRight$_nb3$raw_nf4 - - 0 =processedRight$_nb7$raw_nda - - 1 =processedRight # conflict arbitrators .names _nb5 _nb9 _nc0 _nf7 .def 0 1 - - 1 0 0 1 1 .mv _nf8 2 myTRUE myFALSE .names _nf7 processedLeft$_nb3$raw_nea processedLeft _nf8 1 - - =processedLeft$_nb3$raw_nea 0 - - =processedLeft .names _n95 _n9a _n105 .def 0 1 - 1 0 1 1 .mv _n106 2 myTRUE myFALSE .names _n105 prevLeft$_n93$raw_naa prevLeft _n106 1 - - =prevLeft$_n93$raw_naa 0 - - =prevLeft .names _n73 _n77 _n7e _n82 _n113 .def 0 1 - - - 1 0 1 - - 1 0 0 1 - 1 0 0 0 1 1 .mv _n114 2 myTRUE myFALSE .names _n113 holdToken$_n71$raw_n90 holdToken _n114 1 - - =holdToken$_n71$raw_n90 0 - - =holdToken .names _nb5 _nb9 _nc0 _n121 .def 0 0 1 - 1 0 0 1 1 .mv _n122 2 myTRUE myFALSE .names _n121 processedRight$_nb3$raw_nf4 processedRight _n122 1 - - =processedRight$_nb3$raw_nf4 0 - - =processedRight .names uaLeft$raw_n27 uaLeft - =uaLeft$raw_n27 .names giveChild$raw_n1e giveChild - =giveChild$raw_n1e .names mustGiveParent$raw_n7 mustGiveParent - =mustGiveParent$raw_n7 .names xr$raw_n4f xr - =xr$raw_n4f .names uaRight$raw_n3b uaRight - =uaRight$raw_n3b .names childOwns$raw_n15 childOwns - =childOwns$raw_n15 .names _n95 _n9a _n12f .def 0 1 - 1 0 1 1 .mv _n130 2 myTRUE myFALSE .names _n12f prevRight$_n93$raw_nac prevRight _n130 1 - - =prevRight$_n93$raw_nac 0 - - =prevRight # non-blocking assignments # latches .r prevLeft$raw_n3 prevLeft - =prevLeft$raw_n3 .latch _n106 prevLeft .r processedLeft$raw_n5 processedLeft - =processedLeft$raw_n5 .latch _nf8 processedLeft .r processedRight$raw_n6 processedRight - =processedRight$raw_n6 .latch _n122 processedRight .r holdToken$raw_n14 holdToken - =holdToken$raw_n14 .latch _n114 holdToken .r prevRight$raw_n4 prevRight - =prevRight$raw_n4 .latch _n130 prevRight # quasi-continuous assignment .end .model procModel # I/O ports .outputs req .inputs ack .mv req 4 idle request lock release .mv procState 4 idle request lock release .mv ack 2 myTRUE myFALSE # assign req = procState .mv req$raw_n13d 4 idle request lock release .names procState req$raw_n13d - =procState # procState = 0 .mv procState$raw_n13e 4 idle request lock release .names procState$raw_n13e idle # non-blocking assignments for initial # assign randChoice = $NDset ( 0,1,2,3,4,5,6,7 ) .names -> randChoice<0> randChoice<1> randChoice<2> 0 0 0 1 0 0 0 1 0 1 1 0 0 0 1 1 0 1 0 1 1 1 1 1 .mv _n142 4 idle request lock release .names _n142 idle # procState == 0 .names procState _n142 _n141 .def 0 - =procState 1 .names _n144<0> 1 .names _n144<1> 1 .names _n144<2> 1 # randChoice == 7 .names randChoice<0> _n144<0> _n145<0> .def 0 0 1 1 1 0 1 .names randChoice<1> _n144<1> _n145<1> .def 0 0 1 1 1 0 1 .names randChoice<2> _n144<2> _n145<2> .def 0 0 1 1 1 0 1 .names _n145<0> _n145<1> _n145<2> _n146 .def 1 0 0 0 0 .names _n146 _n143 0 1 1 0 # procState == 0 && (randChoice == 7) .names _n141 _n143 _n147 .def 0 1 1 1 .names _n147 _n148 - =_n147 # procState = 1 .mv procState$_n147_n149$true 4 idle request lock release .names procState$_n147_n149$true request .mv _n14b 4 idle request lock release .names _n14b request # procState == 1 .names procState _n14b _n14a .def 0 - =procState 1 .mv _n14d 2 myTRUE myFALSE .names _n14d myTRUE # ack == 0 .names ack _n14d _n14c .def 0 - =ack 1 # procState == 1 && ack == 0 .names _n14a _n14c _n14e .def 0 1 1 1 .names _n14e _n14f - =_n14e # procState = 2 .mv procState$_n14e_n150$true 4 idle request lock release .names procState$_n14e_n150$true lock .mv _n152 4 idle request lock release .names _n152 lock # procState == 2 .names procState _n152 _n151 .def 0 - =procState 1 .names _n153<0> 1 .names _n153<1> 1 .names _n153<2> 0 # randChoice > 3 .names _n156 0 .names randChoice<0> _n153<0> _n156 _n155<0> .def 0 0 0 1 1 0 1 0 1 1 0 0 1 1 1 1 1 # carry/borrow .names _n158 0 .names randChoice<0> _n153<0> _n158 _n157 .def 0 0 0 1 1 0 1 0 1 0 1 1 1 1 1 1 1 .names randChoice<1> _n153<1> _n157 _n155<1> .def 0 0 0 1 1 0 1 0 1 1 0 0 1 1 1 1 1 # carry/borrow .names randChoice<1> _n153<1> _n157 _n159 .def 0 0 0 1 1 0 1 0 1 0 1 1 1 1 1 1 1 .names randChoice<2> _n153<2> _n159 _n155<2> .def 0 0 0 1 1 0 1 0 1 1 0 0 1 1 1 1 1 # carry/borrow .names randChoice<2> _n153<2> _n159 _n15a .def 0 0 0 1 1 0 1 0 1 0 1 1 1 1 1 1 1 .names _n155<0> _n155<1> _n155<2> _n15b .def 0 0 0 0 1 .names _n15a _n15b _n15c .def 1 0 0 0 .names _n15c _n154 0 1 1 0 # procState == 2 && (randChoice > 3) .names _n151 _n154 _n15d .def 0 1 1 1 .names _n15d _n15e - =_n15d # procState = 3 .mv procState$_n15d_n15f$true 4 idle request lock release .names procState$_n15d_n15f$true release .mv _n161 4 idle request lock release .names _n161 release # procState == 3 .names procState _n161 _n160 .def 0 - =procState 1 .names _n160 _n162 - =_n160 # procState = 0 .mv procState$_n160_n163$true 4 idle request lock release .names procState$_n160_n163$true idle # if/else (procState == 3) .mv procState$_n160$raw_n166 4 idle request lock release .names procState$_n160_n163$true procState _n160 procState$_n160$raw_n166 - - 0 =procState - - 1 =procState$_n160_n163$true # if/else (procState == 2 && (randChoice > 3)) .mv procState$_n15d$raw_n168 4 idle request lock release .names procState$_n15d_n15f$true procState$_n160$raw_n166 _n15d procState$_n15d$raw_n168 - - 0 =procState$_n160$raw_n166 - - 1 =procState$_n15d_n15f$true # if/else (procState == 1 && ack == 0) .mv procState$_n14e$raw_n16c 4 idle request lock release .names procState$_n14e_n150$true procState$_n15d$raw_n168 _n14e procState$_n14e$raw_n16c - - 0 =procState$_n15d$raw_n168 - - 1 =procState$_n14e_n150$true # if/else (procState == 0 && (randChoice == 7)) .mv procState$_n147$raw_n170 4 idle request lock release .names procState$_n147_n149$true procState$_n14e$raw_n16c _n147 procState$_n147$raw_n170 - - 0 =procState$_n14e$raw_n16c - - 1 =procState$_n147_n149$true # conflict arbitrators .names req$raw_n13d req - =req$raw_n13d .names _n148 _n14f _n15e _n162 _n173 .def 0 1 - - - 1 0 1 - - 1 0 0 1 - 1 0 0 0 1 1 .mv _n174 4 idle request lock release .names _n173 procState$_n147$raw_n170 procState _n174 1 - - =procState$_n147$raw_n170 0 - - =procState # non-blocking assignments # latches .r procState$raw_n13e procState - =procState$raw_n13e .latch _n174 procState # quasi-continuous assignment .end