[11] | 1 | # vl2mv ping_pong.v |
---|
| 2 | # version: 0.2 |
---|
| 3 | # date: 11:16:44 12/11/95 (PST) |
---|
| 4 | .model ping_pong |
---|
| 5 | # I/O ports |
---|
| 6 | |
---|
| 7 | .mv action_A 2 HIT NO_HIT |
---|
| 8 | .mv state_B 2 BALL NO_BALL |
---|
| 9 | .mv action_B 2 HIT NO_HIT |
---|
| 10 | .mv state_A 2 BALL NO_BALL |
---|
| 11 | .subckt player player_A opponent=action_B me=action_A state=state_A |
---|
| 12 | .subckt player player_B opponent=action_A me=action_B state=state_B |
---|
| 13 | .subckt never_no_balls nnb state_A=state_A state_B=state_B |
---|
| 14 | .subckt infinitely_often_hit ioh player_action=action_A |
---|
| 15 | # conflict arbitrators |
---|
| 16 | # non-blocking assignments |
---|
| 17 | # latches |
---|
| 18 | # quasi-continuous assignment |
---|
| 19 | .end |
---|
| 20 | |
---|
| 21 | |
---|
| 22 | .model player |
---|
| 23 | # I/O ports |
---|
| 24 | .outputs me |
---|
| 25 | .outputs state |
---|
| 26 | .inputs opponent |
---|
| 27 | |
---|
| 28 | .mv me 2 HIT NO_HIT |
---|
| 29 | .mv state 2 BALL NO_BALL |
---|
| 30 | .mv random 2 HIT NO_HIT |
---|
| 31 | .mv opponent 2 HIT NO_HIT |
---|
| 32 | # state = 0 |
---|
| 33 | .mv state$raw_n0 2 BALL NO_BALL |
---|
| 34 | .names state$raw_n0 |
---|
| 35 | BALL |
---|
| 36 | # non-blocking assignments for initial |
---|
| 37 | # assign random = $NDset ( 0,1 ) |
---|
| 38 | .names random |
---|
| 39 | HIT |
---|
| 40 | NO_HIT |
---|
| 41 | # assign me = (state == BALL ) ? random : 1 |
---|
| 42 | .mv me$raw_n3 2 HIT NO_HIT |
---|
| 43 | .mv _n5 2 BALL NO_BALL |
---|
| 44 | .names _n5 |
---|
| 45 | BALL |
---|
| 46 | # state == 0 |
---|
| 47 | .names state _n5 _n4 |
---|
| 48 | .def 0 |
---|
| 49 | - =state 1 |
---|
| 50 | .mv _n6 2 HIT NO_HIT |
---|
| 51 | .names _n6 |
---|
| 52 | NO_HIT |
---|
| 53 | # (state == 0) ? random : 1 |
---|
| 54 | .mv _n7 2 HIT NO_HIT |
---|
| 55 | .names random _n6 _n4 _n7 |
---|
| 56 | - - 0 =_n6 |
---|
| 57 | - - 1 =random |
---|
| 58 | .names _n7 me$raw_n3 |
---|
| 59 | - =_n7 |
---|
| 60 | .mv _na 2 BALL NO_BALL |
---|
| 61 | .names _na |
---|
| 62 | BALL |
---|
| 63 | .names state _na _n9 |
---|
| 64 | .def 0 |
---|
| 65 | - =state 1 |
---|
| 66 | .names _n9 _n8 |
---|
| 67 | 1 1 |
---|
| 68 | 0 0 |
---|
| 69 | .mv _nc 2 HIT NO_HIT |
---|
| 70 | .names _nc |
---|
| 71 | HIT |
---|
| 72 | # me == 0 |
---|
| 73 | .names me _nc _nb |
---|
| 74 | .def 0 |
---|
| 75 | - =me 1 |
---|
| 76 | .mv _ne 2 HIT NO_HIT |
---|
| 77 | .names _ne |
---|
| 78 | NO_HIT |
---|
| 79 | # opponent == 1 |
---|
| 80 | .names opponent _ne _nd |
---|
| 81 | .def 0 |
---|
| 82 | - =opponent 1 |
---|
| 83 | # (me == 0) && (opponent == 1) |
---|
| 84 | .names _nb _nd _nf |
---|
| 85 | .def 0 |
---|
| 86 | 1 1 1 |
---|
| 87 | .names _nf _n10 |
---|
| 88 | - =_nf |
---|
| 89 | # state = 1 |
---|
| 90 | .mv state$_nf_n11$true 2 BALL NO_BALL |
---|
| 91 | .names state$_nf_n11$true |
---|
| 92 | NO_BALL |
---|
| 93 | # if/else ((me == 0) && (opponent == 1)) |
---|
| 94 | .mv state$_nf$raw_n14 2 BALL NO_BALL |
---|
| 95 | .names state$_nf_n11$true state _nf state$_nf$raw_n14 |
---|
| 96 | - - 0 =state |
---|
| 97 | - - 1 =state$_nf_n11$true |
---|
| 98 | .mv _n17 2 BALL NO_BALL |
---|
| 99 | .names _n17 |
---|
| 100 | NO_BALL |
---|
| 101 | .names state _n17 _n16 |
---|
| 102 | .def 0 |
---|
| 103 | - =state 1 |
---|
| 104 | .names _n16 _n15 |
---|
| 105 | 1 1 |
---|
| 106 | 0 0 |
---|
| 107 | .mv _n19 2 HIT NO_HIT |
---|
| 108 | .names _n19 |
---|
| 109 | HIT |
---|
| 110 | # opponent == 0 |
---|
| 111 | .names opponent _n19 _n18 |
---|
| 112 | .def 0 |
---|
| 113 | - =opponent 1 |
---|
| 114 | .names _n18 _n1a |
---|
| 115 | - =_n18 |
---|
| 116 | # state = 0 |
---|
| 117 | .mv state$_n18_n1b$true 2 BALL NO_BALL |
---|
| 118 | .names state$_n18_n1b$true |
---|
| 119 | BALL |
---|
| 120 | # if/else (opponent == 0) |
---|
| 121 | .mv state$_n18$raw_n1e 2 BALL NO_BALL |
---|
| 122 | .names state$_n18_n1b$true state _n18 state$_n18$raw_n1e |
---|
| 123 | - - 0 =state |
---|
| 124 | - - 1 =state$_n18_n1b$true |
---|
| 125 | # case (state ) |
---|
| 126 | .mv state$_n15$raw_n21 2 BALL NO_BALL |
---|
| 127 | .names state$_n18$raw_n1e state _n15 state$_n15$raw_n21 |
---|
| 128 | - - 0 =state |
---|
| 129 | - - 1 =state$_n18$raw_n1e |
---|
| 130 | .mv state$_n8$raw_n23 2 BALL NO_BALL |
---|
| 131 | .names state$_nf$raw_n14 state$_n15$raw_n21 _n8 state$_n8$raw_n23 |
---|
| 132 | - - 0 =state$_n15$raw_n21 |
---|
| 133 | - - 1 =state$_nf$raw_n14 |
---|
| 134 | # conflict arbitrators |
---|
| 135 | .names me$raw_n3 me |
---|
| 136 | - =me$raw_n3 |
---|
| 137 | .names _n8 _n10 _n15 _n1a _n26 |
---|
| 138 | .def 0 |
---|
| 139 | 1 1 - - 1 |
---|
| 140 | 0 - 1 1 1 |
---|
| 141 | .mv _n27 2 BALL NO_BALL |
---|
| 142 | .names _n26 state$_n8$raw_n23 state _n27 |
---|
| 143 | 1 - - =state$_n8$raw_n23 |
---|
| 144 | 0 - - =state |
---|
| 145 | # non-blocking assignments |
---|
| 146 | # latches |
---|
| 147 | .r state$raw_n0 state |
---|
| 148 | - =state$raw_n0 |
---|
| 149 | .latch _n27 state |
---|
| 150 | # quasi-continuous assignment |
---|
| 151 | .end |
---|
| 152 | |
---|
| 153 | |
---|
| 154 | .model never_no_balls |
---|
| 155 | # I/O ports |
---|
| 156 | .inputs state_B |
---|
| 157 | .inputs state_A |
---|
| 158 | |
---|
| 159 | .mv state_B 2 BALL NO_BALL |
---|
| 160 | .mv state 2 GOOD BAD |
---|
| 161 | .mv state_A 2 BALL NO_BALL |
---|
| 162 | # state = 0 |
---|
| 163 | .mv state$raw_n2b 2 GOOD BAD |
---|
| 164 | .names state$raw_n2b |
---|
| 165 | GOOD |
---|
| 166 | # non-blocking assignments for initial |
---|
| 167 | .mv _n2e 2 GOOD BAD |
---|
| 168 | .names _n2e |
---|
| 169 | GOOD |
---|
| 170 | .names state _n2e _n2d |
---|
| 171 | .def 0 |
---|
| 172 | - =state 1 |
---|
| 173 | .names _n2d _n2c |
---|
| 174 | 1 1 |
---|
| 175 | 0 0 |
---|
| 176 | .mv _n30 2 BALL NO_BALL |
---|
| 177 | .names _n30 |
---|
| 178 | NO_BALL |
---|
| 179 | # state_A == 1 |
---|
| 180 | .names state_A _n30 _n2f |
---|
| 181 | .def 0 |
---|
| 182 | - =state_A 1 |
---|
| 183 | .mv _n32 2 BALL NO_BALL |
---|
| 184 | .names _n32 |
---|
| 185 | NO_BALL |
---|
| 186 | # state_B == 1 |
---|
| 187 | .names state_B _n32 _n31 |
---|
| 188 | .def 0 |
---|
| 189 | - =state_B 1 |
---|
| 190 | # (state_A == 1) && (state_B == 1) |
---|
| 191 | .names _n2f _n31 _n33 |
---|
| 192 | .def 0 |
---|
| 193 | 1 1 1 |
---|
| 194 | .names _n33 _n34 |
---|
| 195 | - =_n33 |
---|
| 196 | # state = 1 |
---|
| 197 | .mv state$_n33_n35$true 2 GOOD BAD |
---|
| 198 | .names state$_n33_n35$true |
---|
| 199 | BAD |
---|
| 200 | # if/else ((state_A == 1) && (state_B == 1)) |
---|
| 201 | .mv state$_n33$raw_n38 2 GOOD BAD |
---|
| 202 | .names state$_n33_n35$true state _n33 state$_n33$raw_n38 |
---|
| 203 | - - 0 =state |
---|
| 204 | - - 1 =state$_n33_n35$true |
---|
| 205 | .mv _n3b 2 GOOD BAD |
---|
| 206 | .names _n3b |
---|
| 207 | BAD |
---|
| 208 | .names state _n3b _n3a |
---|
| 209 | .def 0 |
---|
| 210 | - =state 1 |
---|
| 211 | .names _n3a _n39 |
---|
| 212 | 1 1 |
---|
| 213 | 0 0 |
---|
| 214 | # state = 1 |
---|
| 215 | .mv state$_n39_n3c$true 2 GOOD BAD |
---|
| 216 | .names state$_n39_n3c$true |
---|
| 217 | BAD |
---|
| 218 | # case (state ) |
---|
| 219 | .mv state$_n39$raw_n3f 2 GOOD BAD |
---|
| 220 | .names state$_n39_n3c$true state _n39 state$_n39$raw_n3f |
---|
| 221 | - - 0 =state |
---|
| 222 | - - 1 =state$_n39_n3c$true |
---|
| 223 | .mv state$_n2c$raw_n41 2 GOOD BAD |
---|
| 224 | .names state$_n33$raw_n38 state$_n39$raw_n3f _n2c state$_n2c$raw_n41 |
---|
| 225 | - - 0 =state$_n39$raw_n3f |
---|
| 226 | - - 1 =state$_n33$raw_n38 |
---|
| 227 | # conflict arbitrators |
---|
| 228 | .names _n2c _n34 _n39 _n44 |
---|
| 229 | .def 0 |
---|
| 230 | 1 1 - 1 |
---|
| 231 | 0 - 1 1 |
---|
| 232 | .mv _n45 2 GOOD BAD |
---|
| 233 | .names _n44 state$_n2c$raw_n41 state _n45 |
---|
| 234 | 1 - - =state$_n2c$raw_n41 |
---|
| 235 | 0 - - =state |
---|
| 236 | # non-blocking assignments |
---|
| 237 | # latches |
---|
| 238 | .r state$raw_n2b state |
---|
| 239 | - =state$raw_n2b |
---|
| 240 | .latch _n45 state |
---|
| 241 | # quasi-continuous assignment |
---|
| 242 | .end |
---|
| 243 | |
---|
| 244 | |
---|
| 245 | .model infinitely_often_hit |
---|
| 246 | # I/O ports |
---|
| 247 | .inputs player_action |
---|
| 248 | |
---|
| 249 | .mv player_action 2 HIT NO_HIT |
---|
| 250 | .mv state 2 OKAY PENDING |
---|
| 251 | # state = 0 |
---|
| 252 | .mv state$raw_n47 2 OKAY PENDING |
---|
| 253 | .names state$raw_n47 |
---|
| 254 | OKAY |
---|
| 255 | # non-blocking assignments for initial |
---|
| 256 | .mv _n4a 2 OKAY PENDING |
---|
| 257 | .names _n4a |
---|
| 258 | OKAY |
---|
| 259 | .names state _n4a _n49 |
---|
| 260 | .def 0 |
---|
| 261 | - =state 1 |
---|
| 262 | .names _n49 _n48 |
---|
| 263 | 1 1 |
---|
| 264 | 0 0 |
---|
| 265 | .mv _n4c 2 HIT NO_HIT |
---|
| 266 | .names _n4c |
---|
| 267 | NO_HIT |
---|
| 268 | # player_action == 1 |
---|
| 269 | .names player_action _n4c _n4b |
---|
| 270 | .def 0 |
---|
| 271 | - =player_action 1 |
---|
| 272 | .names _n4b _n4d |
---|
| 273 | - =_n4b |
---|
| 274 | # state = 1 |
---|
| 275 | .mv state$_n4b_n4e$true 2 OKAY PENDING |
---|
| 276 | .names state$_n4b_n4e$true |
---|
| 277 | PENDING |
---|
| 278 | # if/else (player_action == 1) |
---|
| 279 | .mv state$_n4b$raw_n51 2 OKAY PENDING |
---|
| 280 | .names state$_n4b_n4e$true state _n4b state$_n4b$raw_n51 |
---|
| 281 | - - 0 =state |
---|
| 282 | - - 1 =state$_n4b_n4e$true |
---|
| 283 | .mv _n54 2 OKAY PENDING |
---|
| 284 | .names _n54 |
---|
| 285 | PENDING |
---|
| 286 | .names state _n54 _n53 |
---|
| 287 | .def 0 |
---|
| 288 | - =state 1 |
---|
| 289 | .names _n53 _n52 |
---|
| 290 | 1 1 |
---|
| 291 | 0 0 |
---|
| 292 | .mv _n56 2 HIT NO_HIT |
---|
| 293 | .names _n56 |
---|
| 294 | HIT |
---|
| 295 | # player_action == 0 |
---|
| 296 | .names player_action _n56 _n55 |
---|
| 297 | .def 0 |
---|
| 298 | - =player_action 1 |
---|
| 299 | .names _n55 _n57 |
---|
| 300 | - =_n55 |
---|
| 301 | # state = 0 |
---|
| 302 | .mv state$_n55_n58$true 2 OKAY PENDING |
---|
| 303 | .names state$_n55_n58$true |
---|
| 304 | OKAY |
---|
| 305 | # if/else (player_action == 0) |
---|
| 306 | .mv state$_n55$raw_n5b 2 OKAY PENDING |
---|
| 307 | .names state$_n55_n58$true state _n55 state$_n55$raw_n5b |
---|
| 308 | - - 0 =state |
---|
| 309 | - - 1 =state$_n55_n58$true |
---|
| 310 | # case (state ) |
---|
| 311 | .mv state$_n52$raw_n5e 2 OKAY PENDING |
---|
| 312 | .names state$_n55$raw_n5b state _n52 state$_n52$raw_n5e |
---|
| 313 | - - 0 =state |
---|
| 314 | - - 1 =state$_n55$raw_n5b |
---|
| 315 | .mv state$_n48$raw_n60 2 OKAY PENDING |
---|
| 316 | .names state$_n4b$raw_n51 state$_n52$raw_n5e _n48 state$_n48$raw_n60 |
---|
| 317 | - - 0 =state$_n52$raw_n5e |
---|
| 318 | - - 1 =state$_n4b$raw_n51 |
---|
| 319 | # conflict arbitrators |
---|
| 320 | .names _n48 _n4d _n52 _n57 _n63 |
---|
| 321 | .def 0 |
---|
| 322 | 1 1 - - 1 |
---|
| 323 | 0 - 1 1 1 |
---|
| 324 | .mv _n64 2 OKAY PENDING |
---|
| 325 | .names _n63 state$_n48$raw_n60 state _n64 |
---|
| 326 | 1 - - =state$_n48$raw_n60 |
---|
| 327 | 0 - - =state |
---|
| 328 | # non-blocking assignments |
---|
| 329 | # latches |
---|
| 330 | .r state$raw_n47 state |
---|
| 331 | - =state$raw_n47 |
---|
| 332 | .latch _n64 state |
---|
| 333 | # quasi-continuous assignment |
---|
| 334 | .end |
---|
| 335 | |
---|
| 336 | |
---|