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

00001 
00021 #ifndef __IVY_H__
00022 #define __IVY_H__
00023 
00024 #ifdef __cplusplus
00025 extern "C" {
00026 #endif 
00027 
00031 
00032 #include <stdio.h>
00033 #include "extra.h"
00034 #include "vec.h"
00035 
00039 
00043 
00044 typedef struct Ivy_Man_t_            Ivy_Man_t;
00045 typedef struct Ivy_Obj_t_            Ivy_Obj_t;
00046 typedef int                          Ivy_Edge_t;
00047 typedef struct Ivy_FraigParams_t_    Ivy_FraigParams_t;
00048 
00049 // object types
00050 typedef enum { 
00051     IVY_NONE,                        // 0: non-existent object
00052     IVY_PI,                          // 1: primary input (and constant 1 node)
00053     IVY_PO,                          // 2: primary output
00054     IVY_ASSERT,                      // 3: assertion
00055     IVY_LATCH,                       // 4: sequential element
00056     IVY_AND,                         // 5: AND node
00057     IVY_EXOR,                        // 6: EXOR node
00058     IVY_BUF,                         // 7: buffer (temporary)
00059     IVY_VOID                         // 8: unused object
00060 } Ivy_Type_t;
00061 
00062 // latch initial values
00063 typedef enum { 
00064     IVY_INIT_NONE,                   // 0: not a latch
00065     IVY_INIT_0,                      // 1: zero
00066     IVY_INIT_1,                      // 2: one
00067     IVY_INIT_DC                      // 3: don't-care
00068 } Ivy_Init_t;
00069 
00070 // the AIG node
00071 struct Ivy_Obj_t_  // 24 bytes (32-bit) or 32 bytes (64-bit)   // 10 words - 16 words
00072 {
00073     int              Id;             // integer ID
00074     int              TravId;         // traversal ID
00075     unsigned         Type     :  4;  // object type
00076     unsigned         fMarkA   :  1;  // multipurpose mask
00077     unsigned         fMarkB   :  1;  // multipurpose mask
00078     unsigned         fExFan   :  1;  // set to 1 if last fanout added is EXOR
00079     unsigned         fPhase   :  1;  // value under 000...0 pattern
00080     unsigned         fFailTfo :  1;  // the TFO of the failed node
00081     unsigned         Init     :  2;  // latch initial value
00082     unsigned         Level    : 21;  // logic level
00083     int              nRefs;          // reference counter
00084     Ivy_Obj_t *      pFanin0;        // fanin
00085     Ivy_Obj_t *      pFanin1;        // fanin
00086     Ivy_Obj_t *      pFanout;        // fanout
00087     Ivy_Obj_t *      pNextFan0;      // next fanout of the first fanin
00088     Ivy_Obj_t *      pNextFan1;      // next fanout of the second fanin
00089     Ivy_Obj_t *      pPrevFan0;      // prev fanout of the first fanin
00090     Ivy_Obj_t *      pPrevFan1;      // prev fanout of the second fanin
00091     Ivy_Obj_t *      pEquiv;         // equivalent node
00092 };
00093 
00094 // the AIG manager
00095 struct Ivy_Man_t_
00096 {
00097     // AIG nodes
00098     Vec_Ptr_t *      vPis;           // the array of PIs
00099     Vec_Ptr_t *      vPos;           // the array of POs
00100     Vec_Ptr_t *      vBufs;          // the array of buffers
00101     Vec_Ptr_t *      vObjs;          // the array of objects
00102     Ivy_Obj_t *      pConst1;        // the constant 1 node
00103     Ivy_Obj_t        Ghost;          // the ghost node
00104     // AIG node counters
00105     int              nObjs[IVY_VOID];// the number of objects by type
00106     int              nCreated;       // the number of created objects
00107     int              nDeleted;       // the number of deleted objects
00108     // stuctural hash table
00109     int *            pTable;         // structural hash table
00110     int              nTableSize;     // structural hash table size
00111     // various data members
00112     int              fCatchExor;     // set to 1 to detect EXORs
00113     int              nTravIds;       // the traversal ID
00114     int              nLevelMax;      // the maximum level
00115     Vec_Int_t *      vRequired;      // required times
00116     int              fFanout;        // fanout is allocated
00117     void *           pData;          // the temporary data
00118     void *           pCopy;          // the temporary data
00119     Ivy_Man_t *      pHaig;          // history AIG if present
00120     int              nClassesSkip;   // the number of skipped classes
00121     // memory management
00122     Vec_Ptr_t *      vChunks;        // allocated memory pieces
00123     Vec_Ptr_t *      vPages;         // memory pages used by nodes
00124     Ivy_Obj_t *      pListFree;      // the list of free nodes 
00125     // timing statistics
00126     int              time1;
00127     int              time2;
00128 };
00129 
00130 struct Ivy_FraigParams_t_
00131 {
00132     int              nSimWords;         // the number of words in the simulation info
00133     double           dSimSatur;         // the ratio of refined classes when saturation is reached
00134     int              fPatScores;        // enables simulation pattern scoring
00135     int              MaxScore;          // max score after which resimulation is used
00136     double           dActConeRatio;     // the ratio of cone to be bumped
00137     double           dActConeBumpMax;   // the largest bump in activity
00138     int              fProve;            // prove the miter outputs
00139     int              fVerbose;          // verbose output
00140     int              fDoSparse;         // skip sparse functions
00141     int              nBTLimitNode;      // conflict limit at a node
00142     int              nBTLimitMiter;     // conflict limit at an output
00143 //    int              nBTLimitGlobal;    // conflict limit global
00144 //    int              nInsLimitNode;     // inspection limit at a node
00145 //    int              nInsLimitMiter;    // inspection limit at an output
00146 //    int              nInsLimitGlobal;   // inspection limit global
00147 };
00148 
00149 
00150 #define IVY_CUT_LIMIT     256
00151 #define IVY_CUT_INPUT       6
00152 
00153 typedef struct Ivy_Cut_t_ Ivy_Cut_t;
00154 struct Ivy_Cut_t_
00155 {
00156     int         nLatches;
00157     short       nSize;
00158     short       nSizeMax;
00159     int         pArray[IVY_CUT_INPUT];
00160     unsigned    uHash;
00161 };
00162 
00163 typedef struct Ivy_Store_t_ Ivy_Store_t;
00164 struct Ivy_Store_t_
00165 {
00166     int         nCuts;
00167     int         nCutsM;
00168     int         nCutsMax;
00169     int         fSatur;
00170     Ivy_Cut_t   pCuts[IVY_CUT_LIMIT]; // storage for cuts
00171 };
00172 
00173 #define IVY_LEAF_MASK     255
00174 #define IVY_LEAF_BITS       8
00175 
00179 
00180 #define IVY_MIN(a,b)       (((a) < (b))? (a) : (b))
00181 #define IVY_MAX(a,b)       (((a) > (b))? (a) : (b))
00182 
00183 static inline int          Ivy_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);           }
00184 static inline int          Ivy_TruthWordNum( int nVars )          { return nVars <= 5 ? 1 : (1 << (nVars - 5));     }
00185 static inline int          Ivy_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0;       }
00186 static inline void         Ivy_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));                   }
00187 static inline void         Ivy_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));                   }
00188 
00189 static inline Ivy_Obj_t *  Ivy_Regular( Ivy_Obj_t * p )           { return (Ivy_Obj_t *)((unsigned long)(p) & ~01);      }
00190 static inline Ivy_Obj_t *  Ivy_Not( Ivy_Obj_t * p )               { return (Ivy_Obj_t *)((unsigned long)(p) ^  01);      }
00191 static inline Ivy_Obj_t *  Ivy_NotCond( Ivy_Obj_t * p, int c )    { return (Ivy_Obj_t *)((unsigned long)(p) ^ (c));      }
00192 static inline int          Ivy_IsComplement( Ivy_Obj_t * p )      { return (int )(((unsigned long)p) & 01);              }
00193 
00194 static inline Ivy_Obj_t *  Ivy_ManConst0( Ivy_Man_t * p )         { return Ivy_Not(p->pConst1);                     }
00195 static inline Ivy_Obj_t *  Ivy_ManConst1( Ivy_Man_t * p )         { return p->pConst1;                              }
00196 static inline Ivy_Obj_t *  Ivy_ManGhost( Ivy_Man_t * p )          { return &p->Ghost;                               }
00197 static inline Ivy_Obj_t *  Ivy_ManPi( Ivy_Man_t * p, int i )      { return (Ivy_Obj_t *)Vec_PtrEntry(p->vPis, i);   }
00198 static inline Ivy_Obj_t *  Ivy_ManPo( Ivy_Man_t * p, int i )      { return (Ivy_Obj_t *)Vec_PtrEntry(p->vPos, i);   }
00199 static inline Ivy_Obj_t *  Ivy_ManObj( Ivy_Man_t * p, int i )     { return (Ivy_Obj_t *)Vec_PtrEntry(p->vObjs, i);  }
00200 
00201 static inline Ivy_Edge_t   Ivy_EdgeCreate( int Id, int fCompl )            { return (Id << 1) | fCompl;             }
00202 static inline int          Ivy_EdgeId( Ivy_Edge_t Edge )                   { return Edge >> 1;                      }
00203 static inline int          Ivy_EdgeIsComplement( Ivy_Edge_t Edge )         { return Edge & 1;                       }
00204 static inline Ivy_Edge_t   Ivy_EdgeRegular( Ivy_Edge_t Edge )              { return (Edge >> 1) << 1;               }
00205 static inline Ivy_Edge_t   Ivy_EdgeNot( Ivy_Edge_t Edge )                  { return Edge ^ 1;                       }
00206 static inline Ivy_Edge_t   Ivy_EdgeNotCond( Ivy_Edge_t Edge, int fCond )   { return Edge ^ fCond;                   }
00207 static inline Ivy_Edge_t   Ivy_EdgeFromNode( Ivy_Obj_t * pNode )           { return Ivy_EdgeCreate( Ivy_Regular(pNode)->Id, Ivy_IsComplement(pNode) );          }
00208 static inline Ivy_Obj_t *  Ivy_EdgeToNode( Ivy_Man_t * p, Ivy_Edge_t Edge ){ return Ivy_NotCond( Ivy_ManObj(p, Ivy_EdgeId(Edge)), Ivy_EdgeIsComplement(Edge) ); }
00209 
00210 static inline int          Ivy_LeafCreate( int Id, int Lat )      { return (Id << IVY_LEAF_BITS) | Lat;         }
00211 static inline int          Ivy_LeafId( int Leaf )                 { return Leaf >> IVY_LEAF_BITS;               }
00212 static inline int          Ivy_LeafLat( int Leaf )                { return Leaf & IVY_LEAF_MASK;                }
00213 
00214 static inline int          Ivy_ManPiNum( Ivy_Man_t * p )          { return p->nObjs[IVY_PI];                    }
00215 static inline int          Ivy_ManPoNum( Ivy_Man_t * p )          { return p->nObjs[IVY_PO];                    }
00216 static inline int          Ivy_ManAssertNum( Ivy_Man_t * p )      { return p->nObjs[IVY_ASSERT];                }
00217 static inline int          Ivy_ManLatchNum( Ivy_Man_t * p )       { return p->nObjs[IVY_LATCH];                 }
00218 static inline int          Ivy_ManAndNum( Ivy_Man_t * p )         { return p->nObjs[IVY_AND];                   }
00219 static inline int          Ivy_ManExorNum( Ivy_Man_t * p )        { return p->nObjs[IVY_EXOR];                  }
00220 static inline int          Ivy_ManBufNum( Ivy_Man_t * p )         { return p->nObjs[IVY_BUF];                   }
00221 static inline int          Ivy_ManObjNum( Ivy_Man_t * p )         { return p->nCreated - p->nDeleted;           }
00222 static inline int          Ivy_ManObjIdMax( Ivy_Man_t * p )       { return Vec_PtrSize(p->vObjs)-1;             }
00223 static inline int          Ivy_ManNodeNum( Ivy_Man_t * p )        { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR];}
00224 static inline int          Ivy_ManHashObjNum( Ivy_Man_t * p )     { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]+p->nObjs[IVY_LATCH];     }
00225 static inline int          Ivy_ManGetCost( Ivy_Man_t * p )        { return p->nObjs[IVY_AND]+3*p->nObjs[IVY_EXOR]+8*p->nObjs[IVY_LATCH]; }
00226 
00227 static inline Ivy_Type_t   Ivy_ObjType( Ivy_Obj_t * pObj )        { return pObj->Type;               }
00228 static inline Ivy_Init_t   Ivy_ObjInit( Ivy_Obj_t * pObj )        { return pObj->Init;               }
00229 static inline int          Ivy_ObjIsConst1( Ivy_Obj_t * pObj )    { return pObj->Id == 0;            }
00230 static inline int          Ivy_ObjIsGhost( Ivy_Obj_t * pObj )     { return pObj->Id < 0;             }
00231 static inline int          Ivy_ObjIsNone( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_NONE;   }
00232 static inline int          Ivy_ObjIsPi( Ivy_Obj_t * pObj )        { return pObj->Type == IVY_PI;     }
00233 static inline int          Ivy_ObjIsPo( Ivy_Obj_t * pObj )        { return pObj->Type == IVY_PO;     }
00234 static inline int          Ivy_ObjIsCi( Ivy_Obj_t * pObj )        { return pObj->Type == IVY_PI || pObj->Type == IVY_LATCH; }
00235 static inline int          Ivy_ObjIsCo( Ivy_Obj_t * pObj )        { return pObj->Type == IVY_PO || pObj->Type == IVY_LATCH; }
00236 static inline int          Ivy_ObjIsAssert( Ivy_Obj_t * pObj )    { return pObj->Type == IVY_ASSERT; }
00237 static inline int          Ivy_ObjIsLatch( Ivy_Obj_t * pObj )     { return pObj->Type == IVY_LATCH;  }
00238 static inline int          Ivy_ObjIsAnd( Ivy_Obj_t * pObj )       { return pObj->Type == IVY_AND;    }
00239 static inline int          Ivy_ObjIsExor( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_EXOR;   }
00240 static inline int          Ivy_ObjIsBuf( Ivy_Obj_t * pObj )       { return pObj->Type == IVY_BUF;    }
00241 static inline int          Ivy_ObjIsNode( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; }
00242 static inline int          Ivy_ObjIsTerm( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_PI  || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; }
00243 static inline int          Ivy_ObjIsHash( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; }
00244 static inline int          Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj )  { return pObj->Type == IVY_PO  || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; }
00245 
00246 static inline int          Ivy_ObjIsMarkA( Ivy_Obj_t * pObj )     { return pObj->fMarkA;  }
00247 static inline void         Ivy_ObjSetMarkA( Ivy_Obj_t * pObj )    { pObj->fMarkA = 1;     }
00248 static inline void         Ivy_ObjClearMarkA( Ivy_Obj_t * pObj )  { pObj->fMarkA = 0;     }
00249  
00250 static inline void         Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId )                { pObj->TravId = TravId;                               }
00251 static inline void         Ivy_ObjSetTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj )      { pObj->TravId = p->nTravIds;                          }
00252 static inline void         Ivy_ObjSetTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj )     { pObj->TravId = p->nTravIds - 1;                      }
00253 static inline int          Ivy_ObjIsTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj )       { return (int )((int)pObj->TravId == p->nTravIds);     }
00254 static inline int          Ivy_ObjIsTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj )      { return (int )((int)pObj->TravId == p->nTravIds - 1); }
00255 
00256 static inline int          Ivy_ObjId( Ivy_Obj_t * pObj )          { return pObj->Id;                               }
00257 static inline int          Ivy_ObjTravId( Ivy_Obj_t * pObj )      { return pObj->TravId;                           }
00258 static inline int          Ivy_ObjPhase( Ivy_Obj_t * pObj )       { return pObj->fPhase;                           }
00259 static inline int          Ivy_ObjExorFanout( Ivy_Obj_t * pObj )  { return pObj->fExFan;                           }
00260 static inline int          Ivy_ObjRefs( Ivy_Obj_t * pObj )        { return pObj->nRefs;                            }
00261 static inline void         Ivy_ObjRefsInc( Ivy_Obj_t * pObj )     { pObj->nRefs++;                                 }
00262 static inline void         Ivy_ObjRefsDec( Ivy_Obj_t * pObj )     { assert( pObj->nRefs > 0 ); pObj->nRefs--;      }
00263 static inline int          Ivy_ObjFaninId0( Ivy_Obj_t * pObj )    { return pObj->pFanin0? Ivy_ObjId(Ivy_Regular(pObj->pFanin0)) : 0; }
00264 static inline int          Ivy_ObjFaninId1( Ivy_Obj_t * pObj )    { return pObj->pFanin1? Ivy_ObjId(Ivy_Regular(pObj->pFanin1)) : 0; }
00265 static inline int          Ivy_ObjFaninC0( Ivy_Obj_t * pObj )     { return Ivy_IsComplement(pObj->pFanin0);        }
00266 static inline int          Ivy_ObjFaninC1( Ivy_Obj_t * pObj )     { return Ivy_IsComplement(pObj->pFanin1);        }
00267 static inline Ivy_Obj_t *  Ivy_ObjFanin0( Ivy_Obj_t * pObj )      { return Ivy_Regular(pObj->pFanin0);             }
00268 static inline Ivy_Obj_t *  Ivy_ObjFanin1( Ivy_Obj_t * pObj )      { return Ivy_Regular(pObj->pFanin1);             }
00269 static inline Ivy_Obj_t *  Ivy_ObjChild0( Ivy_Obj_t * pObj )      { return pObj->pFanin0;                          }
00270 static inline Ivy_Obj_t *  Ivy_ObjChild1( Ivy_Obj_t * pObj )      { return pObj->pFanin1;                          }
00271 static inline Ivy_Obj_t *  Ivy_ObjChild0Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin0(pObj)? Ivy_NotCond(Ivy_ObjFanin0(pObj)->pEquiv, Ivy_ObjFaninC0(pObj)) : NULL;  }
00272 static inline Ivy_Obj_t *  Ivy_ObjChild1Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin1(pObj)? Ivy_NotCond(Ivy_ObjFanin1(pObj)->pEquiv, Ivy_ObjFaninC1(pObj)) : NULL;  }
00273 static inline Ivy_Obj_t *  Ivy_ObjEquiv( Ivy_Obj_t * pObj )       { return Ivy_Regular(pObj)->pEquiv? Ivy_NotCond(Ivy_Regular(pObj)->pEquiv, Ivy_IsComplement(pObj)) : NULL; }
00274 static inline int          Ivy_ObjLevel( Ivy_Obj_t * pObj )       { return pObj->Level;                            }
00275 static inline int          Ivy_ObjLevelNew( Ivy_Obj_t * pObj )    { return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level);       }
00276 static inline int          Ivy_ObjFaninPhase( Ivy_Obj_t * pObj )  { return Ivy_IsComplement(pObj)? !Ivy_Regular(pObj)->fPhase : pObj->fPhase; }
00277 
00278 static inline void         Ivy_ObjClean( Ivy_Obj_t * pObj )       
00279 { 
00280     int IdSaved = pObj->Id; 
00281     memset( pObj, 0, sizeof(Ivy_Obj_t) ); 
00282     pObj->Id = IdSaved; 
00283 }
00284 static inline void         Ivy_ObjOverwrite( Ivy_Obj_t * pBase, Ivy_Obj_t * pData )   
00285 { 
00286     int IdSaved = pBase->Id; 
00287     memcpy( pBase, pData, sizeof(Ivy_Obj_t) ); 
00288     pBase->Id = IdSaved;         
00289 }
00290 static inline int          Ivy_ObjWhatFanin( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin )    
00291 { 
00292     if ( Ivy_ObjFanin0(pObj) == pFanin ) return 0; 
00293     if ( Ivy_ObjFanin1(pObj) == pFanin ) return 1; 
00294     assert(0); return -1; 
00295 }
00296 static inline int          Ivy_ObjFanoutC( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )    
00297 { 
00298     if ( Ivy_ObjFanin0(pFanout) == pObj ) return Ivy_ObjFaninC0(pObj); 
00299     if ( Ivy_ObjFanin1(pFanout) == pObj ) return Ivy_ObjFaninC1(pObj); 
00300     assert(0); return -1; 
00301 }
00302 
00303 // create the ghost of the new node
00304 static inline Ivy_Obj_t *  Ivy_ObjCreateGhost( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init )    
00305 {
00306     Ivy_Obj_t * pGhost, * pTemp;
00307     assert( Type != IVY_AND || !Ivy_ObjIsConst1(Ivy_Regular(p0)) );
00308     assert( p1 == NULL || !Ivy_ObjIsConst1(Ivy_Regular(p1)) );
00309     assert( Type == IVY_PI || Ivy_Regular(p0) != Ivy_Regular(p1) );
00310     assert( Type != IVY_LATCH || !Ivy_IsComplement(p0) );
00311 //    assert( p1 == NULL || (!Ivy_ObjIsLatch(Ivy_Regular(p0)) || !Ivy_ObjIsLatch(Ivy_Regular(p1))) );
00312     pGhost = Ivy_ManGhost(p);
00313     pGhost->Type = Type;
00314     pGhost->Init = Init;
00315     pGhost->pFanin0 = p0;
00316     pGhost->pFanin1 = p1;
00317     if ( p1 && Ivy_ObjFaninId0(pGhost) > Ivy_ObjFaninId1(pGhost) )
00318         pTemp = pGhost->pFanin0, pGhost->pFanin0 = pGhost->pFanin1, pGhost->pFanin1 = pTemp;
00319     return pGhost;
00320 }
00321 
00322 // get the complemented initial state
00323 static Ivy_Init_t Ivy_InitNotCond( Ivy_Init_t Init, int fCompl )
00324 {
00325     assert( Init != IVY_INIT_NONE );
00326     if ( fCompl == 0 )
00327         return Init;
00328     if ( Init == IVY_INIT_0 )
00329         return IVY_INIT_1;
00330     if ( Init == IVY_INIT_1 )
00331         return IVY_INIT_0;
00332     return IVY_INIT_DC;
00333 }
00334 
00335 // get the initial state after forward retiming over AND gate
00336 static Ivy_Init_t Ivy_InitAnd( Ivy_Init_t InitA, Ivy_Init_t InitB )
00337 {
00338     assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE );
00339     if ( InitA == IVY_INIT_0 || InitB == IVY_INIT_0 )
00340         return IVY_INIT_0;
00341     if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC )
00342         return IVY_INIT_DC;
00343     return IVY_INIT_1;
00344 }
00345 
00346 // get the initial state after forward retiming over EXOR gate
00347 static Ivy_Init_t Ivy_InitExor( Ivy_Init_t InitA, Ivy_Init_t InitB )
00348 {
00349     assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE );
00350     if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC )
00351         return IVY_INIT_DC;
00352     if ( InitA == IVY_INIT_0 && InitB == IVY_INIT_1 )
00353         return IVY_INIT_1;
00354     if ( InitA == IVY_INIT_1 && InitB == IVY_INIT_0 )
00355         return IVY_INIT_1;
00356     return IVY_INIT_0;
00357 }
00358 
00359 // internal memory manager
00360 static inline Ivy_Obj_t * Ivy_ManFetchMemory( Ivy_Man_t * p )  
00361 { 
00362     extern void Ivy_ManAddMemory( Ivy_Man_t * p );
00363     Ivy_Obj_t * pTemp;
00364     if ( p->pListFree == NULL )
00365         Ivy_ManAddMemory( p );
00366     pTemp = p->pListFree;
00367     p->pListFree = *((Ivy_Obj_t **)pTemp);
00368     memset( pTemp, 0, sizeof(Ivy_Obj_t) ); 
00369     return pTemp;
00370 }
00371 static inline void Ivy_ManRecycleMemory( Ivy_Man_t * p, Ivy_Obj_t * pEntry )
00372 {
00373     pEntry->Type = IVY_NONE; // distinquishes dead node from live node
00374     *((Ivy_Obj_t **)pEntry) = p->pListFree;
00375     p->pListFree = pEntry;
00376 }
00377 
00378 
00382 
00383 // iterator over the primary inputs
00384 #define Ivy_ManForEachPi( p, pObj, i )                                          \
00385     Vec_PtrForEachEntry( p->vPis, pObj, i )
00386 // iterator over the primary outputs
00387 #define Ivy_ManForEachPo( p, pObj, i )                                          \
00388     Vec_PtrForEachEntry( p->vPos, pObj, i )
00389 // iterator over all objects, including those currently not used
00390 #define Ivy_ManForEachObj( p, pObj, i )                                         \
00391     Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
00392 // iterator over the combinational inputs
00393 #define Ivy_ManForEachCi( p, pObj, i )                                          \
00394     Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCi(pObj) ) {} else
00395 // iterator over the combinational outputs
00396 #define Ivy_ManForEachCo( p, pObj, i )                                          \
00397     Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCo(pObj) ) {} else
00398 // iterator over logic nodes (AND and EXOR gates)
00399 #define Ivy_ManForEachNode( p, pObj, i )                                        \
00400     Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsNode(pObj) ) {} else
00401 // iterator over logic latches
00402 #define Ivy_ManForEachLatch( p, pObj, i )                                       \
00403     Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsLatch(pObj) ) {} else
00404 // iterator over the nodes whose IDs are stored in the array
00405 #define Ivy_ManForEachNodeVec( p, vIds, pObj, i )                               \
00406     for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Ivy_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
00407 // iterator over the fanouts of an object
00408 #define Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, i )                     \
00409     for ( i = 0, Ivy_ObjCollectFanouts(p, pObj, vArray);                        \
00410           i < Vec_PtrSize(vArray) && ((pFanout) = Vec_PtrEntry(vArray,i)); i++ )
00411 
00415 
00416 /*=== ivyBalance.c ========================================================*/
00417 extern Ivy_Man_t *     Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel );
00418 extern Ivy_Obj_t *     Ivy_NodeBalanceBuildSuper( Ivy_Man_t * p, Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel );
00419 /*=== ivyCanon.c ========================================================*/
00420 extern Ivy_Obj_t *     Ivy_CanonAnd( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
00421 extern Ivy_Obj_t *     Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
00422 extern Ivy_Obj_t *     Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init );
00423 /*=== ivyCheck.c ========================================================*/
00424 extern int             Ivy_ManCheck( Ivy_Man_t * p );
00425 extern int             Ivy_ManCheckFanoutNums( Ivy_Man_t * p );
00426 extern int             Ivy_ManCheckFanouts( Ivy_Man_t * p );
00427 extern int             Ivy_ManCheckChoices( Ivy_Man_t * p );
00428 /*=== ivyCut.c ==========================================================*/
00429 extern void            Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize );
00430 extern Ivy_Store_t *   Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves );
00431 /*=== ivyDfs.c ==========================================================*/
00432 extern Vec_Int_t *     Ivy_ManDfs( Ivy_Man_t * p );
00433 extern Vec_Int_t *     Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches );
00434 extern void            Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone );
00435 extern Vec_Vec_t *     Ivy_ManLevelize( Ivy_Man_t * p );
00436 extern Vec_Int_t *     Ivy_ManRequiredLevels( Ivy_Man_t * p );
00437 extern int             Ivy_ManIsAcyclic( Ivy_Man_t * p );
00438 extern int             Ivy_ManSetLevels( Ivy_Man_t * p, int fHaig );
00439 /*=== ivyDsd.c ==========================================================*/
00440 extern int             Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree );
00441 extern void            Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree );
00442 extern unsigned        Ivy_TruthDsdCompute( Vec_Int_t * vTree );
00443 extern void            Ivy_TruthDsdComputePrint( unsigned uTruth );
00444 extern Ivy_Obj_t *     Ivy_ManDsdConstruct( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vTree );
00445 /*=== ivyFanout.c ==========================================================*/
00446 extern void            Ivy_ManStartFanout( Ivy_Man_t * p );
00447 extern void            Ivy_ManStopFanout( Ivy_Man_t * p );
00448 extern void            Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout );
00449 extern void            Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout );
00450 extern void            Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew );
00451 extern void            Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vArray );
00452 extern Ivy_Obj_t *     Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
00453 extern int             Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj );
00454 /*=== ivyFastMap.c =============================================================*/
00455 extern void            Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbose );
00456 extern void            Ivy_FastMapStop( Ivy_Man_t * pAig );
00457 extern void            Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves );
00458 extern void            Ivy_FastMapReverseLevel( Ivy_Man_t * pAig );
00459 /*=== ivyFraig.c ==========================================================*/
00460 extern int             Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars );
00461 extern Ivy_Man_t *     Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
00462 extern Ivy_Man_t *     Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
00463 extern void            Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams );
00464 /*=== ivyHaig.c ==========================================================*/
00465 extern void            Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose );
00466 extern void            Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew );
00467 extern void            Ivy_ManHaigStop( Ivy_Man_t * p );
00468 extern void            Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose );
00469 extern void            Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj );
00470 extern void            Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew );
00471 extern void            Ivy_ManHaigSimulate( Ivy_Man_t * p );
00472 /*=== ivyMan.c ==========================================================*/
00473 extern Ivy_Man_t *     Ivy_ManStart();
00474 extern Ivy_Man_t *     Ivy_ManStartFrom( Ivy_Man_t * p );
00475 extern Ivy_Man_t *     Ivy_ManDup( Ivy_Man_t * p );
00476 extern Ivy_Man_t *     Ivy_ManFrames( Ivy_Man_t * pMan, int nLatches, int nFrames, int fInit, Vec_Ptr_t ** pvMapping );
00477 extern void            Ivy_ManStop( Ivy_Man_t * p );
00478 extern int             Ivy_ManCleanup( Ivy_Man_t * p );
00479 extern int             Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel );
00480 extern void            Ivy_ManPrintStats( Ivy_Man_t * p );
00481 extern void            Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits );
00482 /*=== ivyMem.c ==========================================================*/
00483 extern void            Ivy_ManStartMemory( Ivy_Man_t * p );
00484 extern void            Ivy_ManStopMemory( Ivy_Man_t * p );
00485 /*=== ivyMulti.c ==========================================================*/
00486 extern Ivy_Obj_t *     Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
00487 extern Ivy_Obj_t *     Ivy_Multi1( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
00488 extern Ivy_Obj_t *     Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type );
00489 extern Ivy_Obj_t *     Ivy_MultiBalance_rec( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
00490 extern int             Ivy_MultiPlus( Ivy_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSol );
00491 /*=== ivyObj.c ==========================================================*/
00492 extern Ivy_Obj_t *     Ivy_ObjCreatePi( Ivy_Man_t * p );
00493 extern Ivy_Obj_t *     Ivy_ObjCreatePo( Ivy_Man_t * p, Ivy_Obj_t * pDriver );
00494 extern Ivy_Obj_t *     Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost );
00495 extern void            Ivy_ObjConnect( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFan0, Ivy_Obj_t * pFan1 );
00496 extern void            Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj );
00497 extern void            Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew );
00498 extern void            Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop );
00499 extern void            Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop );
00500 extern void            Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel );
00501 extern void            Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel );
00502 /*=== ivyOper.c =========================================================*/
00503 extern Ivy_Obj_t *     Ivy_Oper( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type );
00504 extern Ivy_Obj_t *     Ivy_And( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
00505 extern Ivy_Obj_t *     Ivy_Or( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
00506 extern Ivy_Obj_t *     Ivy_Exor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
00507 extern Ivy_Obj_t *     Ivy_Mux( Ivy_Man_t * p, Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 );
00508 extern Ivy_Obj_t *     Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC );
00509 extern Ivy_Obj_t *     Ivy_Miter( Ivy_Man_t * p, Vec_Ptr_t * vPairs );
00510 extern Ivy_Obj_t *     Ivy_Latch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init );
00511 /*=== ivyResyn.c =========================================================*/
00512 extern Ivy_Man_t *     Ivy_ManResyn0( Ivy_Man_t * p, int fUpdateLevel, int fVerbose );
00513 extern Ivy_Man_t *     Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbose );
00514 extern Ivy_Man_t *     Ivy_ManRwsat( Ivy_Man_t * pMan, int fVerbose );
00515 /*=== ivyRewrite.c =========================================================*/
00516 extern int             Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
00517 extern int             Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
00518 extern int             Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose );
00519 /*=== ivySeq.c =========================================================*/
00520 extern int             Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose );
00521 /*=== ivyShow.c =========================================================*/
00522 extern void            Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
00523 /*=== ivyTable.c ========================================================*/
00524 extern Ivy_Obj_t *     Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj );
00525 extern void            Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj );
00526 extern void            Ivy_TableDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj );
00527 extern void            Ivy_TableUpdate( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ObjIdNew );
00528 extern int             Ivy_TableCountEntries( Ivy_Man_t * p );
00529 extern void            Ivy_TableProfile( Ivy_Man_t * p );
00530 /*=== ivyUtil.c =========================================================*/
00531 extern void            Ivy_ManIncrementTravId( Ivy_Man_t * p );
00532 extern void            Ivy_ManCleanTravId( Ivy_Man_t * p );
00533 extern unsigned *      Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth );
00534 extern void            Ivy_ManCollectCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes );
00535 extern Vec_Int_t *     Ivy_ManLatches( Ivy_Man_t * p );
00536 extern int             Ivy_ManLevels( Ivy_Man_t * p );
00537 extern void            Ivy_ManResetLevels( Ivy_Man_t * p );
00538 extern int             Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pObj );
00539 extern void            Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj );
00540 extern void            Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew );
00541 extern int             Ivy_ObjIsMuxType( Ivy_Obj_t * pObj );
00542 extern Ivy_Obj_t *     Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObjT, Ivy_Obj_t ** ppObjE );
00543 extern Ivy_Obj_t *     Ivy_ObjReal( Ivy_Obj_t * pObj );
00544 extern void            Ivy_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig );
00545 extern void            Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig );
00546 extern int             Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth );
00547 
00548 #ifdef __cplusplus
00549 }
00550 #endif
00551 
00552 #endif
00553 
00557