| 1 | # /projects/vl2mv/vl2mvt/mips/bin/vl2mv 8-arbit.v |
|---|
| 2 | # version: 0.2 |
|---|
| 3 | # date: 09:05:18 03/01/97 (PST) |
|---|
| 4 | .model main |
|---|
| 5 | # I/O ports |
|---|
| 6 | .mv sa 2 myTRUE myFALSE |
|---|
| 7 | .mv xa 2 myTRUE myFALSE |
|---|
| 8 | .mv yr 4 idle request lock release |
|---|
| 9 | .mv sr 4 idle request lock release |
|---|
| 10 | .mv xr 4 idle request lock release |
|---|
| 11 | .mv ya 2 myTRUE myFALSE |
|---|
| 12 | .mv constTRUE 2 myTRUE myFALSE |
|---|
| 13 | # assign sa = 1 |
|---|
| 14 | .mv sa$raw_n0 2 myTRUE myFALSE |
|---|
| 15 | .names sa$raw_n0 |
|---|
| 16 | myFALSE |
|---|
| 17 | # assign constTRUE = 0 |
|---|
| 18 | .mv constTRUE$raw_n1 2 myTRUE myFALSE |
|---|
| 19 | .names constTRUE$raw_n1 |
|---|
| 20 | myTRUE |
|---|
| 21 | .subckt arbitCell F0 topCell=constTRUE urLeft=xr urRight=yr uaLeft=xa uaRight=ya xr=sr xa=sa |
|---|
| 22 | .subckt fourCells G1 sa=xa sr=xr |
|---|
| 23 | .subckt fourCells G2 sa=ya sr=yr |
|---|
| 24 | # conflict arbitrators |
|---|
| 25 | .names sa$raw_n0 sa |
|---|
| 26 | - =sa$raw_n0 |
|---|
| 27 | .names constTRUE$raw_n1 constTRUE |
|---|
| 28 | - =constTRUE$raw_n1 |
|---|
| 29 | # non-blocking assignments |
|---|
| 30 | # latches |
|---|
| 31 | # quasi-continuous assignment |
|---|
| 32 | .end |
|---|
| 33 | |
|---|
| 34 | |
|---|
| 35 | .model arbitCell |
|---|
| 36 | # I/O ports |
|---|
| 37 | .outputs uaLeft |
|---|
| 38 | .inputs topCell |
|---|
| 39 | .inputs xa |
|---|
| 40 | .inputs urRight |
|---|
| 41 | .inputs urLeft |
|---|
| 42 | .outputs xr |
|---|
| 43 | .outputs uaRight |
|---|
| 44 | .mv processedLeft 2 myTRUE myFALSE |
|---|
| 45 | .mv prevLeft 2 myTRUE myFALSE |
|---|
| 46 | .mv holdToken 2 myTRUE myFALSE |
|---|
| 47 | .mv processedRight 2 myTRUE myFALSE |
|---|
| 48 | .mv uaLeft 2 myTRUE myFALSE |
|---|
| 49 | .mv topCell 2 myTRUE myFALSE |
|---|
| 50 | .mv xa 2 myTRUE myFALSE |
|---|
| 51 | .mv urRight 4 idle request lock release |
|---|
| 52 | .mv giveChild 2 myTRUE myFALSE |
|---|
| 53 | .mv urLeft 4 idle request lock release |
|---|
| 54 | .mv mustGiveParent 2 myTRUE myFALSE |
|---|
| 55 | .mv xr 4 idle request lock release |
|---|
| 56 | .mv uaRight 2 myTRUE myFALSE |
|---|
| 57 | .mv childOwns 2 myTRUE myFALSE |
|---|
| 58 | .mv prevRight 2 myTRUE myFALSE |
|---|
| 59 | # prevLeft = 1 |
|---|
| 60 | .mv prevLeft$raw_n2 2 myTRUE myFALSE |
|---|
| 61 | .names prevLeft$raw_n2 |
|---|
| 62 | myFALSE |
|---|
| 63 | # non-blocking assignments for initial |
|---|
| 64 | # prevRight = 0 |
|---|
| 65 | .mv prevRight$raw_n3 2 myTRUE myFALSE |
|---|
| 66 | .names prevRight$raw_n3 |
|---|
| 67 | myTRUE |
|---|
| 68 | # non-blocking assignments for initial |
|---|
| 69 | # processedLeft = 1 |
|---|
| 70 | .mv processedLeft$raw_n4 2 myTRUE myFALSE |
|---|
| 71 | .names processedLeft$raw_n4 |
|---|
| 72 | myFALSE |
|---|
| 73 | # non-blocking assignments for initial |
|---|
| 74 | # processedRight = 1 |
|---|
| 75 | .mv processedRight$raw_n5 2 myTRUE myFALSE |
|---|
| 76 | .names processedRight$raw_n5 |
|---|
| 77 | myFALSE |
|---|
| 78 | # non-blocking assignments for initial |
|---|
| 79 | # assign mustGiveParent = (processedLeft == 0) && (processedRight == 0) && (!(topCell == 0)) ? 0 : 1 |
|---|
| 80 | .mv mustGiveParent$raw_n6 2 myTRUE myFALSE |
|---|
| 81 | .mv _n8 2 myTRUE myFALSE |
|---|
| 82 | .names _n8 |
|---|
| 83 | myTRUE |
|---|
| 84 | # processedLeft == 0 |
|---|
| 85 | .names processedLeft _n8 _n7 |
|---|
| 86 | .def 0 |
|---|
| 87 | - =processedLeft 1 |
|---|
| 88 | .mv _na 2 myTRUE myFALSE |
|---|
| 89 | .names _na |
|---|
| 90 | myTRUE |
|---|
| 91 | # processedRight == 0 |
|---|
| 92 | .names processedRight _na _n9 |
|---|
| 93 | .def 0 |
|---|
| 94 | - =processedRight 1 |
|---|
| 95 | # (processedLeft == 0) && (processedRight == 0) |
|---|
| 96 | .names _n7 _n9 _nb |
|---|
| 97 | .def 0 |
|---|
| 98 | 1 1 1 |
|---|
| 99 | .mv _nd 2 myTRUE myFALSE |
|---|
| 100 | .names _nd |
|---|
| 101 | myTRUE |
|---|
| 102 | # topCell == 0 |
|---|
| 103 | .names topCell _nd _nc |
|---|
| 104 | .def 0 |
|---|
| 105 | - =topCell 1 |
|---|
| 106 | .names _nc _ne |
|---|
| 107 | 0 1 |
|---|
| 108 | 1 0 |
|---|
| 109 | # (processedLeft == 0) && (processedRight == 0) && (!(topCell == 0)) |
|---|
| 110 | .names _nb _ne _nf |
|---|
| 111 | .def 0 |
|---|
| 112 | 1 1 1 |
|---|
| 113 | .mv _n10 2 myTRUE myFALSE |
|---|
| 114 | .names _n10 |
|---|
| 115 | myTRUE |
|---|
| 116 | .mv _n11 2 myTRUE myFALSE |
|---|
| 117 | .names _n11 |
|---|
| 118 | myFALSE |
|---|
| 119 | # (processedLeft == 0) && (processedRight == 0) && (!(topCell == 0)) ? 0 : 1 |
|---|
| 120 | .mv _n12 2 myTRUE myFALSE |
|---|
| 121 | .names _n10 _n11 _nf _n12 |
|---|
| 122 | - - 0 =_n11 |
|---|
| 123 | - - 1 =_n10 |
|---|
| 124 | .names _n12 mustGiveParent$raw_n6 |
|---|
| 125 | - =_n12 |
|---|
| 126 | # holdToken = topCell |
|---|
| 127 | .mv holdToken$raw_n13 2 myTRUE myFALSE |
|---|
| 128 | .names topCell holdToken$raw_n13 |
|---|
| 129 | - =topCell |
|---|
| 130 | # non-blocking assignments for initial |
|---|
| 131 | # assign childOwns = (urLeft == lock || urRight == lock ) ? 0 : 1 |
|---|
| 132 | .mv childOwns$raw_n14 2 myTRUE myFALSE |
|---|
| 133 | .mv _n16 4 idle request lock release |
|---|
| 134 | .names _n16 |
|---|
| 135 | lock |
|---|
| 136 | # urLeft == 2 |
|---|
| 137 | .names urLeft _n16 _n15 |
|---|
| 138 | .def 0 |
|---|
| 139 | - =urLeft 1 |
|---|
| 140 | .mv _n18 4 idle request lock release |
|---|
| 141 | .names _n18 |
|---|
| 142 | lock |
|---|
| 143 | # urRight == 2 |
|---|
| 144 | .names urRight _n18 _n17 |
|---|
| 145 | .def 0 |
|---|
| 146 | - =urRight 1 |
|---|
| 147 | # urLeft == 2 || urRight == 2 |
|---|
| 148 | .names _n15 _n17 _n19 |
|---|
| 149 | .def 1 |
|---|
| 150 | 0 0 0 |
|---|
| 151 | .mv _n1a 2 myTRUE myFALSE |
|---|
| 152 | .names _n1a |
|---|
| 153 | myTRUE |
|---|
| 154 | .mv _n1b 2 myTRUE myFALSE |
|---|
| 155 | .names _n1b |
|---|
| 156 | myFALSE |
|---|
| 157 | # (urLeft == 2 || urRight == 2) ? 0 : 1 |
|---|
| 158 | .mv _n1c 2 myTRUE myFALSE |
|---|
| 159 | .names _n1a _n1b _n19 _n1c |
|---|
| 160 | - - 0 =_n1b |
|---|
| 161 | - - 1 =_n1a |
|---|
| 162 | .names _n1c childOwns$raw_n14 |
|---|
| 163 | - =_n1c |
|---|
| 164 | # assign giveChild = (uaLeft == 0 || uaRight == 0) ? 0 : 1 |
|---|
| 165 | .mv giveChild$raw_n1d 2 myTRUE myFALSE |
|---|
| 166 | .mv _n1f 2 myTRUE myFALSE |
|---|
| 167 | .names _n1f |
|---|
| 168 | myTRUE |
|---|
| 169 | # uaLeft == 0 |
|---|
| 170 | .names uaLeft _n1f _n1e |
|---|
| 171 | .def 0 |
|---|
| 172 | - =uaLeft 1 |
|---|
| 173 | .mv _n21 2 myTRUE myFALSE |
|---|
| 174 | .names _n21 |
|---|
| 175 | myTRUE |
|---|
| 176 | # uaRight == 0 |
|---|
| 177 | .names uaRight _n21 _n20 |
|---|
| 178 | .def 0 |
|---|
| 179 | - =uaRight 1 |
|---|
| 180 | # uaLeft == 0 || uaRight == 0 |
|---|
| 181 | .names _n1e _n20 _n22 |
|---|
| 182 | .def 1 |
|---|
| 183 | 0 0 0 |
|---|
| 184 | .mv _n23 2 myTRUE myFALSE |
|---|
| 185 | .names _n23 |
|---|
| 186 | myTRUE |
|---|
| 187 | .mv _n24 2 myTRUE myFALSE |
|---|
| 188 | .names _n24 |
|---|
| 189 | myFALSE |
|---|
| 190 | # (uaLeft == 0 || uaRight == 0) ? 0 : 1 |
|---|
| 191 | .mv _n25 2 myTRUE myFALSE |
|---|
| 192 | .names _n23 _n24 _n22 _n25 |
|---|
| 193 | - - 0 =_n24 |
|---|
| 194 | - - 1 =_n23 |
|---|
| 195 | .names _n25 giveChild$raw_n1d |
|---|
| 196 | - =_n25 |
|---|
| 197 | # assign uaLeft = (!(mustGiveParent == 0) && (holdToken == 0 && urLeft == request && (!(urRight == request ) || prevRight == 0))) ? 0 : 1 |
|---|
| 198 | .mv uaLeft$raw_n26 2 myTRUE myFALSE |
|---|
| 199 | .mv _n28 2 myTRUE myFALSE |
|---|
| 200 | .names _n28 |
|---|
| 201 | myTRUE |
|---|
| 202 | # mustGiveParent == 0 |
|---|
| 203 | .names mustGiveParent _n28 _n27 |
|---|
| 204 | .def 0 |
|---|
| 205 | - =mustGiveParent 1 |
|---|
| 206 | .names _n27 _n29 |
|---|
| 207 | 0 1 |
|---|
| 208 | 1 0 |
|---|
| 209 | .mv _n2b 2 myTRUE myFALSE |
|---|
| 210 | .names _n2b |
|---|
| 211 | myTRUE |
|---|
| 212 | # holdToken == 0 |
|---|
| 213 | .names holdToken _n2b _n2a |
|---|
| 214 | .def 0 |
|---|
| 215 | - =holdToken 1 |
|---|
| 216 | .mv _n2d 4 idle request lock release |
|---|
| 217 | .names _n2d |
|---|
| 218 | request |
|---|
| 219 | # urLeft == 1 |
|---|
| 220 | .names urLeft _n2d _n2c |
|---|
| 221 | .def 0 |
|---|
| 222 | - =urLeft 1 |
|---|
| 223 | # holdToken == 0 && urLeft == 1 |
|---|
| 224 | .names _n2a _n2c _n2e |
|---|
| 225 | .def 0 |
|---|
| 226 | 1 1 1 |
|---|
| 227 | .mv _n30 4 idle request lock release |
|---|
| 228 | .names _n30 |
|---|
| 229 | request |
|---|
| 230 | # urRight == 1 |
|---|
| 231 | .names urRight _n30 _n2f |
|---|
| 232 | .def 0 |
|---|
| 233 | - =urRight 1 |
|---|
| 234 | .names _n2f _n31 |
|---|
| 235 | 0 1 |
|---|
| 236 | 1 0 |
|---|
| 237 | .mv _n33 2 myTRUE myFALSE |
|---|
| 238 | .names _n33 |
|---|
| 239 | myTRUE |
|---|
| 240 | # prevRight == 0 |
|---|
| 241 | .names prevRight _n33 _n32 |
|---|
| 242 | .def 0 |
|---|
| 243 | - =prevRight 1 |
|---|
| 244 | # !(urRight == 1) || prevRight == 0 |
|---|
| 245 | .names _n31 _n32 _n34 |
|---|
| 246 | .def 1 |
|---|
| 247 | 0 0 0 |
|---|
| 248 | # holdToken == 0 && urLeft == 1 && (!(urRight == 1) || prevRight == 0) |
|---|
| 249 | .names _n2e _n34 _n35 |
|---|
| 250 | .def 0 |
|---|
| 251 | 1 1 1 |
|---|
| 252 | # !(mustGiveParent == 0) && (holdToken == 0 && urLeft == 1 && (!(urRight == 1) || prevRight == 0)) |
|---|
| 253 | .names _n29 _n35 _n36 |
|---|
| 254 | .def 0 |
|---|
| 255 | 1 1 1 |
|---|
| 256 | .mv _n37 2 myTRUE myFALSE |
|---|
| 257 | .names _n37 |
|---|
| 258 | myTRUE |
|---|
| 259 | .mv _n38 2 myTRUE myFALSE |
|---|
| 260 | .names _n38 |
|---|
| 261 | myFALSE |
|---|
| 262 | # (!(mustGiveParent == 0) && (holdToken == 0 && urLeft == 1 && (!(urRight == 1) || prevRight == 0))) ? 0 : 1 |
|---|
| 263 | .mv _n39 2 myTRUE myFALSE |
|---|
| 264 | .names _n37 _n38 _n36 _n39 |
|---|
| 265 | - - 0 =_n38 |
|---|
| 266 | - - 1 =_n37 |
|---|
| 267 | .names _n39 uaLeft$raw_n26 |
|---|
| 268 | - =_n39 |
|---|
| 269 | # assign uaRight = (!(mustGiveParent == 0) && (holdToken == 0 && urRight == request && (!(urLeft == request ) || prevLeft == 0))) ? 0 : 1 |
|---|
| 270 | .mv uaRight$raw_n3a 2 myTRUE myFALSE |
|---|
| 271 | .mv _n3c 2 myTRUE myFALSE |
|---|
| 272 | .names _n3c |
|---|
| 273 | myTRUE |
|---|
| 274 | # mustGiveParent == 0 |
|---|
| 275 | .names mustGiveParent _n3c _n3b |
|---|
| 276 | .def 0 |
|---|
| 277 | - =mustGiveParent 1 |
|---|
| 278 | .names _n3b _n3d |
|---|
| 279 | 0 1 |
|---|
| 280 | 1 0 |
|---|
| 281 | .mv _n3f 2 myTRUE myFALSE |
|---|
| 282 | .names _n3f |
|---|
| 283 | myTRUE |
|---|
| 284 | # holdToken == 0 |
|---|
| 285 | .names holdToken _n3f _n3e |
|---|
| 286 | .def 0 |
|---|
| 287 | - =holdToken 1 |
|---|
| 288 | .mv _n41 4 idle request lock release |
|---|
| 289 | .names _n41 |
|---|
| 290 | request |
|---|
| 291 | # urRight == 1 |
|---|
| 292 | .names urRight _n41 _n40 |
|---|
| 293 | .def 0 |
|---|
| 294 | - =urRight 1 |
|---|
| 295 | # holdToken == 0 && urRight == 1 |
|---|
| 296 | .names _n3e _n40 _n42 |
|---|
| 297 | .def 0 |
|---|
| 298 | 1 1 1 |
|---|
| 299 | .mv _n44 4 idle request lock release |
|---|
| 300 | .names _n44 |
|---|
| 301 | request |
|---|
| 302 | # urLeft == 1 |
|---|
| 303 | .names urLeft _n44 _n43 |
|---|
| 304 | .def 0 |
|---|
| 305 | - =urLeft 1 |
|---|
| 306 | .names _n43 _n45 |
|---|
| 307 | 0 1 |
|---|
| 308 | 1 0 |
|---|
| 309 | .mv _n47 2 myTRUE myFALSE |
|---|
| 310 | .names _n47 |
|---|
| 311 | myTRUE |
|---|
| 312 | # prevLeft == 0 |
|---|
| 313 | .names prevLeft _n47 _n46 |
|---|
| 314 | .def 0 |
|---|
| 315 | - =prevLeft 1 |
|---|
| 316 | # !(urLeft == 1) || prevLeft == 0 |
|---|
| 317 | .names _n45 _n46 _n48 |
|---|
| 318 | .def 1 |
|---|
| 319 | 0 0 0 |
|---|
| 320 | # holdToken == 0 && urRight == 1 && (!(urLeft == 1) || prevLeft == 0) |
|---|
| 321 | .names _n42 _n48 _n49 |
|---|
| 322 | .def 0 |
|---|
| 323 | 1 1 1 |
|---|
| 324 | # !(mustGiveParent == 0) && (holdToken == 0 && urRight == 1 && (!(urLeft == 1) || prevLeft == 0)) |
|---|
| 325 | .names _n3d _n49 _n4a |
|---|
| 326 | .def 0 |
|---|
| 327 | 1 1 1 |
|---|
| 328 | .mv _n4b 2 myTRUE myFALSE |
|---|
| 329 | .names _n4b |
|---|
| 330 | myTRUE |
|---|
| 331 | .mv _n4c 2 myTRUE myFALSE |
|---|
| 332 | .names _n4c |
|---|
| 333 | myFALSE |
|---|
| 334 | # (!(mustGiveParent == 0) && (holdToken == 0 && urRight == 1 && (!(urLeft == 1) || prevLeft == 0))) ? 0 : 1 |
|---|
| 335 | .mv _n4d 2 myTRUE myFALSE |
|---|
| 336 | .names _n4b _n4c _n4a _n4d |
|---|
| 337 | - - 0 =_n4c |
|---|
| 338 | - - 1 =_n4b |
|---|
| 339 | .names _n4d uaRight$raw_n3a |
|---|
| 340 | - =_n4d |
|---|
| 341 | # assign xr = (holdToken == myFALSE && (urLeft == 1 || urRight == 1)) ? 1 : (childOwns == myTRUE ) ? 2 : (holdToken == myTRUE && (((mustGiveParent == myTRUE ) || !((urLeft == 1 || urRight == 1))) && !(topCell == myTRUE ))) ? 3 : 0 |
|---|
| 342 | .mv xr$raw_n4e 4 idle request lock release |
|---|
| 343 | .mv _n50 2 myTRUE myFALSE |
|---|
| 344 | .names _n50 |
|---|
| 345 | myFALSE |
|---|
| 346 | # holdToken == 1 |
|---|
| 347 | .names holdToken _n50 _n4f |
|---|
| 348 | .def 0 |
|---|
| 349 | - =holdToken 1 |
|---|
| 350 | .mv _n52 4 idle request lock release |
|---|
| 351 | .names _n52 |
|---|
| 352 | request |
|---|
| 353 | # urLeft == 1 |
|---|
| 354 | .names urLeft _n52 _n51 |
|---|
| 355 | .def 0 |
|---|
| 356 | - =urLeft 1 |
|---|
| 357 | .mv _n54 4 idle request lock release |
|---|
| 358 | .names _n54 |
|---|
| 359 | request |
|---|
| 360 | # urRight == 1 |
|---|
| 361 | .names urRight _n54 _n53 |
|---|
| 362 | .def 0 |
|---|
| 363 | - =urRight 1 |
|---|
| 364 | # urLeft == 1 || urRight == 1 |
|---|
| 365 | .names _n51 _n53 _n55 |
|---|
| 366 | .def 1 |
|---|
| 367 | 0 0 0 |
|---|
| 368 | # holdToken == 1 && (urLeft == 1 || urRight == 1) |
|---|
| 369 | .names _n4f _n55 _n56 |
|---|
| 370 | .def 0 |
|---|
| 371 | 1 1 1 |
|---|
| 372 | .mv _n58 2 myTRUE myFALSE |
|---|
| 373 | .names _n58 |
|---|
| 374 | myTRUE |
|---|
| 375 | # childOwns == 0 |
|---|
| 376 | .names childOwns _n58 _n57 |
|---|
| 377 | .def 0 |
|---|
| 378 | - =childOwns 1 |
|---|
| 379 | .mv _n5a 2 myTRUE myFALSE |
|---|
| 380 | .names _n5a |
|---|
| 381 | myTRUE |
|---|
| 382 | # holdToken == 0 |
|---|
| 383 | .names holdToken _n5a _n59 |
|---|
| 384 | .def 0 |
|---|
| 385 | - =holdToken 1 |
|---|
| 386 | .mv _n5c 2 myTRUE myFALSE |
|---|
| 387 | .names _n5c |
|---|
| 388 | myTRUE |
|---|
| 389 | # mustGiveParent == 0 |
|---|
| 390 | .names mustGiveParent _n5c _n5b |
|---|
| 391 | .def 0 |
|---|
| 392 | - =mustGiveParent 1 |
|---|
| 393 | .mv _n5e 4 idle request lock release |
|---|
| 394 | .names _n5e |
|---|
| 395 | request |
|---|
| 396 | # urLeft == 1 |
|---|
| 397 | .names urLeft _n5e _n5d |
|---|
| 398 | .def 0 |
|---|
| 399 | - =urLeft 1 |
|---|
| 400 | .mv _n60 4 idle request lock release |
|---|
| 401 | .names _n60 |
|---|
| 402 | request |
|---|
| 403 | # urRight == 1 |
|---|
| 404 | .names urRight _n60 _n5f |
|---|
| 405 | .def 0 |
|---|
| 406 | - =urRight 1 |
|---|
| 407 | # urLeft == 1 || urRight == 1 |
|---|
| 408 | .names _n5d _n5f _n61 |
|---|
| 409 | .def 1 |
|---|
| 410 | 0 0 0 |
|---|
| 411 | .names _n61 _n62 |
|---|
| 412 | 0 1 |
|---|
| 413 | 1 0 |
|---|
| 414 | # (mustGiveParent == 0) || !((urLeft == 1 || urRight == 1)) |
|---|
| 415 | .names _n5b _n62 _n63 |
|---|
| 416 | .def 1 |
|---|
| 417 | 0 0 0 |
|---|
| 418 | .mv _n65 2 myTRUE myFALSE |
|---|
| 419 | .names _n65 |
|---|
| 420 | myTRUE |
|---|
| 421 | # topCell == 0 |
|---|
| 422 | .names topCell _n65 _n64 |
|---|
| 423 | .def 0 |
|---|
| 424 | - =topCell 1 |
|---|
| 425 | .names _n64 _n66 |
|---|
| 426 | 0 1 |
|---|
| 427 | 1 0 |
|---|
| 428 | # ((mustGiveParent == 0) || !((urLeft == 1 || urRight == 1))) && !(topCell == 0) |
|---|
| 429 | .names _n63 _n66 _n67 |
|---|
| 430 | .def 0 |
|---|
| 431 | 1 1 1 |
|---|
| 432 | # holdToken == 0 && (((mustGiveParent == 0) || !((urLeft == 1 || urRight == 1))) && !(topCell == 0)) |
|---|
| 433 | .names _n59 _n67 _n68 |
|---|
| 434 | .def 0 |
|---|
| 435 | 1 1 1 |
|---|
| 436 | .mv _n69 4 idle request lock release |
|---|
| 437 | .names _n69 |
|---|
| 438 | release |
|---|
| 439 | .mv _n6a 4 idle request lock release |
|---|
| 440 | .names _n6a |
|---|
| 441 | idle |
|---|
| 442 | # (holdToken == 0 && (((mustGiveParent == 0) || !((urLeft == 1 || urRight == 1))) && !(topCell == 0))) ? 3 : 0 |
|---|
| 443 | .mv _n6b 4 idle request lock release |
|---|
| 444 | .names _n69 _n6a _n68 _n6b |
|---|
| 445 | - - 0 =_n6a |
|---|
| 446 | - - 1 =_n69 |
|---|
| 447 | .mv _n6c 4 idle request lock release |
|---|
| 448 | .names _n6c |
|---|
| 449 | lock |
|---|
| 450 | # (childOwns == 0) ? 2 : (holdToken == 0 && (((mustGiveParent == 0) || !((urLeft == 1 || urRight == 1))) && !(topCell == 0))) ? 3 : 0 |
|---|
| 451 | .mv _n6d 4 idle request lock release |
|---|
| 452 | .names _n6c _n6b _n57 _n6d |
|---|
| 453 | - - 0 =_n6b |
|---|
| 454 | - - 1 =_n6c |
|---|
| 455 | .mv _n6e 4 idle request lock release |
|---|
| 456 | .names _n6e |
|---|
| 457 | request |
|---|
| 458 | # (holdToken == 1 && (urLeft == 1 || urRight == 1)) ? 1 : (childOwns == 0) ? 2 : (holdToken == 0 && (((mustGiveParent == 0) || !((urLeft == 1 || urRight == 1))) && !(topCell == 0))) ? 3 : 0 |
|---|
| 459 | .mv _n6f 4 idle request lock release |
|---|
| 460 | .names _n6e _n6d _n56 _n6f |
|---|
| 461 | - - 0 =_n6d |
|---|
| 462 | - - 1 =_n6e |
|---|
| 463 | .names _n6f xr$raw_n4e |
|---|
| 464 | - =_n6f |
|---|
| 465 | .mv _n71 2 myTRUE myFALSE |
|---|
| 466 | .names _n71 |
|---|
| 467 | myTRUE |
|---|
| 468 | # xa == 0 |
|---|
| 469 | .names xa _n71 _n70 |
|---|
| 470 | .def 0 |
|---|
| 471 | - =xa 1 |
|---|
| 472 | .names _n70 _n72 |
|---|
| 473 | - =_n70 |
|---|
| 474 | # holdToken = 0 |
|---|
| 475 | .mv holdToken$_n70_n73$true 2 myTRUE myFALSE |
|---|
| 476 | .names holdToken$_n70_n73$true |
|---|
| 477 | myTRUE |
|---|
| 478 | .mv _n75 2 myTRUE myFALSE |
|---|
| 479 | .names _n75 |
|---|
| 480 | myTRUE |
|---|
| 481 | # giveChild == 0 |
|---|
| 482 | .names giveChild _n75 _n74 |
|---|
| 483 | .def 0 |
|---|
| 484 | - =giveChild 1 |
|---|
| 485 | .names _n74 _n76 |
|---|
| 486 | - =_n74 |
|---|
| 487 | # holdToken = 1 |
|---|
| 488 | .mv holdToken$_n74_n77$true 2 myTRUE myFALSE |
|---|
| 489 | .names holdToken$_n74_n77$true |
|---|
| 490 | myFALSE |
|---|
| 491 | .mv _n79 4 idle request lock release |
|---|
| 492 | .names _n79 |
|---|
| 493 | release |
|---|
| 494 | # urLeft == 3 |
|---|
| 495 | .names urLeft _n79 _n78 |
|---|
| 496 | .def 0 |
|---|
| 497 | - =urLeft 1 |
|---|
| 498 | .mv _n7b 4 idle request lock release |
|---|
| 499 | .names _n7b |
|---|
| 500 | release |
|---|
| 501 | # urRight == 3 |
|---|
| 502 | .names urRight _n7b _n7a |
|---|
| 503 | .def 0 |
|---|
| 504 | - =urRight 1 |
|---|
| 505 | # urLeft == 3 || urRight == 3 |
|---|
| 506 | .names _n78 _n7a _n7c |
|---|
| 507 | .def 1 |
|---|
| 508 | 0 0 0 |
|---|
| 509 | .names _n7c _n7d |
|---|
| 510 | - =_n7c |
|---|
| 511 | # holdToken = 0 |
|---|
| 512 | .mv holdToken$_n7c_n7e$true 2 myTRUE myFALSE |
|---|
| 513 | .names holdToken$_n7c_n7e$true |
|---|
| 514 | myTRUE |
|---|
| 515 | .mv _n80 4 idle request lock release |
|---|
| 516 | .names _n80 |
|---|
| 517 | release |
|---|
| 518 | # xr == 3 |
|---|
| 519 | .names xr _n80 _n7f |
|---|
| 520 | .def 0 |
|---|
| 521 | - =xr 1 |
|---|
| 522 | .names _n7f _n81 |
|---|
| 523 | - =_n7f |
|---|
| 524 | # holdToken = 1 |
|---|
| 525 | .mv holdToken$_n7f_n82$true 2 myTRUE myFALSE |
|---|
| 526 | .names holdToken$_n7f_n82$true |
|---|
| 527 | myFALSE |
|---|
| 528 | # if/else (xr == 3) |
|---|
| 529 | .mv holdToken$_n7f$raw_n85 2 myTRUE myFALSE |
|---|
| 530 | .names holdToken$_n7f_n82$true holdToken _n7f holdToken$_n7f$raw_n85 |
|---|
| 531 | - - 0 =holdToken |
|---|
| 532 | - - 1 =holdToken$_n7f_n82$true |
|---|
| 533 | # if/else (urLeft == 3 || urRight == 3) |
|---|
| 534 | .mv holdToken$_n7c$raw_n87 2 myTRUE myFALSE |
|---|
| 535 | .names holdToken$_n7c_n7e$true holdToken$_n7f$raw_n85 _n7c holdToken$_n7c$raw_n87 |
|---|
| 536 | - - 0 =holdToken$_n7f$raw_n85 |
|---|
| 537 | - - 1 =holdToken$_n7c_n7e$true |
|---|
| 538 | # if/else (giveChild == 0) |
|---|
| 539 | .mv holdToken$_n74$raw_n8b 2 myTRUE myFALSE |
|---|
| 540 | .names holdToken$_n74_n77$true holdToken$_n7c$raw_n87 _n74 holdToken$_n74$raw_n8b |
|---|
| 541 | - - 0 =holdToken$_n7c$raw_n87 |
|---|
| 542 | - - 1 =holdToken$_n74_n77$true |
|---|
| 543 | # if/else (xa == 0) |
|---|
| 544 | .mv holdToken$_n70$raw_n8f 2 myTRUE myFALSE |
|---|
| 545 | .names holdToken$_n70_n73$true holdToken$_n74$raw_n8b _n70 holdToken$_n70$raw_n8f |
|---|
| 546 | - - 0 =holdToken$_n74$raw_n8b |
|---|
| 547 | - - 1 =holdToken$_n70_n73$true |
|---|
| 548 | .mv _n93 2 myTRUE myFALSE |
|---|
| 549 | .names _n93 |
|---|
| 550 | myTRUE |
|---|
| 551 | # uaLeft == 0 |
|---|
| 552 | .names uaLeft _n93 _n92 |
|---|
| 553 | .def 0 |
|---|
| 554 | - =uaLeft 1 |
|---|
| 555 | .names _n92 _n94 |
|---|
| 556 | - =_n92 |
|---|
| 557 | # prevLeft = 0 |
|---|
| 558 | .mv prevLeft$_n92_n95$true 2 myTRUE myFALSE |
|---|
| 559 | .names prevLeft$_n92_n95$true |
|---|
| 560 | myTRUE |
|---|
| 561 | # prevRight = 1 |
|---|
| 562 | .mv prevRight$_n92_n96$true 2 myTRUE myFALSE |
|---|
| 563 | .names prevRight$_n92_n96$true |
|---|
| 564 | myFALSE |
|---|
| 565 | .mv _n98 2 myTRUE myFALSE |
|---|
| 566 | .names _n98 |
|---|
| 567 | myTRUE |
|---|
| 568 | # uaRight == 0 |
|---|
| 569 | .names uaRight _n98 _n97 |
|---|
| 570 | .def 0 |
|---|
| 571 | - =uaRight 1 |
|---|
| 572 | .names _n97 _n99 |
|---|
| 573 | - =_n97 |
|---|
| 574 | # prevLeft = 1 |
|---|
| 575 | .mv prevLeft$_n97_n9a$true 2 myTRUE myFALSE |
|---|
| 576 | .names prevLeft$_n97_n9a$true |
|---|
| 577 | myFALSE |
|---|
| 578 | # prevRight = 0 |
|---|
| 579 | .mv prevRight$_n97_n9b$true 2 myTRUE myFALSE |
|---|
| 580 | .names prevRight$_n97_n9b$true |
|---|
| 581 | myTRUE |
|---|
| 582 | # if/else (uaRight == 0) |
|---|
| 583 | .mv prevLeft$_n97$raw_na2 2 myTRUE myFALSE |
|---|
| 584 | .names prevLeft$_n97_n9a$true prevLeft _n97 prevLeft$_n97$raw_na2 |
|---|
| 585 | - - 0 =prevLeft |
|---|
| 586 | - - 1 =prevLeft$_n97_n9a$true |
|---|
| 587 | .mv prevRight$_n97$raw_na4 2 myTRUE myFALSE |
|---|
| 588 | .names prevRight$_n97_n9b$true prevRight _n97 prevRight$_n97$raw_na4 |
|---|
| 589 | - - 0 =prevRight |
|---|
| 590 | - - 1 =prevRight$_n97_n9b$true |
|---|
| 591 | # if/else (uaLeft == 0) |
|---|
| 592 | .mv prevLeft$_n92$raw_na9 2 myTRUE myFALSE |
|---|
| 593 | .names prevLeft$_n92_n95$true prevLeft$_n97$raw_na2 _n92 prevLeft$_n92$raw_na9 |
|---|
| 594 | - - 0 =prevLeft$_n97$raw_na2 |
|---|
| 595 | - - 1 =prevLeft$_n92_n95$true |
|---|
| 596 | .mv prevRight$_n92$raw_nab 2 myTRUE myFALSE |
|---|
| 597 | .names prevRight$_n92_n96$true prevRight$_n97$raw_na4 _n92 prevRight$_n92$raw_nab |
|---|
| 598 | - - 0 =prevRight$_n97$raw_na4 |
|---|
| 599 | - - 1 =prevRight$_n92_n96$true |
|---|
| 600 | .mv _nb3 4 idle request lock release |
|---|
| 601 | .names _nb3 |
|---|
| 602 | release |
|---|
| 603 | # urLeft == 3 |
|---|
| 604 | .names urLeft _nb3 _nb2 |
|---|
| 605 | .def 0 |
|---|
| 606 | - =urLeft 1 |
|---|
| 607 | .names _nb2 _nb4 |
|---|
| 608 | - =_nb2 |
|---|
| 609 | # processedLeft = 0 |
|---|
| 610 | .mv processedLeft$_nb2_nb5$true 2 myTRUE myFALSE |
|---|
| 611 | .names processedLeft$_nb2_nb5$true |
|---|
| 612 | myTRUE |
|---|
| 613 | .mv _nb7 4 idle request lock release |
|---|
| 614 | .names _nb7 |
|---|
| 615 | release |
|---|
| 616 | # urRight == 3 |
|---|
| 617 | .names urRight _nb7 _nb6 |
|---|
| 618 | .def 0 |
|---|
| 619 | - =urRight 1 |
|---|
| 620 | .names _nb6 _nb8 |
|---|
| 621 | - =_nb6 |
|---|
| 622 | # processedRight = 0 |
|---|
| 623 | .mv processedRight$_nb6_nb9$true 2 myTRUE myFALSE |
|---|
| 624 | .names processedRight$_nb6_nb9$true |
|---|
| 625 | myTRUE |
|---|
| 626 | .mv _nbb 2 myTRUE myFALSE |
|---|
| 627 | .names _nbb |
|---|
| 628 | myTRUE |
|---|
| 629 | # processedLeft == 0 |
|---|
| 630 | .names processedLeft _nbb _nba |
|---|
| 631 | .def 0 |
|---|
| 632 | - =processedLeft 1 |
|---|
| 633 | .mv _nbd 2 myTRUE myFALSE |
|---|
| 634 | .names _nbd |
|---|
| 635 | myTRUE |
|---|
| 636 | # processedRight == 0 |
|---|
| 637 | .names processedRight _nbd _nbc |
|---|
| 638 | .def 0 |
|---|
| 639 | - =processedRight 1 |
|---|
| 640 | # (processedLeft == 0) && (processedRight == 0) |
|---|
| 641 | .names _nba _nbc _nbe |
|---|
| 642 | .def 0 |
|---|
| 643 | 1 1 1 |
|---|
| 644 | .names _nbe _nbf |
|---|
| 645 | - =_nbe |
|---|
| 646 | # processedLeft = 1 |
|---|
| 647 | .mv processedLeft$_nbe_nc0$true 2 myTRUE myFALSE |
|---|
| 648 | .names processedLeft$_nbe_nc0$true |
|---|
| 649 | myFALSE |
|---|
| 650 | # processedRight = 1 |
|---|
| 651 | .mv processedRight$_nbe_nc1$true 2 myTRUE myFALSE |
|---|
| 652 | .names processedRight$_nbe_nc1$true |
|---|
| 653 | myFALSE |
|---|
| 654 | # if/else ((processedLeft == 0) && (processedRight == 0)) |
|---|
| 655 | .mv processedLeft$_nbe$raw_ncc 2 myTRUE myFALSE |
|---|
| 656 | .names processedLeft$_nbe_nc0$true processedLeft _nbe processedLeft$_nbe$raw_ncc |
|---|
| 657 | - - 0 =processedLeft |
|---|
| 658 | - - 1 =processedLeft$_nbe_nc0$true |
|---|
| 659 | .mv processedRight$_nbe$raw_nce 2 myTRUE myFALSE |
|---|
| 660 | .names processedRight$_nbe_nc1$true processedRight _nbe processedRight$_nbe$raw_nce |
|---|
| 661 | - - 0 =processedRight |
|---|
| 662 | - - 1 =processedRight$_nbe_nc1$true |
|---|
| 663 | # if/else (urRight == 3) |
|---|
| 664 | .mv processedRight$_nb6$raw_nd9 2 myTRUE myFALSE |
|---|
| 665 | .names processedRight$_nb6_nb9$true processedRight$_nbe$raw_nce _nb6 processedRight$_nb6$raw_nd9 |
|---|
| 666 | - - 0 =processedRight$_nbe$raw_nce |
|---|
| 667 | - - 1 =processedRight$_nb6_nb9$true |
|---|
| 668 | .mv processedLeft$_nb6$raw_ne0 2 myTRUE myFALSE |
|---|
| 669 | .names processedLeft processedLeft$_nbe$raw_ncc _nb6 processedLeft$_nb6$raw_ne0 |
|---|
| 670 | - - 0 =processedLeft$_nbe$raw_ncc |
|---|
| 671 | - - 1 =processedLeft |
|---|
| 672 | # if/else (urLeft == 3) |
|---|
| 673 | .mv processedLeft$_nb2$raw_ne9 2 myTRUE myFALSE |
|---|
| 674 | .names processedLeft$_nb2_nb5$true processedLeft$_nb6$raw_ne0 _nb2 processedLeft$_nb2$raw_ne9 |
|---|
| 675 | - - 0 =processedLeft$_nb6$raw_ne0 |
|---|
| 676 | - - 1 =processedLeft$_nb2_nb5$true |
|---|
| 677 | .mv processedRight$_nb2$raw_nf3 2 myTRUE myFALSE |
|---|
| 678 | .names processedRight processedRight$_nb6$raw_nd9 _nb2 processedRight$_nb2$raw_nf3 |
|---|
| 679 | - - 0 =processedRight$_nb6$raw_nd9 |
|---|
| 680 | - - 1 =processedRight |
|---|
| 681 | # conflict arbitrators |
|---|
| 682 | .names _nb4 _nb8 _nbf _nf6 |
|---|
| 683 | .def 0 |
|---|
| 684 | 1 - - 1 |
|---|
| 685 | 0 0 1 1 |
|---|
| 686 | .mv _nf7 2 myTRUE myFALSE |
|---|
| 687 | .names _nf6 processedLeft$_nb2$raw_ne9 processedLeft _nf7 |
|---|
| 688 | 1 - - =processedLeft$_nb2$raw_ne9 |
|---|
| 689 | 0 - - =processedLeft |
|---|
| 690 | .names _n94 _n99 _n104 |
|---|
| 691 | .def 0 |
|---|
| 692 | 1 - 1 |
|---|
| 693 | 0 1 1 |
|---|
| 694 | .mv _n105 2 myTRUE myFALSE |
|---|
| 695 | .names _n104 prevLeft$_n92$raw_na9 prevLeft _n105 |
|---|
| 696 | 1 - - =prevLeft$_n92$raw_na9 |
|---|
| 697 | 0 - - =prevLeft |
|---|
| 698 | .names _n72 _n76 _n7d _n81 _n112 |
|---|
| 699 | .def 0 |
|---|
| 700 | 1 - - - 1 |
|---|
| 701 | 0 1 - - 1 |
|---|
| 702 | 0 0 1 - 1 |
|---|
| 703 | 0 0 0 1 1 |
|---|
| 704 | .mv _n113 2 myTRUE myFALSE |
|---|
| 705 | .names _n112 holdToken$_n70$raw_n8f holdToken _n113 |
|---|
| 706 | 1 - - =holdToken$_n70$raw_n8f |
|---|
| 707 | 0 - - =holdToken |
|---|
| 708 | .names _nb4 _nb8 _nbf _n120 |
|---|
| 709 | .def 0 |
|---|
| 710 | 0 1 - 1 |
|---|
| 711 | 0 0 1 1 |
|---|
| 712 | .mv _n121 2 myTRUE myFALSE |
|---|
| 713 | .names _n120 processedRight$_nb2$raw_nf3 processedRight _n121 |
|---|
| 714 | 1 - - =processedRight$_nb2$raw_nf3 |
|---|
| 715 | 0 - - =processedRight |
|---|
| 716 | .names uaLeft$raw_n26 uaLeft |
|---|
| 717 | - =uaLeft$raw_n26 |
|---|
| 718 | .names giveChild$raw_n1d giveChild |
|---|
| 719 | - =giveChild$raw_n1d |
|---|
| 720 | .names mustGiveParent$raw_n6 mustGiveParent |
|---|
| 721 | - =mustGiveParent$raw_n6 |
|---|
| 722 | .names xr$raw_n4e xr |
|---|
| 723 | - =xr$raw_n4e |
|---|
| 724 | .names uaRight$raw_n3a uaRight |
|---|
| 725 | - =uaRight$raw_n3a |
|---|
| 726 | .names childOwns$raw_n14 childOwns |
|---|
| 727 | - =childOwns$raw_n14 |
|---|
| 728 | .names _n94 _n99 _n12e |
|---|
| 729 | .def 0 |
|---|
| 730 | 1 - 1 |
|---|
| 731 | 0 1 1 |
|---|
| 732 | .mv _n12f 2 myTRUE myFALSE |
|---|
| 733 | .names _n12e prevRight$_n92$raw_nab prevRight _n12f |
|---|
| 734 | 1 - - =prevRight$_n92$raw_nab |
|---|
| 735 | 0 - - =prevRight |
|---|
| 736 | # non-blocking assignments |
|---|
| 737 | # latches |
|---|
| 738 | .r prevLeft$raw_n2 prevLeft |
|---|
| 739 | - =prevLeft$raw_n2 |
|---|
| 740 | .latch _n105 prevLeft |
|---|
| 741 | .r processedLeft$raw_n4 processedLeft |
|---|
| 742 | - =processedLeft$raw_n4 |
|---|
| 743 | .latch _nf7 processedLeft |
|---|
| 744 | .r processedRight$raw_n5 processedRight |
|---|
| 745 | - =processedRight$raw_n5 |
|---|
| 746 | .latch _n121 processedRight |
|---|
| 747 | .r holdToken$raw_n13 holdToken |
|---|
| 748 | - =holdToken$raw_n13 |
|---|
| 749 | .latch _n113 holdToken |
|---|
| 750 | .r prevRight$raw_n3 prevRight |
|---|
| 751 | - =prevRight$raw_n3 |
|---|
| 752 | .latch _n12f prevRight |
|---|
| 753 | # quasi-continuous assignment |
|---|
| 754 | .end |
|---|
| 755 | |
|---|
| 756 | |
|---|
| 757 | .model fourCells |
|---|
| 758 | # I/O ports |
|---|
| 759 | .inputs sa |
|---|
| 760 | .outputs sr |
|---|
| 761 | .mv constFALSE 2 myTRUE myFALSE |
|---|
| 762 | .mv sa 2 myTRUE myFALSE |
|---|
| 763 | .mv ur1 4 idle request lock release |
|---|
| 764 | .mv xa 2 myTRUE myFALSE |
|---|
| 765 | .mv ur2 4 idle request lock release |
|---|
| 766 | .mv yr 4 idle request lock release |
|---|
| 767 | .mv ur3 4 idle request lock release |
|---|
| 768 | .mv ua1 2 myTRUE myFALSE |
|---|
| 769 | .mv ur4 4 idle request lock release |
|---|
| 770 | .mv ua2 2 myTRUE myFALSE |
|---|
| 771 | .mv ua3 2 myTRUE myFALSE |
|---|
| 772 | .mv sr 4 idle request lock release |
|---|
| 773 | .mv ua4 2 myTRUE myFALSE |
|---|
| 774 | .mv xr 4 idle request lock release |
|---|
| 775 | .mv ya 2 myTRUE myFALSE |
|---|
| 776 | .mv constTRUE 2 myTRUE myFALSE |
|---|
| 777 | # assign constTRUE = 0 |
|---|
| 778 | .mv constTRUE$raw_n13c 2 myTRUE myFALSE |
|---|
| 779 | .names constTRUE$raw_n13c |
|---|
| 780 | myTRUE |
|---|
| 781 | # assign constFALSE = 1 |
|---|
| 782 | .mv constFALSE$raw_n13d 2 myTRUE myFALSE |
|---|
| 783 | .names constFALSE$raw_n13d |
|---|
| 784 | myFALSE |
|---|
| 785 | .subckt arbitCell C0 topCell=constFALSE urLeft=xr urRight=yr uaLeft=xa uaRight=ya xr=sr xa=sa |
|---|
| 786 | .subckt arbitCell C1 topCell=constFALSE urLeft=ur1 urRight=ur2 uaLeft=ua1 uaRight=ua2 xr=xr xa=xa |
|---|
| 787 | .subckt arbitCell C2 topCell=constFALSE urLeft=ur3 urRight=ur4 uaLeft=ua3 uaRight=ua4 xr=yr xa=ya |
|---|
| 788 | .subckt procModel P1 ack=ua1 req=ur1 |
|---|
| 789 | .subckt procModel P2 ack=ua2 req=ur2 |
|---|
| 790 | .subckt procModel P3 ack=ua3 req=ur3 |
|---|
| 791 | .subckt procModel P4 ack=ua4 req=ur4 |
|---|
| 792 | # conflict arbitrators |
|---|
| 793 | .names constFALSE$raw_n13d constFALSE |
|---|
| 794 | - =constFALSE$raw_n13d |
|---|
| 795 | .names constTRUE$raw_n13c constTRUE |
|---|
| 796 | - =constTRUE$raw_n13c |
|---|
| 797 | # non-blocking assignments |
|---|
| 798 | # latches |
|---|
| 799 | # quasi-continuous assignment |
|---|
| 800 | .end |
|---|
| 801 | |
|---|
| 802 | |
|---|
| 803 | .model procModel |
|---|
| 804 | # I/O ports |
|---|
| 805 | .outputs req |
|---|
| 806 | .inputs ack |
|---|
| 807 | .mv req 4 idle request lock release |
|---|
| 808 | .mv procState 4 idle request lock release |
|---|
| 809 | .mv ack 2 myTRUE myFALSE |
|---|
| 810 | # assign req = procState |
|---|
| 811 | .mv req$raw_n13e 4 idle request lock release |
|---|
| 812 | .names procState req$raw_n13e |
|---|
| 813 | - =procState |
|---|
| 814 | # assign randChoice = $NDset ( 0,1 ) |
|---|
| 815 | .names randChoice |
|---|
| 816 | 0 |
|---|
| 817 | 1 |
|---|
| 818 | # procState = 0 |
|---|
| 819 | .mv procState$raw_n141 4 idle request lock release |
|---|
| 820 | .names procState$raw_n141 |
|---|
| 821 | idle |
|---|
| 822 | # non-blocking assignments for initial |
|---|
| 823 | .mv _n143 4 idle request lock release |
|---|
| 824 | .names _n143 |
|---|
| 825 | idle |
|---|
| 826 | # procState == 0 |
|---|
| 827 | .names procState _n143 _n142 |
|---|
| 828 | .def 0 |
|---|
| 829 | - =procState 1 |
|---|
| 830 | .names _n145 |
|---|
| 831 | 1 |
|---|
| 832 | # randChoice == 1 |
|---|
| 833 | .names randChoice _n145 _n146 |
|---|
| 834 | .def 0 |
|---|
| 835 | 0 1 1 |
|---|
| 836 | 1 0 1 |
|---|
| 837 | .names _n146 _n144 |
|---|
| 838 | 0 1 |
|---|
| 839 | 1 0 |
|---|
| 840 | # procState == 0 && (randChoice == 1) |
|---|
| 841 | .names _n142 _n144 _n148 |
|---|
| 842 | .def 0 |
|---|
| 843 | 1 1 1 |
|---|
| 844 | .names _n148 _n149 |
|---|
| 845 | - =_n148 |
|---|
| 846 | # procState = 1 |
|---|
| 847 | .mv procState$_n148_n14a$true 4 idle request lock release |
|---|
| 848 | .names procState$_n148_n14a$true |
|---|
| 849 | request |
|---|
| 850 | .mv _n14c 4 idle request lock release |
|---|
| 851 | .names _n14c |
|---|
| 852 | request |
|---|
| 853 | # procState == 1 |
|---|
| 854 | .names procState _n14c _n14b |
|---|
| 855 | .def 0 |
|---|
| 856 | - =procState 1 |
|---|
| 857 | .mv _n14e 2 myTRUE myFALSE |
|---|
| 858 | .names _n14e |
|---|
| 859 | myTRUE |
|---|
| 860 | # ack == 0 |
|---|
| 861 | .names ack _n14e _n14d |
|---|
| 862 | .def 0 |
|---|
| 863 | - =ack 1 |
|---|
| 864 | # procState == 1 && ack == 0 |
|---|
| 865 | .names _n14b _n14d _n14f |
|---|
| 866 | .def 0 |
|---|
| 867 | 1 1 1 |
|---|
| 868 | .names _n14f _n150 |
|---|
| 869 | - =_n14f |
|---|
| 870 | # procState = 2 |
|---|
| 871 | .mv procState$_n14f_n151$true 4 idle request lock release |
|---|
| 872 | .names procState$_n14f_n151$true |
|---|
| 873 | lock |
|---|
| 874 | .mv _n153 4 idle request lock release |
|---|
| 875 | .names _n153 |
|---|
| 876 | lock |
|---|
| 877 | # procState == 2 |
|---|
| 878 | .names procState _n153 _n152 |
|---|
| 879 | .def 0 |
|---|
| 880 | - =procState 1 |
|---|
| 881 | .names _n155 |
|---|
| 882 | 1 |
|---|
| 883 | # randChoice == 1 |
|---|
| 884 | .names randChoice _n155 _n156 |
|---|
| 885 | .def 0 |
|---|
| 886 | 0 1 1 |
|---|
| 887 | 1 0 1 |
|---|
| 888 | .names _n156 _n154 |
|---|
| 889 | 0 1 |
|---|
| 890 | 1 0 |
|---|
| 891 | # procState == 2 && (randChoice == 1) |
|---|
| 892 | .names _n152 _n154 _n158 |
|---|
| 893 | .def 0 |
|---|
| 894 | 1 1 1 |
|---|
| 895 | .names _n158 _n159 |
|---|
| 896 | - =_n158 |
|---|
| 897 | # procState = 3 |
|---|
| 898 | .mv procState$_n158_n15a$true 4 idle request lock release |
|---|
| 899 | .names procState$_n158_n15a$true |
|---|
| 900 | release |
|---|
| 901 | .mv _n15c 4 idle request lock release |
|---|
| 902 | .names _n15c |
|---|
| 903 | release |
|---|
| 904 | # procState == 3 |
|---|
| 905 | .names procState _n15c _n15b |
|---|
| 906 | .def 0 |
|---|
| 907 | - =procState 1 |
|---|
| 908 | .names _n15b _n15d |
|---|
| 909 | - =_n15b |
|---|
| 910 | # procState = 0 |
|---|
| 911 | .mv procState$_n15b_n15e$true 4 idle request lock release |
|---|
| 912 | .names procState$_n15b_n15e$true |
|---|
| 913 | idle |
|---|
| 914 | # if/else (procState == 3) |
|---|
| 915 | .mv procState$_n15b$raw_n161 4 idle request lock release |
|---|
| 916 | .names procState$_n15b_n15e$true procState _n15b procState$_n15b$raw_n161 |
|---|
| 917 | - - 0 =procState |
|---|
| 918 | - - 1 =procState$_n15b_n15e$true |
|---|
| 919 | # if/else (procState == 2 && (randChoice == 1)) |
|---|
| 920 | .mv procState$_n158$raw_n163 4 idle request lock release |
|---|
| 921 | .names procState$_n158_n15a$true procState$_n15b$raw_n161 _n158 procState$_n158$raw_n163 |
|---|
| 922 | - - 0 =procState$_n15b$raw_n161 |
|---|
| 923 | - - 1 =procState$_n158_n15a$true |
|---|
| 924 | # if/else (procState == 1 && ack == 0) |
|---|
| 925 | .mv procState$_n14f$raw_n167 4 idle request lock release |
|---|
| 926 | .names procState$_n14f_n151$true procState$_n158$raw_n163 _n14f procState$_n14f$raw_n167 |
|---|
| 927 | - - 0 =procState$_n158$raw_n163 |
|---|
| 928 | - - 1 =procState$_n14f_n151$true |
|---|
| 929 | # if/else (procState == 0 && (randChoice == 1)) |
|---|
| 930 | .mv procState$_n148$raw_n16b 4 idle request lock release |
|---|
| 931 | .names procState$_n148_n14a$true procState$_n14f$raw_n167 _n148 procState$_n148$raw_n16b |
|---|
| 932 | - - 0 =procState$_n14f$raw_n167 |
|---|
| 933 | - - 1 =procState$_n148_n14a$true |
|---|
| 934 | # conflict arbitrators |
|---|
| 935 | .names req$raw_n13e req |
|---|
| 936 | - =req$raw_n13e |
|---|
| 937 | .names _n149 _n150 _n159 _n15d _n16e |
|---|
| 938 | .def 0 |
|---|
| 939 | 1 - - - 1 |
|---|
| 940 | 0 1 - - 1 |
|---|
| 941 | 0 0 1 - 1 |
|---|
| 942 | 0 0 0 1 1 |
|---|
| 943 | .mv _n16f 4 idle request lock release |
|---|
| 944 | .names _n16e procState$_n148$raw_n16b procState _n16f |
|---|
| 945 | 1 - - =procState$_n148$raw_n16b |
|---|
| 946 | 0 - - =procState |
|---|
| 947 | # non-blocking assignments |
|---|
| 948 | # latches |
|---|
| 949 | .r procState$raw_n141 procState |
|---|
| 950 | - =procState$raw_n141 |
|---|
| 951 | .latch _n16f procState |
|---|
| 952 | # quasi-continuous assignment |
|---|
| 953 | .end |
|---|
| 954 | |
|---|
| 955 | |
|---|
![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
