cudd2.c File Reference

#include "hop.h"
#include "misc/st/st.h"

Go to the source code of this file.

Data Structures
struct	Aig_CuddMan_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Aig_CuddMan_t_	Aig_CuddMan_t
	DECLARATIONS ///. More...

Functions
void	Cudd2_Init (unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void *pCudd)
	FUNCTION DEFINITIONS ///. More...
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 typedefABC_NAMESPACE_IMPL_START struct Aig_CuddMan_t_ Aig_CuddMan_t

DECLARATIONS ///.

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

]

Definition at line 31 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 180 of file cudd2.c.

{
    Aig_Obj_t * pNode0, * pNode1, * pNode;
    pNode0 = Cudd2_GetArg( pArg0 );
    pNode1 = Cudd2_GetArg( pArg1 );
    pNode  = Aig_And( s_pCuddMan->pAig, pNode0, pNode1 );
    Cudd2_SetArg( pNode, pResult );
}

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.

{
    Aig_Obj_t * pNode0, * pNode1, * pNode;
    pNode0 = Cudd2_GetArg( pArg0 );
    pNode1 = Cudd2_GetArg( pArg1 );
    pNode  = Aig_Compose( s_pCuddMan->pAig, pNode0, pNode1, v );
    Cudd2_SetArg( pNode, pResult );
}

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.

{
    Aig_Obj_t * pNode0, * pNode1, * pNode;
    pNode0 = Cudd2_GetArg( pArg0 );
    pNode1 = Cudd2_GetArg( pArg1 );
    pNode  = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
    Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
}

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.

{
    Aig_Obj_t * pNode0, * pNode1, * pNode2, * pNode;
    pNode0 = Cudd2_GetArg( pArg0 );
    pNode1 = Cudd2_GetArg( pArg1 );
    pNode2 = Cudd2_GetArg( pArg2 );
    pNode  = Aig_Mux( s_pCuddMan->pAig, pNode0, pNode1, pNode2 );
    Cudd2_SetArg( pNode, pResult );
}

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.

{
    int v;
    assert( s_pCuddMan != NULL );
    for ( v = Aig_ManPiNum(s_pCuddMan->pAig); v <= iVar; v++ )
        Aig_ObjCreatePi( s_pCuddMan->pAig );
    Cudd2_SetArg( Aig_ManPi(s_pCuddMan->pAig, iVar), pResult );
}

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.

{
    Aig_Obj_t * pNode0, * pNode1, * pNode;
    pNode0 = Cudd2_GetArg( pArg0 );
    pNode1 = Cudd2_GetArg( pArg1 );
    pNode  = Aig_And( s_pCuddMan->pAig, pNode0, Aig_Not(pNode1) );
    Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
}

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.

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

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.

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

void Cudd2_bddOne	(	void *	pCudd,
		void *	pResult
	)

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

Synopsis [Registers constant 1 node.]

Description []

SideEffects []

SeeAlso []

Definition at line 144 of file cudd2.c.

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

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.

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

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.

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

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.

{
    Aig_Obj_t * pNode0, * pNode1, * pNode;
    pNode0 = Cudd2_GetArg( pArg0 );
    pNode1 = Cudd2_GetArg( pArg1 );
    pNode  = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
    Cudd2_SetArg( pNode, pResult );
}

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

{
    Aig_Obj_t * pNode;
    assert( s_pCuddMan != NULL );
    if ( ! st__lookup( s_pCuddMan->pTable, (char *)Aig_Regular(pArg), (char **)&pNode ) )
    {
        printf( "Cudd2_GetArg(): An argument BDD is not in the hash table.\n" );
        return NULL;
    }
    return Aig_NotCond( pNode, Aig_IsComplement(pArg) );
}

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

FUNCTION DEFINITIONS ///.

INCLUDES ///.

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

Synopsis [Start AIG recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 56 of file cudd2.c.

{
    int v;
    // start the BDD-to-AIG manager when the first BDD manager is allocated
    if ( s_pCuddMan != NULL )
        return;
    s_pCuddMan = ALLOC( Aig_CuddMan_t, 1 );
    s_pCuddMan->pAig = Aig_ManStart();
    s_pCuddMan->pTable = st__init_table( st__ptrcmp, st__ptrhash );
    for ( v = 0; v < (int)numVars; v++ )
        Aig_ObjCreatePi( s_pCuddMan->pAig );
}

void Cudd2_Quit

(

void *

pCudd

)

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

Synopsis [Stops AIG recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file cudd2.c.

{
    assert( s_pCuddMan != NULL );
    Aig_ManDumpBlif( s_pCuddMan->pAig, "aig_temp.blif", NULL, NULL );
    Aig_ManStop( s_pCuddMan->pAig );
    st__free_table( s_pCuddMan->pTable );
    free( s_pCuddMan );
    s_pCuddMan = NULL;
}

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

{
    assert( s_pCuddMan != NULL );
    if ( st__is_member( s_pCuddMan->pTable, (char *)Aig_Regular(pResult) ) )
        return;
    pNode = Aig_NotCond( pNode,  Aig_IsComplement(pResult) );
    st__insert( s_pCuddMan->pTable, (char *)Aig_Regular(pResult), (char *)pNode );
}

Variable Documentation

Aig_CuddMan_t* s_pCuddMan = NULL

static

Definition at line 39 of file cudd2.c.