1271294Sngie(* -*-sml-*- *) 2271294Sngie(*****************************************************************************) 3271294Sngie(* Sanity checking "ExecuteSemantics": a derived executable semantics *) 4271294Sngie(* Not for compiling. *) 5271294Sngie(*****************************************************************************) 6271294Sngie 7271294Sngieval _ = loadPath := "../official-semantics" :: 8271294Sngie "../regexp" :: 9271294Sngie !loadPath; 10271294Sngie 11271294Sngieval _ = app load ["bossLib","intLib","regexpLib","ExecuteTools"]; 12271294Sngie 13271294Sngieval _ = quietdec := true; 14271294Sngieopen bossLib regexpLib; 15271294Sngieval _ = quietdec := false; 16271294Sngie 17271294Sngiefun pth t = let val () = print ("\n" ^ thm_to_string t ^ "\n\n") in t end; 18271294Sngieval EVAL = pth o bossLib.EVAL; 19271294Sngieval Define = pth o bossLib.Define; 20 21(****************************************************************************** 22* Set the trace level of the regular expression library: 23* 0: silent 24* 1: 1 character (either - or +) for each list element processed 25* 2: matches as they are discovered 26* 3: transitions as they are calculated 27* 4: internal state of the automata 28******************************************************************************) 29val _ = set_trace "regexpTools" 2; 30 31(****************************************************************************** 32* Set default parsing to natural numbers rather than integers 33******************************************************************************) 34val _ = intLib.deprecate_int(); 35 36(****************************************************************************** 37* Examples 38******************************************************************************) 39 40(****************************************************************************** 41* [{s0};{s1};{s2}] |= [f1 U f2] (f1, f2 arbitrary formulas) 42******************************************************************************) 43val _ = EVAL ``UF_SEM (FINITE[s0;s1;s2]) (F_UNTIL(f1,f2))``; 44 45(****************************************************************************** 46* [{s0};{s1};{s2}] |= [b1 U b2] (b1, b2 arbitrary boolean expressions ) 47******************************************************************************) 48val _ = EVAL ``UF_SEM (FINITE[s0;s1;s2]) (F_UNTIL(F_BOOL b1, F_BOOL b2))``; 49 50(****************************************************************************** 51* [{s0};{s1};{s2}] |= [p1 U p2] (p1, p2 arbitrary atomic propositions) 52******************************************************************************) 53val _ = 54EVAL 55 ``UF_SEM (FINITE[s0;s1;s2]) (F_UNTIL(F_BOOL(B_PROP p1), F_BOOL(B_PROP p2)))``; 56 57(****************************************************************************** 58* [{s0};{s1};{s2}] |= {1}(2) 59******************************************************************************) 60val _ = 61EVAL 62 ``UF_SEM (FINITE[s0;s1;s2]) (F_UNTIL(F_BOOL(B_PROP 1), F_BOOL(B_PROP 2)))``; 63 64(****************************************************************************** 65* [{1};{1};{2}] |= {1}(2) 66******************************************************************************) 67val _ = 68EVAL 69 ``UF_SEM (FINITE[{1};{1};{2}]) (F_UNTIL(F_BOOL(B_PROP 1), F_BOOL(B_PROP 2)))``; 70 71(****************************************************************************** 72* [{1};{3};{2}] |= {1}(2) 73******************************************************************************) 74val _ = 75EVAL 76 ``UF_SEM (FINITE[{1};{3};{2}]) (F_UNTIL(F_BOOL(B_PROP 1), F_BOOL(B_PROP 2)))``; 77 78(* Can't evaluate a variable regular expression using automata! 79EVAL ``UF_SEM (FINITE[s0;s1;s2]) (F_SUFFIX_IMP(r,f))``; 80EVAL ``UF_SEM (FINITE[{1};{3};{2}]) (F_SUFFIX_IMP(r,f))``; 81*) 82 83(****************************************************************************** 84* [{1};{2};{3}] |= {n}(f) 85******************************************************************************) 86val _ = 87EVAL 88``UF_SEM (FINITE[{1};{2};{3}]) 89 (F_SUFFIX_IMP (S_BOOL (B_PROP n), f))``; 90 91(****************************************************************************** 92* [{1};{2};{3}] |= {n}(p) 93******************************************************************************) 94val _ = 95EVAL 96``UF_SEM (FINITE[{1};{2};{3}]) 97 (F_SUFFIX_IMP (S_BOOL (B_PROP n), F_BOOL(B_PROP p)))``; 98 99(****************************************************************************** 100* [{1};{2};{3}] |= {[*]}(f) 101******************************************************************************) 102val _ = 103EVAL 104``UF_SEM (FINITE[{1};{2};{3}]) 105 (F_SUFFIX_IMP (S_REPEAT S_TRUE, f))``; 106 107(****************************************************************************** 108* [{1};{2};{3}] |= {[*]}(p) 109******************************************************************************) 110val _ = 111EVAL 112``UF_SEM (FINITE[{1};{2};{3}]) 113 (F_SUFFIX_IMP (S_REPEAT S_TRUE, F_BOOL(B_PROP p)))``; 114 115(****************************************************************************** 116* [{p};{p};{p}] |= {[*]}(p) 117******************************************************************************) 118val _ = 119EVAL 120``UF_SEM (FINITE[{p};{p};{p}]) 121 (F_SUFFIX_IMP (S_REPEAT S_TRUE, F_BOOL(B_PROP p)))``; 122 123(****************************************************************************** 124* [{p1};{p2};{p3}] |= {[*]}(p) 125******************************************************************************) 126val _ = 127EVAL 128``UF_SEM (FINITE[{p1};{p2};{p3}]) 129 (F_SUFFIX_IMP (S_REPEAT S_TRUE, F_BOOL(B_PROP p)))``; 130 131(****************************************************************************** 132* [{1};{2};{3};{4};{5};{6};{7};{8};{9}] |= {3}(f) 133******************************************************************************) 134val _ = 135EVAL 136``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}]) 137 (F_SUFFIX_IMP(S_BOOL(B_PROP 3), f))``; 138 139(****************************************************************************** 140* [{1};{2};{3};{4};{5};{6};{7};{8};{9}] |= {[*];2;3}(f) 141******************************************************************************) 142val _ = 143EVAL 144``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}]) 145 (F_SUFFIX_IMP 146 (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL (B_PROP 2),S_BOOL (B_PROP 3))), 147 f))``; 148 149(****************************************************************************** 150* [{1};{2};{3};{4};{5};{6};{7};{8};{9}] |= {[*];2:3}(f) 151******************************************************************************) 152val _ = 153EVAL 154``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}]) 155 (F_SUFFIX_IMP 156 (S_CAT(S_REPEAT S_TRUE, S_FUSION(S_BOOL (B_PROP 2),S_BOOL (B_PROP 3))), 157 f))``; 158 159(****************************************************************************** 160* [{1};{2};{3};{4};{5};{6};{7};{8};{9}] |= {[*];2;3;[*]}(f) 161******************************************************************************) 162val _ = 163EVAL 164``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}]) 165 (F_SUFFIX_IMP 166 (S_CAT(S_REPEAT S_TRUE, 167 S_CAT(S_CAT(S_BOOL (B_PROP 2),S_BOOL (B_PROP 3)), 168 S_REPEAT S_TRUE)), 169 f))``; 170 171(****************************************************************************** 172* [{1};{2};{3}] |= {[*];3} 173******************************************************************************) 174val _ = 175EVAL ``US_SEM [{1};{2};{3}] (S_CAT(S_REPEAT S_TRUE, S_BOOL(B_PROP 3)))``; 176 177(****************************************************************************** 178* [{1};{2};{3}] |= {[*];2} 179******************************************************************************) 180val _ = 181EVAL ``US_SEM [{1};{2};{3}] (S_CAT(S_REPEAT S_TRUE, S_BOOL(B_PROP 2)))``; 182 183(****************************************************************************** 184* [{1};{2};{3}] |= {[*];2;[*]} 185******************************************************************************) 186val _ = 187EVAL ``US_SEM 188 [{1};{2};{3};{4};{5}] 189 (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL(B_PROP 2), S_REPEAT S_TRUE)))``; 190 191(****************************************************************************** 192* [{1};{2};{3};{4};{5};{6};{7};{8};{9}] |= {1|3} |-> {[*];3}! 193******************************************************************************) 194val _ = 195EVAL 196``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}]) 197 (F_STRONG_IMP ((S_OR (S_BOOL (B_PROP 1), S_BOOL (B_PROP 3))), 198 (S_CAT (S_REPEAT S_TRUE, S_BOOL (B_PROP 3)))))``; 199 200(****************************************************************************** 201* [{1};{1};{1};{1};{1};{1};{1};{1};{1}] |= always{1} 202******************************************************************************) 203val _ = 204EVAL 205``UF_SEM (FINITE[{1};{1};{1};{1};{1};{1};{1};{1};{1}]) 206 (F_SERE_ALWAYS(S_BOOL(B_PROP 1)))``; 207 208(****************************************************************************** 209* [{1};{1};{1};{1};{1};{1};{1};{1};{1}] |= always{1;1} 210******************************************************************************) 211val _ = 212EVAL 213``UF_SEM (FINITE[{1};{1};{1};{1};{1};{1};{1};{1};{1}]) 214 (F_SERE_ALWAYS(S_CAT(S_BOOL(B_PROP 1), S_BOOL(B_PROP 1))))``; 215 216(****************************************************************************** 217* [{1};{2};{3};{4};{4;5};{4;6};{4;7};{4;8};{4;9}] |= always{4;4} 218******************************************************************************) 219val _ = 220EVAL 221``UF_SEM (FINITE[{1};{2};{3};{4};{4;5};{4;6};{4;7};{4;8};{4;9}]) 222 (F_SERE_ALWAYS(S_CAT(S_BOOL(B_PROP 4), S_BOOL(B_PROP 4))))``; 223 224(****************************************************************************** 225* [{1};{2};{3};{4};{4};{6};{7};{8};{9}] |= never{4;3} 226******************************************************************************) 227val _ = 228EVAL 229``UF_SEM (FINITE[{1};{2};{3};{4};{4};{6};{7};{8};{9}]) 230 (F_SERE_NEVER(S_CAT(S_BOOL(B_PROP 4), S_BOOL(B_PROP 3))))``; 231 232(****************************************************************************** 233* [{1};{2};{3};{4};{4};{6};{7};{8};{9}] |= never{3;4} 234******************************************************************************) 235val _ = 236EVAL 237``UF_SEM (FINITE[{1};{2};{3};{4};{4};{6};{7};{8};{9}]) 238 (F_SERE_NEVER(S_CAT(S_BOOL(B_PROP 3), S_BOOL(B_PROP 4))))``; 239 240 241(****************************************************************************** 242quietdec:=true;; 243loadPath := "../official-semantics" :: "../regexp" :: !loadPath; 244app load ["res_quanTools","PropertiesTheory"]; 245open PSLPathTheory; 246val resq_SS = 247 simpLib.merge_ss 248 [res_quanTools.resq_SS, 249 rewrites 250 [num_to_def,xnum_to_def,IN_DEF,num_to_def,xnum_to_def,LENGTH_def]]; 251quietdec:=false; 252 253val UF_SEM_SUFFIX_IMP_FALSE = 254 store_thm 255 ("UF_SEM_SUFFIX_IMP_FALSE", 256 ``UF_SEM w (F_SUFFIX_IMP(r, F_BOOL B_FALSE)) = 257 !j::(0 to LENGTH w). ~(US_SEM (SEL w (0,j)) r)``, 258 RW_TAC (std_ss++resq_SS) [UF_SEM_def,B_SEM]); 259******************************************************************************) 260 261(****************************************************************************** 262* Generated this from a Verilog model of the BUF example in 263* Chapter 4 of FoCs User's Manual (see test.v) 264* (www.haifa.il.ibm.com/projects/verification/focs/) 265******************************************************************************) 266 267(****************************************************************************** 268* String version 269* val StoB_REQ = ``"StoB_REQ"``; 270* val BtoS_ACK = ``"BtoS_ACK"``; 271* val BtoR_REQ = ``"BtoR_REQ"``; 272* val RtoB_ACK = ``"RtoB_ACK"``; 273******************************************************************************) 274 275(****************************************************************************** 276* Num version 277******************************************************************************) 278val StoB_REQ_def = Define `StoB_REQ = 0`; 279val BtoS_ACK_def = Define `BtoS_ACK = 1`; 280val BtoR_REQ_def = Define `BtoR_REQ = 2`; 281val RtoB_ACK_def = Define `RtoB_ACK = 3`; 282 283quietdec := true; 284val SimRun_def = 285 Define 286 `SimRun = 287 [{}; 288 {StoB_REQ}; 289 {StoB_REQ; BtoS_ACK}; 290 {BtoS_ACK}; 291 {BtoS_ACK; BtoR_REQ}; 292 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 293 {BtoS_ACK; RtoB_ACK}; 294 {}; 295 {StoB_REQ}; 296 {StoB_REQ; BtoS_ACK}; 297 {BtoS_ACK}; 298 {BtoS_ACK; BtoR_REQ}; 299 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 300 {BtoS_ACK; RtoB_ACK}; 301 {}; 302 {StoB_REQ}; 303 {StoB_REQ; BtoS_ACK}; 304 {BtoS_ACK}; 305 {BtoS_ACK; BtoR_REQ}; 306 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 307 {BtoS_ACK; RtoB_ACK}; 308 {}; 309 {StoB_REQ}; 310 {StoB_REQ; BtoS_ACK}; 311 {BtoS_ACK}; 312 {BtoS_ACK; BtoR_REQ}; 313 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 314 {BtoS_ACK; RtoB_ACK}; 315 {}; 316 {StoB_REQ}; 317 {StoB_REQ; BtoS_ACK}; 318 {BtoS_ACK}; 319 {BtoS_ACK; BtoR_REQ}; 320 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 321 {BtoS_ACK; RtoB_ACK}; 322 {}; 323 {StoB_REQ}; 324 {StoB_REQ; BtoS_ACK}; 325 {BtoS_ACK}; 326 {BtoS_ACK; BtoR_REQ}; 327 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 328 {BtoS_ACK; RtoB_ACK}; 329 {}; 330 {StoB_REQ}; 331 {StoB_REQ; BtoS_ACK}; 332 {BtoS_ACK}; 333 {BtoS_ACK; BtoR_REQ}; 334 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 335 {BtoS_ACK; RtoB_ACK}; 336 {}; 337 {StoB_REQ}; 338 {StoB_REQ; BtoS_ACK}; 339 {BtoS_ACK}; 340 {BtoS_ACK; BtoR_REQ}; 341 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 342 {BtoS_ACK; RtoB_ACK}; 343 {}; 344 {StoB_REQ}; 345 {StoB_REQ; BtoS_ACK}; 346 {BtoS_ACK}; 347 {BtoS_ACK; BtoR_REQ}; 348 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 349 {BtoS_ACK; RtoB_ACK}; 350 {}; 351 {StoB_REQ}; 352 {StoB_REQ; BtoS_ACK}; 353 {BtoS_ACK}; 354 {BtoS_ACK; BtoR_REQ}; 355 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 356 {BtoS_ACK; RtoB_ACK}; 357 {}; 358 {StoB_REQ}; 359 {StoB_REQ; BtoS_ACK}; 360 {BtoS_ACK}; 361 {BtoS_ACK; BtoR_REQ}; 362 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 363 {BtoS_ACK; RtoB_ACK}; 364 {}; 365 {StoB_REQ}; 366 {StoB_REQ; BtoS_ACK}; 367 {BtoS_ACK}; 368 {BtoS_ACK; BtoR_REQ}; 369 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 370 {BtoS_ACK; RtoB_ACK}; 371 {}; 372 {StoB_REQ}; 373 {StoB_REQ; BtoS_ACK}; 374 {BtoS_ACK}; 375 {BtoS_ACK; BtoR_REQ}; 376 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 377 {BtoS_ACK; RtoB_ACK}; 378 {}; 379 {StoB_REQ}; 380 {StoB_REQ; BtoS_ACK}; 381 {BtoS_ACK}; 382 {BtoS_ACK; BtoR_REQ}; 383 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 384 {BtoS_ACK; RtoB_ACK}; 385 {}; 386 {StoB_REQ}; 387 {StoB_REQ; BtoS_ACK}; 388 {BtoS_ACK}; 389 {BtoS_ACK; BtoR_REQ}; 390 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 391 {BtoS_ACK; RtoB_ACK}; 392 {}; 393 {StoB_REQ}; 394 {StoB_REQ; BtoS_ACK}; 395 {BtoS_ACK}; 396 {BtoS_ACK; BtoR_REQ}; 397 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 398 {BtoS_ACK; RtoB_ACK}; 399 {}; 400 {StoB_REQ}; 401 {StoB_REQ; BtoS_ACK}; 402 {BtoS_ACK}; 403 {BtoS_ACK; BtoR_REQ}; 404 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 405 {BtoS_ACK; RtoB_ACK}; 406 {}; 407 {StoB_REQ}; 408 {StoB_REQ; BtoS_ACK}; 409 {BtoS_ACK}; 410 {BtoS_ACK; BtoR_REQ}; 411 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 412 {BtoS_ACK; RtoB_ACK}; 413 {}; 414 {StoB_REQ}; 415 {StoB_REQ; BtoS_ACK}; 416 {BtoS_ACK}; 417 {BtoS_ACK; BtoR_REQ}; 418 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 419 {BtoS_ACK; RtoB_ACK}; 420 {}; 421 {StoB_REQ}; 422 {StoB_REQ; BtoS_ACK}; 423 {BtoS_ACK}; 424 {BtoS_ACK; BtoR_REQ}; 425 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 426 {BtoS_ACK; RtoB_ACK}; 427 {}; 428 {StoB_REQ}; 429 {StoB_REQ; BtoS_ACK}; 430 {BtoS_ACK}; 431 {BtoS_ACK; BtoR_REQ}; 432 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 433 {BtoS_ACK; RtoB_ACK}; 434 {}; 435 {StoB_REQ}; 436 {StoB_REQ; BtoS_ACK}; 437 {BtoS_ACK}; 438 {BtoS_ACK; BtoR_REQ}; 439 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 440 {BtoS_ACK; RtoB_ACK}; 441 {}; 442 {StoB_REQ}; 443 {StoB_REQ; BtoS_ACK}; 444 {BtoS_ACK}; 445 {BtoS_ACK; BtoR_REQ}; 446 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 447 {BtoS_ACK; RtoB_ACK}; 448 {}; 449 {StoB_REQ}; 450 {StoB_REQ; BtoS_ACK}; 451 {BtoS_ACK}; 452 {BtoS_ACK; BtoR_REQ}; 453 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 454 {BtoS_ACK; RtoB_ACK}; 455 {}; 456 {StoB_REQ}; 457 {StoB_REQ; BtoS_ACK}; 458 {BtoS_ACK}; 459 {BtoS_ACK; BtoR_REQ}; 460 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 461 {BtoS_ACK; RtoB_ACK}; 462 {}; 463 {StoB_REQ}; 464 {StoB_REQ; BtoS_ACK}; 465 {BtoS_ACK}; 466 {BtoS_ACK; BtoR_REQ}; 467 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 468 {BtoS_ACK; RtoB_ACK}; 469 {}; 470 {StoB_REQ}; 471 {StoB_REQ; BtoS_ACK}; 472 {BtoS_ACK}; 473 {BtoS_ACK; BtoR_REQ}; 474 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 475 {BtoS_ACK; RtoB_ACK}; 476 {}; 477 {StoB_REQ}; 478 {StoB_REQ; BtoS_ACK}; 479 {BtoS_ACK}; 480 {BtoS_ACK; BtoR_REQ}; 481 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 482 {BtoS_ACK; RtoB_ACK}; 483 {}; 484 {StoB_REQ}; 485 {StoB_REQ; BtoS_ACK}; 486 {BtoS_ACK}; 487 {BtoS_ACK; BtoR_REQ}; 488 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 489 {BtoS_ACK; RtoB_ACK}; 490 {}; 491 {StoB_REQ}; 492 {StoB_REQ; BtoS_ACK}; 493 {BtoS_ACK}; 494 {BtoS_ACK; BtoR_REQ}; 495 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 496 {BtoS_ACK; RtoB_ACK}; 497 {}; 498 {StoB_REQ}; 499 {StoB_REQ; BtoS_ACK}; 500 {BtoS_ACK}; 501 {BtoS_ACK; BtoR_REQ}; 502 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 503 {BtoS_ACK; RtoB_ACK}; 504 {}; 505 {StoB_REQ}; 506 {StoB_REQ; BtoS_ACK}; 507 {BtoS_ACK}; 508 {BtoS_ACK; BtoR_REQ}; 509 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 510 {BtoS_ACK; RtoB_ACK}; 511 {}; 512 {StoB_REQ}; 513 {StoB_REQ; BtoS_ACK}; 514 {BtoS_ACK}; 515 {BtoS_ACK; BtoR_REQ}; 516 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 517 {BtoS_ACK; RtoB_ACK}; 518 {}; 519 {StoB_REQ}; 520 {StoB_REQ; BtoS_ACK}; 521 {BtoS_ACK}; 522 {BtoS_ACK; BtoR_REQ}; 523 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 524 {BtoS_ACK; RtoB_ACK}; 525 {}; 526 {StoB_REQ}; 527 {StoB_REQ; BtoS_ACK}; 528 {BtoS_ACK}; 529 {BtoS_ACK; BtoR_REQ}; 530 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 531 {BtoS_ACK; RtoB_ACK}; 532 {}; 533 {StoB_REQ}; 534 {StoB_REQ; BtoS_ACK}; 535 {BtoS_ACK}; 536 {BtoS_ACK; BtoR_REQ}; 537 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 538 {BtoS_ACK; RtoB_ACK}; 539 {}; 540 {StoB_REQ}; 541 {StoB_REQ; BtoS_ACK}; 542 {BtoS_ACK}; 543 {BtoS_ACK; BtoR_REQ}; 544 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 545 {BtoS_ACK; RtoB_ACK}; 546 {}; 547 {StoB_REQ}; 548 {StoB_REQ; BtoS_ACK}; 549 {BtoS_ACK}; 550 {BtoS_ACK; BtoR_REQ}; 551 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 552 {BtoS_ACK; RtoB_ACK}; 553 {}; 554 {StoB_REQ}; 555 {StoB_REQ; BtoS_ACK}; 556 {BtoS_ACK}; 557 {BtoS_ACK; BtoR_REQ}; 558 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 559 {BtoS_ACK; RtoB_ACK}; 560 {}; 561 {StoB_REQ}; 562 {StoB_REQ; BtoS_ACK}; 563 {BtoS_ACK}; 564 {BtoS_ACK; BtoR_REQ}; 565 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 566 {BtoS_ACK; RtoB_ACK}; 567 {}; 568 {StoB_REQ}; 569 {StoB_REQ; BtoS_ACK}; 570 {BtoS_ACK}; 571 {BtoS_ACK; BtoR_REQ}; 572 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 573 {BtoS_ACK; RtoB_ACK}; 574 {}; 575 {StoB_REQ}; 576 {StoB_REQ; BtoS_ACK}; 577 {BtoS_ACK}; 578 {BtoS_ACK; BtoR_REQ}; 579 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 580 {BtoS_ACK; RtoB_ACK}; 581 {}; 582 {StoB_REQ}; 583 {StoB_REQ; BtoS_ACK}; 584 {BtoS_ACK}; 585 {BtoS_ACK; BtoR_REQ}; 586 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 587 {BtoS_ACK; RtoB_ACK}; 588 {}; 589 {StoB_REQ}; 590 {StoB_REQ; BtoS_ACK}; 591 {BtoS_ACK}; 592 {BtoS_ACK; BtoR_REQ}; 593 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 594 {BtoS_ACK; RtoB_ACK}; 595 {}; 596 {StoB_REQ}; 597 {StoB_REQ; BtoS_ACK}; 598 {BtoS_ACK}; 599 {BtoS_ACK; BtoR_REQ}; 600 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 601 {BtoS_ACK; RtoB_ACK}; 602 {}; 603 {StoB_REQ}; 604 {StoB_REQ; BtoS_ACK}; 605 {BtoS_ACK}; 606 {BtoS_ACK; BtoR_REQ}; 607 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 608 {BtoS_ACK; RtoB_ACK}; 609 {}; 610 {StoB_REQ}; 611 {StoB_REQ; BtoS_ACK}; 612 {BtoS_ACK}; 613 {BtoS_ACK; BtoR_REQ}; 614 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 615 {BtoS_ACK; RtoB_ACK}; 616 {}; 617 {StoB_REQ}; 618 {StoB_REQ; BtoS_ACK}; 619 {BtoS_ACK}; 620 {BtoS_ACK; BtoR_REQ}; 621 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 622 {BtoS_ACK; RtoB_ACK}; 623 {}; 624 {StoB_REQ}; 625 {StoB_REQ; BtoS_ACK}; 626 {BtoS_ACK}; 627 {BtoS_ACK; BtoR_REQ}; 628 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 629 {BtoS_ACK; RtoB_ACK}; 630 {}; 631 {StoB_REQ}; 632 {StoB_REQ; BtoS_ACK}; 633 {BtoS_ACK}; 634 {BtoS_ACK; BtoR_REQ}; 635 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 636 {BtoS_ACK; RtoB_ACK}; 637 {}; 638 {StoB_REQ}; 639 {StoB_REQ; BtoS_ACK}; 640 {BtoS_ACK}; 641 {BtoS_ACK; BtoR_REQ}; 642 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 643 {BtoS_ACK; RtoB_ACK}; 644 {}; 645 {StoB_REQ}; 646 {StoB_REQ; BtoS_ACK}; 647 {BtoS_ACK}; 648 {BtoS_ACK; BtoR_REQ}; 649 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 650 {BtoS_ACK; RtoB_ACK}; 651 {}; 652 {StoB_REQ}; 653 {StoB_REQ; BtoS_ACK}; 654 {BtoS_ACK}; 655 {BtoS_ACK; BtoR_REQ}; 656 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 657 {BtoS_ACK; RtoB_ACK}; 658 {}; 659 {StoB_REQ}; 660 {StoB_REQ; BtoS_ACK}; 661 {BtoS_ACK}; 662 {BtoS_ACK; BtoR_REQ}; 663 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 664 {BtoS_ACK; RtoB_ACK}; 665 {}; 666 {StoB_REQ}; 667 {StoB_REQ; BtoS_ACK}; 668 {BtoS_ACK}; 669 {BtoS_ACK; BtoR_REQ}; 670 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 671 {BtoS_ACK; RtoB_ACK}; 672 {}; 673 {StoB_REQ}; 674 {StoB_REQ; BtoS_ACK}; 675 {BtoS_ACK}; 676 {BtoS_ACK; BtoR_REQ}; 677 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 678 {BtoS_ACK; RtoB_ACK}; 679 {}; 680 {StoB_REQ}; 681 {StoB_REQ; BtoS_ACK}; 682 {BtoS_ACK}; 683 {BtoS_ACK; BtoR_REQ}; 684 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 685 {BtoS_ACK; RtoB_ACK}; 686 {}; 687 {StoB_REQ}; 688 {StoB_REQ; BtoS_ACK}; 689 {BtoS_ACK}; 690 {BtoS_ACK; BtoR_REQ}; 691 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 692 {BtoS_ACK; RtoB_ACK}; 693 {}; 694 {StoB_REQ}; 695 {StoB_REQ; BtoS_ACK}; 696 {BtoS_ACK}; 697 {BtoS_ACK; BtoR_REQ}; 698 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 699 {BtoS_ACK; RtoB_ACK}; 700 {}; 701 {StoB_REQ}; 702 {StoB_REQ; BtoS_ACK}; 703 {BtoS_ACK}; 704 {BtoS_ACK; BtoR_REQ}; 705 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 706 {BtoS_ACK; RtoB_ACK}; 707 {}; 708 {StoB_REQ}; 709 {StoB_REQ; BtoS_ACK}; 710 {BtoS_ACK}; 711 {BtoS_ACK; BtoR_REQ}; 712 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 713 {BtoS_ACK; RtoB_ACK}; 714 {}; 715 {StoB_REQ}; 716 {StoB_REQ; BtoS_ACK}; 717 {BtoS_ACK}; 718 {BtoS_ACK; BtoR_REQ}; 719 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 720 {BtoS_ACK; RtoB_ACK}; 721 {}; 722 {StoB_REQ}; 723 {StoB_REQ; BtoS_ACK}; 724 {BtoS_ACK}; 725 {BtoS_ACK; BtoR_REQ}; 726 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 727 {BtoS_ACK; RtoB_ACK}; 728 {}; 729 {StoB_REQ}; 730 {StoB_REQ; BtoS_ACK}; 731 {BtoS_ACK}; 732 {BtoS_ACK; BtoR_REQ}; 733 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 734 {BtoS_ACK; RtoB_ACK}; 735 {}; 736 {StoB_REQ}; 737 {StoB_REQ; BtoS_ACK}; 738 {BtoS_ACK}; 739 {BtoS_ACK; BtoR_REQ}; 740 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 741 {BtoS_ACK; RtoB_ACK}; 742 {}; 743 {StoB_REQ}; 744 {StoB_REQ; BtoS_ACK}; 745 {BtoS_ACK}; 746 {BtoS_ACK; BtoR_REQ}; 747 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 748 {BtoS_ACK; RtoB_ACK}; 749 {}; 750 {StoB_REQ}; 751 {StoB_REQ; BtoS_ACK}; 752 {BtoS_ACK}; 753 {BtoS_ACK; BtoR_REQ}; 754 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 755 {BtoS_ACK; RtoB_ACK}; 756 {}; 757 {StoB_REQ}; 758 {StoB_REQ; BtoS_ACK}; 759 {BtoS_ACK}; 760 {BtoS_ACK; BtoR_REQ}; 761 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 762 {BtoS_ACK; RtoB_ACK}; 763 {}; 764 {StoB_REQ}; 765 {StoB_REQ; BtoS_ACK}; 766 {BtoS_ACK}; 767 {BtoS_ACK; BtoR_REQ}; 768 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 769 {BtoS_ACK; RtoB_ACK}; 770 {}; 771 {StoB_REQ}; 772 {StoB_REQ; BtoS_ACK}; 773 {BtoS_ACK}; 774 {BtoS_ACK; BtoR_REQ}; 775 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 776 {BtoS_ACK; RtoB_ACK}; 777 {}; 778 {StoB_REQ}; 779 {StoB_REQ; BtoS_ACK}; 780 {BtoS_ACK}; 781 {BtoS_ACK; BtoR_REQ}; 782 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 783 {BtoS_ACK; RtoB_ACK}; 784 {}; 785 {StoB_REQ}; 786 {StoB_REQ; BtoS_ACK}; 787 {BtoS_ACK}; 788 {BtoS_ACK; BtoR_REQ}; 789 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 790 {BtoS_ACK; RtoB_ACK}; 791 {}; 792 {StoB_REQ}; 793 {StoB_REQ; BtoS_ACK}; 794 {BtoS_ACK}; 795 {BtoS_ACK; BtoR_REQ}; 796 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 797 {BtoS_ACK; RtoB_ACK}; 798 {}; 799 {StoB_REQ}; 800 {StoB_REQ; BtoS_ACK}; 801 {BtoS_ACK}; 802 {BtoS_ACK; BtoR_REQ}; 803 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 804 {BtoS_ACK; RtoB_ACK}; 805 {}; 806 {StoB_REQ}; 807 {StoB_REQ; BtoS_ACK}; 808 {BtoS_ACK}; 809 {BtoS_ACK; BtoR_REQ}; 810 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 811 {BtoS_ACK; RtoB_ACK}; 812 {}; 813 {StoB_REQ}; 814 {StoB_REQ; BtoS_ACK}; 815 {BtoS_ACK}; 816 {BtoS_ACK; BtoR_REQ}; 817 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 818 {BtoS_ACK; RtoB_ACK}; 819 {}; 820 {StoB_REQ}; 821 {StoB_REQ; BtoS_ACK}; 822 {BtoS_ACK}; 823 {BtoS_ACK; BtoR_REQ}; 824 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 825 {BtoS_ACK; RtoB_ACK}; 826 {}; 827 {StoB_REQ}; 828 {StoB_REQ; BtoS_ACK}; 829 {BtoS_ACK}; 830 {BtoS_ACK; BtoR_REQ}; 831 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 832 {BtoS_ACK; RtoB_ACK}; 833 {}; 834 {StoB_REQ}; 835 {StoB_REQ; BtoS_ACK}; 836 {BtoS_ACK}; 837 {BtoS_ACK; BtoR_REQ}; 838 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 839 {BtoS_ACK; RtoB_ACK}; 840 {}; 841 {StoB_REQ}; 842 {StoB_REQ; BtoS_ACK}; 843 {BtoS_ACK}; 844 {BtoS_ACK; BtoR_REQ}; 845 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 846 {BtoS_ACK; RtoB_ACK}; 847 {}; 848 {StoB_REQ}; 849 {StoB_REQ; BtoS_ACK}; 850 {BtoS_ACK}; 851 {BtoS_ACK; BtoR_REQ}; 852 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 853 {BtoS_ACK; RtoB_ACK}; 854 {}; 855 {StoB_REQ}; 856 {StoB_REQ; BtoS_ACK}; 857 {BtoS_ACK}; 858 {BtoS_ACK; BtoR_REQ}; 859 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 860 {BtoS_ACK; RtoB_ACK}; 861 {}; 862 {StoB_REQ}; 863 {StoB_REQ; BtoS_ACK}; 864 {BtoS_ACK}; 865 {BtoS_ACK; BtoR_REQ}; 866 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 867 {BtoS_ACK; RtoB_ACK}; 868 {}; 869 {StoB_REQ}; 870 {StoB_REQ; BtoS_ACK}; 871 {BtoS_ACK}; 872 {BtoS_ACK; BtoR_REQ}; 873 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 874 {BtoS_ACK; RtoB_ACK}; 875 {}; 876 {StoB_REQ}; 877 {StoB_REQ; BtoS_ACK}; 878 {BtoS_ACK}; 879 {BtoS_ACK; BtoR_REQ}; 880 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 881 {BtoS_ACK; RtoB_ACK}; 882 {}; 883 {StoB_REQ}; 884 {StoB_REQ; BtoS_ACK}; 885 {BtoS_ACK}; 886 {BtoS_ACK; BtoR_REQ}; 887 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 888 {BtoS_ACK; RtoB_ACK}; 889 {}; 890 {StoB_REQ}; 891 {StoB_REQ; BtoS_ACK}; 892 {BtoS_ACK}; 893 {BtoS_ACK; BtoR_REQ}; 894 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 895 {BtoS_ACK; RtoB_ACK}; 896 {}; 897 {StoB_REQ}; 898 {StoB_REQ; BtoS_ACK}; 899 {BtoS_ACK}; 900 {BtoS_ACK; BtoR_REQ}; 901 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 902 {BtoS_ACK; RtoB_ACK}; 903 {}; 904 {StoB_REQ}; 905 {StoB_REQ; BtoS_ACK}; 906 {BtoS_ACK}; 907 {BtoS_ACK; BtoR_REQ}; 908 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 909 {BtoS_ACK; RtoB_ACK}; 910 {}; 911 {StoB_REQ}; 912 {StoB_REQ; BtoS_ACK}; 913 {BtoS_ACK}; 914 {BtoS_ACK; BtoR_REQ}; 915 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 916 {BtoS_ACK; RtoB_ACK}; 917 {}; 918 {StoB_REQ}; 919 {StoB_REQ; BtoS_ACK}; 920 {BtoS_ACK}; 921 {BtoS_ACK; BtoR_REQ}; 922 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 923 {BtoS_ACK; RtoB_ACK}; 924 {}; 925 {StoB_REQ}; 926 {StoB_REQ; BtoS_ACK}; 927 {BtoS_ACK}; 928 {BtoS_ACK; BtoR_REQ}; 929 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 930 {BtoS_ACK; RtoB_ACK}; 931 {}; 932 {StoB_REQ}; 933 {StoB_REQ; BtoS_ACK}; 934 {BtoS_ACK}; 935 {BtoS_ACK; BtoR_REQ}; 936 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 937 {BtoS_ACK; RtoB_ACK}; 938 {}; 939 {StoB_REQ}; 940 {StoB_REQ; BtoS_ACK}; 941 {BtoS_ACK}; 942 {BtoS_ACK; BtoR_REQ}; 943 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 944 {BtoS_ACK; RtoB_ACK}; 945 {}; 946 {StoB_REQ}; 947 {StoB_REQ; BtoS_ACK}; 948 {BtoS_ACK}; 949 {BtoS_ACK; BtoR_REQ}; 950 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 951 {BtoS_ACK; RtoB_ACK}; 952 {}; 953 {StoB_REQ}; 954 {StoB_REQ; BtoS_ACK}; 955 {BtoS_ACK}; 956 {BtoS_ACK; BtoR_REQ}; 957 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 958 {BtoS_ACK; RtoB_ACK}; 959 {}; 960 {StoB_REQ}; 961 {StoB_REQ; BtoS_ACK}; 962 {BtoS_ACK}; 963 {BtoS_ACK; BtoR_REQ}; 964 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 965 {BtoS_ACK; RtoB_ACK}; 966 {}; 967 {StoB_REQ}; 968 {StoB_REQ; BtoS_ACK}; 969 {BtoS_ACK}; 970 {BtoS_ACK; BtoR_REQ}; 971 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 972 {BtoS_ACK; RtoB_ACK}; 973 {}; 974 {StoB_REQ}; 975 {StoB_REQ; BtoS_ACK}; 976 {BtoS_ACK}; 977 {BtoS_ACK; BtoR_REQ}; 978 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 979 {BtoS_ACK; RtoB_ACK}; 980 {}; 981 {StoB_REQ}; 982 {StoB_REQ; BtoS_ACK}; 983 {BtoS_ACK}; 984 {BtoS_ACK; BtoR_REQ}; 985 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 986 {BtoS_ACK; RtoB_ACK}; 987 {}]`; 988 989quietdec := false; 990 991(* A pure computeLib version *) 992 993(****************************************************************************** 994* SimRun |= {[*]; StoB_REQ; [*]} 995******************************************************************************) 996val _ = 997time 998 EVAL 999 ``US_SEM 1000 SimRun 1001 (S_CAT(S_REPEAT S_TRUE, 1002 S_CAT(S_BOOL(B_PROP StoB_REQ), 1003 S_REPEAT S_TRUE)))``; 1004 1005(****************************************************************************** 1006* SimRun |= {[*]; StoB_REQ; StoB_REQ; [*]} 1007******************************************************************************) 1008val _ = 1009time 1010 EVAL 1011 ``US_SEM 1012 SimRun 1013 (S_CAT(S_REPEAT S_TRUE, 1014 S_CAT(S_CAT(S_BOOL(B_PROP StoB_REQ),S_BOOL(B_PROP StoB_REQ)), 1015 S_REPEAT S_TRUE)))``; 1016 1017 1018(****************************************************************************** 1019* SimRun |= {[*]; StoB_REQ; BtoR_REQ; [*]} 1020******************************************************************************) 1021val _ = 1022time 1023 EVAL 1024 ``US_SEM 1025 SimRun 1026 (S_CAT(S_REPEAT S_TRUE, 1027 S_CAT(S_CAT(S_BOOL(B_PROP StoB_REQ),S_BOOL(B_PROP BtoR_REQ)), 1028 S_REPEAT S_TRUE)))``; 1029 1030(****************************************************************************** 1031* The following 4 properties make up the vunit 1032* four_phase_handshake_left of page 19 of the FoCs User's Manual 1033* with "never r" replaced by "{r}(F)" 1034******************************************************************************) 1035 1036(****************************************************************************** 1037* {[*]; !StoB_REQ & BtoS_ACK; StoB_REQ}(F) 1038******************************************************************************) 1039val _ = 1040time 1041 EVAL 1042 ``UF_SEM 1043 (FINITE SimRun) 1044 (F_SUFFIX_IMP 1045 (S_CAT(S_REPEAT S_TRUE, 1046 S_CAT(S_BOOL(B_AND(B_NOT(B_PROP StoB_REQ), B_PROP BtoS_ACK)), 1047 S_BOOL(B_PROP StoB_REQ))), 1048 F_BOOL B_FALSE))``; 1049 1050(****************************************************************************** 1051* FINITE SimRun |= {[*]; StoB_REG & !BtoS_ACK; !StoB_REQ}(F) 1052******************************************************************************) 1053val _ = 1054time 1055 EVAL 1056 ``UF_SEM 1057 (FINITE SimRun) 1058 (F_SUFFIX_IMP 1059 (S_CAT(S_REPEAT S_TRUE, 1060 S_CAT(S_BOOL(B_AND(B_PROP StoB_REQ, B_NOT(B_PROP BtoS_ACK))), 1061 S_BOOL(B_NOT(B_PROP StoB_REQ)))), 1062 F_BOOL B_FALSE))``; 1063 1064(****************************************************************************** 1065* FINITE SimRun |= {[*]; !BtoS_ACK & !StoB_REQ; BtoS_ACK}(F) 1066******************************************************************************) 1067val _ = 1068time 1069 EVAL 1070 ``UF_SEM 1071 (FINITE SimRun) 1072 (F_SUFFIX_IMP 1073 (S_CAT(S_REPEAT S_TRUE, 1074 S_CAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK), 1075 B_NOT(B_PROP StoB_REQ))), 1076 S_BOOL(B_PROP BtoS_ACK))), 1077 F_BOOL B_FALSE))``; 1078 1079(****************************************************************************** 1080* {[*]; BtoS_ACK & StoB_REQ; !BtoS_ACK}(F) 1081******************************************************************************) 1082val _ = 1083time 1084 EVAL 1085 ``UF_SEM 1086 (FINITE SimRun) 1087 (F_SUFFIX_IMP 1088 (S_CAT(S_REPEAT S_TRUE, 1089 S_CAT(S_BOOL(B_AND(B_PROP BtoS_ACK, B_PROP StoB_REQ)), 1090 S_BOOL(B_NOT(B_PROP BtoS_ACK)))), 1091 F_BOOL B_FALSE))``; 1092 1093 1094(****************************************************************************** 1095* Make "&" into an infix for F_AND 1096******************************************************************************) 1097val _ = set_fixity "&" (Infixl 500); 1098val F_AND_IX_def = xDefine "F_AND_IX" `$& f1 f2 = F_AND(f1,f2)`; 1099 1100(****************************************************************************** 1101* A single property characterising a four-phase handshake 1102******************************************************************************) 1103 1104val FOUR_PHASE_def = 1105 Define 1106 `FOUR_PHASE req ack = 1107 F_SUFFIX_IMP 1108 (S_CAT(S_REPEAT S_TRUE, 1109 S_CAT(S_BOOL(B_AND(B_NOT(B_PROP req), B_PROP ack)), 1110 S_BOOL(B_PROP req))), 1111 F_BOOL B_FALSE) 1112 & 1113 F_SUFFIX_IMP 1114 (S_CAT(S_REPEAT S_TRUE, 1115 S_CAT(S_BOOL(B_AND(B_PROP req, B_NOT(B_PROP ack))), 1116 S_BOOL(B_NOT(B_PROP req)))), 1117 F_BOOL B_FALSE) 1118 & 1119 F_SUFFIX_IMP 1120 (S_CAT(S_REPEAT S_TRUE, 1121 S_CAT(S_BOOL(B_AND(B_NOT(B_PROP ack), B_NOT(B_PROP req))), 1122 S_BOOL(B_PROP ack))), 1123 F_BOOL B_FALSE) 1124 & 1125 F_SUFFIX_IMP 1126 (S_CAT(S_REPEAT S_TRUE, 1127 S_CAT(S_BOOL(B_AND(B_PROP ack, B_PROP req)), 1128 S_BOOL(B_NOT(B_PROP ack)))), 1129 F_BOOL B_FALSE)`; 1130 1131(****************************************************************************** 1132* vunit four_phase_handskake_left (page 19, FoCs User's Manual) 1133* FOUR_PHASE StoB_REQ BtoS_ACK 1134******************************************************************************) 1135val _ = 1136time EVAL ``UF_SEM (FINITE SimRun) (FOUR_PHASE StoB_REQ BtoS_ACK)``; 1137 1138 1139(****************************************************************************** 1140* vunit four_phase_handskake_right (page 20, FoCs User's Manual) 1141* FOUR_PHASE BtoR_REQ RtoB_ACK 1142******************************************************************************) 1143val _ = 1144time EVAL ``UF_SEM (FINITE SimRun) (FOUR_PHASE BtoR_REQ RtoB_ACK)``; 1145 1146(****************************************************************************** 1147* f1 before f2 = [not f2 W (f1 & not f2)] 1148******************************************************************************) 1149val F_BEFORE_def = 1150 Define 1151 `F_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`; 1152 1153(****************************************************************************** 1154* FINITE SimRun |= StoB_REQ before BtoS_ACK 1155******************************************************************************) 1156val _ = 1157time 1158 EVAL 1159 ``UF_SEM 1160 (FINITE SimRun) 1161 (F_BEFORE(F_BOOL(B_PROP StoB_REQ), F_BOOL(B_PROP BtoS_ACK)))``; 1162 1163(****************************************************************************** 1164* FINITE SimRun |= BtoS_ACK before StoB_REQ 1165******************************************************************************) 1166val _ = 1167time 1168 EVAL 1169 ``UF_SEM 1170 (FINITE SimRun) 1171 (F_BEFORE(F_BOOL(B_PROP BtoS_ACK), F_BOOL(B_PROP StoB_REQ)))``; 1172 1173(****************************************************************************** 1174* FINITE SimRun |= {[*]}(StoB_REQ before BtoS_ACK) 1175******************************************************************************) 1176val _ = 1177time 1178 EVAL 1179 ``UF_SEM 1180 (FINITE SimRun) 1181 (F_SUFFIX_IMP 1182 (S_REPEAT S_TRUE, 1183 F_BEFORE(F_BOOL(B_PROP StoB_REQ), F_BOOL(B_PROP BtoS_ACK))))``; 1184 1185(****************************************************************************** 1186* FINITE SimRun |= {[*]}(BtoS_ACK before StoB_REQ) 1187******************************************************************************) 1188val _ = 1189time 1190 EVAL 1191 ``UF_SEM 1192 (FINITE SimRun) 1193 (F_SUFFIX_IMP 1194 (S_REPEAT S_TRUE, 1195 F_BEFORE(F_BOOL(B_PROP BtoS_ACK), F_BOOL(B_PROP StoB_REQ))))``; 1196 1197 1198(****************************************************************************** 1199* Make ";;" into an infix for S_CAT 1200******************************************************************************) 1201val _ = set_fixity ";;" (Infixl 500); 1202val S_CAT_IX_def = xDefine "S_CAT_IX" `$;; r1 r2 = S_CAT(r1,r2)`; 1203 1204(****************************************************************************** 1205* FINITE SimRun |= {[*];!BtoS_ACK;BtoS_ACK}(F) 1206******************************************************************************) 1207val _ = 1208time 1209 EVAL 1210 ``UF_SEM 1211 (FINITE SimRun) 1212 (F_SUFFIX_IMP 1213 ((S_REPEAT(S_BOOL B_TRUE) ;; 1214 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1215 S_BOOL(B_PROP BtoS_ACK)), 1216 F_BOOL B_FALSE))``; 1217 1218(****************************************************************************** 1219* FINITE SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[*];!BtoS_ACK;BtoS_ACK}(F) 1220******************************************************************************) 1221val _ = 1222time 1223 EVAL 1224 ``UF_SEM 1225 (FINITE SimRun) 1226 (F_SUFFIX_IMP 1227 ((S_REPEAT(S_BOOL B_TRUE) ;; 1228 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1229 S_BOOL(B_PROP BtoS_ACK) ;; 1230 S_REPEAT(S_BOOL B_TRUE) ;; 1231 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1232 S_BOOL(B_PROP BtoS_ACK)), 1233 F_BOOL B_FALSE))``; 1234 1235(****************************************************************************** 1236* FINITE SimRun |= {[*];BtoS_ACK;[RtoB_ACK];BtoS_ACK}(F) 1237******************************************************************************) 1238val _ = 1239time 1240 EVAL 1241 ``UF_SEM 1242 (FINITE SimRun) 1243 (F_SUFFIX_IMP 1244 ((S_REPEAT(S_BOOL B_TRUE) ;; 1245 S_BOOL(B_PROP BtoS_ACK) ;; 1246 S_REPEAT(S_BOOL(B_PROP RtoB_ACK)) ;; 1247 S_BOOL(B_PROP BtoS_ACK)), 1248 F_BOOL B_FALSE))``; 1249 1250(****************************************************************************** 1251* FINITE SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[RtoB_ACK];!BtoS_ACK;BtoS_ACK}(F) 1252******************************************************************************) 1253val _ = 1254time 1255 EVAL 1256 ``UF_SEM 1257 (FINITE SimRun) 1258 (F_SUFFIX_IMP 1259 ((S_REPEAT(S_BOOL B_TRUE) ;; 1260 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1261 S_BOOL(B_PROP BtoS_ACK) ;; 1262 S_REPEAT(S_BOOL(B_PROP RtoB_ACK)) ;; 1263 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1264 S_BOOL(B_PROP BtoS_ACK)), 1265 F_BOOL B_FALSE))``; 1266 1267(****************************************************************************** 1268* FINITE SimRun |= {[*];BtoS_ACK;[!RtoB_ACK];BtoS_ACK}(F) 1269******************************************************************************) 1270val _ = 1271time 1272 EVAL 1273 ``UF_SEM 1274 (FINITE SimRun) 1275 (F_SUFFIX_IMP 1276 ((S_REPEAT(S_BOOL B_TRUE) ;; 1277 S_BOOL(B_PROP BtoS_ACK) ;; 1278 S_REPEAT(S_BOOL(B_NOT(B_PROP RtoB_ACK))) ;; 1279 S_BOOL(B_PROP BtoS_ACK)), 1280 F_BOOL B_FALSE))``; 1281 1282(****************************************************************************** 1283* FINITE SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[!RtoB_ACK];!BtoS_ACK;BtoS_ACK}(F) 1284******************************************************************************) 1285val _ = 1286time 1287 EVAL 1288 ``UF_SEM 1289 (FINITE SimRun) 1290 (F_SUFFIX_IMP 1291 ((S_REPEAT(S_BOOL B_TRUE) ;; 1292 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1293 S_BOOL(B_PROP BtoS_ACK) ;; 1294 S_REPEAT(S_BOOL(B_NOT(B_PROP RtoB_ACK))) ;; 1295 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1296 S_BOOL(B_PROP BtoS_ACK)), 1297 F_BOOL B_FALSE))``; 1298 1299(****************************************************************************** 1300* FINITE SimRun 1301* |= {[*];!BtoS_ACK;BtoS_ACK;[*];!RtoB_ACK;RtoB_ACK;[*];!BtoS_ACK;BtoS_ACK}(F) 1302******************************************************************************) 1303val _ = 1304time 1305 EVAL 1306 ``UF_SEM 1307 (FINITE SimRun) 1308 (F_SUFFIX_IMP 1309 ((S_REPEAT(S_BOOL B_TRUE) ;; 1310 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1311 S_BOOL(B_PROP BtoS_ACK) ;; 1312 S_REPEAT(S_BOOL(B_TRUE)) ;; 1313 S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; 1314 S_BOOL(B_PROP RtoB_ACK) ;; 1315 S_REPEAT(S_BOOL(B_TRUE)) ;; 1316 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1317 S_BOOL(B_PROP BtoS_ACK)), 1318 F_BOOL B_FALSE))``; 1319 1320(****************************************************************************** 1321* SimRun 1322* |= {[*];!BtoS_ACK;BtoS_ACK; 1323* [BtoS_ACK];[!BtoS_ACK]; 1324* ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK)); 1325* [!BtoS_ACK];BtoS_ACK} 1326******************************************************************************) 1327val _ = 1328time 1329 EVAL 1330 ``US_SEM 1331 SimRun 1332 ((S_REPEAT(S_BOOL B_TRUE) ;; 1333 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1334 S_BOOL(B_PROP BtoS_ACK) ;; 1335 S_REPEAT(S_BOOL(B_PROP BtoS_ACK));; 1336 S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; 1337 S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)), 1338 (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;; 1339 S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; 1340 S_BOOL(B_PROP BtoS_ACK)))``; 1341 1342(****************************************************************************** 1343* FINITE SimRun 1344* |= {[*];!BtoS_ACK;BtoS_ACK; 1345* [BtoS_ACK];[!BtoS_ACK]; 1346* ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK)); 1347* [!BtoS_ACK];BtoS_ACK} 1348* (F) 1349******************************************************************************) 1350val _ = 1351time 1352 EVAL 1353 ``UF_SEM 1354 (FINITE SimRun) 1355 (F_SUFFIX_IMP 1356 ((S_REPEAT(S_BOOL B_TRUE) ;; 1357 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1358 S_BOOL(B_PROP BtoS_ACK) ;; 1359 S_REPEAT(S_BOOL(B_PROP BtoS_ACK));; 1360 S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; 1361 S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)), 1362 (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;; 1363 S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; 1364 S_BOOL(B_PROP BtoS_ACK)), 1365 F_BOOL B_FALSE))``; 1366 1367(****************************************************************************** 1368* FINITE SimRun 1369* |= {[*];!BtoS_ACK;BtoS_ACK; 1370* [BtoS_ACK];[!BtoS_ACK]; 1371* ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK)); 1372* [!BtoS_ACK];BtoS_ACK} 1373* (T) 1374******************************************************************************) 1375val _ = 1376time 1377 EVAL 1378 ``UF_SEM 1379 (FINITE SimRun) 1380 (F_SUFFIX_IMP 1381 ((S_REPEAT(S_BOOL B_TRUE) ;; 1382 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1383 S_BOOL(B_PROP BtoS_ACK) ;; 1384 S_REPEAT(S_BOOL(B_PROP BtoS_ACK));; 1385 S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; 1386 S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)), 1387 (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;; 1388 S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; 1389 S_BOOL(B_PROP BtoS_ACK)), 1390 F_BOOL B_TRUE))``; 1391(****************************************************************************** 1392* FINITE SimRun 1393* |= {[*];!BtoS_ACK; 1394* BtoS_ACK; 1395* [BtoS_ACK&!RtoB_ACK]; 1396* [!BtoS_ACK&!RoB_ACK]; 1397* BtoS_ACK} 1398* (F) 1399******************************************************************************) 1400val _ = 1401time 1402 EVAL 1403 ``UF_SEM 1404 (FINITE SimRun) 1405 (F_SUFFIX_IMP 1406 ((S_REPEAT(S_BOOL B_TRUE) ;; 1407 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1408 S_BOOL(B_PROP BtoS_ACK) ;; 1409 S_REPEAT(S_BOOL(B_AND(B_PROP BtoS_ACK, 1410 B_NOT(B_PROP RtoB_ACK)))) ;; 1411 S_REPEAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK), 1412 B_NOT(B_PROP RtoB_ACK)))) ;; 1413 S_BOOL(B_PROP BtoS_ACK)), 1414 F_BOOL B_FALSE))``; 1415 1416 1417(****************************************************************************** 1418* FINITE SimRun |= (!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK) 1419******************************************************************************) 1420val _ = 1421time 1422 EVAL 1423 ``UF_SEM 1424 (FINITE SimRun) 1425 (F_BEFORE 1426 (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), 1427 F_NEXT(F_BOOL(B_PROP RtoB_ACK))), 1428 F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), 1429 F_NEXT(F_BOOL(B_PROP BtoS_ACK)))))``; 1430 1431(****************************************************************************** 1432* FINITE SimRun 1433* |= {[*]; !BtoS_ACK; BtoS_ACK; true} 1434* ((!RtoB_ACK & X RtoB_ACK) before (!BtoS_ACK & X BtoS_ACK)) 1435******************************************************************************) 1436val _ = 1437time 1438 EVAL 1439 ``UF_SEM 1440 (FINITE SimRun) 1441 (F_SUFFIX_IMP 1442 ((S_REPEAT(S_BOOL B_TRUE) ;; 1443 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1444 S_BOOL(B_PROP BtoS_ACK) ;; 1445 S_BOOL B_TRUE), 1446 F_BEFORE 1447 (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), 1448 F_NEXT(F_BOOL(B_PROP RtoB_ACK))), 1449 F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), 1450 F_NEXT(F_BOOL(B_PROP BtoS_ACK))))))``; 1451 1452(****************************************************************************** 1453* FINITE SimRun 1454* |= {[*]; !RtoB_ACK; RtoB_ACK; true} 1455* ((!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK)) 1456******************************************************************************) 1457val _ = 1458time 1459 EVAL 1460 ``UF_SEM 1461 (FINITE SimRun) 1462 (F_SUFFIX_IMP 1463 ((S_REPEAT(S_BOOL B_TRUE) ;; 1464 S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; 1465 S_BOOL(B_PROP RtoB_ACK) ;; 1466 S_BOOL B_TRUE), 1467 F_BEFORE 1468 (F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), 1469 F_NEXT(F_BOOL(B_PROP BtoS_ACK))), 1470 F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), 1471 F_NEXT(F_BOOL(B_PROP RtoB_ACK))))))``; 1472 1473 1474(****************************************************************************** 1475* FINITE SimRun 1476* |= {[*]; !BtoS_ACK; BtoS_ACK} 1477* ((!RtoB_ACK & X RtoB_ACK) before (!BtoS_ACK & X BtoS_ACK)) 1478******************************************************************************) 1479val _ = 1480time 1481 EVAL 1482 ``UF_SEM 1483 (FINITE SimRun) 1484 (F_SUFFIX_IMP 1485 ((S_REPEAT(S_BOOL B_TRUE) ;; 1486 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 1487 S_BOOL(B_PROP BtoS_ACK)), 1488 F_BEFORE 1489 (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), 1490 F_NEXT(F_BOOL(B_PROP RtoB_ACK))), 1491 F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), 1492 F_NEXT(F_BOOL(B_PROP BtoS_ACK))))))``; 1493 1494(****************************************************************************** 1495* FINITE SimRun 1496* |= {[*]; !RtoB_ACK; RtoB_ACK} 1497* ((!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK)) 1498******************************************************************************) 1499val _ = 1500time 1501 EVAL 1502 ``UF_SEM 1503 (FINITE SimRun) 1504 (F_SUFFIX_IMP 1505 ((S_REPEAT(S_BOOL B_TRUE) ;; 1506 S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; 1507 S_BOOL(B_PROP RtoB_ACK)), 1508 F_BEFORE 1509 (F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), 1510 F_NEXT(F_BOOL(B_PROP BtoS_ACK))), 1511 F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), 1512 F_NEXT(F_BOOL(B_PROP RtoB_ACK))))))``; 1513 1514(****************************************************************************** 1515* Generating checkers from formulas. 1516* An example from the Accellera PSL reference manual, page 45. 1517* Mentioned in Joe Hurd's ARG Lunch, 4 November 2003. 1518******************************************************************************) 1519val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define; 1520val a_def = pureDefine `a = 0`; 1521val b_def = pureDefine `b = 1`; 1522val c_def = pureDefine `c = 2`; 1523val alpha = map Term [`a`,`b`,`c`]; 1524val prop = ``F_AND (F_BOOL (B_PROP c), 1525 F_NEXT (F_W (F_BOOL (B_PROP a), F_BOOL (B_PROP b))))``; 1526val prop_sere = time EVAL ``checker ^prop``; 1527val sere = rhs (concl prop_sere); 1528val sere_re = time EVAL ``sere2regexp ^sere``; 1529val re = rhs (concl sere_re); 1530val dfa = verilog_dfa {alphabet = alpha, name = "Checker1", regexp = re}; 1531val _ = print ("\n\n" ^ dfa ^ "\n\n"); 1532