| 1 | # vl2mv ping_pong_new.v |
|---|
| 2 | # version: 0.2 |
|---|
| 3 | # date: 11:17:06 12/11/95 (PST) |
|---|
| 4 | .model ping_pong |
|---|
| 5 | # I/O ports |
|---|
| 6 | |
|---|
| 7 | .mv state_ball_2 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 8 | .mv state_ball_1 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 9 | .mv action_A 2 HIT IDLE |
|---|
| 10 | .mv state_B 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 11 | .mv action_B 2 HIT IDLE |
|---|
| 12 | .mv state_A 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 13 | .subckt player player_A opponent=action_B out=action_A state=state_A |
|---|
| 14 | .subckt player player_B opponent=action_A out=action_B state=state_B |
|---|
| 15 | .mv _n0 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 16 | .names _n0 |
|---|
| 17 | TO_A |
|---|
| 18 | .subckt ball ball_1 action_A=action_A action_B=action_B state=state_ball_1 init=_n0 |
|---|
| 19 | .mv _n1 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 20 | .names _n1 |
|---|
| 21 | TO_B |
|---|
| 22 | .subckt ball ball_2 action_A=action_A action_B=action_B state=state_ball_2 init=_n1 |
|---|
| 23 | # conflict arbitrators |
|---|
| 24 | # non-blocking assignments |
|---|
| 25 | # latches |
|---|
| 26 | # quasi-continuous assignment |
|---|
| 27 | .end |
|---|
| 28 | |
|---|
| 29 | |
|---|
| 30 | .model player |
|---|
| 31 | # I/O ports |
|---|
| 32 | .outputs out |
|---|
| 33 | .outputs state |
|---|
| 34 | .inputs opponent |
|---|
| 35 | |
|---|
| 36 | .mv out 2 HIT IDLE |
|---|
| 37 | .mv r_state 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 38 | .mv state 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 39 | .mv opponent 2 HIT IDLE |
|---|
| 40 | # assign out = (state == 0) ? 0 : 1 |
|---|
| 41 | .mv out$raw_n2 2 HIT IDLE |
|---|
| 42 | .mv _n4 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 43 | .names _n4 |
|---|
| 44 | HIT |
|---|
| 45 | # state == 0 |
|---|
| 46 | .names state _n4 _n3 |
|---|
| 47 | .def 0 |
|---|
| 48 | - =state 1 |
|---|
| 49 | .mv _n5 2 HIT IDLE |
|---|
| 50 | .names _n5 |
|---|
| 51 | HIT |
|---|
| 52 | .mv _n6 2 HIT IDLE |
|---|
| 53 | .names _n6 |
|---|
| 54 | IDLE |
|---|
| 55 | # (state == 0) ? 0 : 1 |
|---|
| 56 | .mv _n7 2 HIT IDLE |
|---|
| 57 | .names _n5 _n6 _n3 _n7 |
|---|
| 58 | - - 0 =_n6 |
|---|
| 59 | - - 1 =_n5 |
|---|
| 60 | .names _n7 out$raw_n2 |
|---|
| 61 | - =_n7 |
|---|
| 62 | # assign r_state = $NDset ( 2,0 ) |
|---|
| 63 | .names r_state |
|---|
| 64 | WAIT_COMING |
|---|
| 65 | HIT |
|---|
| 66 | # state = 0 |
|---|
| 67 | .mv state$raw_na 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 68 | .names state$raw_na |
|---|
| 69 | HIT |
|---|
| 70 | # non-blocking assignments for initial |
|---|
| 71 | .mv _nd 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 72 | .names _nd |
|---|
| 73 | HIT |
|---|
| 74 | .names state _nd _nc |
|---|
| 75 | .def 0 |
|---|
| 76 | - =state 1 |
|---|
| 77 | .names _nc _nb |
|---|
| 78 | 1 1 |
|---|
| 79 | 0 0 |
|---|
| 80 | .mv _nf 2 HIT IDLE |
|---|
| 81 | .names _nf |
|---|
| 82 | IDLE |
|---|
| 83 | # opponent == 1 |
|---|
| 84 | .names opponent _nf _ne |
|---|
| 85 | .def 0 |
|---|
| 86 | - =opponent 1 |
|---|
| 87 | .names _ne _n10 |
|---|
| 88 | - =_ne |
|---|
| 89 | # state = 1 |
|---|
| 90 | .mv state$_ne_n11$true 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 91 | .names state$_ne_n11$true |
|---|
| 92 | WAIT_GOING |
|---|
| 93 | .mv _n13 2 HIT IDLE |
|---|
| 94 | .names _n13 |
|---|
| 95 | HIT |
|---|
| 96 | # opponent == 0 |
|---|
| 97 | .names opponent _n13 _n12 |
|---|
| 98 | .def 0 |
|---|
| 99 | - =opponent 1 |
|---|
| 100 | .names _n12 _n14 |
|---|
| 101 | - =_n12 |
|---|
| 102 | # state = 2 |
|---|
| 103 | .mv state$_n12_n15$true 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 104 | .names state$_n12_n15$true |
|---|
| 105 | WAIT_COMING |
|---|
| 106 | # if/else (opponent == 0) |
|---|
| 107 | .mv state$_n12$raw_n18 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 108 | .names state$_n12_n15$true state _n12 state$_n12$raw_n18 |
|---|
| 109 | - - 0 =state |
|---|
| 110 | - - 1 =state$_n12_n15$true |
|---|
| 111 | # if/else (opponent == 1) |
|---|
| 112 | .mv state$_ne$raw_n1a 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 113 | .names state$_ne_n11$true state$_n12$raw_n18 _ne state$_ne$raw_n1a |
|---|
| 114 | - - 0 =state$_n12$raw_n18 |
|---|
| 115 | - - 1 =state$_ne_n11$true |
|---|
| 116 | .mv _n1f 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 117 | .names _n1f |
|---|
| 118 | WAIT_GOING |
|---|
| 119 | .names state _n1f _n1e |
|---|
| 120 | .def 0 |
|---|
| 121 | - =state 1 |
|---|
| 122 | .names _n1e _n1d |
|---|
| 123 | 1 1 |
|---|
| 124 | 0 0 |
|---|
| 125 | .mv _n21 2 HIT IDLE |
|---|
| 126 | .names _n21 |
|---|
| 127 | HIT |
|---|
| 128 | # opponent == 0 |
|---|
| 129 | .names opponent _n21 _n20 |
|---|
| 130 | .def 0 |
|---|
| 131 | - =opponent 1 |
|---|
| 132 | .names _n20 _n22 |
|---|
| 133 | - =_n20 |
|---|
| 134 | # state = 2 |
|---|
| 135 | .mv state$_n20_n23$true 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 136 | .names state$_n20_n23$true |
|---|
| 137 | WAIT_COMING |
|---|
| 138 | # if/else (opponent == 0) |
|---|
| 139 | .mv state$_n20$raw_n26 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 140 | .names state$_n20_n23$true state _n20 state$_n20$raw_n26 |
|---|
| 141 | - - 0 =state |
|---|
| 142 | - - 1 =state$_n20_n23$true |
|---|
| 143 | .mv _n29 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 144 | .names _n29 |
|---|
| 145 | WAIT_COMING |
|---|
| 146 | .names state _n29 _n28 |
|---|
| 147 | .def 0 |
|---|
| 148 | - =state 1 |
|---|
| 149 | .names _n28 _n27 |
|---|
| 150 | 1 1 |
|---|
| 151 | 0 0 |
|---|
| 152 | # state = r_state |
|---|
| 153 | .mv state$_n27_n2a$true 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 154 | .names r_state state$_n27_n2a$true |
|---|
| 155 | - =r_state |
|---|
| 156 | # case (state ) |
|---|
| 157 | .mv state$_n27$raw_n2d 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 158 | .names state$_n27_n2a$true state _n27 state$_n27$raw_n2d |
|---|
| 159 | - - 0 =state |
|---|
| 160 | - - 1 =state$_n27_n2a$true |
|---|
| 161 | .mv state$_n1d$raw_n2f 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 162 | .names state$_n20$raw_n26 state$_n27$raw_n2d _n1d state$_n1d$raw_n2f |
|---|
| 163 | - - 0 =state$_n27$raw_n2d |
|---|
| 164 | - - 1 =state$_n20$raw_n26 |
|---|
| 165 | .mv state$_nb$raw_n33 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 166 | .names state$_ne$raw_n1a state$_n1d$raw_n2f _nb state$_nb$raw_n33 |
|---|
| 167 | - - 0 =state$_n1d$raw_n2f |
|---|
| 168 | - - 1 =state$_ne$raw_n1a |
|---|
| 169 | # conflict arbitrators |
|---|
| 170 | .names out$raw_n2 out |
|---|
| 171 | - =out$raw_n2 |
|---|
| 172 | .names _nb _n10 _n14 _n1d _n22 _n27 _n36 |
|---|
| 173 | .def 0 |
|---|
| 174 | 1 1 - - - - 1 |
|---|
| 175 | 1 0 1 - - - 1 |
|---|
| 176 | 0 - - 1 1 - 1 |
|---|
| 177 | 0 - - 0 - 1 1 |
|---|
| 178 | .mv _n37 3 HIT WAIT_GOING WAIT_COMING |
|---|
| 179 | .names _n36 state$_nb$raw_n33 state _n37 |
|---|
| 180 | 1 - - =state$_nb$raw_n33 |
|---|
| 181 | 0 - - =state |
|---|
| 182 | # non-blocking assignments |
|---|
| 183 | # latches |
|---|
| 184 | .r state$raw_na state |
|---|
| 185 | - =state$raw_na |
|---|
| 186 | .latch _n37 state |
|---|
| 187 | # quasi-continuous assignment |
|---|
| 188 | .end |
|---|
| 189 | |
|---|
| 190 | |
|---|
| 191 | .model ball |
|---|
| 192 | # I/O ports |
|---|
| 193 | .inputs action_A |
|---|
| 194 | .inputs action_B |
|---|
| 195 | .outputs state |
|---|
| 196 | .inputs init |
|---|
| 197 | |
|---|
| 198 | .mv action_A 2 HIT IDLE |
|---|
| 199 | .mv action_B 2 HIT IDLE |
|---|
| 200 | .mv state 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 201 | .mv init 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 202 | # state = init |
|---|
| 203 | .mv state$raw_n3c 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 204 | .names init state$raw_n3c |
|---|
| 205 | - =init |
|---|
| 206 | # non-blocking assignments for initial |
|---|
| 207 | .mv _n3f 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 208 | .names _n3f |
|---|
| 209 | TO_A |
|---|
| 210 | .names state _n3f _n3e |
|---|
| 211 | .def 0 |
|---|
| 212 | - =state 1 |
|---|
| 213 | .names _n3e _n3d |
|---|
| 214 | 1 1 |
|---|
| 215 | 0 0 |
|---|
| 216 | .mv _n41 2 HIT IDLE |
|---|
| 217 | .names _n41 |
|---|
| 218 | HIT |
|---|
| 219 | # action_A == 0 |
|---|
| 220 | .names action_A _n41 _n40 |
|---|
| 221 | .def 0 |
|---|
| 222 | - =action_A 1 |
|---|
| 223 | .names _n40 _n42 |
|---|
| 224 | - =_n40 |
|---|
| 225 | # state = 1 |
|---|
| 226 | .mv state$_n40_n43$true 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 227 | .names state$_n40_n43$true |
|---|
| 228 | TO_B |
|---|
| 229 | .mv _n45 2 HIT IDLE |
|---|
| 230 | .names _n45 |
|---|
| 231 | IDLE |
|---|
| 232 | # action_A == 1 |
|---|
| 233 | .names action_A _n45 _n44 |
|---|
| 234 | .def 0 |
|---|
| 235 | - =action_A 1 |
|---|
| 236 | .mv _n47 2 HIT IDLE |
|---|
| 237 | .names _n47 |
|---|
| 238 | HIT |
|---|
| 239 | # action_B == 0 |
|---|
| 240 | .names action_B _n47 _n46 |
|---|
| 241 | .def 0 |
|---|
| 242 | - =action_B 1 |
|---|
| 243 | # (action_A == 1) && (action_B == 0) |
|---|
| 244 | .names _n44 _n46 _n48 |
|---|
| 245 | .def 0 |
|---|
| 246 | 1 1 1 |
|---|
| 247 | .names _n48 _n49 |
|---|
| 248 | - =_n48 |
|---|
| 249 | # state = 2 |
|---|
| 250 | .mv state$_n48_n4a$true 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 251 | .names state$_n48_n4a$true |
|---|
| 252 | OUT_OF_PLAY |
|---|
| 253 | # if/else ((action_A == 1) && (action_B == 0)) |
|---|
| 254 | .mv state$_n48$raw_n4d 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 255 | .names state$_n48_n4a$true state _n48 state$_n48$raw_n4d |
|---|
| 256 | - - 0 =state |
|---|
| 257 | - - 1 =state$_n48_n4a$true |
|---|
| 258 | # if/else (action_A == 0) |
|---|
| 259 | .mv state$_n40$raw_n4f 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 260 | .names state$_n40_n43$true state$_n48$raw_n4d _n40 state$_n40$raw_n4f |
|---|
| 261 | - - 0 =state$_n48$raw_n4d |
|---|
| 262 | - - 1 =state$_n40_n43$true |
|---|
| 263 | .mv _n54 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 264 | .names _n54 |
|---|
| 265 | TO_B |
|---|
| 266 | .names state _n54 _n53 |
|---|
| 267 | .def 0 |
|---|
| 268 | - =state 1 |
|---|
| 269 | .names _n53 _n52 |
|---|
| 270 | 1 1 |
|---|
| 271 | 0 0 |
|---|
| 272 | .mv _n56 2 HIT IDLE |
|---|
| 273 | .names _n56 |
|---|
| 274 | HIT |
|---|
| 275 | # action_B == 0 |
|---|
| 276 | .names action_B _n56 _n55 |
|---|
| 277 | .def 0 |
|---|
| 278 | - =action_B 1 |
|---|
| 279 | .names _n55 _n57 |
|---|
| 280 | - =_n55 |
|---|
| 281 | # state = 0 |
|---|
| 282 | .mv state$_n55_n58$true 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 283 | .names state$_n55_n58$true |
|---|
| 284 | TO_A |
|---|
| 285 | .mv _n5a 2 HIT IDLE |
|---|
| 286 | .names _n5a |
|---|
| 287 | IDLE |
|---|
| 288 | # action_B == 1 |
|---|
| 289 | .names action_B _n5a _n59 |
|---|
| 290 | .def 0 |
|---|
| 291 | - =action_B 1 |
|---|
| 292 | .mv _n5c 2 HIT IDLE |
|---|
| 293 | .names _n5c |
|---|
| 294 | HIT |
|---|
| 295 | # action_A == 0 |
|---|
| 296 | .names action_A _n5c _n5b |
|---|
| 297 | .def 0 |
|---|
| 298 | - =action_A 1 |
|---|
| 299 | # (action_B == 1) && (action_A == 0) |
|---|
| 300 | .names _n59 _n5b _n5d |
|---|
| 301 | .def 0 |
|---|
| 302 | 1 1 1 |
|---|
| 303 | .names _n5d _n5e |
|---|
| 304 | - =_n5d |
|---|
| 305 | # state = 2 |
|---|
| 306 | .mv state$_n5d_n5f$true 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 307 | .names state$_n5d_n5f$true |
|---|
| 308 | OUT_OF_PLAY |
|---|
| 309 | # if/else ((action_B == 1) && (action_A == 0)) |
|---|
| 310 | .mv state$_n5d$raw_n62 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 311 | .names state$_n5d_n5f$true state _n5d state$_n5d$raw_n62 |
|---|
| 312 | - - 0 =state |
|---|
| 313 | - - 1 =state$_n5d_n5f$true |
|---|
| 314 | # if/else (action_B == 0) |
|---|
| 315 | .mv state$_n55$raw_n64 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 316 | .names state$_n55_n58$true state$_n5d$raw_n62 _n55 state$_n55$raw_n64 |
|---|
| 317 | - - 0 =state$_n5d$raw_n62 |
|---|
| 318 | - - 1 =state$_n55_n58$true |
|---|
| 319 | .mv _n69 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 320 | .names _n69 |
|---|
| 321 | OUT_OF_PLAY |
|---|
| 322 | .names state _n69 _n68 |
|---|
| 323 | .def 0 |
|---|
| 324 | - =state 1 |
|---|
| 325 | .names _n68 _n67 |
|---|
| 326 | 1 1 |
|---|
| 327 | 0 0 |
|---|
| 328 | # state = 2 |
|---|
| 329 | .mv state$_n67_n6a$true 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 330 | .names state$_n67_n6a$true |
|---|
| 331 | OUT_OF_PLAY |
|---|
| 332 | # case (state ) |
|---|
| 333 | .mv state$_n67$raw_n6d 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 334 | .names state$_n67_n6a$true state _n67 state$_n67$raw_n6d |
|---|
| 335 | - - 0 =state |
|---|
| 336 | - - 1 =state$_n67_n6a$true |
|---|
| 337 | .mv state$_n52$raw_n6f 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 338 | .names state$_n55$raw_n64 state$_n67$raw_n6d _n52 state$_n52$raw_n6f |
|---|
| 339 | - - 0 =state$_n67$raw_n6d |
|---|
| 340 | - - 1 =state$_n55$raw_n64 |
|---|
| 341 | .mv state$_n3d$raw_n73 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 342 | .names state$_n40$raw_n4f state$_n52$raw_n6f _n3d state$_n3d$raw_n73 |
|---|
| 343 | - - 0 =state$_n52$raw_n6f |
|---|
| 344 | - - 1 =state$_n40$raw_n4f |
|---|
| 345 | # conflict arbitrators |
|---|
| 346 | .names _n3d _n42 _n49 _n52 _n57 _n5e _n67 _n76 |
|---|
| 347 | .def 0 |
|---|
| 348 | 1 1 - - - - - 1 |
|---|
| 349 | 1 0 1 - - - - 1 |
|---|
| 350 | 0 - - 1 1 - - 1 |
|---|
| 351 | 0 - - 1 0 1 - 1 |
|---|
| 352 | 0 - - 0 - - 1 1 |
|---|
| 353 | .mv _n77 3 TO_A TO_B OUT_OF_PLAY |
|---|
| 354 | .names _n76 state$_n3d$raw_n73 state _n77 |
|---|
| 355 | 1 - - =state$_n3d$raw_n73 |
|---|
| 356 | 0 - - =state |
|---|
| 357 | # non-blocking assignments |
|---|
| 358 | # latches |
|---|
| 359 | .r state$raw_n3c state |
|---|
| 360 | - =state$raw_n3c |
|---|
| 361 | .latch _n77 state |
|---|
| 362 | # quasi-continuous assignment |
|---|
| 363 | .end |
|---|
| 364 | |
|---|
| 365 | |
|---|
![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
