diff options
Diffstat (limited to 'src/aig/hop/cudd2.c')
-rw-r--r-- | src/aig/hop/cudd2.c | 355 |
1 files changed, 0 insertions, 355 deletions
diff --git a/src/aig/hop/cudd2.c b/src/aig/hop/cudd2.c deleted file mode 100644 index 28d13ce0..00000000 --- a/src/aig/hop/cudd2.c +++ /dev/null @@ -1,355 +0,0 @@ -/**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" - -//////////////////////////////////////////////////////////////////////// -/// 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" ); - 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 /// -//////////////////////////////////////////////////////////////////////// - - |