1 /**CFile****************************************************************
2 
3   FileName    [abcAig.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Network and node package.]
8 
9   Synopsis    [Simple structural hashing package.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 20, 2005.]
16 
17   Revision    [$Id: abcAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "abc.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 /*
26     AIG is an And-Inv Graph with structural hashing.
27     It is always structurally hashed. It means that at any time:
28     - for each AND gate, there are no other AND gates with the same children
29     - the constants are propagated
30     - there is no single-input nodes (inverters/buffers)
31     Additionally the following invariants are satisfied:
32     - there are no dangling nodes (the nodes without fanout)
33     - the level of each AND gate reflects the levels of this fanins
34     - the EXOR-status of each node is up-to-date
35     - the AND nodes are in the topological order
36     - the constant 1 node has always number 0 in the object list
37     The operations that are performed on AIGs:
38     - building new nodes (Abc_AigAnd)
39     - performing elementary Boolean operations (Abc_AigOr, Abc_AigXor, etc)
40     - replacing one node by another (Abc_AigReplace)
41     - propagating constants (Abc_AigReplace)
42     When AIG is duplicated, the new graph is structurally hashed too.
43     If this repeated hashing leads to fewer nodes, it means the original
44     AIG was not strictly hashed (one of the conditions above is violated).
45 */
46 
47 ////////////////////////////////////////////////////////////////////////
48 ///                        DECLARATIONS                              ///
49 ////////////////////////////////////////////////////////////////////////
50 
51 // the simple AIG manager
52 struct Abc_Aig_t_
53 {
54     Abc_Ntk_t *       pNtkAig;           // the AIG network
55     Abc_Obj_t *       pConst1;           // the constant 1 object (not a node!)
56     Abc_Obj_t **      pBins;             // the table bins
57     int               nBins;             // the size of the table
58     int               nEntries;          // the total number of entries in the table
59     Vec_Ptr_t *       vNodes;            // the temporary array of nodes
60     Vec_Ptr_t *       vStackReplaceOld;  // the nodes to be replaced
61     Vec_Ptr_t *       vStackReplaceNew;  // the nodes to be used for replacement
62     Vec_Vec_t *       vLevels;           // the nodes to be updated
63     Vec_Vec_t *       vLevelsR;          // the nodes to be updated
64     Vec_Ptr_t *       vAddedCells;       // the added nodes
65     Vec_Ptr_t *       vUpdatedNets;      // the nodes whose fanouts have changed
66 
67     int               nStrash0;
68     int               nStrash1;
69     int               nStrash5;
70     int               nStrash2;
71 };
72 
73 // iterators through the entries in the linked lists of nodes
74 #define Abc_AigBinForEachEntry( pBin, pEnt )                   \
75     for ( pEnt = pBin;                                         \
76           pEnt;                                                \
77           pEnt = pEnt->pNext )
78 #define Abc_AigBinForEachEntrySafe( pBin, pEnt, pEnt2 )        \
79     for ( pEnt = pBin,                                         \
80           pEnt2 = pEnt? pEnt->pNext: NULL;                     \
81           pEnt;                                                \
82           pEnt = pEnt2,                                        \
83           pEnt2 = pEnt? pEnt->pNext: NULL )
84 
85 // hash key for the structural hash table
86 //static inline unsigned Abc_HashKey2( Abc_Obj_t * p0, Abc_Obj_t * p1, int TableSize ) { return ((unsigned)(p0) + (unsigned)(p1) * 12582917) % TableSize; }
87 //static inline unsigned Abc_HashKey2( Abc_Obj_t * p0, Abc_Obj_t * p1, int TableSize ) { return ((unsigned)((a)->Id + (b)->Id) * ((a)->Id + (b)->Id + 1) / 2) % TableSize; }
88 
89 // hashing the node
Abc_HashKey2(Abc_Obj_t * p0,Abc_Obj_t * p1,int TableSize)90 static unsigned Abc_HashKey2( Abc_Obj_t * p0, Abc_Obj_t * p1, int TableSize )
91 {
92     unsigned Key = 0;
93     Key ^= Abc_ObjRegular(p0)->Id * 7937;
94     Key ^= Abc_ObjRegular(p1)->Id * 2971;
95     Key ^= Abc_ObjIsComplement(p0) * 911;
96     Key ^= Abc_ObjIsComplement(p1) * 353;
97     return Key % TableSize;
98 }
99 
100 // structural hash table procedures
101 static Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
102 static Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, Abc_Obj_t * pAnd );
103 static void        Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis );
104 static void        Abc_AigResize( Abc_Aig_t * pMan );
105 // incremental AIG procedures
106 static void        Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel );
107 static void        Abc_AigUpdateLevel_int( Abc_Aig_t * pMan );
108 static void        Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan );
109 static void        Abc_AigRemoveFromLevelStructure( Vec_Vec_t * vStruct, Abc_Obj_t * pNode );
110 static void        Abc_AigRemoveFromLevelStructureR( Vec_Vec_t * vStruct, Abc_Obj_t * pNode );
111 
112 
113 ////////////////////////////////////////////////////////////////////////
114 ///                     FUNCTION DEFINITIONS                         ///
115 ////////////////////////////////////////////////////////////////////////
116 
117 /**Function*************************************************************
118 
119   Synopsis    [Allocates the local AIG manager.]
120 
121   Description []
122 
123   SideEffects []
124 
125   SeeAlso     []
126 
127 ***********************************************************************/
Abc_AigAlloc(Abc_Ntk_t * pNtkAig)128 Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
129 {
130     Abc_Aig_t * pMan;
131     // start the manager
132     pMan = ABC_ALLOC( Abc_Aig_t, 1 );
133     memset( pMan, 0, sizeof(Abc_Aig_t) );
134     // allocate the table
135     pMan->nBins    = Abc_PrimeCudd( 10000 );
136     pMan->pBins    = ABC_ALLOC( Abc_Obj_t *, pMan->nBins );
137     memset( pMan->pBins, 0, sizeof(Abc_Obj_t *) * pMan->nBins );
138     pMan->vNodes   = Vec_PtrAlloc( 100 );
139     pMan->vLevels  = Vec_VecAlloc( 100 );
140     pMan->vLevelsR = Vec_VecAlloc( 100 );
141     pMan->vStackReplaceOld = Vec_PtrAlloc( 100 );
142     pMan->vStackReplaceNew = Vec_PtrAlloc( 100 );
143     // create the constant node
144     assert( pNtkAig->vObjs->nSize == 0 );
145     pMan->pConst1 = Abc_NtkCreateObj( pNtkAig, ABC_OBJ_NODE );
146     pMan->pConst1->Type = ABC_OBJ_CONST1;
147     pMan->pConst1->fPhase = 1;
148     pNtkAig->nObjCounts[ABC_OBJ_NODE]--;
149     // save the current network
150     pMan->pNtkAig = pNtkAig;
151     return pMan;
152 }
153 
154 /**Function*************************************************************
155 
156   Synopsis    [Deallocates the local AIG manager.]
157 
158   Description []
159 
160   SideEffects []
161 
162   SeeAlso     []
163 
164 ***********************************************************************/
Abc_AigFree(Abc_Aig_t * pMan)165 void Abc_AigFree( Abc_Aig_t * pMan )
166 {
167     assert( Vec_PtrSize( pMan->vStackReplaceOld ) == 0 );
168     assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 );
169     // free the table
170     if ( pMan->vAddedCells )
171         Vec_PtrFree( pMan->vAddedCells );
172     if ( pMan->vUpdatedNets )
173         Vec_PtrFree( pMan->vUpdatedNets );
174     Vec_VecFree( pMan->vLevels );
175     Vec_VecFree( pMan->vLevelsR );
176     Vec_PtrFree( pMan->vStackReplaceOld );
177     Vec_PtrFree( pMan->vStackReplaceNew );
178     Vec_PtrFree( pMan->vNodes );
179     ABC_FREE( pMan->pBins );
180     ABC_FREE( pMan );
181 }
182 
183 /**Function*************************************************************
184 
185   Synopsis    [Returns the number of dangling nodes removed.]
186 
187   Description []
188 
189   SideEffects []
190 
191   SeeAlso     []
192 
193 ***********************************************************************/
Abc_AigCleanup(Abc_Aig_t * pMan)194 int Abc_AigCleanup( Abc_Aig_t * pMan )
195 {
196     Vec_Ptr_t * vDangles;
197     Abc_Obj_t * pAnd;
198     int i, nNodesOld;
199 //    printf( "Strash0 = %d.  Strash1 = %d.  Strash100 = %d.  StrashM = %d.\n",
200 //        pMan->nStrash0, pMan->nStrash1, pMan->nStrash5, pMan->nStrash2 );
201     nNodesOld = pMan->nEntries;
202     // collect the AND nodes that do not fanout
203     vDangles = Vec_PtrAlloc( 100 );
204     for ( i = 0; i < pMan->nBins; i++ )
205         Abc_AigBinForEachEntry( pMan->pBins[i], pAnd )
206             if ( Abc_ObjFanoutNum(pAnd) == 0 )
207                 Vec_PtrPush( vDangles, pAnd );
208     // process the dangling nodes and their MFFCs
209     Vec_PtrForEachEntry( Abc_Obj_t *, vDangles, pAnd, i )
210         Abc_AigDeleteNode( pMan, pAnd );
211     Vec_PtrFree( vDangles );
212     return nNodesOld - pMan->nEntries;
213 }
214 
215 /**Function*************************************************************
216 
217   Synopsis    [Makes sure that every node in the table is in the network and vice versa.]
218 
219   Description []
220 
221   SideEffects []
222 
223   SeeAlso     []
224 
225 ***********************************************************************/
Abc_AigCheck(Abc_Aig_t * pMan)226 int Abc_AigCheck( Abc_Aig_t * pMan )
227 {
228     Abc_Obj_t * pObj, * pAnd;
229     int i, nFanins, Counter;
230     Abc_NtkForEachNode( pMan->pNtkAig, pObj, i )
231     {
232         nFanins = Abc_ObjFaninNum(pObj);
233         if ( nFanins == 0 )
234         {
235             if ( !Abc_AigNodeIsConst(pObj) )
236             {
237                 printf( "Abc_AigCheck: The AIG has non-standard constant nodes.\n" );
238                 return 0;
239             }
240             continue;
241         }
242         if ( nFanins == 1 )
243         {
244             printf( "Abc_AigCheck: The AIG has single input nodes.\n" );
245             return 0;
246         }
247         if ( nFanins > 2 )
248         {
249             printf( "Abc_AigCheck: The AIG has non-standard nodes.\n" );
250             return 0;
251         }
252         if ( pObj->Level != 1 + (unsigned)Abc_MaxInt( Abc_ObjFanin0(pObj)->Level, Abc_ObjFanin1(pObj)->Level ) )
253             printf( "Abc_AigCheck: Node \"%s\" has level that does not agree with the fanin levels.\n", Abc_ObjName(pObj) );
254         pAnd = Abc_AigAndLookup( pMan, Abc_ObjChild0(pObj), Abc_ObjChild1(pObj) );
255         if ( pAnd != pObj )
256             printf( "Abc_AigCheck: Node \"%s\" is not in the structural hashing table.\n", Abc_ObjName(pObj) );
257     }
258     // count the number of nodes in the table
259     Counter = 0;
260     for ( i = 0; i < pMan->nBins; i++ )
261         Abc_AigBinForEachEntry( pMan->pBins[i], pAnd )
262             Counter++;
263     if ( Counter != Abc_NtkNodeNum(pMan->pNtkAig) )
264     {
265         printf( "Abc_AigCheck: The number of nodes in the structural hashing table is wrong.\n" );
266         return 0;
267     }
268     // if the node is a choice node, nodes in its class should not have fanouts
269     Abc_NtkForEachNode( pMan->pNtkAig, pObj, i )
270         if ( Abc_AigNodeIsChoice(pObj) )
271             for ( pAnd = (Abc_Obj_t *)pObj->pData; pAnd; pAnd = (Abc_Obj_t *)pAnd->pData )
272                 if ( Abc_ObjFanoutNum(pAnd) > 0 )
273                 {
274                     printf( "Abc_AigCheck: Representative %s", Abc_ObjName(pAnd) );
275                     printf( " of choice node %s has %d fanouts.\n", Abc_ObjName(pObj), Abc_ObjFanoutNum(pAnd) );
276                     return 0;
277                 }
278     return 1;
279 }
280 
281 /**Function*************************************************************
282 
283   Synopsis    [Computes the number of logic levels not counting PIs/POs.]
284 
285   Description []
286 
287   SideEffects []
288 
289   SeeAlso     []
290 
291 ***********************************************************************/
Abc_AigLevel(Abc_Ntk_t * pNtk)292 int Abc_AigLevel( Abc_Ntk_t * pNtk )
293 {
294     Abc_Obj_t * pNode;
295     int i, LevelsMax;
296     assert( Abc_NtkIsStrash(pNtk) );
297     if ( pNtk->nBarBufs )
298         return Abc_NtkLevel( pNtk );
299     // perform the traversal
300     LevelsMax = 0;
301     Abc_NtkForEachCo( pNtk, pNode, i )
302         if ( LevelsMax < (int)Abc_ObjFanin0(pNode)->Level )
303             LevelsMax = (int)Abc_ObjFanin0(pNode)->Level;
304     return LevelsMax;
305 }
306 
307 
308 /**Function*************************************************************
309 
310   Synopsis    [Performs canonicization step.]
311 
312   Description [The argument nodes can be complemented.]
313 
314   SideEffects []
315 
316   SeeAlso     []
317 
318 ***********************************************************************/
Abc_AigAndCreate(Abc_Aig_t * pMan,Abc_Obj_t * p0,Abc_Obj_t * p1)319 Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
320 {
321     Abc_Obj_t * pAnd;
322     unsigned Key;
323     // check if it is a good time for table resizing
324     if ( pMan->nEntries > 2 * pMan->nBins )
325         Abc_AigResize( pMan );
326     // order the arguments
327     if ( Abc_ObjRegular(p0)->Id > Abc_ObjRegular(p1)->Id )
328         pAnd = p0, p0 = p1, p1 = pAnd;
329     // create the new node
330     pAnd = Abc_NtkCreateNode( pMan->pNtkAig );
331     Abc_ObjAddFanin( pAnd, p0 );
332     Abc_ObjAddFanin( pAnd, p1 );
333     // set the level of the new node
334     pAnd->Level  = 1 + Abc_MaxInt( Abc_ObjRegular(p0)->Level, Abc_ObjRegular(p1)->Level );
335     pAnd->fExor  = Abc_NodeIsExorType(pAnd);
336     pAnd->fPhase = (Abc_ObjIsComplement(p0) ^ Abc_ObjRegular(p0)->fPhase) & (Abc_ObjIsComplement(p1) ^ Abc_ObjRegular(p1)->fPhase);
337     // add the node to the corresponding linked list in the table
338     Key = Abc_HashKey2( p0, p1, pMan->nBins );
339     pAnd->pNext      = pMan->pBins[Key];
340     pMan->pBins[Key] = pAnd;
341     pMan->nEntries++;
342     // create the cuts if defined
343 //    if ( pAnd->pNtk->pManCut )
344 //        Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
345     pAnd->pCopy = NULL;
346     // add the node to the list of updated nodes
347     if ( pMan->vAddedCells )
348         Vec_PtrPush( pMan->vAddedCells, pAnd );
349     return pAnd;
350 }
351 
352 /**Function*************************************************************
353 
354   Synopsis    [Performs canonicization step.]
355 
356   Description [The argument nodes can be complemented.]
357 
358   SideEffects []
359 
360   SeeAlso     []
361 
362 ***********************************************************************/
Abc_AigAndCreateFrom(Abc_Aig_t * pMan,Abc_Obj_t * p0,Abc_Obj_t * p1,Abc_Obj_t * pAnd)363 Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, Abc_Obj_t * pAnd )
364 {
365     Abc_Obj_t * pTemp;
366     unsigned Key;
367     assert( !Abc_ObjIsComplement(pAnd) );
368     // order the arguments
369     if ( Abc_ObjRegular(p0)->Id > Abc_ObjRegular(p1)->Id )
370         pTemp = p0, p0 = p1, p1 = pTemp;
371     // create the new node
372     Abc_ObjAddFanin( pAnd, p0 );
373     Abc_ObjAddFanin( pAnd, p1 );
374     // set the level of the new node
375     pAnd->Level      = 1 + Abc_MaxInt( Abc_ObjRegular(p0)->Level, Abc_ObjRegular(p1)->Level );
376     pAnd->fExor      = Abc_NodeIsExorType(pAnd);
377     // add the node to the corresponding linked list in the table
378     Key = Abc_HashKey2( p0, p1, pMan->nBins );
379     pAnd->pNext      = pMan->pBins[Key];
380     pMan->pBins[Key] = pAnd;
381     pMan->nEntries++;
382     // create the cuts if defined
383 //    if ( pAnd->pNtk->pManCut )
384 //        Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
385     pAnd->pCopy = NULL;
386     // add the node to the list of updated nodes
387 //    if ( pMan->vAddedCells )
388 //        Vec_PtrPush( pMan->vAddedCells, pAnd );
389     return pAnd;
390 }
391 
392 /**Function*************************************************************
393 
394   Synopsis    [Performs canonicization step.]
395 
396   Description [The argument nodes can be complemented.]
397 
398   SideEffects []
399 
400   SeeAlso     []
401 
402 ***********************************************************************/
Abc_AigAndLookup(Abc_Aig_t * pMan,Abc_Obj_t * p0,Abc_Obj_t * p1)403 Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
404 {
405     Abc_Obj_t * pAnd, * pConst1;
406     unsigned Key;
407     assert( Abc_ObjRegular(p0)->pNtk->pManFunc == pMan );
408     assert( Abc_ObjRegular(p1)->pNtk->pManFunc == pMan );
409     // check for trivial cases
410     pConst1 = Abc_AigConst1(pMan->pNtkAig);
411     if ( p0 == p1 )
412         return p0;
413     if ( p0 == Abc_ObjNot(p1) )
414         return Abc_ObjNot(pConst1);
415     if ( Abc_ObjRegular(p0) == pConst1 )
416     {
417         if ( p0 == pConst1 )
418             return p1;
419         return Abc_ObjNot(pConst1);
420     }
421     if ( Abc_ObjRegular(p1) == pConst1 )
422     {
423         if ( p1 == pConst1 )
424             return p0;
425         return Abc_ObjNot(pConst1);
426     }
427 /*
428     {
429         int nFans0 = Abc_ObjFanoutNum( Abc_ObjRegular(p0) );
430         int nFans1 = Abc_ObjFanoutNum( Abc_ObjRegular(p1) );
431         if ( nFans0 == 0 || nFans1 == 0 )
432             pMan->nStrash0++;
433         else if ( nFans0 == 1 || nFans1 == 1 )
434             pMan->nStrash1++;
435         else if ( nFans0 <= 100 && nFans1 <= 100 )
436             pMan->nStrash5++;
437         else
438             pMan->nStrash2++;
439     }
440 */
441     {
442         int nFans0 = Abc_ObjFanoutNum( Abc_ObjRegular(p0) );
443         int nFans1 = Abc_ObjFanoutNum( Abc_ObjRegular(p1) );
444         if ( nFans0 == 0 || nFans1 == 0 )
445             return NULL;
446     }
447 
448     // order the arguments
449     if ( Abc_ObjRegular(p0)->Id > Abc_ObjRegular(p1)->Id )
450         pAnd = p0, p0 = p1, p1 = pAnd;
451     // get the hash key for these two nodes
452     Key = Abc_HashKey2( p0, p1, pMan->nBins );
453     // find the matching node in the table
454     Abc_AigBinForEachEntry( pMan->pBins[Key], pAnd )
455         if ( p0 == Abc_ObjChild0(pAnd) && p1 == Abc_ObjChild1(pAnd) )
456         {
457 //            assert( Abc_ObjFanoutNum(Abc_ObjRegular(p0)) && Abc_ObjFanoutNum(p1) );
458              return pAnd;
459         }
460     return NULL;
461 }
462 
463 /**Function*************************************************************
464 
465   Synopsis    [Returns the gate implementing EXOR of the two arguments if it exists.]
466 
467   Description [The argument nodes can be complemented.]
468 
469   SideEffects []
470 
471   SeeAlso     []
472 
473 ***********************************************************************/
Abc_AigXorLookup(Abc_Aig_t * pMan,Abc_Obj_t * p0,Abc_Obj_t * p1,int * pType)474 Abc_Obj_t * Abc_AigXorLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, int * pType )
475 {
476     Abc_Obj_t * pNode1, * pNode2, * pNode;
477     // set the flag to zero
478     if ( pType ) *pType = 0;
479     // check the case of XOR(a,b) = OR(ab, a'b')'
480     if ( (pNode1 = Abc_AigAndLookup(pMan, Abc_ObjNot(p0), Abc_ObjNot(p1))) &&
481          (pNode2 = Abc_AigAndLookup(pMan, p0, p1)) )
482     {
483         pNode = Abc_AigAndLookup( pMan, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) );
484         if ( pNode && pType ) *pType = 1;
485         return pNode;
486     }
487     // check the case of XOR(a,b) = OR(a'b, ab')
488     if ( (pNode1 = Abc_AigAndLookup(pMan, p0, Abc_ObjNot(p1))) &&
489          (pNode2 = Abc_AigAndLookup(pMan, Abc_ObjNot(p0), p1)) )
490     {
491         pNode = Abc_AigAndLookup( pMan, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) );
492         return pNode? Abc_ObjNot(pNode) : NULL;
493     }
494     return NULL;
495 }
496 
497 /**Function*************************************************************
498 
499   Synopsis    [Returns the gate implementing EXOR of the two arguments if it exists.]
500 
501   Description [The argument nodes can be complemented.]
502 
503   SideEffects []
504 
505   SeeAlso     []
506 
507 ***********************************************************************/
Abc_AigMuxLookup(Abc_Aig_t * pMan,Abc_Obj_t * pC,Abc_Obj_t * pT,Abc_Obj_t * pE,int * pType)508 Abc_Obj_t * Abc_AigMuxLookup( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * pT, Abc_Obj_t * pE, int * pType )
509 {
510     Abc_Obj_t * pNode1, * pNode2, * pNode;
511     // set the flag to zero
512     if ( pType ) *pType = 0;
513     // check the case of MUX(c,t,e) = OR(ct', c'e')'
514     if ( (pNode1 = Abc_AigAndLookup(pMan, pC, Abc_ObjNot(pT))) &&
515          (pNode2 = Abc_AigAndLookup(pMan, Abc_ObjNot(pC), Abc_ObjNot(pE))) )
516     {
517         pNode = Abc_AigAndLookup( pMan, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) );
518         if ( pNode && pType ) *pType = 1;
519         return pNode;
520     }
521     // check the case of MUX(c,t,e) = OR(ct, c'e)
522     if ( (pNode1 = Abc_AigAndLookup(pMan, pC, pT)) &&
523          (pNode2 = Abc_AigAndLookup(pMan, Abc_ObjNot(pC), pE)) )
524     {
525         pNode = Abc_AigAndLookup( pMan, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) );
526         return pNode? Abc_ObjNot(pNode) : NULL;
527     }
528     return NULL;
529 }
530 
531 /**Function*************************************************************
532 
533   Synopsis    [Deletes an AIG node from the hash table.]
534 
535   Description []
536 
537   SideEffects []
538 
539   SeeAlso     []
540 
541 ***********************************************************************/
Abc_AigAndDelete(Abc_Aig_t * pMan,Abc_Obj_t * pThis)542 void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis )
543 {
544     Abc_Obj_t * pAnd, * pAnd0, * pAnd1, ** ppPlace;
545     unsigned Key;
546     assert( !Abc_ObjIsComplement(pThis) );
547     assert( Abc_ObjIsNode(pThis) );
548     assert( Abc_ObjFaninNum(pThis) == 2 );
549     assert( pMan->pNtkAig == pThis->pNtk );
550     // get the hash key for these two nodes
551     pAnd0 = Abc_ObjRegular( Abc_ObjChild0(pThis) );
552     pAnd1 = Abc_ObjRegular( Abc_ObjChild1(pThis) );
553     Key = Abc_HashKey2( Abc_ObjChild0(pThis), Abc_ObjChild1(pThis), pMan->nBins );
554     // find the matching node in the table
555     ppPlace = pMan->pBins + Key;
556     Abc_AigBinForEachEntry( pMan->pBins[Key], pAnd )
557     {
558         if ( pAnd != pThis )
559         {
560             ppPlace = &pAnd->pNext;
561             continue;
562         }
563         *ppPlace = pAnd->pNext;
564         break;
565     }
566     assert( pAnd == pThis );
567     pMan->nEntries--;
568     // delete the cuts if defined
569     if ( pThis->pNtk->pManCut )
570         Abc_NodeFreeCuts( pThis->pNtk->pManCut, pThis );
571 }
572 
573 /**Function*************************************************************
574 
575   Synopsis    [Resizes the hash table of AIG nodes.]
576 
577   Description []
578 
579   SideEffects []
580 
581   SeeAlso     []
582 
583 ***********************************************************************/
Abc_AigResize(Abc_Aig_t * pMan)584 void Abc_AigResize( Abc_Aig_t * pMan )
585 {
586     Abc_Obj_t ** pBinsNew;
587     Abc_Obj_t * pEnt, * pEnt2;
588     int nBinsNew, Counter, i;
589     abctime clk;
590     unsigned Key;
591 
592 clk = Abc_Clock();
593     // get the new table size
594     nBinsNew = Abc_PrimeCudd( 3 * pMan->nBins );
595     // allocate a new array
596     pBinsNew = ABC_ALLOC( Abc_Obj_t *, nBinsNew );
597     memset( pBinsNew, 0, sizeof(Abc_Obj_t *) * nBinsNew );
598     // rehash the entries from the old table
599     Counter = 0;
600     for ( i = 0; i < pMan->nBins; i++ )
601         Abc_AigBinForEachEntrySafe( pMan->pBins[i], pEnt, pEnt2 )
602         {
603             Key = Abc_HashKey2( Abc_ObjChild0(pEnt), Abc_ObjChild1(pEnt), nBinsNew );
604             pEnt->pNext   = pBinsNew[Key];
605             pBinsNew[Key] = pEnt;
606             Counter++;
607         }
608     assert( Counter == pMan->nEntries );
609 //    printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew );
610 //    ABC_PRT( "Time", Abc_Clock() - clk );
611     // replace the table and the parameters
612     ABC_FREE( pMan->pBins );
613     pMan->pBins = pBinsNew;
614     pMan->nBins = nBinsNew;
615 }
616 
617 /**Function*************************************************************
618 
619   Synopsis    [Resizes the hash table of AIG nodes.]
620 
621   Description []
622 
623   SideEffects []
624 
625   SeeAlso     []
626 
627 ***********************************************************************/
Abc_AigRehash(Abc_Aig_t * pMan)628 void Abc_AigRehash( Abc_Aig_t * pMan )
629 {
630     Abc_Obj_t ** pBinsNew;
631     Abc_Obj_t * pEnt, * pEnt2;
632     int * pArray;
633     unsigned Key;
634     int Counter, Temp, i;
635 
636     // allocate a new array
637     pBinsNew = ABC_ALLOC( Abc_Obj_t *, pMan->nBins );
638     memset( pBinsNew, 0, sizeof(Abc_Obj_t *) * pMan->nBins );
639     // rehash the entries from the old table
640     Counter = 0;
641     for ( i = 0; i < pMan->nBins; i++ )
642         Abc_AigBinForEachEntrySafe( pMan->pBins[i], pEnt, pEnt2 )
643         {
644             // swap the fanins if needed
645             pArray = pEnt->vFanins.pArray;
646             if ( pArray[0] > pArray[1] )
647             {
648                 Temp = pArray[0];
649                 pArray[0] = pArray[1];
650                 pArray[1] = Temp;
651                 Temp = pEnt->fCompl0;
652                 pEnt->fCompl0 = pEnt->fCompl1;
653                 pEnt->fCompl1 = Temp;
654             }
655             // rehash the node
656             Key = Abc_HashKey2( Abc_ObjChild0(pEnt), Abc_ObjChild1(pEnt), pMan->nBins );
657             pEnt->pNext   = pBinsNew[Key];
658             pBinsNew[Key] = pEnt;
659             Counter++;
660         }
661     assert( Counter == pMan->nEntries );
662     // replace the table and the parameters
663     ABC_FREE( pMan->pBins );
664     pMan->pBins = pBinsNew;
665 }
666 
667 
668 
669 
670 
671 
672 /**Function*************************************************************
673 
674   Synopsis    [Performs canonicization step.]
675 
676   Description [The argument nodes can be complemented.]
677 
678   SideEffects []
679 
680   SeeAlso     []
681 
682 ***********************************************************************/
Abc_AigConst1(Abc_Ntk_t * pNtk)683 Abc_Obj_t * Abc_AigConst1( Abc_Ntk_t * pNtk )
684 {
685     assert( Abc_NtkIsStrash(pNtk) );
686     return ((Abc_Aig_t *)pNtk->pManFunc)->pConst1;
687 }
688 
689 /**Function*************************************************************
690 
691   Synopsis    [Performs canonicization step.]
692 
693   Description [The argument nodes can be complemented.]
694 
695   SideEffects []
696 
697   SeeAlso     []
698 
699 ***********************************************************************/
Abc_AigAnd(Abc_Aig_t * pMan,Abc_Obj_t * p0,Abc_Obj_t * p1)700 Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
701 {
702     Abc_Obj_t * pAnd;
703     if ( (pAnd = Abc_AigAndLookup( pMan, p0, p1 )) )
704         return pAnd;
705     return Abc_AigAndCreate( pMan, p0, p1 );
706 }
707 
708 /**Function*************************************************************
709 
710   Synopsis    [Implements Boolean OR.]
711 
712   Description []
713 
714   SideEffects []
715 
716   SeeAlso     []
717 
718 ***********************************************************************/
Abc_AigOr(Abc_Aig_t * pMan,Abc_Obj_t * p0,Abc_Obj_t * p1)719 Abc_Obj_t * Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
720 {
721     return Abc_ObjNot( Abc_AigAnd( pMan, Abc_ObjNot(p0), Abc_ObjNot(p1) ) );
722 }
723 
724 /**Function*************************************************************
725 
726   Synopsis    [Implements Boolean XOR.]
727 
728   Description []
729 
730   SideEffects []
731 
732   SeeAlso     []
733 
734 ***********************************************************************/
Abc_AigXor(Abc_Aig_t * pMan,Abc_Obj_t * p0,Abc_Obj_t * p1)735 Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
736 {
737     return Abc_AigOr( pMan, Abc_AigAnd(pMan, p0, Abc_ObjNot(p1)),
738                             Abc_AigAnd(pMan, p1, Abc_ObjNot(p0)) );
739 }
740 
741 /**Function*************************************************************
742 
743   Synopsis    [Implements Boolean XOR.]
744 
745   Description []
746 
747   SideEffects []
748 
749   SeeAlso     []
750 
751 ***********************************************************************/
Abc_AigMux(Abc_Aig_t * pMan,Abc_Obj_t * pC,Abc_Obj_t * p1,Abc_Obj_t * p0)752 Abc_Obj_t * Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 )
753 {
754     return Abc_AigOr( pMan, Abc_AigAnd(pMan, pC, p1), Abc_AigAnd(pMan, Abc_ObjNot(pC), p0) );
755 }
756 
757 /**Function*************************************************************
758 
759   Synopsis    [Implements the miter.]
760 
761   Description []
762 
763   SideEffects []
764 
765   SeeAlso     []
766 
767 ***********************************************************************/
Abc_AigMiter_rec(Abc_Aig_t * pMan,Abc_Obj_t ** ppObjs,int nObjs)768 Abc_Obj_t * Abc_AigMiter_rec( Abc_Aig_t * pMan, Abc_Obj_t ** ppObjs, int nObjs )
769 {
770     Abc_Obj_t * pObj1, * pObj2;
771     if ( nObjs == 1 )
772         return ppObjs[0];
773     pObj1 = Abc_AigMiter_rec( pMan, ppObjs,           nObjs/2 );
774     pObj2 = Abc_AigMiter_rec( pMan, ppObjs + nObjs/2, nObjs - nObjs/2 );
775     return Abc_AigOr( pMan, pObj1, pObj2 );
776 }
777 
778 /**Function*************************************************************
779 
780   Synopsis    [Implements the miter.]
781 
782   Description []
783 
784   SideEffects []
785 
786   SeeAlso     []
787 
788 ***********************************************************************/
Abc_AigMiter(Abc_Aig_t * pMan,Vec_Ptr_t * vPairs,int fImplic)789 Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs, int fImplic )
790 {
791     int i;
792     if ( vPairs->nSize == 0 )
793         return Abc_ObjNot( Abc_AigConst1(pMan->pNtkAig) );
794     assert( vPairs->nSize % 2 == 0 );
795     // go through the cubes of the node's SOP
796     if ( fImplic )
797     {
798         for ( i = 0; i < vPairs->nSize; i += 2 )
799             vPairs->pArray[i/2] = Abc_AigAnd( pMan, (Abc_Obj_t *)vPairs->pArray[i], Abc_ObjNot((Abc_Obj_t *)vPairs->pArray[i+1]) );
800     }
801     else
802     {
803         for ( i = 0; i < vPairs->nSize; i += 2 )
804             vPairs->pArray[i/2] = Abc_AigXor( pMan, (Abc_Obj_t *)vPairs->pArray[i], (Abc_Obj_t *)vPairs->pArray[i+1] );
805     }
806     vPairs->nSize = vPairs->nSize/2;
807     return Abc_AigMiter_rec( pMan, (Abc_Obj_t **)vPairs->pArray, vPairs->nSize );
808 }
809 
810 /**Function*************************************************************
811 
812   Synopsis    [Implements the miter.]
813 
814   Description []
815 
816   SideEffects []
817 
818   SeeAlso     []
819 
820 ***********************************************************************/
Abc_AigMiter2(Abc_Aig_t * pMan,Vec_Ptr_t * vPairs)821 Abc_Obj_t * Abc_AigMiter2( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
822 {
823     Abc_Obj_t * pMiter, * pXor;
824     int i;
825     assert( vPairs->nSize % 2 == 0 );
826     // go through the cubes of the node's SOP
827     pMiter = Abc_ObjNot( Abc_AigConst1(pMan->pNtkAig) );
828     for ( i = 0; i < vPairs->nSize; i += 2 )
829     {
830         pXor   = Abc_AigXor( pMan, (Abc_Obj_t *)vPairs->pArray[i], (Abc_Obj_t *)vPairs->pArray[i+1] );
831         pMiter = Abc_AigOr( pMan, pMiter, pXor );
832     }
833     return pMiter;
834 }
835 
836 
837 
838 
839 /**Function*************************************************************
840 
841   Synopsis    [Replaces one AIG node by the other.]
842 
843   Description []
844 
845   SideEffects []
846 
847   SeeAlso     []
848 
849 ***********************************************************************/
Abc_AigReplace(Abc_Aig_t * pMan,Abc_Obj_t * pOld,Abc_Obj_t * pNew,int fUpdateLevel)850 void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel )
851 {
852     assert( Vec_PtrSize(pMan->vStackReplaceOld) == 0 );
853     assert( Vec_PtrSize(pMan->vStackReplaceNew) == 0 );
854     Vec_PtrPush( pMan->vStackReplaceOld, pOld );
855     Vec_PtrPush( pMan->vStackReplaceNew, pNew );
856     assert( !Abc_ObjIsComplement(pOld) );
857     // process the replacements
858     while ( Vec_PtrSize(pMan->vStackReplaceOld) )
859     {
860         pOld = (Abc_Obj_t *)Vec_PtrPop( pMan->vStackReplaceOld );
861         pNew = (Abc_Obj_t *)Vec_PtrPop( pMan->vStackReplaceNew );
862         Abc_AigReplace_int( pMan, pOld, pNew, fUpdateLevel );
863     }
864     if ( fUpdateLevel )
865     {
866         Abc_AigUpdateLevel_int( pMan );
867         if ( pMan->pNtkAig->vLevelsR )
868             Abc_AigUpdateLevelR_int( pMan );
869     }
870 }
871 
872 /**Function*************************************************************
873 
874   Synopsis    [Performs internal replacement step.]
875 
876   Description []
877 
878   SideEffects []
879 
880   SeeAlso     []
881 
882 ***********************************************************************/
Abc_AigReplace_int(Abc_Aig_t * pMan,Abc_Obj_t * pOld,Abc_Obj_t * pNew,int fUpdateLevel)883 void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel )
884 {
885     Abc_Obj_t * pFanin1, * pFanin2, * pFanout, * pFanoutNew, * pFanoutFanout;
886     int k, v, iFanin;
887     // make sure the old node is regular and has fanouts
888     // (the new node can be complemented and can have fanouts)
889     assert( !Abc_ObjIsComplement(pOld) );
890     assert( Abc_ObjFanoutNum(pOld) > 0 );
891     // look at the fanouts of old node
892     Abc_NodeCollectFanouts( pOld, pMan->vNodes );
893     Vec_PtrForEachEntry( Abc_Obj_t *, pMan->vNodes, pFanout, k )
894     {
895         if ( Abc_ObjIsCo(pFanout) )
896         {
897             Abc_ObjPatchFanin( pFanout, pOld, pNew );
898             continue;
899         }
900         // find the old node as a fanin of this fanout
901         iFanin = Vec_IntFind( &pFanout->vFanins, pOld->Id );
902         assert( iFanin == 0 || iFanin == 1 );
903         // get the new fanin
904         pFanin1 = Abc_ObjNotCond( pNew, Abc_ObjFaninC(pFanout, iFanin) );
905         assert( Abc_ObjRegular(pFanin1) != pFanout );
906         // get another fanin
907         pFanin2 = Abc_ObjChild( pFanout, iFanin ^ 1 );
908         assert( Abc_ObjRegular(pFanin2) != pFanout );
909         // check if the node with these fanins exists
910         if ( (pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 )) )
911         { // such node exists (it may be a constant)
912             // schedule replacement of the old fanout by the new fanout
913             Vec_PtrPush( pMan->vStackReplaceOld, pFanout );
914             Vec_PtrPush( pMan->vStackReplaceNew, pFanoutNew );
915             continue;
916         }
917         // such node does not exist - modify the old fanout node
918         // (this way the change will not propagate all the way to the COs)
919         assert( Abc_ObjRegular(pFanin1) != Abc_ObjRegular(pFanin2) );
920 
921         // if the node is in the level structure, remove it
922         if ( pFanout->fMarkA )
923             Abc_AigRemoveFromLevelStructure( pMan->vLevels, pFanout );
924         // if the node is in the level structure, remove it
925         if ( pFanout->fMarkB )
926             Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pFanout );
927 
928         // remove the old fanout node from the structural hashing table
929         Abc_AigAndDelete( pMan, pFanout );
930         // remove the fanins of the old fanout
931         Abc_ObjRemoveFanins( pFanout );
932         // recreate the old fanout with new fanins and add it to the table
933         Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
934         assert( Abc_AigNodeIsAcyclic(pFanout, pFanout) );
935 
936         if ( fUpdateLevel )
937         {
938             // schedule the updated fanout for updating direct level
939             assert( pFanout->fMarkA == 0 );
940             pFanout->fMarkA = 1;
941             Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout );
942             // schedule the updated fanout for updating reverse level
943             if ( pMan->pNtkAig->vLevelsR )
944             {
945                 assert( pFanout->fMarkB == 0 );
946                 pFanout->fMarkB = 1;
947                 Vec_VecPush( pMan->vLevelsR, Abc_ObjReverseLevel(pFanout), pFanout );
948             }
949         }
950 
951         // the fanout has changed, update EXOR status of its fanouts
952         Abc_ObjForEachFanout( pFanout, pFanoutFanout, v )
953             if ( Abc_AigNodeIsAnd(pFanoutFanout) )
954                 pFanoutFanout->fExor = Abc_NodeIsExorType(pFanoutFanout);
955     }
956     // if the node has no fanouts left, remove its MFFC
957     if ( Abc_ObjFanoutNum(pOld) == 0 )
958         Abc_AigDeleteNode( pMan, pOld );
959 }
960 
961 /**Function*************************************************************
962 
963   Synopsis    [Performs internal deletion step.]
964 
965   Description []
966 
967   SideEffects []
968 
969   SeeAlso     []
970 
971 ***********************************************************************/
Abc_AigDeleteNode(Abc_Aig_t * pMan,Abc_Obj_t * pNode)972 void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
973 {
974     Abc_Obj_t * pNode0, * pNode1, * pTemp;
975     int i, k;
976 
977     // make sure the node is regular and dangling
978     assert( !Abc_ObjIsComplement(pNode) );
979     assert( Abc_ObjIsNode(pNode) );
980     assert( Abc_ObjFaninNum(pNode) == 2 );
981     assert( Abc_ObjFanoutNum(pNode) == 0 );
982 
983     // when deleting an old node that is scheduled for replacement, remove it from the replacement queue
984     Vec_PtrForEachEntry( Abc_Obj_t *, pMan->vStackReplaceOld, pTemp, i )
985         if ( pNode == pTemp )
986         {
987             // remove the entry from the replacement array
988             for ( k = i; k < pMan->vStackReplaceOld->nSize - 1; k++ )
989             {
990                 pMan->vStackReplaceOld->pArray[k] = pMan->vStackReplaceOld->pArray[k+1];
991                 pMan->vStackReplaceNew->pArray[k] = pMan->vStackReplaceNew->pArray[k+1];
992             }
993             pMan->vStackReplaceOld->nSize--;
994             pMan->vStackReplaceNew->nSize--;
995         }
996 
997     // when deleting a new node that should replace another node, do not delete
998     Vec_PtrForEachEntry( Abc_Obj_t *, pMan->vStackReplaceNew, pTemp, i )
999         if ( pNode == Abc_ObjRegular(pTemp) )
1000             return;
1001 
1002     // remember the node's fanins
1003     pNode0 = Abc_ObjFanin0( pNode );
1004     pNode1 = Abc_ObjFanin1( pNode );
1005 
1006     // add the node to the list of updated nodes
1007     if ( pMan->vUpdatedNets )
1008     {
1009         Vec_PtrPushUnique( pMan->vUpdatedNets, pNode0 );
1010         Vec_PtrPushUnique( pMan->vUpdatedNets, pNode1 );
1011     }
1012 
1013     // remove the node from the table
1014     Abc_AigAndDelete( pMan, pNode );
1015     // if the node is in the level structure, remove it
1016     if ( pNode->fMarkA )
1017         Abc_AigRemoveFromLevelStructure( pMan->vLevels, pNode );
1018     if ( pNode->fMarkB )
1019         Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pNode );
1020     // remove the node from the network
1021     Abc_NtkDeleteObj( pNode );
1022 
1023     // call recursively for the fanins
1024     if ( Abc_ObjIsNode(pNode0) && pNode0->vFanouts.nSize == 0 )
1025         Abc_AigDeleteNode( pMan, pNode0 );
1026     if ( Abc_ObjIsNode(pNode1) && pNode1->vFanouts.nSize == 0 )
1027         Abc_AigDeleteNode( pMan, pNode1 );
1028 }
1029 
1030 
1031 /**Function*************************************************************
1032 
1033   Synopsis    [Updates the level of the node after it has changed.]
1034 
1035   Description [This procedure is based on the observation that
1036   after the node's level has changed, the fanouts levels can change too,
1037   but the new fanout levels are always larger than the node's level.
1038   As a result, we can accumulate the nodes to be updated in the queue
1039   and process them in the increasing order of levels.]
1040 
1041   SideEffects []
1042 
1043   SeeAlso     []
1044 
1045 ***********************************************************************/
Abc_AigUpdateLevel_int(Abc_Aig_t * pMan)1046 void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan )
1047 {
1048     Abc_Obj_t * pNode, * pFanout;
1049     Vec_Ptr_t * vVec;
1050     int LevelNew, i, k, v;
1051 
1052     // go through the nodes and update the level of their fanouts
1053     Vec_VecForEachLevel( pMan->vLevels, vVec, i )
1054     {
1055         if ( Vec_PtrSize(vVec) == 0 )
1056             continue;
1057         Vec_PtrForEachEntry( Abc_Obj_t *, vVec, pNode, k )
1058         {
1059             if ( pNode == NULL )
1060                 continue;
1061             assert( Abc_ObjIsNode(pNode) );
1062             assert( (int)pNode->Level == i );
1063             // clean the mark
1064             assert( pNode->fMarkA == 1 );
1065             pNode->fMarkA = 0;
1066             // iterate through the fanouts
1067             Abc_ObjForEachFanout( pNode, pFanout, v )
1068             {
1069                 if ( Abc_ObjIsCo(pFanout) )
1070                     continue;
1071                 // get the new level of this fanout
1072                 LevelNew = 1 + Abc_MaxInt( Abc_ObjFanin0(pFanout)->Level, Abc_ObjFanin1(pFanout)->Level );
1073                 assert( LevelNew > i );
1074                 if ( (int)pFanout->Level == LevelNew ) // no change
1075                     continue;
1076                 // if the fanout is present in the data structure, pull it out
1077                 if ( pFanout->fMarkA )
1078                     Abc_AigRemoveFromLevelStructure( pMan->vLevels, pFanout );
1079                 // update the fanout level
1080                 pFanout->Level = LevelNew;
1081                 // add the fanout to the data structure to update its fanouts
1082                 assert( pFanout->fMarkA == 0 );
1083                 pFanout->fMarkA = 1;
1084                 Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout );
1085             }
1086         }
1087         Vec_PtrClear( vVec );
1088     }
1089 }
1090 
1091 /**Function*************************************************************
1092 
1093   Synopsis    [Updates the level of the node after it has changed.]
1094 
1095   Description []
1096 
1097   SideEffects []
1098 
1099   SeeAlso     []
1100 
1101 ***********************************************************************/
Abc_AigUpdateLevelR_int(Abc_Aig_t * pMan)1102 void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan )
1103 {
1104     Abc_Obj_t * pNode, * pFanin, * pFanout;
1105     Vec_Ptr_t * vVec;
1106     int LevelNew, i, k, v, j;
1107 
1108     // go through the nodes and update the level of their fanouts
1109     Vec_VecForEachLevel( pMan->vLevelsR, vVec, i )
1110     {
1111         if ( Vec_PtrSize(vVec) == 0 )
1112             continue;
1113         Vec_PtrForEachEntry( Abc_Obj_t *, vVec, pNode, k )
1114         {
1115             if ( pNode == NULL )
1116                 continue;
1117             assert( Abc_ObjIsNode(pNode) );
1118             assert( Abc_ObjReverseLevel(pNode) == i );
1119             // clean the mark
1120             assert( pNode->fMarkB == 1 );
1121             pNode->fMarkB = 0;
1122             // iterate through the fanins
1123             Abc_ObjForEachFanin( pNode, pFanin, v )
1124             {
1125                 if ( Abc_ObjIsCi(pFanin) )
1126                     continue;
1127                 // get the new reverse level of this fanin
1128                 LevelNew = 0;
1129                 Abc_ObjForEachFanout( pFanin, pFanout, j )
1130                     if ( LevelNew < Abc_ObjReverseLevel(pFanout) )
1131                         LevelNew = Abc_ObjReverseLevel(pFanout);
1132                 LevelNew += 1;
1133                 assert( LevelNew > i );
1134                 if ( Abc_ObjReverseLevel(pFanin) == LevelNew ) // no change
1135                     continue;
1136                 // if the fanin is present in the data structure, pull it out
1137                 if ( pFanin->fMarkB )
1138                     Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pFanin );
1139                 // update the reverse level
1140                 Abc_ObjSetReverseLevel( pFanin, LevelNew );
1141                 // add the fanin to the data structure to update its fanins
1142                 assert( pFanin->fMarkB == 0 );
1143                 pFanin->fMarkB = 1;
1144                 Vec_VecPush( pMan->vLevelsR, LevelNew, pFanin );
1145             }
1146         }
1147         Vec_PtrClear( vVec );
1148     }
1149 }
1150 
1151 /**Function*************************************************************
1152 
1153   Synopsis    [Removes the node from the level structure.]
1154 
1155   Description []
1156 
1157   SideEffects []
1158 
1159   SeeAlso     []
1160 
1161 ***********************************************************************/
Abc_AigRemoveFromLevelStructure(Vec_Vec_t * vStruct,Abc_Obj_t * pNode)1162 void Abc_AigRemoveFromLevelStructure( Vec_Vec_t * vStruct, Abc_Obj_t * pNode )
1163 {
1164     Vec_Ptr_t * vVecTemp;
1165     Abc_Obj_t * pTemp;
1166     int m;
1167     assert( pNode->fMarkA );
1168     vVecTemp = Vec_VecEntry( vStruct, pNode->Level );
1169     Vec_PtrForEachEntry( Abc_Obj_t *, vVecTemp, pTemp, m )
1170     {
1171         if ( pTemp != pNode )
1172             continue;
1173         Vec_PtrWriteEntry( vVecTemp, m, NULL );
1174         break;
1175     }
1176     assert( m < Vec_PtrSize(vVecTemp) ); // found
1177     pNode->fMarkA = 0;
1178 }
1179 
1180 /**Function*************************************************************
1181 
1182   Synopsis    [Removes the node from the level structure.]
1183 
1184   Description []
1185 
1186   SideEffects []
1187 
1188   SeeAlso     []
1189 
1190 ***********************************************************************/
Abc_AigRemoveFromLevelStructureR(Vec_Vec_t * vStruct,Abc_Obj_t * pNode)1191 void Abc_AigRemoveFromLevelStructureR( Vec_Vec_t * vStruct, Abc_Obj_t * pNode )
1192 {
1193     Vec_Ptr_t * vVecTemp;
1194     Abc_Obj_t * pTemp;
1195     int m;
1196     assert( pNode->fMarkB );
1197     vVecTemp = Vec_VecEntry( vStruct, Abc_ObjReverseLevel(pNode) );
1198     Vec_PtrForEachEntry( Abc_Obj_t *, vVecTemp, pTemp, m )
1199     {
1200         if ( pTemp != pNode )
1201             continue;
1202         Vec_PtrWriteEntry( vVecTemp, m, NULL );
1203         break;
1204     }
1205     assert( m < Vec_PtrSize(vVecTemp) ); // found
1206     pNode->fMarkB = 0;
1207 }
1208 
1209 
1210 
1211 
1212 /**Function*************************************************************
1213 
1214   Synopsis    [Returns 1 if the node has at least one complemented fanout.]
1215 
1216   Description [A fanout is complemented if the fanout's fanin edge pointing
1217   to the given node is complemented.]
1218 
1219   SideEffects []
1220 
1221   SeeAlso     []
1222 
1223 ***********************************************************************/
Abc_AigNodeHasComplFanoutEdge(Abc_Obj_t * pNode)1224 int Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode )
1225 {
1226     Abc_Obj_t * pFanout;
1227     int i, iFanin;
1228     Abc_ObjForEachFanout( pNode, pFanout, i )
1229     {
1230         iFanin = Vec_IntFind( &pFanout->vFanins, pNode->Id );
1231         assert( iFanin >= 0 );
1232         if ( Abc_ObjFaninC( pFanout, iFanin ) )
1233             return 1;
1234     }
1235     return 0;
1236 }
1237 
1238 /**Function*************************************************************
1239 
1240   Synopsis    [Returns 1 if the node has at least one complemented fanout.]
1241 
1242   Description [A fanout is complemented if the fanout's fanin edge pointing
1243   to the given node is complemented. Only the fanouts with current TravId
1244   are counted.]
1245 
1246   SideEffects []
1247 
1248   SeeAlso     []
1249 
1250 ***********************************************************************/
Abc_AigNodeHasComplFanoutEdgeTrav(Abc_Obj_t * pNode)1251 int Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode )
1252 {
1253     Abc_Obj_t * pFanout;
1254     int i, iFanin;
1255     Abc_ObjForEachFanout( pNode, pFanout, i )
1256     {
1257         if ( !Abc_NodeIsTravIdCurrent(pFanout) )
1258             continue;
1259         iFanin = Vec_IntFind( &pFanout->vFanins, pNode->Id );
1260         assert( iFanin >= 0 );
1261         if ( Abc_ObjFaninC( pFanout, iFanin ) )
1262             return 1;
1263     }
1264     return 0;
1265 }
1266 
1267 
1268 /**Function*************************************************************
1269 
1270   Synopsis    [Prints the AIG node for debugging purposes.]
1271 
1272   Description []
1273 
1274   SideEffects []
1275 
1276   SeeAlso     []
1277 
1278 ***********************************************************************/
Abc_AigPrintNode(Abc_Obj_t * pNode)1279 void Abc_AigPrintNode( Abc_Obj_t * pNode )
1280 {
1281     Abc_Obj_t * pNodeR = Abc_ObjRegular(pNode);
1282     if ( Abc_ObjIsCi(pNodeR) )
1283     {
1284         printf( "CI %4s%s.\n", Abc_ObjName(pNodeR), Abc_ObjIsComplement(pNode)? "\'" : "" );
1285         return;
1286     }
1287     if ( Abc_AigNodeIsConst(pNodeR) )
1288     {
1289         printf( "Constant 1 %s.\n", Abc_ObjIsComplement(pNode)? "(complemented)" : ""  );
1290         return;
1291     }
1292     // print the node's function
1293     printf( "%7s%s", Abc_ObjName(pNodeR),                Abc_ObjIsComplement(pNode)? "\'" : "" );
1294     printf( " = " );
1295     printf( "%7s%s", Abc_ObjName(Abc_ObjFanin0(pNodeR)), Abc_ObjFaninC0(pNodeR)?     "\'" : "" );
1296     printf( " * " );
1297     printf( "%7s%s", Abc_ObjName(Abc_ObjFanin1(pNodeR)), Abc_ObjFaninC1(pNodeR)?     "\'" : "" );
1298     printf( "\n" );
1299 }
1300 
1301 
1302 /**Function*************************************************************
1303 
1304   Synopsis    [Check if the node has a combination loop of depth 1 or 2.]
1305 
1306   Description []
1307 
1308   SideEffects []
1309 
1310   SeeAlso     []
1311 
1312 ***********************************************************************/
Abc_AigNodeIsAcyclic(Abc_Obj_t * pNode,Abc_Obj_t * pRoot)1313 int Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot )
1314 {
1315     Abc_Obj_t * pFanin0, * pFanin1;
1316     Abc_Obj_t * pChild00, * pChild01;
1317     Abc_Obj_t * pChild10, * pChild11;
1318     if ( !Abc_AigNodeIsAnd(pNode) )
1319         return 1;
1320     pFanin0 = Abc_ObjFanin0(pNode);
1321     pFanin1 = Abc_ObjFanin1(pNode);
1322     if ( pRoot == pFanin0 || pRoot == pFanin1 )
1323         return 0;
1324     if ( Abc_ObjIsCi(pFanin0) )
1325     {
1326         pChild00 = NULL;
1327         pChild01 = NULL;
1328     }
1329     else
1330     {
1331         pChild00 = Abc_ObjFanin0(pFanin0);
1332         pChild01 = Abc_ObjFanin1(pFanin0);
1333         if ( pRoot == pChild00 || pRoot == pChild01 )
1334             return 0;
1335     }
1336     if ( Abc_ObjIsCi(pFanin1) )
1337     {
1338         pChild10 = NULL;
1339         pChild11 = NULL;
1340     }
1341     else
1342     {
1343         pChild10 = Abc_ObjFanin0(pFanin1);
1344         pChild11 = Abc_ObjFanin1(pFanin1);
1345         if ( pRoot == pChild10 || pRoot == pChild11 )
1346             return 0;
1347     }
1348     return 1;
1349 }
1350 
1351 /**Function*************************************************************
1352 
1353   Synopsis    [Resizes the hash table of AIG nodes.]
1354 
1355   Description []
1356 
1357   SideEffects []
1358 
1359   SeeAlso     []
1360 
1361 ***********************************************************************/
Abc_AigCheckFaninOrder(Abc_Aig_t * pMan)1362 void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan )
1363 {
1364     Abc_Obj_t * pEnt;
1365     int i;
1366     for ( i = 0; i < pMan->nBins; i++ )
1367         Abc_AigBinForEachEntry( pMan->pBins[i], pEnt )
1368         {
1369             if ( Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id > Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id )
1370             {
1371 //                int i0 = Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id;
1372 //                int i1 = Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id;
1373                 printf( "Node %d has incorrect ordering of fanins.\n", pEnt->Id );
1374             }
1375         }
1376 }
1377 
1378 /**Function*************************************************************
1379 
1380   Synopsis    [Sets the correct phase of the nodes.]
1381 
1382   Description [The AIG nodes should be in the DFS order.]
1383 
1384   SideEffects []
1385 
1386   SeeAlso     []
1387 
1388 ***********************************************************************/
Abc_AigSetNodePhases(Abc_Ntk_t * pNtk)1389 void Abc_AigSetNodePhases( Abc_Ntk_t * pNtk )
1390 {
1391     Abc_Obj_t * pObj;
1392     int i;
1393     assert( Abc_NtkIsDfsOrdered(pNtk) );
1394     Abc_AigConst1(pNtk)->fPhase = 1;
1395     Abc_NtkForEachPi( pNtk, pObj, i )
1396         pObj->fPhase = 0;
1397     Abc_NtkForEachLatchOutput( pNtk, pObj, i )
1398         pObj->fPhase = Abc_LatchIsInit1(pObj);
1399     Abc_AigForEachAnd( pNtk, pObj, i )
1400         pObj->fPhase = (Abc_ObjFanin0(pObj)->fPhase ^ Abc_ObjFaninC0(pObj)) & (Abc_ObjFanin1(pObj)->fPhase ^ Abc_ObjFaninC1(pObj));
1401     Abc_NtkForEachPo( pNtk, pObj, i )
1402         pObj->fPhase = (Abc_ObjFanin0(pObj)->fPhase ^ Abc_ObjFaninC0(pObj));
1403     Abc_NtkForEachLatchInput( pNtk, pObj, i )
1404         pObj->fPhase = (Abc_ObjFanin0(pObj)->fPhase ^ Abc_ObjFaninC0(pObj));
1405 }
1406 
1407 
1408 
1409 /**Function*************************************************************
1410 
1411   Synopsis    [Start the update list.]
1412 
1413   Description []
1414 
1415   SideEffects []
1416 
1417   SeeAlso     []
1418 
1419 ***********************************************************************/
Abc_AigUpdateStart(Abc_Aig_t * pMan,Vec_Ptr_t ** pvUpdatedNets)1420 Vec_Ptr_t * Abc_AigUpdateStart( Abc_Aig_t * pMan, Vec_Ptr_t ** pvUpdatedNets )
1421 {
1422     assert( pMan->vAddedCells == NULL );
1423     pMan->vAddedCells  = Vec_PtrAlloc( 1000 );
1424     pMan->vUpdatedNets = Vec_PtrAlloc( 1000 );
1425     *pvUpdatedNets = pMan->vUpdatedNets;
1426     return pMan->vAddedCells;
1427 }
1428 
1429 /**Function*************************************************************
1430 
1431   Synopsis    [Start the update list.]
1432 
1433   Description []
1434 
1435   SideEffects []
1436 
1437   SeeAlso     []
1438 
1439 ***********************************************************************/
Abc_AigUpdateStop(Abc_Aig_t * pMan)1440 void Abc_AigUpdateStop( Abc_Aig_t * pMan )
1441 {
1442     assert( pMan->vAddedCells != NULL );
1443     Vec_PtrFree( pMan->vAddedCells );
1444     Vec_PtrFree( pMan->vUpdatedNets );
1445     pMan->vAddedCells = NULL;
1446     pMan->vUpdatedNets = NULL;
1447 }
1448 
1449 /**Function*************************************************************
1450 
1451   Synopsis    [Start the update list.]
1452 
1453   Description []
1454 
1455   SideEffects []
1456 
1457   SeeAlso     []
1458 
1459 ***********************************************************************/
Abc_AigUpdateReset(Abc_Aig_t * pMan)1460 void Abc_AigUpdateReset( Abc_Aig_t * pMan )
1461 {
1462     assert( pMan->vAddedCells != NULL );
1463     Vec_PtrClear( pMan->vAddedCells );
1464     Vec_PtrClear( pMan->vUpdatedNets );
1465 }
1466 
1467 /**Function*************************************************************
1468 
1469   Synopsis    [Start the update list.]
1470 
1471   Description []
1472 
1473   SideEffects []
1474 
1475   SeeAlso     []
1476 
1477 ***********************************************************************/
Abc_AigCountNext(Abc_Aig_t * pMan)1478 int Abc_AigCountNext( Abc_Aig_t * pMan )
1479 {
1480     Abc_Obj_t * pAnd;
1481     int i, Counter = 0, CounterTotal = 0;
1482     // count how many nodes have pNext set
1483     for ( i = 0; i < pMan->nBins; i++ )
1484         Abc_AigBinForEachEntry( pMan->pBins[i], pAnd )
1485         {
1486             Counter += (pAnd->pNext != NULL);
1487             CounterTotal++;
1488         }
1489     printf( "Counter = %d.  Nodes = %d.  Ave = %6.2f\n", Counter, CounterTotal, 1.0 * CounterTotal/pMan->nBins );
1490     return Counter;
1491 }
1492 
1493 ////////////////////////////////////////////////////////////////////////
1494 ///                       END OF FILE                                ///
1495 ////////////////////////////////////////////////////////////////////////
1496 
1497 
Abc_NtkHelloWorld(Abc_Ntk_t * pNtk)1498 void Abc_NtkHelloWorld( Abc_Ntk_t * pNtk )
1499 {
1500     printf( "Hello, World!\n" );
1501 }
1502 
1503 
1504 ABC_NAMESPACE_IMPL_END
1505 
1506