1 /**CFile****************************************************************
2 
3   FileName    [hopDfs.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Minimalistic And-Inverter Graph package.]
8 
9   Synopsis    [DFS traversal procedures.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - May 11, 2006.]
16 
17   Revision    [$Id: hopDfs.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "hop.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 ///                        DECLARATIONS                              ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 ///                     FUNCTION DEFINITIONS                         ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36   Synopsis    [Collects internal nodes in the DFS order.]
37 
38   Description []
39 
40   SideEffects []
41 
42   SeeAlso     []
43 
44 ***********************************************************************/
Hop_ManDfs_rec(Hop_Obj_t * pObj,Vec_Ptr_t * vNodes)45 void Hop_ManDfs_rec( Hop_Obj_t * pObj, Vec_Ptr_t * vNodes )
46 {
47     assert( !Hop_IsComplement(pObj) );
48     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
49         return;
50     Hop_ManDfs_rec( Hop_ObjFanin0(pObj), vNodes );
51     Hop_ManDfs_rec( Hop_ObjFanin1(pObj), vNodes );
52     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
53     Hop_ObjSetMarkA(pObj);
54     Vec_PtrPush( vNodes, pObj );
55 }
56 
57 /**Function*************************************************************
58 
59   Synopsis    [Collects internal nodes in the DFS order.]
60 
61   Description []
62 
63   SideEffects []
64 
65   SeeAlso     []
66 
67 ***********************************************************************/
Hop_ManDfs(Hop_Man_t * p)68 Vec_Ptr_t * Hop_ManDfs( Hop_Man_t * p )
69 {
70     Vec_Ptr_t * vNodes;
71     Hop_Obj_t * pObj;
72     int i;
73     vNodes = Vec_PtrAlloc( Hop_ManNodeNum(p) );
74     Hop_ManForEachNode( p, pObj, i )
75         Hop_ManDfs_rec( pObj, vNodes );
76     Hop_ManForEachNode( p, pObj, i )
77         Hop_ObjClearMarkA(pObj);
78     return vNodes;
79 }
80 
81 /**Function*************************************************************
82 
83   Synopsis    [Collects internal nodes in the DFS order.]
84 
85   Description []
86 
87   SideEffects []
88 
89   SeeAlso     []
90 
91 ***********************************************************************/
Hop_ManDfsNode(Hop_Man_t * p,Hop_Obj_t * pNode)92 Vec_Ptr_t * Hop_ManDfsNode( Hop_Man_t * p, Hop_Obj_t * pNode )
93 {
94     Vec_Ptr_t * vNodes;
95     Hop_Obj_t * pObj;
96     int i;
97     assert( !Hop_IsComplement(pNode) );
98     vNodes = Vec_PtrAlloc( 16 );
99     Hop_ManDfs_rec( pNode, vNodes );
100     Vec_PtrForEachEntry( Hop_Obj_t *, vNodes, pObj, i )
101         Hop_ObjClearMarkA(pObj);
102     return vNodes;
103 }
104 
105 /**Function*************************************************************
106 
107   Synopsis    [Computes the max number of levels in the manager.]
108 
109   Description []
110 
111   SideEffects []
112 
113   SeeAlso     []
114 
115 ***********************************************************************/
Hop_ManCountLevels(Hop_Man_t * p)116 int Hop_ManCountLevels( Hop_Man_t * p )
117 {
118     Vec_Ptr_t * vNodes;
119     Hop_Obj_t * pObj;
120     int i, LevelsMax, Level0, Level1;
121     // initialize the levels
122     Hop_ManConst1(p)->pData = NULL;
123     Hop_ManForEachPi( p, pObj, i )
124         pObj->pData = NULL;
125     // compute levels in a DFS order
126     vNodes = Hop_ManDfs( p );
127     Vec_PtrForEachEntry( Hop_Obj_t *, vNodes, pObj, i )
128     {
129         Level0 = (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData;
130         Level1 = (int)(ABC_PTRUINT_T)Hop_ObjFanin1(pObj)->pData;
131         pObj->pData = (void *)(ABC_PTRUINT_T)(1 + Hop_ObjIsExor(pObj) + Abc_MaxInt(Level0, Level1));
132     }
133     Vec_PtrFree( vNodes );
134     // get levels of the POs
135     LevelsMax = 0;
136     Hop_ManForEachPo( p, pObj, i )
137         LevelsMax = Abc_MaxInt( LevelsMax, (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData );
138     return LevelsMax;
139 }
140 
141 /**Function*************************************************************
142 
143   Synopsis    [Creates correct reference counters at each node.]
144 
145   Description []
146 
147   SideEffects []
148 
149   SeeAlso     []
150 
151 ***********************************************************************/
Hop_ManCreateRefs(Hop_Man_t * p)152 void Hop_ManCreateRefs( Hop_Man_t * p )
153 {
154     Hop_Obj_t * pObj;
155     int i;
156     if ( p->fRefCount )
157         return;
158     p->fRefCount = 1;
159     // clear refs
160     Hop_ObjClearRef( Hop_ManConst1(p) );
161     Hop_ManForEachPi( p, pObj, i )
162         Hop_ObjClearRef( pObj );
163     Hop_ManForEachNode( p, pObj, i )
164         Hop_ObjClearRef( pObj );
165     Hop_ManForEachPo( p, pObj, i )
166         Hop_ObjClearRef( pObj );
167     // set refs
168     Hop_ManForEachNode( p, pObj, i )
169     {
170         Hop_ObjRef( Hop_ObjFanin0(pObj) );
171         Hop_ObjRef( Hop_ObjFanin1(pObj) );
172     }
173     Hop_ManForEachPo( p, pObj, i )
174         Hop_ObjRef( Hop_ObjFanin0(pObj) );
175 }
176 
177 /**Function*************************************************************
178 
179   Synopsis    [Counts the number of AIG nodes rooted at this cone.]
180 
181   Description []
182 
183   SideEffects []
184 
185   SeeAlso     []
186 
187 ***********************************************************************/
Hop_ConeMark_rec(Hop_Obj_t * pObj)188 void Hop_ConeMark_rec( Hop_Obj_t * pObj )
189 {
190     assert( !Hop_IsComplement(pObj) );
191     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
192         return;
193     Hop_ConeMark_rec( Hop_ObjFanin0(pObj) );
194     Hop_ConeMark_rec( Hop_ObjFanin1(pObj) );
195     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
196     Hop_ObjSetMarkA( pObj );
197 }
198 
199 /**Function*************************************************************
200 
201   Synopsis    [Counts the number of AIG nodes rooted at this cone.]
202 
203   Description []
204 
205   SideEffects []
206 
207   SeeAlso     []
208 
209 ***********************************************************************/
Hop_ConeCleanAndMark_rec(Hop_Obj_t * pObj)210 void Hop_ConeCleanAndMark_rec( Hop_Obj_t * pObj )
211 {
212     assert( !Hop_IsComplement(pObj) );
213     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
214         return;
215     Hop_ConeCleanAndMark_rec( Hop_ObjFanin0(pObj) );
216     Hop_ConeCleanAndMark_rec( Hop_ObjFanin1(pObj) );
217     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
218     Hop_ObjSetMarkA( pObj );
219     pObj->pData = NULL;
220 }
221 
222 /**Function*************************************************************
223 
224   Synopsis    [Counts the number of AIG nodes rooted at this cone.]
225 
226   Description []
227 
228   SideEffects []
229 
230   SeeAlso     []
231 
232 ***********************************************************************/
Hop_ConeCountAndMark_rec(Hop_Obj_t * pObj)233 int Hop_ConeCountAndMark_rec( Hop_Obj_t * pObj )
234 {
235     int Counter;
236     assert( !Hop_IsComplement(pObj) );
237     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
238         return 0;
239     Counter = 1 + Hop_ConeCountAndMark_rec( Hop_ObjFanin0(pObj) ) +
240         Hop_ConeCountAndMark_rec( Hop_ObjFanin1(pObj) );
241     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
242     Hop_ObjSetMarkA( pObj );
243     return Counter;
244 }
245 
246 /**Function*************************************************************
247 
248   Synopsis    [Counts the number of AIG nodes rooted at this cone.]
249 
250   Description []
251 
252   SideEffects []
253 
254   SeeAlso     []
255 
256 ***********************************************************************/
Hop_ConeUnmark_rec(Hop_Obj_t * pObj)257 void Hop_ConeUnmark_rec( Hop_Obj_t * pObj )
258 {
259     assert( !Hop_IsComplement(pObj) );
260     if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
261         return;
262     Hop_ConeUnmark_rec( Hop_ObjFanin0(pObj) );
263     Hop_ConeUnmark_rec( Hop_ObjFanin1(pObj) );
264     assert( Hop_ObjIsMarkA(pObj) ); // loop detection
265     Hop_ObjClearMarkA( pObj );
266 }
267 
268 /**Function*************************************************************
269 
270   Synopsis    [Counts the number of AIG nodes rooted at this cone.]
271 
272   Description []
273 
274   SideEffects []
275 
276   SeeAlso     []
277 
278 ***********************************************************************/
Hop_DagSize(Hop_Obj_t * pObj)279 int Hop_DagSize( Hop_Obj_t * pObj )
280 {
281     int Counter;
282     Counter = Hop_ConeCountAndMark_rec( Hop_Regular(pObj) );
283     Hop_ConeUnmark_rec( Hop_Regular(pObj) );
284     return Counter;
285 }
286 
287 /**Function*************************************************************
288 
289   Synopsis    [Counts how many fanout the given node has.]
290 
291   Description []
292 
293   SideEffects []
294 
295   SeeAlso     []
296 
297 ***********************************************************************/
Hop_ObjFanoutCount_rec(Hop_Obj_t * pObj,Hop_Obj_t * pPivot)298 int Hop_ObjFanoutCount_rec( Hop_Obj_t * pObj, Hop_Obj_t * pPivot )
299 {
300     int Counter;
301     assert( !Hop_IsComplement(pObj) );
302     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
303         return (int)(pObj == pPivot);
304     Counter = Hop_ObjFanoutCount_rec( Hop_ObjFanin0(pObj), pPivot ) +
305               Hop_ObjFanoutCount_rec( Hop_ObjFanin1(pObj), pPivot );
306     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
307     Hop_ObjSetMarkA( pObj );
308     return Counter;
309 }
Hop_ObjFanoutCount(Hop_Obj_t * pObj,Hop_Obj_t * pPivot)310 int Hop_ObjFanoutCount( Hop_Obj_t * pObj, Hop_Obj_t * pPivot )
311 {
312     int Counter;
313     assert( !Hop_IsComplement(pPivot) );
314     Counter = Hop_ObjFanoutCount_rec( Hop_Regular(pObj), pPivot );
315     Hop_ConeUnmark_rec( Hop_Regular(pObj) );
316     return Counter;
317 }
318 
319 /**Function*************************************************************
320 
321   Synopsis    [Transfers the AIG from one manager into another.]
322 
323   Description []
324 
325   SideEffects []
326 
327   SeeAlso     []
328 
329 ***********************************************************************/
Hop_Transfer_rec(Hop_Man_t * pDest,Hop_Obj_t * pObj)330 void Hop_Transfer_rec( Hop_Man_t * pDest, Hop_Obj_t * pObj )
331 {
332     assert( !Hop_IsComplement(pObj) );
333     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
334         return;
335     Hop_Transfer_rec( pDest, Hop_ObjFanin0(pObj) );
336     Hop_Transfer_rec( pDest, Hop_ObjFanin1(pObj) );
337     pObj->pData = Hop_And( pDest, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
338     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
339     Hop_ObjSetMarkA( pObj );
340 }
341 
342 /**Function*************************************************************
343 
344   Synopsis    [Transfers the AIG from one manager into another.]
345 
346   Description []
347 
348   SideEffects []
349 
350   SeeAlso     []
351 
352 ***********************************************************************/
Hop_Transfer(Hop_Man_t * pSour,Hop_Man_t * pDest,Hop_Obj_t * pRoot,int nVars)353 Hop_Obj_t * Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pRoot, int nVars )
354 {
355     Hop_Obj_t * pObj;
356     int i;
357     // solve simple cases
358     if ( pSour == pDest )
359         return pRoot;
360     if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
361         return Hop_NotCond( Hop_ManConst1(pDest), Hop_IsComplement(pRoot) );
362     // set the PI mapping
363     Hop_ManForEachPi( pSour, pObj, i )
364     {
365         if ( i == nVars )
366            break;
367         pObj->pData = Hop_IthVar(pDest, i);
368     }
369     // transfer and set markings
370     Hop_Transfer_rec( pDest, Hop_Regular(pRoot) );
371     // clear the markings
372     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
373     return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
374 }
375 
376 /**Function*************************************************************
377 
378   Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
379 
380   Description []
381 
382   SideEffects []
383 
384   SeeAlso     []
385 
386 ***********************************************************************/
Hop_Compose_rec(Hop_Man_t * p,Hop_Obj_t * pObj,Hop_Obj_t * pFunc,Hop_Obj_t * pVar)387 void Hop_Compose_rec( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFunc, Hop_Obj_t * pVar )
388 {
389     assert( !Hop_IsComplement(pObj) );
390     if ( Hop_ObjIsMarkA(pObj) )
391         return;
392     if ( Hop_ObjIsConst1(pObj) || Hop_ObjIsPi(pObj) )
393     {
394         pObj->pData = pObj == pVar ? pFunc : pObj;
395         return;
396     }
397     Hop_Compose_rec( p, Hop_ObjFanin0(pObj), pFunc, pVar );
398     Hop_Compose_rec( p, Hop_ObjFanin1(pObj), pFunc, pVar );
399     pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
400     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
401     Hop_ObjSetMarkA( pObj );
402 }
403 
404 /**Function*************************************************************
405 
406   Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
407 
408   Description []
409 
410   SideEffects []
411 
412   SeeAlso     []
413 
414 ***********************************************************************/
Hop_Compose(Hop_Man_t * p,Hop_Obj_t * pRoot,Hop_Obj_t * pFunc,int iVar)415 Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar )
416 {
417     // quit if the PI variable is not defined
418     if ( iVar >= Hop_ManPiNum(p) )
419     {
420         printf( "Hop_Compose(): The PI variable %d is not defined.\n", iVar );
421         return NULL;
422     }
423     // recursively perform composition
424     Hop_Compose_rec( p, Hop_Regular(pRoot), pFunc, Hop_ManPi(p, iVar) );
425     // clear the markings
426     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
427     return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
428 }
429 
430 /**Function*************************************************************
431 
432   Synopsis    [Complements the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
433 
434   Description []
435 
436   SideEffects []
437 
438   SeeAlso     []
439 
440 ***********************************************************************/
Hop_Complement_rec(Hop_Man_t * p,Hop_Obj_t * pObj,Hop_Obj_t * pVar)441 void Hop_Complement_rec( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pVar )
442 {
443     assert( !Hop_IsComplement(pObj) );
444     if ( Hop_ObjIsMarkA(pObj) )
445         return;
446     if ( Hop_ObjIsConst1(pObj) || Hop_ObjIsPi(pObj) )
447     {
448         pObj->pData = pObj == pVar ? Hop_Not(pObj) : pObj;
449         return;
450     }
451     Hop_Complement_rec( p, Hop_ObjFanin0(pObj), pVar );
452     Hop_Complement_rec( p, Hop_ObjFanin1(pObj), pVar );
453     pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
454     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
455     Hop_ObjSetMarkA( pObj );
456 }
457 
458 /**Function*************************************************************
459 
460   Synopsis    [Complements the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
461 
462   Description []
463 
464   SideEffects []
465 
466   SeeAlso     []
467 
468 ***********************************************************************/
Hop_Complement(Hop_Man_t * p,Hop_Obj_t * pRoot,int iVar)469 Hop_Obj_t * Hop_Complement( Hop_Man_t * p, Hop_Obj_t * pRoot, int iVar )
470 {
471     // quit if the PI variable is not defined
472     if ( iVar >= Hop_ManPiNum(p) )
473     {
474         printf( "Hop_Complement(): The PI variable %d is not defined.\n", iVar );
475         return NULL;
476     }
477     // recursively perform composition
478     Hop_Complement_rec( p, Hop_Regular(pRoot), Hop_ManPi(p, iVar) );
479     // clear the markings
480     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
481     return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
482 }
483 
484 /**Function*************************************************************
485 
486   Synopsis    [Remaps the AIG (pRoot) to have the given support (uSupp).]
487 
488   Description []
489 
490   SideEffects []
491 
492   SeeAlso     []
493 
494 ***********************************************************************/
Hop_Remap_rec(Hop_Man_t * p,Hop_Obj_t * pObj)495 void Hop_Remap_rec( Hop_Man_t * p, Hop_Obj_t * pObj )
496 {
497     assert( !Hop_IsComplement(pObj) );
498     if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
499         return;
500     Hop_Remap_rec( p, Hop_ObjFanin0(pObj) );
501     Hop_Remap_rec( p, Hop_ObjFanin1(pObj) );
502     pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
503     assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
504     Hop_ObjSetMarkA( pObj );
505 }
506 
507 /**Function*************************************************************
508 
509   Synopsis    [Remaps the AIG (pRoot) to have the given support (uSupp).]
510 
511   Description []
512 
513   SideEffects []
514 
515   SeeAlso     []
516 
517 ***********************************************************************/
Hop_Remap(Hop_Man_t * p,Hop_Obj_t * pRoot,unsigned uSupp,int nVars)518 Hop_Obj_t * Hop_Remap( Hop_Man_t * p, Hop_Obj_t * pRoot, unsigned uSupp, int nVars )
519 {
520     Hop_Obj_t * pObj;
521     int i, k;
522     // quit if the PI variable is not defined
523     if ( nVars > Hop_ManPiNum(p) )
524     {
525         printf( "Hop_Remap(): The number of variables (%d) is more than the manager size (%d).\n", nVars, Hop_ManPiNum(p) );
526         return NULL;
527     }
528     // return if constant
529     if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
530         return pRoot;
531     if ( uSupp == 0 )
532         return Hop_NotCond( Hop_ManConst0(p), Hop_ObjPhaseCompl(pRoot) );
533     // set the PI mapping
534     k = 0;
535     Hop_ManForEachPi( p, pObj, i )
536     {
537         if ( i == nVars )
538            break;
539         if ( uSupp & (1 << i) )
540             pObj->pData = Hop_IthVar(p, k++);
541         else
542             pObj->pData = Hop_ManConst0(p);
543     }
544     assert( k > 0 && k < nVars );
545     // recursively perform composition
546     Hop_Remap_rec( p, Hop_Regular(pRoot) );
547     // clear the markings
548     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
549     return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
550 }
551 
552 /**Function*************************************************************
553 
554   Synopsis    [Permute the AIG according to the given permutation.]
555 
556   Description []
557 
558   SideEffects []
559 
560   SeeAlso     []
561 
562 ***********************************************************************/
Hop_Permute(Hop_Man_t * p,Hop_Obj_t * pRoot,int nRootVars,int * pPermute)563 Hop_Obj_t * Hop_Permute( Hop_Man_t * p, Hop_Obj_t * pRoot, int nRootVars, int * pPermute )
564 {
565     Hop_Obj_t * pObj;
566     int i;
567     // return if constant
568     if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
569         return pRoot;
570     // create mapping
571     Hop_ManForEachPi( p, pObj, i )
572     {
573         if ( i == nRootVars )
574             break;
575         assert( pPermute[i] >= 0 && pPermute[i] < Hop_ManPiNum(p) );
576         pObj->pData = Hop_IthVar( p, pPermute[i] );
577     }
578     // recursively perform composition
579     Hop_Remap_rec( p, Hop_Regular(pRoot) );
580     // clear the markings
581     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
582     return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
583 }
584 
585 ////////////////////////////////////////////////////////////////////////
586 ///                       END OF FILE                                ///
587 ////////////////////////////////////////////////////////////////////////
588 
589 
590 ABC_NAMESPACE_IMPL_END
591 
592