1 /**CFile****************************************************************
2
3 FileName [ivy.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [And-Inverter Graph package.]
8
9 Synopsis [External declarations.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - May 11, 2006.]
16
17 Revision [$Id: ivy.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__aig__ivy__ivy_h
22 #define ABC__aig__ivy__ivy_h
23
24
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28
29 #include <stdio.h>
30 #include "misc/extra/extra.h"
31 #include "misc/vec/vec.h"
32
33 ////////////////////////////////////////////////////////////////////////
34 /// PARAMETERS ///
35 ////////////////////////////////////////////////////////////////////////
36
37
38
39 ABC_NAMESPACE_HEADER_START
40
41
42 ////////////////////////////////////////////////////////////////////////
43 /// BASIC TYPES ///
44 ////////////////////////////////////////////////////////////////////////
45
46 typedef struct Ivy_Man_t_ Ivy_Man_t;
47 typedef struct Ivy_Obj_t_ Ivy_Obj_t;
48 typedef int Ivy_Edge_t;
49 typedef struct Ivy_FraigParams_t_ Ivy_FraigParams_t;
50
51 // object types
52 typedef enum {
53 IVY_NONE, // 0: non-existent object
54 IVY_PI, // 1: primary input (and constant 1 node)
55 IVY_PO, // 2: primary output
56 IVY_ASSERT, // 3: assertion
57 IVY_LATCH, // 4: sequential element
58 IVY_AND, // 5: AND node
59 IVY_EXOR, // 6: EXOR node
60 IVY_BUF, // 7: buffer (temporary)
61 IVY_VOID // 8: unused object
62 } Ivy_Type_t;
63
64 // latch initial values
65 typedef enum {
66 IVY_INIT_NONE, // 0: not a latch
67 IVY_INIT_0, // 1: zero
68 IVY_INIT_1, // 2: one
69 IVY_INIT_DC // 3: don't-care
70 } Ivy_Init_t;
71
72 // the AIG node
73 struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit) // 10 words - 16 words
74 {
75 int Id; // integer ID
76 int TravId; // traversal ID
77 unsigned Type : 4; // object type
78 unsigned fMarkA : 1; // multipurpose mask
79 unsigned fMarkB : 1; // multipurpose mask
80 unsigned fExFan : 1; // set to 1 if last fanout added is EXOR
81 unsigned fPhase : 1; // value under 000...0 pattern
82 unsigned fFailTfo : 1; // the TFO of the failed node
83 unsigned Init : 2; // latch initial value
84 unsigned Level : 21; // logic level
85 int nRefs; // reference counter
86 Ivy_Obj_t * pFanin0; // fanin
87 Ivy_Obj_t * pFanin1; // fanin
88 Ivy_Obj_t * pFanout; // fanout
89 Ivy_Obj_t * pNextFan0; // next fanout of the first fanin
90 Ivy_Obj_t * pNextFan1; // next fanout of the second fanin
91 Ivy_Obj_t * pPrevFan0; // prev fanout of the first fanin
92 Ivy_Obj_t * pPrevFan1; // prev fanout of the second fanin
93 Ivy_Obj_t * pEquiv; // equivalent node
94 };
95
96 // the AIG manager
97 struct Ivy_Man_t_
98 {
99 // AIG nodes
100 Vec_Ptr_t * vPis; // the array of PIs
101 Vec_Ptr_t * vPos; // the array of POs
102 Vec_Ptr_t * vBufs; // the array of buffers
103 Vec_Ptr_t * vObjs; // the array of objects
104 Ivy_Obj_t * pConst1; // the constant 1 node
105 Ivy_Obj_t Ghost; // the ghost node
106 // AIG node counters
107 int nObjs[IVY_VOID];// the number of objects by type
108 int nCreated; // the number of created objects
109 int nDeleted; // the number of deleted objects
110 // stuctural hash table
111 int * pTable; // structural hash table
112 int nTableSize; // structural hash table size
113 // various data members
114 int fCatchExor; // set to 1 to detect EXORs
115 int nTravIds; // the traversal ID
116 int nLevelMax; // the maximum level
117 Vec_Int_t * vRequired; // required times
118 int fFanout; // fanout is allocated
119 void * pData; // the temporary data
120 void * pCopy; // the temporary data
121 Ivy_Man_t * pHaig; // history AIG if present
122 int nClassesSkip; // the number of skipped classes
123 // memory management
124 Vec_Ptr_t * vChunks; // allocated memory pieces
125 Vec_Ptr_t * vPages; // memory pages used by nodes
126 Ivy_Obj_t * pListFree; // the list of free nodes
127 // timing statistics
128 abctime time1;
129 abctime time2;
130 };
131
132 struct Ivy_FraigParams_t_
133 {
134 int nSimWords; // the number of words in the simulation info
135 double dSimSatur; // the ratio of refined classes when saturation is reached
136 int fPatScores; // enables simulation pattern scoring
137 int MaxScore; // max score after which resimulation is used
138 double dActConeRatio; // the ratio of cone to be bumped
139 double dActConeBumpMax; // the largest bump in activity
140 int fProve; // prove the miter outputs
141 int fVerbose; // verbose output
142 int fDoSparse; // skip sparse functions
143 int nBTLimitNode; // conflict limit at a node
144 int nBTLimitMiter; // conflict limit at an output
145 // int nBTLimitGlobal; // conflict limit global
146 // int nInsLimitNode; // inspection limit at a node
147 // int nInsLimitMiter; // inspection limit at an output
148 // int nInsLimitGlobal; // inspection limit global
149 };
150
151
152 #define IVY_CUT_LIMIT 256
153 #define IVY_CUT_INPUT 6
154
155 typedef struct Ivy_Cut_t_ Ivy_Cut_t;
156 struct Ivy_Cut_t_
157 {
158 int nLatches;
159 short nSize;
160 short nSizeMax;
161 int pArray[IVY_CUT_INPUT];
162 unsigned uHash;
163 };
164
165 typedef struct Ivy_Store_t_ Ivy_Store_t;
166 struct Ivy_Store_t_
167 {
168 int nCuts;
169 int nCutsM;
170 int nCutsMax;
171 int fSatur;
172 Ivy_Cut_t pCuts[IVY_CUT_LIMIT]; // storage for cuts
173 };
174
175 #define IVY_LEAF_MASK 255
176 #define IVY_LEAF_BITS 8
177
178 ////////////////////////////////////////////////////////////////////////
179 /// MACRO DEFINITIONS ///
180 ////////////////////////////////////////////////////////////////////////
181
182 #define IVY_MIN(a,b) (((a) < (b))? (a) : (b))
183 #define IVY_MAX(a,b) (((a) > (b))? (a) : (b))
184
185 extern void Ivy_ManAddMemory( Ivy_Man_t * p );
186
Ivy_BitWordNum(int nBits)187 static inline int Ivy_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
Ivy_TruthWordNum(int nVars)188 static inline int Ivy_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
Ivy_InfoHasBit(unsigned * p,int i)189 static inline int Ivy_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
Ivy_InfoSetBit(unsigned * p,int i)190 static inline void Ivy_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
Ivy_InfoXorBit(unsigned * p,int i)191 static inline void Ivy_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
192
Ivy_Regular(Ivy_Obj_t * p)193 static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
Ivy_Not(Ivy_Obj_t * p)194 static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); }
Ivy_NotCond(Ivy_Obj_t * p,int c)195 static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
Ivy_IsComplement(Ivy_Obj_t * p)196 static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); }
197
Ivy_ManConst0(Ivy_Man_t * p)198 static inline Ivy_Obj_t * Ivy_ManConst0( Ivy_Man_t * p ) { return Ivy_Not(p->pConst1); }
Ivy_ManConst1(Ivy_Man_t * p)199 static inline Ivy_Obj_t * Ivy_ManConst1( Ivy_Man_t * p ) { return p->pConst1; }
Ivy_ManGhost(Ivy_Man_t * p)200 static inline Ivy_Obj_t * Ivy_ManGhost( Ivy_Man_t * p ) { return &p->Ghost; }
Ivy_ManPi(Ivy_Man_t * p,int i)201 static inline Ivy_Obj_t * Ivy_ManPi( Ivy_Man_t * p, int i ) { return (Ivy_Obj_t *)Vec_PtrEntry(p->vPis, i); }
Ivy_ManPo(Ivy_Man_t * p,int i)202 static inline Ivy_Obj_t * Ivy_ManPo( Ivy_Man_t * p, int i ) { return (Ivy_Obj_t *)Vec_PtrEntry(p->vPos, i); }
Ivy_ManObj(Ivy_Man_t * p,int i)203 static inline Ivy_Obj_t * Ivy_ManObj( Ivy_Man_t * p, int i ) { return (Ivy_Obj_t *)Vec_PtrEntry(p->vObjs, i); }
204
Ivy_EdgeCreate(int Id,int fCompl)205 static inline Ivy_Edge_t Ivy_EdgeCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; }
Ivy_EdgeId(Ivy_Edge_t Edge)206 static inline int Ivy_EdgeId( Ivy_Edge_t Edge ) { return Edge >> 1; }
Ivy_EdgeIsComplement(Ivy_Edge_t Edge)207 static inline int Ivy_EdgeIsComplement( Ivy_Edge_t Edge ) { return Edge & 1; }
Ivy_EdgeRegular(Ivy_Edge_t Edge)208 static inline Ivy_Edge_t Ivy_EdgeRegular( Ivy_Edge_t Edge ) { return (Edge >> 1) << 1; }
Ivy_EdgeNot(Ivy_Edge_t Edge)209 static inline Ivy_Edge_t Ivy_EdgeNot( Ivy_Edge_t Edge ) { return Edge ^ 1; }
Ivy_EdgeNotCond(Ivy_Edge_t Edge,int fCond)210 static inline Ivy_Edge_t Ivy_EdgeNotCond( Ivy_Edge_t Edge, int fCond ) { return Edge ^ fCond; }
Ivy_EdgeFromNode(Ivy_Obj_t * pNode)211 static inline Ivy_Edge_t Ivy_EdgeFromNode( Ivy_Obj_t * pNode ) { return Ivy_EdgeCreate( Ivy_Regular(pNode)->Id, Ivy_IsComplement(pNode) ); }
Ivy_EdgeToNode(Ivy_Man_t * p,Ivy_Edge_t Edge)212 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) ); }
213
Ivy_LeafCreate(int Id,int Lat)214 static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << IVY_LEAF_BITS) | Lat; }
Ivy_LeafId(int Leaf)215 static inline int Ivy_LeafId( int Leaf ) { return Leaf >> IVY_LEAF_BITS; }
Ivy_LeafLat(int Leaf)216 static inline int Ivy_LeafLat( int Leaf ) { return Leaf & IVY_LEAF_MASK; }
217
Ivy_ManPiNum(Ivy_Man_t * p)218 static inline int Ivy_ManPiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PI]; }
Ivy_ManPoNum(Ivy_Man_t * p)219 static inline int Ivy_ManPoNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PO]; }
Ivy_ManAssertNum(Ivy_Man_t * p)220 static inline int Ivy_ManAssertNum( Ivy_Man_t * p ) { return p->nObjs[IVY_ASSERT]; }
Ivy_ManLatchNum(Ivy_Man_t * p)221 static inline int Ivy_ManLatchNum( Ivy_Man_t * p ) { return p->nObjs[IVY_LATCH]; }
Ivy_ManAndNum(Ivy_Man_t * p)222 static inline int Ivy_ManAndNum( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]; }
Ivy_ManExorNum(Ivy_Man_t * p)223 static inline int Ivy_ManExorNum( Ivy_Man_t * p ) { return p->nObjs[IVY_EXOR]; }
Ivy_ManBufNum(Ivy_Man_t * p)224 static inline int Ivy_ManBufNum( Ivy_Man_t * p ) { return p->nObjs[IVY_BUF]; }
Ivy_ManObjNum(Ivy_Man_t * p)225 static inline int Ivy_ManObjNum( Ivy_Man_t * p ) { return p->nCreated - p->nDeleted; }
Ivy_ManObjIdMax(Ivy_Man_t * p)226 static inline int Ivy_ManObjIdMax( Ivy_Man_t * p ) { return Vec_PtrSize(p->vObjs)-1; }
Ivy_ManNodeNum(Ivy_Man_t * p)227 static inline int Ivy_ManNodeNum( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR];}
Ivy_ManHashObjNum(Ivy_Man_t * p)228 static inline int Ivy_ManHashObjNum( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]+p->nObjs[IVY_LATCH]; }
Ivy_ManGetCost(Ivy_Man_t * p)229 static inline int Ivy_ManGetCost( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]+3*p->nObjs[IVY_EXOR]+8*p->nObjs[IVY_LATCH]; }
230
Ivy_ObjType(Ivy_Obj_t * pObj)231 static inline Ivy_Type_t Ivy_ObjType( Ivy_Obj_t * pObj ) { return (Ivy_Type_t)pObj->Type; }
Ivy_ObjInit(Ivy_Obj_t * pObj)232 static inline Ivy_Init_t Ivy_ObjInit( Ivy_Obj_t * pObj ) { return (Ivy_Init_t)pObj->Init; }
Ivy_ObjIsConst1(Ivy_Obj_t * pObj)233 static inline int Ivy_ObjIsConst1( Ivy_Obj_t * pObj ) { return pObj->Id == 0; }
Ivy_ObjIsGhost(Ivy_Obj_t * pObj)234 static inline int Ivy_ObjIsGhost( Ivy_Obj_t * pObj ) { return pObj->Id < 0; }
Ivy_ObjIsNone(Ivy_Obj_t * pObj)235 static inline int Ivy_ObjIsNone( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_NONE; }
Ivy_ObjIsPi(Ivy_Obj_t * pObj)236 static inline int Ivy_ObjIsPi( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PI; }
Ivy_ObjIsPo(Ivy_Obj_t * pObj)237 static inline int Ivy_ObjIsPo( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PO; }
Ivy_ObjIsCi(Ivy_Obj_t * pObj)238 static inline int Ivy_ObjIsCi( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PI || pObj->Type == IVY_LATCH; }
Ivy_ObjIsCo(Ivy_Obj_t * pObj)239 static inline int Ivy_ObjIsCo( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PO || pObj->Type == IVY_LATCH; }
Ivy_ObjIsAssert(Ivy_Obj_t * pObj)240 static inline int Ivy_ObjIsAssert( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_ASSERT; }
Ivy_ObjIsLatch(Ivy_Obj_t * pObj)241 static inline int Ivy_ObjIsLatch( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_LATCH; }
Ivy_ObjIsAnd(Ivy_Obj_t * pObj)242 static inline int Ivy_ObjIsAnd( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_AND; }
Ivy_ObjIsExor(Ivy_Obj_t * pObj)243 static inline int Ivy_ObjIsExor( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_EXOR; }
Ivy_ObjIsBuf(Ivy_Obj_t * pObj)244 static inline int Ivy_ObjIsBuf( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_BUF; }
Ivy_ObjIsNode(Ivy_Obj_t * pObj)245 static inline int Ivy_ObjIsNode( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; }
Ivy_ObjIsTerm(Ivy_Obj_t * pObj)246 static inline int Ivy_ObjIsTerm( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PI || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; }
Ivy_ObjIsHash(Ivy_Obj_t * pObj)247 static inline int Ivy_ObjIsHash( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; }
Ivy_ObjIsOneFanin(Ivy_Obj_t * pObj)248 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; }
249
Ivy_ObjIsMarkA(Ivy_Obj_t * pObj)250 static inline int Ivy_ObjIsMarkA( Ivy_Obj_t * pObj ) { return pObj->fMarkA; }
Ivy_ObjSetMarkA(Ivy_Obj_t * pObj)251 static inline void Ivy_ObjSetMarkA( Ivy_Obj_t * pObj ) { pObj->fMarkA = 1; }
Ivy_ObjClearMarkA(Ivy_Obj_t * pObj)252 static inline void Ivy_ObjClearMarkA( Ivy_Obj_t * pObj ) { pObj->fMarkA = 0; }
253
Ivy_ObjSetTravId(Ivy_Obj_t * pObj,int TravId)254 static inline void Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId ) { pObj->TravId = TravId; }
Ivy_ObjSetTravIdCurrent(Ivy_Man_t * p,Ivy_Obj_t * pObj)255 static inline void Ivy_ObjSetTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { pObj->TravId = p->nTravIds; }
Ivy_ObjSetTravIdPrevious(Ivy_Man_t * p,Ivy_Obj_t * pObj)256 static inline void Ivy_ObjSetTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { pObj->TravId = p->nTravIds - 1; }
Ivy_ObjIsTravIdCurrent(Ivy_Man_t * p,Ivy_Obj_t * pObj)257 static inline int Ivy_ObjIsTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return (int )((int)pObj->TravId == p->nTravIds); }
Ivy_ObjIsTravIdPrevious(Ivy_Man_t * p,Ivy_Obj_t * pObj)258 static inline int Ivy_ObjIsTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return (int )((int)pObj->TravId == p->nTravIds - 1); }
259
Ivy_ObjId(Ivy_Obj_t * pObj)260 static inline int Ivy_ObjId( Ivy_Obj_t * pObj ) { return pObj->Id; }
Ivy_ObjTravId(Ivy_Obj_t * pObj)261 static inline int Ivy_ObjTravId( Ivy_Obj_t * pObj ) { return pObj->TravId; }
Ivy_ObjPhase(Ivy_Obj_t * pObj)262 static inline int Ivy_ObjPhase( Ivy_Obj_t * pObj ) { return pObj->fPhase; }
Ivy_ObjExorFanout(Ivy_Obj_t * pObj)263 static inline int Ivy_ObjExorFanout( Ivy_Obj_t * pObj ) { return pObj->fExFan; }
Ivy_ObjRefs(Ivy_Obj_t * pObj)264 static inline int Ivy_ObjRefs( Ivy_Obj_t * pObj ) { return pObj->nRefs; }
Ivy_ObjRefsInc(Ivy_Obj_t * pObj)265 static inline void Ivy_ObjRefsInc( Ivy_Obj_t * pObj ) { pObj->nRefs++; }
Ivy_ObjRefsDec(Ivy_Obj_t * pObj)266 static inline void Ivy_ObjRefsDec( Ivy_Obj_t * pObj ) { assert( pObj->nRefs > 0 ); pObj->nRefs--; }
Ivy_ObjFaninId0(Ivy_Obj_t * pObj)267 static inline int Ivy_ObjFaninId0( Ivy_Obj_t * pObj ) { return pObj->pFanin0? Ivy_ObjId(Ivy_Regular(pObj->pFanin0)) : 0; }
Ivy_ObjFaninId1(Ivy_Obj_t * pObj)268 static inline int Ivy_ObjFaninId1( Ivy_Obj_t * pObj ) { return pObj->pFanin1? Ivy_ObjId(Ivy_Regular(pObj->pFanin1)) : 0; }
Ivy_ObjFaninC0(Ivy_Obj_t * pObj)269 static inline int Ivy_ObjFaninC0( Ivy_Obj_t * pObj ) { return Ivy_IsComplement(pObj->pFanin0); }
Ivy_ObjFaninC1(Ivy_Obj_t * pObj)270 static inline int Ivy_ObjFaninC1( Ivy_Obj_t * pObj ) { return Ivy_IsComplement(pObj->pFanin1); }
Ivy_ObjFanin0(Ivy_Obj_t * pObj)271 static inline Ivy_Obj_t * Ivy_ObjFanin0( Ivy_Obj_t * pObj ) { return Ivy_Regular(pObj->pFanin0); }
Ivy_ObjFanin1(Ivy_Obj_t * pObj)272 static inline Ivy_Obj_t * Ivy_ObjFanin1( Ivy_Obj_t * pObj ) { return Ivy_Regular(pObj->pFanin1); }
Ivy_ObjChild0(Ivy_Obj_t * pObj)273 static inline Ivy_Obj_t * Ivy_ObjChild0( Ivy_Obj_t * pObj ) { return pObj->pFanin0; }
Ivy_ObjChild1(Ivy_Obj_t * pObj)274 static inline Ivy_Obj_t * Ivy_ObjChild1( Ivy_Obj_t * pObj ) { return pObj->pFanin1; }
Ivy_ObjChild0Equiv(Ivy_Obj_t * pObj)275 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; }
Ivy_ObjChild1Equiv(Ivy_Obj_t * pObj)276 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; }
Ivy_ObjEquiv(Ivy_Obj_t * pObj)277 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; }
Ivy_ObjLevel(Ivy_Obj_t * pObj)278 static inline int Ivy_ObjLevel( Ivy_Obj_t * pObj ) { return pObj->Level; }
Ivy_ObjLevelNew(Ivy_Obj_t * pObj)279 static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); }
Ivy_ObjFaninPhase(Ivy_Obj_t * pObj)280 static inline int Ivy_ObjFaninPhase( Ivy_Obj_t * pObj ) { return Ivy_IsComplement(pObj)? !Ivy_Regular(pObj)->fPhase : pObj->fPhase; }
281
Ivy_ObjClean(Ivy_Obj_t * pObj)282 static inline void Ivy_ObjClean( Ivy_Obj_t * pObj )
283 {
284 int IdSaved = pObj->Id;
285 memset( pObj, 0, sizeof(Ivy_Obj_t) );
286 pObj->Id = IdSaved;
287 }
Ivy_ObjOverwrite(Ivy_Obj_t * pBase,Ivy_Obj_t * pData)288 static inline void Ivy_ObjOverwrite( Ivy_Obj_t * pBase, Ivy_Obj_t * pData )
289 {
290 int IdSaved = pBase->Id;
291 memcpy( pBase, pData, sizeof(Ivy_Obj_t) );
292 pBase->Id = IdSaved;
293 }
Ivy_ObjWhatFanin(Ivy_Obj_t * pObj,Ivy_Obj_t * pFanin)294 static inline int Ivy_ObjWhatFanin( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin )
295 {
296 if ( Ivy_ObjFanin0(pObj) == pFanin ) return 0;
297 if ( Ivy_ObjFanin1(pObj) == pFanin ) return 1;
298 assert(0); return -1;
299 }
Ivy_ObjFanoutC(Ivy_Obj_t * pObj,Ivy_Obj_t * pFanout)300 static inline int Ivy_ObjFanoutC( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
301 {
302 if ( Ivy_ObjFanin0(pFanout) == pObj ) return Ivy_ObjFaninC0(pObj);
303 if ( Ivy_ObjFanin1(pFanout) == pObj ) return Ivy_ObjFaninC1(pObj);
304 assert(0); return -1;
305 }
306
307 // create the ghost of the new node
Ivy_ObjCreateGhost(Ivy_Man_t * p,Ivy_Obj_t * p0,Ivy_Obj_t * p1,Ivy_Type_t Type,Ivy_Init_t Init)308 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 )
309 {
310 Ivy_Obj_t * pGhost, * pTemp;
311 assert( Type != IVY_AND || !Ivy_ObjIsConst1(Ivy_Regular(p0)) );
312 assert( p1 == NULL || !Ivy_ObjIsConst1(Ivy_Regular(p1)) );
313 assert( Type == IVY_PI || Ivy_Regular(p0) != Ivy_Regular(p1) );
314 assert( Type != IVY_LATCH || !Ivy_IsComplement(p0) );
315 // assert( p1 == NULL || (!Ivy_ObjIsLatch(Ivy_Regular(p0)) || !Ivy_ObjIsLatch(Ivy_Regular(p1))) );
316 pGhost = Ivy_ManGhost(p);
317 pGhost->Type = Type;
318 pGhost->Init = Init;
319 pGhost->pFanin0 = p0;
320 pGhost->pFanin1 = p1;
321 if ( p1 && Ivy_ObjFaninId0(pGhost) > Ivy_ObjFaninId1(pGhost) )
322 pTemp = pGhost->pFanin0, pGhost->pFanin0 = pGhost->pFanin1, pGhost->pFanin1 = pTemp;
323 return pGhost;
324 }
325
326 // get the complemented initial state
Ivy_InitNotCond(Ivy_Init_t Init,int fCompl)327 static Ivy_Init_t Ivy_InitNotCond( Ivy_Init_t Init, int fCompl )
328 {
329 assert( Init != IVY_INIT_NONE );
330 if ( fCompl == 0 )
331 return Init;
332 if ( Init == IVY_INIT_0 )
333 return IVY_INIT_1;
334 if ( Init == IVY_INIT_1 )
335 return IVY_INIT_0;
336 return IVY_INIT_DC;
337 }
338
339 // get the initial state after forward retiming over AND gate
Ivy_InitAnd(Ivy_Init_t InitA,Ivy_Init_t InitB)340 static Ivy_Init_t Ivy_InitAnd( Ivy_Init_t InitA, Ivy_Init_t InitB )
341 {
342 assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE );
343 if ( InitA == IVY_INIT_0 || InitB == IVY_INIT_0 )
344 return IVY_INIT_0;
345 if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC )
346 return IVY_INIT_DC;
347 return IVY_INIT_1;
348 }
349
350 // get the initial state after forward retiming over EXOR gate
Ivy_InitExor(Ivy_Init_t InitA,Ivy_Init_t InitB)351 static Ivy_Init_t Ivy_InitExor( Ivy_Init_t InitA, Ivy_Init_t InitB )
352 {
353 assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE );
354 if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC )
355 return IVY_INIT_DC;
356 if ( InitA == IVY_INIT_0 && InitB == IVY_INIT_1 )
357 return IVY_INIT_1;
358 if ( InitA == IVY_INIT_1 && InitB == IVY_INIT_0 )
359 return IVY_INIT_1;
360 return IVY_INIT_0;
361 }
362
363 // internal memory manager
Ivy_ManFetchMemory(Ivy_Man_t * p)364 static inline Ivy_Obj_t * Ivy_ManFetchMemory( Ivy_Man_t * p )
365 {
366 Ivy_Obj_t * pTemp;
367 if ( p->pListFree == NULL )
368 Ivy_ManAddMemory( p );
369 pTemp = p->pListFree;
370 p->pListFree = *((Ivy_Obj_t **)pTemp);
371 memset( pTemp, 0, sizeof(Ivy_Obj_t) );
372 return pTemp;
373 }
Ivy_ManRecycleMemory(Ivy_Man_t * p,Ivy_Obj_t * pEntry)374 static inline void Ivy_ManRecycleMemory( Ivy_Man_t * p, Ivy_Obj_t * pEntry )
375 {
376 pEntry->Type = IVY_NONE; // distinquishes dead node from live node
377 *((Ivy_Obj_t **)pEntry) = p->pListFree;
378 p->pListFree = pEntry;
379 }
380
381
382 ////////////////////////////////////////////////////////////////////////
383 /// ITERATORS ///
384 ////////////////////////////////////////////////////////////////////////
385
386 // iterator over the primary inputs
387 #define Ivy_ManForEachPi( p, pObj, i ) \
388 Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPis, pObj, i )
389 // iterator over the primary outputs
390 #define Ivy_ManForEachPo( p, pObj, i ) \
391 Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPos, pObj, i )
392 // iterator over all objects, including those currently not used
393 #define Ivy_ManForEachObj( p, pObj, i ) \
394 Vec_PtrForEachEntry( Ivy_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
395 // iterator over the combinational inputs
396 #define Ivy_ManForEachCi( p, pObj, i ) \
397 Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCi(pObj) ) {} else
398 // iterator over the combinational outputs
399 #define Ivy_ManForEachCo( p, pObj, i ) \
400 Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCo(pObj) ) {} else
401 // iterator over logic nodes (AND and EXOR gates)
402 #define Ivy_ManForEachNode( p, pObj, i ) \
403 Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsNode(pObj) ) {} else
404 // iterator over logic latches
405 #define Ivy_ManForEachLatch( p, pObj, i ) \
406 Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsLatch(pObj) ) {} else
407 // iterator over the nodes whose IDs are stored in the array
408 #define Ivy_ManForEachNodeVec( p, vIds, pObj, i ) \
409 for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Ivy_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
410 // iterator over the fanouts of an object
411 #define Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, i ) \
412 for ( i = 0, Ivy_ObjCollectFanouts(p, pObj, vArray); \
413 i < Vec_PtrSize(vArray) && ((pFanout) = (Ivy_Obj_t *)Vec_PtrEntry(vArray,i)); i++ )
414
415 ////////////////////////////////////////////////////////////////////////
416 /// FUNCTION DECLARATIONS ///
417 ////////////////////////////////////////////////////////////////////////
418
419 /*=== ivyBalance.c ========================================================*/
420 extern Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel );
421 extern Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Ivy_Man_t * p, Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel );
422 /*=== ivyCanon.c ========================================================*/
423 extern Ivy_Obj_t * Ivy_CanonAnd( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
424 extern Ivy_Obj_t * Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
425 extern Ivy_Obj_t * Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init );
426 /*=== ivyCheck.c ========================================================*/
427 extern int Ivy_ManCheck( Ivy_Man_t * p );
428 extern int Ivy_ManCheckFanoutNums( Ivy_Man_t * p );
429 extern int Ivy_ManCheckFanouts( Ivy_Man_t * p );
430 extern int Ivy_ManCheckChoices( Ivy_Man_t * p );
431 /*=== ivyCut.c ==========================================================*/
432 extern void Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize );
433 extern Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves );
434 /*=== ivyDfs.c ==========================================================*/
435 extern Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p );
436 extern Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches );
437 extern void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone );
438 extern Vec_Vec_t * Ivy_ManLevelize( Ivy_Man_t * p );
439 extern Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p );
440 extern int Ivy_ManIsAcyclic( Ivy_Man_t * p );
441 extern int Ivy_ManSetLevels( Ivy_Man_t * p, int fHaig );
442 /*=== ivyDsd.c ==========================================================*/
443 extern int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree );
444 extern void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree );
445 extern unsigned Ivy_TruthDsdCompute( Vec_Int_t * vTree );
446 extern void Ivy_TruthDsdComputePrint( unsigned uTruth );
447 extern Ivy_Obj_t * Ivy_ManDsdConstruct( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vTree );
448 /*=== ivyFanout.c ==========================================================*/
449 extern void Ivy_ManStartFanout( Ivy_Man_t * p );
450 extern void Ivy_ManStopFanout( Ivy_Man_t * p );
451 extern void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout );
452 extern void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout );
453 extern void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew );
454 extern void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vArray );
455 extern Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
456 extern int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj );
457 /*=== ivyFastMap.c =============================================================*/
458 extern void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbose );
459 extern void Ivy_FastMapStop( Ivy_Man_t * pAig );
460 extern void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves );
461 extern void Ivy_FastMapReverseLevel( Ivy_Man_t * pAig );
462 /*=== ivyFraig.c ==========================================================*/
463 extern int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars );
464 extern Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
465 extern Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
466 extern void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams );
467 /*=== ivyHaig.c ==========================================================*/
468 extern void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose );
469 extern void Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew );
470 extern void Ivy_ManHaigStop( Ivy_Man_t * p );
471 extern void Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose );
472 extern void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj );
473 extern void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew );
474 extern void Ivy_ManHaigSimulate( Ivy_Man_t * p );
475 /*=== ivyMan.c ==========================================================*/
476 extern Ivy_Man_t * Ivy_ManStart();
477 extern Ivy_Man_t * Ivy_ManStartFrom( Ivy_Man_t * p );
478 extern Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p );
479 extern Ivy_Man_t * Ivy_ManFrames( Ivy_Man_t * pMan, int nLatches, int nFrames, int fInit, Vec_Ptr_t ** pvMapping );
480 extern void Ivy_ManStop( Ivy_Man_t * p );
481 extern int Ivy_ManCleanup( Ivy_Man_t * p );
482 extern int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel );
483 extern void Ivy_ManPrintStats( Ivy_Man_t * p );
484 extern void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits );
485 /*=== ivyMem.c ==========================================================*/
486 extern void Ivy_ManStartMemory( Ivy_Man_t * p );
487 extern void Ivy_ManStopMemory( Ivy_Man_t * p );
488 /*=== ivyMulti.c ==========================================================*/
489 extern Ivy_Obj_t * Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
490 extern Ivy_Obj_t * Ivy_Multi1( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
491 extern Ivy_Obj_t * Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type );
492 extern Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
493 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 );
494 /*=== ivyObj.c ==========================================================*/
495 extern Ivy_Obj_t * Ivy_ObjCreatePi( Ivy_Man_t * p );
496 extern Ivy_Obj_t * Ivy_ObjCreatePo( Ivy_Man_t * p, Ivy_Obj_t * pDriver );
497 extern Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost );
498 extern void Ivy_ObjConnect( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFan0, Ivy_Obj_t * pFan1 );
499 extern void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj );
500 extern void Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew );
501 extern void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop );
502 extern void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop );
503 extern void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel );
504 extern void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel );
505 /*=== ivyOper.c =========================================================*/
506 extern Ivy_Obj_t * Ivy_Oper( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type );
507 extern Ivy_Obj_t * Ivy_And( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
508 extern Ivy_Obj_t * Ivy_Or( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
509 extern Ivy_Obj_t * Ivy_Exor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
510 extern Ivy_Obj_t * Ivy_Mux( Ivy_Man_t * p, Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 );
511 extern Ivy_Obj_t * Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC );
512 extern Ivy_Obj_t * Ivy_Miter( Ivy_Man_t * p, Vec_Ptr_t * vPairs );
513 extern Ivy_Obj_t * Ivy_Latch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init );
514 /*=== ivyResyn.c =========================================================*/
515 extern Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * p, int fUpdateLevel, int fVerbose );
516 extern Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbose );
517 extern Ivy_Man_t * Ivy_ManRwsat( Ivy_Man_t * pMan, int fVerbose );
518 /*=== ivyRewrite.c =========================================================*/
519 extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
520 extern int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
521 extern int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose );
522 /*=== ivySeq.c =========================================================*/
523 extern int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose );
524 /*=== ivyShow.c =========================================================*/
525 extern void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
526 /*=== ivyTable.c ========================================================*/
527 extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj );
528 extern void Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj );
529 extern void Ivy_TableDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj );
530 extern void Ivy_TableUpdate( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ObjIdNew );
531 extern int Ivy_TableCountEntries( Ivy_Man_t * p );
532 extern void Ivy_TableProfile( Ivy_Man_t * p );
533 /*=== ivyUtil.c =========================================================*/
534 extern void Ivy_ManIncrementTravId( Ivy_Man_t * p );
535 extern void Ivy_ManCleanTravId( Ivy_Man_t * p );
536 extern unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth );
537 extern void Ivy_ManCollectCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes );
538 extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p );
539 extern int Ivy_ManLevels( Ivy_Man_t * p );
540 extern void Ivy_ManResetLevels( Ivy_Man_t * p );
541 extern int Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pObj );
542 extern void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj );
543 extern void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew );
544 extern int Ivy_ObjIsMuxType( Ivy_Obj_t * pObj );
545 extern Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObjT, Ivy_Obj_t ** ppObjE );
546 extern Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj );
547 extern void Ivy_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig );
548 extern void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig );
549 extern int Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth );
550
551
552
553 ABC_NAMESPACE_HEADER_END
554
555
556
557 #endif
558
559 ////////////////////////////////////////////////////////////////////////
560 /// END OF FILE ///
561 ////////////////////////////////////////////////////////////////////////
562
563