abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bbrNtbdd.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bbrNtbdd.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [BDD-based reachability analysis.]
8 
9  Synopsis [Procedures to construct global BDDs for 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: bbrNtbdd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "bbr.h"
22 //#include "bar.h"
23 
25 
26 
27 typedef char ProgressBar;
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 static inline void Aig_ObjSetGlobalBdd( Aig_Obj_t * pObj, DdNode * bFunc ) { pObj->pData = bFunc; }
34 static inline void Aig_ObjCleanGlobalBdd( DdManager * dd, Aig_Obj_t * pObj ) { Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); pObj->pData = NULL; }
35 
36 ////////////////////////////////////////////////////////////////////////
37 /// FUNCTION DEFINITIONS ///
38 ////////////////////////////////////////////////////////////////////////
39 
40 /**Function*************************************************************
41 
42  Synopsis [Derives the global BDD for one AIG node.]
43 
44  Description []
45 
46  SideEffects []
47 
48  SeeAlso []
49 
50 ***********************************************************************/
51 DdNode * Bbr_NodeGlobalBdds_rec( DdManager * dd, Aig_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose )
52 {
53  DdNode * bFunc, * bFunc0, * bFunc1;
54  assert( !Aig_IsComplement(pNode) );
55  if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
56  {
57 // Extra_ProgressBarStop( pProgress );
58  if ( fVerbose )
59  printf( "The number of live nodes reached %d.\n", nBddSizeMax );
60  fflush( stdout );
61  return NULL;
62  }
63  // if the result is available return
64  if ( Aig_ObjGlobalBdd(pNode) == NULL )
65  {
66  // compute the result for both branches
67  bFunc0 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );
68  if ( bFunc0 == NULL )
69  return NULL;
70  Cudd_Ref( bFunc0 );
71  bFunc1 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin1(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );
72  if ( bFunc1 == NULL )
73  return NULL;
74  Cudd_Ref( bFunc1 );
75  bFunc0 = Cudd_NotCond( bFunc0, Aig_ObjFaninC0(pNode) );
76  bFunc1 = Cudd_NotCond( bFunc1, Aig_ObjFaninC1(pNode) );
77  // get the final result
78  bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
79  Cudd_RecursiveDeref( dd, bFunc0 );
80  Cudd_RecursiveDeref( dd, bFunc1 );
81  // add the number of used nodes
82  (*pCounter)++;
83  // set the result
84  assert( Aig_ObjGlobalBdd(pNode) == NULL );
85  Aig_ObjSetGlobalBdd( pNode, bFunc );
86  // increment the progress bar
87 // if ( pProgress )
88 // Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
89  }
90  // prepare the return value
91  bFunc = Aig_ObjGlobalBdd(pNode);
92  // dereference BDD at the node
93  if ( --pNode->nRefs == 0 && fDropInternal )
94  {
95  Cudd_Deref( bFunc );
96  Aig_ObjSetGlobalBdd( pNode, NULL );
97  }
98  return bFunc;
99 }
100 
101 /**Function*************************************************************
102 
103  Synopsis [Frees the global BDDs of the network.]
104 
105  Description []
106 
107  SideEffects []
108 
109  SeeAlso []
110 
111 ***********************************************************************/
113 {
114  Aig_Obj_t * pObj;
115  int i;
116  Aig_ManForEachObj( p, pObj, i )
117  if ( Aig_ObjGlobalBdd(pObj) )
118  Aig_ObjCleanGlobalBdd( dd, pObj );
119 }
120 
121 /**Function*************************************************************
122 
123  Synopsis [Returns the shared size of global BDDs of the COs.]
124 
125  Description []
126 
127  SideEffects []
128 
129  SeeAlso []
130 
131 ***********************************************************************/
133 {
134  Vec_Ptr_t * vFuncsGlob;
135  Aig_Obj_t * pObj;
136  int RetValue, i;
137  // complement the global functions
138  vFuncsGlob = Vec_PtrAlloc( Aig_ManCoNum(p) );
139  Aig_ManForEachCo( p, pObj, i )
140  Vec_PtrPush( vFuncsGlob, Aig_ObjGlobalBdd(pObj) );
141  RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
142  Vec_PtrFree( vFuncsGlob );
143  return RetValue;
144 }
145 
146 /**Function*************************************************************
147 
148  Synopsis [Recursively computes global BDDs for the AIG in the manager.]
149 
150  Description [On exit, BDDs are stored in the pNode->pData fields.]
151 
152  SideEffects []
153 
154  SeeAlso []
155 
156 ***********************************************************************/
157 DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose )
158 {
159  ProgressBar * pProgress = NULL;
160  Aig_Obj_t * pObj;
161  DdManager * dd;
162  DdNode * bFunc;
163  int i, Counter;
164  // start the manager
166  // set reordering
167  if ( fReorder )
169  // prepare to construct global BDDs
170  Aig_ManCleanData( p );
171  // assign the constant node BDD
172  Aig_ObjSetGlobalBdd( Aig_ManConst1(p), dd->one ); Cudd_Ref( dd->one );
173  // set the elementary variables
174  Aig_ManForEachCi( p, pObj, i )
175  {
176  Aig_ObjSetGlobalBdd( pObj, dd->vars[i] ); Cudd_Ref( dd->vars[i] );
177  }
178 
179  // collect the global functions of the COs
180  Counter = 0;
181  // construct the BDDs
182 // pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p) );
183  Aig_ManForEachCo( p, pObj, i )
184  {
185  bFunc = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose );
186  if ( bFunc == NULL )
187  {
188  if ( fVerbose )
189  printf( "Constructing global BDDs is aborted.\n" );
190  Aig_ManFreeGlobalBdds( p, dd );
191  Cudd_Quit( dd );
192  // reset references
193  Aig_ManResetRefs( p );
194  return NULL;
195  }
196  bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pObj) ); Cudd_Ref( bFunc );
197  Aig_ObjSetGlobalBdd( pObj, bFunc );
198  }
199 // Extra_ProgressBarStop( pProgress );
200  // reset references
201  Aig_ManResetRefs( p );
202  // reorder one more time
203  if ( fReorder )
204  {
206  Cudd_AutodynDisable( dd );
207  }
208 // Cudd_PrintInfo( dd, stdout );
209  return dd;
210 }
211 
212 ////////////////////////////////////////////////////////////////////////
213 /// END OF FILE ///
214 ////////////////////////////////////////////////////////////////////////
215 
216 
218 
ABC_NAMESPACE_IMPL_START typedef char ProgressBar
Definition: bbrNtbdd.c:27
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
void * pData
Definition: aig.h:87
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static ABC_NAMESPACE_HEADER_START DdNode * Aig_ObjGlobalBdd(Aig_Obj_t *pObj)
INCLUDES ///.
Definition: bbr.h:51
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
static void Aig_ObjSetGlobalBdd(Aig_Obj_t *pObj, DdNode *bFunc)
DECLARATIONS ///.
Definition: bbrNtbdd.c:33
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
int Aig_ManSizeOfGlobalBdds(Aig_Man_t *p)
Definition: bbrNtbdd.c:132
void Aig_ManFreeGlobalBdds(Aig_Man_t *p, DdManager *dd)
Definition: bbrNtbdd.c:112
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
DECLARATIONS ///.
DdManager * Aig_ManComputeGlobalBdds(Aig_Man_t *p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose)
Definition: bbrNtbdd.c:157
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
DdNode * Bbr_NodeGlobalBdds_rec(DdManager *dd, Aig_Obj_t *pNode, int nBddSizeMax, int fDropInternal, ProgressBar *pProgress, int *pCounter, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: bbrNtbdd.c:51
Definition: aig.h:69
static int Counter
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
void Cudd_AutodynDisable(DdManager *unique)
Definition: cuddAPI.c:708
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
DdNode ** vars
Definition: cuddInt.h:390
DdNode * one
Definition: cuddInt.h:345
unsigned int Cudd_ReadKeys(DdManager *dd)
Definition: cuddAPI.c:1626
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
#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
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
unsigned int Cudd_ReadDead(DdManager *dd)
Definition: cuddAPI.c:1646
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
static void ** Vec_PtrArray(Vec_Ptr_t *p)
Definition: vecPtr.h:279
int Cudd_SharingSize(DdNode **nodeArray, int n)
Definition: cuddUtil.c:544
void Aig_ManResetRefs(Aig_Man_t *p)
Definition: aigUtil.c:122
unsigned int nRefs
Definition: aig.h:81
static void Aig_ObjCleanGlobalBdd(DdManager *dd, Aig_Obj_t *pObj)
Definition: bbrNtbdd.c:34
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223