1(* -*-sml-*- *) 2(*****************************************************************************) 3(* Example from FoCs Manual *) 4(* Not for compiling. *) 5(*****************************************************************************) 6 7loadPath := "../official-semantics" :: "../regexp" :: !loadPath; 8app load ["bossLib","intLib","regexpLib","ExecuteTools"]; 9 10quietdec := true; 11open bossLib regexpLib; 12quietdec := false; 13 14(****************************************************************************** 15* Set the trace level of the regular expression library: 16* 0: silent 17* 1: 1 character (either - or +) for each list element processed 18* 2: matches as they are discovered 19* 3: transitions as they are calculated 20* 4: internal state of the automata 21******************************************************************************) 22set_trace "regexpTools" 1; 23 24(****************************************************************************** 25* Set default parsing to natural numbers rather than integers 26******************************************************************************) 27val _ = intLib.deprecate_int(); 28 29(****************************************************************************** 30* Generated this from a Verilog model of the BUF example in 31* Chapter 4 of FoCs User's Manual (see test.v) 32* (www.haifa.il.ibm.com/projects/verification/focs/) 33******************************************************************************) 34 35(****************************************************************************** 36* String version 37* val StoB_REQ = ``"StoB_REQ"``; 38* val BtoS_ACK = ``"BtoS_ACK"``; 39* val BtoR_REQ = ``"BtoR_REQ"``; 40* val RtoB_ACK = ``"RtoB_ACK"``; 41******************************************************************************) 42 43(****************************************************************************** 44* Num version 45******************************************************************************) 46val StoB_REQ_def = Define `StoB_REQ = 0`; 47val BtoS_ACK_def = Define `BtoS_ACK = 1`; 48val BtoR_REQ_def = Define `BtoR_REQ = 2`; 49val RtoB_ACK_def = Define `RtoB_ACK = 3`; 50 51quietdec := true; 52val SimRun_def = 53 Define 54 `SimRun = 55 [{}; 56 {StoB_REQ}; 57 {StoB_REQ; BtoS_ACK}; 58 {BtoS_ACK}; 59 {BtoS_ACK; BtoR_REQ}; 60 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 61 {BtoS_ACK; RtoB_ACK}; 62 {}; 63 {StoB_REQ}; 64 {StoB_REQ; BtoS_ACK}; 65 {BtoS_ACK}; 66 {BtoS_ACK; BtoR_REQ}; 67 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 68 {BtoS_ACK; RtoB_ACK}; 69 {}; 70 {StoB_REQ}; 71 {StoB_REQ; BtoS_ACK}; 72 {BtoS_ACK}; 73 {BtoS_ACK; BtoR_REQ}; 74 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 75 {BtoS_ACK; RtoB_ACK}; 76 {}; 77 {StoB_REQ}; 78 {StoB_REQ; BtoS_ACK}; 79 {BtoS_ACK}; 80 {BtoS_ACK; BtoR_REQ}; 81 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 82 {BtoS_ACK; RtoB_ACK}; 83 {}; 84 {StoB_REQ}; 85 {StoB_REQ; BtoS_ACK}; 86 {BtoS_ACK}; 87 {BtoS_ACK; BtoR_REQ}; 88 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 89 {BtoS_ACK; RtoB_ACK}; 90 {}; 91 {StoB_REQ}; 92 {StoB_REQ; BtoS_ACK}; 93 {BtoS_ACK}; 94 {BtoS_ACK; BtoR_REQ}; 95 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 96 {BtoS_ACK; RtoB_ACK}; 97 {}; 98 {StoB_REQ}; 99 {StoB_REQ; BtoS_ACK}; 100 {BtoS_ACK}; 101 {BtoS_ACK; BtoR_REQ}; 102 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 103 {BtoS_ACK; RtoB_ACK}; 104 {}; 105 {StoB_REQ}; 106 {StoB_REQ; BtoS_ACK}; 107 {BtoS_ACK}; 108 {BtoS_ACK; BtoR_REQ}; 109 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 110 {BtoS_ACK; RtoB_ACK}; 111 {}; 112 {StoB_REQ}; 113 {StoB_REQ; BtoS_ACK}; 114 {BtoS_ACK}; 115 {BtoS_ACK; BtoR_REQ}; 116 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 117 {BtoS_ACK; RtoB_ACK}; 118 {}; 119 {StoB_REQ}; 120 {StoB_REQ; BtoS_ACK}; 121 {BtoS_ACK}; 122 {BtoS_ACK; BtoR_REQ}; 123 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 124 {BtoS_ACK; RtoB_ACK}; 125 {}; 126 {StoB_REQ}; 127 {StoB_REQ; BtoS_ACK}; 128 {BtoS_ACK}; 129 {BtoS_ACK; BtoR_REQ}; 130 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 131 {BtoS_ACK; RtoB_ACK}; 132 {}; 133 {StoB_REQ}; 134 {StoB_REQ; BtoS_ACK}; 135 {BtoS_ACK}; 136 {BtoS_ACK; BtoR_REQ}; 137 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 138 {BtoS_ACK; RtoB_ACK}; 139 {}; 140 {StoB_REQ}; 141 {StoB_REQ; BtoS_ACK}; 142 {BtoS_ACK}; 143 {BtoS_ACK; BtoR_REQ}; 144 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 145 {BtoS_ACK; RtoB_ACK}; 146 {}; 147 {StoB_REQ}; 148 {StoB_REQ; BtoS_ACK}; 149 {BtoS_ACK}; 150 {BtoS_ACK; BtoR_REQ}; 151 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 152 {BtoS_ACK; RtoB_ACK}; 153 {}; 154 {StoB_REQ}; 155 {StoB_REQ; BtoS_ACK}; 156 {BtoS_ACK}; 157 {BtoS_ACK; BtoR_REQ}; 158 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 159 {BtoS_ACK; RtoB_ACK}; 160 {}; 161 {StoB_REQ}; 162 {StoB_REQ; BtoS_ACK}; 163 {BtoS_ACK}; 164 {BtoS_ACK; BtoR_REQ}; 165 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 166 {BtoS_ACK; RtoB_ACK}; 167 {}; 168 {StoB_REQ}; 169 {StoB_REQ; BtoS_ACK}; 170 {BtoS_ACK}; 171 {BtoS_ACK; BtoR_REQ}; 172 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 173 {BtoS_ACK; RtoB_ACK}; 174 {}; 175 {StoB_REQ}; 176 {StoB_REQ; BtoS_ACK}; 177 {BtoS_ACK}; 178 {BtoS_ACK; BtoR_REQ}; 179 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 180 {BtoS_ACK; RtoB_ACK}; 181 {}; 182 {StoB_REQ}; 183 {StoB_REQ; BtoS_ACK}; 184 {BtoS_ACK}; 185 {BtoS_ACK; BtoR_REQ}; 186 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 187 {BtoS_ACK; RtoB_ACK}; 188 {}; 189 {StoB_REQ}; 190 {StoB_REQ; BtoS_ACK}; 191 {BtoS_ACK}; 192 {BtoS_ACK; BtoR_REQ}; 193 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 194 {BtoS_ACK; RtoB_ACK}; 195 {}; 196 {StoB_REQ}; 197 {StoB_REQ; BtoS_ACK}; 198 {BtoS_ACK}; 199 {BtoS_ACK; BtoR_REQ}; 200 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 201 {BtoS_ACK; RtoB_ACK}; 202 {}; 203 {StoB_REQ}; 204 {StoB_REQ; BtoS_ACK}; 205 {BtoS_ACK}; 206 {BtoS_ACK; BtoR_REQ}; 207 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 208 {BtoS_ACK; RtoB_ACK}; 209 {}; 210 {StoB_REQ}; 211 {StoB_REQ; BtoS_ACK}; 212 {BtoS_ACK}; 213 {BtoS_ACK; BtoR_REQ}; 214 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 215 {BtoS_ACK; RtoB_ACK}; 216 {}; 217 {StoB_REQ}; 218 {StoB_REQ; BtoS_ACK}; 219 {BtoS_ACK}; 220 {BtoS_ACK; BtoR_REQ}; 221 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 222 {BtoS_ACK; RtoB_ACK}; 223 {}; 224 {StoB_REQ}; 225 {StoB_REQ; BtoS_ACK}; 226 {BtoS_ACK}; 227 {BtoS_ACK; BtoR_REQ}; 228 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 229 {BtoS_ACK; RtoB_ACK}; 230 {}; 231 {StoB_REQ}; 232 {StoB_REQ; BtoS_ACK}; 233 {BtoS_ACK}; 234 {BtoS_ACK; BtoR_REQ}; 235 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 236 {BtoS_ACK; RtoB_ACK}; 237 {}; 238 {StoB_REQ}; 239 {StoB_REQ; BtoS_ACK}; 240 {BtoS_ACK}; 241 {BtoS_ACK; BtoR_REQ}; 242 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 243 {BtoS_ACK; RtoB_ACK}; 244 {}; 245 {StoB_REQ}; 246 {StoB_REQ; BtoS_ACK}; 247 {BtoS_ACK}; 248 {BtoS_ACK; BtoR_REQ}; 249 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 250 {BtoS_ACK; RtoB_ACK}; 251 {}; 252 {StoB_REQ}; 253 {StoB_REQ; BtoS_ACK}; 254 {BtoS_ACK}; 255 {BtoS_ACK; BtoR_REQ}; 256 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 257 {BtoS_ACK; RtoB_ACK}; 258 {}; 259 {StoB_REQ}; 260 {StoB_REQ; BtoS_ACK}; 261 {BtoS_ACK}; 262 {BtoS_ACK; BtoR_REQ}; 263 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 264 {BtoS_ACK; RtoB_ACK}; 265 {}; 266 {StoB_REQ}; 267 {StoB_REQ; BtoS_ACK}; 268 {BtoS_ACK}; 269 {BtoS_ACK; BtoR_REQ}; 270 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 271 {BtoS_ACK; RtoB_ACK}; 272 {}; 273 {StoB_REQ}; 274 {StoB_REQ; BtoS_ACK}; 275 {BtoS_ACK}; 276 {BtoS_ACK; BtoR_REQ}; 277 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 278 {BtoS_ACK; RtoB_ACK}; 279 {}; 280 {StoB_REQ}; 281 {StoB_REQ; BtoS_ACK}; 282 {BtoS_ACK}; 283 {BtoS_ACK; BtoR_REQ}; 284 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 285 {BtoS_ACK; RtoB_ACK}; 286 {}; 287 {StoB_REQ}; 288 {StoB_REQ; BtoS_ACK}; 289 {BtoS_ACK}; 290 {BtoS_ACK; BtoR_REQ}; 291 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 292 {BtoS_ACK; RtoB_ACK}; 293 {}; 294 {StoB_REQ}; 295 {StoB_REQ; BtoS_ACK}; 296 {BtoS_ACK}; 297 {BtoS_ACK; BtoR_REQ}; 298 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 299 {BtoS_ACK; RtoB_ACK}; 300 {}; 301 {StoB_REQ}; 302 {StoB_REQ; BtoS_ACK}; 303 {BtoS_ACK}; 304 {BtoS_ACK; BtoR_REQ}; 305 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 306 {BtoS_ACK; RtoB_ACK}; 307 {}; 308 {StoB_REQ}; 309 {StoB_REQ; BtoS_ACK}; 310 {BtoS_ACK}; 311 {BtoS_ACK; BtoR_REQ}; 312 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 313 {BtoS_ACK; RtoB_ACK}; 314 {}; 315 {StoB_REQ}; 316 {StoB_REQ; BtoS_ACK}; 317 {BtoS_ACK}; 318 {BtoS_ACK; BtoR_REQ}; 319 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 320 {BtoS_ACK; RtoB_ACK}; 321 {}; 322 {StoB_REQ}; 323 {StoB_REQ; BtoS_ACK}; 324 {BtoS_ACK}; 325 {BtoS_ACK; BtoR_REQ}; 326 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 327 {BtoS_ACK; RtoB_ACK}; 328 {}; 329 {StoB_REQ}; 330 {StoB_REQ; BtoS_ACK}; 331 {BtoS_ACK}; 332 {BtoS_ACK; BtoR_REQ}; 333 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 334 {BtoS_ACK; RtoB_ACK}; 335 {}; 336 {StoB_REQ}; 337 {StoB_REQ; BtoS_ACK}; 338 {BtoS_ACK}; 339 {BtoS_ACK; BtoR_REQ}; 340 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 341 {BtoS_ACK; RtoB_ACK}; 342 {}; 343 {StoB_REQ}; 344 {StoB_REQ; BtoS_ACK}; 345 {BtoS_ACK}; 346 {BtoS_ACK; BtoR_REQ}; 347 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 348 {BtoS_ACK; RtoB_ACK}; 349 {}; 350 {StoB_REQ}; 351 {StoB_REQ; BtoS_ACK}; 352 {BtoS_ACK}; 353 {BtoS_ACK; BtoR_REQ}; 354 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 355 {BtoS_ACK; RtoB_ACK}; 356 {}; 357 {StoB_REQ}; 358 {StoB_REQ; BtoS_ACK}; 359 {BtoS_ACK}; 360 {BtoS_ACK; BtoR_REQ}; 361 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 362 {BtoS_ACK; RtoB_ACK}; 363 {}; 364 {StoB_REQ}; 365 {StoB_REQ; BtoS_ACK}; 366 {BtoS_ACK}; 367 {BtoS_ACK; BtoR_REQ}; 368 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 369 {BtoS_ACK; RtoB_ACK}; 370 {}; 371 {StoB_REQ}; 372 {StoB_REQ; BtoS_ACK}; 373 {BtoS_ACK}; 374 {BtoS_ACK; BtoR_REQ}; 375 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 376 {BtoS_ACK; RtoB_ACK}; 377 {}; 378 {StoB_REQ}; 379 {StoB_REQ; BtoS_ACK}; 380 {BtoS_ACK}; 381 {BtoS_ACK; BtoR_REQ}; 382 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 383 {BtoS_ACK; RtoB_ACK}; 384 {}; 385 {StoB_REQ}; 386 {StoB_REQ; BtoS_ACK}; 387 {BtoS_ACK}; 388 {BtoS_ACK; BtoR_REQ}; 389 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 390 {BtoS_ACK; RtoB_ACK}; 391 {}; 392 {StoB_REQ}; 393 {StoB_REQ; BtoS_ACK}; 394 {BtoS_ACK}; 395 {BtoS_ACK; BtoR_REQ}; 396 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 397 {BtoS_ACK; RtoB_ACK}; 398 {}; 399 {StoB_REQ}; 400 {StoB_REQ; BtoS_ACK}; 401 {BtoS_ACK}; 402 {BtoS_ACK; BtoR_REQ}; 403 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 404 {BtoS_ACK; RtoB_ACK}; 405 {}; 406 {StoB_REQ}; 407 {StoB_REQ; BtoS_ACK}; 408 {BtoS_ACK}; 409 {BtoS_ACK; BtoR_REQ}; 410 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 411 {BtoS_ACK; RtoB_ACK}; 412 {}; 413 {StoB_REQ}; 414 {StoB_REQ; BtoS_ACK}; 415 {BtoS_ACK}; 416 {BtoS_ACK; BtoR_REQ}; 417 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 418 {BtoS_ACK; RtoB_ACK}; 419 {}; 420 {StoB_REQ}; 421 {StoB_REQ; BtoS_ACK}; 422 {BtoS_ACK}; 423 {BtoS_ACK; BtoR_REQ}; 424 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 425 {BtoS_ACK; RtoB_ACK}; 426 {}; 427 {StoB_REQ}; 428 {StoB_REQ; BtoS_ACK}; 429 {BtoS_ACK}; 430 {BtoS_ACK; BtoR_REQ}; 431 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 432 {BtoS_ACK; RtoB_ACK}; 433 {}; 434 {StoB_REQ}; 435 {StoB_REQ; BtoS_ACK}; 436 {BtoS_ACK}; 437 {BtoS_ACK; BtoR_REQ}; 438 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 439 {BtoS_ACK; RtoB_ACK}; 440 {}; 441 {StoB_REQ}; 442 {StoB_REQ; BtoS_ACK}; 443 {BtoS_ACK}; 444 {BtoS_ACK; BtoR_REQ}; 445 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 446 {BtoS_ACK; RtoB_ACK}; 447 {}; 448 {StoB_REQ}; 449 {StoB_REQ; BtoS_ACK}; 450 {BtoS_ACK}; 451 {BtoS_ACK; BtoR_REQ}; 452 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 453 {BtoS_ACK; RtoB_ACK}; 454 {}; 455 {StoB_REQ}; 456 {StoB_REQ; BtoS_ACK}; 457 {BtoS_ACK}; 458 {BtoS_ACK; BtoR_REQ}; 459 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 460 {BtoS_ACK; RtoB_ACK}; 461 {}; 462 {StoB_REQ}; 463 {StoB_REQ; BtoS_ACK}; 464 {BtoS_ACK}; 465 {BtoS_ACK; BtoR_REQ}; 466 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 467 {BtoS_ACK; RtoB_ACK}; 468 {}; 469 {StoB_REQ}; 470 {StoB_REQ; BtoS_ACK}; 471 {BtoS_ACK}; 472 {BtoS_ACK; BtoR_REQ}; 473 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 474 {BtoS_ACK; RtoB_ACK}; 475 {}; 476 {StoB_REQ}; 477 {StoB_REQ; BtoS_ACK}; 478 {BtoS_ACK}; 479 {BtoS_ACK; BtoR_REQ}; 480 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 481 {BtoS_ACK; RtoB_ACK}; 482 {}; 483 {StoB_REQ}; 484 {StoB_REQ; BtoS_ACK}; 485 {BtoS_ACK}; 486 {BtoS_ACK; BtoR_REQ}; 487 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 488 {BtoS_ACK; RtoB_ACK}; 489 {}; 490 {StoB_REQ}; 491 {StoB_REQ; BtoS_ACK}; 492 {BtoS_ACK}; 493 {BtoS_ACK; BtoR_REQ}; 494 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 495 {BtoS_ACK; RtoB_ACK}; 496 {}; 497 {StoB_REQ}; 498 {StoB_REQ; BtoS_ACK}; 499 {BtoS_ACK}; 500 {BtoS_ACK; BtoR_REQ}; 501 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 502 {BtoS_ACK; RtoB_ACK}; 503 {}; 504 {StoB_REQ}; 505 {StoB_REQ; BtoS_ACK}; 506 {BtoS_ACK}; 507 {BtoS_ACK; BtoR_REQ}; 508 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 509 {BtoS_ACK; RtoB_ACK}; 510 {}; 511 {StoB_REQ}; 512 {StoB_REQ; BtoS_ACK}; 513 {BtoS_ACK}; 514 {BtoS_ACK; BtoR_REQ}; 515 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 516 {BtoS_ACK; RtoB_ACK}; 517 {}; 518 {StoB_REQ}; 519 {StoB_REQ; BtoS_ACK}; 520 {BtoS_ACK}; 521 {BtoS_ACK; BtoR_REQ}; 522 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 523 {BtoS_ACK; RtoB_ACK}; 524 {}; 525 {StoB_REQ}; 526 {StoB_REQ; BtoS_ACK}; 527 {BtoS_ACK}; 528 {BtoS_ACK; BtoR_REQ}; 529 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 530 {BtoS_ACK; RtoB_ACK}; 531 {}; 532 {StoB_REQ}; 533 {StoB_REQ; BtoS_ACK}; 534 {BtoS_ACK}; 535 {BtoS_ACK; BtoR_REQ}; 536 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 537 {BtoS_ACK; RtoB_ACK}; 538 {}; 539 {StoB_REQ}; 540 {StoB_REQ; BtoS_ACK}; 541 {BtoS_ACK}; 542 {BtoS_ACK; BtoR_REQ}; 543 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 544 {BtoS_ACK; RtoB_ACK}; 545 {}; 546 {StoB_REQ}; 547 {StoB_REQ; BtoS_ACK}; 548 {BtoS_ACK}; 549 {BtoS_ACK; BtoR_REQ}; 550 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 551 {BtoS_ACK; RtoB_ACK}; 552 {}; 553 {StoB_REQ}; 554 {StoB_REQ; BtoS_ACK}; 555 {BtoS_ACK}; 556 {BtoS_ACK; BtoR_REQ}; 557 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 558 {BtoS_ACK; RtoB_ACK}; 559 {}; 560 {StoB_REQ}; 561 {StoB_REQ; BtoS_ACK}; 562 {BtoS_ACK}; 563 {BtoS_ACK; BtoR_REQ}; 564 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 565 {BtoS_ACK; RtoB_ACK}; 566 {}; 567 {StoB_REQ}; 568 {StoB_REQ; BtoS_ACK}; 569 {BtoS_ACK}; 570 {BtoS_ACK; BtoR_REQ}; 571 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 572 {BtoS_ACK; RtoB_ACK}; 573 {}; 574 {StoB_REQ}; 575 {StoB_REQ; BtoS_ACK}; 576 {BtoS_ACK}; 577 {BtoS_ACK; BtoR_REQ}; 578 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 579 {BtoS_ACK; RtoB_ACK}; 580 {}; 581 {StoB_REQ}; 582 {StoB_REQ; BtoS_ACK}; 583 {BtoS_ACK}; 584 {BtoS_ACK; BtoR_REQ}; 585 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 586 {BtoS_ACK; RtoB_ACK}; 587 {}; 588 {StoB_REQ}; 589 {StoB_REQ; BtoS_ACK}; 590 {BtoS_ACK}; 591 {BtoS_ACK; BtoR_REQ}; 592 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 593 {BtoS_ACK; RtoB_ACK}; 594 {}; 595 {StoB_REQ}; 596 {StoB_REQ; BtoS_ACK}; 597 {BtoS_ACK}; 598 {BtoS_ACK; BtoR_REQ}; 599 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 600 {BtoS_ACK; RtoB_ACK}; 601 {}; 602 {StoB_REQ}; 603 {StoB_REQ; BtoS_ACK}; 604 {BtoS_ACK}; 605 {BtoS_ACK; BtoR_REQ}; 606 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 607 {BtoS_ACK; RtoB_ACK}; 608 {}; 609 {StoB_REQ}; 610 {StoB_REQ; BtoS_ACK}; 611 {BtoS_ACK}; 612 {BtoS_ACK; BtoR_REQ}; 613 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 614 {BtoS_ACK; RtoB_ACK}; 615 {}; 616 {StoB_REQ}; 617 {StoB_REQ; BtoS_ACK}; 618 {BtoS_ACK}; 619 {BtoS_ACK; BtoR_REQ}; 620 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 621 {BtoS_ACK; RtoB_ACK}; 622 {}; 623 {StoB_REQ}; 624 {StoB_REQ; BtoS_ACK}; 625 {BtoS_ACK}; 626 {BtoS_ACK; BtoR_REQ}; 627 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 628 {BtoS_ACK; RtoB_ACK}; 629 {}; 630 {StoB_REQ}; 631 {StoB_REQ; BtoS_ACK}; 632 {BtoS_ACK}; 633 {BtoS_ACK; BtoR_REQ}; 634 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 635 {BtoS_ACK; RtoB_ACK}; 636 {}; 637 {StoB_REQ}; 638 {StoB_REQ; BtoS_ACK}; 639 {BtoS_ACK}; 640 {BtoS_ACK; BtoR_REQ}; 641 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 642 {BtoS_ACK; RtoB_ACK}; 643 {}; 644 {StoB_REQ}; 645 {StoB_REQ; BtoS_ACK}; 646 {BtoS_ACK}; 647 {BtoS_ACK; BtoR_REQ}; 648 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 649 {BtoS_ACK; RtoB_ACK}; 650 {}; 651 {StoB_REQ}; 652 {StoB_REQ; BtoS_ACK}; 653 {BtoS_ACK}; 654 {BtoS_ACK; BtoR_REQ}; 655 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 656 {BtoS_ACK; RtoB_ACK}; 657 {}; 658 {StoB_REQ}; 659 {StoB_REQ; BtoS_ACK}; 660 {BtoS_ACK}; 661 {BtoS_ACK; BtoR_REQ}; 662 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 663 {BtoS_ACK; RtoB_ACK}; 664 {}; 665 {StoB_REQ}; 666 {StoB_REQ; BtoS_ACK}; 667 {BtoS_ACK}; 668 {BtoS_ACK; BtoR_REQ}; 669 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 670 {BtoS_ACK; RtoB_ACK}; 671 {}; 672 {StoB_REQ}; 673 {StoB_REQ; BtoS_ACK}; 674 {BtoS_ACK}; 675 {BtoS_ACK; BtoR_REQ}; 676 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 677 {BtoS_ACK; RtoB_ACK}; 678 {}; 679 {StoB_REQ}; 680 {StoB_REQ; BtoS_ACK}; 681 {BtoS_ACK}; 682 {BtoS_ACK; BtoR_REQ}; 683 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 684 {BtoS_ACK; RtoB_ACK}; 685 {}; 686 {StoB_REQ}; 687 {StoB_REQ; BtoS_ACK}; 688 {BtoS_ACK}; 689 {BtoS_ACK; BtoR_REQ}; 690 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 691 {BtoS_ACK; RtoB_ACK}; 692 {}; 693 {StoB_REQ}; 694 {StoB_REQ; BtoS_ACK}; 695 {BtoS_ACK}; 696 {BtoS_ACK; BtoR_REQ}; 697 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 698 {BtoS_ACK; RtoB_ACK}; 699 {}; 700 {StoB_REQ}; 701 {StoB_REQ; BtoS_ACK}; 702 {BtoS_ACK}; 703 {BtoS_ACK; BtoR_REQ}; 704 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 705 {BtoS_ACK; RtoB_ACK}; 706 {}; 707 {StoB_REQ}; 708 {StoB_REQ; BtoS_ACK}; 709 {BtoS_ACK}; 710 {BtoS_ACK; BtoR_REQ}; 711 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 712 {BtoS_ACK; RtoB_ACK}; 713 {}; 714 {StoB_REQ}; 715 {StoB_REQ; BtoS_ACK}; 716 {BtoS_ACK}; 717 {BtoS_ACK; BtoR_REQ}; 718 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 719 {BtoS_ACK; RtoB_ACK}; 720 {}; 721 {StoB_REQ}; 722 {StoB_REQ; BtoS_ACK}; 723 {BtoS_ACK}; 724 {BtoS_ACK; BtoR_REQ}; 725 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 726 {BtoS_ACK; RtoB_ACK}; 727 {}; 728 {StoB_REQ}; 729 {StoB_REQ; BtoS_ACK}; 730 {BtoS_ACK}; 731 {BtoS_ACK; BtoR_REQ}; 732 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 733 {BtoS_ACK; RtoB_ACK}; 734 {}; 735 {StoB_REQ}; 736 {StoB_REQ; BtoS_ACK}; 737 {BtoS_ACK}; 738 {BtoS_ACK; BtoR_REQ}; 739 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 740 {BtoS_ACK; RtoB_ACK}; 741 {}; 742 {StoB_REQ}; 743 {StoB_REQ; BtoS_ACK}; 744 {BtoS_ACK}; 745 {BtoS_ACK; BtoR_REQ}; 746 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 747 {BtoS_ACK; RtoB_ACK}; 748 {}; 749 {StoB_REQ}; 750 {StoB_REQ; BtoS_ACK}; 751 {BtoS_ACK}; 752 {BtoS_ACK; BtoR_REQ}; 753 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 754 {BtoS_ACK; RtoB_ACK}; 755 {}]`; 756 757quietdec := false; 758 759(****************************************************************************** 760* Make "&" into an infix for F_AND 761******************************************************************************) 762val _ = set_fixity "&" (Infixl 500); 763val F_AND_IX_def = xDefine "F_AND_IX" `$& f1 f2 = F_AND(f1,f2)`; 764 765(****************************************************************************** 766* Make ";;" into an infix for S_CAT 767******************************************************************************) 768val _ = set_fixity ";;" (Infixl 500); 769val S_CAT_IX_def = xDefine "S_CAT_IX" `$;; r1 r2 = S_CAT(r1,r2)`; 770 771(****************************************************************************** 772* A single property characterising a four-phase handshake 773******************************************************************************) 774val FOUR_PHASE_def = 775 Define 776 `FOUR_PHASE req ack = 777 F_NEVER 778 (S_REPEAT S_TRUE ;; 779 S_BOOL(B_AND(B_NOT(B_PROP req),B_PROP ack)) ;; 780 S_BOOL(B_PROP req)) 781 & 782 F_NEVER 783 (S_REPEAT S_TRUE ;; 784 S_BOOL(B_AND(B_PROP req,B_NOT(B_PROP ack))) ;; 785 S_BOOL(B_NOT(B_PROP req))) 786 & 787 F_NEVER 788 (S_REPEAT S_TRUE ;; 789 S_BOOL(B_AND(B_NOT(B_PROP ack),B_NOT(B_PROP req))) ;; 790 S_BOOL(B_PROP ack)) 791 & 792 F_NEVER 793 (S_REPEAT S_TRUE ;; 794 S_BOOL(B_AND(B_PROP ack,B_PROP req)) ;; 795 S_BOOL(B_NOT(B_PROP ack)))`; 796 797(* Version without S_REPEAT S_TRUE 798val FOUR_PHASE_def = 799 Define 800 `FOUR_PHASE req ack = 801 F_NEVER 802 ( 803 S_BOOL(B_AND(B_NOT(B_PROP req),B_PROP ack)) ;; 804 S_BOOL(B_PROP req)) 805 & 806 F_NEVER 807 ( 808 S_BOOL(B_AND(B_PROP req,B_NOT(B_PROP ack))) ;; 809 S_BOOL(B_NOT(B_PROP req))) 810 & 811 F_NEVER 812 ( 813 S_BOOL(B_AND(B_NOT(B_PROP ack),B_NOT(B_PROP req))) ;; 814 S_BOOL(B_PROP ack)) 815 & 816 F_NEVER 817 ( 818 S_BOOL(B_AND(B_PROP ack,B_PROP req)) ;; 819 S_BOOL(B_NOT(B_PROP ack)))`; 820*) 821 822(****************************************************************************** 823* Making Verilog finite state machines from FOUR_PHASE regular expressions. 824******************************************************************************) 825val alph = [``StoB_REQ``, ``BtoS_ACK``, ``BtoR_REQ``, ``RtoB_ACK``]; 826 827fun regexp_ra req ack = 828 ``sere2regexp 829 (S_REPEAT S_TRUE ;; 830 S_BOOL(B_AND(B_NOT(B_PROP ^req),B_PROP ^ack)) ;; 831 S_BOOL(B_PROP ^req)) : (num -> bool) regexp``; 832 833val r1 = regexp_ra ``StoB_REQ`` ``BtoS_ACK``; 834 835val d1 = try (extract_dfa alph) r1; 836 837val inp1 = {name = "Checker1", alphabet = alph, regexp = r1}; 838 839val s1 = print ("\n\n" ^ verilog_dfa inp1 ^ "\n"); 840 841val r2 = 842 ``sere2regexp 843 (S_REPEAT(S_BOOL B_TRUE) ;; 844 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 845 S_BOOL(B_PROP BtoS_ACK) ;; 846 S_REPEAT(S_BOOL(B_AND(B_PROP BtoS_ACK, 847 B_NOT(B_PROP RtoB_ACK)))) ;; 848 S_REPEAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK), 849 B_NOT(B_PROP RtoB_ACK)))) ;; 850 S_BOOL(B_PROP BtoS_ACK))``; 851 852val d2 = try (extract_dfa alph) r2; 853 854val inp2 = {name = "Checker2", alphabet = alph, regexp = r2}; 855 856val s2 = print ("\n\n" ^ verilog_dfa inp2 ^ "\n"); 857 858(****************************************************************************** 859* vunit four_phase_handskake_left (page 23, FoCs User's Manual, Version 1.0) 860* FOUR_PHASE StoB_REQ BtoS_ACK 861******************************************************************************) 862 863val four_phase_handskake_left = 864 time EVAL ``F_SEM (FINITE SimRun) B_TRUE (FOUR_PHASE StoB_REQ BtoS_ACK)``; 865 866(****************************************************************************** 867* vunit four_phase_handskake_right (page 24, FoCs User's Manual, Version 1.0) 868* FOUR_PHASE BtoR_REQ RtoB_ACK 869******************************************************************************) 870 871val four_phase_handskake_right = 872time EVAL ``F_SEM (FINITE SimRun) B_TRUE (FOUR_PHASE BtoR_REQ RtoB_ACK)``; 873 874(****************************************************************************** 875* f1 before f2 = [not f2 W (f1 & not f2)] 876******************************************************************************) 877val F_BEFORE_def = 878 Define 879 `F_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`; 880 881(****************************************************************************** 882* No underflow: ack1 is asserted between any two ack2 assertions 883******************************************************************************) 884 885val ACK_INTERLEAVE_def = 886 Define 887 `ACK_INTERLEAVE ack1 ack2 = 888 F_SUFFIX_IMP 889 ((S_REPEAT(S_BOOL B_TRUE) ;; 890 S_BOOL(B_NOT(B_PROP ack1)) ;; 891 S_BOOL(B_PROP ack1)), 892 F_BEFORE 893 (F_AND(F_NOT(F_BOOL(B_PROP ack2)), 894 F_NEXT(F_BOOL(B_PROP ack2))), 895 F_AND(F_NOT(F_BOOL(B_PROP ack1)), 896 F_NEXT(F_BOOL(B_PROP ack1)))))`; 897 898(****************************************************************************** 899* vunit ack_interleaving (page 22, FoCs User's Manual, Version 1.0) 900******************************************************************************) 901 902val ack_interleaving = 903 time 904 EVAL 905 ``F_SEM (FINITE SimRun) B_TRUE (ACK_INTERLEAVE BtoS_ACK RtoB_ACK) 906 /\ 907 F_SEM (FINITE SimRun) B_TRUE (ACK_INTERLEAVE RtoB_ACK BtoS_ACK)``; 908