abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcNtbdd.c File Reference
#include "base/abc/abc.h"
#include "misc/extra/extraBdd.h"

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START void 
Abc_NtkBddToMuxesPerform (Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkNew)
 DECLARATIONS ///. More...
 
static Abc_Obj_tAbc_NodeBddToMuxes (Abc_Obj_t *pNodeOld, Abc_Ntk_t *pNtkNew)
 
static Abc_Obj_tAbc_NodeBddToMuxes_rec (DdManager *dd, DdNode *bFunc, Abc_Ntk_t *pNtkNew, st__table *tBdd2Node)
 
static DdNodeAbc_NodeGlobalBdds_rec (DdManager *dd, Abc_Obj_t *pNode, int nBddSizeMax, int fDropInternal, ProgressBar *pProgress, int *pCounter, int fVerbose)
 
Abc_Ntk_tAbc_NtkDeriveFromBdd (void *dd0, void *bFunc, char *pNamePo, Vec_Ptr_t *vNamesPi)
 FUNCTION DEFINITIONS ///. More...
 
Abc_Ntk_tAbc_NtkBddToMuxes (Abc_Ntk_t *pNtk)
 
void * Abc_NtkBuildGlobalBdds (Abc_Ntk_t *pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose)
 
void * Abc_NtkFreeGlobalBdds (Abc_Ntk_t *pNtk, int fFreeMan)
 
int Abc_NtkSizeOfGlobalBdds (Abc_Ntk_t *pNtk)
 
double Abc_NtkSpacePercentage (Abc_Obj_t *pNode)
 
void Abc_NtkBddImplicationTest ()
 

Function Documentation

Abc_Obj_t * Abc_NodeBddToMuxes ( Abc_Obj_t pNodeOld,
Abc_Ntk_t pNtkNew 
)
static

Function*************************************************************

Synopsis [Converts the node to MUXes.]

Description []

SideEffects []

SeeAlso []

Definition at line 187 of file abcNtbdd.c.

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 }
void st__free_table(st__table *table)
Definition: st.c:81
Definition: cudd.h:278
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
#define Cudd_Regular(node)
Definition: cudd.h:397
int st__ptrcmp(const char *, const char *)
Definition: st.c:480
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
void * pManFunc
Definition: abc.h:191
#define Cudd_IsComplement(node)
Definition: cudd.h:425
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeInv(Abc_Ntk_t *pNtk, Abc_Obj_t *pFanin)
Definition: abcObj.c:662
Definition: st.h:52
if(last==0)
Definition: sparse_int.h:34
Abc_Ntk_t * pNtk
Definition: abc.h:130
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition: abc.h:524
static Abc_Obj_t * Abc_NodeBddToMuxes_rec(DdManager *dd, DdNode *bFunc, Abc_Ntk_t *pNtkNew, st__table *tBdd2Node)
Definition: abcNtbdd.c:218
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
void * pData
Definition: abc.h:145
int st__ptrhash(const char *, int)
Definition: st.c:468
Abc_Obj_t * Abc_NodeBddToMuxes_rec ( DdManager dd,
DdNode bFunc,
Abc_Ntk_t pNtkNew,
st__table tBdd2Node 
)
static

Function*************************************************************

Synopsis [Converts the node to MUXes.]

Description []

SideEffects []

SeeAlso []

Definition at line 218 of file abcNtbdd.c.

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 }
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
#define b1
Definition: extraBdd.h:76
#define Cudd_Regular(node)
Definition: cudd.h:397
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeConst1(Abc_Ntk_t *pNtk)
Definition: abcObj.c:633
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
#define Cudd_IsComplement(node)
Definition: cudd.h:425
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeInv(Abc_Ntk_t *pNtk, Abc_Obj_t *pFanin)
Definition: abcObj.c:662
#define cuddT(node)
Definition: cuddInt.h:636
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
static Abc_Obj_t * Abc_NodeBddToMuxes_rec(DdManager *dd, DdNode *bFunc, Abc_Ntk_t *pNtkNew, st__table *tBdd2Node)
Definition: abcNtbdd.c:218
DdHalfWord index
Definition: cudd.h:279
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
#define cuddE(node)
Definition: cuddInt.h:652
#define assert(ex)
Definition: util_old.h:213
DdNode * Abc_NodeGlobalBdds_rec ( DdManager dd,
Abc_Obj_t pNode,
int  nBddSizeMax,
int  fDropInternal,
ProgressBar pProgress,
int *  pCounter,
int  fVerbose 
)
static

Function*************************************************************

Synopsis [Derives the global BDD for one AIG node.]

Description []

SideEffects []

SeeAlso []

Definition at line 367 of file abcNtbdd.c.

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 }
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
static int Abc_ObjFaninC1(Abc_Obj_t *pObj)
Definition: abc.h:378
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
static void * Abc_ObjGlobalBdd(Abc_Obj_t *pObj)
Definition: abc.h:431
static int Abc_ObjIsNode(Abc_Obj_t *pObj)
Definition: abc.h:355
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
ABC_DLL int Abc_NodeIsMuxType(Abc_Obj_t *pNode)
Definition: abcUtil.c:1301
void Extra_ProgressBarStop(ProgressBar *p)
static void Abc_ObjSetGlobalBdd(Abc_Obj_t *pObj, void *bF)
Definition: abc.h:432
Vec_Int_t vFanouts
Definition: abc.h:144
static Abc_Obj_t * Abc_ObjRegular(Abc_Obj_t *p)
Definition: abc.h:323
unsigned int Cudd_ReadKeys(DdManager *dd)
Definition: cuddAPI.c:1626
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
#define assert(ex)
Definition: util_old.h:213
static void Extra_ProgressBarUpdate(ProgressBar *p, int nItemsCur, char *pString)
Definition: extra.h:243
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
unsigned int Cudd_ReadDead(DdManager *dd)
Definition: cuddAPI.c:1646
static Abc_Obj_t * Abc_ObjFanin(Abc_Obj_t *pObj, int i)
Definition: abc.h:372
static int Abc_ObjIsComplement(Abc_Obj_t *p)
Definition: abc.h:322
ABC_DLL Abc_Obj_t * Abc_NodeRecognizeMux(Abc_Obj_t *pNode, Abc_Obj_t **ppNodeT, Abc_Obj_t **ppNodeE)
Definition: abcUtil.c:1389
void Abc_NtkBddImplicationTest ( )

Function*************************************************************

Synopsis [Experiment with BDD-based representation of implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 568 of file abcNtbdd.c.

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 );
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) );
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 }
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
static abctime Abc_Clock()
Definition: abc_global.h:279
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
#define b0
Definition: extraBdd.h:75
DdNode ** vars
Definition: cuddInt.h:390
#define ABC_PRT(a, t)
Definition: abc_global.h:220
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
void Cudd_Quit(DdManager *unique)
Definition: cuddInit.c:225
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddReorder.c:176
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:669
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
ABC_INT64_T abctime
Definition: abc_global.h:278
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
Abc_Ntk_t* Abc_NtkBddToMuxes ( Abc_Ntk_t pNtk)

Function*************************************************************

Synopsis [Creates the network isomorphic to the union of local BDDs of the nodes.]

Description [The nodes of the local BDDs are converted into the network nodes with logic functions equal to the MUX.]

SideEffects []

SeeAlso []

Definition at line 125 of file abcNtbdd.c.

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 }
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
ABC_DLL Abc_Ntk_t * Abc_NtkStartFrom(Abc_Ntk_t *pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func)
Definition: abcNtk.c:106
ABC_DLL void Abc_NtkFinalize(Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkNew)
Definition: abcNtk.c:302
static ABC_NAMESPACE_IMPL_START void Abc_NtkBddToMuxesPerform(Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkNew)
DECLARATIONS ///.
Definition: abcNtbdd.c:153
static int Abc_NtkIsBddLogic(Abc_Ntk_t *pNtk)
Definition: abc.h:265
#define assert(ex)
Definition: util_old.h:213
void Abc_NtkBddToMuxesPerform ( Abc_Ntk_t pNtk,
Abc_Ntk_t pNtkNew 
)
static

DECLARATIONS ///.

CFile****************************************************************

FileName [abcNtbdd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Procedures to translate between the BDD and the network.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
abcNtbdd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Function*************************************************************

Synopsis [Converts the network to MUXes.]

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file abcNtbdd.c.

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 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static Abc_Obj_t * Abc_NodeBddToMuxes(Abc_Obj_t *pNodeOld, Abc_Ntk_t *pNtkNew)
Definition: abcNtbdd.c:187
ABC_DLL Vec_Ptr_t * Abc_NtkDfs(Abc_Ntk_t *pNtk, int fCollectAll)
Definition: abcDfs.c:81
static int Abc_ObjIsNode(Abc_Obj_t *pObj)
Definition: abc.h:355
DECLARATIONS ///.
Abc_Obj_t * pCopy
Definition: abc.h:148
void Extra_ProgressBarStop(ProgressBar *p)
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
#define assert(ex)
Definition: util_old.h:213
static void Extra_ProgressBarUpdate(ProgressBar *p, int nItemsCur, char *pString)
Definition: extra.h:243
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
void* Abc_NtkBuildGlobalBdds ( Abc_Ntk_t pNtk,
int  nBddSizeMax,
int  fDropInternal,
int  fReorder,
int  fVerbose 
)

Function*************************************************************

Synopsis [Derives global BDDs for the COs of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file abcNtbdd.c.

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 );
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 )
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  {
350  Cudd_AutodynDisable( dd );
351  }
352 // Cudd_PrintInfo( dd, stdout );
353  return dd;
354 }
Vec_Ptr_t * vAttrs
Definition: abc.h:214
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
void * Abc_NtkFreeGlobalBdds(Abc_Ntk_t *pNtk, int fFreeMan)
Definition: abcNtbdd.c:476
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
static int Abc_NtkObjNumMax(Abc_Ntk_t *pNtk)
Definition: abc.h:284
static int Abc_ObjIsBo(Abc_Obj_t *pObj)
Definition: abc.h:350
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition: abcAig.c:683
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
static void * Abc_NtkGlobalBdd(Abc_Ntk_t *pNtk)
Definition: abc.h:428
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
DECLARATIONS ///.
Definition: abcAig.c:52
void * pManFunc
Definition: abc.h:191
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
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
DECLARATIONS ///.
ABC_DLL int Abc_AigCleanup(Abc_Aig_t *pMan)
Definition: abcAig.c:194
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
if(last==0)
Definition: sparse_int.h:34
static int Counter
void Extra_ProgressBarStop(ProgressBar *p)
static void Abc_ObjSetGlobalBdd(Abc_Obj_t *pObj, void *bF)
Definition: abc.h:432
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
void Cudd_AutodynDisable(DdManager *unique)
Definition: cuddAPI.c:708
static int Abc_ObjIsBi(Abc_Obj_t *pObj)
Definition: abc.h:349
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition: abc.h:524
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
DdNode ** vars
Definition: cuddInt.h:390
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
DdNode * one
Definition: cuddInt.h:345
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
#define assert(ex)
Definition: util_old.h:213
static int Abc_ObjIsBox(Abc_Obj_t *pObj)
Definition: abc.h:357
void Cudd_Quit(DdManager *unique)
Definition: cuddInit.c:225
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddReorder.c:176
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:669
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
#define Abc_NtkForEachObj(pNtk, pObj, i)
ITERATORS ///.
Definition: abc.h:446
Abc_Ntk_t* Abc_NtkDeriveFromBdd ( void *  dd0,
void *  bFunc,
char *  pNamePo,
Vec_Ptr_t vNamesPi 
)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Constructs the network isomorphic to the given BDD.]

Description [Assumes that the BDD depends on the variables whose indexes correspond to the names in the array (pNamesPi). Otherwise, returns NULL. The resulting network comes with one node, whose functionality is equal to the given BDD. To decompose this BDD into the network of multiplexers use Abc_NtkBddToMuxes(). To decompose this BDD into an And-Inverter Graph, use Abc_NtkStrash().]

SideEffects []

SeeAlso []

Definition at line 56 of file abcNtbdd.c.

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
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 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
ABC_DLL int Abc_NtkMinimumBase(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcMinBase.c:48
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:740
int size
Definition: cuddInt.h:361
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition: abcNames.c:68
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
char * Extra_UtilStrsav(const char *s)
DdNode * Cudd_bddTransfer(DdManager *ddSource, DdManager *ddDestination, DdNode *f)
Definition: cuddBridge.c:409
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition: abcNtk.c:50
static void check(int expr)
Definition: satSolver.c:46
ABC_DLL void Abc_NodeFreeNames(Vec_Ptr_t *vNames)
Definition: abcNames.c:257
void * pManFunc
Definition: abc.h:191
ABC_DLL Vec_Ptr_t * Abc_NodeGetFakeNames(int nNames)
Definition: abcNames.c:221
if(last==0)
Definition: sparse_int.h:34
static Abc_Obj_t * Abc_NtkCreatePi(Abc_Ntk_t *pNtk)
Definition: abc.h:303
#define cuddT(node)
Definition: cuddInt.h:636
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
unsigned int Cudd_NodeReadIndex(DdNode *node)
Definition: cuddAPI.c:2277
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
static Abc_Obj_t * Abc_NtkCreateNode(Abc_Ntk_t *pNtk)
Definition: abc.h:308
Abc_Ntk_t * Abc_NtkDeriveFromBdd(void *dd0, void *bFunc, char *pNamePo, Vec_Ptr_t *vNamesPi)
FUNCTION DEFINITIONS ///.
Definition: abcNtbdd.c:56
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static Abc_Obj_t * Abc_NtkCreatePo(Abc_Ntk_t *pNtk)
Definition: abc.h:304
char * pName
Definition: abc.h:158
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
void* Abc_NtkFreeGlobalBdds ( Abc_Ntk_t pNtk,
int  fFreeMan 
)

Function*************************************************************

Synopsis [Frees the global BDDs of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 476 of file abcNtbdd.c.

477 {
478  return Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, fFreeMan );
479 }
ABC_DLL void * Abc_NtkAttrFree(Abc_Ntk_t *pNtk, int Attr, int fFreeMan)
DECLARATIONS ///.
Definition: abcUtil.c:50
int Abc_NtkSizeOfGlobalBdds ( Abc_Ntk_t pNtk)

Function*************************************************************

Synopsis [Returns the shared size of global BDDs of the COs.]

Description []

SideEffects []

SeeAlso []

Definition at line 492 of file abcNtbdd.c.

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 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Definition: cudd.h:278
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
static int Abc_NtkCoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:288
static void * Abc_ObjGlobalBdd(Abc_Obj_t *pObj)
Definition: abc.h:431
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
static void ** Vec_PtrArray(Vec_Ptr_t *p)
Definition: vecPtr.h:279
int Cudd_SharingSize(DdNode **nodeArray, int n)
Definition: cuddUtil.c:544
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
double Abc_NtkSpacePercentage ( Abc_Obj_t pNode)

Function*************************************************************

Synopsis [Computes the BDD of the logic cone of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 517 of file abcNtbdd.c.

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 }