summaryrefslogtreecommitdiffstats
path: root/src/aig/hop/hopBalance.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/hop/hopBalance.c')
-rw-r--r--src/aig/hop/hopBalance.c391
1 files changed, 391 insertions, 0 deletions
diff --git a/src/aig/hop/hopBalance.c b/src/aig/hop/hopBalance.c
new file mode 100644
index 00000000..73c90685
--- /dev/null
+++ b/src/aig/hop/hopBalance.c
@@ -0,0 +1,391 @@
+/**CFile****************************************************************
+
+ FileName [hopBalance.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Minimalistic And-Inverter Graph package.]
+
+ Synopsis [Algebraic AIG balancing.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - May 11, 2006.]
+
+ Revision [$Id: hopBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "hop.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static Hop_Obj_t * Hop_NodeBalance_rec( Hop_Man_t * pNew, Hop_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel );
+static Vec_Ptr_t * Hop_NodeBalanceCone( Hop_Obj_t * pObj, Vec_Vec_t * vStore, int Level );
+static int Hop_NodeBalanceFindLeft( Vec_Ptr_t * vSuper );
+static void Hop_NodeBalancePermute( Hop_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor );
+static void Hop_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Hop_Obj_t * pObj );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs algebraic balancing of the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Hop_Man_t * Hop_ManBalance( Hop_Man_t * p, int fUpdateLevel )
+{
+ Hop_Man_t * pNew;
+ Hop_Obj_t * pObj, * pObjNew;
+ Vec_Vec_t * vStore;
+ int i;
+ // create the new manager
+ pNew = Hop_ManStart();
+ pNew->fRefCount = 0;
+ // map the PI nodes
+ Hop_ManCleanData( p );
+ Hop_ManConst1(p)->pData = Hop_ManConst1(pNew);
+ Hop_ManForEachPi( p, pObj, i )
+ pObj->pData = Hop_ObjCreatePi(pNew);
+ // balance the AIG
+ vStore = Vec_VecAlloc( 50 );
+ Hop_ManForEachPo( p, pObj, i )
+ {
+ pObjNew = Hop_NodeBalance_rec( pNew, Hop_ObjFanin0(pObj), vStore, 0, fUpdateLevel );
+ Hop_ObjCreatePo( pNew, Hop_NotCond( pObjNew, Hop_ObjFaninC0(pObj) ) );
+ }
+ Vec_VecFree( vStore );
+ // remove dangling nodes
+// Hop_ManCreateRefs( pNew );
+// if ( i = Hop_ManCleanup( pNew ) )
+// printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
+ // check the resulting AIG
+ if ( !Hop_ManCheck(pNew) )
+ printf( "Hop_ManBalance(): The check has failed.\n" );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the new node constructed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Hop_Obj_t * Hop_NodeBalance_rec( Hop_Man_t * pNew, Hop_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
+{
+ Hop_Obj_t * pObjNew;
+ Vec_Ptr_t * vSuper;
+ int i;
+ assert( !Hop_IsComplement(pObjOld) );
+ // return if the result is known
+ if ( pObjOld->pData )
+ return pObjOld->pData;
+ assert( Hop_ObjIsNode(pObjOld) );
+ // get the implication supergate
+ vSuper = Hop_NodeBalanceCone( pObjOld, vStore, Level );
+ // check if supergate contains two nodes in the opposite polarity
+ if ( vSuper->nSize == 0 )
+ return pObjOld->pData = Hop_ManConst0(pNew);
+ if ( Vec_PtrSize(vSuper) < 2 )
+ printf( "BUG!\n" );
+ // for each old node, derive the new well-balanced node
+ for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
+ {
+ pObjNew = Hop_NodeBalance_rec( pNew, Hop_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
+ vSuper->pArray[i] = Hop_NotCond( pObjNew, Hop_IsComplement(vSuper->pArray[i]) );
+ }
+ // build the supergate
+ pObjNew = Hop_NodeBalanceBuildSuper( pNew, vSuper, Hop_ObjType(pObjOld), fUpdateLevel );
+ // make sure the balanced node is not assigned
+// assert( pObjOld->Level >= Hop_Regular(pObjNew)->Level );
+ assert( pObjOld->pData == NULL );
+ return pObjOld->pData = pObjNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the nodes of the supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Hop_NodeBalanceCone_rec( Hop_Obj_t * pRoot, Hop_Obj_t * pObj, Vec_Ptr_t * vSuper )
+{
+ int RetValue1, RetValue2, i;
+ // check if the node is visited
+ if ( Hop_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] == Hop_Not(pObj) )
+ return -1;
+ assert( 0 );
+ return 0;
+ }
+ // if the new node is complemented or a PI, another gate begins
+ if ( pObj != pRoot && (Hop_IsComplement(pObj) || Hop_ObjType(pObj) != Hop_ObjType(pRoot) || Hop_ObjRefs(pObj) > 1) )
+ {
+ Vec_PtrPush( vSuper, pObj );
+ Hop_Regular(pObj)->fMarkB = 1;
+ return 0;
+ }
+ assert( !Hop_IsComplement(pObj) );
+ assert( Hop_ObjIsNode(pObj) );
+ // go through the branches
+ RetValue1 = Hop_NodeBalanceCone_rec( pRoot, Hop_ObjChild0(pObj), vSuper );
+ RetValue2 = Hop_NodeBalanceCone_rec( pRoot, Hop_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 * Hop_NodeBalanceCone( Hop_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
+{
+ Vec_Ptr_t * vNodes;
+ int RetValue, i;
+ assert( !Hop_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 = Hop_NodeBalanceCone_rec( pObj, pObj, vNodes );
+ assert( vNodes->nSize > 1 );
+ // unmark the visited nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ Hop_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 [Procedure used for sorting the nodes in decreasing order of levels.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Hop_NodeCompareLevelsDecrease( Hop_Obj_t ** pp1, Hop_Obj_t ** pp2 )
+{
+ int Diff = Hop_ObjLevel(Hop_Regular(*pp1)) - Hop_ObjLevel(Hop_Regular(*pp2));
+ if ( Diff > 0 )
+ return -1;
+ if ( Diff < 0 )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Builds implication supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Hop_Obj_t * Hop_NodeBalanceBuildSuper( Hop_Man_t * p, Vec_Ptr_t * vSuper, Hop_Type_t Type, int fUpdateLevel )
+{
+ Hop_Obj_t * pObj1, * pObj2;
+ int LeftBound;
+ assert( vSuper->nSize > 1 );
+ // sort the new nodes by level in the decreasing order
+ Vec_PtrSort( vSuper, Hop_NodeCompareLevelsDecrease );
+ // balance the nodes
+ while ( vSuper->nSize > 1 )
+ {
+ // find the left bound on the node to be paired
+ LeftBound = (!fUpdateLevel)? 0 : Hop_NodeBalanceFindLeft( vSuper );
+ // find the node that can be shared (if no such node, randomize choice)
+ Hop_NodeBalancePermute( p, vSuper, LeftBound, Type == AIG_EXOR );
+ // pull out the last two nodes
+ pObj1 = Vec_PtrPop(vSuper);
+ pObj2 = Vec_PtrPop(vSuper);
+ Hop_NodeBalancePushUniqueOrderByLevel( vSuper, Hop_Oper(p, pObj1, pObj2, Type) );
+ }
+ return Vec_PtrEntry(vSuper, 0);
+}
+
+/**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 Hop_NodeBalanceFindLeft( Vec_Ptr_t * vSuper )
+{
+ Hop_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 ( Hop_ObjLevel(Hop_Regular(pObjLeft)) != Hop_ObjLevel(Hop_Regular(pObjRight)) )
+ break;
+ }
+ Current++;
+ // get the node, for which the equality holds
+ pObjLeft = Vec_PtrEntry( vSuper, Current );
+ assert( Hop_ObjLevel(Hop_Regular(pObjLeft)) == Hop_ObjLevel(Hop_Regular(pObjRight)) );
+ 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 Hop_NodeBalancePermute( Hop_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
+{
+ Hop_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 ( Hop_Regular(pObj1) == p->pConst1 || Hop_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 ( Hop_Regular(pObj3) == p->pConst1 )
+ {
+ Vec_PtrWriteEntry( vSuper, i, pObj2 );
+ Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
+ return;
+ }
+ pGhost = Hop_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_EXOR : AIG_AND );
+ if ( Hop_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 Hop_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Hop_Obj_t * pObj )
+{
+ Hop_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 ( Hop_ObjLevel(Hop_Regular(pObj1)) <= Hop_ObjLevel(Hop_Regular(pObj2)) )
+ break;
+ vStore->pArray[i ] = pObj2;
+ vStore->pArray[i-1] = pObj1;
+ }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+