From 6ad22b4d3b0446652919d95b15fefb374bddfac0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 22 Nov 2006 08:01:00 -0800 Subject: Version abc61122 --- src/aig/hop/cudd2.c | 355 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 355 insertions(+) create mode 100644 src/aig/hop/cudd2.c (limited to 'src/aig/hop/cudd2.c') diff --git a/src/aig/hop/cudd2.c b/src/aig/hop/cudd2.c new file mode 100644 index 00000000..28d13ce0 --- /dev/null +++ b/src/aig/hop/cudd2.c @@ -0,0 +1,355 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3