Version abc80130_2

1 files changed, 355 insertions, 0 deletions

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                                ///
+////////////////////////////////////////////////////////////////////////
+
+