abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcNtbdd.c
Go to the documentation of this file.
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 "misc/extra/extraBdd.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 static void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
32 static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew );
33 static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st__table * tBdd2Node );
34 static DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose );
35 
36 ////////////////////////////////////////////////////////////////////////
37 /// FUNCTION DEFINITIONS ///
38 ////////////////////////////////////////////////////////////////////////
39 
40 /**Function*************************************************************
41 
42  Synopsis [Constructs the network isomorphic to the given BDD.]
43 
44  Description [Assumes that the BDD depends on the variables whose indexes
45  correspond to the names in the array (pNamesPi). Otherwise, returns NULL.
46  The resulting network comes with one node, whose functionality is
47  equal to the given BDD. To decompose this BDD into the network of
48  multiplexers use Abc_NtkBddToMuxes(). To decompose this BDD into
49  an And-Inverter Graph, use Abc_NtkStrash().]
50 
51  SideEffects []
52 
53  SeeAlso []
54 
55 ***********************************************************************/
56 Abc_Ntk_t * Abc_NtkDeriveFromBdd( void * dd0, void * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi )
57 {
58  DdManager * dd = (DdManager *)dd0;
59  Abc_Ntk_t * pNtk;
60  Vec_Ptr_t * vNamesPiFake = NULL;
61  Abc_Obj_t * pNode, * pNodePi, * pNodePo;
62  DdNode * bSupp, * bTemp;
63  char * pName;
64  int i;
65 
66  // supply fake names if real names are not given
67  if ( pNamePo == NULL )
68  pNamePo = "F";
69  if ( vNamesPi == NULL )
70  {
71  vNamesPiFake = Abc_NodeGetFakeNames( dd->size );
72  vNamesPi = vNamesPiFake;
73  }
74 
75  // make sure BDD depends on the variables whose index
76  // does not exceed the size of the array with PI names
77  bSupp = Cudd_Support( dd, (DdNode *)bFunc ); Cudd_Ref( bSupp );
78  for ( bTemp = bSupp; bTemp != Cudd_ReadOne(dd); bTemp = cuddT(bTemp) )
79  if ( (int)Cudd_NodeReadIndex(bTemp) >= Vec_PtrSize(vNamesPi) )
80  break;
81  Cudd_RecursiveDeref( dd, bSupp );
82  if ( bTemp != Cudd_ReadOne(dd) )
83  return NULL;
84 
85  // start the network
86  pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
87  pNtk->pName = Extra_UtilStrsav(pNamePo);
88  // make sure the new manager has enough inputs
89  Cudd_bddIthVar( (DdManager *)pNtk->pManFunc, Vec_PtrSize(vNamesPi) );
90  // add the PIs corresponding to the names
91  Vec_PtrForEachEntry( char *, vNamesPi, pName, i )
92  Abc_ObjAssignName( Abc_NtkCreatePi(pNtk), pName, NULL );
93  // create the node
94  pNode = Abc_NtkCreateNode( pNtk );
95  pNode->pData = (DdNode *)Cudd_bddTransfer( dd, (DdManager *)pNtk->pManFunc, (DdNode *)bFunc ); Cudd_Ref((DdNode *)pNode->pData);
96  Abc_NtkForEachPi( pNtk, pNodePi, i )
97  Abc_ObjAddFanin( pNode, pNodePi );
98  // create the only PO
99  pNodePo = Abc_NtkCreatePo( pNtk );
100  Abc_ObjAddFanin( pNodePo, pNode );
101  Abc_ObjAssignName( pNodePo, pNamePo, NULL );
102  // make the network minimum base
103  Abc_NtkMinimumBase( pNtk );
104  if ( vNamesPiFake )
105  Abc_NodeFreeNames( vNamesPiFake );
106  if ( !Abc_NtkCheck( pNtk ) )
107  fprintf( stdout, "Abc_NtkDeriveFromBdd(): Network check has failed.\n" );
108  return pNtk;
109 }
110 
111 
112 
113 /**Function*************************************************************
114 
115  Synopsis [Creates the network isomorphic to the union of local BDDs of the nodes.]
116 
117  Description [The nodes of the local BDDs are converted into the network nodes
118  with logic functions equal to the MUX.]
119 
120  SideEffects []
121 
122  SeeAlso []
123 
124 ***********************************************************************/
125 Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk )
126 {
127  Abc_Ntk_t * pNtkNew;
128  assert( Abc_NtkIsBddLogic(pNtk) );
129  pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
130  Abc_NtkBddToMuxesPerform( pNtk, pNtkNew );
131  Abc_NtkFinalize( pNtk, pNtkNew );
132  // make sure everything is okay
133  if ( !Abc_NtkCheck( pNtkNew ) )
134  {
135  printf( "Abc_NtkBddToMuxes: The network check has failed.\n" );
136  Abc_NtkDelete( pNtkNew );
137  return NULL;
138  }
139  return pNtkNew;
140 }
141 
142 /**Function*************************************************************
143 
144  Synopsis [Converts the network to MUXes.]
145 
146  Description []
147 
148  SideEffects []
149 
150  SeeAlso []
151 
152 ***********************************************************************/
153 void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
154 {
155  ProgressBar * pProgress;
156  Abc_Obj_t * pNode, * pNodeNew;
157  Vec_Ptr_t * vNodes;
158  int i;
159  // perform conversion in the topological order
160  vNodes = Abc_NtkDfs( pNtk, 0 );
161  pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
162  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
163  {
164  Extra_ProgressBarUpdate( pProgress, i, NULL );
165  // convert one node
166  assert( Abc_ObjIsNode(pNode) );
167  pNodeNew = Abc_NodeBddToMuxes( pNode, pNtkNew );
168  // mark the old node with the new one
169  assert( pNode->pCopy == NULL );
170  pNode->pCopy = pNodeNew;
171  }
172  Vec_PtrFree( vNodes );
173  Extra_ProgressBarStop( pProgress );
174 }
175 
176 /**Function*************************************************************
177 
178  Synopsis [Converts the node to MUXes.]
179 
180  Description []
181 
182  SideEffects []
183 
184  SeeAlso []
185 
186 ***********************************************************************/
187 Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
188 {
189  DdManager * dd = (DdManager *)pNodeOld->pNtk->pManFunc;
190  DdNode * bFunc = (DdNode *)pNodeOld->pData;
191  Abc_Obj_t * pFaninOld, * pNodeNew;
192  st__table * tBdd2Node;
193  int i;
194  // create the table mapping BDD nodes into the ABC nodes
195  tBdd2Node = st__init_table( st__ptrcmp, st__ptrhash );
196  // add the constant and the elementary vars
197  Abc_ObjForEachFanin( pNodeOld, pFaninOld, i )
198  st__insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pFaninOld->pCopy );
199  // create the new nodes recursively
200  pNodeNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node );
201  st__free_table( tBdd2Node );
202  if ( Cudd_IsComplement(bFunc) )
203  pNodeNew = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew );
204  return pNodeNew;
205 }
206 
207 /**Function*************************************************************
208 
209  Synopsis [Converts the node to MUXes.]
210 
211  Description []
212 
213  SideEffects []
214 
215  SeeAlso []
216 
217 ***********************************************************************/
218 Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st__table * tBdd2Node )
219 {
220  Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
221  assert( !Cudd_IsComplement(bFunc) );
222  if ( bFunc == b1 )
223  return Abc_NtkCreateNodeConst1(pNtkNew);
224  if ( st__lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
225  return pNodeNew;
226  // solve for the children nodes
227  pNodeNew0 = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(cuddE(bFunc)), pNtkNew, tBdd2Node );
228  if ( Cudd_IsComplement(cuddE(bFunc)) )
229  pNodeNew0 = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew0 );
230  pNodeNew1 = Abc_NodeBddToMuxes_rec( dd, cuddT(bFunc), pNtkNew, tBdd2Node );
231  if ( ! st__lookup( tBdd2Node, (char *)Cudd_bddIthVar(dd, bFunc->index), (char **)&pNodeNewC ) )
232  assert( 0 );
233  // create the MUX node
234  pNodeNew = Abc_NtkCreateNodeMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 );
235  st__insert( tBdd2Node, (char *)bFunc, (char *)pNodeNew );
236  return pNodeNew;
237 }
238 
239 
240 /**Function*************************************************************
241 
242  Synopsis [Derives global BDDs for the COs of the network.]
243 
244  Description []
245 
246  SideEffects []
247 
248  SeeAlso []
249 
250 ***********************************************************************/
251 void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose )
252 {
253  ProgressBar * pProgress;
254  Abc_Obj_t * pObj, * pFanin;
255  Vec_Att_t * pAttMan;
256  DdManager * dd;
257  DdNode * bFunc;
258  int i, k, Counter;
259 
260  // remove dangling nodes
261  Abc_AigCleanup( (Abc_Aig_t *)pNtk->pManFunc );
262 
263  // start the manager
264  assert( Abc_NtkGlobalBdd(pNtk) == NULL );
265  dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
266  pAttMan = Vec_AttAlloc( Abc_NtkObjNumMax(pNtk) + 1, dd, (void (*)(void*))Extra_StopManager, NULL, (void (*)(void*,void*))Cudd_RecursiveDeref );
267  Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD, pAttMan );
268 
269  // set reordering
270  if ( fReorder )
271  Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
272 
273  // assign the constant node BDD
274  pObj = Abc_AigConst1(pNtk);
275  if ( Abc_ObjFanoutNum(pObj) > 0 )
276  {
277  bFunc = dd->one;
278  Abc_ObjSetGlobalBdd( pObj, bFunc ); Cudd_Ref( bFunc );
279  }
280  // set the elementary variables
281  Abc_NtkForEachCi( pNtk, pObj, i )
282  if ( Abc_ObjFanoutNum(pObj) > 0 )
283  {
284  bFunc = dd->vars[i];
285 // bFunc = dd->vars[Abc_NtkCiNum(pNtk) - 1 - i];
286  Abc_ObjSetGlobalBdd( pObj, bFunc ); Cudd_Ref( bFunc );
287  }
288 
289  // collect the global functions of the COs
290  Counter = 0;
291  // construct the BDDs
292  pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
293  Abc_NtkForEachCo( pNtk, pObj, i )
294  {
295  bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose );
296  if ( bFunc == NULL )
297  {
298  if ( fVerbose )
299  printf( "Constructing global BDDs is aborted.\n" );
300  Abc_NtkFreeGlobalBdds( pNtk, 0 );
301  Cudd_Quit( dd );
302 
303  // reset references
304  Abc_NtkForEachObj( pNtk, pObj, i )
305  if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) )
306  pObj->vFanouts.nSize = 0;
307  Abc_NtkForEachObj( pNtk, pObj, i )
308  if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
309  Abc_ObjForEachFanin( pObj, pFanin, k )
310  pFanin->vFanouts.nSize++;
311  return NULL;
312  }
313  bFunc = Cudd_NotCond( bFunc, (int)Abc_ObjFaninC0(pObj) ); Cudd_Ref( bFunc );
314  Abc_ObjSetGlobalBdd( pObj, bFunc );
315  }
316  Extra_ProgressBarStop( pProgress );
317 
318 /*
319  // derefence the intermediate BDDs
320  Abc_NtkForEachNode( pNtk, pObj, i )
321  if ( pObj->pCopy )
322  {
323  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pCopy );
324  pObj->pCopy = NULL;
325  }
326 */
327 /*
328  // make sure all nodes are derefed
329  Abc_NtkForEachObj( pNtk, pObj, i )
330  {
331  if ( pObj->pCopy != NULL )
332  printf( "Abc_NtkBuildGlobalBdds() error: Node %d has BDD assigned\n", pObj->Id );
333  if ( pObj->vFanouts.nSize > 0 )
334  printf( "Abc_NtkBuildGlobalBdds() error: Node %d has refs assigned\n", pObj->Id );
335  }
336 */
337  // reset references
338  Abc_NtkForEachObj( pNtk, pObj, i )
339  if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) )
340  pObj->vFanouts.nSize = 0;
341  Abc_NtkForEachObj( pNtk, pObj, i )
342  if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
343  Abc_ObjForEachFanin( pObj, pFanin, k )
344  pFanin->vFanouts.nSize++;
345 
346  // reorder one more time
347  if ( fReorder )
348  {
349  Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
350  Cudd_AutodynDisable( dd );
351  }
352 // Cudd_PrintInfo( dd, stdout );
353  return dd;
354 }
355 
356 /**Function*************************************************************
357 
358  Synopsis [Derives the global BDD for one AIG node.]
359 
360  Description []
361 
362  SideEffects []
363 
364  SeeAlso []
365 
366 ***********************************************************************/
367 DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose )
368 {
369  DdNode * bFunc, * bFunc0, * bFunc1, * bFuncC;
370  int fDetectMuxes = 1;
371  assert( !Abc_ObjIsComplement(pNode) );
372  if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
373  {
374  Extra_ProgressBarStop( pProgress );
375  if ( fVerbose )
376  printf( "The number of live nodes reached %d.\n", nBddSizeMax );
377  fflush( stdout );
378  return NULL;
379  }
380  // if the result is available return
381  if ( Abc_ObjGlobalBdd(pNode) == NULL )
382  {
383  Abc_Obj_t * pNodeC, * pNode0, * pNode1;
384  pNode0 = Abc_ObjFanin0(pNode);
385  pNode1 = Abc_ObjFanin1(pNode);
386  // check for the special case when it is MUX/EXOR
387  if ( fDetectMuxes &&
388  Abc_ObjGlobalBdd(pNode0) == NULL && Abc_ObjGlobalBdd(pNode1) == NULL &&
389  Abc_ObjIsNode(pNode0) && Abc_ObjFanoutNum(pNode0) == 1 &&
390  Abc_ObjIsNode(pNode1) && Abc_ObjFanoutNum(pNode1) == 1 &&
391  Abc_NodeIsMuxType(pNode) )
392  {
393  // deref the fanins
394  pNode0->vFanouts.nSize--;
395  pNode1->vFanouts.nSize--;
396  // recognize the MUX
397  pNodeC = Abc_NodeRecognizeMux( pNode, &pNode1, &pNode0 );
398  assert( Abc_ObjFanoutNum(pNodeC) > 1 );
399  // dereference the control once (the second time it will be derefed when BDDs are computed)
400  pNodeC->vFanouts.nSize--;
401 
402  // compute the result for all branches
403  bFuncC = Abc_NodeGlobalBdds_rec( dd, pNodeC, nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );
404  if ( bFuncC == NULL )
405  return NULL;
406  Cudd_Ref( bFuncC );
407  bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode0), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );
408  if ( bFunc0 == NULL )
409  return NULL;
410  Cudd_Ref( bFunc0 );
411  bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode1), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );
412  if ( bFunc1 == NULL )
413  return NULL;
414  Cudd_Ref( bFunc1 );
415 
416  // complement the branch BDDs
417  bFunc0 = Cudd_NotCond( bFunc0, (int)Abc_ObjIsComplement(pNode0) );
418  bFunc1 = Cudd_NotCond( bFunc1, (int)Abc_ObjIsComplement(pNode1) );
419  // get the final result
420  bFunc = Cudd_bddIte( dd, bFuncC, bFunc1, bFunc0 ); Cudd_Ref( bFunc );
421  Cudd_RecursiveDeref( dd, bFunc0 );
422  Cudd_RecursiveDeref( dd, bFunc1 );
423  Cudd_RecursiveDeref( dd, bFuncC );
424  // add the number of used nodes
425  (*pCounter) += 3;
426  }
427  else
428  {
429  // compute the result for both branches
430  bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );
431  if ( bFunc0 == NULL )
432  return NULL;
433  Cudd_Ref( bFunc0 );
434  bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );
435  if ( bFunc1 == NULL )
436  return NULL;
437  Cudd_Ref( bFunc1 );
438  bFunc0 = Cudd_NotCond( bFunc0, (int)Abc_ObjFaninC0(pNode) );
439  bFunc1 = Cudd_NotCond( bFunc1, (int)Abc_ObjFaninC1(pNode) );
440  // get the final result
441  bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
442  Cudd_RecursiveDeref( dd, bFunc0 );
443  Cudd_RecursiveDeref( dd, bFunc1 );
444  // add the number of used nodes
445  (*pCounter)++;
446  }
447  // set the result
448  assert( Abc_ObjGlobalBdd(pNode) == NULL );
449  Abc_ObjSetGlobalBdd( pNode, bFunc );
450  // increment the progress bar
451  if ( pProgress )
452  Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
453  }
454  // prepare the return value
455  bFunc = (DdNode *)Abc_ObjGlobalBdd(pNode);
456  // dereference BDD at the node
457  if ( --pNode->vFanouts.nSize == 0 && fDropInternal )
458  {
459  Cudd_Deref( bFunc );
460  Abc_ObjSetGlobalBdd( pNode, NULL );
461  }
462  return bFunc;
463 }
464 
465 /**Function*************************************************************
466 
467  Synopsis [Frees the global BDDs of the network.]
468 
469  Description []
470 
471  SideEffects []
472 
473  SeeAlso []
474 
475 ***********************************************************************/
476 void * Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan )
477 {
478  return Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, fFreeMan );
479 }
480 
481 /**Function*************************************************************
482 
483  Synopsis [Returns the shared size of global BDDs of the COs.]
484 
485  Description []
486 
487  SideEffects []
488 
489  SeeAlso []
490 
491 ***********************************************************************/
492 int Abc_NtkSizeOfGlobalBdds( Abc_Ntk_t * pNtk )
493 {
494  Vec_Ptr_t * vFuncsGlob;
495  Abc_Obj_t * pObj;
496  int RetValue, i;
497  // complement the global functions
498  vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
499  Abc_NtkForEachCo( pNtk, pObj, i )
500  Vec_PtrPush( vFuncsGlob, Abc_ObjGlobalBdd(pObj) );
501  RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
502  Vec_PtrFree( vFuncsGlob );
503  return RetValue;
504 }
505 
506 /**Function*************************************************************
507 
508  Synopsis [Computes the BDD of the logic cone of the node.]
509 
510  Description []
511 
512  SideEffects []
513 
514  SeeAlso []
515 
516 ***********************************************************************/
517 double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
518 {
519  /*
520  Vec_Ptr_t * vNodes;
521  Abc_Obj_t * pObj, * pNodeR;
522  DdManager * dd;
523  DdNode * bFunc;
524  double Result;
525  int i;
526  pNodeR = Abc_ObjRegular(pNode);
527  assert( Abc_NtkIsStrash(pNodeR->pNtk) );
528  Abc_NtkCleanCopy( pNodeR->pNtk );
529  // get the CIs in the support of the node
530  vNodes = Abc_NtkNodeSupport( pNodeR->pNtk, &pNodeR, 1 );
531  // start the manager
532  dd = Cudd_Init( Vec_PtrSize(vNodes), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
533  Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
534  // assign elementary BDDs for the CIs
535  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
536  pObj->pCopy = (Abc_Obj_t *)dd->vars[i];
537  // build the BDD of the cone
538  bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000, 1, NULL, NULL, 1 ); Cudd_Ref( bFunc );
539  bFunc = Cudd_NotCond( bFunc, pNode != pNodeR );
540  // count minterms
541  Result = Cudd_CountMinterm( dd, bFunc, dd->size );
542  // get the percentagle
543  Result *= 100.0;
544  for ( i = 0; i < dd->size; i++ )
545  Result /= 2;
546  // clean up
547  Cudd_Quit( dd );
548  Vec_PtrFree( vNodes );
549  return Result;
550  */
551  return 0.0;
552 }
553 
554 
555 
556 
557 /**Function*************************************************************
558 
559  Synopsis [Experiment with BDD-based representation of implications.]
560 
561  Description []
562 
563  SideEffects []
564 
565  SeeAlso []
566 
567 ***********************************************************************/
568 void Abc_NtkBddImplicationTest()
569 {
570  DdManager * dd;
571  DdNode * bImp, * bSum, * bTemp;
572  int nVars = 200;
573  int nImps = 200;
574  int i;
575  abctime clk;
576 clk = Abc_Clock();
577  dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
578  Cudd_AutodynEnable( dd, CUDD_REORDER_SIFT );
579  bSum = b0; Cudd_Ref( bSum );
580  for ( i = 0; i < nImps; i++ )
581  {
582  printf( "." );
583  bImp = Cudd_bddAnd( dd, dd->vars[rand()%nVars], dd->vars[rand()%nVars] ); Cudd_Ref( bImp );
584  bSum = Cudd_bddOr( dd, bTemp = bSum, bImp ); Cudd_Ref( bSum );
585  Cudd_RecursiveDeref( dd, bTemp );
586  Cudd_RecursiveDeref( dd, bImp );
587  }
588  printf( "The BDD before = %d.\n", Cudd_DagSize(bSum) );
589  Cudd_ReduceHeap( dd, CUDD_REORDER_SIFT, 1 );
590  printf( "The BDD after = %d.\n", Cudd_DagSize(bSum) );
591 ABC_PRT( "Time", Abc_Clock() - clk );
592  Cudd_RecursiveDeref( dd, bSum );
593  Cudd_Quit( dd );
594 }
595 
596 ////////////////////////////////////////////////////////////////////////
597 /// END OF FILE ///
598 ////////////////////////////////////////////////////////////////////////
599 
600 
601 ABC_NAMESPACE_IMPL_END
602 
st__free_table
void st__free_table(st__table *table)
Definition: st.c:81
Abc_Ntk_t_::vAttrs
Vec_Ptr_t * vAttrs
Definition: abc.h:214
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_ObjFanin1
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
CUDD_UNIQUE_SLOTS
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
Abc_NtkFreeGlobalBdds
void * Abc_NtkFreeGlobalBdds(Abc_Ntk_t *pNtk, int fFreeMan)
Definition: abcNtbdd.c:476
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Abc_NtkObjNumMax
static int Abc_NtkObjNumMax(Abc_Ntk_t *pNtk)
Definition: abc.h:284
Abc_ObjIsBo
static int Abc_ObjIsBo(Abc_Obj_t *pObj)
Definition: abc.h:350
Abc_AigConst1
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition: abcAig.c:683
Abc_NtkMinimumBase
ABC_DLL int Abc_NtkMinimumBase(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcMinBase.c:48
Abc_NtkBuildGlobalBdds
void * Abc_NtkBuildGlobalBdds(Abc_Ntk_t *pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose)
Definition: abcNtbdd.c:251
Abc_ObjFaninC1
static int Abc_ObjFaninC1(Abc_Obj_t *pObj)
Definition: abc.h:378
st__insert
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
Cudd_Support
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:740
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
DdManager::size
int size
Definition: cuddInt.h:361
Abc_Ntk_t_
Definition: abc.h:153
Abc_ObjFanoutNum
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
b1
#define b1
Definition: extraBdd.h:76
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
Abc_NodeBddToMuxes
static Abc_Obj_t * Abc_NodeBddToMuxes(Abc_Obj_t *pNodeOld, Abc_Ntk_t *pNtkNew)
Definition: abcNtbdd.c:187
st__ptrcmp
int st__ptrcmp(const char *, const char *)
Definition: st.c:480
Abc_NtkGlobalBdd
static void * Abc_NtkGlobalBdd(Abc_Ntk_t *pNtk)
Definition: abc.h:428
Abc_NtkCreateNodeConst1
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeConst1(Abc_Ntk_t *pNtk)
Definition: abcObj.c:633
Abc_ObjFaninC0
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
CUDD_CACHE_SLOTS
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Abc_NtkCreateNodeMux
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeMux(Abc_Ntk_t *pNtk, Abc_Obj_t *pNodeC, Abc_Obj_t *pNode1, Abc_Obj_t *pNode0)
Definition: abcObj.c:812
Abc_NtkCiNum
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
Abc_NtkForEachCo
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
Abc_NtkCheck
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
Abc_ObjAssignName
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition: abcNames.c:68
Abc_NtkSizeOfGlobalBdds
int Abc_NtkSizeOfGlobalBdds(Abc_Ntk_t *pNtk)
Definition: abcNtbdd.c:492
Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
Abc_NtkDfs
ABC_DLL Vec_Ptr_t * Abc_NtkDfs(Abc_Ntk_t *pNtk, int fCollectAll)
Definition: abcDfs.c:81
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Extra_StopManager
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Abc_ObjFanin0
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
Abc_NtkCoNum
static int Abc_NtkCoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:288
Abc_Aig_t_
DECLARATIONS ///.
Definition: abcAig.c:52
Abc_NtkDelete
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
Extra_UtilStrsav
char * Extra_UtilStrsav(const char *s)
Definition: extraUtilUtil.c:169
Cudd_bddTransfer
DdNode * Cudd_bddTransfer(DdManager *ddSource, DdManager *ddDestination, DdNode *f)
Definition: cuddBridge.c:409
Abc_ObjGlobalBdd
static void * Abc_ObjGlobalBdd(Abc_Obj_t *pObj)
Definition: abc.h:431
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
Abc_NtkAlloc
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition: abcNtk.c:50
Abc_Obj_t_
Definition: abc.h:128
st__init_table
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
Abc_NodeFreeNames
ABC_DLL void Abc_NodeFreeNames(Vec_Ptr_t *vNames)
Definition: abcNames.c:257
Abc_NtkBddImplicationTest
void Abc_NtkBddImplicationTest()
Definition: abcNtbdd.c:568
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition: abc.h:191
Abc_ObjIsNode
static int Abc_ObjIsNode(Abc_Obj_t *pObj)
Definition: abc.h:355
Abc_NtkNodeNum
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
Abc_NodeGlobalBdds_rec
static DdNode * Abc_NodeGlobalBdds_rec(DdManager *dd, Abc_Obj_t *pNode, int nBddSizeMax, int fDropInternal, ProgressBar *pProgress, int *pCounter, int fVerbose)
Definition: abcNtbdd.c:367
ProgressBarStruct
DECLARATIONS ///.
Definition: extraUtilProgress.c:32
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
Abc_NtkStartFrom
ABC_DLL Abc_Ntk_t * Abc_NtkStartFrom(Abc_Ntk_t *pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func)
Definition: abcNtk.c:106
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition: abc.h:148
Abc_NodeIsMuxType
ABC_DLL int Abc_NodeIsMuxType(Abc_Obj_t *pNode)
Definition: abcUtil.c:1301
Abc_AigCleanup
ABC_DLL int Abc_AigCleanup(Abc_Aig_t *pMan)
Definition: abcAig.c:194
Abc_NtkCreateNodeInv
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeInv(Abc_Ntk_t *pNtk, Abc_Obj_t *pFanin)
Definition: abcObj.c:662
st__table
Definition: st.h:52
Abc_NodeGetFakeNames
ABC_DLL Vec_Ptr_t * Abc_NodeGetFakeNames(int nNames)
Definition: abcNames.c:221
Abc_NtkBddToMuxes
Abc_Ntk_t * Abc_NtkBddToMuxes(Abc_Ntk_t *pNtk)
Definition: abcNtbdd.c:125
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Cudd_Init
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
Abc_NtkFinalize
ABC_DLL void Abc_NtkFinalize(Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkNew)
Definition: abcNtk.c:302
Counter
static int Counter
Definition: extraBddMisc.c:1877
Abc_NtkCreatePi
static Abc_Obj_t * Abc_NtkCreatePi(Abc_Ntk_t *pNtk)
Definition: abc.h:303
Cudd_bddOr
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
Abc_NtkBddToMuxesPerform
static ABC_NAMESPACE_IMPL_START void Abc_NtkBddToMuxesPerform(Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkNew)
DECLARATIONS ///.
Definition: abcNtbdd.c:153
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition: extraUtilProgress.c:118
Abc_ObjSetGlobalBdd
static void Abc_ObjSetGlobalBdd(Abc_Obj_t *pObj, void *bF)
Definition: abc.h:432
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Abc_Obj_t_::vFanouts
Vec_Int_t vFanouts
Definition: abc.h:144
Cudd_AutodynDisable
void Cudd_AutodynDisable(DdManager *unique)
Definition: cuddAPI.c:708
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
Abc_ObjRegular
static Abc_Obj_t * Abc_ObjRegular(Abc_Obj_t *p)
Definition: abc.h:323
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition: abc.h:130
Abc_ObjIsBi
static int Abc_ObjIsBi(Abc_Obj_t *pObj)
Definition: abc.h:349
Abc_NtkForEachCi
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Abc_ObjForEachFanin
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition: abc.h:524
Abc_NodeBddToMuxes_rec
static Abc_Obj_t * Abc_NodeBddToMuxes_rec(DdManager *dd, DdNode *bFunc, Abc_Ntk_t *pNtkNew, st__table *tBdd2Node)
Definition: abcNtbdd.c:218
Vec_AttAlloc
static Vec_Att_t * Vec_AttAlloc(int nSize, void *pMan, void(*pFuncFreeMan)(void *), void *(*pFuncStartObj)(void *), void(*pFuncFreeObj)(void *, void *))
MACRO DEFINITIONS ///.
Definition: vecAtt.h:96
b0
#define b0
Definition: extraBdd.h:75
DdNode::index
DdHalfWord index
Definition: cudd.h:279
Abc_NtkIsBddLogic
static int Abc_NtkIsBddLogic(Abc_Ntk_t *pNtk)
Definition: abc.h:265
Cudd_NodeReadIndex
unsigned int Cudd_NodeReadIndex(DdNode *node)
Definition: cuddAPI.c:2277
DdManager::vars
DdNode ** vars
Definition: cuddInt.h:390
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Abc_NtkCreateNode
static Abc_Obj_t * Abc_NtkCreateNode(Abc_Ntk_t *pNtk)
Definition: abc.h:308
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition: extraUtilProgress.c:62
DdManager::one
DdNode * one
Definition: cuddInt.h:345
Cudd_ReadKeys
unsigned int Cudd_ReadKeys(DdManager *dd)
Definition: cuddAPI.c:1626
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Abc_NtkDeriveFromBdd
Abc_Ntk_t * Abc_NtkDeriveFromBdd(void *dd0, void *bFunc, char *pNamePo, Vec_Ptr_t *vNamesPi)
FUNCTION DEFINITIONS ///.
Definition: abcNtbdd.c:56
assert
#define assert(ex)
Definition: util_old.h:213
Extra_ProgressBarUpdate
static void Extra_ProgressBarUpdate(ProgressBar *p, int nItemsCur, char *pString)
Definition: extra.h:243
Abc_ObjIsBox
static int Abc_ObjIsBox(Abc_Obj_t *pObj)
Definition: abc.h:357
Cudd_Quit
void Cudd_Quit(DdManager *unique)
Definition: cuddInit.c:225
Cudd_ReduceHeap
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddReorder.c:176
Cudd_AutodynEnable
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:669
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Cudd_ReadDead
unsigned int Cudd_ReadDead(DdManager *dd)
Definition: cuddAPI.c:1646
Abc_ObjFanin
static Abc_Obj_t * Abc_ObjFanin(Abc_Obj_t *pObj, int i)
Definition: abc.h:372
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_ObjIsComplement
static int Abc_ObjIsComplement(Abc_Obj_t *p)
Definition: abc.h:322
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Abc_NtkForEachObj
#define Abc_NtkForEachObj(pNtk, pObj, i)
ITERATORS ///.
Definition: abc.h:446
Abc_NtkSpacePercentage
double Abc_NtkSpacePercentage(Abc_Obj_t *pNode)
Definition: abcNtbdd.c:517
Vec_Att_t_
Definition: vecAtt.h:63
Abc_NtkCreatePo
static Abc_Obj_t * Abc_NtkCreatePo(Abc_Ntk_t *pNtk)
Definition: abc.h:304
Vec_PtrArray
static void ** Vec_PtrArray(Vec_Ptr_t *p)
Definition: vecPtr.h:279
Cudd_SharingSize
int Cudd_SharingSize(DdNode **nodeArray, int n)
Definition: cuddUtil.c:544
Abc_NtkAttrFree
ABC_DLL void * Abc_NtkAttrFree(Abc_Ntk_t *pNtk, int Attr, int fFreeMan)
DECLARATIONS ///.
Definition: abcUtil.c:50
st__ptrhash
int st__ptrhash(const char *, int)
Definition: st.c:468
Abc_Ntk_t_::pName
char * pName
Definition: abc.h:158
Abc_NodeRecognizeMux
ABC_DLL Abc_Obj_t * Abc_NodeRecognizeMux(Abc_Obj_t *pNode, Abc_Obj_t **ppNodeT, Abc_Obj_t **ppNodeE)
Definition: abcUtil.c:1389
Abc_NtkForEachPi
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223