distrib/sources/bdd/log_lib.h

   1 /*
   2  * This file is part of the Alliance CAD System
   3  * Copyright (C) Laboratoire LIP6 - Département ASIM
   4  * Universite Pierre et Marie Curie
   5  *
   6  * Home page          : http://www-asim.lip6.fr/alliance/
   7  * E-mail support     : mailto:alliance-support@asim.lip6.fr
   8  *
   9  * This progam is  free software; you can redistribute it  and/or modify it
  10  * under the  terms of the GNU  General Public License as  published by the
  11  * Free Software Foundation;  either version 2 of the License,  or (at your
  12  * option) any later version.
  13  *
  14  * Alliance VLSI  CAD System  is distributed  in the hope  that it  will be
  15  * useful, but WITHOUT  ANY WARRANTY; without even the  implied warranty of
  16  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
  17  * Public License for more details.
  18  *
  19  * You should have received a copy  of the GNU General Public License along
  20  * with the GNU C Library; see the  file COPYING. If not, write to the Free
  21  * Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
  22  */
  23
  24 /*
  25  * Tool    : ABL, BDD, HT Librarie
  26  * Date    : 1991,92
  27  * Author  : Luc Burgun
  28  * Modified by Czo <Olivier.Sirol@lip6.fr> 1996,97
  29  */
  30
  31
  32
  33 /* $Id: log_lib.h,v 1.39 2009/07/07 14:28:25 anthony Exp $ */
  34
  35 #ifndef LUC_LOG_H
  36 #define LUC_LOG_H
  37
  38 #undef OR
  39 #undef AND
  40 #undef XOR
  41 #undef NOT
  42 #undef NOR
  43 #undef NAND
  44 #undef NXOR
  45 #undef CONTRAINT
  46 #undef STABLE
  47 #undef RESTRICT
  48 #undef CNST
  49 #undef CAT
  50 #undef REPLICATE
  51
  52
  53 #define OR 0
  54 #define AND 1
  55 #define XOR 2
  56 #define NOT 3
  57 #define NOR 4
  58 #define NAND 5
  59 #define NXOR 6
  60 #define CONTRAINT 7
  61 #define STABLE 8
  62 #define RESTRICT 9
  63 #define CNST 10
  64 #define CAT         11
  65 #define REPLICATE   12
  66
  67
  68 /* ==================================================================
  69    Gestion de table de hachage                    Version du 16.07.91
  70    Les structures de donnees
  71    Burgun L.
  72    ================================================================== */
  73
  74
  75 #define EMPTYTH -1l
  76 #define VIDETH -1l
  77 #define DELETETH -2l
  78
  79 /*------ les structures pour la table de hachage des entiers -----*/
  80 #if 0
  81 typedef struct elemTH
  82   {
  83     char *key;
  84     long value;
  85   }
  86  *pElemTH;
  87
  88 /* table de hachage
  89    length est la longueur de la table,
  90    pElemTH le pointeur sur le debut de table,
  91    count le nombre d'elements deja rentres. */
  92
  93 typedef struct tableTH
  94   {
  95     int length;
  96     pElemTH pElem;
  97     int count;
  98   }
  99  *pTH;
 100 #endif
 101
 102   typedef ht *pTH;
 103   typedef htitem *pElemTH;
 104
 105 #define createTH addht
 106 #define destroyTH delht
 107 #define searchTH gethtitem
 108 #define addTH addhtitem
 109 #define addExistTH sethtitem
 110 #define deleteTH delhtitem
 111
 112 /* ==============================================================
 113    La bibliotheque des Arbres binaires Lisp-like version 23/08/91
 114    Burgun L.
 115    Structures de donnees
 116    ============================================================== */
 117
 118
 119
 120 /*-----------  Fonctions Lisp-Like de bas-niveau  -------------*/
 121
 122 #define CDR(expr)           (expr->NEXT)
 123 #define CAR(expr)           (*(chain_list **) &expr->DATA)
 124 #define CADR(expr)          CAR(CDR(expr))
 125 #define CDAR(expr)          CDR(CAR(expr))
 126 #define ATOM(expr)          (!expr->NEXT)
 127 #define VALUE_ATOM(expr)    (*(char **) &expr->DATA)
 128 #define OPER(expr)          (*(long *)&(CAR(expr))->DATA)
 129 #define VECT_S(expr)        (*(long *)&CADR(CAR(expr)))
 130 #define REP_NB(expr)        (*(long *)&CADR(CDAR(expr)))
 131 #define ATTRIB(expr)        CDAR(expr)
 132 #define VALUE_ATTRIB(expr)  REP_NB(expr)
 133
 134 /* ==============================================================
 135    La bibliotheque des graphes de decision binaires version 06/09/91
 136    Burgun L.
 137    Structures de donnees
 138    ============================================================== */
 139
 140 #undef OUI
 141 #undef NON
 142 #undef TRUE
 143 #undef FALSE
 144 #undef INPUT
 145 #undef OUTPUT
 146 #undef SMALL
 147 #undef MEDIUM
 148 #undef LARGE
 149
 150 #undef VIDE
 151 #undef DELETE
 152 #undef TABLE_PLEINE
 153 #undef BDDDELETE
 154 #undef BDDTABLE_PLEINE
 155 #undef MAX_SIZE_BDD
 156
 157 #undef DONTCARE0
 158 #undef DONTCARE1
 159 #undef DONTCARE2
 160
 161
 162 #define OUI 1
 163 #define NON 0
 164 #define TRUE 1
 165 #define FALSE 0
 166 #define INPUT 0
 167 #define OUTPUT 1
 168 #define SMALL 999
 169 #define MEDIUM 9999
 170 #define LARGE 99999
 171 #define SMALL_BDD 0
 172 #define MEDIUM_BDD 1
 173 #define LARGE_BDD 2
 174
 175 #define VIDE -1l
 176 #define DELETE -2l
 177 #define TABLE_PLEINE -3l
 178 #define BDDDELETE (pNode) DELETE
 179 #define BDDTABLE_PLEINE (pNode) TABLE_PLEINE
 180 #define MAX_SIZE_BDD 50000000   /* 50 Mega de noeuds Bdd */
 181
 182 #define DONTCARE0 11
 183 #define DONTCARE1 12
 184 #define DONTCARE2 13
 185
 186
 187
 188 /*---------------- structure d'un noeud de BDD -------------------*/
 189
 190 typedef struct node
 191   {
 192     struct node *high, *low;    /* les noeuds fils */
 193     short index;                /* index de la variable */
 194     short mark;                 /* nombre de peres pointant le noeud */
 195   }
 196  *pNode;
 197
 198
 199 /*--------------- La table de hachage pour des BDD ------------ */
 200
 201 /* table de hachage qui retourne des pointeurs de BDD
 202    lenTableBdd est la longueur de la table,
 203    pBddT le pointeur sur le debut de table,
 204    compteur le nombre d'elements deja rentres. */
 205
 206 typedef struct tableBdd
 207   {
 208     int lenTableBdd;
 209     pNode *pBdd;
 210     int compteur;
 211   }
 212  *pTableBdd;
 213
 214
 215
 216 /*------ les structures pour la table de hachage local -----*/
 217
 218 typedef struct vertexLoc
 219   {
 220     pNode high, low, father;
 221     short oper;
 222   }
 223  *pVertexLoc;
 224
 225 /* table de hachage pour la recuperation d'operation locale.
 226    lenTable est la longueur de la table,
 227    pElemT le pointeur sur le debut de table,
 228    compteur le nombre d'elements deja rentres. */
 229
 230 typedef struct tableLoc
 231   {
 232     int lenTabLoc;
 233     pVertexLoc pLoc;
 234   }
 235  *pTableLoc;
 236
 237 /*------------- structure pour les circuits -------------*/
 238
 239 typedef struct circuit
 240   {
 241     pTH pTI;
 242     pTH pTO;
 243     short countI;
 244     char **pNameI;
 245     char *name;
 246   }
 247  *pCircuit;
 248
 249 #define MAX_PACK 1000
 250
 251 /* structure systeme pour la generation de GDB . */
 252
 253 struct systemBdd
 254   {
 255     chain_list *lpAT;
 256     pTableBdd pRT;
 257     pNode pAT;
 258     int indiceAT;
 259     pTableLoc pMC;
 260   };
 261
 262 extern struct systemBdd sysBdd;
 263
 264 //extern pNode one, zero;
 265 extern pNode BDD_one, BDD_zero;
 266
 267 /**************** DECLARATION DES FONCTIONS *******/
 268
 269 #ifndef __P
 270 # if defined(__STDC__) || defined(__GNUC__)
 271 #  define __P(x) x
 272 # else
 273 #  define __P(x) ()
 274 # endif
 275 #endif
 276
 277 /* Prototypes from log_bdd0.c */
 278
 279   extern             int bddSystemAbandoned __P((void));
 280   extern            void setBddCeiling __P((int limit));
 281   extern             int getBddCeiling __P((void));
 282   extern            void unsetBddCeiling __P((void));
 283   extern           pNode initVertexBdd __P((int index, pNode high, pNode low));
 284   extern           pNode createNodeTermBdd __P((short index));
 285   extern            void initializeBdd __P((int size));
 286   extern            void destroyBdd __P((int level));
 287   extern            void resetBdd __P(());
 288   extern             int numberNodeAllBdd __P(());
 289   extern             int numberNodeBdd __P((pNode pBdd));
 290   extern             int countNode __P((pNode pt));
 291   extern             int countNodeTdg __P((pNode pt));
 292   extern    chain_list * muxAbl __P((pNode high, pNode low, chain_list *a, char **tabName));
 293   extern    chain_list * bddToAbl __P((pNode pt, char **tabName));
 294   extern            void displayBddLoc __P((short level, pNode pt));
 295   extern            void displayBdd __P((pNode pBdd, int level));
 296   extern            void assignNumNodeBdd __P((pNode bdd, pTH vTable, int *pNodeNumber));
 297   extern            void displayGraphicBdd __P((pNode pBdd));
 298   extern            void displayBddName __P((short level, pNode pt, char **TabName));
 299   extern            void displayBddNameLog __P((int lib, int loglevel, short level, pNode pt, char **TabName));
 300   extern           pNode notBdd __P((pNode pBdd));
 301   extern           pNode applyTerm __P((int oper, short index, pNode pBdd));
 302   extern           pNode applyBinBdd __P((short oper, pNode pBdd1, pNode pBdd2));
 303   extern           pNode applyBdd __P((short oper, chain_list *pt));
 304   extern           pNode cnstBdd __P((pNode pBdd1, pNode pBddGc));
 305   extern           pNode restrictBdd __P((pNode pBdd1, pNode pBddGc));
 306   extern           pNode constraintBdd __P((pNode pBdd1, pNode pBddGc));
 307   extern           pNode simplifDcZeroBdd __P((pNode pGon, pNode pGdc));
 308   extern           pNode simplifPlusDcZeroBdd __P((pNode pGon, pNode pGdc));
 309   extern           pNode simplifDcOneBdd __P((pNode pGon, pNode pGdc));
 310   extern           pNode simplifDcOneFPGABdd __P((pNode pGon, pNode pGdc));
 311   extern           pNode composeBdd __P((pNode pBdd1, pNode pBdd2, int index));
 312   extern    chain_list * addListBdd __P((chain_list *pt, pNode pBdd));
 313   extern             int oneBdd __P((pNode pBdd));
 314   extern             int zeroBdd __P((pNode pBdd));
 315   extern             int equalBdd __P((pNode pBdd1, pNode pBdd2));
 316   extern            void markBdd __P((pNode pBdd, short value));
 317   extern           pNode upVarBdd __P((pNode pF, pNode pFoldIndex, short newIndex));
 318   extern            void markAllBdd __P((short value));
 319   extern            void supportBddInt __P((pNode pt, chain_list **ppCL));
 320   extern    chain_list * supportChain_listBdd __P((pNode pBdd));
 321   extern           pNode initVertexBddAux __P((short index, pNode high, pNode low, struct systemBdd *sysCible));
 322   extern           pNode regenereBdd __P((pNode pBdd, struct systemBdd *sysCible, pTH pTHNode));
 323   extern            void gcNodeBdd __P((chain_list *pt));
 324   extern            void rempTabIndex __P((pNode pt, char *tabIndex));
 325   extern    chain_list * supportIndexBdd __P((pNode pt, int sens));
 326
 327
 328 /* Prototypes from log_bdd1.c */
 329
 330   extern        pCircuit initializeCct __P((char *name, int nbI, int nbO));
 331   extern            void resetCct __P((pCircuit pC));
 332   extern            void destroyCct __P((pCircuit pC));
 333   extern           pNode searchOutputCct __P((pCircuit pC, char *name));
 334   extern           pNode searchOutputCct_no_NA __P((pCircuit pC, char *name));
 335   extern            void addOutputCct __P((pCircuit pC, char *name, pNode pt));
 336   extern            void addOutputCct_no_NA __P((pCircuit pC, char *name, pNode pt));
 337   extern          char * searchIndexCct __P((pCircuit pC, short index));
 338   extern           short searchInputCct __P((pCircuit pC, char *name));
 339   extern           short searchInputCct_no_NA __P((pCircuit pC, char *name));
 340   extern           short addInputCct __P((pCircuit pC, char *name));
 341   extern           short addInputCct_no_NA __P((pCircuit pC, char *name));
 342   extern            void delInputCct __P((pCircuit pC, char *name));
 343   extern            void displayCctLog __P((int lib, int loglevel, pCircuit pC, int mode));
 344   extern            void displayCct __P((pCircuit pC, int mode));
 345
 346   extern            void composeCct __P((pCircuit pC, char *name, pNode pt));
 347   extern            void constraintCct __P((pCircuit pC, pNode pt));
 348   extern            void proofCct __P((pCircuit pC1, pCircuit pC2));
 349   extern           pNode ablToBddCct __P((pCircuit pC, chain_list *expr));
 350   extern            void cpOrderCct __P((pCircuit CC1, pCircuit CC2));
 351   extern            void upVarCct __P((pCircuit pC, pNode ptOldIndex, short newIndex));
 352   extern             int numberNodeCct __P((pCircuit pC));
 353   extern             int numberNodeTdgCct __P((pCircuit pC));
 354   extern    chain_list * bddToAblCct __P((pCircuit pC, pNode pBdd));
 355   extern            void gcNodeCct __P((pCircuit pC));
 356
 357
 358 /* Prototypes from log_prefbib.c */
 359
 360   extern          char * gensym_abl __P((char *name, int num));
 361   extern            void ablError __P((chain_list *expr, char *func));
 362   extern    chain_list * createAtom __P((char *name));
 363   extern    chain_list * createAtom_no_NA __P((char *name));
 364   extern    chain_list * createExpr __P((short oper));
 365   extern    chain_list * notExpr __P((chain_list *expr));
 366   extern    chain_list * createBinExpr __P((short oper, chain_list *expr1, chain_list *expr2));
 367   extern            void addQExpr __P((chain_list *expr1, chain_list *expr2));
 368   extern            void addHExpr __P((chain_list *expr1, chain_list *expr2));
 369   extern            void freeExpr __P((chain_list *expr));
 370   extern          char * operToChar __P((short oper));
 371   extern           short charToOper __P((char *name));
 372   extern            void displayExpr __P((chain_list *expr));
 373   extern            void displayExprLog __P((int lib, int loglevel, chain_list *expr));
 374   extern            void displayInfExprLog __P((int lib, int loglevel, chain_list *expr));
 375   extern            void displayInfExpr __P((chain_list *expr));
 376   extern          char * exprToCharInt __P((chain_list *expr, int mode, char *chaine, int *taille));
 377   extern          char * exprToChar __P((chain_list *expr, int mode));
 378   extern          char * identExprInt __P((chain_list *expr, char *chaine, int *taille));
 379   extern          char * identExpr __P((chain_list *expr));
 380   extern             int profExpr __P((chain_list *expr));
 381   extern             int profAOExpr __P((chain_list *expr));
 382   extern    chain_list * mapCarExpr __P((chain_list *(*func)(), short oper, chain_list *expr));
 383   extern            void mapExpr __P((void (*func)(), chain_list *expr));
 384   extern             int anyExpr __P((int (*func)(), chain_list *expr));
 385   extern             int everyExpr __P((int (*func)(), chain_list *expr));
 386   extern             int searchOperExpr __P((chain_list *expr, short oper));
 387   extern           short searchExprLow __P((chain_list *expr, char *name));
 388   extern             int searchExpr __P((chain_list *expr, char *name));
 389   extern             int equalExpr __P((chain_list *expr1, chain_list *expr2));
 390   extern             int equalVarExpr __P((chain_list *expr1, chain_list *expr2));
 391   extern             int lengthExpr __P((chain_list *expr));
 392   extern             int numberOperBinExpr __P((chain_list *expr));
 393   extern             int numberAtomExpr __P((chain_list *expr));
 394   extern    chain_list * copyExpr __P((chain_list *expr));
 395   extern            void substPhyExpr __P((chain_list *expr1, char *name, chain_list *expr2));
 396   extern    chain_list * substExpr __P((chain_list *expr1, char *name, chain_list *expr2));
 397   extern    chain_list * devXorExpr __P((chain_list *expr));
 398   extern    chain_list * devXor2Expr __P((chain_list *expr));
 399   extern    chain_list * flatPolarityExpr __P((chain_list *expr, int signe));
 400   extern            void flatArityExpr __P((chain_list *expr));
 401   extern            void supportChain_listExprInt __P((chain_list *expr, chain_list **ppCL));
 402   extern    chain_list * supportChain_listExpr __P((chain_list *expr));
 403   extern            void fullSupportChain_listExprInt __P((chain_list *expr, chain_list **ppCL));
 404   extern    chain_list * fullSupportChain_listExpr __P((chain_list *expr));
 405   extern            void supportPtype_listExprInt __P((chain_list *expr, ptype_list **ppCL));
 406   extern    ptype_list * supportPtype_listExpr __P((chain_list *expr));
 407   extern    chain_list * maxExpr __P((chain_list *expr, int (*func)()));
 408   extern    chain_list * minExpr __P((chain_list *expr, int (*func)()));
 409   extern            void sortExpr __P((chain_list *expr, long (*func)(), int direction));
 410   extern            long funcNormExpr __P((chain_list *expr));
 411   extern            void normExpr __P((chain_list *expr));
 412   extern            void deleteNumExpr __P((chain_list *expr, int i));
 413   extern    chain_list * searchNumExpr __P((chain_list *expr, int i));
 414   extern             int numberOccExpr __P((chain_list *exp, char *name));
 415   extern            void changeOperExpr __P((chain_list *expr, short oper));
 416   extern    chain_list * simplif10Expr __P((chain_list *expr));
 417   extern    chain_list * simplifNotExpr __P((chain_list *exp));
 418   extern    chain_list * charToExprInt __P((char *stringExpr, int *cptCar));
 419   extern    chain_list * charToExpr __P((char *stringExpr));
 420   extern          char * tokenExpr __P((char *stringExpr, int *cptCar));
 421   extern             int PMExprInt __P((chain_list *expr, chain_list *pattern, ptype_list **bind));
 422   extern             int PMExpr __P((chain_list *expr, chain_list *pattern));
 423
 424   extern            void replaceAtomByExpr __P((chain_list *expr, char *name, chain_list *newexpr));
 425
 426 /* Prototypes from log_thash.c */
 427 #if 0
 428   extern             int hashTH __P((char *pn));
 429   extern             pTH createTH __P((int len));
 430   extern            void destroyTH __P((pTH pTable));
 431   extern            long searchTH __P((pTH pTable, char *key));
 432   extern            long addTH __P((pTH pTable, char *key, long value));
 433   extern            long addExistTH __P((pTH pTable, char *key, long value));
 434   extern            long deleteTH __P((pTH pTable, char *key));
 435   extern            void displayTH __P((pTH pTable));
 436   extern            void reAllocTH __P((pTH pTable));
 437 #endif
 438
 439
 440 /* Prototypes from log_thashbdd.c */
 441
 442   extern            long hashBdd __P((int index, pNode high, pNode low));
 443   extern            long newKeyBdd __P((int index, pNode high, pNode low));
 444   extern       pTableBdd createTableBdd __P((int len));
 445   extern            void destroyTableBdd __P((pTableBdd pTab));
 446   extern       pTableBdd reAllocTableBdd __P((pTableBdd pTab));
 447   extern           pNode searchTableBdd __P((pTableBdd pTab, int index, pNode high, pNode low));
 448   extern            long addTableBdd __P((pTableBdd pTab, pNode pBdd));
 449   extern            long deleteTableBdd __P((pTableBdd pTab, pNode pBdd));
 450   extern            void displayHashBdd __P((pTableBdd pTab));
 451
 452
 453 /* Prototypes from log_thashloc.c */
 454
 455   extern            long hashLoc __P((pNode high, pNode low));
 456   extern       pTableLoc createTabLoc __P((int len));
 457   extern            void destroyTabLoc __P((pTableLoc pTab));
 458   extern           pNode searchTabLoc __P((pTableLoc pTab, pNode high, pNode low, short oper));
 459   extern            long addTabLoc __P((pTableLoc pTab, pNode high, pNode low, pNode father, short oper));
 460   extern            void displayLoc __P((pTableLoc pTab));
 461   extern            void videTabLoc __P((pTableLoc pTab));
 462
 463
 464 /* Prototypes from log_vectabl.c */
 465   extern    chain_list * concatAbl __P((chain_list *expr1,chain_list *expr2));
 466   extern    chain_list * replicateAbl __P((chain_list *expr ,int  n));
 467   extern    chain_list * getAblAtPos __P((chain_list *expr ,int  pos));
 468   extern             int getVectAblRange __P((chain_list *expr ,int *left,int *right));
 469   extern          char * getVectAblVarName __P((chain_list *expr));
 470   extern             int verifyVectAbl __P((chain_list *expr));
 471   extern             int getAtomSize __P((chain_list *expr));
 472   extern    chain_list * getAblAtIndex __P((chain_list *expr,int left,int right,int index));
 473   extern            void invertVectAbl __P((chain_list *expr));
 474   extern            void invertAtom __P((chain_list *expr));
 475   extern            void initBitStrTable __P((void));
 476   extern             int isBitStr __P((char *bitstr));
 477   extern          char * genOneBitStr __P((int n));
 478   extern          char * genZeroBitStr __P((int n));
 479   extern          char * genHZBitStr __P((int n));
 480   extern            void fprintHZBitStr __P((FILE *file,char *bitstr));
 481   extern          char * notBitStr __P((char *bitstr));
 482   extern    chain_list * createBitStr __P((char *bitstr));
 483   extern          char * genUBitStr __P((int n));
 484   extern          char * getBitStr __P((char *str));
 485   extern             int changeAblAtRange __P((chain_list *expr,int left,int right, chain_list *added,int mode));
 486   extern          char * renameVectAtom __P((char *oldname,char *newname,int shift));
 487   extern    chain_list * createVectAtom __P((char *name,int left,int right));
 488   extern          char * createVectAtomName __P((char *name,int left,int right));
 489   extern            void getVectAtomRange __P((chain_list *expr,char **name,int *left, int*right));
 490   extern            void repToCatVectAbl __P((chain_list *expr));
 491   extern          char * makeBitStr __P((char *bistr));
 492   extern FILE *LOG_DEBUG_FILE;
 493   extern    chain_list * supportChain_listBddExpr(pCircuit circuit, pNode bdd);
 494
 495   chain_list *ablCreateMintermList(chain_list *expr);
 496
 497 #endif