1 /**CFile****************************************************************
2
3 FileName [giaClp.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Collapsing AIG.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22
23 #ifdef ABC_USE_CUDD
24 #include "bdd/extrab/extraBdd.h"
25 #include "bdd/dsd/dsd.h"
26 #endif
27
28 ABC_NAMESPACE_IMPL_START
29
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 #ifdef ABC_USE_CUDD
35
36 extern int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
37 extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
38 extern int Abc_NtkDeriveFlatGiaSop( Gia_Man_t * pGia, int * gFanins, char * pSop );
39 extern int Gia_ManFactorNode( Gia_Man_t * p, char * pSop, Vec_Int_t * vLeaves );
40
41 ////////////////////////////////////////////////////////////////////////
42 /// FUNCTION DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44
45 /**Function*************************************************************
46
47 Synopsis []
48
49 Description []
50
51 SideEffects []
52
53 SeeAlso []
54
55 ***********************************************************************/
Gia_GetFakeNames(int nNames)56 Vec_Ptr_t * Gia_GetFakeNames( int nNames )
57 {
58 Vec_Ptr_t * vNames;
59 char Buffer[5];
60 int i;
61
62 vNames = Vec_PtrAlloc( nNames );
63 for ( i = 0; i < nNames; i++ )
64 {
65 if ( nNames < 26 )
66 {
67 Buffer[0] = 'a' + i;
68 Buffer[1] = 0;
69 }
70 else
71 {
72 Buffer[0] = 'a' + i%26;
73 Buffer[1] = '0' + i/26;
74 Buffer[2] = 0;
75 }
76 Vec_PtrPush( vNames, Extra_UtilStrsav(Buffer) );
77 }
78 return vNames;
79 }
80
81 /**Function*************************************************************
82
83 Synopsis []
84
85 Description []
86
87 SideEffects []
88
89 SeeAlso []
90
91 ***********************************************************************/
Gia_ManRebuildIsop(DdManager * dd,DdNode * bLocal,Gia_Man_t * pNew,Vec_Int_t * vFanins,Vec_Str_t * vSop,Vec_Str_t * vCube)92 int Gia_ManRebuildIsop( DdManager * dd, DdNode * bLocal, Gia_Man_t * pNew, Vec_Int_t * vFanins, Vec_Str_t * vSop, Vec_Str_t * vCube )
93 {
94 char * pSop;
95 DdNode * bCover, * zCover, * zCover0, * zCover1;
96 int nFanins = Vec_IntSize(vFanins);
97 int fPhase, nCubes, nCubes0, nCubes1;
98
99 // get the ZDD of the negative polarity
100 bCover = Cudd_zddIsop( dd, Cudd_Not(bLocal), Cudd_Not(bLocal), &zCover0 );
101 Cudd_Ref( zCover0 );
102 Cudd_Ref( bCover );
103 Cudd_RecursiveDeref( dd, bCover );
104 nCubes0 = Abc_CountZddCubes( dd, zCover0 );
105
106 // get the ZDD of the positive polarity
107 bCover = Cudd_zddIsop( dd, bLocal, bLocal, &zCover1 );
108 Cudd_Ref( zCover1 );
109 Cudd_Ref( bCover );
110 Cudd_RecursiveDeref( dd, bCover );
111 nCubes1 = Abc_CountZddCubes( dd, zCover1 );
112
113 // compare the number of cubes
114 if ( nCubes1 <= nCubes0 )
115 { // use positive polarity
116 nCubes = nCubes1;
117 zCover = zCover1;
118 Cudd_RecursiveDerefZdd( dd, zCover0 );
119 fPhase = 1;
120 }
121 else
122 { // use negative polarity
123 nCubes = nCubes0;
124 zCover = zCover0;
125 Cudd_RecursiveDerefZdd( dd, zCover1 );
126 fPhase = 0;
127 }
128 if ( nCubes > 1000 )
129 {
130 Cudd_RecursiveDerefZdd( dd, zCover );
131 return -1;
132 }
133
134 // allocate memory for the cover
135 Vec_StrGrow( vSop, (nFanins + 3) * nCubes + 1 );
136 pSop = Vec_StrArray( vSop );
137 pSop[(nFanins + 3) * nCubes] = 0;
138 // create the SOP
139 Vec_StrFill( vCube, nFanins, '-' );
140 Vec_StrPush( vCube, '\0' );
141 Abc_ConvertZddToSop( dd, zCover, pSop, nFanins, vCube, fPhase );
142 Cudd_RecursiveDerefZdd( dd, zCover );
143
144 // perform factoring
145 // return Abc_NtkDeriveFlatGiaSop( pNew, Vec_IntArray(vFanins), pSop );
146 return Gia_ManFactorNode( pNew, pSop, vFanins );
147 }
Gia_ManRebuildNode(Dsd_Manager_t * pManDsd,Dsd_Node_t * pNodeDsd,Gia_Man_t * pNew,DdManager * ddNew,Vec_Int_t * vFanins,Vec_Str_t * vSop,Vec_Str_t * vCube)148 int Gia_ManRebuildNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Gia_Man_t * pNew, DdManager * ddNew, Vec_Int_t * vFanins, Vec_Str_t * vSop, Vec_Str_t * vCube )
149 {
150 DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd );
151 DdNode * bLocal, * bTemp;
152 Dsd_Node_t * pFaninDsd;
153 Dsd_Type_t Type;
154 int i, nDecs, iLit = -1;
155
156 // add the fanins
157 Type = Dsd_NodeReadType( pNodeDsd );
158 nDecs = Dsd_NodeReadDecsNum( pNodeDsd );
159 assert( nDecs > 1 );
160 Vec_IntClear( vFanins );
161 for ( i = 0; i < nDecs; i++ )
162 {
163 pFaninDsd = Dsd_NodeReadDec( pNodeDsd, i );
164 iLit = Dsd_NodeReadMark( Dsd_Regular(pFaninDsd) );
165 iLit = Abc_LitNotCond( iLit, Dsd_IsComplement(pFaninDsd) );
166 assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) );
167 Vec_IntPush( vFanins, iLit );
168 }
169
170 // create the local function depending on the type of the node
171 switch ( Type )
172 {
173 case DSD_NODE_CONST1:
174 {
175 iLit = 1;
176 break;
177 }
178 case DSD_NODE_OR:
179 {
180 iLit = 0;
181 for ( i = 0; i < nDecs; i++ )
182 iLit = Gia_ManHashOr( pNew, iLit, Vec_IntEntry(vFanins, i) );
183 break;
184 }
185 case DSD_NODE_EXOR:
186 {
187 iLit = 0;
188 for ( i = 0; i < nDecs; i++ )
189 iLit = Gia_ManHashXor( pNew, iLit, Vec_IntEntry(vFanins, i) );
190 break;
191 }
192 case DSD_NODE_PRIME:
193 {
194 bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd ); Cudd_Ref( bLocal );
195 bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal );
196 Cudd_RecursiveDeref( ddDsd, bTemp );
197 // bLocal is now in the new BDD manager
198 iLit = Gia_ManRebuildIsop( ddNew, bLocal, pNew, vFanins, vSop, vCube );
199 Cudd_RecursiveDeref( ddNew, bLocal );
200 break;
201 }
202 default:
203 {
204 assert( 0 );
205 break;
206 }
207 }
208 Dsd_NodeSetMark( pNodeDsd, iLit );
209 return iLit;
210 }
Gia_ManRebuild(Gia_Man_t * p,Dsd_Manager_t * pManDsd,DdManager * ddNew)211 Gia_Man_t * Gia_ManRebuild( Gia_Man_t * p, Dsd_Manager_t * pManDsd, DdManager * ddNew )
212 {
213 Gia_Man_t * pNew;
214 Dsd_Node_t ** ppNodesDsd;
215 Dsd_Node_t * pNodeDsd;
216 int i, nNodesDsd, iLit = -1;
217 Vec_Str_t * vSop, * vCube;
218 Vec_Int_t * vFanins;
219
220 vFanins = Vec_IntAlloc( 1000 );
221 vSop = Vec_StrAlloc( 10000 );
222 vCube = Vec_StrAlloc( 1000 );
223
224 pNew = Gia_ManStart( 2*Gia_ManObjNum(p) );
225 pNew->pName = Abc_UtilStrsav( p->pName );
226 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
227 Gia_ManHashAlloc( pNew );
228
229 // save the CI nodes in the DSD nodes
230 Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), 1 );
231 for ( i = 0; i < Gia_ManCiNum(p); i++ )
232 {
233 pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
234 Dsd_NodeSetMark( pNodeDsd, Gia_ManAppendCi( pNew ) );
235 }
236
237 // collect DSD nodes in DFS order (leaves and const1 are not collected)
238 ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd );
239 for ( i = 0; i < nNodesDsd; i++ )
240 {
241 iLit = Gia_ManRebuildNode( pManDsd, ppNodesDsd[i], pNew, ddNew, vFanins, vSop, vCube );
242 if ( iLit == -1 )
243 break;
244 }
245 ABC_FREE( ppNodesDsd );
246 Vec_IntFree( vFanins );
247 Vec_StrFree( vSop );
248 Vec_StrFree( vCube );
249 if ( iLit == -1 )
250 {
251 Gia_ManStop( pNew );
252 return Gia_ManDup(p);
253 }
254
255 // set the pointers to the CO drivers
256 for ( i = 0; i < Gia_ManCoNum(p); i++ )
257 {
258 pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
259 iLit = Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
260 iLit = Abc_LitNotCond( iLit, Dsd_IsComplement(pNodeDsd) );
261 Gia_ManAppendCo( pNew, iLit );
262 }
263 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
264 return pNew;
265 }
266
267 /**Function*************************************************************
268
269 Synopsis []
270
271 Description []
272
273 SideEffects []
274
275 SeeAlso []
276
277 ***********************************************************************/
Gia_ManCollapseDeref(DdManager * dd,Vec_Ptr_t * vFuncs)278 void Gia_ManCollapseDeref( DdManager * dd, Vec_Ptr_t * vFuncs )
279 {
280 DdNode * bFunc; int i;
281 Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
282 if ( bFunc )
283 Cudd_RecursiveDeref( dd, bFunc );
284 Vec_PtrFree( vFuncs );
285 }
Gia_ObjCollapseDeref(Gia_Man_t * p,DdManager * dd,Vec_Ptr_t * vFuncs,int Id)286 void Gia_ObjCollapseDeref( Gia_Man_t * p, DdManager * dd, Vec_Ptr_t * vFuncs, int Id )
287 {
288 if ( Gia_ObjRefDecId(p, Id) )
289 return;
290 Cudd_RecursiveDeref( dd, (DdNode *)Vec_PtrEntry(vFuncs, Id) );
291 Vec_PtrWriteEntry( vFuncs, Id, NULL );
292 }
Gia_ManCollapse(Gia_Man_t * p,DdManager * dd,int nBddLimit,int fVerbose)293 Vec_Ptr_t * Gia_ManCollapse( Gia_Man_t * p, DdManager * dd, int nBddLimit, int fVerbose )
294 {
295 Vec_Ptr_t * vFuncs;
296 DdNode * bFunc0, * bFunc1, * bFunc;
297 Gia_Obj_t * pObj;
298 int i, Id;
299 Gia_ManCreateRefs( p );
300 // assign constant node
301 vFuncs = Vec_PtrStart( Gia_ManObjNum(p) );
302 if ( Gia_ObjRefNumId(p, 0) > 0 )
303 Vec_PtrWriteEntry( vFuncs, 0, Cudd_ReadLogicZero(dd) ), Cudd_Ref(Cudd_ReadLogicZero(dd));
304 // assign elementary variables
305 Gia_ManForEachCiId( p, Id, i )
306 if ( Gia_ObjRefNumId(p, Id) > 0 )
307 Vec_PtrWriteEntry( vFuncs, Id, Cudd_bddIthVar(dd,i) ), Cudd_Ref(Cudd_bddIthVar(dd,i));
308 // create BDD for AND nodes
309 Gia_ManForEachAnd( p, pObj, i )
310 {
311 bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj) );
312 bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj) );
313 bFunc = Cudd_bddAndLimit( dd, bFunc0, bFunc1, nBddLimit );
314 if ( bFunc == NULL )
315 {
316 Gia_ManCollapseDeref( dd, vFuncs );
317 return NULL;
318 }
319 Cudd_Ref( bFunc );
320 Vec_PtrWriteEntry( vFuncs, i, bFunc );
321 Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId0(pObj, i) );
322 Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId1(pObj, i) );
323 }
324 // create BDD for outputs
325 Gia_ManForEachCoId( p, Id, i )
326 {
327 pObj = Gia_ManCo( p, i );
328 bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId0(pObj, Id)), Gia_ObjFaninC0(pObj) );
329 Vec_PtrWriteEntry( vFuncs, Id, bFunc0 ); Cudd_Ref( bFunc0 );
330 Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId0(pObj, Id) );
331 }
332 assert( Vec_PtrSize(vFuncs) == Vec_PtrCountZero(vFuncs) + Gia_ManCoNum(p) );
333 // compact
334 Gia_ManForEachCoId( p, Id, i )
335 Vec_PtrWriteEntry( vFuncs, i, Vec_PtrEntry(vFuncs, Id) );
336 Vec_PtrShrink( vFuncs, Gia_ManCoNum(p) );
337 return vFuncs;
338 }
339
340 /**Function*************************************************************
341
342 Synopsis []
343
344 Description []
345
346 SideEffects []
347
348 SeeAlso []
349
350 ***********************************************************************/
Gia_ManCollapseTest(Gia_Man_t * p,int fVerbose)351 Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
352 {
353 Gia_Man_t * pNew;
354 DdManager * dd, * ddNew;
355 Dsd_Manager_t * pManDsd;
356 Vec_Ptr_t * vFuncs;
357 // derive global BDDs
358 dd = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
359 Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
360 vFuncs = Gia_ManCollapse( p, dd, 10000, 0 );
361 Cudd_AutodynDisable( dd );
362 if ( vFuncs == NULL )
363 {
364 Extra_StopManager( dd );
365 return Gia_ManDup(p);
366 }
367 // start ISOP manager
368 ddNew = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
369 Cudd_zddVarsFromBddVars( ddNew, 2 );
370 // Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
371 if ( fVerbose )
372 printf( "Ins = %d. Outs = %d. Shared BDD nodes = %d. Peak live nodes = %d. Peak nodes = %d.\n",
373 Gia_ManCiNum(p), Gia_ManCoNum(p),
374 Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) ),
375 Cudd_ReadPeakLiveNodeCount(dd), (int)Cudd_ReadNodeCount(dd) );
376 // perform decomposition
377 pManDsd = Dsd_ManagerStart( dd, Gia_ManCiNum(p), 0 );
378 Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
379 if ( fVerbose )
380 {
381 Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) );
382 Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
383 char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
384 char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
385 Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1 );
386 Vec_PtrFreeFree( vNamesCi );
387 Vec_PtrFreeFree( vNamesCo );
388 }
389
390 pNew = Gia_ManRebuild( p, pManDsd, ddNew );
391 Dsd_ManagerStop( pManDsd );
392 // return manager
393 Gia_ManCollapseDeref( dd, vFuncs );
394 Extra_StopManager( dd );
395 Extra_StopManager( ddNew );
396 return pNew;
397 }
Gia_ManCollapseTestTest(Gia_Man_t * p)398 void Gia_ManCollapseTestTest( Gia_Man_t * p )
399 {
400 Gia_Man_t * pNew;
401 pNew = Gia_ManCollapseTest( p, 0 );
402 Gia_ManPrintStats( p, NULL );
403 Gia_ManPrintStats( pNew, NULL );
404 Gia_ManStop( pNew );
405 }
406
407 #else
408
409 Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
410 {
411 return NULL;
412 }
413
414 #endif
415
416 ////////////////////////////////////////////////////////////////////////
417 /// END OF FILE ///
418 ////////////////////////////////////////////////////////////////////////
419
420
421 ABC_NAMESPACE_IMPL_END
422
423