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 : mailto:alliance-users@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., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 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.h,v 1.7 2012/05/14 14:20:19 alliance 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 50 #define OR 0 51 #define AND 1 52 #define XOR 2 53 #define NOT 3 54 #define NOR 4 55 #define NAND 5 56 #define NXOR 6 57 #define CONTRAINT 7 58 #define STABLE 8 59 #define RESTRICT 9 60 #define CNST 10 61 62 /* ================================================================== 63 Gestion de table de hachage Version du 16.07.91 64 Les structures de donnees 65 Burgun L. 66 ================================================================== */ 67 68 69 #define EMPTYTH -1 70 #define VIDETH -1 71 #define DELETETH -2 72 73 /*------ les structures pour la table de hachage des entiers -----*/ 74 75 typedef struct elemTH 76 { 77 char *key; 78 long value; 79 } 80 *pElemTH; 81 82 /* table de hachage 83 length est la longueur de la table, 84 pElemTH le pointeur sur le debut de table, 85 count le nombre d'elements deja rentres. */ 86 87 typedef struct tableTH 88 { 89 long length; 90 pElemTH pElem; 91 long count; 92 } 93 *pTH; 94 95 96 /* ============================================================== 97 La bibliotheque des Arbres binaires Lisp-like version 23/08/91 98 Burgun L. 99 Structures de donnees 100 ============================================================== */ 101 102 103 104 /*----------- Fonctions Lisp-Like de bas-niveau -------------*/ 105 106 #define CDR(expr) (expr->NEXT) 107 #define CAR(expr) ((chain_list *) expr->DATA) 108 #define CADR(expr) CAR(CDR(expr)) 109 #define ATOM(expr) (!expr->NEXT) 110 #define VALUE_ATOM(expr) (char *) expr->DATA 111 #define OPER(expr) ((long)(CAR(expr))->DATA) 112 113 114 115 /* ============================================================== 116 La bibliotheque des graphes de decision binaires version 06/09/91 117 Burgun L. 118 Structures de donnees 119 ============================================================== */ 120 121 #undef OUI 122 #undef NON 123 #undef TRUE 124 #undef FALSE 125 #undef INPUT 126 #undef OUTPUT 127 #undef SMALL 128 #undef MEDIUM 129 #undef LARGE 130 131 #undef VIDE 132 #undef DELETE 133 #undef TABLE_PLEINE 134 #undef BDDDELETE 135 #undef BDDTABLE_PLEINE 136 #undef MAX_SIZE_BDD 137 138 #undef DONTCARE0 139 #undef DONTCARE1 140 #undef DONTCARE2 141 142 143 #define OUI 1 144 #define NON 0 145 #define TRUE 1 146 #define FALSE 0 147 #define INPUT 0 148 #define OUTPUT 1 149 #define SMALL 999 150 #define MEDIUM 9999 151 #define LARGE 99999 152 #define SMALL_BDD 0 153 #define MEDIUM_BDD 1 154 #define LARGE_BDD 2 155 156 #define VIDE -1 157 #define DELETE -2 158 #define TABLE_PLEINE -3 159 #define BDDDELETE (pNode) DELETE 160 #define BDDTABLE_PLEINE (pNode) TABLE_PLEINE 161 #define MAX_SIZE_BDD 50000000 /* 50 Mega de noeuds Bdd */ 162 163 #define DONTCARE0 11 164 #define DONTCARE1 12 165 #define DONTCARE2 13 166 167 168 169 /*---------------- structure d'un noeud de BDD -------------------*/ 170 171 typedef struct node 172 { 173 struct node *high, *low; /* les noeuds fils */ 174 short index; /* index de la variable */ 175 short mark; /* nombre de peres pointant le noeud */ 176 } 177 *pNode; 178 179 180 /*--------------- La table de hachage pour des BDD ------------ */ 181 182 /* table de hachage qui retourne des pointeurs de BDD 183 lenTableBdd est la longueur de la table, 184 pBddT le pointeur sur le debut de table, 185 compteur le nombre d'elements deja rentres. */ 186 187 typedef struct tableBdd 188 { 189 long lenTableBdd; 190 pNode *pBdd; 191 long compteur; 192 } 193 *pTableBdd; 194 195 196 197 /*------ les structures pour la table de hachage local -----*/ 198 199 typedef struct vertexLoc 200 { 201 pNode high, low, father; 202 short oper; 203 } 204 *pVertexLoc; 205 206 /* table de hachage pour la recuperation d'operation locale. 207 lenTable est la longueur de la table, 208 pElemT le pointeur sur le debut de table, 209 compteur le nombre d'elements deja rentres. */ 210 211 typedef struct tableLoc 212 { 213 long lenTabLoc; 214 pVertexLoc pLoc; 215 } 216 *pTableLoc; 217 218 /*------------- structure pour les circuits -------------*/ 219 220 typedef struct circuit 221 { 222 pTH pTI; 223 pTH pTO; 224 short countI; 225 char **pNameI; 226 char *name; 227 } 228 *pCircuit; 229 230 #define MAX_PACK 1000 231 232 /* structure systeme pour la generation de GDB . */ 233 234 struct systemBdd 235 { 236 chain_list *lpAT; 237 pTableBdd pRT; 238 pNode pAT; 239 long indiceAT; 240 pTableLoc pMC; 241 }; 242 extern struct systemBdd sysBdd; 243 244 extern pNode one, zero; 245 246 /**************** DECLARATION DES FONCTIONS *******/ 247 248 #ifndef __P 249 # if defined(__STDC__) || defined(__GNUC__) 250 # define __P(x) x 251 # else 252 # define __P(x) () 253 # endif 254 #endif 255 256 /* Prototypes from log_bdd0.c */ 257 258 extern pNode initVertexBdd __P((long index, pNode high, pNode low)); 259 extern pNode createNodeTermBdd __P((short index)); 260 extern void initializeBdd __P((long size)); 261 extern void destroyBdd __P((long level)); 262 extern void resetBdd __P(()); 263 extern long numberNodeAllBdd __P(()); 264 extern long numberNodeBdd __P((pNode pBdd)); 265 extern long countNode __P((pNode pt)); 266 extern long countNodeTdg __P((pNode pt)); 267 extern chain_list * muxAbl __P((pNode high, pNode low, chain_list *a, char **tabName)); 268 extern chain_list * bddToAbl __P((pNode pt, char **tabName)); 269 extern void displayBddLoc __P((short level, pNode pt)); 270 extern void displayBdd __P((pNode pBdd, long level)); 271 extern void assignNumNodeBdd __P((pNode bdd, pTH vTable, long *pNodeNumber)); 272 extern void displayGraphicBdd __P((pNode pBdd)); 273 extern void displayBddName __P((short level, pNode pt, char **TabName)); 274 extern pNode notBdd __P((pNode pBdd)); 275 extern pNode applyTerm __P((long oper, short index, pNode pBdd)); 276 extern pNode applyBinBdd __P((short oper, pNode pBdd1, pNode pBdd2)); 277 extern pNode applyBdd __P((short oper, chain_list *pt)); 278 extern pNode cnstBdd __P((pNode pBdd1, pNode pBddGc)); 279 extern pNode restrictBdd __P((pNode pBdd1, pNode pBddGc)); 280 extern pNode constraintBdd __P((pNode pBdd1, pNode pBddGc)); 281 extern pNode simplifDcZeroBdd __P((pNode pGon, pNode pGdc)); 282 extern pNode simplifPlusDcZeroBdd __P((pNode pGon, pNode pGdc)); 283 extern pNode simplifDcOneBdd __P((pNode pGon, pNode pGdc)); 284 extern pNode simplifDcOneFPGABdd __P((pNode pGon, pNode pGdc)); 285 extern pNode composeBdd __P((pNode pBdd1, pNode pBdd2, long index)); 286 extern chain_list * addListBdd __P((chain_list *pt, pNode pBdd)); 287 extern long oneBdd __P((pNode pBdd)); 288 extern long zeroBdd __P((pNode pBdd)); 289 extern long equalBdd __P((pNode pBdd1, pNode pBdd2)); 290 extern void markBdd __P((pNode pBdd, short value)); 291 extern pNode upVarBdd __P((pNode pF, pNode pFoldIndex, short newIndex)); 292 extern void markAllBdd __P((short value)); 293 extern void supportBddInt __P((pNode pt, chain_list **ppCL)); 294 extern chain_list * supportChain_listBdd __P((pNode pBdd)); 295 extern pNode initVertexBddAux __P((short index, pNode high, pNode low, struct systemBdd *sysCible)); 296 extern pNode regenereBdd __P((pNode pBdd, struct systemBdd *sysCible, pTH pTHNode)); 297 extern void gcNodeBdd __P((chain_list *pt)); 298 extern void rempTabIndex __P((pNode pt, char *tabIndex)); 299 extern chain_list * supportIndexBdd __P((pNode pt, long sens)); 300 301 302 /* Prototypes from log_bdd1.c */ 303 304 extern pCircuit initializeCct __P((char *name, long nbI, long nbO)); 305 extern void resetCct __P((pCircuit pC)); 306 extern void destroyCct __P((pCircuit pC)); 307 extern pNode searchOutputCct __P((pCircuit pC, char *name)); 308 extern void addOutputCct __P((pCircuit pC, char *name, pNode pt)); 309 extern char * searchIndexCct __P((pCircuit pC, short index)); 310 extern short searchInputCct __P((pCircuit pC, char *name)); 311 extern short addInputCct __P((pCircuit pC, char *name)); 312 extern void delInputCct __P((pCircuit pC, char *name)); 313 extern void displayCct __P((pCircuit pC, long mode)); 314 extern void composeCct __P((pCircuit pC, char *name, pNode pt)); 315 extern void constraintCct __P((pCircuit pC, pNode pt)); 316 extern void proofCct __P((pCircuit pC1, pCircuit pC2)); 317 extern pNode ablToBddCct __P((pCircuit pC, chain_list *expr)); 318 extern void cpOrderCct __P((pCircuit CC1, pCircuit CC2)); 319 extern void upVarCct __P((pCircuit pC, pNode ptOldIndex, short newIndex)); 320 extern long numberNodeCct __P((pCircuit pC)); 321 extern long numberNodeTdgCct __P((pCircuit pC)); 322 extern chain_list * bddToAblCct __P((pCircuit pC, pNode pBdd)); 323 extern void gcNodeCct __P((pCircuit pC)); 324 325 326 /* Prototypes from log_prefbib.c */ 327 328 extern char * gensym_abl __P((char *name, long num)); 329 extern void ablError __P((chain_list *expr, char *func)); 330 extern chain_list * createAtom __P((char *name)); 331 extern chain_list * createExpr __P((short oper)); 332 extern chain_list * notExpr __P((chain_list *expr)); 333 extern chain_list * createBinExpr __P((short oper, chain_list *expr1, chain_list *expr2)); 334 extern void addQExpr __P((chain_list *expr1, chain_list *expr2)); 335 extern void addHExpr __P((chain_list *expr1, chain_list *expr2)); 336 extern void freeExpr __P((chain_list *expr)); 337 extern char * operToChar __P((short oper)); 338 extern short charToOper __P((char *name)); 339 extern void displayExprInt __P((chain_list *expr)); 340 extern void displayExpr __P((chain_list *expr)); 341 extern void displayInfExpr __P((chain_list *expr)); 342 extern char * exprToCharInt __P((chain_list *expr, long mode, char *chaine, long *taille)); 343 extern char * exprToChar __P((chain_list *expr, long mode)); 344 extern char * identExprInt __P((chain_list *expr, char *chaine, long *taille)); 345 extern char * identExpr __P((chain_list *expr)); 346 extern long profExpr __P((chain_list *expr)); 347 extern long profAOExpr __P((chain_list *expr)); 348 extern chain_list * mapCarExpr __P((chain_list *(*func)(), short oper, chain_list *expr)); 349 extern void mapExpr __P((void (*func)(), chain_list *expr)); 350 extern long anyExpr __P((long (*func)(), chain_list *expr)); 351 extern long everyExpr __P((long (*func)(), chain_list *expr)); 352 extern long searchOperExpr __P((chain_list *expr, short oper)); 353 extern short searchExprLow __P((chain_list *expr, char *name)); 354 extern long searchExpr __P((chain_list *expr, char *name)); 355 extern long equalExpr __P((chain_list *expr1, chain_list *expr2)); 356 extern long equalVarExpr __P((chain_list *expr1, chain_list *expr2)); 357 extern long lengthExpr __P((chain_list *expr)); 358 extern long numberOperBinExpr __P((chain_list *expr)); 359 extern long numberAtomExpr __P((chain_list *expr)); 360 extern chain_list * copyExpr __P((chain_list *expr)); 361 extern void substPhyExpr __P((chain_list *expr1, char *name, chain_list *expr2)); 362 extern chain_list * substExpr __P((chain_list *expr1, char *name, chain_list *expr2)); 363 extern chain_list * devXorExpr __P((chain_list *expr)); 364 extern chain_list * devXor2Expr __P((chain_list *expr)); 365 extern chain_list * flatPolarityExpr __P((chain_list *expr, long signe)); 366 extern void flatArityExpr __P((chain_list *expr)); 367 extern void supportChain_listExprInt __P((chain_list *expr, chain_list **ppCL)); 368 extern chain_list * supportChain_listExpr __P((chain_list *expr)); 369 extern void supportPtype_listExprInt __P((chain_list *expr, ptype_list **ppCL)); 370 extern ptype_list * supportPtype_listExpr __P((chain_list *expr)); 371 extern chain_list * maxExpr __P((chain_list *expr, long (*func)())); 372 extern chain_list * minExpr __P((chain_list *expr, long (*func)())); 373 extern void sortExpr __P((chain_list *expr, long (*func)(), long direction)); 374 extern long funcNormExpr __P((chain_list *expr)); 375 extern void normExpr __P((chain_list *expr)); 376 extern void deleteNumExpr __P((chain_list *expr, long i)); 377 extern chain_list * searchNumExpr __P((chain_list *expr, long i)); 378 extern long numberOccExpr __P((chain_list *exp, char *name)); 379 extern void changeOperExpr __P((chain_list *expr, short oper)); 380 extern chain_list * simplif10Expr __P((chain_list *expr)); 381 extern chain_list * simplifNotExpr __P((chain_list *exp)); 382 extern chain_list * charToExprInt __P((char *stringExpr, long *cptCar)); 383 extern chain_list * charToExpr __P((char *stringExpr)); 384 extern char * tokenExpr __P((char *stringExpr, long *cptCar)); 385 extern long PMExprInt __P((chain_list *expr, chain_list *pattern, ptype_list **bind)); 386 extern long PMExpr __P((chain_list *expr, chain_list *pattern)); 387 388 389 /* Prototypes from log_thash.c */ 390 391 extern long hashTH __P((char *pn)); 392 extern pTH createTH __P((long len)); 393 extern void destroyTH __P((pTH pTable)); 394 extern long searchTH __P((pTH pTable, char *key)); 395 extern long addTH __P((pTH pTable, char *key, long value)); 396 extern long addExistTH __P((pTH pTable, char *key, long value)); 397 extern long deleteTH __P((pTH pTable, char *key)); 398 extern void displayTH __P((pTH pTable)); 399 extern void reAllocTH __P((pTH pTable)); 400 401 402 /* Prototypes from log_thashbdd.c */ 403 404 extern long hashBdd __P((long index, pNode high, pNode low)); 405 extern long newKeyBdd __P((long index, pNode high, pNode low)); 406 extern pTableBdd createTableBdd __P((long len)); 407 extern void destroyTableBdd __P((pTableBdd pTab)); 408 extern pTableBdd reAllocTableBdd __P((pTableBdd pTab)); 409 extern pNode searchTableBdd __P((pTableBdd pTab, long index, pNode high, pNode low)); 410 extern long addTableBdd __P((pTableBdd pTab, pNode pBdd)); 411 extern long deleteTableBdd __P((pTableBdd pTab, pNode pBdd)); 412 extern void displayHashBdd __P((pTableBdd pTab)); 413 414 415 /* Prototypes from log_thashloc.c */ 416 417 extern long hashLoc __P((pNode high, pNode low)); 418 extern pTableLoc createTabLoc __P((long len)); 419 extern void destroyTabLoc __P((pTableLoc pTab)); 420 extern pNode searchTabLoc __P((pTableLoc pTab, pNode high, pNode low, short oper)); 421 extern long addTabLoc __P((pTableLoc pTab, pNode high, pNode low, pNode father, short oper)); 422 extern void displayLoc __P((pTableLoc pTab)); 423 extern void videTabLoc __P((pTableLoc pTab)); 424 #endif 425