abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Macros | Functions
cudd2.h File Reference

Go to the source code of this file.

Macros

#define MSG(msg)   (printf("%s = \n",(msg)));
 

Functions

ABC_NAMESPACE_HEADER_START void Cudd2_Init (unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void *pCudd)
 INCLUDES ///. More...
 
void Cudd2_Quit (void *pCudd)
 
void Cudd2_bddOne (void *pCudd, void *pResult)
 
void Cudd2_bddIthVar (void *pCudd, int iVar, void *pResult)
 
void Cudd2_bddAnd (void *pCudd, void *pArg0, void *pArg1, void *pResult)
 
void Cudd2_bddOr (void *pCudd, void *pArg0, void *pArg1, void *pResult)
 
void Cudd2_bddNand (void *pCudd, void *pArg0, void *pArg1, void *pResult)
 
void Cudd2_bddNor (void *pCudd, void *pArg0, void *pArg1, void *pResult)
 
void Cudd2_bddXor (void *pCudd, void *pArg0, void *pArg1, void *pResult)
 
void Cudd2_bddXnor (void *pCudd, void *pArg0, void *pArg1, void *pResult)
 
void Cudd2_bddIte (void *pCudd, void *pArg0, void *pArg1, void *pArg2, void *pResult)
 
void Cudd2_bddCompose (void *pCudd, void *pArg0, void *pArg1, int v, void *pResult)
 
void Cudd2_bddLeq (void *pCudd, void *pArg0, void *pArg1, int Result)
 
void Cudd2_bddEqual (void *pCudd, void *pArg0, void *pArg1, int Result)
 

Macro Definition Documentation

#define MSG (   msg)    (printf("%s = \n",(msg)));

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

FileName [cudd2.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Minimalistic And-Inverter Graph package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 3, 2006.]

Revision [

Id:
cudd2.h,v 1.00 2006/05/11 00:00:00 alanmi Exp

]

Definition at line 27 of file cudd2.h.

Function Documentation

void Cudd2_bddAnd ( void *  pCudd,
void *  pArg0,
void *  pArg1,
void *  pResult 
)

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 180 of file cudd2.c.

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 }
Cudd2_GetArg
static Aig_Obj_t * Cudd2_GetArg(void *pArg)
Definition: cudd2.c:101
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_Obj_t_
Definition: aig.h:69
s_pCuddMan
static Aig_CuddMan_t * s_pCuddMan
Definition: cudd2.c:39
Cudd2_SetArg
static void Cudd2_SetArg(Aig_Obj_t *pNode, void *pResult)
Definition: cudd2.c:124
void Cudd2_bddCompose ( void *  pCudd,
void *  pArg0,
void *  pArg1,
int  v,
void *  pResult 
)

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 305 of file cudd2.c.

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 }
Cudd2_GetArg
static Aig_Obj_t * Cudd2_GetArg(void *pArg)
Definition: cudd2.c:101
Aig_Obj_t_
Definition: aig.h:69
s_pCuddMan
static Aig_CuddMan_t * s_pCuddMan
Definition: cudd2.c:39
Cudd2_SetArg
static void Cudd2_SetArg(Aig_Obj_t *pNode, void *pResult)
Definition: cudd2.c:124
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
void Cudd2_bddEqual ( void *  pCudd,
void *  pArg0,
void *  pArg1,
int  Result 
)

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

Synopsis [Should be called after each equality check.]

Description [Result should be 1 if they are equal.]

SideEffects []

SeeAlso []

Definition at line 345 of file cudd2.c.

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 }
Aig_Exor
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:220
Cudd2_GetArg
static Aig_Obj_t * Cudd2_GetArg(void *pArg)
Definition: cudd2.c:101
Aig_Obj_t_
Definition: aig.h:69
s_pCuddMan
static Aig_CuddMan_t * s_pCuddMan
Definition: cudd2.c:39
void Cudd2_bddIte ( void *  pCudd,
void *  pArg0,
void *  pArg1,
void *  pArg2,
void *  pResult 
)

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 284 of file cudd2.c.

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 }
Cudd2_GetArg
static Aig_Obj_t * Cudd2_GetArg(void *pArg)
Definition: cudd2.c:101
Aig_Obj_t_
Definition: aig.h:69
s_pCuddMan
static Aig_CuddMan_t * s_pCuddMan
Definition: cudd2.c:39
Cudd2_SetArg
static void Cudd2_SetArg(Aig_Obj_t *pNode, void *pResult)
Definition: cudd2.c:124
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
void Cudd2_bddIthVar ( void *  pCudd,
int  iVar,
void *  pResult 
)

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

Synopsis [Adds elementary variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file cudd2.c.

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 }
s_pCuddMan
static Aig_CuddMan_t * s_pCuddMan
Definition: cudd2.c:39
Cudd2_SetArg
static void Cudd2_SetArg(Aig_Obj_t *pNode, void *pResult)
Definition: cudd2.c:124
assert
#define assert(ex)
Definition: util_old.h:213
void Cudd2_bddLeq ( void *  pCudd,
void *  pArg0,
void *  pArg1,
int  Result 
)

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

Synopsis [Should be called after each containment check.]

Description [Result should be 1 if Cudd2_bddLeq returned 1.]

SideEffects []

SeeAlso []

Definition at line 325 of file cudd2.c.

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 }
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
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_Obj_t_
Definition: aig.h:69
s_pCuddMan
static Aig_CuddMan_t * s_pCuddMan
Definition: cudd2.c:39
void Cudd2_bddNand ( void *  pCudd,
void *  pArg0,
void *  pArg1,
void *  pResult 
)

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 216 of file cudd2.c.

217 {
218  Cudd2_bddAnd( pCudd, pArg0, pArg1, Aig_Not(pResult) );
219 }
Aig_Not
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
Cudd2_bddAnd
void Cudd2_bddAnd(void *pCudd, void *pArg0, void *pArg1, void *pResult)
Definition: cudd2.c:180
void Cudd2_bddNor ( void *  pCudd,
void *  pArg0,
void *  pArg1,
void *  pResult 
)

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 232 of file cudd2.c.

233 {
234  Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), pResult );
235 }
Aig_Not
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
Cudd2_bddAnd
void Cudd2_bddAnd(void *pCudd, void *pArg0, void *pArg1, void *pResult)
Definition: cudd2.c:180
void Cudd2_bddOne ( void *  pCudd,
void *  pResult 
)

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

Synopsis [Registers constant 1 node.]

Description []

SideEffects []

SeeAlso []

Definition at line 144 of file cudd2.c.

145 {
146  Cudd2_SetArg( Aig_ManConst1(s_pCuddMan->pAig), pResult );
147 }
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
Cudd2_SetArg
static void Cudd2_SetArg(Aig_Obj_t *pNode, void *pResult)
Definition: cudd2.c:124
void Cudd2_bddOr ( void *  pCudd,
void *  pArg0,
void *  pArg1,
void *  pResult 
)

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 200 of file cudd2.c.

201 {
202  Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), Aig_Not(pResult) );
203 }
Aig_Not
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
Cudd2_bddAnd
void Cudd2_bddAnd(void *pCudd, void *pArg0, void *pArg1, void *pResult)
Definition: cudd2.c:180
void Cudd2_bddXnor ( void *  pCudd,
void *  pArg0,
void *  pArg1,
void *  pResult 
)

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 268 of file cudd2.c.

269 {
270  Cudd2_bddXor( pCudd, pArg0, pArg1, Aig_Not(pResult) );
271 }
Aig_Not
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
Cudd2_bddXor
void Cudd2_bddXor(void *pCudd, void *pArg0, void *pArg1, void *pResult)
Definition: cudd2.c:248
void Cudd2_bddXor ( void *  pCudd,
void *  pArg0,
void *  pArg1,
void *  pResult 
)

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 248 of file cudd2.c.

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 }
Aig_Exor
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:220
Cudd2_GetArg
static Aig_Obj_t * Cudd2_GetArg(void *pArg)
Definition: cudd2.c:101
Aig_Obj_t_
Definition: aig.h:69
s_pCuddMan
static Aig_CuddMan_t * s_pCuddMan
Definition: cudd2.c:39
Cudd2_SetArg
static void Cudd2_SetArg(Aig_Obj_t *pNode, void *pResult)
Definition: cudd2.c:124
ABC_NAMESPACE_HEADER_START void Cudd2_Init ( unsigned int  numVars,
unsigned int  numVarsZ,
unsigned int  numSlots,
unsigned int  cacheSize,
unsigned long  maxMemory,
void *  pCudd 
)

INCLUDES ///.

PARAMETERS ///BASIC TYPES ///MACRO DEFINITIONS ///ITERATORS ///FUNCTION DECLARATIONS ///

INCLUDES ///.

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

Synopsis [Start AIG recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 56 of file cudd2.c.

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 }
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
st__ptrcmp
int st__ptrcmp(const char *, const char *)
Definition: st.c:480
st__init_table
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
ALLOC
#define ALLOC(type, num)
Definition: avl.h:27
s_pCuddMan
static Aig_CuddMan_t * s_pCuddMan
Definition: cudd2.c:39
Aig_CuddMan_t
typedefABC_NAMESPACE_IMPL_START struct Aig_CuddMan_t_ Aig_CuddMan_t
DECLARATIONS ///.
Definition: cudd2.c:31
st__ptrhash
int st__ptrhash(const char *, int)
Definition: st.c:468
void Cudd2_Quit ( void *  pCudd)

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

Synopsis [Stops AIG recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file cudd2.c.

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 }
st__free_table
void st__free_table(st__table *table)
Definition: st.c:81
free
VOID_HACK free()
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
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
assert
#define assert(ex)
Definition: util_old.h:213