1(* -*-sml-*- *) 2(*****************************************************************************) 3(* Sanity checking "ExecuteSemantics": a derived executable semantics *) 4(* Not for compiling. *) 5(*****************************************************************************) 6 7loadPath := "../official-semantics" :: "../regexp" :: !loadPath; 8app 9 load 10 ["bossLib","metisLib","intLib","stringLib","pred_setLib", 11 "regexpLib","ExecuteSemanticsTheory","PropertiesTheory"]; 12 13quietdec := true; 14open bossLib metisLib intLib stringLib rich_listTheory 15open regexpLib FinitePSLPathTheory UnclockedSemanticsTheory ExecuteSemanticsTheory; 16quietdec := false; 17 18(****************************************************************************** 19* Set default parsing to natural numbers rather than integers 20******************************************************************************) 21val _ = intLib.deprecate_int(); 22 23(****************************************************************************** 24* Version of Define that doesn't add to the EVAL compset 25******************************************************************************) 26val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define; 27 28(****************************************************************************** 29* Evaluating expressions of the form x IN {y1; y2; ...; yn} 30******************************************************************************) 31 32(* For the current set of Sugar2 example properties, the following INSERT 33 theorems seem to work better than this general conversion. 34val _ = 35 computeLib.add_convs 36 [(``$IN``, 37 2, 38 (pred_setLib.SET_SPEC_CONV ORELSEC pred_setLib.IN_CONV EVAL))]; 39*) 40 41val () = computeLib.add_funs 42 [pred_setTheory.IN_INSERT, 43 pred_setTheory.NOT_IN_EMPTY]; 44 45(****************************************************************************** 46* Evaluating Sugar2 formulas 47******************************************************************************) 48val _ = computeLib.add_funs 49 ([PSLPathTheory.SEL_REC_AUX, 50 UF_SEM_F_UNTIL_REC, 51 B_SEM, 52 EVAL_US_SEM, 53 EVAL_UF_SEM_F_SUFFIX_IMP, 54 UF_SEM_F_STRONG_IMP_F_SUFFIX_IMP]); 55 56(****************************************************************************** 57* For simplification during symbolic evaluation of Sugar2 formulas 58******************************************************************************) 59 60val EXISTS_COND = prove 61 (``!p c a b. 62 EXISTS p (if c then a else b) = if c then EXISTS p a else EXISTS p b``, 63 RW_TAC std_ss []); 64 65val COND_SIMP = prove 66 (``!c a b. 67 (COND c a F = c /\ a) /\ (COND c a T = ~c \/ a) /\ 68 (COND c T b = c \/ b) /\ (COND c F b = ~c /\ b)``, 69 RW_TAC std_ss [IMP_DISJ_THM]); 70 71val () = computeLib.add_funs [EXISTS_COND, COND_SIMP]; 72 73(****************************************************************************** 74* Examples 75******************************************************************************) 76 77(* 78** Generated this from a Verilog model of the BUF example in 79** Chapter 4 of FoCs User's Manual (see test2.v) 80** but with each component separately clocked 81** (www.haifa.il.ibm.com/projects/verification/focs/) 82*) 83 84val clk1_def = Define `clk1 = 1`; 85val clk2_def = Define `clk2 = 2`; 86val clk3_def = Define `clk3 = 3`; 87val StoB_REQ_def = Define `StoB_REQ = 4`; 88val BtoS_ACK_def = Define `BtoS_ACK = 5`; 89val BtoR_REQ_def = Define `BtoR_REQ = 6`; 90val RtoB_ACK_def = Define `RtoB_ACK = 7`; 91 92 93quietdec := true; 94val SimRun_def = 95 Define 96 `SimRun = 97 [{}; 98 {}; 99 {}; 100 {}; 101 {clk1}; 102 {clk1; clk2}; 103 {clk2; StoB_REQ}; 104 {clk2; clk3; StoB_REQ}; 105 {clk3; StoB_REQ}; 106 {clk1; clk3; StoB_REQ}; 107 {clk1; clk2; clk3; StoB_REQ}; 108 {clk2; clk3; StoB_REQ}; 109 {clk2; StoB_REQ}; 110 {clk2; StoB_REQ; BtoS_ACK}; 111 {StoB_REQ; BtoS_ACK}; 112 {clk1; StoB_REQ; BtoS_ACK}; 113 {clk1; BtoS_ACK}; 114 {clk1; clk3; BtoS_ACK}; 115 {clk1; clk2; clk3; BtoS_ACK}; 116 {clk2; clk3; BtoS_ACK}; 117 {clk2; clk3; BtoS_ACK; BtoR_REQ}; 118 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ}; 119 {clk1; clk3; BtoS_ACK; BtoR_REQ}; 120 {clk1; BtoS_ACK; BtoR_REQ}; 121 {BtoS_ACK; BtoR_REQ}; 122 {clk2; BtoS_ACK; BtoR_REQ}; 123 {clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 124 {clk1; clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 125 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 126 {clk1; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 127 {clk1; clk3; BtoS_ACK; RtoB_ACK}; 128 {clk3; BtoS_ACK; RtoB_ACK}; 129 {clk2; clk3; BtoS_ACK; RtoB_ACK}; 130 {clk2; clk3}; 131 {clk2}; 132 {clk1; clk2}; 133 {clk1}; 134 {}; 135 {clk3}; 136 {clk2; clk3}; 137 {clk1; clk2; clk3}; 138 {clk2; clk3; StoB_REQ}; 139 {clk3; StoB_REQ}; 140 {StoB_REQ}; 141 {clk1; StoB_REQ}; 142 {clk1; clk2; StoB_REQ}; 143 {clk2; clk3; StoB_REQ}; 144 {clk2; clk3; StoB_REQ; BtoS_ACK}; 145 {clk3; StoB_REQ; BtoS_ACK}; 146 {clk1; clk3; StoB_REQ; BtoS_ACK}; 147 {clk1; clk3; BtoS_ACK}; 148 {clk1; clk2; clk3; BtoS_ACK}; 149 {clk1; clk2; BtoS_ACK}; 150 {clk2; BtoS_ACK}; 151 {clk2; BtoS_ACK; BtoR_REQ}; 152 {BtoS_ACK; BtoR_REQ}; 153 {clk1; BtoS_ACK; BtoR_REQ}; 154 {clk1; clk3; BtoS_ACK; BtoR_REQ}; 155 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ}; 156 {clk2; clk3; BtoS_ACK; BtoR_REQ}; 157 {clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 158 {clk1; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 159 {clk1; BtoS_ACK; RtoB_ACK}; 160 {clk2; BtoS_ACK; RtoB_ACK}; 161 {clk2}; 162 {clk2; clk3}; 163 {clk1; clk2; clk3}; 164 {clk1; clk3}; 165 {clk3}; 166 {clk2; clk3}; 167 {clk2}; 168 {clk1; clk2}; 169 {clk1}; 170 {StoB_REQ}; 171 {clk3; StoB_REQ}; 172 {clk2; clk3; StoB_REQ}; 173 {clk1; clk2; clk3; StoB_REQ}; 174 {clk1; clk2; clk3; StoB_REQ; BtoS_ACK}; 175 {clk1; StoB_REQ; BtoS_ACK}; 176 {StoB_REQ; BtoS_ACK}; 177 {BtoS_ACK}; 178 {clk2; BtoS_ACK}; 179 {clk1; clk2; BtoS_ACK}; 180 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ}; 181 {clk2; clk3; BtoS_ACK; BtoR_REQ}; 182 {clk3; BtoS_ACK; BtoR_REQ}; 183 {clk1; clk3; BtoS_ACK; BtoR_REQ}; 184 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ}; 185 {clk1; clk2; BtoS_ACK; BtoR_REQ}; 186 {clk1; clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 187 {clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 188 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 189 {BtoS_ACK; RtoB_ACK}; 190 {clk1; clk3; BtoS_ACK; RtoB_ACK}; 191 {clk1; clk2; clk3; BtoS_ACK; RtoB_ACK}; 192 {clk1; clk2; clk3}; 193 {clk2; clk3}; 194 {clk2}; 195 {}; 196 {clk1}; 197 {clk1; clk2}; 198 {clk2; StoB_REQ}; 199 {clk2; clk3; StoB_REQ}; 200 {clk1; clk2; clk3; StoB_REQ}; 201 {clk1; clk3; StoB_REQ}; 202 {clk3; StoB_REQ}; 203 {clk2; StoB_REQ}; 204 {clk1; clk2; StoB_REQ}; 205 {clk1; clk2; StoB_REQ; BtoS_ACK}; 206 {clk1; StoB_REQ; BtoS_ACK}; 207 {clk1; clk3; StoB_REQ; BtoS_ACK}; 208 {clk3; StoB_REQ; BtoS_ACK}; 209 {clk3; BtoS_ACK}; 210 {clk2; clk3; BtoS_ACK}; 211 {clk1; clk2; clk3; BtoS_ACK}; 212 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ}; 213 {clk1; clk2; BtoS_ACK; BtoR_REQ}; 214 {clk1; BtoS_ACK; BtoR_REQ}; 215 {BtoS_ACK; BtoR_REQ}; 216 {clk2; BtoS_ACK; BtoR_REQ}; 217 {clk1; clk2; BtoS_ACK; BtoR_REQ}; 218 {clk1; clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 219 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 220 {clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 221 {clk3; BtoS_ACK; RtoB_ACK}; 222 {BtoS_ACK; RtoB_ACK}; 223 {clk1; clk2; BtoS_ACK; RtoB_ACK}; 224 {clk1; clk2}; 225 {clk2}; 226 {}; 227 {clk3}; 228 {clk1; clk3}; 229 {clk1; clk2; clk3}; 230 {clk2; clk3; StoB_REQ}; 231 {clk2; StoB_REQ}; 232 {StoB_REQ}; 233 {clk1; StoB_REQ}; 234 {clk1; clk2; StoB_REQ}; 235 {clk2; clk3; StoB_REQ}; 236 {clk2; clk3; StoB_REQ; BtoS_ACK}; 237 {clk3; StoB_REQ; BtoS_ACK}; 238 {clk1; clk3; StoB_REQ; BtoS_ACK}; 239 {clk1; clk3; BtoS_ACK}; 240 {clk1; BtoS_ACK}; 241 {clk1; clk2; BtoS_ACK}; 242 {clk2; BtoS_ACK}; 243 {clk2; BtoS_ACK; BtoR_REQ}; 244 {clk1; clk2; BtoS_ACK; BtoR_REQ}; 245 {clk1; BtoS_ACK; BtoR_REQ}; 246 {clk1; clk3; BtoS_ACK; BtoR_REQ}; 247 {clk3; BtoS_ACK; BtoR_REQ}; 248 {clk2; clk3; BtoS_ACK; BtoR_REQ}; 249 {clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 250 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 251 {clk1; clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 252 {clk1; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 253 {clk1; BtoS_ACK; RtoB_ACK}; 254 {BtoS_ACK; RtoB_ACK}; 255 {clk2; BtoS_ACK; RtoB_ACK}; 256 {clk2}; 257 {clk2; clk3}; 258 {clk1; clk2; clk3}; 259 {clk1; clk3}; 260 {clk3}; 261 {}; 262 {clk2}; 263 {clk1; clk2}; 264 {clk2; StoB_REQ}; 265 {StoB_REQ}; 266 {clk3; StoB_REQ}; 267 {clk1; clk3; StoB_REQ}; 268 {clk1; clk2; clk3; StoB_REQ}; 269 {clk1; clk2; StoB_REQ}; 270 {clk2; StoB_REQ}; 271 {clk2; StoB_REQ; BtoS_ACK}; 272 {StoB_REQ; BtoS_ACK}; 273 {clk1; StoB_REQ; BtoS_ACK}; 274 {clk1; BtoS_ACK}; 275 {clk1; clk2; BtoS_ACK}; 276 {clk1; clk2; clk3; BtoS_ACK}; 277 {clk2; clk3; BtoS_ACK}; 278 {clk2; clk3; BtoS_ACK; BtoR_REQ}; 279 {clk3; BtoS_ACK; BtoR_REQ}; 280 {clk1; clk3; BtoS_ACK; BtoR_REQ}; 281 {clk1; BtoS_ACK; BtoR_REQ}; 282 {clk1; clk2; BtoS_ACK; BtoR_REQ}; 283 {clk2; BtoS_ACK; BtoR_REQ}; 284 {clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 285 {clk1; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 286 {clk1; clk3; BtoS_ACK; RtoB_ACK}; 287 {clk2; clk3; BtoS_ACK; RtoB_ACK}; 288 {clk2; clk3}; 289 {clk2}; 290 {clk1; clk2}; 291 {clk1}; 292 {}; 293 {clk2}; 294 {clk2; clk3}; 295 {clk1; clk2; clk3}; 296 {clk1; clk3}; 297 {clk3; StoB_REQ}; 298 {StoB_REQ}; 299 {clk2; StoB_REQ}; 300 {clk1; clk2; StoB_REQ}; 301 {clk1; clk2; StoB_REQ; BtoS_ACK}; 302 {clk1; clk2; clk3; StoB_REQ; BtoS_ACK}; 303 {clk1; clk3; StoB_REQ; BtoS_ACK}; 304 {clk3; StoB_REQ; BtoS_ACK}; 305 {clk3; BtoS_ACK}; 306 {clk2; clk3; BtoS_ACK}; 307 {clk1; clk2; clk3; BtoS_ACK}; 308 {clk1; clk2; BtoS_ACK}; 309 {clk1; clk2; BtoS_ACK; BtoR_REQ}; 310 {clk2; BtoS_ACK; BtoR_REQ}; 311 {BtoS_ACK; BtoR_REQ}; 312 {clk1; BtoS_ACK; BtoR_REQ}; 313 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ}; 314 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 315 {clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 316 {clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 317 {clk3; BtoS_ACK; RtoB_ACK}; 318 {BtoS_ACK; RtoB_ACK}; 319 {clk1; BtoS_ACK; RtoB_ACK}; 320 {clk1; clk2; BtoS_ACK; RtoB_ACK}; 321 {clk1; clk2}; 322 {clk2}; 323 {clk2; clk3}; 324 {clk3}; 325 {clk1; clk3}; 326 {clk1; clk2; clk3}; 327 {clk2; clk3; StoB_REQ}; 328 {clk2; StoB_REQ}; 329 {clk1; clk2; StoB_REQ}; 330 {clk1; StoB_REQ}; 331 {clk3; StoB_REQ}; 332 {clk2; clk3; StoB_REQ}; 333 {clk1; clk2; clk3; StoB_REQ}; 334 {clk1; clk2; clk3; StoB_REQ; BtoS_ACK}; 335 {clk1; clk3; StoB_REQ; BtoS_ACK}; 336 {clk1; StoB_REQ; BtoS_ACK}; 337 {StoB_REQ; BtoS_ACK}; 338 {BtoS_ACK}; 339 {clk2; BtoS_ACK}; 340 {clk1; clk2; BtoS_ACK}; 341 {clk1; clk2; BtoS_ACK; BtoR_REQ}; 342 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ}; 343 {clk1; clk3; BtoS_ACK; BtoR_REQ}; 344 {clk3; BtoS_ACK; BtoR_REQ}; 345 {clk2; clk3; BtoS_ACK; BtoR_REQ}; 346 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ}; 347 {clk1; clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 348 {BtoS_ACK; BtoR_REQ; RtoB_ACK}; 349 {BtoS_ACK; RtoB_ACK}; 350 {clk3; BtoS_ACK; RtoB_ACK}; 351 {clk1; clk2; clk3; BtoS_ACK; RtoB_ACK}; 352 {clk1; clk2; clk3}; 353 {clk2; clk3}; 354 {clk3}; 355 {}; 356 {clk1}; 357 {clk1; clk2}; 358 {clk2; StoB_REQ}; 359 {clk2; clk3; StoB_REQ}; 360 {clk3; StoB_REQ}; 361 {clk1; clk3; StoB_REQ}; 362 {clk1; clk2; clk3; StoB_REQ}; 363 {clk1; clk2; StoB_REQ}; 364 {clk2; StoB_REQ}; 365 {clk2; StoB_REQ; BtoS_ACK}; 366 {StoB_REQ; BtoS_ACK}; 367 {clk1; StoB_REQ; BtoS_ACK}; 368 {clk1; clk3; BtoS_ACK}; 369 {clk1; clk2; clk3; BtoS_ACK}; 370 {clk2; clk3; BtoS_ACK}; 371 {clk2; clk3; BtoS_ACK; BtoR_REQ}; 372 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ}; 373 {clk1; clk3; BtoS_ACK; BtoR_REQ}; 374 {clk1; BtoS_ACK; BtoR_REQ}; 375 {BtoS_ACK; BtoR_REQ}; 376 {clk2; BtoS_ACK; BtoR_REQ}; 377 {clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 378 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 379 {clk1; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 380 {clk1; clk3; BtoS_ACK; RtoB_ACK}; 381 {clk3; BtoS_ACK; RtoB_ACK}; 382 {clk2; clk3; BtoS_ACK; RtoB_ACK}; 383 {clk2; clk3}; 384 {clk2}; 385 {clk1; clk2}; 386 {clk1}; 387 {}; 388 {clk3}; 389 {clk2; clk3}; 390 {clk1; clk2; clk3}; 391 {clk2; clk3; StoB_REQ}; 392 {StoB_REQ}; 393 {clk1; StoB_REQ}; 394 {clk1; clk2; StoB_REQ}; 395 {clk1; clk2; clk3; StoB_REQ}; 396 {clk2; clk3; StoB_REQ}; 397 {clk2; clk3; StoB_REQ; BtoS_ACK}; 398 {clk3; StoB_REQ; BtoS_ACK}; 399 {clk1; clk3; StoB_REQ; BtoS_ACK}; 400 {clk1; clk3; BtoS_ACK}; 401 {clk1; clk2; clk3; BtoS_ACK}; 402 {clk1; clk2; BtoS_ACK}; 403 {clk2; BtoS_ACK}; 404 {clk2; BtoS_ACK; BtoR_REQ}; 405 {BtoS_ACK; BtoR_REQ}; 406 {clk1; BtoS_ACK; BtoR_REQ}; 407 {clk1; clk3; BtoS_ACK; BtoR_REQ}; 408 {clk1; clk2; clk3; BtoS_ACK; BtoR_REQ}; 409 {clk2; clk3; BtoS_ACK; BtoR_REQ}; 410 {clk2; clk3; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 411 {clk2; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 412 {clk1; BtoS_ACK; BtoR_REQ; RtoB_ACK}; 413 {clk1; BtoS_ACK; RtoB_ACK}; 414 {clk2; BtoS_ACK; RtoB_ACK}; 415 {clk2}; 416 {clk2; clk3}; 417 {clk1; clk2; clk3}; 418 {clk1; clk3}; 419 {clk3}; 420 {clk2}; 421 {clk1; clk2}; 422 {clk1}; 423 {clk3}; 424 {clk2; clk3}]`; 425quietdec := false; 426 427(* A pure computeLib version *) 428time 429 EVAL 430 ``US_SEM 431 SimRun 432 (S_CAT(S_REPEAT S_TRUE, 433 S_CAT(S_BOOL(B_PROP StoB_REQ), 434 S_REPEAT S_TRUE)))``; 435 436(* A version using BIGLIST to keep terms small 437 (however, it doesn't seem to have much effect) 438val SimRun_def = pureDefine `SimRun = SimRun`; 439val () = computeLib.add_funs (time EVAL_BIGLIST SimRun_def); 440time 441 EVAL 442 ``US_SEM 443 (BIGLIST SimRun) 444 (S_CAT(S_REPEAT S_TRUE, 445 S_CAT(S_BOOL(B_PROP StoB_REQ), 446 S_REPEAT S_TRUE)))``; 447*) 448 449time 450 EVAL 451 ``US_SEM 452 SimRun 453 (S_CAT(S_REPEAT S_TRUE, 454 S_CAT(S_CAT(S_BOOL(B_PROP StoB_REQ),S_BOOL(B_PROP StoB_REQ)), 455 S_REPEAT S_TRUE)))``; 456 457time 458 EVAL 459 ``US_SEM 460 SimRun 461 (S_CAT(S_REPEAT S_TRUE, 462 S_CAT(S_CAT(S_BOOL(B_PROP StoB_REQ),S_BOOL(B_PROP BtoR_REQ)), 463 S_REPEAT S_TRUE)))``; 464 465(****************************************************************************** 466* The following 4 properties make up the vunit 467* four_phase_handshake_left of page 19 of the FoCs User's Manual 468* with "never r" replaced by "{r}(F)" 469******************************************************************************) 470 471(* 472** {[*]; !StoB_REQ & BtoS_ACK; StoB_REQ}(F) 473*) 474time 475 EVAL 476 ``UF_SEM 477 (FINITE SimRun) 478 (F_SUFFIX_IMP 479 (S_CAT(S_REPEAT S_TRUE, 480 S_CAT(S_BOOL(B_AND(B_NOT(B_PROP StoB_REQ), B_PROP BtoS_ACK)), 481 S_BOOL(B_PROP StoB_REQ))), 482 F_BOOL B_FALSE))``; 483 484(* 485** {[*]; StoB_REG & !BtoS_ACK; !StoB_REQ}(F) 486*) 487time 488 EVAL 489 ``UF_SEM 490 (FINITE SimRun) 491 (F_SUFFIX_IMP 492 (S_CAT(S_REPEAT S_TRUE, 493 S_CAT(S_BOOL(B_AND(B_PROP StoB_REQ, B_NOT(B_PROP BtoS_ACK))), 494 S_BOOL(B_NOT(B_PROP StoB_REQ)))), 495 F_BOOL B_FALSE))``; 496 497(* 498** {[*]; !BtoS_ACK & !StoB_REQ; BtoS_ACK}(F) 499*) 500time 501 EVAL 502 ``UF_SEM 503 (FINITE SimRun) 504 (F_SUFFIX_IMP 505 (S_CAT(S_REPEAT S_TRUE, 506 S_CAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK), B_NOT(B_PROP StoB_REQ))), 507 S_BOOL(B_PROP BtoS_ACK))), 508 F_BOOL B_FALSE))``; 509 510(* 511** {[*]; BtoS_ACK & StoB_REQ; !BtoS_ACK}(F) 512*) 513time 514 EVAL 515 ``UF_SEM 516 (FINITE SimRun) 517 (F_SUFFIX_IMP 518 (S_CAT(S_REPEAT S_TRUE, 519 S_CAT(S_BOOL(B_AND(B_PROP BtoS_ACK, B_PROP StoB_REQ)), 520 S_BOOL(B_NOT(B_PROP BtoS_ACK)))), 521 F_BOOL B_FALSE))``; 522 523 524(****************************************************************************** 525* Make "&" into an infix for F_AND 526******************************************************************************) 527val _ = set_fixity "&" (Infixl 500); 528val F_AND_IX_def = xDefine "F_AND_IX" `$& f1 f2 = F_AND(f1,f2)`; 529 530(****************************************************************************** 531* A single property characterising a four-phasse handshake 532******************************************************************************) 533 534val FOUR_PHASE_def = 535 Define 536 `FOUR_PHASE req ack = 537 F_SUFFIX_IMP 538 (S_CAT(S_REPEAT S_TRUE, 539 S_CAT(S_BOOL(B_AND(B_NOT(B_PROP req), B_PROP ack)), 540 S_BOOL(B_PROP req))), 541 F_BOOL B_FALSE) 542 & 543 F_SUFFIX_IMP 544 (S_CAT(S_REPEAT S_TRUE, 545 S_CAT(S_BOOL(B_AND(B_PROP req, B_NOT(B_PROP ack))), 546 S_BOOL(B_NOT(B_PROP req)))), 547 F_BOOL B_FALSE) 548 & 549 F_SUFFIX_IMP 550 (S_CAT(S_REPEAT S_TRUE, 551 S_CAT(S_BOOL(B_AND(B_NOT(B_PROP ack), B_NOT(B_PROP req))), 552 S_BOOL(B_PROP ack))), 553 F_BOOL B_FALSE) 554 & 555 F_SUFFIX_IMP 556 (S_CAT(S_REPEAT S_TRUE, 557 S_CAT(S_BOOL(B_AND(B_PROP ack, B_PROP req)), 558 S_BOOL(B_NOT(B_PROP ack)))), 559 F_BOOL B_FALSE)`; 560 561(* 562** vunit four_phase_handskake_left (page 19, FoCs User's Manual) 563** FOUR_PHASE StoB_REQ BtoS_ACK 564*) 565 566time EVAL ``UF_SEM (FINITE SimRun) (FOUR_PHASE StoB_REQ BtoS_ACK)``; 567 568 569(* 570** vunit four_phase_handskake_right (page 20, FoCs User's Manual) 571** FOUR_PHASE BtoR_REQ RtoB_ACK 572*) 573 574time EVAL ``UF_SEM (FINITE SimRun) (FOUR_PHASE BtoR_REQ RtoB_ACK)``; 575 576(****************************************************************************** 577* f1 before f2 = [not f2 W (f1 & not f2)] 578******************************************************************************) 579val F_BEFORE_def = 580 Define 581 `F_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`; 582 583(* 584** SimRun |= StoB_REQ before BtoS_ACK 585*) 586time 587 EVAL 588 ``UF_SEM 589 (FINITE SimRun) 590 (F_BEFORE(F_BOOL(B_PROP StoB_REQ), F_BOOL(B_PROP BtoS_ACK)))``; 591 592(* 593** SimRun |= BtoS_ACK before StoB_REQ 594*) 595time 596 EVAL 597 ``UF_SEM 598 (FINITE SimRun) 599 (F_BEFORE(F_BOOL(B_PROP BtoS_ACK), F_BOOL(B_PROP StoB_REQ)))``; 600 601(* 602** SimRun |= {[*]}(StoB_REQ before BtoS_ACK) 603*) 604time 605 EVAL 606 ``UF_SEM 607 (FINITE SimRun) 608 (F_SUFFIX_IMP 609 (S_REPEAT S_TRUE, 610 F_BEFORE(F_BOOL(B_PROP StoB_REQ), F_BOOL(B_PROP BtoS_ACK))))``; 611 612(* 613** SimRun |= {[*]}(BtoS_ACK before StoB_REQ) 614*) 615time 616 EVAL 617 ``UF_SEM 618 (FINITE SimRun) 619 (F_SUFFIX_IMP 620 (S_REPEAT S_TRUE, 621 F_BEFORE(F_BOOL(B_PROP BtoS_ACK), F_BOOL(B_PROP StoB_REQ))))``; 622 623 624(****************************************************************************** 625* Make ";;" into an infix for S_CAT 626******************************************************************************) 627val _ = set_fixity ";;" (Infixl 500); 628val S_CAT_IX_def = xDefine "S_CAT_IX" `$;; r1 r2 = S_CAT(r1,r2)`; 629 630(****************************************************************************** 631* SimRun |= {[*];!BtoS_ACK;BtoS_ACK}(F) 632******************************************************************************) 633time 634 EVAL 635 ``UF_SEM 636 (FINITE SimRun) 637 (F_SUFFIX_IMP 638 ((S_REPEAT(S_BOOL B_TRUE) ;; 639 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 640 S_BOOL(B_PROP BtoS_ACK)), 641 F_BOOL B_FALSE))``; 642 643(****************************************************************************** 644* SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[*];!BtoS_ACK;BtoS_ACK}(F) 645******************************************************************************) 646time 647 EVAL 648 ``UF_SEM 649 (FINITE SimRun) 650 (F_SUFFIX_IMP 651 ((S_REPEAT(S_BOOL B_TRUE) ;; 652 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 653 S_BOOL(B_PROP BtoS_ACK) ;; 654 S_REPEAT(S_BOOL B_TRUE) ;; 655 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 656 S_BOOL(B_PROP BtoS_ACK)), 657 F_BOOL B_FALSE))``; 658 659(****************************************************************************** 660* SimRun |= {[*];BtoS_ACK;[RtoB_ACK];BtoS_ACK}(F) 661******************************************************************************) 662time 663 EVAL 664 ``UF_SEM 665 (FINITE SimRun) 666 (F_SUFFIX_IMP 667 ((S_REPEAT(S_BOOL B_TRUE) ;; 668 S_BOOL(B_PROP BtoS_ACK) ;; 669 S_REPEAT(S_BOOL(B_PROP RtoB_ACK)) ;; 670 S_BOOL(B_PROP BtoS_ACK)), 671 F_BOOL B_FALSE))``; 672 673(****************************************************************************** 674* SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[RtoB_ACK];!BtoS_ACK;BtoS_ACK}(F) 675******************************************************************************) 676time 677 EVAL 678 ``UF_SEM 679 (FINITE SimRun) 680 (F_SUFFIX_IMP 681 ((S_REPEAT(S_BOOL B_TRUE) ;; 682 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 683 S_BOOL(B_PROP BtoS_ACK) ;; 684 S_REPEAT(S_BOOL(B_PROP RtoB_ACK)) ;; 685 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 686 S_BOOL(B_PROP BtoS_ACK)), 687 F_BOOL B_FALSE))``; 688 689(****************************************************************************** 690* SimRun |= {[*];BtoS_ACK;[!RtoB_ACK];BtoS_ACK}(F) 691******************************************************************************) 692time 693 EVAL 694 ``UF_SEM 695 (FINITE SimRun) 696 (F_SUFFIX_IMP 697 ((S_REPEAT(S_BOOL B_TRUE) ;; 698 S_BOOL(B_PROP BtoS_ACK) ;; 699 S_REPEAT(S_BOOL(B_NOT(B_PROP RtoB_ACK))) ;; 700 S_BOOL(B_PROP BtoS_ACK)), 701 F_BOOL B_FALSE))``; 702 703(****************************************************************************** 704* SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[!RtoB_ACK];!BtoS_ACK;BtoS_ACK}(F) 705******************************************************************************) 706time 707 EVAL 708 ``UF_SEM 709 (FINITE SimRun) 710 (F_SUFFIX_IMP 711 ((S_REPEAT(S_BOOL B_TRUE) ;; 712 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 713 S_BOOL(B_PROP BtoS_ACK) ;; 714 S_REPEAT(S_BOOL(B_NOT(B_PROP RtoB_ACK))) ;; 715 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 716 S_BOOL(B_PROP BtoS_ACK)), 717 F_BOOL B_FALSE))``; 718 719(****************************************************************************** 720* SimRun 721* |= {[*];!BtoS_ACK;BtoS_ACK;[*];!RtoB_ACK;RtoB_ACK;[*];!BtoS_ACK;BtoS_ACK}(F) 722******************************************************************************) 723time 724 EVAL 725 ``UF_SEM 726 (FINITE SimRun) 727 (F_SUFFIX_IMP 728 ((S_REPEAT(S_BOOL B_TRUE) ;; 729 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 730 S_BOOL(B_PROP BtoS_ACK) ;; 731 S_REPEAT(S_BOOL(B_TRUE)) ;; 732 S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; 733 S_BOOL(B_PROP RtoB_ACK) ;; 734 S_REPEAT(S_BOOL(B_TRUE)) ;; 735 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 736 S_BOOL(B_PROP BtoS_ACK)), 737 F_BOOL B_FALSE))``; 738 739(****************************************************************************** 740* SimRun 741* |= {[*];!BtoS_ACK;BtoS_ACK; 742* [BtoS_ACK];[!BtoS_ACK]; 743* ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK)); 744* [!BtoS_ACK];BtoS_ACK} 745******************************************************************************) 746time 747 EVAL 748 ``US_SEM 749 SimRun 750 ((S_REPEAT(S_BOOL B_TRUE) ;; 751 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 752 S_BOOL(B_PROP BtoS_ACK) ;; 753 S_REPEAT(S_BOOL(B_PROP BtoS_ACK));; 754 S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; 755 S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)), 756 (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;; 757 S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; 758 S_BOOL(B_PROP BtoS_ACK)))``; 759 760(****************************************************************************** 761* SimRun 762* |= {[*];!BtoS_ACK;BtoS_ACK; 763* [BtoS_ACK];[!BtoS_ACK]; 764* ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK)); 765* [!BtoS_ACK];BtoS_ACK} 766* (F) 767******************************************************************************) 768time 769 EVAL 770 ``UF_SEM 771 (FINITE SimRun) 772 (F_SUFFIX_IMP 773 ((S_REPEAT(S_BOOL B_TRUE) ;; 774 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 775 S_BOOL(B_PROP BtoS_ACK) ;; 776 S_REPEAT(S_BOOL(B_PROP BtoS_ACK));; 777 S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; 778 S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)), 779 (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;; 780 S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; 781 S_BOOL(B_PROP BtoS_ACK)), 782 F_BOOL B_FALSE))``; 783 784(****************************************************************************** 785* SimRun 786* |= {[*];!BtoS_ACK;BtoS_ACK; 787* [BtoS_ACK];[!BtoS_ACK]; 788* ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK)); 789* [!BtoS_ACK];BtoS_ACK} 790* (T) 791******************************************************************************) 792time 793 EVAL 794 ``UF_SEM 795 (FINITE SimRun) 796 (F_SUFFIX_IMP 797 ((S_REPEAT(S_BOOL B_TRUE) ;; 798 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 799 S_BOOL(B_PROP BtoS_ACK) ;; 800 S_REPEAT(S_BOOL(B_PROP BtoS_ACK));; 801 S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; 802 S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)), 803 (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;; 804 S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; 805 S_BOOL(B_PROP BtoS_ACK)), 806 F_BOOL B_TRUE))``; 807(****************************************************************************** 808* SimRun 809* |= {[*];!BtoS_ACK; 810* BtoS_ACK; 811* [BtoS_ACK&!RtoB_ACK]; 812* [!BtoS_ACK&!RoB_ACK]; 813* BtoS_ACK} 814* (F) 815******************************************************************************) 816time 817 EVAL 818 ``UF_SEM 819 (FINITE SimRun) 820 (F_SUFFIX_IMP 821 ((S_REPEAT(S_BOOL B_TRUE) ;; 822 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 823 S_BOOL(B_PROP BtoS_ACK) ;; 824 S_REPEAT(S_BOOL(B_AND(B_PROP BtoS_ACK, 825 B_NOT(B_PROP RtoB_ACK)))) ;; 826 S_REPEAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK), 827 B_NOT(B_PROP RtoB_ACK)))) ;; 828 S_BOOL(B_PROP BtoS_ACK)), 829 F_BOOL B_FALSE))``; 830 831(****************************************************************************** 832* SimRun 833* |= {[*]; !BtoS_ACK; BtoS_ACK; true} 834* ((!RtoB_ACK & X RtoB_ACK) before (!BtoS_ACK & X BtoS_ACK)) 835******************************************************************************) 836time 837 EVAL 838 ``UF_SEM 839 (FINITE SimRun) 840 (F_SUFFIX_IMP 841 ((S_REPEAT(S_BOOL B_TRUE) ;; 842 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 843 S_BOOL(B_PROP BtoS_ACK) ;; 844 S_BOOL B_TRUE), 845 F_BEFORE 846 (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), 847 F_NEXT(F_BOOL(B_PROP RtoB_ACK))), 848 F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), 849 F_NEXT(F_BOOL(B_PROP BtoS_ACK))))))``; 850 851(****************************************************************************** 852* SimRun 853* |= {[*]; !RtoB_ACK; RtoB_ACK; true} 854* ((!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK)) 855******************************************************************************) 856time 857 EVAL 858 ``UF_SEM 859 (FINITE SimRun) 860 (F_SUFFIX_IMP 861 ((S_REPEAT(S_BOOL B_TRUE) ;; 862 S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; 863 S_BOOL(B_PROP BtoS_ACK) ;; 864 S_BOOL B_TRUE), 865 F_BEFORE 866 (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), 867 F_NEXT(F_BOOL(B_PROP RtoB_ACK))), 868 F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), 869 F_NEXT(F_BOOL(B_PROP BtoS_ACK))))))``; 870 871 872 873(****************************************************************************** 874* SimRun 875* |= (!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK) 876******************************************************************************) 877time 878 EVAL 879 ``UF_SEM 880 (FINITE SimRun) 881 (F_BEFORE 882 (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), 883 F_NEXT(F_BOOL(B_PROP RtoB_ACK))), 884 F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), 885 F_NEXT(F_BOOL(B_PROP BtoS_ACK)))))``; 886 887(****************************************************************************** 888* Some examples using EVAL to perform clock removing rewriting used in paper 889******************************************************************************) 890time 891 EVAL 892 ``S_CLOCK_COMP c 893 (S_CAT(S_REPEAT S_TRUE, 894 S_CAT(S_AND(S_BOOL(B_NOT(B_PROP rq)), S_BOOL(B_PROP ak)), 895 S_BOOL(B_PROP rq))))``; 896 897 898time 899 EVAL 900 ``S_CLOCK_COMP c1 901 (S_CAT(S_REPEAT S_TRUE, 902 S_CAT(S_AND(S_BOOL(B_NOT(B_PROP rq)), S_CLOCK(S_BOOL(B_PROP ak),B_PROP c2)), 903 S_BOOL(B_PROP rq))))``; 904 905time 906 EVAL 907 ``S_CLOCK_COMP c 908 (S_CAT(S_REPEAT S_TRUE, 909 S_CAT(S_AND(S_CLOCK(S_BOOL(B_NOT(B_PROP rq)),B_PROP c1), 910 S_CLOCK(S_BOOL(B_PROP ak),B_PROP c2)), 911 S_CLOCK(S_BOOL(B_PROP rq), B_PROP c1))))``;; 912 913time 914 (REWRITE_RULE[S_CAT_IX_def] o EVAL) 915 ``F_CLOCK_COMP c 916 (F_SUFFIX_IMP 917 ((S_REPEAT(S_BOOL B_TRUE) ;; 918 S_BOOL(B_NOT(B_PROP ak1)) ;; 919 S_BOOL(B_PROP ak1) ;; 920 S_BOOL B_TRUE), 921 F_BEFORE 922 (F_AND(F_NOT(F_BOOL(B_PROP ak2)), 923 F_NEXT(F_BOOL(B_PROP ak2))), 924 F_AND(F_NOT(F_BOOL(B_PROP ak1)), 925 F_NEXT(F_BOOL(B_PROP ak1))))))``; 926 927(* 928** {[*]; !StoB_REQ & BtoS_ACK; StoB_REQ}(F)@clk1 929*) 930time 931 EVAL 932 ``UF_SEM 933 (FINITE SimRun) 934 (F_CLOCK_COMP 935 (B_PROP clk1) 936 (F_SUFFIX_IMP 937 (S_CAT(S_REPEAT S_TRUE, 938 S_CAT(S_BOOL(B_AND(B_NOT(B_PROP StoB_REQ), B_PROP BtoS_ACK)), 939 S_BOOL(B_PROP StoB_REQ))), 940 F_BOOL B_FALSE)))``; 941 942(* 943** {[*]; !StoB_REQ & BtoS_ACK; StoB_REQ}(F)@(clk1 or clk2 or clk3) 944*) 945time 946 EVAL 947 ``UF_SEM 948 (FINITE SimRun) 949 (F_CLOCK_COMP 950 (BOOL_OR(B_PROP clk1, BOOL_OR(B_PROP clk2, B_PROP clk3))) 951 (F_SUFFIX_IMP 952 (S_CAT(S_REPEAT S_TRUE, 953 S_CAT(S_BOOL(B_AND(B_NOT(B_PROP StoB_REQ), B_PROP BtoS_ACK)), 954 S_BOOL(B_PROP StoB_REQ))), 955 F_BOOL B_FALSE)))``; 956 957 958 959 960 961 962 963