/**CFile**************************************************************** FileName [giaEquiv.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Scalable AIG package.] Synopsis [Manipulation of equivalence classes.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: giaEquiv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "gia.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Given representatives, derives pointers to the next objects.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int * Gia_ManDeriveNexts( Gia_Man_t * p ) { unsigned * pNexts, * pTails; int i; assert( p->pReprs ); pNexts = ABC_CALLOC( unsigned, Gia_ManObjNum(p) ); pTails = ABC_ALLOC( unsigned, Gia_ManObjNum(p) ); for ( i = 0; i < Gia_ManObjNum(p); i++ ) pTails[i] = i; for ( i = 0; i < Gia_ManObjNum(p); i++ ) { if ( !p->pReprs[i].iRepr || p->pReprs[i].iRepr == GIA_VOID ) continue; pNexts[ pTails[p->pReprs[i].iRepr] ] = i; pTails[p->pReprs[i].iRepr] = i; } ABC_FREE( pTails ); return (int *)pNexts; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManEquivCountOne( Gia_Man_t * p, int i ) { int Ent, nLits = 1; Gia_ClassForEachObj1( p, i, Ent ) { assert( Gia_ObjRepr(p, Ent) == i ); nLits++; } return nLits; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter ) { int Ent; printf( "Class %4d : Num = %2d {", Counter, Gia_ManEquivCountOne(p, i) ); Gia_ClassForEachObj( p, i, Ent ) { printf(" %d", Ent ); if ( p->pReprs[Ent].fColorA || p->pReprs[Ent].fColorB ) printf(" <%d%d>", p->pReprs[Ent].fColorA, p->pReprs[Ent].fColorB ); } printf( " }\n" ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManEquivCountLitsAll( Gia_Man_t * p ) { int i, nLits = 0; for ( i = 0; i < Gia_ManObjNum(p); i++ ) nLits += (Gia_ObjRepr(p, i) != GIA_VOID); return nLits; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits ) { int nLitsReal = Gia_ManEquivCountLitsAll( p ); if ( nLitsReal != nLits ) printf( "Detected a mismatch in counting equivalence classes (%d).\n", nLitsReal - nLits ); return 1; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) { int i, Counter = 0, Counter1 = 0, CounterX = 0, Proved = 0, nLits; for ( i = 1; i < Gia_ManObjNum(p); i++ ) { if ( Gia_ObjIsHead(p, i) ) Counter++; else if ( Gia_ObjIsConst(p, i) ) Counter1++; else if ( Gia_ObjIsNone(p, i) ) CounterX++; if ( Gia_ObjProved(p, i) ) Proved++; } CounterX -= Gia_ManCoNum(p); nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; printf( "cls =%7d cst =%8d lit =%8d unused =%8d proof =%6d mem =%5.2f Mb\n", Counter, Counter1, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem ); assert( Gia_ManEquivCheckLits( p, nLits ) ); if ( fVerbose ) { Counter = 0; Gia_ManForEachClass( p, i ) Gia_ManEquivPrintOne( p, i, ++Counter ); } } /**Function************************************************************* Synopsis [Returns representative node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj ) { if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) return NULL; return Gia_ManObj( p, Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ); } /**Function************************************************************* Synopsis [Duplicates the AIG in the DFS order.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) { Gia_Obj_t * pRepr; if ( ~pObj->Value ) return; assert( Gia_ObjIsAnd(pObj) ); if ( (pRepr = Gia_ManEquivRepr(p, pObj)) ) { Gia_ManEquivReduce_rec( pNew, p, pRepr ); pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj) ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } /**Function************************************************************* Synopsis [Reduces AIG using equivalence classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p ) { Gia_Man_t * pNew; Gia_Obj_t * pObj, * pRepr; int i; Gia_ManSetPhase( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) { pObj->Value = Gia_ManAppendCi(pNew); if ( (pRepr = Gia_ManEquivRepr(p, pObj)) ) pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); } Gia_ManHashAlloc( pNew ); Gia_ManForEachCo( p, pObj, i ) Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); Gia_ManForEachCo( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManHashStop( pNew ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); return pNew; } /**Function************************************************************* Synopsis [Reduces AIG using equivalence classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManEquivFixOutputPairs( Gia_Man_t * p ) { Gia_Obj_t * pObj0, * pObj1; int i; assert( (Gia_ManPoNum(p) & 1) == 0 ); Gia_ManForEachPo( p, pObj0, i ) { pObj1 = Gia_ManPo( p, ++i ); if ( Gia_ObjChild0(pObj0) != Gia_ObjChild0(pObj1) ) continue; pObj0->iDiff0 = Gia_ObjId(p, pObj0); pObj0->fCompl0 = 0; pObj1->iDiff0 = Gia_ObjId(p, pObj1); pObj1->fCompl0 = 0; } } /**Function************************************************************* Synopsis [Removes pointers to the unmarked nodes..] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManEquivUpdatePointers( Gia_Man_t * p, Gia_Man_t * pNew ) { Gia_Obj_t * pObj, * pObjNew; int i; Gia_ManForEachObj( p, pObj, i ) { if ( !~pObj->Value ) continue; pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) ); if ( pObjNew->fMark0 ) pObj->Value = ~0; } } /**Function************************************************************* Synopsis [Removes pointers to the unmarked nodes..] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFinal ) { Vec_Int_t * vClass; Gia_Obj_t * pObj, * pObjNew; int i, k, iNode, iRepr, iPrev; // start representatives pFinal->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pFinal) ); for ( i = 0; i < Gia_ManObjNum(pFinal); i++ ) Gia_ObjSetRepr( pFinal, i, GIA_VOID ); // iterate over constant candidates Gia_ManForEachConst( p, i ) { pObj = Gia_ManObj( p, i ); if ( !~pObj->Value ) continue; pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) ); if ( Gia_Lit2Var(pObjNew->Value) == 0 ) continue; Gia_ObjSetRepr( pFinal, Gia_Lit2Var(pObjNew->Value), 0 ); } // iterate over class candidates vClass = Vec_IntAlloc( 100 ); Gia_ManForEachClass( p, i ) { Vec_IntClear( vClass ); Gia_ClassForEachObj( p, i, k ) { pObj = Gia_ManObj( p, k ); if ( !~pObj->Value ) continue; pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) ); Vec_IntPushUnique( vClass, Gia_Lit2Var(pObjNew->Value) ); } if ( Vec_IntSize( vClass ) < 2 ) continue; Vec_IntSort( vClass, 0 ); iRepr = iPrev = Vec_IntEntry( vClass, 0 ); Vec_IntForEachEntryStart( vClass, iNode, k, 1 ) { Gia_ObjSetRepr( pFinal, iNode, iRepr ); assert( iPrev < iNode ); iPrev = iNode; } } Vec_IntFree( vClass ); pFinal->pNexts = Gia_ManDeriveNexts( pFinal ); } /**Function************************************************************* Synopsis [Reduces AIG while remapping equivalence classes.] Description [Drops the pairs of outputs if they are proved equivalent.] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ) { Gia_Man_t * pNew, * pFinal; pNew = Gia_ManEquivReduce( p ); if ( fMiterPairs ) Gia_ManEquivFixOutputPairs( pNew ); if ( fSeq ) Gia_ManSeqMarkUsed( pNew ); else Gia_ManCombMarkUsed( pNew ); Gia_ManEquivUpdatePointers( p, pNew ); pFinal = Gia_ManDupMarked( pNew ); Gia_ManEquivDeriveReprs( p, pNew, pFinal ); Gia_ManStop( pNew ); return pFinal; } /**Function************************************************************* Synopsis [Marks CIs/COs/ANDs unreachable from POs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManEquivSetColor_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fOdds ) { if ( Gia_ObjVisitColor( p, Gia_ObjId(p,pObj), fOdds ) ) return 0; if ( Gia_ObjIsRo(p, pObj) ) return 1 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p, pObj)), fOdds ); assert( Gia_ObjIsAnd(pObj) ); return 1 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), fOdds ) + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin1(pObj), fOdds ); } /**Function************************************************************* Synopsis [Marks CIs/COs/ANDs unreachable from POs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ) { Gia_Obj_t * pObj; int i, nNodes[2] = {0,0}, nDiffs[2]; assert( (Gia_ManPoNum(p) & 1) == 0 ); Gia_ObjSetColors( p, 0 ); Gia_ManForEachPi( p, pObj, i ) Gia_ObjSetColors( p, Gia_ObjId(p,pObj) ); Gia_ManForEachPo( p, pObj, i ) nNodes[i&1] += Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), i&1 ); // Gia_ManForEachObj( p, pObj, i ) // if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ) // assert( Gia_ObjColors(p, i) ); nDiffs[0] = Gia_ManCiNum(p) + Gia_ManAndNum(p) - (Gia_ManPiNum(p) + nNodes[0]); nDiffs[1] = Gia_ManCiNum(p) + Gia_ManAndNum(p) - (Gia_ManPiNum(p) + nNodes[1]); if ( fVerbose ) { printf( "CI+AND = %7d A = %7d B = %7d Ad = %7d Bd = %7d AB = %7d.\n", Gia_ManCiNum(p) + Gia_ManAndNum(p), Gia_ManPiNum(p) + nNodes[0], Gia_ManPiNum(p) + nNodes[1], nDiffs[0], nDiffs[1], Gia_ManCiNum(p) + Gia_ManAndNum(p) - nDiffs[0] - nDiffs[1] ); } return (nDiffs[0] + nDiffs[1]) / 2; } /**Function************************************************************* Synopsis [Duplicates the AIG in the DFS order.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits ) { Gia_Obj_t * pRepr; int iLitNew; if ( ~pObj->Value ) return; assert( Gia_ObjIsAnd(pObj) ); Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits ); Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); if ( pRepr == NULL ) return; iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); if ( pObj->Value != (unsigned)iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) ); pObj->Value = iLitNew; } /**Function************************************************************* Synopsis [Reduces AIG using equivalence classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj, * pRepr; Vec_Int_t * vXorLits; int i, iLitNew; if ( !p->pReprs ) return NULL; vXorLits = Vec_IntAlloc( 1000 ); Gia_ManSetPhase( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); Gia_ManHashAlloc( pNew ); Gia_ManForEachCi( p, pObj, i ) { pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); if ( pRepr == NULL ) continue; iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); if ( pObj->Value != (unsigned)iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) ); pObj->Value = iLitNew; } Gia_ManForEachCo( p, pObj, i ) Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits ); Vec_IntForEachEntry( vXorLits, iLitNew, i ) Gia_ManAppendCo( pNew, iLitNew ); if ( Vec_IntSize(vXorLits) == 0 ) { printf( "Speculatively reduced model has no primary outputs.\n" ); Gia_ManAppendCo( pNew, 0 ); } Gia_ManForEachRi( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Vec_IntFree( vXorLits ); Gia_ManHashStop( pNew ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); return pNew; } /**Function************************************************************* Synopsis [Transforms equiv classes by removing the AB nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ) { extern void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass ); Vec_Int_t * vClass, * vClassNew; int iRepr, iNode, Ent, k; int nRemovedLits = 0, nRemovedClas = 0; int nTotalLits = 0, nTotalClas = 0; Gia_Obj_t * pObj; int i; assert( p->pReprs && p->pNexts ); vClass = Vec_IntAlloc( 100 ); vClassNew = Vec_IntAlloc( 100 ); Gia_ManForEachObj( p, pObj, i ) if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ) assert( Gia_ObjColors(p, i) ); Gia_ManForEachClassReverse( p, iRepr ) { nTotalClas++; Vec_IntClear( vClass ); Vec_IntClear( vClassNew ); Gia_ClassForEachObj( p, iRepr, iNode ) { nTotalLits++; Vec_IntPush( vClass, iNode ); assert( Gia_ObjColors(p, iNode) ); if ( Gia_ObjColors(p, iNode) != 3 ) Vec_IntPush( vClassNew, iNode ); else nRemovedLits++; } Vec_IntForEachEntry( vClass, Ent, k ) { p->pReprs[Ent].fFailed = p->pReprs[Ent].fProved = 0; p->pReprs[Ent].iRepr = GIA_VOID; p->pNexts[Ent] = 0; } if ( Vec_IntSize(vClassNew) < 2 ) { nRemovedClas++; continue; } Cec_ManSimClassCreate( p, vClassNew ); } Vec_IntFree( vClass ); Vec_IntFree( vClassNew ); if ( fVerbose ) printf( "Removed classes = %6d (out of %6d). Removed literals = %6d (out of %6d).\n", nRemovedClas, nTotalClas, nRemovedLits, nTotalLits ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////