| 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 | |
|---|
![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
