src/aig/hop/cudd2.c File Reference

#include "hop.h"
#include "st.h"
Include dependency graph for cudd2.c:

Go to the source code of this file.

Data Structures

struct  Aig_CuddMan_t_

Typedefs

typedef struct Aig_CuddMan_t_ Aig_CuddMan_t

Functions

void Cudd2_Init (unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void *pCudd)
void Cudd2_Quit (void *pCudd)
static Aig_Obj_t * Cudd2_GetArg (void *pArg)
static void Cudd2_SetArg (Aig_Obj_t *pNode, void *pResult)
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)

Variables

static Aig_CuddMan_t * s_pCuddMan = NULL

Typedef Documentation

typedef struct Aig_CuddMan_t_ Aig_CuddMan_t

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

FileName [cudd2.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Minimalistic And-Inverter Graph package.]

Synopsis [Recording AIGs for the BDD operations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id
cudd2.c,v 1.00 2006/10/03 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 28 of file cudd2.c.

Function Documentation

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

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file cudd2.c.

00178 {
00179     Aig_Obj_t * pNode0, * pNode1, * pNode;
00180     pNode0 = Cudd2_GetArg( pArg0 );
00181     pNode1 = Cudd2_GetArg( pArg1 );
00182     pNode  = Aig_And( s_pCuddMan->pAig, pNode0, pNode1 );
00183     Cudd2_SetArg( pNode, pResult );
00184 }

void Cudd2_bddCompose ( void *  pCudd,
void *  pArg0,
void *  pArg1,
int  v,
void *  pResult 
)

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 302 of file cudd2.c.

00303 {
00304     Aig_Obj_t * pNode0, * pNode1, * pNode;
00305     pNode0 = Cudd2_GetArg( pArg0 );
00306     pNode1 = Cudd2_GetArg( pArg1 );
00307     pNode  = Aig_Compose( s_pCuddMan->pAig, pNode0, pNode1, v );
00308     Cudd2_SetArg( pNode, pResult );
00309 }

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 342 of file cudd2.c.

00343 {
00344     Aig_Obj_t * pNode0, * pNode1, * pNode;
00345     pNode0 = Cudd2_GetArg( pArg0 );
00346     pNode1 = Cudd2_GetArg( pArg1 );
00347     pNode  = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
00348     Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
00349 }

void Cudd2_bddIte ( void *  pCudd,
void *  pArg0,
void *  pArg1,
void *  pArg2,
void *  pResult 
)

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 281 of file cudd2.c.

00282 {
00283     Aig_Obj_t * pNode0, * pNode1, * pNode2, * pNode;
00284     pNode0 = Cudd2_GetArg( pArg0 );
00285     pNode1 = Cudd2_GetArg( pArg1 );
00286     pNode2 = Cudd2_GetArg( pArg2 );
00287     pNode  = Aig_Mux( s_pCuddMan->pAig, pNode0, pNode1, pNode2 );
00288     Cudd2_SetArg( pNode, pResult );
00289 }

void Cudd2_bddIthVar ( void *  pCudd,
int  iVar,
void *  pResult 
)

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

Synopsis [Adds elementary variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 157 of file cudd2.c.

00158 {
00159     int v;
00160     assert( s_pCuddMan != NULL );
00161     for ( v = Aig_ManPiNum(s_pCuddMan->pAig); v <= iVar; v++ )
00162         Aig_ObjCreatePi( s_pCuddMan->pAig );
00163     Cudd2_SetArg( Aig_ManPi(s_pCuddMan->pAig, iVar), pResult );
00164 }

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 322 of file cudd2.c.

00323 {
00324     Aig_Obj_t * pNode0, * pNode1, * pNode;
00325     pNode0 = Cudd2_GetArg( pArg0 );
00326     pNode1 = Cudd2_GetArg( pArg1 );
00327     pNode  = Aig_And( s_pCuddMan->pAig, pNode0, Aig_Not(pNode1) );
00328     Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
00329 }

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

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 213 of file cudd2.c.

00214 {
00215     Cudd2_bddAnd( pCudd, pArg0, pArg1, Aig_Not(pResult) );
00216 }

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

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file cudd2.c.

00230 {
00231     Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), pResult );
00232 }

void Cudd2_bddOne ( void *  pCudd,
void *  pResult 
)

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

Synopsis [Registers constant 1 node.]

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file cudd2.c.

00142 {
00143     Cudd2_SetArg( Aig_ManConst1(s_pCuddMan->pAig), pResult );
00144 }

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

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file cudd2.c.

00198 {
00199     Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), Aig_Not(pResult) );
00200 }

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

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 265 of file cudd2.c.

00266 {
00267     Cudd2_bddXor( pCudd, pArg0, pArg1, Aig_Not(pResult) );
00268 }

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

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

Synopsis [Performs BDD operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 245 of file cudd2.c.

00246 {
00247     Aig_Obj_t * pNode0, * pNode1, * pNode;
00248     pNode0 = Cudd2_GetArg( pArg0 );
00249     pNode1 = Cudd2_GetArg( pArg1 );
00250     pNode  = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
00251     Cudd2_SetArg( pNode, pResult );
00252 }

static Aig_Obj_t* Cudd2_GetArg ( void *  pArg  )  [static]

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

Synopsis [Fetches AIG node corresponding to the BDD node from the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file cudd2.c.

00099 {
00100     Aig_Obj_t * pNode;
00101     assert( s_pCuddMan != NULL );
00102     if ( !st_lookup( s_pCuddMan->pTable, (char *)Aig_Regular(pArg), (char **)&pNode ) )
00103     {
00104         printf( "Cudd2_GetArg(): An argument BDD is not in the hash table.\n" );
00105         return NULL;
00106     }
00107     return Aig_NotCond( pNode, Aig_IsComplement(pArg) );
00108 }

void Cudd2_Init ( unsigned int  numVars,
unsigned int  numVarsZ,
unsigned int  numSlots,
unsigned int  cacheSize,
unsigned long  maxMemory,
void *  pCudd 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Start AIG recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 53 of file cudd2.c.

00054 {
00055     int v;
00056     // start the BDD-to-AIG manager when the first BDD manager is allocated
00057     if ( s_pCuddMan != NULL )
00058         return;
00059     s_pCuddMan = ALLOC( Aig_CuddMan_t, 1 );
00060     s_pCuddMan->pAig = Aig_ManStart();
00061     s_pCuddMan->pTable = st_init_table( st_ptrcmp, st_ptrhash );
00062     for ( v = 0; v < (int)numVars; v++ )
00063         Aig_ObjCreatePi( s_pCuddMan->pAig );
00064 }

void Cudd2_Quit ( void *  pCudd  ) 

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

Synopsis [Stops AIG recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file cudd2.c.

00078 {
00079     assert( s_pCuddMan != NULL );
00080     Aig_ManDumpBlif( s_pCuddMan->pAig, "aig_temp.blif" );
00081     Aig_ManStop( s_pCuddMan->pAig );
00082     st_free_table( s_pCuddMan->pTable );
00083     free( s_pCuddMan );
00084     s_pCuddMan = NULL;
00085 }

static void Cudd2_SetArg ( Aig_Obj_t *  pNode,
void *  pResult 
) [static]

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

Synopsis [Inserts the AIG node corresponding to the BDD node into the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file cudd2.c.

00122 {
00123     assert( s_pCuddMan != NULL );
00124     if ( st_is_member( s_pCuddMan->pTable, (char *)Aig_Regular(pResult) ) )
00125         return;
00126     pNode = Aig_NotCond( pNode,  Aig_IsComplement(pResult) );
00127     st_insert( s_pCuddMan->pTable, (char *)Aig_Regular(pResult), (char *)pNode );
00128 }

Variable Documentation

Aig_CuddMan_t* s_pCuddMan = NULL [static]

Definition at line 36 of file cudd2.c.

Generated on Tue Jan 5 12:18:20 2010 for abc70930 by  doxygen 1.6.1