1with Types; use Types; 2with PSL.Types; use PSL.Types; 3with PSL.Errors; use PSL.Errors; 4with PSL.CSE; use PSL.CSE; 5 6package body PSL.Rewrites is 7-- procedure Location_Copy (Dst, Src : Node) is 8-- begin 9-- Set_Location (Dst, Get_Location (Src)); 10-- end Location_Copy; 11 12 -- Return [*0] 13 function Build_Empty return Node is 14 Res, Tmp : Node; 15 begin 16 Res := Create_Node (N_Star_Repeat_Seq); 17 Tmp := Create_Node (N_Number); 18 Set_Value (Tmp, 0); 19 Set_Low_Bound (Res, Tmp); 20 return Res; 21 end Build_Empty; 22 23 -- Return N[*] 24 function Build_Star (N : Node) return Node is 25 Res : Node; 26 begin 27 Res := Create_Node (N_Star_Repeat_Seq); 28 Set_Sequence (Res, N); 29 return Res; 30 end Build_Star; 31 32 -- Return N[+] 33 function Build_Plus (N : Node) return Node is 34 Res : Node; 35 begin 36 Res := Create_Node (N_Plus_Repeat_Seq); 37 Set_Sequence (Res, N); 38 return Res; 39 end Build_Plus; 40 41 -- Return N! 42 function Build_Strong (N : Node) return Node is 43 Res : Node; 44 begin 45 Res := Create_Node (N_Strong); 46 Set_Property (Res, N); 47 return Res; 48 end Build_Strong; 49 50 -- Return T[*] 51 function Build_True_Star return Node is 52 begin 53 return Build_Star (True_Node); 54 end Build_True_Star; 55 56 function Build_Binary (K : Nkind; L, R : Node) return Node is 57 Res : Node; 58 begin 59 Res := Create_Node (K); 60 Set_Left (Res, L); 61 Set_Right (Res, R); 62 return Res; 63 end Build_Binary; 64 65 function Build_Concat (L, R : Node) return Node is 66 begin 67 return Build_Binary (N_Concat_SERE, L, R); 68 end Build_Concat; 69 70 function Build_Repeat (N : Node; Cnt : Uns32) return Node is 71 Res : Node; 72 begin 73 if Cnt = 0 then 74 raise Internal_Error; 75 end if; 76 Res := N; 77 for I in 2 .. Cnt loop 78 Res := Build_Concat (Res, N); 79 end loop; 80 return Res; 81 end Build_Repeat; 82 83 function Build_Overlap_Imp_Seq (S : Node; P : Node) return Node 84 is 85 Res : Node; 86 begin 87 Res := Create_Node (N_Overlap_Imp_Seq); 88 Set_Sequence (Res, S); 89 Set_Property (Res, P); 90 return Res; 91 end Build_Overlap_Imp_Seq; 92 93 function Rewrite_Boolean (N : Node) return Node 94 is 95 Res : Node; 96 begin 97 case Get_Kind (N) is 98 when N_Name => 99 Res := Get_Decl (N); 100 pragma Assert (Res /= Null_Node); 101 return Res; 102 when N_Not_Bool => 103 Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); 104 return N; 105 when N_And_Bool 106 | N_Or_Bool 107 | N_Imp_Bool 108 | N_Equiv_Bool => 109 Set_Left (N, Rewrite_Boolean (Get_Left (N))); 110 Set_Right (N, Rewrite_Boolean (Get_Right (N))); 111 return N; 112 when N_HDL_Expr => 113 return Get_HDL_Hash (N); 114 when N_HDL_Bool => 115 return N; 116 when others => 117 Error_Kind ("rewrite_boolean", N); 118 end case; 119 end Rewrite_Boolean; 120 121 function Rewrite_Star_Repeat_Seq (Seq : Node; 122 Lo, Hi : Uns32) return Node 123 is 124 Res : Node; 125 begin 126 pragma Assert (Lo <= Hi); 127 128 if Lo = Hi then 129 130 if Lo = 0 then 131 -- r[*0] --> [*0] 132 return Build_Empty; 133 elsif Lo = 1 then 134 -- r[*1] --> r 135 return Seq; 136 end if; 137 -- r[*c+] --> r;r;r...;r (c times) 138 return Build_Repeat (Seq, Lo); 139 end if; 140 141 -- r[*0:1] --> [*0] | r 142 -- r[*0:2] --> [*0] | r;{[*0]|r} 143 144 -- r[*0:n] --> [*0] | r;r[*0:n-1] 145 -- r[*l:h] --> r[*l] ; r[*0:h-l] 146 Res := Build_Binary (N_Or_Seq, Build_Empty, Seq); 147 for I in Lo + 2 .. Hi loop 148 Res := Build_Concat (Seq, Res); 149 Res := Build_Binary (N_Or_Seq, Build_Empty, Res); 150 end loop; 151 if Lo > 0 then 152 Res := Build_Concat (Build_Repeat (Seq, Lo), Res); 153 end if; 154 155 return Res; 156 end Rewrite_Star_Repeat_Seq; 157 158 function Rewrite_Star_Repeat_Seq (Seq : Node; 159 Lo, Hi : Node) return Node 160 is 161 Cnt_Lo : Uns32; 162 Cnt_Hi : Uns32; 163 begin 164 if Lo = Null_Node then 165 -- r[*] 166 raise Program_Error; 167 end if; 168 169 Cnt_Lo := Get_Value (Lo); 170 if Hi = Null_Node then 171 Cnt_Hi := Cnt_Lo; 172 else 173 Cnt_Hi := Get_Value (Hi); 174 end if; 175 return Rewrite_Star_Repeat_Seq (Seq, Cnt_Lo, Cnt_Hi); 176 end Rewrite_Star_Repeat_Seq; 177 178 function Rewrite_Star_Repeat_Seq (N : Node) return Node 179 is 180 Seq : constant Node := Get_Sequence (N); 181 Lo : constant Node := Get_Low_Bound (N); 182 begin 183 if Lo = Null_Node then 184 -- r[*] --> r[*] 185 return N; 186 else 187 return Rewrite_Star_Repeat_Seq (Seq, Lo, Get_High_Bound (N)); 188 end if; 189 end Rewrite_Star_Repeat_Seq; 190 191 function Rewrite_Goto_Repeat_Seq (Seq : Node; 192 Lo, Hi : Node) return Node is 193 Res : Node; 194 begin 195 -- b[->] --> {(~b)[*];b} 196 Res := Build_Concat (Build_Star (Build_Bool_Not (Seq)), Seq); 197 198 if Lo = Null_Node then 199 return Res; 200 end if; 201 202 -- b[->l:h] --> {b[->]}[*l:h] 203 return Rewrite_Star_Repeat_Seq (Res, Lo, Hi); 204 end Rewrite_Goto_Repeat_Seq; 205 206 function Rewrite_Goto_Repeat_Seq (Seq : Node; 207 Lo, Hi : Uns32) return Node is 208 Res : Node; 209 begin 210 -- b[->] --> {(~b)[*];b} 211 Res := Build_Concat (Build_Star (Build_Bool_Not (Seq)), Seq); 212 213 -- b[->l:h] --> {b[->]}[*l:h] 214 return Rewrite_Star_Repeat_Seq (Res, Lo, Hi); 215 end Rewrite_Goto_Repeat_Seq; 216 217 function Rewrite_Equal_Repeat_Seq (N : Node) return Node 218 is 219 Seq : constant Node := Get_Sequence (N); 220 Lo : constant Node := Get_Low_Bound (N); 221 Hi : constant Node := Get_High_Bound (N); 222 begin 223 -- b[=l:h] --> {b[->l:h]};(~b)[*] 224 return Build_Concat (Rewrite_Goto_Repeat_Seq (Seq, Lo, Hi), 225 Build_Star (Build_Bool_Not (Seq))); 226 end Rewrite_Equal_Repeat_Seq; 227 228 function Rewrite_Within (N : Node) return Node is 229 Res : Node; 230 begin 231 Res := Build_Concat (Build_Concat (Build_True_Star, Get_Left (N)), 232 Build_True_Star); 233 return Build_Binary (N_Match_And_Seq, Res, Get_Right (N)); 234 end Rewrite_Within; 235 236 function Rewrite_And_Seq (L : Node; R : Node) return Node is 237 begin 238 return Build_Binary (N_Or_Seq, 239 Build_Binary (N_Match_And_Seq, 240 L, 241 Build_Concat (R, Build_True_Star)), 242 Build_Binary (N_Match_And_Seq, 243 Build_Concat (L, Build_True_Star), 244 R)); 245 end Rewrite_And_Seq; 246 pragma Unreferenced (Rewrite_And_Seq); 247 248 procedure Rewrite_Instance (N : Node) 249 is 250 Assoc : Node := Get_Association_Chain (N); 251 begin 252 while Assoc /= Null_Node loop 253 case Get_Kind (Get_Formal (Assoc)) is 254 when N_Const_Parameter => 255 null; 256 when N_Boolean_Parameter => 257 Set_Actual (Assoc, Rewrite_Boolean (Get_Actual (Assoc))); 258 when N_Sequence_Parameter => 259 Set_Actual (Assoc, Rewrite_SERE (Get_Actual (Assoc))); 260 when N_Property_Parameter => 261 Set_Actual (Assoc, Rewrite_Property (Get_Actual (Assoc))); 262 when others => 263 Error_Kind ("rewrite_instance", 264 Get_Formal (Assoc)); 265 end case; 266 Assoc := Get_Chain (Assoc); 267 end loop; 268 end Rewrite_Instance; 269 270 function Rewrite_SERE (N : Node) return Node is 271 S : Node; 272 begin 273 case Get_Kind (N) is 274 when N_Star_Repeat_Seq => 275 S := Get_Sequence (N); 276 if S = Null_Node then 277 S := True_Node; 278 else 279 S := Rewrite_SERE (S); 280 end if; 281 Set_Sequence (N, S); 282 return Rewrite_Star_Repeat_Seq (N); 283 when N_Plus_Repeat_Seq => 284 S := Get_Sequence (N); 285 if S = Null_Node then 286 S := True_Node; 287 else 288 S := Rewrite_SERE (S); 289 end if; 290 Set_Sequence (N, S); 291 return N; 292 when N_Goto_Repeat_Seq => 293 return Rewrite_Goto_Repeat_Seq 294 (Rewrite_SERE (Get_Sequence (N)), 295 Get_Low_Bound (N), Get_High_Bound (N)); 296 when N_Equal_Repeat_Seq => 297 Set_Sequence (N, Rewrite_SERE (Get_Sequence (N))); 298 return Rewrite_Equal_Repeat_Seq (N); 299 when N_Braced_SERE => 300 return Rewrite_SERE (Get_SERE (N)); 301 when N_Clocked_SERE => 302 Set_SERE (N, Rewrite_SERE (Get_SERE (N))); 303 Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); 304 return N; 305 when N_Within_SERE => 306 Set_Left (N, Rewrite_SERE (Get_Left (N))); 307 Set_Right (N, Rewrite_SERE (Get_Right (N))); 308 return Rewrite_Within (N); 309-- when N_And_Seq => 310-- return Rewrite_And_Seq (Rewrite_SERE (Get_Left (N)), 311-- Rewrite_SERE (Get_Right (N))); 312 when N_Concat_SERE 313 | N_Fusion_SERE 314 | N_Match_And_Seq 315 | N_And_Seq 316 | N_Or_Seq => 317 Set_Left (N, Rewrite_SERE (Get_Left (N))); 318 Set_Right (N, Rewrite_SERE (Get_Right (N))); 319 return N; 320 when N_Booleans => 321 return Rewrite_Boolean (N); 322 when N_Name => 323 return Get_Decl (N); 324 when N_Sequence_Instance => 325 Rewrite_Instance (N); 326 return N; 327 when N_Endpoint_Instance => 328 return N; 329 when N_Boolean_Parameter 330 | N_Sequence_Parameter 331 | N_Const_Parameter => 332 return N; 333 when others => 334 Error_Kind ("rewrite_SERE", N); 335 end case; 336 end Rewrite_SERE; 337 338 function Rewrite_Until (N : Node) return Node 339 is 340 Res : Node; 341 B : Node; 342 L : Node; 343 S : Node; 344 begin 345 if Get_Inclusive_Flag (N) then 346 -- B1 until_ B2 --> {B1[+]:B2} 347 Res := Build_Binary (N_Fusion_SERE, 348 Build_Plus (Rewrite_Boolean (Get_Left (N))), 349 Rewrite_Boolean (Get_Right (N))); 350 if Get_Strong_Flag (N) then 351 Res := Build_Strong (Res); 352 end if; 353 else 354 -- P until B --> {(!B)[+]} |-> P 355 B := Rewrite_Boolean (Get_Right (N)); 356 L := Build_Plus (Build_Bool_Not (B)); 357 Res := Build_Overlap_Imp_Seq (L, Rewrite_Property (Get_Left (N))); 358 359 if Get_Strong_Flag (N) then 360 -- p until! b --> (p until b) && ({b[->]}!) 361 S := Build_Strong 362 (Rewrite_Goto_Repeat_Seq (B, Null_Node, Null_Node)); 363 Res := Build_Binary (N_And_Prop, Res, S); 364 end if; 365 end if; 366 return Res; 367 end Rewrite_Until; 368 369 function Rewrite_Next_Event_A (B : Node; 370 Lo, Hi : Uns32; 371 P : Node; 372 Strong : Boolean) return Node 373 is 374 Res : Node; 375 begin 376 Res := Rewrite_Goto_Repeat_Seq (B, Lo, Hi); 377 Res := Build_Overlap_Imp_Seq (Res, P); 378 379 if Strong then 380 Res := Build_Binary 381 (N_And_Prop, 382 Res, 383 Build_Strong (Rewrite_Goto_Repeat_Seq (B, Lo, Lo))); 384 end if; 385 386 return Res; 387 end Rewrite_Next_Event_A; 388 389 function Rewrite_Next_Event (B : Node; 390 N : Uns32; 391 P : Node; 392 Strong : Boolean) return Node is 393 begin 394 return Rewrite_Next_Event_A (B, N, N, P, Strong); 395 end Rewrite_Next_Event; 396 397 function Rewrite_Next_Event (B : Node; 398 Num : Node; 399 P : Node; 400 Strong : Boolean) return Node 401 is 402 N : Uns32; 403 begin 404 if Num = Null_Node then 405 N := 1; 406 else 407 N := Get_Value (Num); 408 end if; 409 return Rewrite_Next_Event (B, N, P, Strong); 410 end Rewrite_Next_Event; 411 412 function Rewrite_Next (Num : Node; P : Node; Strong : Boolean) return Node 413 is 414 N : Uns32; 415 begin 416 if Num = Null_Node then 417 N := 1; 418 else 419 N := Get_Value (Num); 420 end if; 421 return Rewrite_Next_Event (True_Node, N + 1, P, Strong); 422 end Rewrite_Next; 423 424 function Rewrite_Next_A (Lo, Hi : Uns32; 425 P : Node; Strong : Boolean) return Node 426 is 427 begin 428 return Rewrite_Next_Event_A (True_Node, Lo + 1, Hi + 1, P, Strong); 429 end Rewrite_Next_A; 430 431 function Rewrite_Next_Event_E (B1 : Node; 432 Lo, Hi : Uns32; 433 B2 : Node; Strong : Boolean) return Node 434 is 435 Res : Node; 436 begin 437 Res := Build_Binary (N_Fusion_SERE, 438 Rewrite_Goto_Repeat_Seq (B1, Lo, Hi), 439 B2); 440 if Strong then 441 Res := Build_Strong (Res); 442 end if; 443 return Res; 444 end Rewrite_Next_Event_E; 445 446 function Rewrite_Next_E (Lo, Hi : Uns32; 447 B : Node; Strong : Boolean) return Node 448 is 449 begin 450 return Rewrite_Next_Event_E (True_Node, Lo + 1, Hi + 1, B, Strong); 451 end Rewrite_Next_E; 452 453 function Rewrite_Before (N : Node) return Node 454 is 455 Res : Node; 456 R : Node; 457 B1, B2 : Node; 458 N_B2 : Node; 459 begin 460 B1 := Rewrite_Boolean (Get_Left (N)); 461 B2 := Rewrite_Boolean (Get_Right (N)); 462 N_B2 := Build_Bool_Not (B2); 463 Res := Build_Star (Build_Bool_And (Build_Bool_Not (B1), N_B2)); 464 465 if Get_Inclusive_Flag (N) then 466 R := B2; 467 else 468 R := Build_Bool_And (B1, N_B2); 469 end if; 470 Res := Build_Concat (Res, R); 471 if Get_Strong_Flag (N) then 472 Res := Build_Strong (Res); 473 end if; 474 return Res; 475 end Rewrite_Before; 476 477 function Rewrite_Or (L, R : Node) return Node 478 is 479 B, P : Node; 480 begin 481 if Get_Kind (L) in N_Booleans then 482 if Get_Kind (R) in N_Booleans then 483 return Build_Bool_Or (L, R); 484 else 485 B := L; 486 P := R; 487 end if; 488 elsif Get_Kind (R) in N_Booleans then 489 B := R; 490 P := L; 491 else 492 -- Not in the simple subset. 493 raise Program_Error; 494 end if; 495 496 -- B || P --> (~B) -> P 497 return Build_Binary (N_Log_Imp_Prop, Build_Bool_Not (B), P); 498 end Rewrite_Or; 499 500 function Rewrite_Property (N : Node) return Node is 501 begin 502 case Get_Kind (N) is 503 when N_Star_Repeat_Seq 504 | N_Plus_Repeat_Seq 505 | N_Goto_Repeat_Seq 506 | N_Sequence_Instance 507 | N_Endpoint_Instance 508 | N_Braced_SERE 509 | N_And_Seq 510 | N_Or_Seq => 511 return Rewrite_SERE (N); 512 when N_Imp_Seq 513 | N_Overlap_Imp_Seq => 514 Set_Sequence (N, Rewrite_Property (Get_Sequence (N))); 515 Set_Property (N, Rewrite_Property (Get_Property (N))); 516 return N; 517 when N_Log_Imp_Prop => 518 -- b -> p --> {b} |-> p 519 return Build_Overlap_Imp_Seq 520 (Rewrite_Boolean (Get_Left (N)), 521 Rewrite_Property (Get_Right (N))); 522 when N_Eventually => 523 return Build_Strong 524 (Build_Binary (N_Fusion_SERE, 525 Build_Plus (True_Node), 526 Rewrite_SERE (Get_Property (N)))); 527 when N_Until => 528 return Rewrite_Until (N); 529 when N_Next => 530 return Rewrite_Next (Get_Number (N), 531 Rewrite_Property (Get_Property (N)), 532 Get_Strong_Flag (N)); 533 when N_Next_Event => 534 return Rewrite_Next_Event (Rewrite_Boolean (Get_Boolean (N)), 535 Get_Number (N), 536 Rewrite_Property (Get_Property (N)), 537 Get_Strong_Flag (N)); 538 when N_Next_A => 539 return Rewrite_Next_A (Get_Value (Get_Low_Bound (N)), 540 Get_Value (Get_High_Bound (N)), 541 Rewrite_Property (Get_Property (N)), 542 Get_Strong_Flag (N)); 543 when N_Next_Event_A => 544 return Rewrite_Next_Event_A 545 (Rewrite_Boolean (Get_Boolean (N)), 546 Get_Value (Get_Low_Bound (N)), 547 Get_Value (Get_High_Bound (N)), 548 Rewrite_Property (Get_Property (N)), 549 Get_Strong_Flag (N)); 550 when N_Next_E => 551 return Rewrite_Next_E (Get_Value (Get_Low_Bound (N)), 552 Get_Value (Get_High_Bound (N)), 553 Rewrite_Property (Get_Property (N)), 554 Get_Strong_Flag (N)); 555 when N_Next_Event_E => 556 return Rewrite_Next_Event_E 557 (Rewrite_Boolean (Get_Boolean (N)), 558 Get_Value (Get_Low_Bound (N)), 559 Get_Value (Get_High_Bound (N)), 560 Rewrite_Property (Get_Property (N)), 561 Get_Strong_Flag (N)); 562 when N_Before => 563 return Rewrite_Before (N); 564 when N_Booleans => 565 return Rewrite_Boolean (N); 566 when N_Name => 567 return Get_Decl (N); 568 when N_Never 569 | N_Always 570 | N_Strong => 571 -- Fully handled by psl.build 572 Set_Property (N, Rewrite_Property (Get_Property (N))); 573 return N; 574 when N_Clock_Event => 575 Set_Property (N, Rewrite_Property (Get_Property (N))); 576 Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); 577 return N; 578 when N_And_Prop => 579 Set_Left (N, Rewrite_Property (Get_Left (N))); 580 Set_Right (N, Rewrite_Property (Get_Right (N))); 581 return N; 582 when N_Or_Prop => 583 return Rewrite_Or (Rewrite_Property (Get_Left (N)), 584 Rewrite_Property (Get_Right (N))); 585 when N_Abort => 586 Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); 587 Set_Property (N, Rewrite_Property (Get_Property (N))); 588 return N; 589 when N_Property_Instance => 590 Rewrite_Instance (N); 591 return N; 592 when N_Paren_Prop => 593 -- Note: discard it. 594 return Rewrite_Property (Get_Property (N)); 595 when others => 596 Error_Kind ("rewrite_property", N); 597 end case; 598 end Rewrite_Property; 599 600 procedure Rewrite_Unit (N : Node) is 601 Item : Node; 602 begin 603 Item := Get_Item_Chain (N); 604 while Item /= Null_Node loop 605 case Get_Kind (Item) is 606 when N_Name_Decl => 607 null; 608 when N_Assert_Directive => 609 Set_Property (Item, Rewrite_Property (Get_Property (Item))); 610 when N_Property_Declaration => 611 Set_Property (Item, Rewrite_Property (Get_Property (Item))); 612 when others => 613 Error_Kind ("rewrite_unit", Item); 614 end case; 615 Item := Get_Chain (Item); 616 end loop; 617 end Rewrite_Unit; 618end PSL.Rewrites; 619