mirror of https://github.com/YosysHQ/abc.git
716 lines
23 KiB
C
716 lines
23 KiB
C
/**CFile****************************************************************
|
|
|
|
FileName [darBalance.c]
|
|
|
|
SystemName [ABC: Logic synthesis and verification system.]
|
|
|
|
PackageName [DAG-aware AIG rewriting.]
|
|
|
|
Synopsis [Algebraic AIG balancing.]
|
|
|
|
Author [Alan Mishchenko]
|
|
|
|
Affiliation [UC Berkeley]
|
|
|
|
Date [Ver. 1.0. Started - April 28, 2007.]
|
|
|
|
Revision [$Id: darBalance.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
|
|
|
|
***********************************************************************/
|
|
|
|
#include "darInt.h"
|
|
#include "misc/tim/tim.h"
|
|
|
|
ABC_NAMESPACE_IMPL_START
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
//#define USE_LUTSIZE_BALANCE
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DEFINITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Uniqifies the node.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Dar_ObjCompareLits( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
|
|
{
|
|
int Diff = Aig_ObjToLit(*pp1) - Aig_ObjToLit(*pp2);
|
|
if ( Diff < 0 )
|
|
return -1;
|
|
if ( Diff > 0 )
|
|
return 1;
|
|
return 0;
|
|
}
|
|
void Dar_BalanceUniqify( Aig_Obj_t * pObj, Vec_Ptr_t * vNodes, int fExor )
|
|
{
|
|
Aig_Obj_t * pTemp, * pTempNext;
|
|
int i, k;
|
|
// sort the nodes by their literal
|
|
Vec_PtrSort( vNodes, (int (*)())Dar_ObjCompareLits );
|
|
// remove duplicates
|
|
k = 0;
|
|
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, i )
|
|
{
|
|
if ( i + 1 == Vec_PtrSize(vNodes) )
|
|
{
|
|
Vec_PtrWriteEntry( vNodes, k++, pTemp );
|
|
break;
|
|
}
|
|
pTempNext = (Aig_Obj_t *)Vec_PtrEntry( vNodes, i+1 );
|
|
if ( !fExor && pTemp == Aig_Not(pTempNext) ) // pos_lit & neg_lit = 0
|
|
{
|
|
Vec_PtrClear( vNodes );
|
|
return;
|
|
}
|
|
if ( pTemp != pTempNext ) // save if different
|
|
Vec_PtrWriteEntry( vNodes, k++, pTemp );
|
|
else if ( fExor ) // in case of XOR, remove identical
|
|
i++;
|
|
}
|
|
Vec_PtrShrink( vNodes, k );
|
|
// check that there is no duplicates
|
|
pTemp = (Aig_Obj_t *)Vec_PtrEntry( vNodes, 0 );
|
|
Vec_PtrForEachEntryStart( Aig_Obj_t *, vNodes, pTempNext, i, 1 )
|
|
{
|
|
assert( pTemp != pTempNext );
|
|
pTemp = pTempNext;
|
|
}
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Collects the nodes of the supergate.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
|
|
{
|
|
if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1 || Vec_PtrSize(vSuper) > 10000) )
|
|
Vec_PtrPush( vSuper, pObj );
|
|
else
|
|
{
|
|
assert( !Aig_IsComplement(pObj) );
|
|
assert( Aig_ObjIsNode(pObj) );
|
|
// go through the branches
|
|
Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
|
|
Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
|
|
}
|
|
}
|
|
Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
|
|
{
|
|
Vec_Ptr_t * vNodes;
|
|
assert( !Aig_IsComplement(pObj) );
|
|
assert( Aig_ObjIsNode(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
|
|
Dar_BalanceCone_rec( pObj, pObj, vNodes );
|
|
// remove duplicates
|
|
Dar_BalanceUniqify( pObj, vNodes, Aig_ObjIsExor(pObj) );
|
|
return vNodes;
|
|
}
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Collects the nodes of the supergate.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
/*
|
|
int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
|
|
{
|
|
int RetValue1, RetValue2, i;
|
|
// check if the node is visited
|
|
if ( Aig_Regular(pObj)->fMarkB )
|
|
{
|
|
if ( Aig_ObjIsExor(pRoot) )
|
|
{
|
|
assert( !Aig_IsComplement(pObj) );
|
|
// check if the node occurs in the same polarity
|
|
Vec_PtrRemove( vSuper, pObj );
|
|
Aig_Regular(pObj)->fMarkB = 0;
|
|
//printf( " Duplicated EXOR input!!! " );
|
|
return 1;
|
|
}
|
|
else
|
|
{
|
|
// 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] == Aig_Not(pObj) )
|
|
return -1;
|
|
}
|
|
assert( 0 );
|
|
return 0;
|
|
}
|
|
// if the new node is complemented or a PI, another gate begins
|
|
if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1 || Vec_PtrSize(vSuper) > 10000) )
|
|
{
|
|
Vec_PtrPush( vSuper, pObj );
|
|
Aig_Regular(pObj)->fMarkB = 1;
|
|
return 0;
|
|
}
|
|
assert( !Aig_IsComplement(pObj) );
|
|
assert( Aig_ObjIsNode(pObj) );
|
|
// go through the branches
|
|
RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
|
|
RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
|
|
if ( RetValue1 == -1 || RetValue2 == -1 )
|
|
return -1;
|
|
// return 1 if at least one branch has a duplicate
|
|
return RetValue1 || RetValue2;
|
|
}
|
|
Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
|
|
{
|
|
Vec_Ptr_t * vNodes;
|
|
int RetValue, i;
|
|
assert( !Aig_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 = Dar_BalanceCone_rec( pObj, pObj, vNodes );
|
|
assert( RetValue != 0 || vNodes->nSize > 1 );
|
|
// unmark the visited nodes
|
|
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
|
|
Aig_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 Dar_BalanceFindLeft( Vec_Ptr_t * vSuper )
|
|
{
|
|
Aig_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 = (Aig_Obj_t *)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 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
|
|
// if the level of this node is different, quit the loop
|
|
if ( Aig_ObjLevel(Aig_Regular(pObjLeft)) != Aig_ObjLevel(Aig_Regular(pObjRight)) )
|
|
break;
|
|
}
|
|
Current++;
|
|
// get the node, for which the equality holds
|
|
pObjLeft = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
|
|
assert( Aig_ObjLevel(Aig_Regular(pObjLeft)) == Aig_ObjLevel(Aig_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 Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
|
|
{
|
|
Aig_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 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, RightBound + 1 );
|
|
pObj2 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, RightBound );
|
|
if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 || Aig_Regular(pObj1) == Aig_Regular(pObj2) )
|
|
return;
|
|
// find the first node that can be shared
|
|
for ( i = RightBound; i >= LeftBound; i-- )
|
|
{
|
|
pObj3 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, i );
|
|
if ( Aig_Regular(pObj3) == p->pConst1 )
|
|
{
|
|
Vec_PtrWriteEntry( vSuper, i, pObj2 );
|
|
Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
|
|
return;
|
|
}
|
|
if ( Aig_Regular(pObj1) == Aig_Regular(pObj3) )
|
|
{
|
|
if ( pObj3 == pObj2 )
|
|
return;
|
|
Vec_PtrWriteEntry( vSuper, i, pObj2 );
|
|
Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
|
|
return;
|
|
}
|
|
pGhost = Aig_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_OBJ_EXOR : AIG_OBJ_AND );
|
|
if ( Aig_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 = Aig_ManRandom(0) % (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 [Procedure used for sorting the nodes in decreasing order of levels.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
|
|
{
|
|
int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2));
|
|
if ( Diff > 0 )
|
|
return -1;
|
|
if ( Diff < 0 )
|
|
return 1;
|
|
Diff = Aig_ObjId(Aig_Regular(*pp1)) - Aig_ObjId(Aig_Regular(*pp2));
|
|
if ( Diff > 0 )
|
|
return -1;
|
|
if ( Diff < 0 )
|
|
return 1;
|
|
return 0;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Inserts a new node in the order by levels.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj, int fExor )
|
|
{
|
|
Aig_Obj_t * pObj1, * pObj2;
|
|
int i;
|
|
if ( Vec_PtrPushUnique(vStore, pObj) )
|
|
{
|
|
if ( fExor )
|
|
Vec_PtrRemove(vStore, pObj);
|
|
return;
|
|
}
|
|
// find the p of the node
|
|
for ( i = vStore->nSize-1; i > 0; i-- )
|
|
{
|
|
pObj1 = (Aig_Obj_t *)vStore->pArray[i ];
|
|
pObj2 = (Aig_Obj_t *)vStore->pArray[i-1];
|
|
if ( Aig_ObjLevel(Aig_Regular(pObj1)) <= Aig_ObjLevel(Aig_Regular(pObj2)) )
|
|
break;
|
|
vStore->pArray[i ] = pObj2;
|
|
vStore->pArray[i-1] = pObj1;
|
|
}
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Builds implication supergate.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel )
|
|
{
|
|
Aig_Obj_t * pObj1, * pObj2;
|
|
int LeftBound;
|
|
assert( vSuper->nSize > 1 );
|
|
// sort the new nodes by level in the decreasing order
|
|
Vec_PtrSort( vSuper, (int (*)(void))Aig_NodeCompareLevelsDecrease );
|
|
// balance the nodes
|
|
while ( vSuper->nSize > 1 )
|
|
{
|
|
// find the left bound on the node to be paired
|
|
LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper );
|
|
// find the node that can be shared (if no such node, randomize choice)
|
|
Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR );
|
|
// pull out the last two nodes
|
|
pObj1 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
|
|
pObj2 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
|
|
Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type), Type == AIG_OBJ_EXOR );
|
|
}
|
|
return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
|
|
}
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Returns affective support size.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Aig_BaseSize( Aig_Man_t * p, Aig_Obj_t * pObj, int nLutSize )
|
|
{
|
|
int nBaseSize;
|
|
pObj = Aig_Regular(pObj);
|
|
if ( Aig_ObjIsConst1(pObj) )
|
|
return 0;
|
|
if ( Aig_ObjLevel(pObj) >= nLutSize )
|
|
return 1;
|
|
nBaseSize = Aig_SupportSize( p, pObj );
|
|
if ( nBaseSize >= nLutSize )
|
|
return 1;
|
|
return nBaseSize;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Builds implication supergate.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Aig_Obj_t * Dar_BalanceBuildSuperTop( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel, int nLutSize )
|
|
{
|
|
Vec_Ptr_t * vSubset;
|
|
Aig_Obj_t * pObj;
|
|
int i, nBaseSizeAll, nBaseSize;
|
|
assert( vSuper->nSize > 1 );
|
|
// sort the new nodes by level in the decreasing order
|
|
Vec_PtrSort( vSuper, (int (*)(void))Aig_NodeCompareLevelsDecrease );
|
|
// add one LUT at a time
|
|
while ( Vec_PtrSize(vSuper) > 1 )
|
|
{
|
|
// isolate the group of nodes with nLutSize inputs
|
|
nBaseSizeAll = 0;
|
|
vSubset = Vec_PtrAlloc( nLutSize );
|
|
Vec_PtrForEachEntryReverse( Aig_Obj_t *, vSuper, pObj, i )
|
|
{
|
|
nBaseSize = Aig_BaseSize( p, pObj, nLutSize );
|
|
if ( nBaseSizeAll + nBaseSize > nLutSize && Vec_PtrSize(vSubset) > 1 )
|
|
break;
|
|
nBaseSizeAll += nBaseSize;
|
|
Vec_PtrPush( vSubset, pObj );
|
|
}
|
|
// remove them from vSuper
|
|
Vec_PtrShrink( vSuper, Vec_PtrSize(vSuper) - Vec_PtrSize(vSubset) );
|
|
// create the new supergate
|
|
pObj = Dar_BalanceBuildSuper( p, vSubset, Type, fUpdateLevel );
|
|
Vec_PtrFree( vSubset );
|
|
// add the new output
|
|
Dar_BalancePushUniqueOrderByLevel( vSuper, pObj, Type == AIG_OBJ_EXOR );
|
|
}
|
|
return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Returns the new node constructed.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
|
|
{
|
|
Aig_Obj_t * pObjNew;
|
|
Vec_Ptr_t * vSuper;
|
|
int i;
|
|
assert( !Aig_IsComplement(pObjOld) );
|
|
assert( !Aig_ObjIsBuf(pObjOld) );
|
|
// return if the result is known
|
|
if ( pObjOld->pData )
|
|
return (Aig_Obj_t *)pObjOld->pData;
|
|
assert( Aig_ObjIsNode(pObjOld) );
|
|
// get the implication supergate
|
|
vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
|
|
// check if supergate contains two nodes in the opposite polarity
|
|
if ( vSuper->nSize == 0 )
|
|
return (Aig_Obj_t *)(pObjOld->pData = Aig_ManConst0(pNew));
|
|
if ( vSuper->nSize == 1 )
|
|
return (Aig_Obj_t *)((Aig_Obj_t *)Vec_PtrEntry(vSuper, 0))->pData;
|
|
if ( Vec_PtrSize(vSuper) < 2 )
|
|
printf( "Dar_Balance_rec: Internal error!\n" );
|
|
// for each old node, derive the new well-balanced node
|
|
for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
|
|
{
|
|
pObjNew = Dar_Balance_rec( pNew, Aig_Regular((Aig_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
|
|
vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement((Aig_Obj_t *)vSuper->pArray[i]) );
|
|
}
|
|
// build the supergate
|
|
#ifdef USE_LUTSIZE_BALANCE
|
|
pObjNew = Dar_BalanceBuildSuperTop( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel, 6 );
|
|
#else
|
|
pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
|
|
#endif
|
|
// make sure the balanced node is not assigned
|
|
// assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
|
|
assert( pObjOld->pData == NULL );
|
|
return (Aig_Obj_t *)(pObjOld->pData = pObjNew);
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Performs algebraic balancing of the AIG.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
|
|
{
|
|
Aig_Man_t * pNew;
|
|
Aig_Obj_t * pObj, * pDriver, * pObjNew;
|
|
Vec_Vec_t * vStore;
|
|
int i;
|
|
assert( Aig_ManVerifyTopoOrder(p) );
|
|
// create the new manager
|
|
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
|
|
pNew->pName = Abc_UtilStrsav( p->pName );
|
|
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
|
|
pNew->nAsserts = p->nAsserts;
|
|
pNew->nConstrs = p->nConstrs;
|
|
if ( p->vFlopNums )
|
|
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
|
|
// map the PI nodes
|
|
Aig_ManCleanData( p );
|
|
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
|
|
vStore = Vec_VecAlloc( 50 );
|
|
if ( p->pManTime != NULL )
|
|
{
|
|
float arrTime;
|
|
Tim_ManIncrementTravId( (Tim_Man_t *)p->pManTime );
|
|
Aig_ManSetCioIds( p );
|
|
Aig_ManForEachObj( p, pObj, i )
|
|
{
|
|
if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
|
|
continue;
|
|
if ( Aig_ObjIsCi(pObj) )
|
|
{
|
|
// copy the PI
|
|
pObjNew = Aig_ObjCreateCi(pNew);
|
|
pObj->pData = pObjNew;
|
|
// set the arrival time of the new PI
|
|
arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
|
|
pObjNew->Level = (int)arrTime;
|
|
}
|
|
else if ( Aig_ObjIsCo(pObj) )
|
|
{
|
|
// perform balancing
|
|
pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
|
|
pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
|
|
pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
|
|
// save arrival time of the output
|
|
arrTime = (float)Aig_Regular(pObjNew)->Level;
|
|
Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj), arrTime );
|
|
// create PO
|
|
pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
|
|
}
|
|
else
|
|
assert( 0 );
|
|
}
|
|
Aig_ManCleanCioIds( p );
|
|
pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
|
|
}
|
|
else
|
|
{
|
|
Aig_ManForEachCi( p, pObj, i )
|
|
{
|
|
pObjNew = Aig_ObjCreateCi(pNew);
|
|
pObjNew->Level = pObj->Level;
|
|
pObj->pData = pObjNew;
|
|
}
|
|
Aig_ManForEachCo( p, pObj, i )
|
|
{
|
|
pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
|
|
pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
|
|
pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
|
|
pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
|
|
}
|
|
}
|
|
Vec_VecFree( vStore );
|
|
// remove dangling nodes
|
|
Aig_ManCleanup( pNew );
|
|
Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
|
|
// check the resulting AIG
|
|
if ( !Aig_ManCheck(pNew) )
|
|
printf( "Dar_ManBalance(): The check has failed.\n" );
|
|
return pNew;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Reproduces script "compress2".]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose )
|
|
{
|
|
Aig_Man_t * pAigXor, * pRes;
|
|
if ( fExor )
|
|
{
|
|
pAigXor = Aig_ManDupExor( pAig );
|
|
if ( fVerbose )
|
|
Dar_BalancePrintStats( pAigXor );
|
|
pRes = Dar_ManBalance( pAigXor, fUpdateLevel );
|
|
Aig_ManStop( pAigXor );
|
|
}
|
|
else
|
|
{
|
|
pRes = Dar_ManBalance( pAig, fUpdateLevel );
|
|
}
|
|
return pRes;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Inserts a new node in the order by levels.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Dar_BalancePrintStats( Aig_Man_t * p )
|
|
{
|
|
Vec_Ptr_t * vSuper;
|
|
Aig_Obj_t * pObj, * pTemp;
|
|
int i, k;
|
|
if ( Aig_ManExorNum(p) == 0 )
|
|
{
|
|
printf( "There is no EXOR gates.\n" );
|
|
return;
|
|
}
|
|
Aig_ManForEachExor( p, pObj, i )
|
|
{
|
|
Aig_ObjFanin0(pObj)->fMarkA = 1;
|
|
Aig_ObjFanin1(pObj)->fMarkA = 1;
|
|
assert( !Aig_ObjFaninC0(pObj) );
|
|
assert( !Aig_ObjFaninC1(pObj) );
|
|
}
|
|
vSuper = Vec_PtrAlloc( 1000 );
|
|
Aig_ManForEachExor( p, pObj, i )
|
|
{
|
|
if ( pObj->fMarkA && pObj->nRefs == 1 )
|
|
continue;
|
|
Vec_PtrClear( vSuper );
|
|
Dar_BalanceCone_rec( pObj, pObj, vSuper );
|
|
Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
|
|
pTemp->fMarkB = 0;
|
|
if ( Vec_PtrSize(vSuper) < 3 )
|
|
continue;
|
|
printf( " %d(", Vec_PtrSize(vSuper) );
|
|
Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
|
|
printf( " %d", pTemp->Level );
|
|
printf( " )" );
|
|
}
|
|
Vec_PtrFree( vSuper );
|
|
Aig_ManForEachObj( p, pObj, i )
|
|
pObj->fMarkA = 0;
|
|
printf( "\n" );
|
|
}
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
ABC_NAMESPACE_IMPL_END
|
|
|