abc70930: src/aig/aig/aig.h Source File

00001 
00021 #ifndef __AIG_H__
00022 #define __AIG_H__
00023 
00024 #ifdef __cplusplus
00025 extern "C" {
00026 #endif 
00027 
00031 
00032 #include <stdio.h>
00033 #include <stdlib.h>
00034 #include <string.h>
00035 #include <assert.h>
00036 #include <time.h>
00037 
00038 #include "vec.h"
00039 
00043 
00047 
00048 typedef struct Aig_Man_t_            Aig_Man_t;
00049 typedef struct Aig_Obj_t_            Aig_Obj_t;
00050 typedef struct Aig_MmFixed_t_        Aig_MmFixed_t;    
00051 typedef struct Aig_MmFlex_t_         Aig_MmFlex_t;     
00052 typedef struct Aig_MmStep_t_         Aig_MmStep_t;     
00053 typedef struct Aig_TMan_t_           Aig_TMan_t;
00054 
00055 // object types
00056 typedef enum { 
00057     AIG_OBJ_NONE,                    // 0: non-existent object
00058     AIG_OBJ_CONST1,                  // 1: constant 1 
00059     AIG_OBJ_PI,                      // 2: primary input
00060     AIG_OBJ_PO,                      // 3: primary output
00061     AIG_OBJ_BUF,                     // 4: buffer node
00062     AIG_OBJ_AND,                     // 5: AND node
00063     AIG_OBJ_EXOR,                    // 6: EXOR node
00064     AIG_OBJ_LATCH,                   // 7: latch
00065     AIG_OBJ_VOID                     // 8: unused object
00066 } Aig_Type_t;
00067 
00068 // the AIG node
00069 struct Aig_Obj_t_  // 8 words
00070 {
00071     Aig_Obj_t *      pNext;          // strashing table
00072     Aig_Obj_t *      pFanin0;        // fanin
00073     Aig_Obj_t *      pFanin1;        // fanin
00074     unsigned int     Type    :  3;   // object type
00075     unsigned int     fPhase  :  1;   // value under 000...0 pattern
00076     unsigned int     fMarkA  :  1;   // multipurpose mask
00077     unsigned int     fMarkB  :  1;   // multipurpose mask
00078     unsigned int     nRefs   : 26;   // reference count 
00079     unsigned         Level   : 24;   // the level of this node
00080     unsigned         nCuts   :  8;   // the number of cuts
00081     int              TravId;         // unique ID of last traversal involving the node
00082     int              Id;             // unique ID of the node
00083     union {                          // temporary store for user's data
00084         void *       pData;
00085         int          iData;
00086         float        dData;
00087     };
00088 };
00089 
00090 // the AIG manager
00091 struct Aig_Man_t_
00092 {
00093     char *           pName;          // the design name
00094     // AIG nodes
00095     Vec_Ptr_t *      vPis;           // the array of PIs
00096     Vec_Ptr_t *      vPos;           // the array of POs
00097     Vec_Ptr_t *      vObjs;          // the array of all nodes (optional)
00098     Vec_Ptr_t *      vBufs;          // the array of buffers
00099     Aig_Obj_t *      pConst1;        // the constant 1 node
00100     Aig_Obj_t        Ghost;          // the ghost node
00101     int              nRegs;          // the number of registers (registers are last POs)
00102     int              nAsserts;       // the number of asserts among POs (asserts are first POs)
00103     // AIG node counters
00104     int              nObjs[AIG_OBJ_VOID];// the number of objects by type
00105     int              nCreated;       // the number of created objects
00106     int              nDeleted;       // the number of deleted objects
00107     // structural hash table
00108     Aig_Obj_t **     pTable;         // structural hash table
00109     int              nTableSize;     // structural hash table size
00110     // representation of fanouts
00111     int *            pFanData;       // the database to store fanout information
00112     int              nFansAlloc;     // the size of fanout representation
00113     Vec_Vec_t *      vLevels;        // used to update timing information
00114     int              nBufReplaces;   // the number of times replacement led to a buffer
00115     int              nBufFixes;      // the number of times buffers were propagated
00116     int              nBufMax;        // the maximum number of buffers during computation
00117     // topological order
00118     unsigned *       pOrderData;
00119     int              nOrderAlloc;
00120     int              iPrev;
00121     int              iNext;
00122     int              nAndTotal;
00123     int              nAndPrev;
00124     // representatives
00125     Aig_Obj_t **     pEquivs;        // linked list of equivalent nodes (when choices are used)
00126     Aig_Obj_t **     pReprs;         // representatives of each node
00127     int              nReprsAlloc;    // the number of allocated representatives
00128     // various data members
00129     Aig_MmFixed_t *  pMemObjs;       // memory manager for objects
00130     Vec_Int_t *      vLevelR;        // the reverse level of the nodes
00131     int              nLevelMax;      // maximum number of levels
00132     void *           pData;          // the temporary data
00133     int              nTravIds;       // the current traversal ID
00134     int              fCatchExor;     // enables EXOR nodes
00135     int              fAddStrash;     // performs additional strashing
00136     Aig_Obj_t **     pObjCopies;     // mapping of AIG nodes into FRAIG nodes
00137     void (*pImpFunc) (void*, void*); // implication checking precedure
00138     void *           pImpData;       // implication checking data
00139     Aig_TMan_t *     pManTime;       // the timing manager
00140     Vec_Ptr_t *      vMapped;
00141     Vec_Int_t *      vFlopNums;      
00142     // timing statistics
00143     int              time1;
00144     int              time2;
00145 };
00146 
00150 
00151 #define AIG_MIN(a,b)       (((a) < (b))? (a) : (b))
00152 #define AIG_MAX(a,b)       (((a) > (b))? (a) : (b))
00153 #define AIG_ABS(a)         (((a) >= 0)?  (a) :-(a))
00154 #define AIG_INFINITY       (100000000)
00155 
00156 #ifndef PRT
00157 #define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
00158 #endif
00159 
00160 static inline int          Aig_Base2Log( unsigned n )             { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
00161 static inline int          Aig_Base10Log( unsigned n )            { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
00162 static inline char *       Aig_UtilStrsav( char * s )             { return s ? strcpy(ALLOC(char, strlen(s)+1), s) : NULL; }
00163 static inline int          Aig_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);                  }
00164 static inline int          Aig_TruthWordNum( int nVars )          { return nVars <= 5 ? 1 : (1 << (nVars - 5));            }
00165 static inline int          Aig_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0;              }
00166 static inline void         Aig_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));                          }
00167 static inline void         Aig_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));                          }
00168 static inline unsigned     Aig_InfoMask( int nVar )               { return (~(unsigned)0) >> (32-nVar);                    }
00169 static inline unsigned     Aig_ObjCutSign( unsigned ObjId )       { return (1 << (ObjId & 31));                            }
00170 static inline int          Aig_WordCountOnes( unsigned uWord )
00171 {
00172     uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
00173     uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
00174     uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
00175     uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
00176     return  (uWord & 0x0000FFFF) + (uWord>>16);
00177 }
00178 
00179 static inline Aig_Obj_t *  Aig_Regular( Aig_Obj_t * p )           { return (Aig_Obj_t *)((unsigned long)(p) & ~01); }
00180 static inline Aig_Obj_t *  Aig_Not( Aig_Obj_t * p )               { return (Aig_Obj_t *)((unsigned long)(p) ^  01); }
00181 static inline Aig_Obj_t *  Aig_NotCond( Aig_Obj_t * p, int c )    { return (Aig_Obj_t *)((unsigned long)(p) ^ (c)); }
00182 static inline int          Aig_IsComplement( Aig_Obj_t * p )      { return (int )(((unsigned long)p) & 01);         }
00183 
00184 static inline int          Aig_ManPiNum( Aig_Man_t * p )          { return p->nObjs[AIG_OBJ_PI];                    }
00185 static inline int          Aig_ManPoNum( Aig_Man_t * p )          { return p->nObjs[AIG_OBJ_PO];                    }
00186 static inline int          Aig_ManBufNum( Aig_Man_t * p )         { return p->nObjs[AIG_OBJ_BUF];                   }
00187 static inline int          Aig_ManAndNum( Aig_Man_t * p )         { return p->nObjs[AIG_OBJ_AND];                   }
00188 static inline int          Aig_ManExorNum( Aig_Man_t * p )        { return p->nObjs[AIG_OBJ_EXOR];                  }
00189 static inline int          Aig_ManLatchNum( Aig_Man_t * p )       { return p->nObjs[AIG_OBJ_LATCH];                 }
00190 static inline int          Aig_ManNodeNum( Aig_Man_t * p )        { return p->nObjs[AIG_OBJ_AND]+p->nObjs[AIG_OBJ_EXOR];   }
00191 static inline int          Aig_ManGetCost( Aig_Man_t * p )        { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; }
00192 static inline int          Aig_ManObjNum( Aig_Man_t * p )         { return p->nCreated - p->nDeleted;               }
00193 static inline int          Aig_ManObjNumMax( Aig_Man_t * p )      { return Vec_PtrSize(p->vObjs);                   }
00194 static inline int          Aig_ManRegNum( Aig_Man_t * p )         { return p->nRegs;                                }
00195 
00196 static inline Aig_Obj_t *  Aig_ManConst0( Aig_Man_t * p )         { return Aig_Not(p->pConst1);                     }
00197 static inline Aig_Obj_t *  Aig_ManConst1( Aig_Man_t * p )         { return p->pConst1;                              }
00198 static inline Aig_Obj_t *  Aig_ManGhost( Aig_Man_t * p )          { return &p->Ghost;                               }
00199 static inline Aig_Obj_t *  Aig_ManPi( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, i);   }
00200 static inline Aig_Obj_t *  Aig_ManPo( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, i);   }
00201 static inline Aig_Obj_t *  Aig_ManLo( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Aig_ManPiNum(p)-Aig_ManRegNum(p)+i);   }
00202 static inline Aig_Obj_t *  Aig_ManLi( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Aig_ManPoNum(p)-Aig_ManRegNum(p)+i);   }
00203 static inline Aig_Obj_t *  Aig_ManObj( Aig_Man_t * p, int i )     { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL;  }
00204 
00205 static inline Aig_Type_t   Aig_ObjType( Aig_Obj_t * pObj )        { return (Aig_Type_t)pObj->Type;       }
00206 static inline int          Aig_ObjIsNone( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_NONE;   }
00207 static inline int          Aig_ObjIsConst1( Aig_Obj_t * pObj )    { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_OBJ_CONST1; }
00208 static inline int          Aig_ObjIsPi( Aig_Obj_t * pObj )        { return pObj->Type == AIG_OBJ_PI;     }
00209 static inline int          Aig_ObjIsPo( Aig_Obj_t * pObj )        { return pObj->Type == AIG_OBJ_PO;     }
00210 static inline int          Aig_ObjIsBuf( Aig_Obj_t * pObj )       { return pObj->Type == AIG_OBJ_BUF;    }
00211 static inline int          Aig_ObjIsAnd( Aig_Obj_t * pObj )       { return pObj->Type == AIG_OBJ_AND;    }
00212 static inline int          Aig_ObjIsExor( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_EXOR;   }
00213 static inline int          Aig_ObjIsLatch( Aig_Obj_t * pObj )     { return pObj->Type == AIG_OBJ_LATCH;  }
00214 static inline int          Aig_ObjIsNode( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR;   }
00215 static inline int          Aig_ObjIsTerm( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_PI  || pObj->Type == AIG_OBJ_PO || pObj->Type == AIG_OBJ_CONST1;   }
00216 static inline int          Aig_ObjIsHash( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR || pObj->Type == AIG_OBJ_LATCH;  }
00217 static inline int          Aig_ObjIsChoice( Aig_Man_t * p, Aig_Obj_t * pObj )    { return p->pEquivs && p->pEquivs[pObj->Id] && pObj->nRefs > 0;                    }
00218 
00219 static inline int          Aig_ObjIsMarkA( Aig_Obj_t * pObj )     { return pObj->fMarkA;  }
00220 static inline void         Aig_ObjSetMarkA( Aig_Obj_t * pObj )    { pObj->fMarkA = 1;     }
00221 static inline void         Aig_ObjClearMarkA( Aig_Obj_t * pObj )  { pObj->fMarkA = 0;     }
00222  
00223 static inline void         Aig_ObjSetTravId( Aig_Obj_t * pObj, int TravId )                { pObj->TravId = TravId;                         }
00224 static inline void         Aig_ObjSetTravIdCurrent( Aig_Man_t * p, Aig_Obj_t * pObj )      { pObj->TravId = p->nTravIds;                    }
00225 static inline void         Aig_ObjSetTravIdPrevious( Aig_Man_t * p, Aig_Obj_t * pObj )     { pObj->TravId = p->nTravIds - 1;                }
00226 static inline int          Aig_ObjIsTravIdCurrent( Aig_Man_t * p, Aig_Obj_t * pObj )       { return (int)(pObj->TravId == p->nTravIds);     }
00227 static inline int          Aig_ObjIsTravIdPrevious( Aig_Man_t * p, Aig_Obj_t * pObj )      { return (int)(pObj->TravId == p->nTravIds - 1); }
00228 
00229 static inline int          Aig_ObjPhase( Aig_Obj_t * pObj )       { return pObj->fPhase;                           }
00230 static inline int          Aig_ObjPhaseReal( Aig_Obj_t * pObj )   { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 1;                              }
00231 static inline int          Aig_ObjRefs( Aig_Obj_t * pObj )        { return pObj->nRefs;                            }
00232 static inline void         Aig_ObjRef( Aig_Obj_t * pObj )         { pObj->nRefs++;                                 }
00233 static inline void         Aig_ObjDeref( Aig_Obj_t * pObj )       { assert( pObj->nRefs > 0 ); pObj->nRefs--;      }
00234 static inline void         Aig_ObjClearRef( Aig_Obj_t * pObj )    { pObj->nRefs = 0;                               }
00235 static inline int          Aig_ObjFaninId0( Aig_Obj_t * pObj )    { return pObj->pFanin0? Aig_Regular(pObj->pFanin0)->Id : -1; }
00236 static inline int          Aig_ObjFaninId1( Aig_Obj_t * pObj )    { return pObj->pFanin1? Aig_Regular(pObj->pFanin1)->Id : -1; }
00237 static inline int          Aig_ObjFaninC0( Aig_Obj_t * pObj )     { return Aig_IsComplement(pObj->pFanin0);        }
00238 static inline int          Aig_ObjFaninC1( Aig_Obj_t * pObj )     { return Aig_IsComplement(pObj->pFanin1);        }
00239 static inline Aig_Obj_t *  Aig_ObjFanin0( Aig_Obj_t * pObj )      { return Aig_Regular(pObj->pFanin0);             }
00240 static inline Aig_Obj_t *  Aig_ObjFanin1( Aig_Obj_t * pObj )      { return Aig_Regular(pObj->pFanin1);             }
00241 static inline Aig_Obj_t *  Aig_ObjChild0( Aig_Obj_t * pObj )      { return pObj->pFanin0;                          }
00242 static inline Aig_Obj_t *  Aig_ObjChild1( Aig_Obj_t * pObj )      { return pObj->pFanin1;                          }
00243 static inline Aig_Obj_t *  Aig_ObjChild0Copy( Aig_Obj_t * pObj )  { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL;  }
00244 static inline Aig_Obj_t *  Aig_ObjChild1Copy( Aig_Obj_t * pObj )  { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL;  }
00245 static inline int          Aig_ObjLevel( Aig_Obj_t * pObj )       { return pObj->Level;                            }
00246 static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
00247 static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj, 0, sizeof(Aig_Obj_t) );                                                             }
00248 static inline Aig_Obj_t *  Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj )  { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } 
00249 static inline Aig_Obj_t *  Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj )    { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; } 
00250 static inline int          Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
00251 { 
00252     if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; 
00253     if ( Aig_ObjFanin1(pObj) == pFanin ) return 1; 
00254     assert(0); return -1; 
00255 }
00256 static inline int          Aig_ObjFanoutC( Aig_Obj_t * pObj, Aig_Obj_t * pFanout )    
00257 { 
00258     if ( Aig_ObjFanin0(pFanout) == pObj ) return Aig_ObjFaninC0(pObj); 
00259     if ( Aig_ObjFanin1(pFanout) == pObj ) return Aig_ObjFaninC1(pObj); 
00260     assert(0); return -1; 
00261 }
00262 
00263 // create the ghost of the new node
00264 static inline Aig_Obj_t *  Aig_ObjCreateGhost( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type )    
00265 {
00266     Aig_Obj_t * pGhost;
00267     assert( Type != AIG_OBJ_AND || !Aig_ObjIsConst1(Aig_Regular(p0)) );
00268     assert( p1 == NULL || !Aig_ObjIsConst1(Aig_Regular(p1)) );
00269     assert( Type == AIG_OBJ_PI || Aig_Regular(p0) != Aig_Regular(p1) );
00270     pGhost = Aig_ManGhost(p);
00271     pGhost->Type = Type;
00272     if ( p1 == NULL || Aig_Regular(p0)->Id < Aig_Regular(p1)->Id )
00273     {
00274         pGhost->pFanin0 = p0;
00275         pGhost->pFanin1 = p1;
00276     }
00277     else
00278     {
00279         pGhost->pFanin0 = p1;
00280         pGhost->pFanin1 = p0;
00281     }
00282     return pGhost;
00283 }
00284 
00285 // internal memory manager
00286 static inline Aig_Obj_t * Aig_ManFetchMemory( Aig_Man_t * p )  
00287 {
00288     extern char * Aig_MmFixedEntryFetch( Aig_MmFixed_t * p );
00289     Aig_Obj_t * pTemp;
00290     pTemp = (Aig_Obj_t *)Aig_MmFixedEntryFetch( p->pMemObjs );
00291     memset( pTemp, 0, sizeof(Aig_Obj_t) ); 
00292     Vec_PtrPush( p->vObjs, pTemp );
00293     pTemp->Id = p->nCreated++;
00294     return pTemp;
00295 }
00296 static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
00297 {
00298     extern void Aig_MmFixedEntryRecycle( Aig_MmFixed_t * p, char * pEntry );
00299     assert( pEntry->nRefs == 0 );
00300     pEntry->Type = AIG_OBJ_NONE; // distinquishes a dead node from a live node
00301     Aig_MmFixedEntryRecycle( p->pMemObjs, (char *)pEntry );
00302     p->nDeleted++;
00303 }
00304 
00305 
00309 
00310 // iterator over the primary inputs
00311 #define Aig_ManForEachPi( p, pObj, i )                                          \
00312     Vec_PtrForEachEntry( p->vPis, pObj, i )
00313 // iterator over the primary outputs
00314 #define Aig_ManForEachPo( p, pObj, i )                                          \
00315     Vec_PtrForEachEntry( p->vPos, pObj, i )
00316 // iterator over the assertions
00317 #define Aig_ManForEachAssert( p, pObj, i )                                      \
00318     Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-p->nAsserts )
00319 // iterator over all objects, including those currently not used
00320 #define Aig_ManForEachObj( p, pObj, i )                                         \
00321     Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
00322 // iterator over all nodes
00323 #define Aig_ManForEachNode( p, pObj, i )                                        \
00324     Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
00325 // iterator over the nodes whose IDs are stored in the array
00326 #define Aig_ManForEachNodeVec( p, vIds, pObj, i )                               \
00327     for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
00328 // iterator over the nodes in the topological order
00329 #define Aig_ManForEachNodeInOrder( p, pObj )                                    \
00330     for ( assert(p->pOrderData), p->iPrev = 0, p->iNext = p->pOrderData[1];     \
00331           p->iNext && (((pObj) = Aig_ManObj(p, p->iNext)), 1);                  \
00332           p->iNext = p->pOrderData[2*p->iPrev+1] )
00333 
00334 // these two procedures are only here for the use inside the iterator
00335 static inline int     Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId )  { assert(ObjId < p->nFansAlloc);  return p->pFanData[5*ObjId];                         }
00336 static inline int     Aig_ObjFanoutNext( Aig_Man_t * p, int iFan )   { assert(iFan/2 < p->nFansAlloc); return p->pFanData[5*(iFan >> 1) + 3 + (iFan & 1)];  }
00337 // iterator over the fanouts
00338 #define Aig_ObjForEachFanout( p, pObj, pFanout, iFan, i )                       \
00339     for ( assert(p->pFanData), i = 0; (i < (int)(pObj)->nRefs) &&               \
00340           (((iFan) = i? Aig_ObjFanoutNext(p, iFan) : Aig_ObjFanout0Int(p, pObj->Id)), 1) && \
00341           (((pFanout) = Aig_ManObj(p, iFan>>1)), 1); i++ )
00342 
00343 
00347 
00348 // iterator over the primary inputs
00349 #define Aig_ManForEachPiSeq( p, pObj, i )                                       \
00350     Vec_PtrForEachEntryStop( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
00351 // iterator over the latch outputs
00352 #define Aig_ManForEachLoSeq( p, pObj, i )                                       \
00353     Vec_PtrForEachEntryStart( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
00354 // iterator over the primary outputs
00355 #define Aig_ManForEachPoSeq( p, pObj, i )                                       \
00356     Vec_PtrForEachEntryStop( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) )
00357 // iterator over the latch inputs
00358 #define Aig_ManForEachLiSeq( p, pObj, i )                                       \
00359     Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) )
00360 // iterator over the latch input and outputs
00361 #define Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, k )                           \
00362     for ( k = 0; (k < Aig_ManRegNum(p)) && (((pObjLi) = Aig_ManLi(p, k)), 1)    \
00363         && (((pObjLo)=Aig_ManLo(p, k)), 1); k++ )
00364 
00368 
00369 /*=== aigCheck.c ========================================================*/
00370 extern int             Aig_ManCheck( Aig_Man_t * p );
00371 extern void            Aig_ManCheckMarkA( Aig_Man_t * p );
00372 extern void            Aig_ManCheckPhase( Aig_Man_t * p );
00373 /*=== aigDfs.c ==========================================================*/
00374 extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p );
00375 extern Vec_Ptr_t *     Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
00376 extern Vec_Ptr_t *     Aig_ManDfsChoices( Aig_Man_t * p );
00377 extern Vec_Ptr_t *     Aig_ManDfsReverse( Aig_Man_t * p );
00378 extern int             Aig_ManLevelNum( Aig_Man_t * p );
00379 extern int             Aig_ManCountLevels( Aig_Man_t * p );
00380 extern int             Aig_DagSize( Aig_Obj_t * pObj );
00381 extern int             Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
00382 extern void            Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
00383 extern Aig_Obj_t *     Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
00384 extern Aig_Obj_t *     Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
00385 extern void            Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes );
00386 extern int             Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper );
00387 /*=== aigFanout.c ==========================================================*/
00388 extern void            Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
00389 extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
00390 extern void            Aig_ManFanoutStart( Aig_Man_t * p );
00391 extern void            Aig_ManFanoutStop( Aig_Man_t * p );
00392 /*=== aigMan.c ==========================================================*/
00393 extern Aig_Man_t *     Aig_ManStart( int nNodesMax );
00394 extern Aig_Man_t *     Aig_ManStartFrom( Aig_Man_t * p );
00395 extern Aig_Obj_t *     Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj );
00396 extern Aig_Man_t *     Aig_ManDup( Aig_Man_t * p, int fOrdered );
00397 extern Aig_Man_t *     Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
00398 extern void            Aig_ManStop( Aig_Man_t * p );
00399 extern int             Aig_ManCleanup( Aig_Man_t * p );
00400 extern void            Aig_ManPrintStats( Aig_Man_t * p );
00401 /*=== aigMem.c ==========================================================*/
00402 extern void            Aig_ManStartMemory( Aig_Man_t * p );
00403 extern void            Aig_ManStopMemory( Aig_Man_t * p );
00404 /*=== aigMffc.c ==========================================================*/
00405 extern int             Aig_NodeRef_rec( Aig_Obj_t * pNode, unsigned LevelMin );
00406 extern int             Aig_NodeDeref_rec( Aig_Obj_t * pNode, unsigned LevelMin );
00407 extern int             Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp );
00408 extern int             Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode );
00409 extern int             Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves );
00410 extern int             Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult );
00411 /*=== aigObj.c ==========================================================*/
00412 extern Aig_Obj_t *     Aig_ObjCreatePi( Aig_Man_t * p );
00413 extern Aig_Obj_t *     Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver );
00414 extern Aig_Obj_t *     Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost );
00415 extern void            Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj_t * pFan1 );
00416 extern void            Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj );
00417 extern void            Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
00418 extern void            Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fFreeTop );
00419 extern void            Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew );
00420 extern void            Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel );
00421 /*=== aigOper.c =========================================================*/
00422 extern Aig_Obj_t *     Aig_IthVar( Aig_Man_t * p, int i );
00423 extern Aig_Obj_t *     Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type );
00424 extern Aig_Obj_t *     Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
00425 extern Aig_Obj_t *     Aig_Latch( Aig_Man_t * p, Aig_Obj_t * pObj, int fInitOne );
00426 extern Aig_Obj_t *     Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
00427 extern Aig_Obj_t *     Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
00428 extern Aig_Obj_t *     Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 );
00429 extern Aig_Obj_t *     Aig_Maj( Aig_Man_t * p, Aig_Obj_t * pA, Aig_Obj_t * pB, Aig_Obj_t * pC );
00430 extern Aig_Obj_t *     Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs );
00431 extern Aig_Obj_t *     Aig_MiterTwo( Aig_Man_t * p, Vec_Ptr_t * vNodes1, Vec_Ptr_t * vNodes2 );
00432 extern Aig_Obj_t *     Aig_CreateAnd( Aig_Man_t * p, int nVars );
00433 extern Aig_Obj_t *     Aig_CreateOr( Aig_Man_t * p, int nVars );
00434 extern Aig_Obj_t *     Aig_CreateExor( Aig_Man_t * p, int nVars );
00435 /*=== aigOrder.c =========================================================*/
00436 extern void            Aig_ManOrderStart( Aig_Man_t * p );
00437 extern void            Aig_ManOrderStop( Aig_Man_t * p );
00438 extern void            Aig_ObjOrderInsert( Aig_Man_t * p, int ObjId );
00439 extern void            Aig_ObjOrderRemove( Aig_Man_t * p, int ObjId );
00440 extern void            Aig_ObjOrderAdvance( Aig_Man_t * p );
00441 /*=== aigPart.c =========================================================*/
00442 extern Vec_Ptr_t *     Aig_ManSupports( Aig_Man_t * pMan );
00443 extern Vec_Ptr_t *     Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
00444 extern Vec_Ptr_t *     Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
00445 extern Aig_Man_t *     Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize );
00446 /*=== aigRepr.c =========================================================*/
00447 extern void            Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
00448 extern void            Aig_ManReprStop( Aig_Man_t * p );
00449 extern void            Aig_ObjCreateRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
00450 extern void            Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
00451 extern Aig_Man_t *     Aig_ManDupRepr( Aig_Man_t * p, int fOrdered );
00452 extern Aig_Man_t *     Aig_ManRehash( Aig_Man_t * p );
00453 extern void            Aig_ManMarkValidChoices( Aig_Man_t * p );
00454 /*=== aigRet.c ========================================================*/
00455 extern Aig_Man_t *     Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
00456 /*=== aigScl.c ==========================================================*/
00457 extern Aig_Man_t *     Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
00458 extern int             Aig_ManSeqCleanup( Aig_Man_t * p );
00459 extern int             Aig_ManCountMergeRegs( Aig_Man_t * p );
00460 extern Aig_Man_t *     Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
00461 /*=== aigSeq.c ========================================================*/
00462 extern int             Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
00463 /*=== aigShow.c ========================================================*/
00464 extern void            Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
00465 /*=== aigTable.c ========================================================*/
00466 extern Aig_Obj_t *     Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost );
00467 extern Aig_Obj_t *     Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * pFanin1 );
00468 extern void            Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj );
00469 extern void            Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
00470 extern int             Aig_TableCountEntries( Aig_Man_t * p );
00471 extern void            Aig_TableProfile( Aig_Man_t * p );
00472 /*=== aigTiming.c ========================================================*/
00473 extern void            Aig_ObjClearReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj );
00474 extern int             Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj );
00475 extern void            Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease );
00476 extern void            Aig_ManStopReverseLevels( Aig_Man_t * p );
00477 extern void            Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
00478 extern void            Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
00479 extern void            Aig_ManVerifyLevel( Aig_Man_t * p );
00480 extern void            Aig_ManVerifyReverseLevel( Aig_Man_t * p );
00481 /*=== aigTruth.c ========================================================*/
00482 extern unsigned *      Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore );
00483 /*=== aigTsim.c ========================================================*/
00484 extern Aig_Man_t *     Aig_ManConstReduce( Aig_Man_t * p, int fVerbose );
00485 /*=== aigUtil.c =========================================================*/
00486 extern unsigned        Aig_PrimeCudd( unsigned p );
00487 extern void            Aig_ManIncrementTravId( Aig_Man_t * p );
00488 extern int             Aig_ManLevels( Aig_Man_t * p );
00489 extern void            Aig_ManResetRefs( Aig_Man_t * p );
00490 extern void            Aig_ManCleanMarkA( Aig_Man_t * p );
00491 extern void            Aig_ManCleanMarkB( Aig_Man_t * p );
00492 extern void            Aig_ManCleanData( Aig_Man_t * p );
00493 extern void            Aig_ObjCleanData_rec( Aig_Obj_t * pObj );
00494 extern void            Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper );
00495 extern int             Aig_ObjIsMuxType( Aig_Obj_t * pObj );
00496 extern int             Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 );
00497 extern Aig_Obj_t *     Aig_ObjRecognizeMux( Aig_Obj_t * pObj, Aig_Obj_t ** ppObjT, Aig_Obj_t ** ppObjE );
00498 extern Aig_Obj_t *     Aig_ObjReal_rec( Aig_Obj_t * pObj );
00499 extern void            Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
00500 extern void            Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
00501 extern void            Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
00502 extern void            Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
00503 extern void            Aig_ManDump( Aig_Man_t * p );
00504 extern void            Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
00505 extern void            Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
00506 /*=== aigWin.c =========================================================*/
00507 extern void            Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
00508  
00509 /*=== aigMem.c ===========================================================*/
00510 // fixed-size-block memory manager
00511 extern Aig_MmFixed_t * Aig_MmFixedStart( int nEntrySize, int nEntriesMax );
00512 extern void            Aig_MmFixedStop( Aig_MmFixed_t * p, int fVerbose );
00513 extern char *          Aig_MmFixedEntryFetch( Aig_MmFixed_t * p );
00514 extern void            Aig_MmFixedEntryRecycle( Aig_MmFixed_t * p, char * pEntry );
00515 extern void            Aig_MmFixedRestart( Aig_MmFixed_t * p );
00516 extern int             Aig_MmFixedReadMemUsage( Aig_MmFixed_t * p );
00517 extern int             Aig_MmFixedReadMaxEntriesUsed( Aig_MmFixed_t * p );
00518 // flexible-size-block memory manager
00519 extern Aig_MmFlex_t *  Aig_MmFlexStart();
00520 extern void            Aig_MmFlexStop( Aig_MmFlex_t * p, int fVerbose );
00521 extern char *          Aig_MmFlexEntryFetch( Aig_MmFlex_t * p, int nBytes );
00522 extern void            Aig_MmFlexRestart( Aig_MmFlex_t * p );
00523 extern int             Aig_MmFlexReadMemUsage( Aig_MmFlex_t * p );
00524 // hierarchical memory manager
00525 extern Aig_MmStep_t *  Aig_MmStepStart( int nSteps );
00526 extern void            Aig_MmStepStop( Aig_MmStep_t * p, int fVerbose );
00527 extern char *          Aig_MmStepEntryFetch( Aig_MmStep_t * p, int nBytes );
00528 extern void            Aig_MmStepEntryRecycle( Aig_MmStep_t * p, char * pEntry, int nBytes );
00529 extern int             Aig_MmStepReadMemUsage( Aig_MmStep_t * p );
00530 
00531 /*=== aigTime.c ===========================================================*/
00532 extern Aig_TMan_t *    Aig_TManStart( int nPis, int nPos );
00533 extern void            Aig_TManStop( Aig_TMan_t * p );
00534 extern void            Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes );
00535 extern void            Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay );
00536 extern void            Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay );
00537 extern void            Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay );
00538 extern void            Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay );
00539 extern void            Aig_TManIncrementTravId( Aig_TMan_t * p );
00540 extern float           Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi );
00541 extern float           Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo );
00542 
00543 
00544 #ifdef __cplusplus
00545 }
00546 #endif
00547 
00548 #endif
00549 
00553