1 /*------------------------------------------------------------\ 2 | | 3 | This file is part of the Alliance CAD System Copyright | 4 | (C) Laboratoire LIP6 - D�partement ASIM Universite P&M Curie| 5 | | 6 | Home page : http://www-asim.lip6.fr/alliance/ | 7 | E-mail : mailto:alliance-users@asim.lip6.fr | 8 | | 9 | This progam is free software; you can redistribute it | 10 | and/or modify it under the terms of the GNU Library General| 11 | Public License as published by the Free Software Foundation | 12 | either version 2 of the License, or (at your option) any | 13 | later version. | 14 | | 15 | Alliance VLSI CAD System is distributed in the hope that | 16 | it will be useful, but WITHOUT ANY WARRANTY; | 17 | without even the implied warranty of MERCHANTABILITY or | 18 | FITNESS FOR A PARTICULAR PURPOSE. See the GNU General | 19 | Public License for more details. | 20 | | 21 | You should have received a copy of the GNU General Public | 22 | License along with the GNU C Library; see the file COPYING. | 23 | If not, write to the Free Software Foundation, Inc., | 24 | 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. | 25 | | 26 \------------------------------------------------------------*/ 27 /*------------------------------------------------------\ 28 | | 29 | Title : Structures and fonctions for BDD | 30 | | 31 | Date : 19.06.2000 | 32 | | 33 | Author : Jacomme Ludovic | 34 | | 35 \------------------------------------------------------*/ 36 37 # ifndef BDD_105_H 38 # define BDD_105_H 39 40 /*------------------------------------------------------\ 41 | | 42 | Constants | 43 | | 44 \------------------------------------------------------*/ 45 /*------------------------------------------------------\ 46 | | 47 | Hash Oper Constants | 48 | | 49 \------------------------------------------------------*/ 50 51 # define BDD_OPER_RESTRICT ((long)0x00010000) 52 # define BDD_OPER_COMPOSE ((long)0x00020000) 53 # define BDD_OPER_SIMP_DC_ON ((long)0x00040000) 54 # define BDD_OPER_SIMP_DC_OFF ((long)0x00080000) 55 # define BDD_OPER_INTERSECT ((long)0x00100000) 56 # define BDD_OPER_COFACTOR ((long)0x00200000) 57 # define BDD_OPER_SUBSTITUTE ((long)0x00400000) 58 # define BDD_OPER_EXIST ((long)0x00800000) 59 # define BDD_OPER_EXIST_MISS ((long)0x01000000) 60 # define BDD_OPER_REDUCE ((long)0x02000000) 61 # define BDD_OPER_REL_PROD ((long)0x04000000) 62 63 # define BDD_OPER_MASK ((long)0x03FF0000) 64 65 /*------------------------------------------------------\ 66 | | 67 | Bdd Hash Node | 68 | | 69 \------------------------------------------------------*/ 70 71 # define BDD_HASH_NODE_EMPTY ((bddhnode)0) 72 # define BDD_HASH_NODE_DELETED ((bddhnode)1) 73 74 /*------------------------------------------------------\ 75 | | 76 | Bdd Index | 77 | | 78 \------------------------------------------------------*/ 79 80 # define BDD_INDEX_ZERO ((bddindex) 0) 81 # define BDD_INDEX_ONE ((bddindex) 1) 82 # define BDD_INDEX_MIN ((bddindex) 2) 83 84 # define BDD_MAX_INDEX ((bddindex)-1) 85 86 /*------------------------------------------------------\ 87 | | 88 | Bdd Short | 89 | | 90 \------------------------------------------------------*/ 91 92 # define BDD_MAX_SHORT ((bddshort)-1) 93 94 /*------------------------------------------------------\ 95 | | 96 | Bdd Variable | 97 | | 98 \------------------------------------------------------*/ 99 100 # define BDD_MAX_VAR ( ((bddvar)-1) - BDD_INDEX_MIN ) 101 # define BDD_MIN_VAR ((bddvar)-1) 102 103 /*------------------------------------------------------\ 104 | | 105 | Bdd Reference | 106 | | 107 \------------------------------------------------------*/ 108 109 # define BDD_MAX_REF ((bddref)-1) 110 111 /*------------------------------------------------------\ 112 | | 113 | Bdd Flag | 114 | | 115 \------------------------------------------------------*/ 116 117 # define BDD_FLAG_NUM_MASK (bddflag)( 0x0001 ) 118 # define BDD_MAX_FLAG (bddflag)( -1 ) 119 120 /*------------------------------------------------------\ 121 | | 122 | Support Type | 123 | | 124 \------------------------------------------------------*/ 125 126 # define BDD_SUPPORT_CHAIN 0 127 # define BDD_SUPPORT_PTYPE 1 128 129 /*------------------------------------------------------\ 130 | | 131 | Add Input Mode | 132 | | 133 \------------------------------------------------------*/ 134 135 # define BDD_IN_MODE_FIRST 0x00 136 # define BDD_IN_MODE_LAST 0x01 137 # define BDD_IN_MODE_BEFORE 0x02 138 # define BDD_IN_MODE_AFTER 0x03 139 # define BDD_IN_MODE_IMPOSE 0x04 140 141 /*------------------------------------------------------\ 142 | | 143 | Add Auxiliar Mode | 144 | | 145 \------------------------------------------------------*/ 146 147 # define BDD_AUX_MODE_SINGLE 0x00 148 # define BDD_AUX_MODE_GLOBAL 0x01 149 150 /*------------------------------------------------------\ 151 | | 152 | User Function Type | 153 | | 154 \------------------------------------------------------*/ 155 156 # define BDD_FUNC_RESET_HASH_OPER 0 157 158 /*------------------------------------------------------\ 159 | | 160 | Bdd System Flags | 161 | | 162 \------------------------------------------------------*/ 163 164 # define BDD_SYSTEM_REORDER_ON_MASK 0x0001 165 # define BDD_SYSTEM_REORDER_MASK 0x0002 166 # define BDD_SYSTEM_EXPLOSION_ON_MASK 0x0004 167 # define BDD_SYSTEM_EXPLOSION_MASK 0x0008 168 # define BDD_SYSTEM_SWAP_VAR_MASK 0x0010 169 # define BDD_SYSTEM_NO_WARNING_MASK 0x0020 170 171 /*------------------------------------------------------\ 172 | | 173 | Macros | 174 | | 175 \------------------------------------------------------*/ 176 177 #ifndef __P 178 # if defined(__STDC__) || defined(__GNUC__) 179 # define __P(x) x 180 # else 181 # define __P(x) () 182 # endif 183 #endif 184 185 /*------------------------------------------------------\ 186 | | 187 | Bdd System Mask | 188 | | 189 \------------------------------------------------------*/ 190 191 # define SetBddSystemReorderOn( S ) ( (S)->FLAGS |= BDD_SYSTEM_REORDER_ON_MASK ) 192 # define IsBddSystemReorderOn( S ) ( (S)->FLAGS & BDD_SYSTEM_REORDER_ON_MASK ) 193 # define ClearBddSystemReorderOn( S ) ( (S)->FLAGS &= ~BDD_SYSTEM_REORDER_ON_MASK) 194 195 # define SetBddSystemReorder( S ) ( (S)->FLAGS |= BDD_SYSTEM_REORDER_MASK ) 196 # define IsBddSystemReorder( S ) ( (S)->FLAGS & BDD_SYSTEM_REORDER_MASK ) 197 # define ClearBddSystemReorder( S ) ( (S)->FLAGS &= ~BDD_SYSTEM_REORDER_MASK) 198 199 # define SetBddSystemExplosionOn( S ) ( (S)->FLAGS |= BDD_SYSTEM_EXPLOSION_ON_MASK ) 200 # define IsBddSystemExplosionOn( S ) ( (S)->FLAGS & BDD_SYSTEM_EXPLOSION_ON_MASK ) 201 # define ClearBddSystemExplosionOn( S ) ( (S)->FLAGS &= ~BDD_SYSTEM_EXPLOSION_ON_MASK) 202 203 # define SetBddSystemExplosion( S ) ( (S)->FLAGS |= BDD_SYSTEM_EXPLOSION_MASK ) 204 # define IsBddSystemExplosion( S ) ( (S)->FLAGS & BDD_SYSTEM_EXPLOSION_MASK ) 205 # define ClearBddSystemExplosion( S ) ((S)->FLAGS &= ~BDD_SYSTEM_EXPLOSION_MASK) 206 207 # define SetBddSystemSwapVar( S ) ( (S)->FLAGS |= BDD_SYSTEM_SWAP_VAR_MASK ) 208 # define IsBddSystemSwapVar( S ) ( (S)->FLAGS & BDD_SYSTEM_SWAP_VAR_MASK ) 209 # define ClearBddSystemSwapVar( S ) ( (S)->FLAGS &= ~BDD_SYSTEM_SWAP_VAR_MASK) 210 211 # define SetBddSystemNoWarning( S ) ( (S)->FLAGS |= BDD_SYSTEM_NO_WARNING_MASK ) 212 # define IsBddSystemNoWarning( S ) ( (S)->FLAGS & BDD_SYSTEM_NO_WARNING_MASK ) 213 # define ClearBddSystemNoWarning( S ) ( (S)->FLAGS &= ~BDD_SYSTEM_NO_WARNING_MASK) 214 215 /*------------------------------------------------------\ 216 | | 217 | Bdd Local System | 218 | | 219 \------------------------------------------------------*/ 220 221 # define setbddlocalsystem( S ) \ 222 \ 223 do { if ( (S) ) BddLocalSystem = (S); } while (0) 224 225 /*------------------------------------------------------\ 226 | | 227 | Bdd Local Circuit | 228 | | 229 \------------------------------------------------------*/ 230 231 # define setbddlocalcircuit( C ) \ 232 \ 233 do { if ( (C) ) { BddLocalCircuit = (C); \ 234 BddLocalSystem = (C)->BDD_SYSTEM; } } while (0) 235 236 /*------------------------------------------------------\ 237 | | 238 | Bdd Support | 239 | | 240 \------------------------------------------------------*/ 241 242 # define getbddnodesupportchain( S, N ) \ 243 \ 244 ((chain_list *)getbddnodesupport( (S), (N), BDD_SUPPORT_CHAIN )) 245 246 # define getbddnodesupportptype( S, N ) \ 247 \ 248 ((ptype_list *)getbddnodesupport( (S), (N), BDD_SUPPORT_PTYPE )) 249 250 /*------------------------------------------------------\ 251 | | 252 | Type | 253 | | 254 \------------------------------------------------------*/ 255 /*------------------------------------------------------\ 256 | | 257 | Index Ref Mark and Var | 258 | | 259 \------------------------------------------------------*/ 260 261 typedef unsigned short bddindex; 262 typedef unsigned short bddref; 263 typedef unsigned char bddmark; 264 typedef unsigned char bddflag; 265 typedef unsigned short bddvar; 266 typedef unsigned short bddshort; 267 268 /*------------------------------------------------------\ 269 | | 270 | Bdd Alloc Info | 271 | | 272 \------------------------------------------------------*/ 273 274 typedef struct bddallocinfo 275 { 276 long CIRCUIT; 277 long SYSTEM; 278 long BLOCK; 279 long NODE_BLOCK; 280 long HASH_NODE_TABLE; 281 long HASH_NODE; 282 long HASH_OPER_TABLE; 283 long HASH_OPER; 284 long VAR_TREE; 285 long VAR_CHILD; 286 long VAR; 287 long VAR_NODE; 288 long INDEX_NODE; 289 long INDEX; 290 long ASSOC; 291 long ASSOC_NODE; 292 long NAME_IN; 293 long INDEX_IN; 294 long HEATH; 295 long USER_FUNC; 296 297 } bddallocinfo; 298 299 /*------------------------------------------------------\ 300 | | 301 | Bdd User Function | 302 | | 303 \------------------------------------------------------*/ 304 305 typedef struct bdduserfunc 306 { 307 struct bdduserfunc *NEXT; 308 void (*FUNC)(); 309 void *DATA; 310 long TYPE; 311 312 } bdduserfunc; 313 314 /*------------------------------------------------------\ 315 | | 316 | Bdd Node | 317 | | 318 \------------------------------------------------------*/ 319 320 typedef struct bddnode 321 { 322 struct bddnode *HIGH; 323 struct bddnode *LOW; 324 bddindex INDEX; 325 bddmark MARK; 326 bddflag FLAG; 327 bddref REF_EXT; 328 bddref REF_INT; 329 330 } bddnode; 331 332 /*------------------------------------------------------\ 333 | | 334 | Bdd Hash Node | 335 | | 336 \------------------------------------------------------*/ 337 338 typedef bddnode *bddhnode; 339 340 /*------------------------------------------------------\ 341 | | 342 | Bdd Block | 343 | | 344 \------------------------------------------------------*/ 345 346 typedef struct bddblock 347 { 348 struct bddblock *NEXT; 349 struct bddnode *NODE; 350 long NODE_FREE; 351 352 } bddblock; 353 354 /*------------------------------------------------------\ 355 | | 356 | Bdd Hash Node Table | 357 | | 358 \------------------------------------------------------*/ 359 360 typedef struct bddhnodetable 361 { 362 bddhnode *TABLE; 363 long TABLE_SIZE; 364 long NUMBER_NODE; 365 long NUMBER_ADD; 366 long NUMBER_SCAN; 367 long NUMBER_STRETCH; 368 long NUMBER_RESIZE; 369 370 } bddhnodetable; 371 372 /*------------------------------------------------------\ 373 | | 374 | Bdd Hash Oper | 375 | | 376 \------------------------------------------------------*/ 377 378 typedef struct bddhoper 379 { 380 bddnode *LEFT; 381 bddnode *RIGHT; 382 bddnode *FATHER; 383 long OPERATOR; 384 385 } bddhoper; 386 387 /*------------------------------------------------------\ 388 | | 389 | Bdd Hash Oper Table | 390 | | 391 \------------------------------------------------------*/ 392 393 typedef struct bddhopertable 394 { 395 bddhoper *TABLE; 396 long TABLE_SIZE; 397 long TABLE_FREEZE; 398 long NUMBER_OPER; 399 long NUMBER_ADD; 400 long NUMBER_HIT; 401 long NUMBER_MISS; 402 long NUMBER_RESET; 403 404 } bddhopertable; 405 406 /*------------------------------------------------------\ 407 | | 408 | Bdd Variable Node | 409 | | 410 \------------------------------------------------------*/ 411 412 typedef bddnode *bddvarnode; 413 414 /*------------------------------------------------------\ 415 | | 416 | Bdd Index Node | 417 | | 418 \------------------------------------------------------*/ 419 420 typedef bddhnodetable *bddindexnode; 421 422 /*------------------------------------------------------\ 423 | | 424 | Bdd Assoc Node | 425 | | 426 \------------------------------------------------------*/ 427 428 typedef bddnode *bddassocnode; 429 430 /*------------------------------------------------------\ 431 | | 432 | Bdd Assoc | 433 | | 434 \------------------------------------------------------*/ 435 436 typedef struct bddassoc 437 { 438 struct bddassoc *NEXT; 439 bddassocnode *ASSOC_NODE; 440 bddvar FIRST; 441 bddvar LAST; 442 bddshort IDENT; 443 bddshort CACHE; 444 445 } bddassoc; 446 447 /*------------------------------------------------------\ 448 | | 449 | Bdd System | 450 | | 451 \------------------------------------------------------*/ 452 453 typedef struct bddsystem 454 { 455 bddblock *BLOCK; 456 bddnode *NODE_FREE; 457 long NUMBER_FREE; 458 459 bddindexnode *INDEX_NODE; 460 bddvarnode *VAR_NODE; 461 bddindex *VAR_TO_INDEX; 462 bddvar *INDEX_TO_VAR; 463 464 465 long NUMBER_NODE; 466 long MAX_NODE; 467 long TOP_NODE; 468 469 long NUMBER_VAR; 470 long MAX_VAR; 471 472 long NUMBER_INDEX; 473 long MAX_INDEX; 474 475 bddassoc *ASSOC; 476 unsigned char ASSOC_RESET; 477 478 bddhopertable *HASH_OPER; 479 480 bddnode *ONE; 481 bddnode *ZERO; 482 483 bddmark MARK; 484 long FLAGS; 485 486 void (*REORDER_FUNC)(); 487 long REORDER_LOW; 488 long REORDER_LIMIT; 489 long REORDER_RATIO; 490 491 bdduserfunc *USER_FUNC; 492 493 long VAR_MODEL; 494 long OPER_MODEL; 495 496 void (*EXPLOSION_FUNC)(); 497 long EXPLOSION_LIMIT; 498 499 } bddsystem; 500 501 /*------------------------------------------------------\ 502 | | 503 | Bdd Name Input | 504 | | 505 \------------------------------------------------------*/ 506 507 typedef char *bddnamein; 508 509 /*------------------------------------------------------\ 510 | | 511 | Bdd Circuit | 512 | | 513 \------------------------------------------------------*/ 514 515 typedef struct bddcircuit 516 { 517 char *NAME; 518 519 authtable *HASH_IN; 520 authtable *HASH_OUT; 521 522 bddnamein *NAME_IN; 523 long NAME_IN_SIZE; 524 525 bddindex *INDEX_IN; 526 long INDEX_IN_SIZE; 527 528 long NUMBER_NAME_IN; 529 long NUMBER_NAME_OUT; 530 531 bddsystem *BDD_SYSTEM; 532 533 } bddcircuit; 534 535 /*------------------------------------------------------\ 536 | | 537 | Bdd Heath | 538 | | 539 \------------------------------------------------------*/ 540 541 typedef struct bddheath 542 { 543 struct bddheath *NEXT; 544 struct bddnode *VAR; 545 struct bddnode *MINUS; 546 struct bddnode *PLUS; 547 548 } bddheath; 549 550 /*------------------------------------------------------\ 551 | | 552 | Global Variables | 553 | | 554 \------------------------------------------------------*/ 555 556 extern long BDD_HNODE_STRETCH_FACTOR; 557 extern long BDD_HNODE_RESIZE_FACTOR; 558 extern long BDD_HNODE_MIN_FILL_FACTOR; 559 extern long BDD_HNODE_MAX_SCAN; 560 561 extern bddsystem *BddLocalSystem; 562 extern bddcircuit *BddLocalCircuit; 563 extern bddallocinfo BddAllocInfo; 564 565 /*------------------------------------------------------\ 566 | | 567 | Functions | 568 | | 569 \------------------------------------------------------*/ 570 /*------------------------------------------------------\ 571 | | 572 | Env Functions | 573 | | 574 \------------------------------------------------------*/ 575 576 extern void bddenv __P(()); 577 578 /*------------------------------------------------------\ 579 | | 580 | Alloc Functions | 581 | | 582 \------------------------------------------------------*/ 583 584 extern bddcircuit * allocbddcircuit __P(()); 585 extern bddsystem * allocbddsystem __P(()); 586 587 extern bddblock * allocbddblock __P(()); 588 extern bddnode * allocbddnodeblock __P((long Number)); 589 extern bddhnodetable * allocbddhnodetable __P(()); 590 extern bddhnode * allocbddhnode __P((long Number)); 591 extern bddhopertable * allocbddhopertable __P(()); 592 extern bddhoper * allocbddhoper __P((long Number)); 593 594 extern bddvar * allocbddvar __P((long Number)); 595 extern bddvarnode * allocbddvarnode __P((long Number)); 596 extern bddindexnode * allocbddindexnode __P((long Number)); 597 extern bddindex * allocbddindex __P((long Number)); 598 extern bddnamein * allocbddnamein __P((long Number)); 599 extern bddindex * allocbddindexin __P((long Number)); 600 601 extern bddassoc * allocbddassoc __P(()); 602 extern bddassocnode * allocbddassocnode __P((long Number)); 603 604 extern bddheath * allocbddheath __P(()); 605 extern bdduserfunc * allocbdduserfunc __P(()); 606 607 extern void viewbddallocinfo __P(()); 608 609 /*------------------------------------------------------\ 610 | | 611 | Resize Functions | 612 | | 613 \------------------------------------------------------*/ 614 615 extern bddvar * resizebddvar __P((bddvar *BddVar, long OldNum, long NewNum)); 616 extern bddvarnode * resizebddvarnode __P((bddvarnode *BddVarNode, long OldNum, long NewNum)); 617 extern bddindexnode * resizebddindexnode __P((bddindexnode *BddIndexNode, long OldNum, long NewNum)); 618 extern bddindex * resizebddindex __P((bddindex *BddIndex, long OldNum, long NewNum)); 619 extern bddassocnode * resizebddassocnode __P((bddassocnode *BddAssocNode, long OldNum, long NewNum)); 620 extern bddnamein * resizebddnamein __P((bddnamein *NameIn, long OldNum, long NewNum)); 621 extern bddindex * resizebddindexin __P((bddindex *IndexIn, long OldNum, long NewNum)); 622 623 /*------------------------------------------------------\ 624 | | 625 | Free Functions | 626 | | 627 \------------------------------------------------------*/ 628 629 extern void freebddcircuit __P((bddcircuit *BddCircuit)); 630 extern void freebddsystem __P((bddsystem *BddSystem)); 631 extern void freebddblock __P((bddblock *BddBlock)); 632 extern void freebddnodeblock __P((bddnode *BddNode)); 633 extern void freebddhnodetable __P((bddhnodetable *HashTable)); 634 extern void freebddhnode __P((bddhnode *HashNode)); 635 extern void freebddhopertable __P((bddhopertable *HashTable)); 636 extern void freebddhoper __P((bddhoper *HashOper)); 637 extern void freebddvar __P((bddvar *BddVariable)); 638 extern void freebddvarnode __P((bddvarnode *BddVariableNode)); 639 extern void freebddindex __P((bddindex *BddIndex)); 640 extern void freebddindexnode __P((bddindexnode *BddIndexNode)); 641 extern void freebddnamein __P((bddnamein *NameIn)); 642 extern void freebddindexin __P((bddindex *IndexIn)); 643 extern void freebddassoc __P((bddassoc *BddAssoc)); 644 extern void freebddassocnode __P((bddassocnode *BddAssocNode)); 645 extern void freebddheath __P((bddheath *BddHeath)); 646 extern void freebdduserfunc __P((bdduserfunc *BddUserFunc)); 647 648 /*------------------------------------------------------\ 649 | | 650 | Circuit Functions | 651 | | 652 \------------------------------------------------------*/ 653 654 extern bddcircuit * createbddcircuit __P((char *Name, long NumberIn, long NumberOut, bddsystem *BddSystem)); 655 extern void resetbddcircuit __P((bddcircuit *BddCircuit)); 656 extern void destroybddcircuit __P((bddcircuit *BddCircuit)); 657 extern void viewbddcircuit __P((bddcircuit *BddCircuit, char ViewName)); 658 659 extern bddnode * searchbddcircuitin __P((bddcircuit *BddCircuit, char *InputName)); 660 extern bddnode * addbddcircuitin __P((bddcircuit *BddCircuit, char *InputName, bddindex Index, long Mode)); 661 extern char * getbddcircuitinname __P((bddcircuit *BddCircuit, bddindex Index )); 662 extern bddnode * addbddcircuitaux __P((bddcircuit *BddCircuit, char *InputName, bddnode *BddAux, int (*UserFunc)(), long Mode)); 663 extern bddnode * renamebddcircuitin __P((bddcircuit *BddCircuit, char *InputName, char *NewName)); 664 665 extern bddnode * searchbddcircuitout __P((bddcircuit *BddCircuit, char *OutputName)); 666 extern bddnode * addbddcircuitout __P((bddcircuit *BddCircuit, char *OutputName, bddnode *BddNode)); 667 extern int delbddcircuitout __P((bddcircuit *BddCircuit, char *OutputName)); 668 669 extern bddnode * addbddcircuitabl __P((bddcircuit *BddCircuit, ablexpr *Expr)); 670 extern ablexpr * convertbddcircuitabl __P((bddcircuit *BddCircuit, bddnode *BddNode)); 671 extern ablexpr * convertbddcircuitsumabl __P((bddcircuit *BddCircuit, bddnode *BddNode)); 672 673 extern long getbddcircuitnumnode __P(( bddcircuit *BddCircuit )); 674 extern long getbddcircuitsize __P(( bddcircuit *BddCircuit )); 675 extern void optimizebddcircuit __P(( bddcircuit *BddCircuit, long (*CostFunc)(), float MaxSizeFactor )); 676 677 /*------------------------------------------------------\ 678 | | 679 | System Functions | 680 | | 681 \------------------------------------------------------*/ 682 683 extern bddsystem * createbddsystem __P((long ModelVar, long ModelOper, long MaxVar, long MaxNode)); 684 extern void resetbddsystem __P((bddsystem *BddSystem)); 685 extern void destroybddsystem __P((bddsystem *BddSystem)); 686 extern void viewbddsystem __P((bddsystem *BddSystem, char ViewIndex)); 687 extern void viewbddsysteminfo __P((bddsystem *BddSystem)); 688 689 /*------------------------------------------------------\ 690 | | 691 | Block Functions | 692 | | 693 \------------------------------------------------------*/ 694 695 extern bddblock * createbddblock __P((bddsystem *BddSystem)); 696 extern void resetbddblock __P((bddsystem *BddSystem)); 697 extern void destroybddblock __P((bddsystem *BddSystem)); 698 extern void viewbddblock __P((bddsystem *BddSystem, void (*FuncView)())); 699 700 extern bddblock * addbddblock __P((bddsystem *BddSystem)); 701 702 /*------------------------------------------------------\ 703 | | 704 | User Functions | 705 | | 706 \------------------------------------------------------*/ 707 708 extern bdduserfunc * addbdduserfunc __P((bddsystem *BddSystem, long Type, void (*Func)(), void *Data)); 709 extern void execbdduserfunc __P((bddsystem *BddSystem, long Type)); 710 extern int delbdduserfunc __P((bddsystem *BddSystem, bdduserfunc *BddUserFunc)); 711 extern void destroybdduserfunc __P((bddsystem *BddSystem)); 712 713 /*------------------------------------------------------\ 714 | | 715 | Variable Functions | 716 | | 717 \------------------------------------------------------*/ 718 719 extern bddindex newbddvar __P((bddsystem *BddSystem, bddvar Variable)); 720 extern bddnode * addbddvar __P((bddsystem *BddSystem, bddvar Variable)); 721 extern bddnode * addbddvarfirst __P((bddsystem *BddSystem)); 722 extern bddnode * addbddvarlast __P((bddsystem *BddSystem)); 723 extern bddnode * addbddvarbefore __P((bddsystem *BddSystem, bddindex Index)); 724 extern bddnode * addbddvarafter __P((bddsystem *BddSystem, bddindex Index)); 725 726 extern int swapbddvar __P((bddsystem *BddSystem, bddvar Variable)); 727 extern void sweepbddvar __P((bddsystem *BddSystem, bddvar Variable, int SweepRef)); 728 729 extern bddindex getbddvarindex __P((bddsystem *BddSystem, bddvar Variable)); 730 extern bddvar getbddvarbyindex __P((bddsystem *BddSystem, bddindex Index)); 731 extern bddnode * getbddvarnode __P((bddsystem *BddSystem, bddvar Variable)); 732 extern bddnode * getbddvarnodebyindex __P((bddsystem *BddSystem, bddindex Index)); 733 734 /*------------------------------------------------------\ 735 | | 736 | Auxiliary Variable Functions | 737 | | 738 \------------------------------------------------------*/ 739 740 extern bddnode * addbddvarauxsingle __P((bddsystem *BddSystem, bddnode *BddAux)); 741 extern bddnode * addbddvarauxglobal __P((bddsystem *BddSystem, bddnode *BddAux, int (*UserFunc)())); 742 extern bddnode *addbddvarauxuser(); 743 744 /*------------------------------------------------------\ 745 | | 746 | Node Functions | 747 | | 748 \------------------------------------------------------*/ 749 750 extern bddnode * addbddnode __P((bddsystem *BddSystem, bddindex Index, bddnode *High, bddnode *Low)); 751 extern void delbddnode __P((bddsystem *BddSystem, bddnode *BddNode)); 752 extern void viewbddnode __P((bddsystem *BddSystem, bddnode *BddNode)); 753 754 extern chain_list * addbddnodelist __P((bddsystem *BddSystem, chain_list *HeadList, bddnode *BddNode)); 755 extern void delbddnodelist __P((bddsystem *BddSystem, chain_list *HeadList)); 756 757 /*------------------------------------------------------\ 758 | | 759 | Reference Functions | 760 | | 761 \------------------------------------------------------*/ 762 763 extern bddnode * incbddrefext __P((bddnode *BddNode)); 764 extern bddnode * decbddrefext __P((bddnode *BddNode)); 765 extern bddnode * incbddrefint __P((bddnode *BddNode)); 766 extern bddnode * decbddrefint __P((bddnode *BddNode)); 767 768 extern bddnode * setbddrefext __P((bddnode *BddNode)); 769 extern bddnode * unsetbddrefext __P((bddnode *BddNode)); 770 771 extern void updatebddref __P((bddnode *BddNode)); 772 773 extern void clearbddsystemrefext __P((bddsystem *BddSystem)); 774 extern void clearbddsystemrefint __P((bddsystem *BddSystem)); 775 extern void clearbddsystemref __P((bddsystem *BddSystem)); 776 777 /*------------------------------------------------------\ 778 | | 779 | Association Functions | 780 | | 781 \------------------------------------------------------*/ 782 783 extern bddassoc * addbddassoc __P((bddsystem *BddSystem)); 784 extern int delbddassoc __P((bddsystem *BddSystem, bddassoc *BddAssoc)); 785 extern void viewbddassoc __P((bddsystem *BddSystem, bddassoc *BddAssoc, void (*FuncView)())); 786 787 extern void resetbddassoc __P((bddsystem *BddSystem, bddassoc *BddAssoc)); 788 extern void destroybddassoc __P((bddsystem *BddSystem)); 789 790 extern bddassoc * addbddnodeassoc __P((bddsystem *BddSystem, bddassoc *BddAssoc, bddvar Variable, bddnode *BddNode)); 791 extern int delbddnodeassoc __P((bddsystem *BddSystem, bddassoc *BddAssoc, bddvar Variable)); 792 793 /*------------------------------------------------------\ 794 | | 795 | Mark Functions | 796 | | 797 \------------------------------------------------------*/ 798 799 extern void newbddsystemmark __P(( bddsystem *BddSystem )); 800 extern void setbddnodemark __P(( bddsystem *BddSystem, bddnode *BddNode )); 801 extern int testbddnodemark __P(( bddsystem *BddSystem, bddnode *BddNode )); 802 803 extern long getbddnodenum __P((bddsystem *BddSystem, bddnode *BddNode)); 804 extern long getbddnodesize __P((bddsystem *BddSystem, bddnode *BddNode)); 805 806 /*------------------------------------------------------\ 807 | | 808 | Flag Functions | 809 | | 810 \------------------------------------------------------*/ 811 812 extern long flagbddnode __P((bddsystem *BddSystem, bddnode *BddNode, bddflag Flag)); 813 extern long unflagbddnode __P((bddsystem *BddSystem, bddnode *BddNode, bddflag Flag)); 814 815 /*------------------------------------------------------\ 816 | | 817 | Check Functions | 818 | | 819 \------------------------------------------------------*/ 820 821 extern int checkbddindex __P((bddsystem *BddSystem, bddindex Index, int Severity)); 822 extern int checkbddvar __P((bddsystem *BddSystem, bddvar Variable, int Severity)); 823 extern int checkbddoper __P((bddsystem *BddSystem, long Oper, int Severity)); 824 extern int checkbddassoc __P((bddsystem *BddSystem, bddassoc *BddAssoc, int Severity)); 825 extern int checkbddmaxnode __P((bddsystem *BddSystem, int Severity)); 826 827 /*------------------------------------------------------\ 828 | | 829 | Get Hash Functions | 830 | | 831 \------------------------------------------------------*/ 832 833 extern long getbddhnodesize __P((long Size)); 834 extern long getbddhnodekey __P((bddhnodetable *Table, bddnode *BddNode)); 835 extern long getbddhnodeindex __P((bddhnodetable *Table, bddnode *BddNode, long Index)); 836 837 extern long getbddhopersize __P((long Size)); 838 extern long getbddhoperkey __P((bddhopertable *Table, long Oper, bddnode *BddLeft, bddnode *BddRight)); 839 840 /*------------------------------------------------------\ 841 | | 842 | Check Hash Functions | 843 | | 844 \------------------------------------------------------*/ 845 846 extern int checkbddhnode __P((bddnode *HashNode, int Severity)); 847 848 /*------------------------------------------------------\ 849 | | 850 | Set Hash Functions | 851 | | 852 \------------------------------------------------------*/ 853 854 extern void setbddhnodefunc __P((long (*FuncSize)(), long (*FuncKey)(), long (*FuncIndex)())); 855 extern void setbddhoperfunc __P((long (*FuncSize)(), long (*FuncKey)())); 856 857 /*------------------------------------------------------\ 858 | | 859 | Hash Table Functions | 860 | | 861 \------------------------------------------------------*/ 862 863 extern bddhnodetable * createbddhnodetable __P((long Length)); 864 extern void stretchbddhnodetable __P((bddhnodetable *HashTable)); 865 extern void destroybddhnodetable __P((bddhnodetable *HashTable)); 866 extern void resetbddhnodetable __P((bddhnodetable *HashTable)); 867 extern void viewbddhnodetable __P((bddhnodetable *HashTable, void (*FuncView)())); 868 869 extern bddhopertable * createbddhopertable __P((long Length)); 870 extern void destroybddhopertable __P((bddhopertable *HashTable)); 871 extern void resetbddhopertable __P((bddhopertable *HashTable)); 872 extern void viewbddhopertable __P((bddhopertable *HashTable, void (*FuncView)())); 873 874 /*------------------------------------------------------\ 875 | | 876 | Hash Node Functions | 877 | | 878 \------------------------------------------------------*/ 879 880 extern bddnode * addbddhnode __P((bddhnodetable *HashTable, bddnode *BddNode)); 881 extern int delbddhnode __P((bddhnodetable *HashTable, bddnode *BddNode)); 882 extern void viewbddhnode __P((bddnode *HashNode)); 883 884 /*------------------------------------------------------\ 885 | | 886 | Hash Oper Functions | 887 | | 888 \------------------------------------------------------*/ 889 890 extern bddhoper * addbddhoper __P((bddhopertable *HashTable, long Oper, bddnode *BddLeft, bddnode *BddRight, bddnode *BddFather)); 891 extern bddhoper * searchbddhoper __P((bddhopertable *HashTable, long Oper, bddnode *BddLeft, bddnode *BddRight)); 892 extern void viewbddhoper __P((bddhoper *HashOper)); 893 894 /*------------------------------------------------------\ 895 | | 896 | View Index and Variable Nodes | 897 | | 898 \------------------------------------------------------*/ 899 900 extern void viewbddindexnode __P((bddsystem *BddSystem, void (*FuncView)())); 901 extern void viewbddvarnode __P((bddsystem *BddSystem, void (*FuncView)())); 902 903 /*------------------------------------------------------\ 904 | | 905 | Apply Functions | 906 | | 907 \------------------------------------------------------*/ 908 909 extern bddnode * applybddnode __P((bddsystem *BddSystem, long Oper, bddnode *BddNode1, bddnode *BddNode2)); 910 extern bddnode * applybddnodenot __P((bddsystem *BddSystem, bddnode *BddNode)); 911 extern bddnode * applybddnodeite __P((bddsystem *BddSystem, bddnode *BddIf, bddnode *BddThen, bddnode *BddElse)); 912 extern bddnode * applybddnodeterm __P((bddsystem *BddSystem, long Oper, bddindex Index, bddnode *BddNode)); 913 extern bddnode * applybddnodelist __P((bddsystem *BddSystem, long Oper, chain_list *BddList)); 914 915 /*------------------------------------------------------\ 916 | | 917 | Support Functions | 918 | | 919 \------------------------------------------------------*/ 920 921 extern void * getbddnodesupport __P((bddsystem *BddSystem, bddnode *BddNode, int Mode)); 922 extern int isbddvarinsupport __P((bddsystem *BddSystem, bddnode *BddNode, bddvar Variable)); 923 924 /*------------------------------------------------------\ 925 | | 926 | Compose Functions | 927 | | 928 \------------------------------------------------------*/ 929 930 extern bddnode * restrictbddnode __P((bddsystem *BddSystem, bddnode *BddNode, bddvar Variable, bddnode *BddSubst)); 931 extern bddnode * composebddnode __P((bddsystem *BddSystem, bddnode *BddNode, bddvar Variable, bddnode *BddSubst)); 932 933 /*------------------------------------------------------\ 934 | | 935 | Substitute Functions | 936 | | 937 \------------------------------------------------------*/ 938 939 extern bddnode * substbddnodeassoc __P((bddsystem *BddSystem, bddnode *BddNode, bddassoc *BddAssoc)); 940 941 /*------------------------------------------------------\ 942 | | 943 | Existential Quantification Functions | 944 | | 945 \------------------------------------------------------*/ 946 947 extern bddnode *forallbddnodeassoc __P((bddsystem *BddSystem, bddnode *BddNode, bddassoc *BddAssoc)); 948 extern bddnode *forallbddnodemissassoc __P((bddsystem *BddSystem, bddnode *BddNode, bddassoc *BddAssoc)); 949 extern bddnode *existbddnodeassoc __P((bddsystem *BddSystem, bddnode *BddNode, bddassoc *BddAssoc)); 950 extern bddnode *existbddnodemissassoc __P((bddsystem *BddSystem, bddnode *BddNode, bddassoc *BddAssoc)); 951 952 /*------------------------------------------------------\ 953 | | 954 | Relational Product Functions | 955 | | 956 \------------------------------------------------------*/ 957 958 extern bddnode *relprodbddnodeassoc __P((bddsystem *BddSystem, bddnode *BddNode1, bddnode *BddNode2, bddassoc *BddAssoc)); 959 960 /*------------------------------------------------------\ 961 | | 962 | Intersect & Imply Functions | 963 | | 964 \------------------------------------------------------*/ 965 966 extern bddnode * implybddnode __P((bddsystem *BddSystem, bddnode *BddNode1, bddnode *BddNode2)); 967 extern bddnode * intersectbddnode __P((bddsystem *BddSystem, bddnode *BddNode1, bddnode *BddNode2)); 968 969 /*------------------------------------------------------\ 970 | | 971 | Fraction Functions | 972 | | 973 \------------------------------------------------------*/ 974 975 extern double fractionbddnode __P((bddsystem *BddSystem, bddnode *BddNode)); 976 977 /*------------------------------------------------------\ 978 | | 979 | Satisfy Functions | 980 | | 981 \------------------------------------------------------*/ 982 983 extern bddnode * satisfybddnode __P((bddsystem *BddSystem, bddnode *BddNode)); 984 extern bddnode * satisfybddnodeassoc __P((bddsystem *BddSystem, bddnode *BddNode, bddassoc *BddAssoc)); 985 986 /*------------------------------------------------------\ 987 | | 988 | Cofactor Functions | 989 | | 990 \------------------------------------------------------*/ 991 992 extern bddnode * cofactorbddnode __P((bddsystem *BddSystem, bddnode *BddNode1, bddnode *BddNode2)); 993 994 /*------------------------------------------------------\ 995 | | 996 | Reduce Functions | 997 | | 998 \------------------------------------------------------*/ 999 1000 extern bddnode * reducebddnode __P((bddsystem *BddSystem, bddnode *BddNode1, bddnode *BddNode2)); 1001 1002 /*------------------------------------------------------\ 1003 | | 1004 | Heath Functions | 1005 | | 1006 \------------------------------------------------------*/ 1007 1008 extern bddheath * getbddheath __P((bddsystem *BddSystem, bddnode *BddNode)); 1009 extern bddheath * getbddheathvar __P((bddsystem *BddSystem, bddnode *BddNode, bddvar Variable)); 1010 extern void delbddheath __P((bddsystem *BddSystem, bddheath *BddHeath)); 1011 1012 /*------------------------------------------------------\ 1013 | | 1014 | Simplify Functions | 1015 | | 1016 \------------------------------------------------------*/ 1017 1018 extern bddnode * simpbddnodedcon __P((bddsystem *BddSystem, bddnode *BddOn, bddnode *BddDc)); 1019 extern bddnode * simpbddnodedcoff __P((bddsystem *BddSystem, bddnode *BddOff, bddnode *BddDc)); 1020 1021 /*------------------------------------------------------\ 1022 | | 1023 | Conversion Functions | 1024 | | 1025 \------------------------------------------------------*/ 1026 1027 extern chain_list * convertbddnodeabl __P((bddsystem *BddSystem, char **NameArray, bddindex *IndexArray, bddnode *BddNode)); 1028 extern ablexpr *convertbddnodemuxabl(); 1029 extern chain_list * convertbddnodesumabl __P((bddsystem *BddSystem, char **NameArray, bddindex *IndexArray, bddnode *BddNode)); 1030 extern chain_list * convertbddindexabl __P((bddsystem *BddSystem, char **NameArray, bddindex *IndexArray, bddindex Index)); 1031 1032 /*------------------------------------------------------\ 1033 | | 1034 | Garbage Collect Functions | 1035 | | 1036 \------------------------------------------------------*/ 1037 1038 extern void garbagebddsystem __P((bddsystem *BddSystem)); 1039 extern void sweepbddsystem __P((bddsystem *BddSystem)); 1040 1041 /*------------------------------------------------------\ 1042 | | 1043 | Reorder Functions | 1044 | | 1045 \------------------------------------------------------*/ 1046 1047 extern void reorderbddsystemsimple __P((bddsystem *BddSystem)); 1048 extern void reorderbddsystemwindow __P((bddsystem *BddSystem)); 1049 extern void reorderbddsystemtop __P((bddsystem *BddSystem)); 1050 1051 extern void reorderbddsystemdynamic __P((bddsystem *BddSystem, void (*ReorderFunc)(), long ReorderLow, long ReorderRatio)); 1052 1053 /*------------------------------------------------------\ 1054 | | 1055 | Explosion Functions | 1056 | | 1057 \------------------------------------------------------*/ 1058 1059 extern void explosionbddsystemdynamic __P((bddsystem *BddSystem, void (*ExplosionFunc)(), long ExplosionLimit)); 1060 extern void explosionbddsystemrestart __P((bddsystem *BddSystem)); 1061 1062 /*------------------------------------------------------\ 1063 | | 1064 | Test Functions | 1065 | | 1066 \------------------------------------------------------*/ 1067 1068 extern int testbddcircuit __P((bddcircuit *BddCircuit)); 1069 1070 /*------------------------------------------------------\ 1071 | | 1072 | Dump Functions | 1073 | | 1074 \------------------------------------------------------*/ 1075 1076 extern bddcircuit * undumpbddcircuit __P((bddsystem *BddSystem, char *FileName)); 1077 extern void dumpbddcircuit __P((bddcircuit *BddCircuit, char *FileName)); 1078 1079 /*------------------------------------------------------\ 1080 | | 1081 | Name Functions | 1082 | | 1083 \------------------------------------------------------*/ 1084 1085 extern char * isbddstablename __P((char *StableName)); 1086 extern char * getbddstablename __P((char *Name)); 1087 1088 /*------------------------------------------------------\ 1089 | | 1090 | Log Compatibility Functions | 1091 | | 1092 \------------------------------------------------------*/ 1093 1094 extern bddnode * getlogbddnodeone __P(()); 1095 extern bddnode * getlogbddnodezero __P(()); 1096 extern bddnode * getlogbddnodeterm __P((bddindex Index)); 1097 extern bddnode * getlogbddnodenot __P((bddnode *BddNode)); 1098 extern bddnode * applylogbddnode __P((long Oper, bddnode *BddNode1, bddnode *BddNode2)); 1099 extern ablexpr * convertlogbddnode __P((bddcircuit *BddCircuit, bddnode *BddNode)); 1100 extern short addlogbddcircuitin __P((bddcircuit *BddCircuit, char *Name)); 1101 1102 /*------------------------------------------------------\ 1103 | | 1104 | Bdd Transfert Functions | 1105 | | 1106 \------------------------------------------------------*/ 1107 1108 extern bddnode * transfertbdd __P(( bddsystem *SystemSrc, bddsystem *SystemDst, bddnode *Node )); 1109 1110 1111 # endif 1112