abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cudd2.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [cudd2.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Minimalistic And-Inverter Graph package.]
8 
9  Synopsis [Recording AIGs for the BDD operations.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - October 3, 2006.]
16 
17  Revision [$Id: cudd2.c,v 1.00 2006/10/03 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "hop.h"
22 #include "misc/st/st.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 typedef struct Aig_CuddMan_t_ Aig_CuddMan_t;
32 struct Aig_CuddMan_t_
33 {
34  Aig_Man_t * pAig; // internal AIG package
35  st__table * pTable; // hash table mapping BDD nodes into AIG nodes
36 };
37 
38 // static Cudd AIG manager used in this experiment
39 static Aig_CuddMan_t * s_pCuddMan = NULL;
40 
41 ////////////////////////////////////////////////////////////////////////
42 /// FUNCTION DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44 
45 /**Function*************************************************************
46 
47  Synopsis [Start AIG recording.]
48 
49  Description []
50 
51  SideEffects []
52 
53  SeeAlso []
54 
55 ***********************************************************************/
56 void Cudd2_Init( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd )
57 {
58  int v;
59  // start the BDD-to-AIG manager when the first BDD manager is allocated
60  if ( s_pCuddMan != NULL )
61  return;
62  s_pCuddMan = ALLOC( Aig_CuddMan_t, 1 );
63  s_pCuddMan->pAig = Aig_ManStart();
64  s_pCuddMan->pTable = st__init_table( st__ptrcmp, st__ptrhash );
65  for ( v = 0; v < (int)numVars; v++ )
66  Aig_ObjCreatePi( s_pCuddMan->pAig );
67 }
68 
69 /**Function*************************************************************
70 
71  Synopsis [Stops AIG recording.]
72 
73  Description []
74 
75  SideEffects []
76 
77  SeeAlso []
78 
79 ***********************************************************************/
80 void Cudd2_Quit( void * pCudd )
81 {
82  assert( s_pCuddMan != NULL );
83  Aig_ManDumpBlif( s_pCuddMan->pAig, "aig_temp.blif", NULL, NULL );
84  Aig_ManStop( s_pCuddMan->pAig );
85  st__free_table( s_pCuddMan->pTable );
86  free( s_pCuddMan );
87  s_pCuddMan = NULL;
88 }
89 
90 /**Function*************************************************************
91 
92  Synopsis [Fetches AIG node corresponding to the BDD node from the hash table.]
93 
94  Description []
95 
96  SideEffects []
97 
98  SeeAlso []
99 
100 ***********************************************************************/
101 static Aig_Obj_t * Cudd2_GetArg( void * pArg )
102 {
103  Aig_Obj_t * pNode;
104  assert( s_pCuddMan != NULL );
105  if ( ! st__lookup( s_pCuddMan->pTable, (char *)Aig_Regular(pArg), (char **)&pNode ) )
106  {
107  printf( "Cudd2_GetArg(): An argument BDD is not in the hash table.\n" );
108  return NULL;
109  }
110  return Aig_NotCond( pNode, Aig_IsComplement(pArg) );
111 }
112 
113 /**Function*************************************************************
114 
115  Synopsis [Inserts the AIG node corresponding to the BDD node into the hash table.]
116 
117  Description []
118 
119  SideEffects []
120 
121  SeeAlso []
122 
123 ***********************************************************************/
124 static void Cudd2_SetArg( Aig_Obj_t * pNode, void * pResult )
125 {
126  assert( s_pCuddMan != NULL );
127  if ( st__is_member( s_pCuddMan->pTable, (char *)Aig_Regular(pResult) ) )
128  return;
129  pNode = Aig_NotCond( pNode, Aig_IsComplement(pResult) );
130  st__insert( s_pCuddMan->pTable, (char *)Aig_Regular(pResult), (char *)pNode );
131 }
132 
133 /**Function*************************************************************
134 
135  Synopsis [Registers constant 1 node.]
136 
137  Description []
138 
139  SideEffects []
140 
141  SeeAlso []
142 
143 ***********************************************************************/
144 void Cudd2_bddOne( void * pCudd, void * pResult )
145 {
146  Cudd2_SetArg( Aig_ManConst1(s_pCuddMan->pAig), pResult );
147 }
148 
149 /**Function*************************************************************
150 
151  Synopsis [Adds elementary variable.]
152 
153  Description []
154 
155  SideEffects []
156 
157  SeeAlso []
158 
159 ***********************************************************************/
160 void Cudd2_bddIthVar( void * pCudd, int iVar, void * pResult )
161 {
162  int v;
163  assert( s_pCuddMan != NULL );
164  for ( v = Aig_ManPiNum(s_pCuddMan->pAig); v <= iVar; v++ )
165  Aig_ObjCreatePi( s_pCuddMan->pAig );
166  Cudd2_SetArg( Aig_ManPi(s_pCuddMan->pAig, iVar), pResult );
167 }
168 
169 /**Function*************************************************************
170 
171  Synopsis [Performs BDD operation.]
172 
173  Description []
174 
175  SideEffects []
176 
177  SeeAlso []
178 
179 ***********************************************************************/
180 void Cudd2_bddAnd( void * pCudd, void * pArg0, void * pArg1, void * pResult )
181 {
182  Aig_Obj_t * pNode0, * pNode1, * pNode;
183  pNode0 = Cudd2_GetArg( pArg0 );
184  pNode1 = Cudd2_GetArg( pArg1 );
185  pNode = Aig_And( s_pCuddMan->pAig, pNode0, pNode1 );
186  Cudd2_SetArg( pNode, pResult );
187 }
188 
189 /**Function*************************************************************
190 
191  Synopsis [Performs BDD operation.]
192 
193  Description []
194 
195  SideEffects []
196 
197  SeeAlso []
198 
199 ***********************************************************************/
200 void Cudd2_bddOr( void * pCudd, void * pArg0, void * pArg1, void * pResult )
201 {
202  Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), Aig_Not(pResult) );
203 }
204 
205 /**Function*************************************************************
206 
207  Synopsis [Performs BDD operation.]
208 
209  Description []
210 
211  SideEffects []
212 
213  SeeAlso []
214 
215 ***********************************************************************/
216 void Cudd2_bddNand( void * pCudd, void * pArg0, void * pArg1, void * pResult )
217 {
218  Cudd2_bddAnd( pCudd, pArg0, pArg1, Aig_Not(pResult) );
219 }
220 
221 /**Function*************************************************************
222 
223  Synopsis [Performs BDD operation.]
224 
225  Description []
226 
227  SideEffects []
228 
229  SeeAlso []
230 
231 ***********************************************************************/
232 void Cudd2_bddNor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
233 {
234  Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), pResult );
235 }
236 
237 /**Function*************************************************************
238 
239  Synopsis [Performs BDD operation.]
240 
241  Description []
242 
243  SideEffects []
244 
245  SeeAlso []
246 
247 ***********************************************************************/
248 void Cudd2_bddXor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
249 {
250  Aig_Obj_t * pNode0, * pNode1, * pNode;
251  pNode0 = Cudd2_GetArg( pArg0 );
252  pNode1 = Cudd2_GetArg( pArg1 );
253  pNode = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
254  Cudd2_SetArg( pNode, pResult );
255 }
256 
257 /**Function*************************************************************
258 
259  Synopsis [Performs BDD operation.]
260 
261  Description []
262 
263  SideEffects []
264 
265  SeeAlso []
266 
267 ***********************************************************************/
268 void Cudd2_bddXnor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
269 {
270  Cudd2_bddXor( pCudd, pArg0, pArg1, Aig_Not(pResult) );
271 }
272 
273 /**Function*************************************************************
274 
275  Synopsis [Performs BDD operation.]
276 
277  Description []
278 
279  SideEffects []
280 
281  SeeAlso []
282 
283 ***********************************************************************/
284 void Cudd2_bddIte( void * pCudd, void * pArg0, void * pArg1, void * pArg2, void * pResult )
285 {
286  Aig_Obj_t * pNode0, * pNode1, * pNode2, * pNode;
287  pNode0 = Cudd2_GetArg( pArg0 );
288  pNode1 = Cudd2_GetArg( pArg1 );
289  pNode2 = Cudd2_GetArg( pArg2 );
290  pNode = Aig_Mux( s_pCuddMan->pAig, pNode0, pNode1, pNode2 );
291  Cudd2_SetArg( pNode, pResult );
292 }
293 
294 /**Function*************************************************************
295 
296  Synopsis [Performs BDD operation.]
297 
298  Description []
299 
300  SideEffects []
301 
302  SeeAlso []
303 
304 ***********************************************************************/
305 void Cudd2_bddCompose( void * pCudd, void * pArg0, void * pArg1, int v, void * pResult )
306 {
307  Aig_Obj_t * pNode0, * pNode1, * pNode;
308  pNode0 = Cudd2_GetArg( pArg0 );
309  pNode1 = Cudd2_GetArg( pArg1 );
310  pNode = Aig_Compose( s_pCuddMan->pAig, pNode0, pNode1, v );
311  Cudd2_SetArg( pNode, pResult );
312 }
313 
314 /**Function*************************************************************
315 
316  Synopsis [Should be called after each containment check.]
317 
318  Description [Result should be 1 if Cudd2_bddLeq returned 1.]
319 
320  SideEffects []
321 
322  SeeAlso []
323 
324 ***********************************************************************/
325 void Cudd2_bddLeq( void * pCudd, void * pArg0, void * pArg1, int Result )
326 {
327  Aig_Obj_t * pNode0, * pNode1, * pNode;
328  pNode0 = Cudd2_GetArg( pArg0 );
329  pNode1 = Cudd2_GetArg( pArg1 );
330  pNode = Aig_And( s_pCuddMan->pAig, pNode0, Aig_Not(pNode1) );
331  Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
332 }
333 
334 /**Function*************************************************************
335 
336  Synopsis [Should be called after each equality check.]
337 
338  Description [Result should be 1 if they are equal.]
339 
340  SideEffects []
341 
342  SeeAlso []
343 
344 ***********************************************************************/
345 void Cudd2_bddEqual( void * pCudd, void * pArg0, void * pArg1, int Result )
346 {
347  Aig_Obj_t * pNode0, * pNode1, * pNode;
348  pNode0 = Cudd2_GetArg( pArg0 );
349  pNode1 = Cudd2_GetArg( pArg1 );
350  pNode = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
351  Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
352 }
353 
354 ////////////////////////////////////////////////////////////////////////
355 /// END OF FILE ///
356 ////////////////////////////////////////////////////////////////////////
357 
358 
359 ABC_NAMESPACE_IMPL_END
360 
st__free_table
void st__free_table(st__table *table)
Definition: st.c:81
free
VOID_HACK free()
Cudd2_bddOne
void Cudd2_bddOne(void *pCudd, void *pResult)
Definition: cudd2.c:144
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Cudd2_bddIthVar
void Cudd2_bddIthVar(void *pCudd, int iVar, void *pResult)
Definition: cudd2.c:160
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
st__insert
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
Aig_Exor
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:220
Cudd2_bddNor
void Cudd2_bddNor(void *pCudd, void *pArg0, void *pArg1, void *pResult)
Definition: cudd2.c:232
Cudd2_bddNand
void Cudd2_bddNand(void *pCudd, void *pArg0, void *pArg1, void *pResult)
Definition: cudd2.c:216
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Cudd2_bddLeq
void Cudd2_bddLeq(void *pCudd, void *pArg0, void *pArg1, int Result)
Definition: cudd2.c:325
st__ptrcmp
int st__ptrcmp(const char *, const char *)
Definition: st.c:480
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Cudd2_bddIte
void Cudd2_bddIte(void *pCudd, void *pArg0, void *pArg1, void *pArg2, void *pResult)
Definition: cudd2.c:284
Cudd2_bddEqual
void Cudd2_bddEqual(void *pCudd, void *pArg0, void *pArg1, int Result)
Definition: cudd2.c:345
Aig_Not
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
Cudd2_GetArg
static Aig_Obj_t * Cudd2_GetArg(void *pArg)
Definition: cudd2.c:101
st__is_member
#define st__is_member(table, key)
Definition: st.h:70
Aig_CuddMan_t_::pAig
Aig_Man_t * pAig
Definition: cudd2.c:34
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
st__init_table
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
Cudd2_bddXor
void Cudd2_bddXor(void *pCudd, void *pArg0, void *pArg1, void *pResult)
Definition: cudd2.c:248
ALLOC
#define ALLOC(type, num)
Definition: avl.h:27
Cudd2_Quit
void Cudd2_Quit(void *pCudd)
Definition: cudd2.c:80
st__table
Definition: st.h:52
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_Obj_t_
Definition: aig.h:69
Aig_CuddMan_t_::pTable
st__table * pTable
Definition: cudd2.c:35
Aig_ManDumpBlif
void Aig_ManDumpBlif(Aig_Man_t *p, char *pFileName, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vPoNames)
Definition: aigUtil.c:733
s_pCuddMan
static Aig_CuddMan_t * s_pCuddMan
Definition: cudd2.c:39
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Cudd2_SetArg
static void Cudd2_SetArg(Aig_Obj_t *pNode, void *pResult)
Definition: cudd2.c:124
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
Aig_Mux
Aig_Obj_t * Aig_Mux(Aig_Man_t *p, Aig_Obj_t *pC, Aig_Obj_t *p1, Aig_Obj_t *p0)
Definition: aigOper.c:317
Cudd2_bddOr
void Cudd2_bddOr(void *pCudd, void *pArg0, void *pArg1, void *pResult)
Definition: cudd2.c:200
Cudd2_bddAnd
void Cudd2_bddAnd(void *pCudd, void *pArg0, void *pArg1, void *pResult)
Definition: cudd2.c:180
Cudd2_Init
void Cudd2_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void *pCudd)
FUNCTION DEFINITIONS ///.
Definition: cudd2.c:56
Cudd2_bddCompose
void Cudd2_bddCompose(void *pCudd, void *pArg0, void *pArg1, int v, void *pResult)
Definition: cudd2.c:305
assert
#define assert(ex)
Definition: util_old.h:213
Aig_CuddMan_t
typedefABC_NAMESPACE_IMPL_START struct Aig_CuddMan_t_ Aig_CuddMan_t
DECLARATIONS ///.
Definition: cudd2.c:31
Aig_Compose
Aig_Obj_t * Aig_Compose(Aig_Man_t *p, Aig_Obj_t *pRoot, Aig_Obj_t *pFunc, int iVar)
Definition: aigDfs.c:966
Cudd2_bddXnor
void Cudd2_bddXnor(void *pCudd, void *pArg0, void *pArg1, void *pResult)
Definition: cudd2.c:268
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Aig_CuddMan_t_
Definition: cudd2.c:32
st__ptrhash
int st__ptrhash(const char *, int)
Definition: st.c:468