/**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 $]
***********************************************************************/
#include "hop.h"
#include "st.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Aig_CuddMan_t_ Aig_CuddMan_t;
struct Aig_CuddMan_t_
{
Aig_Man_t * pAig; // internal AIG package
st_table * pTable; // hash table mapping BDD nodes into AIG nodes
};
// static Cudd AIG manager used in this experiment
static Aig_CuddMan_t * s_pCuddMan = NULL;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Start AIG recording.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_Init( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd )
{
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 );
}
/**Function*************************************************************
Synopsis [Stops AIG recording.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_Quit( void * pCudd )
{
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;
}
/**Function*************************************************************
Synopsis [Fetches AIG node corresponding to the BDD node from the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Aig_Obj_t * Cudd2_GetArg( void * pArg )
{
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) );
}
/**Function*************************************************************
Synopsis [Inserts the AIG node corresponding to the BDD node into the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Cudd2_SetArg( Aig_Obj_t * pNode, void * pResult )
{
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 );
}
/**Function*************************************************************
Synopsis [Registers constant 1 node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddOne( void * pCudd, void * pResult )
{
Cudd2_SetArg( Aig_ManConst1(s_pCuddMan->pAig), pResult );
}
/**Function*************************************************************
Synopsis [Adds elementary variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddIthVar( void * pCudd, int iVar, void * pResult )
{
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 );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddAnd( void * pCudd, void * pArg0, void * pArg1, void * pResult )
{
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 );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddOr( void * pCudd, void * pArg0, void * pArg1, void * pResult )
{
Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), Aig_Not(pResult) );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddNand( void * pCudd, void * pArg0, void * pArg1, void * pResult )
{
Cudd2_bddAnd( pCudd, pArg0, pArg1, Aig_Not(pResult) );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddNor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
{
Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), pResult );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddXor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
{
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 );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddXnor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
{
Cudd2_bddXor( pCudd, pArg0, pArg1, Aig_Not(pResult) );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddIte( void * pCudd, void * pArg0, void * pArg1, void * pArg2, void * pResult )
{
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 );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddCompose( void * pCudd, void * pArg0, void * pArg1, int v, void * pResult )
{
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 );
}
/**Function*************************************************************
Synopsis [Should be called after each containment check.]
Description [Result should be 1 if Cudd2_bddLeq returned 1.]
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddLeq( void * pCudd, void * pArg0, void * pArg1, int Result )
{
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 );
}
/**Function*************************************************************
Synopsis [Should be called after each equality check.]
Description [Result should be 1 if they are equal.]
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddEqual( void * pCudd, void * pArg0, void * pArg1, int Result )
{
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 );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END