1 /**CFile****************************************************************
2
3 FileName [abcNtbdd.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [Procedures to translate between the BDD and the network.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: abcNtbdd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "base/abc/abc.h"
22 #include "aig/saig/saig.h"
23
24 #ifdef ABC_USE_CUDD
25 #include "bdd/extrab/extraBdd.h"
26 #endif
27
28 ABC_NAMESPACE_IMPL_START
29
30
31 ////////////////////////////////////////////////////////////////////////
32 /// DECLARATIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 #ifdef ABC_USE_CUDD
36
37 static int Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int Limit );
38 static void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
39 static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew );
40 static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st__table * tBdd2Node );
41 static DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose );
42
43 ////////////////////////////////////////////////////////////////////////
44 /// FUNCTION DEFINITIONS ///
45 ////////////////////////////////////////////////////////////////////////
46
47 /**Function*************************************************************
48
49 Synopsis [Constructs the network isomorphic to the given BDD.]
50
51 Description [Assumes that the BDD depends on the variables whose indexes
52 correspond to the names in the array (pNamesPi). Otherwise, returns NULL.
53 The resulting network comes with one node, whose functionality is
54 equal to the given BDD. To decompose this BDD into the network of
55 multiplexers use Abc_NtkBddToMuxes(). To decompose this BDD into
56 an And-Inverter Graph, use Abc_NtkStrash().]
57
58 SideEffects []
59
60 SeeAlso []
61
62 ***********************************************************************/
Abc_NtkDeriveFromBdd(void * dd0,void * bFunc,char * pNamePo,Vec_Ptr_t * vNamesPi)63 Abc_Ntk_t * Abc_NtkDeriveFromBdd( void * dd0, void * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi )
64 {
65 DdManager * dd = (DdManager *)dd0;
66 Abc_Ntk_t * pNtk;
67 Vec_Ptr_t * vNamesPiFake = NULL;
68 Abc_Obj_t * pNode, * pNodePi, * pNodePo;
69 DdNode * bSupp, * bTemp;
70 char * pName;
71 int i;
72
73 // supply fake names if real names are not given
74 if ( pNamePo == NULL )
75 pNamePo = "F";
76 if ( vNamesPi == NULL )
77 {
78 vNamesPiFake = Abc_NodeGetFakeNames( dd->size );
79 vNamesPi = vNamesPiFake;
80 }
81
82 // make sure BDD depends on the variables whose index
83 // does not exceed the size of the array with PI names
84 bSupp = Cudd_Support( dd, (DdNode *)bFunc ); Cudd_Ref( bSupp );
85 for ( bTemp = bSupp; bTemp != Cudd_ReadOne(dd); bTemp = cuddT(bTemp) )
86 if ( (int)Cudd_NodeReadIndex(bTemp) >= Vec_PtrSize(vNamesPi) )
87 break;
88 Cudd_RecursiveDeref( dd, bSupp );
89 if ( bTemp != Cudd_ReadOne(dd) )
90 return NULL;
91
92 // start the network
93 pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
94 pNtk->pName = Extra_UtilStrsav(pNamePo);
95 // make sure the new manager has enough inputs
96 Cudd_bddIthVar( (DdManager *)pNtk->pManFunc, Vec_PtrSize(vNamesPi) );
97 // add the PIs corresponding to the names
98 Vec_PtrForEachEntry( char *, vNamesPi, pName, i )
99 Abc_ObjAssignName( Abc_NtkCreatePi(pNtk), pName, NULL );
100 // create the node
101 pNode = Abc_NtkCreateNode( pNtk );
102 pNode->pData = (DdNode *)Cudd_bddTransfer( dd, (DdManager *)pNtk->pManFunc, (DdNode *)bFunc ); Cudd_Ref((DdNode *)pNode->pData);
103 Abc_NtkForEachPi( pNtk, pNodePi, i )
104 Abc_ObjAddFanin( pNode, pNodePi );
105 // create the only PO
106 pNodePo = Abc_NtkCreatePo( pNtk );
107 Abc_ObjAddFanin( pNodePo, pNode );
108 Abc_ObjAssignName( pNodePo, pNamePo, NULL );
109 // make the network minimum base
110 Abc_NtkMinimumBase( pNtk );
111 if ( vNamesPiFake )
112 Abc_NodeFreeNames( vNamesPiFake );
113 if ( !Abc_NtkCheck( pNtk ) )
114 fprintf( stdout, "Abc_NtkDeriveFromBdd(): Network check has failed.\n" );
115 return pNtk;
116 }
117
118
119
120 /**Function*************************************************************
121
122 Synopsis [Creates the network isomorphic to the union of local BDDs of the nodes.]
123
124 Description [The nodes of the local BDDs are converted into the network nodes
125 with logic functions equal to the MUX.]
126
127 SideEffects []
128
129 SeeAlso []
130
131 ***********************************************************************/
Abc_NtkBddToMuxes(Abc_Ntk_t * pNtk,int fGlobal,int Limit)132 Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk, int fGlobal, int Limit )
133 {
134 Abc_Ntk_t * pNtkNew;
135 pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
136 if ( fGlobal )
137 {
138 if ( !Abc_NtkBddToMuxesPerformGlo( pNtk, pNtkNew, Limit ) )
139 return NULL;
140 }
141 else
142 {
143 Abc_NtkBddToMuxesPerform( pNtk, pNtkNew );
144 Abc_NtkFinalize( pNtk, pNtkNew );
145 }
146 // make sure everything is okay
147 if ( !Abc_NtkCheck( pNtkNew ) )
148 {
149 printf( "Abc_NtkBddToMuxes: The network check has failed.\n" );
150 Abc_NtkDelete( pNtkNew );
151 return NULL;
152 }
153 return pNtkNew;
154 }
155
156 /**Function*************************************************************
157
158 Synopsis [Converts the network to MUXes.]
159
160 Description []
161
162 SideEffects []
163
164 SeeAlso []
165
166 ***********************************************************************/
Abc_NtkBddToMuxesPerform(Abc_Ntk_t * pNtk,Abc_Ntk_t * pNtkNew)167 void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
168 {
169 ProgressBar * pProgress;
170 Abc_Obj_t * pNode, * pNodeNew;
171 Vec_Ptr_t * vNodes;
172 int i;
173 assert( Abc_NtkIsBddLogic(pNtk) );
174 // perform conversion in the topological order
175 vNodes = Abc_NtkDfs( pNtk, 0 );
176 pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
177 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
178 {
179 Extra_ProgressBarUpdate( pProgress, i, NULL );
180 // convert one node
181 assert( Abc_ObjIsNode(pNode) );
182 pNodeNew = Abc_NodeBddToMuxes( pNode, pNtkNew );
183 // mark the old node with the new one
184 assert( pNode->pCopy == NULL );
185 pNode->pCopy = pNodeNew;
186 }
187 Vec_PtrFree( vNodes );
188 Extra_ProgressBarStop( pProgress );
189 }
190
191 /**Function*************************************************************
192
193 Synopsis [Converts the node to MUXes.]
194
195 Description []
196
197 SideEffects []
198
199 SeeAlso []
200
201 ***********************************************************************/
Abc_NodeBddToMuxes(Abc_Obj_t * pNodeOld,Abc_Ntk_t * pNtkNew)202 Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
203 {
204 DdManager * dd = (DdManager *)pNodeOld->pNtk->pManFunc;
205 DdNode * bFunc = (DdNode *)pNodeOld->pData;
206 Abc_Obj_t * pFaninOld, * pNodeNew;
207 st__table * tBdd2Node;
208 int i;
209 // create the table mapping BDD nodes into the ABC nodes
210 tBdd2Node = st__init_table( st__ptrcmp, st__ptrhash );
211 // add the constant and the elementary vars
212 Abc_ObjForEachFanin( pNodeOld, pFaninOld, i )
213 st__insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pFaninOld->pCopy );
214 // create the new nodes recursively
215 pNodeNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node );
216 st__free_table( tBdd2Node );
217 if ( Cudd_IsComplement(bFunc) )
218 pNodeNew = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew );
219 return pNodeNew;
220 }
221
222 /**Function*************************************************************
223
224 Synopsis [Converts the node to MUXes.]
225
226 Description []
227
228 SideEffects []
229
230 SeeAlso []
231
232 ***********************************************************************/
Abc_NodeBddToMuxes_rec(DdManager * dd,DdNode * bFunc,Abc_Ntk_t * pNtkNew,st__table * tBdd2Node)233 Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st__table * tBdd2Node )
234 {
235 Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
236 assert( !Cudd_IsComplement(bFunc) );
237 if ( bFunc == b1 )
238 return Abc_NtkCreateNodeConst1(pNtkNew);
239 if ( st__lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
240 return pNodeNew;
241 // solve for the children nodes
242 pNodeNew0 = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(cuddE(bFunc)), pNtkNew, tBdd2Node );
243 if ( Cudd_IsComplement(cuddE(bFunc)) )
244 pNodeNew0 = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew0 );
245 pNodeNew1 = Abc_NodeBddToMuxes_rec( dd, cuddT(bFunc), pNtkNew, tBdd2Node );
246 if ( ! st__lookup( tBdd2Node, (char *)Cudd_bddIthVar(dd, bFunc->index), (char **)&pNodeNewC ) )
247 assert( 0 );
248 // create the MUX node
249 pNodeNew = Abc_NtkCreateNodeMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 );
250 st__insert( tBdd2Node, (char *)bFunc, (char *)pNodeNew );
251 return pNodeNew;
252 }
253
254 /**Function*************************************************************
255
256 Synopsis [Converts the node to MUXes.]
257
258 Description []
259
260 SideEffects []
261
262 SeeAlso []
263
264 ***********************************************************************/
Abc_NtkBddToMuxesPerformGlo(Abc_Ntk_t * pNtk,Abc_Ntk_t * pNtkNew,int Limit)265 int Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int Limit )
266 {
267 DdManager * dd;
268 Abc_Obj_t * pObj, * pObjNew; int i;
269 st__table * tBdd2Node;
270 assert( Abc_NtkIsStrash(pNtk) );
271 dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, Limit, 1, 1, 0, 0 );
272 if ( dd == NULL )
273 {
274 printf( "Construction of global BDDs has failed.\n" );
275 return 0;
276 }
277 //printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
278
279 tBdd2Node = st__init_table( st__ptrcmp, st__ptrhash );
280 Abc_NtkForEachCi( pNtkNew, pObjNew, i )
281 st__insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pObjNew );
282
283 // complement the global functions
284 Abc_NtkForEachCo( pNtk, pObj, i )
285 {
286 DdNode * bFunc = Abc_ObjGlobalBdd(pObj);
287 pObjNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node );
288 if ( Cudd_IsComplement(bFunc) )
289 pObjNew = Abc_NtkCreateNodeInv( pNtkNew, pObjNew );
290 Abc_ObjAddFanin( pObj->pCopy, pObjNew );
291 }
292
293 // cleanup
294 st__free_table( tBdd2Node );
295 Abc_NtkFreeGlobalBdds( pNtk, 0 );
296 Extra_StopManager( dd );
297 Abc_NtkCleanCopy( pNtk );
298 return 1;
299 }
300
301 /**Function*************************************************************
302
303 Synopsis [Derives global BDDs for the COs of the network.]
304
305 Description []
306
307 SideEffects []
308
309 SeeAlso []
310
311 ***********************************************************************/
Abc_NtkBuildGlobalBdds(Abc_Ntk_t * pNtk,int nBddSizeMax,int fDropInternal,int fReorder,int fReverse,int fVerbose)312 void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fReverse, int fVerbose )
313 {
314 ProgressBar * pProgress;
315 Abc_Obj_t * pObj, * pFanin;
316 Vec_Att_t * pAttMan;
317 DdManager * dd;
318 DdNode * bFunc;
319 int i, k, Counter;
320
321 // remove dangling nodes
322 Abc_AigCleanup( (Abc_Aig_t *)pNtk->pManFunc );
323
324 // start the manager
325 assert( Abc_NtkGlobalBdd(pNtk) == NULL );
326 dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
327 pAttMan = Vec_AttAlloc( Abc_NtkObjNumMax(pNtk) + 1, dd, (void (*)(void*))Extra_StopManager, NULL, (void (*)(void*,void*))Cudd_RecursiveDeref );
328 Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD, pAttMan );
329
330 // set reordering
331 if ( fReorder )
332 Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
333
334 // assign the constant node BDD
335 pObj = Abc_AigConst1(pNtk);
336 if ( Abc_ObjFanoutNum(pObj) > 0 )
337 {
338 bFunc = dd->one;
339 Abc_ObjSetGlobalBdd( pObj, bFunc ); Cudd_Ref( bFunc );
340 }
341 // set the elementary variables
342 Abc_NtkForEachCi( pNtk, pObj, i )
343 if ( Abc_ObjFanoutNum(pObj) > 0 )
344 {
345 bFunc = fReverse ? dd->vars[Abc_NtkCiNum(pNtk) - 1 - i] : dd->vars[i];
346 Abc_ObjSetGlobalBdd( pObj, bFunc ); Cudd_Ref( bFunc );
347 }
348
349 // collect the global functions of the COs
350 Counter = 0;
351 // construct the BDDs
352 pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
353 Abc_NtkForEachCo( pNtk, pObj, i )
354 {
355 bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose );
356 if ( bFunc == NULL )
357 {
358 if ( fVerbose )
359 printf( "Constructing global BDDs is aborted.\n" );
360 Abc_NtkFreeGlobalBdds( pNtk, 0 );
361 Cudd_Quit( dd );
362
363 // reset references
364 Abc_NtkForEachObj( pNtk, pObj, i )
365 if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) )
366 pObj->vFanouts.nSize = 0;
367 Abc_NtkForEachObj( pNtk, pObj, i )
368 if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
369 Abc_ObjForEachFanin( pObj, pFanin, k )
370 pFanin->vFanouts.nSize++;
371 return NULL;
372 }
373 bFunc = Cudd_NotCond( bFunc, (int)Abc_ObjFaninC0(pObj) ); Cudd_Ref( bFunc );
374 Abc_ObjSetGlobalBdd( pObj, bFunc );
375 }
376 Extra_ProgressBarStop( pProgress );
377
378 /*
379 // derefence the intermediate BDDs
380 Abc_NtkForEachNode( pNtk, pObj, i )
381 if ( pObj->pCopy )
382 {
383 Cudd_RecursiveDeref( dd, (DdNode *)pObj->pCopy );
384 pObj->pCopy = NULL;
385 }
386 */
387 /*
388 // make sure all nodes are derefed
389 Abc_NtkForEachObj( pNtk, pObj, i )
390 {
391 if ( pObj->pCopy != NULL )
392 printf( "Abc_NtkBuildGlobalBdds() error: Node %d has BDD assigned\n", pObj->Id );
393 if ( pObj->vFanouts.nSize > 0 )
394 printf( "Abc_NtkBuildGlobalBdds() error: Node %d has refs assigned\n", pObj->Id );
395 }
396 */
397 // reset references
398 Abc_NtkForEachObj( pNtk, pObj, i )
399 if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) )
400 pObj->vFanouts.nSize = 0;
401 Abc_NtkForEachObj( pNtk, pObj, i )
402 if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
403 Abc_ObjForEachFanin( pObj, pFanin, k )
404 pFanin->vFanouts.nSize++;
405
406 // reorder one more time
407 if ( fReorder )
408 {
409 Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
410 Cudd_AutodynDisable( dd );
411 }
412 // Cudd_PrintInfo( dd, stdout );
413 return dd;
414 }
415
416 /**Function*************************************************************
417
418 Synopsis [Derives the global BDD for one AIG node.]
419
420 Description []
421
422 SideEffects []
423
424 SeeAlso []
425
426 ***********************************************************************/
Abc_NodeGlobalBdds_rec(DdManager * dd,Abc_Obj_t * pNode,int nBddSizeMax,int fDropInternal,ProgressBar * pProgress,int * pCounter,int fVerbose)427 DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose )
428 {
429 DdNode * bFunc, * bFunc0, * bFunc1, * bFuncC;
430 int fDetectMuxes = 0;
431 assert( !Abc_ObjIsComplement(pNode) );
432 if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
433 {
434 Extra_ProgressBarStop( pProgress );
435 if ( fVerbose )
436 printf( "The number of live nodes reached %d.\n", nBddSizeMax );
437 fflush( stdout );
438 return NULL;
439 }
440 // if the result is available return
441 if ( Abc_ObjGlobalBdd(pNode) == NULL )
442 {
443 Abc_Obj_t * pNodeC, * pNode0, * pNode1;
444 pNode0 = Abc_ObjFanin0(pNode);
445 pNode1 = Abc_ObjFanin1(pNode);
446 // check for the special case when it is MUX/EXOR
447 if ( fDetectMuxes &&
448 Abc_ObjGlobalBdd(pNode0) == NULL && Abc_ObjGlobalBdd(pNode1) == NULL &&
449 Abc_ObjIsNode(pNode0) && Abc_ObjFanoutNum(pNode0) == 1 &&
450 Abc_ObjIsNode(pNode1) && Abc_ObjFanoutNum(pNode1) == 1 &&
451 Abc_NodeIsMuxType(pNode) )
452 {
453 // deref the fanins
454 pNode0->vFanouts.nSize--;
455 pNode1->vFanouts.nSize--;
456 // recognize the MUX
457 pNodeC = Abc_NodeRecognizeMux( pNode, &pNode1, &pNode0 );
458 assert( Abc_ObjFanoutNum(pNodeC) > 1 );
459 // dereference the control once (the second time it will be derefed when BDDs are computed)
460 pNodeC->vFanouts.nSize--;
461
462 // compute the result for all branches
463 bFuncC = Abc_NodeGlobalBdds_rec( dd, pNodeC, nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );
464 if ( bFuncC == NULL )
465 return NULL;
466 Cudd_Ref( bFuncC );
467 bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode0), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );
468 if ( bFunc0 == NULL )
469 return NULL;
470 Cudd_Ref( bFunc0 );
471 bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode1), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );
472 if ( bFunc1 == NULL )
473 return NULL;
474 Cudd_Ref( bFunc1 );
475
476 // complement the branch BDDs
477 bFunc0 = Cudd_NotCond( bFunc0, (int)Abc_ObjIsComplement(pNode0) );
478 bFunc1 = Cudd_NotCond( bFunc1, (int)Abc_ObjIsComplement(pNode1) );
479 // get the final result
480 bFunc = Cudd_bddIte( dd, bFuncC, bFunc1, bFunc0 ); Cudd_Ref( bFunc );
481 Cudd_RecursiveDeref( dd, bFunc0 );
482 Cudd_RecursiveDeref( dd, bFunc1 );
483 Cudd_RecursiveDeref( dd, bFuncC );
484 // add the number of used nodes
485 (*pCounter) += 3;
486 }
487 else
488 {
489 // compute the result for both branches
490 bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );
491 if ( bFunc0 == NULL )
492 return NULL;
493 Cudd_Ref( bFunc0 );
494 bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );
495 if ( bFunc1 == NULL )
496 return NULL;
497 Cudd_Ref( bFunc1 );
498 bFunc0 = Cudd_NotCond( bFunc0, (int)Abc_ObjFaninC0(pNode) );
499 bFunc1 = Cudd_NotCond( bFunc1, (int)Abc_ObjFaninC1(pNode) );
500 // get the final result
501 bFunc = Cudd_bddAndLimit( dd, bFunc0, bFunc1, nBddSizeMax );
502 if ( bFunc == NULL )
503 return NULL;
504 Cudd_Ref( bFunc );
505 Cudd_RecursiveDeref( dd, bFunc0 );
506 Cudd_RecursiveDeref( dd, bFunc1 );
507 // add the number of used nodes
508 (*pCounter)++;
509 }
510 // set the result
511 assert( Abc_ObjGlobalBdd(pNode) == NULL );
512 Abc_ObjSetGlobalBdd( pNode, bFunc );
513 // increment the progress bar
514 if ( pProgress )
515 Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
516 }
517 // prepare the return value
518 bFunc = (DdNode *)Abc_ObjGlobalBdd(pNode);
519 // dereference BDD at the node
520 if ( --pNode->vFanouts.nSize == 0 && fDropInternal )
521 {
522 Cudd_Deref( bFunc );
523 Abc_ObjSetGlobalBdd( pNode, NULL );
524 }
525 return bFunc;
526 }
527
528 /**Function*************************************************************
529
530 Synopsis [Frees the global BDDs of the network.]
531
532 Description []
533
534 SideEffects []
535
536 SeeAlso []
537
538 ***********************************************************************/
Abc_NtkFreeGlobalBdds(Abc_Ntk_t * pNtk,int fFreeMan)539 void * Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan )
540 {
541 return Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, fFreeMan );
542 }
543
544 /**Function*************************************************************
545
546 Synopsis [Returns the shared size of global BDDs of the COs.]
547
548 Description []
549
550 SideEffects []
551
552 SeeAlso []
553
554 ***********************************************************************/
Abc_NtkSizeOfGlobalBdds(Abc_Ntk_t * pNtk)555 int Abc_NtkSizeOfGlobalBdds( Abc_Ntk_t * pNtk )
556 {
557 Vec_Ptr_t * vFuncsGlob;
558 Abc_Obj_t * pObj;
559 int RetValue, i;
560 // complement the global functions
561 vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
562 Abc_NtkForEachCo( pNtk, pObj, i )
563 Vec_PtrPush( vFuncsGlob, Abc_ObjGlobalBdd(pObj) );
564 RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
565 Vec_PtrFree( vFuncsGlob );
566 return RetValue;
567 }
568
569 /**Function*************************************************************
570
571 Synopsis [Computes the BDD of the logic cone of the node.]
572
573 Description []
574
575 SideEffects []
576
577 SeeAlso []
578
579 ***********************************************************************/
Abc_NtkSpacePercentage(Abc_Obj_t * pNode)580 double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
581 {
582 /*
583 Vec_Ptr_t * vNodes;
584 Abc_Obj_t * pObj, * pNodeR;
585 DdManager * dd;
586 DdNode * bFunc;
587 double Result;
588 int i;
589 pNodeR = Abc_ObjRegular(pNode);
590 assert( Abc_NtkIsStrash(pNodeR->pNtk) );
591 Abc_NtkCleanCopy( pNodeR->pNtk );
592 // get the CIs in the support of the node
593 vNodes = Abc_NtkNodeSupport( pNodeR->pNtk, &pNodeR, 1 );
594 // start the manager
595 dd = Cudd_Init( Vec_PtrSize(vNodes), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
596 Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
597 // assign elementary BDDs for the CIs
598 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
599 pObj->pCopy = (Abc_Obj_t *)dd->vars[i];
600 // build the BDD of the cone
601 bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000, 1, NULL, NULL, 1 ); Cudd_Ref( bFunc );
602 bFunc = Cudd_NotCond( bFunc, pNode != pNodeR );
603 // count minterms
604 Result = Cudd_CountMinterm( dd, bFunc, dd->size );
605 // get the percentagle
606 Result *= 100.0;
607 for ( i = 0; i < dd->size; i++ )
608 Result /= 2;
609 // clean up
610 Cudd_Quit( dd );
611 Vec_PtrFree( vNodes );
612 return Result;
613 */
614 return 0.0;
615 }
616
617
618
619
620 /**Function*************************************************************
621
622 Synopsis [Experiment with BDD-based representation of implications.]
623
624 Description []
625
626 SideEffects []
627
628 SeeAlso []
629
630 ***********************************************************************/
Abc_NtkBddImplicationTest()631 void Abc_NtkBddImplicationTest()
632 {
633 DdManager * dd;
634 DdNode * bImp, * bSum, * bTemp;
635 int nVars = 200;
636 int nImps = 200;
637 int i;
638 abctime clk;
639 clk = Abc_Clock();
640 dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
641 Cudd_AutodynEnable( dd, CUDD_REORDER_SIFT );
642 bSum = b0; Cudd_Ref( bSum );
643 for ( i = 0; i < nImps; i++ )
644 {
645 printf( "." );
646 bImp = Cudd_bddAnd( dd, dd->vars[rand()%nVars], dd->vars[rand()%nVars] ); Cudd_Ref( bImp );
647 bSum = Cudd_bddOr( dd, bTemp = bSum, bImp ); Cudd_Ref( bSum );
648 Cudd_RecursiveDeref( dd, bTemp );
649 Cudd_RecursiveDeref( dd, bImp );
650 }
651 printf( "The BDD before = %d.\n", Cudd_DagSize(bSum) );
652 Cudd_ReduceHeap( dd, CUDD_REORDER_SIFT, 1 );
653 printf( "The BDD after = %d.\n", Cudd_DagSize(bSum) );
654 ABC_PRT( "Time", Abc_Clock() - clk );
655 Cudd_RecursiveDeref( dd, bSum );
656 Cudd_Quit( dd );
657 }
658
659 #else
660
661 double Abc_NtkSpacePercentage( Abc_Obj_t * pNode ) { return 0.0; }
662 Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk, int fGlobal, int Limit ) { return NULL; }
663
664
665 #endif
666
667 ////////////////////////////////////////////////////////////////////////
668 /// END OF FILE ///
669 ////////////////////////////////////////////////////////////////////////
670
671
672 ABC_NAMESPACE_IMPL_END
673
674