diff options
Diffstat (limited to 'abc70930/src/aig/ivy/ivyRwrAlg.c')
| -rw-r--r-- | abc70930/src/aig/ivy/ivyRwrAlg.c | 408 |
1 files changed, 408 insertions, 0 deletions
diff --git a/abc70930/src/aig/ivy/ivyRwrAlg.c b/abc70930/src/aig/ivy/ivyRwrAlg.c new file mode 100644 index 00000000..fc48deb0 --- /dev/null +++ b/abc70930/src/aig/ivy/ivyRwrAlg.c @@ -0,0 +1,408 @@ +/**CFile**************************************************************** + + FileName [ivyRwrAlg.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Algebraic AIG rewriting.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyRwrAlg.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone ); +static Ivy_Obj_t * Ivy_NodeRewriteAlg( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vSols, int LevelR, int fUseZeroCost ); +static int Ivy_NodeCountMffc( Ivy_Obj_t * pNode ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Algebraic AIG rewriting.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ) +{ + Vec_Int_t * vRequired; + Vec_Ptr_t * vFront, * vLeaves, * vCone, * vSol; + Ivy_Obj_t * pObj, * pResult; + int i, RetValue, LevelR, nNodesOld; + int CountUsed, CountUndo; + vRequired = fUpdateLevel? Ivy_ManRequiredLevels( p ) : NULL; + vFront = Vec_PtrAlloc( 100 ); + vLeaves = Vec_PtrAlloc( 100 ); + vCone = Vec_PtrAlloc( 100 ); + vSol = Vec_PtrAlloc( 100 ); + // go through the nodes in the topological order + CountUsed = CountUndo = 0; + nNodesOld = Ivy_ManObjIdNext(p); + Ivy_ManForEachObj( p, pObj, i ) + { + assert( !Ivy_ObjIsBuf(pObj) ); + if ( i >= nNodesOld ) + break; + // skip no-nodes and MUX roots + if ( !Ivy_ObjIsNode(pObj) || Ivy_ObjIsExor(pObj) || Ivy_ObjIsMuxType(pObj) ) + continue; +// if ( pObj->Id > 297 ) // 296 --- 297 +// break; + if ( pObj->Id == 297 ) + { + int x = 0; + } + // get the largest algebraic cut + RetValue = Ivy_ManFindAlgCut( pObj, vFront, vLeaves, vCone ); + // the case of a trivial tree cut + if ( RetValue == 1 ) + continue; + // the case of constant 0 cone + if ( RetValue == -1 ) + { + Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0, 1 ); + continue; + } + assert( Vec_PtrSize(vLeaves) > 2 ); + // get the required level for this node + LevelR = vRequired? Vec_IntEntry(vRequired, pObj->Id) : 1000000; + // create a new cone + pResult = Ivy_NodeRewriteAlg( pObj, vFront, vLeaves, vCone, vSol, LevelR, fUseZeroCost ); + if ( pResult == NULL || pResult == pObj ) + continue; + assert( Vec_PtrSize(vSol) == 1 || !Ivy_IsComplement(pResult) ); + if ( Ivy_ObjLevel(Ivy_Regular(pResult)) > LevelR && Ivy_ObjRefs(Ivy_Regular(pResult)) == 0 ) + Ivy_ObjDelete_rec(Ivy_Regular(pResult), 1), CountUndo++; + else + Ivy_ObjReplace( pObj, pResult, 1, 0, 1 ), CountUsed++; + } + printf( "Used = %d. Undo = %d.\n", CountUsed, CountUndo ); + Vec_PtrFree( vFront ); + Vec_PtrFree( vCone ); + Vec_PtrFree( vSol ); + if ( vRequired ) Vec_IntFree( vRequired ); + if ( i = Ivy_ManCleanup(p) ) + printf( "Cleanup after rewriting removed %d dangling nodes.\n", i ); + if ( !Ivy_ManCheck(p) ) + printf( "Ivy_ManRewriteAlg(): The check has failed.\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Analizes one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_NodeRewriteAlg( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vSols, int LevelR, int fUseZeroCost ) +{ + int fVerbose = 0; + Ivy_Obj_t * pTemp; + int k, Counter, nMffc, RetValue; + + if ( fVerbose ) + { + if ( Ivy_ObjIsExor(pObj) ) + printf( "x " ); + else + printf( " " ); + } + +/* + printf( "%d ", Vec_PtrSize(vFront) ); + printf( "( " ); + Vec_PtrForEachEntry( vFront, pTemp, k ) + printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) ); + printf( ")\n" ); +*/ + // collect nodes in the cone + if ( Ivy_ObjIsExor(pObj) ) + Ivy_ManCollectCone( pObj, vFront, vCone ); + else + Ivy_ManCollectCone( pObj, vLeaves, vCone ); + + // deref nodes in the cone + Vec_PtrForEachEntry( vCone, pTemp, k ) + { + Ivy_ObjRefsDec( Ivy_ObjFanin0(pTemp) ); + Ivy_ObjRefsDec( Ivy_ObjFanin1(pTemp) ); + pTemp->fMarkB = 1; + } + + // count the MFFC size + Vec_PtrForEachEntry( vFront, pTemp, k ) + Ivy_Regular(pTemp)->fMarkA = 1; + nMffc = Ivy_NodeCountMffc( pObj ); + Vec_PtrForEachEntry( vFront, pTemp, k ) + Ivy_Regular(pTemp)->fMarkA = 0; + + if ( fVerbose ) + { + Counter = 0; + Vec_PtrForEachEntry( vCone, pTemp, k ) + Counter += (Ivy_ObjRefs(pTemp) > 0); + printf( "%5d : Leaves = %2d. Cone = %2d. ConeRef = %2d. Mffc = %d. Lev = %d. LevR = %d.\n", + pObj->Id, Vec_PtrSize(vFront), Vec_PtrSize(vCone), Counter-1, nMffc, Ivy_ObjLevel(pObj), LevelR ); + } +/* + printf( "Leaves:" ); + Vec_PtrForEachEntry( vLeaves, pTemp, k ) + printf( " %d%s", Ivy_Regular(pTemp)->Id, Ivy_IsComplement(pTemp)? "\'" : "" ); + printf( "\n" ); + printf( "Cone:\n" ); + Vec_PtrForEachEntry( vCone, pTemp, k ) + printf( " %5d = %d%s %d%s\n", pTemp->Id, + Ivy_ObjFaninId0(pTemp), Ivy_ObjFaninC0(pTemp)? "\'" : "", + Ivy_ObjFaninId1(pTemp), Ivy_ObjFaninC1(pTemp)? "\'" : "" ); +*/ + + RetValue = Ivy_MultiPlus( vLeaves, vCone, Ivy_ObjType(pObj), nMffc + fUseZeroCost, vSols ); + + // ref nodes in the cone + Vec_PtrForEachEntry( vCone, pTemp, k ) + { + Ivy_ObjRefsInc( Ivy_ObjFanin0(pTemp) ); + Ivy_ObjRefsInc( Ivy_ObjFanin1(pTemp) ); + pTemp->fMarkA = 0; + pTemp->fMarkB = 0; + } + + if ( !RetValue ) + return NULL; + + if ( Vec_PtrSize( vSols ) == 1 ) + return Vec_PtrEntry( vSols, 0 ); + return Ivy_NodeBalanceBuildSuper( vSols, Ivy_ObjType(pObj), 1 ); +} + +/**Function************************************************************* + + Synopsis [Comparison for node pointers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeCountMffc_rec( Ivy_Obj_t * pNode ) +{ + if ( Ivy_ObjRefs(pNode) > 0 || Ivy_ObjIsCi(pNode) || pNode->fMarkA ) + return 0; + assert( pNode->fMarkB ); + pNode->fMarkA = 1; +// printf( "%d ", pNode->Id ); + if ( Ivy_ObjIsBuf(pNode) ) + return Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ); + return 1 + Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ) + Ivy_NodeCountMffc_rec( Ivy_ObjFanin1(pNode) ); +} + +/**Function************************************************************* + + Synopsis [Comparison for node pointers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeCountMffc( Ivy_Obj_t * pNode ) +{ + assert( pNode->fMarkB ); + return 1 + Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ) + Ivy_NodeCountMffc_rec( Ivy_ObjFanin1(pNode) ); +} + +/**Function************************************************************* + + Synopsis [Comparison for node pointers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManFindAlgCutCompare( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 ) +{ + if ( *pp1 < *pp2 ) + return -1; + if ( *pp1 > *pp2 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Computing one algebraic cut.] + + Description [Returns 1 if the tree-leaves of this node where traversed + and found to have no external references (and have not been collected). + Returns 0 if the tree-leaves have external references and are collected.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManFindAlgCut_rec( Ivy_Obj_t * pObj, Ivy_Type_t Type, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone ) +{ + int RetValue0, RetValue1; + Ivy_Obj_t * pObjR = Ivy_Regular(pObj); + assert( !Ivy_ObjIsBuf(pObjR) ); + assert( Type != IVY_EXOR || !Ivy_IsComplement(pObj) ); + + // make sure the node is not visited twice in different polarities + if ( Ivy_IsComplement(pObj) ) + { // if complemented, mark B + if ( pObjR->fMarkA ) + return -1; + pObjR->fMarkB = 1; + } + else + { // if non-complicated, mark A + if ( pObjR->fMarkB ) + return -1; + pObjR->fMarkA = 1; + } + Vec_PtrPush( vCone, pObjR ); + + // if the node is the end of the tree, return + if ( Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Type ) + { + if ( Ivy_ObjRefs(pObjR) == 1 ) + return 1; + assert( Ivy_ObjRefs(pObjR) > 1 ); + Vec_PtrPush( vFront, pObj ); + return 0; + } + + // branch on the node + assert( !Ivy_IsComplement(pObj) ); + assert( Ivy_ObjIsNode(pObj) ); + // what if buffer has more than one fanout??? + RetValue0 = Ivy_ManFindAlgCut_rec( Ivy_ObjReal( Ivy_ObjChild0(pObj) ), Type, vFront, vCone ); + RetValue1 = Ivy_ManFindAlgCut_rec( Ivy_ObjReal( Ivy_ObjChild1(pObj) ), Type, vFront, vCone ); + if ( RetValue0 == -1 || RetValue1 == -1 ) + return -1; + + // the case when both have no external references + if ( RetValue0 && RetValue1 ) + { + if ( Ivy_ObjRefs(pObj) == 1 ) + return 1; + assert( Ivy_ObjRefs(pObj) > 1 ); + Vec_PtrPush( vFront, pObj ); + return 0; + } + // the case when one of them has external references + if ( RetValue0 ) + Vec_PtrPush( vFront, Ivy_ObjReal( Ivy_ObjChild0(pObj) ) ); + if ( RetValue1 ) + Vec_PtrPush( vFront, Ivy_ObjReal( Ivy_ObjChild1(pObj) ) ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Computing one algebraic cut.] + + Description [Algebraic cut stops when we hit (a) CI, (b) complemented edge, + (c) boundary of different gates. Returns 1 if this is a pure tree. + Returns -1 if the contant 0 is detected. Return 0 if the array can be used.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone ) +{ + Ivy_Obj_t * pObj, * pPrev; + int RetValue, i; + assert( !Ivy_IsComplement(pRoot) ); + assert( Ivy_ObjIsNode(pRoot) ); + // clear the frontier and collect the nodes + Vec_PtrClear( vCone ); + Vec_PtrClear( vFront ); + Vec_PtrClear( vLeaves ); + RetValue = Ivy_ManFindAlgCut_rec( pRoot, Ivy_ObjType(pRoot), vFront, vCone ); + // clean the marks + Vec_PtrForEachEntry( vCone, pObj, i ) + pObj->fMarkA = pObj->fMarkB = 0; + // quit if the same node is found in both polarities + if ( RetValue == -1 ) + return -1; + // return if the node is the root of a tree + if ( RetValue == 1 ) + return 1; + // return if the cut is composed of two nodes + if ( Vec_PtrSize(vFront) <= 2 ) + return 1; + // sort the entries in increasing order + Vec_PtrSort( vFront, Ivy_ManFindAlgCutCompare ); + // remove duplicates from vFront and save the nodes in vLeaves + pPrev = Vec_PtrEntry(vFront, 0); + Vec_PtrPush( vLeaves, pPrev ); + Vec_PtrForEachEntryStart( vFront, pObj, i, 1 ) + { + // compare current entry and the previous entry + if ( pObj == pPrev ) + { + if ( Ivy_ObjIsExor(pRoot) ) // A <+> A = 0 + { + // vLeaves are no longer structural support of pRoot!!! + Vec_PtrPop(vLeaves); + pPrev = Vec_PtrSize(vLeaves) == 0 ? NULL : Vec_PtrEntryLast(vLeaves); + } + continue; + } + if ( pObj == Ivy_Not(pPrev) ) + { + assert( Ivy_ObjIsAnd(pRoot) ); + return -1; + } + pPrev = pObj; + Vec_PtrPush( vLeaves, pObj ); + } + if ( Vec_PtrSize(vLeaves) == 0 ) + return -1; + if ( Vec_PtrSize(vLeaves) <= 2 ) + return 1; + return 0; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |