Version abc71001

1 files changed, 404 insertions, 0 deletions

diff --git a/src/aig/ivy/ivyBalance.c b/src/aig/ivy/ivyBalance.c
new file mode 100644
index 00000000..5627039a
--- /dev/null
+++ b/src/aig/ivy/ivyBalance.c
@@ -0,0 +1,404 @@
+/**CFile****************************************************************
+
+  FileName    [ivyBalance.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Algebraic AIG balancing.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int         Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel );
+static Vec_Ptr_t * Ivy_NodeBalanceCone( Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level );
+static int         Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper );
+static void        Ivy_NodeBalancePermute( Ivy_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor );
+static void        Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Ivy_Obj_t * pObj );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs algebraic balancing of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
+{
+    Ivy_Man_t * pNew;
+    Ivy_Obj_t * pObj, * pDriver;
+    Vec_Vec_t * vStore;
+    int i, NewNodeId;
+    // clean the old manager
+    Ivy_ManCleanTravId( p );
+    // create the new manager 
+    pNew = Ivy_ManStart();
+    // map the nodes
+    Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) );
+    Ivy_ManForEachPi( p, pObj, i )
+        pObj->TravId = Ivy_EdgeFromNode( Ivy_ObjCreatePi(pNew) );
+    // if HAIG is defined, trasfer the pointers to the PIs/latches
+//    if ( p->pHaig )
+//        Ivy_ManHaigTrasfer( p, pNew );
+    // balance the AIG
+    vStore = Vec_VecAlloc( 50 );
+    Ivy_ManForEachPo( p, pObj, i )
+    {
+        pDriver   = Ivy_ObjReal( Ivy_ObjChild0(pObj) );
+        NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(pDriver), vStore, 0, fUpdateLevel );
+        NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(pDriver) );
+        Ivy_ObjCreatePo( pNew, Ivy_EdgeToNode(pNew, NewNodeId) );
+    }
+    Vec_VecFree( vStore );
+    if ( i = Ivy_ManCleanup( pNew ) )
+    {
+//        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
+    }
+    // check the resulting AIG
+    if ( !Ivy_ManCheck(pNew) )
+        printf( "Ivy_ManBalance(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeCompareLevelsDecrease( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
+{
+    int Diff = Ivy_Regular(*pp1)->Level - Ivy_Regular(*pp2)->Level;
+    if ( Diff > 0 )
+        return -1;
+    if ( Diff < 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the ID of new node constructed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
+{
+    Ivy_Obj_t * pObjNew;
+    Vec_Ptr_t * vSuper;
+    int i, NewNodeId;
+    assert( !Ivy_IsComplement(pObjOld) );
+    assert( !Ivy_ObjIsBuf(pObjOld) );
+    // return if the result is known
+    if ( Ivy_ObjIsConst1(pObjOld) )
+        return pObjOld->TravId;
+    if ( pObjOld->TravId )
+        return pObjOld->TravId;
+    assert( Ivy_ObjIsNode(pObjOld) );
+    // get the implication supergate
+    vSuper = Ivy_NodeBalanceCone( pObjOld, vStore, Level );
+    if ( vSuper->nSize == 0 )
+    { // it means that the supergate contains two nodes in the opposite polarity
+        pObjOld->TravId = Ivy_EdgeFromNode( Ivy_ManConst0(pNew) );
+        return pObjOld->TravId;
+    }
+    if ( vSuper->nSize < 2 )
+        printf( "BUG!\n" );
+    // for each old node, derive the new well-balanced node
+    for ( i = 0; i < vSuper->nSize; i++ )
+    {
+        NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
+        NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(vSuper->pArray[i]) );
+        vSuper->pArray[i] = Ivy_EdgeToNode( pNew, NewNodeId );
+    }
+    // build the supergate
+    pObjNew = Ivy_NodeBalanceBuildSuper( pNew, vSuper, Ivy_ObjType(pObjOld), fUpdateLevel );
+    vSuper->nSize = 0;
+    // make sure the balanced node is not assigned
+    assert( pObjOld->TravId == 0 );
+    pObjOld->TravId = Ivy_EdgeFromNode( pObjNew );
+//    assert( pObjOld->Level >= Ivy_Regular(pObjNew)->Level );
+    return pObjOld->TravId;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Builds implication supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Ivy_Man_t * p, Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel )
+{
+    Ivy_Obj_t * pObj1, * pObj2;
+    int LeftBound;
+    assert( vSuper->nSize > 1 );
+    // sort the new nodes by level in the decreasing order
+    Vec_PtrSort( vSuper, Ivy_NodeCompareLevelsDecrease );
+    // balance the nodes
+    while ( vSuper->nSize > 1 )
+    {
+        // find the left bound on the node to be paired
+        LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vSuper );
+        // find the node that can be shared (if no such node, randomize choice)
+        Ivy_NodeBalancePermute( p, vSuper, LeftBound, Type == IVY_EXOR );
+        // pull out the last two nodes
+        pObj1 = Vec_PtrPop(vSuper);
+        pObj2 = Vec_PtrPop(vSuper);
+        Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(p, pObj1, pObj2, Type) );
+    }
+    return Vec_PtrEntry(vSuper, 0);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes of the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeBalanceCone_rec( Ivy_Obj_t * pRoot, Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper )
+{
+    int RetValue1, RetValue2, i;
+    // check if the node is visited
+    if ( Ivy_Regular(pObj)->fMarkB )
+    {
+        // check if the node occurs in the same polarity
+        for ( i = 0; i < vSuper->nSize; i++ )
+            if ( vSuper->pArray[i] == pObj )
+                return 1;
+        // check if the node is present in the opposite polarity
+        for ( i = 0; i < vSuper->nSize; i++ )
+            if ( vSuper->pArray[i] == Ivy_Not(pObj) )
+                return -1;
+        assert( 0 );
+        return 0;
+    }
+    // if the new node is complemented or a PI, another gate begins
+    if ( pObj != pRoot && (Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Ivy_ObjType(pRoot) || Ivy_ObjRefs(pObj) > 1) )
+    {
+        Vec_PtrPush( vSuper, pObj );
+        Ivy_Regular(pObj)->fMarkB = 1;
+        return 0;
+    }
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjIsNode(pObj) );
+    // go through the branches
+    RetValue1 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_ObjChild0(pObj) ), vSuper );
+    RetValue2 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_ObjChild1(pObj) ), vSuper );
+    if ( RetValue1 == -1 || RetValue2 == -1 )
+        return -1;
+    // return 1 if at least one branch has a duplicate
+    return RetValue1 || RetValue2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes of the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ivy_NodeBalanceCone( Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
+{
+    Vec_Ptr_t * vNodes;
+    int RetValue, i;
+    assert( !Ivy_IsComplement(pObj) );
+    // extend the storage
+    if ( Vec_VecSize( vStore ) <= Level )
+        Vec_VecPush( vStore, Level, 0 );
+    // get the temporary array of nodes
+    vNodes = Vec_VecEntry( vStore, Level );
+    Vec_PtrClear( vNodes );
+    // collect the nodes in the implication supergate
+    RetValue = Ivy_NodeBalanceCone_rec( pObj, pObj, vNodes );
+    assert( vNodes->nSize > 1 );
+    // unmark the visited nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Ivy_Regular(pObj)->fMarkB = 0;
+    // if we found the node and its complement in the same implication supergate, 
+    // return empty set of nodes (meaning that we should use constant-0 node)
+    if ( RetValue == -1 )
+        vNodes->nSize = 0;
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the left bound on the next candidate to be paired.]
+
+  Description [The nodes in the array are in the decreasing order of levels. 
+  The last node in the array has the smallest level. By default it would be paired 
+  with the next node on the left. However, it may be possible to pair it with some
+  other node on the left, in such a way that the new node is shared. This procedure
+  finds the index of the left-most node, which can be paired with the last node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper )
+{
+    Ivy_Obj_t * pObjRight, * pObjLeft;
+    int Current;
+    // if two or less nodes, pair with the first
+    if ( Vec_PtrSize(vSuper) < 3 )
+        return 0;
+    // set the pointer to the one before the last
+    Current = Vec_PtrSize(vSuper) - 2;
+    pObjRight = Vec_PtrEntry( vSuper, Current );
+    // go through the nodes to the left of this one
+    for ( Current--; Current >= 0; Current-- )
+    {
+        // get the next node on the left
+        pObjLeft = Vec_PtrEntry( vSuper, Current );
+        // if the level of this node is different, quit the loop
+        if ( Ivy_Regular(pObjLeft)->Level != Ivy_Regular(pObjRight)->Level )
+            break;
+    }
+    Current++;    
+    // get the node, for which the equality holds
+    pObjLeft = Vec_PtrEntry( vSuper, Current );
+    assert( Ivy_Regular(pObjLeft)->Level == Ivy_Regular(pObjRight)->Level );
+    return Current;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Moves closer to the end the node that is best for sharing.]
+
+  Description [If there is no node with sharing, randomly chooses one of 
+  the legal nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeBalancePermute( Ivy_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
+{
+    Ivy_Obj_t * pObj1, * pObj2, * pObj3, * pGhost;
+    int RightBound, i;
+    // get the right bound
+    RightBound = Vec_PtrSize(vSuper) - 2;
+    assert( LeftBound <= RightBound );
+    if ( LeftBound == RightBound )
+        return;
+    // get the two last nodes
+    pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 );
+    pObj2 = Vec_PtrEntry( vSuper, RightBound     );
+    if ( Ivy_Regular(pObj1) == p->pConst1 || Ivy_Regular(pObj2) == p->pConst1 )
+        return;
+    // find the first node that can be shared
+    for ( i = RightBound; i >= LeftBound; i-- )
+    {
+        pObj3 = Vec_PtrEntry( vSuper, i );
+        if ( Ivy_Regular(pObj3) == p->pConst1 )
+        {
+            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
+            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
+            return;
+        }
+        pGhost = Ivy_ObjCreateGhost( p, pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE );
+        if ( Ivy_TableLookup( p, pGhost ) )
+        {
+            if ( pObj3 == pObj2 )
+                return;
+            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
+            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
+            return;
+        }
+    }
+/*
+    // we did not find the node to share, randomize choice
+    {
+        int Choice = rand() % (RightBound - LeftBound + 1);
+        pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
+        if ( pObj3 == pObj2 )
+            return;
+        Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 );
+        Vec_PtrWriteEntry( vSuper, RightBound,         pObj3 );
+    }
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts a new node in the order by levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Ivy_Obj_t * pObj )
+{
+    Ivy_Obj_t * pObj1, * pObj2;
+    int i;
+    if ( Vec_PtrPushUnique(vStore, pObj) )
+        return;
+    // find the p of the node
+    for ( i = vStore->nSize-1; i > 0; i-- )
+    {
+        pObj1 = vStore->pArray[i  ];
+        pObj2 = vStore->pArray[i-1];
+        if ( Ivy_Regular(pObj1)->Level <= Ivy_Regular(pObj2)->Level )
+            break;
+        vStore->pArray[i  ] = pObj2;
+        vStore->pArray[i-1] = pObj1;
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+