diff options
Diffstat (limited to 'src/aig/gia/giaChoice.c')
-rw-r--r-- | src/aig/gia/giaChoice.c | 498 |
1 files changed, 498 insertions, 0 deletions
diff --git a/src/aig/gia/giaChoice.c b/src/aig/gia/giaChoice.c new file mode 100644 index 00000000..373f9104 --- /dev/null +++ b/src/aig/gia/giaChoice.c @@ -0,0 +1,498 @@ +/**CFile**************************************************************** + + FileName [giaChoice.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Normalization of structural choices.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaChoice.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "giaAig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Reverse the order of nodes in equiv classes.] + + Description [If the flag is 1, assumed current increasing order ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing ) +{ + Vec_Int_t * vCollected; + Vec_Int_t * vClass; + int i, k, iRepr, iNode, iPrev; + // collect classes + vCollected = Vec_IntAlloc( 100 ); + Gia_ManForEachClass( p, iRepr ) + { + Vec_IntPush( vCollected, iRepr ); +/* + // check classes + if ( !fNowIncreasing ) + { + iPrev = iRepr; + Gia_ClassForEachObj1( p, iRepr, iNode ) + { + if ( iPrev < iNode ) + { + printf( "Class %d : ", iRepr ); + Gia_ClassForEachObj( p, iRepr, iNode ) + printf( " %d", iNode ); + printf( "\n" ); + break; + } + iPrev = iNode; + } + } +*/ + } + // correct each class + vClass = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vCollected, iRepr, i ) + { + Vec_IntClear( vClass ); + Vec_IntPush( vClass, iRepr ); + Gia_ClassForEachObj1( p, iRepr, iNode ) + { + if ( fNowIncreasing ) + assert( iRepr < iNode ); +// else +// assert( iRepr > iNode ); + Vec_IntPush( vClass, iNode ); + } + if ( !fNowIncreasing ) + Vec_IntSort( vClass, 1 ); +// if ( iRepr == 129720 || iRepr == 129737 ) +// Vec_IntPrint( vClass ); + // reverse the class + iPrev = 0; + iRepr = Vec_IntEntryLast( vClass ); + Vec_IntForEachEntry( vClass, iNode, k ) + { + if ( fNowIncreasing ) + Gia_ObjSetReprRev( p, iNode, iNode == iRepr ? GIA_VOID : iRepr ); + else + Gia_ObjSetRepr( p, iNode, iNode == iRepr ? GIA_VOID : iRepr ); + Gia_ObjSetNext( p, iNode, iPrev ); + iPrev = iNode; + } + } + Vec_IntFree( vCollected ); + Vec_IntFree( vClass ); + // verify + Gia_ManForEachClass( p, iRepr ) + Gia_ClassForEachObj1( p, iRepr, iNode ) + if ( fNowIncreasing ) + assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr > iNode ); + else + assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr < iNode ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManVerifyChoices( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, iRepr, iNode, fProb = 0; + assert( p->pReprs ); + + // mark nodes + Gia_ManCleanMark0(p); + Gia_ManForEachClass( p, iRepr ) + Gia_ClassForEachObj1( p, iRepr, iNode ) + { + if ( Gia_ObjIsHead(p, iNode) ) + printf( "Member %d of choice class %d is a representative.\n", iNode, iRepr ), fProb = 1; + if ( Gia_ManObj( p, iNode )->fMark0 == 1 ) + printf( "Node %d participates in more than one choice node.\n", iNode ), fProb = 1; + Gia_ManObj( p, iNode )->fMark0 = 1; + } + Gia_ManCleanMark0(p); + + Gia_ManForEachObj( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + { + if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) ) + printf( "Fanin 0 of AND node %d has a repr.\n", i ), fProb = 1; + if ( Gia_ObjHasRepr(p, Gia_ObjFaninId1(pObj, i)) ) + printf( "Fanin 1 of AND node %d has a repr.\n", i ), fProb = 1; + } + else if ( Gia_ObjIsCo(pObj) ) + { + if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) ) + printf( "Fanin 0 of CO node %d has a repr.\n", i ), fProb = 1; + } + } + if ( !fProb ) + printf( "GIA with choices is correct.\n" ); +} + +/**Function************************************************************* + + Synopsis [Make sure reprsentative nodes do not have representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCheckReprs( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, fProb = 0; + Gia_ManForEachObj( p, pObj, i ) + { + if ( !Gia_ObjHasRepr(p, i) ) + continue; + if ( !Gia_ObjIsAnd(pObj) ) + printf( "Obj %d is not an AND but it has a repr %d.\n", i, Gia_ObjRepr(p, i) ), fProb = 1; + else if ( Gia_ObjHasRepr( p, Gia_ObjRepr(p, i) ) ) + printf( "Obj %d has repr %d with a repr %d.\n", i, Gia_ObjRepr(p, i), Gia_ObjRepr(p, Gia_ObjRepr(p, i)) ), fProb = 1; + } + if ( !fProb ) + printf( "GIA \"%s\": Representive verification successful.\n", Gia_ManName(p) ); +} + +/**Function************************************************************* + + Synopsis [Find minimum level of each node using representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManMinLevelRepr_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + int levMin, levCur, objId, reprId; + // skip visited nodes + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return Gia_ObjLevel(p, pObj); + Gia_ObjSetTravIdCurrent(p, pObj); + // skip CI nodes + if ( Gia_ObjIsCi(pObj) ) + return Gia_ObjLevel(p, pObj); + assert( Gia_ObjIsAnd(pObj) ); + objId = Gia_ObjId(p, pObj); + if ( Gia_ObjIsNone(p, objId) ) + { + // not part of the equivalence class + Gia_ManMinLevelRepr_rec( p, Gia_ObjFanin0(pObj) ); + Gia_ManMinLevelRepr_rec( p, Gia_ObjFanin1(pObj) ); + Gia_ObjSetAndLevel( p, pObj ); + return Gia_ObjLevel(p, pObj); + } + // has equivalences defined + assert( Gia_ObjHasRepr(p, objId) || Gia_ObjIsHead(p, objId) ); + reprId = Gia_ObjHasRepr(p, objId) ? Gia_ObjRepr(p, objId) : objId; + // iterate through objects + levMin = ABC_INFINITY; + Gia_ClassForEachObj( p, reprId, objId ) + { + levCur = Gia_ManMinLevelRepr_rec( p, Gia_ManObj(p, objId) ); + levMin = Abc_MinInt( levMin, levCur ); + } + assert( levMin < ABC_INFINITY ); + // assign minimum level to all + Gia_ClassForEachObj( p, reprId, objId ) + Gia_ObjSetLevelId( p, objId, levMin ); + return levMin; +} +int Gia_ManMinLevelRepr( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, LevelCur, LevelMax = 0; + assert( Gia_ManRegNum(p) == 0 ); + Gia_ManCleanLevels( p, Gia_ManObjNum(p) ); + Gia_ManIncrementTravId( p ); + Gia_ManForEachAnd( p, pObj, i ) + { + assert( !Gia_ObjIsConst(p, i) ); + LevelCur = Gia_ManMinLevelRepr_rec( p, pObj ); + LevelMax = Abc_MaxInt( LevelMax, LevelCur ); + } + printf( "Max level %d\n", LevelMax ); + return LevelMax; +} + +/**Function************************************************************* + + Synopsis [Returns mapping of each old repr into new repr.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Gia_ManFindMinLevelMap( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int reprId, objId, levFan0, levFan1; + int levMin, levMinOld, levMax, reprBest; + int * pReprMap, * pMinLevels, iFanin; + int i, fChange = 1; + + Gia_ManLevelNum( p ); + pMinLevels = ABC_ALLOC( int, Gia_ManObjNum(p) ); + while ( fChange ) + { + fChange = 0; + // clean min-levels + memset( pMinLevels, 0xFF, sizeof(int) * Gia_ManObjNum(p) ); + // for each class find min level + Gia_ManForEachClass( p, reprId ) + { + levMin = ABC_INFINITY; + Gia_ClassForEachObj( p, reprId, objId ) + levMin = Abc_MinInt( levMin, Gia_ObjLevelId(p, objId) ); + assert( levMin >= 0 && levMin < ABC_INFINITY ); + Gia_ClassForEachObj( p, reprId, objId ) + { + assert( pMinLevels[objId] == -1 ); + pMinLevels[objId] = levMin; + } + } + // recompute levels + levMax = 0; + Gia_ManForEachAnd( p, pObj, i ) + { + iFanin = Gia_ObjFaninId0(pObj, i); + if ( Gia_ObjIsNone(p, iFanin) ) + levFan0 = Gia_ObjLevelId(p, iFanin); + else if ( Gia_ObjIsConst(p, iFanin) ) + levFan0 = 0; + else + { + assert( Gia_ObjIsClass( p, iFanin ) ); + assert( pMinLevels[iFanin] >= 0 ); + levFan0 = pMinLevels[iFanin]; + } + + iFanin = Gia_ObjFaninId1(pObj, i); + if ( Gia_ObjIsNone(p, iFanin) ) + levFan1 = Gia_ObjLevelId(p, iFanin); + else if ( Gia_ObjIsConst(p, iFanin) ) + levFan1 = 0; + else + { + assert( Gia_ObjIsClass( p, iFanin ) ); + assert( pMinLevels[iFanin] >= 0 ); + levFan1 = pMinLevels[iFanin]; + } + levMinOld = Gia_ObjLevelId(p, i); + levMin = 1 + Abc_MaxInt( levFan0, levFan1 ); + Gia_ObjSetLevelId( p, i, levMin ); + assert( levMin <= levMinOld ); + if ( levMin < levMinOld ) + fChange = 1; + levMax = Abc_MaxInt( levMax, levMin ); + } + printf( "%d ", levMax ); + } + ABC_FREE( pMinLevels ); + printf( "\n" ); + + // create repr map + pReprMap = ABC_FALLOC( int, Gia_ManObjNum(p) ); + Gia_ManForEachAnd( p, pObj, i ) + if ( Gia_ObjIsConst(p, i) ) + pReprMap[i] = 0; + Gia_ManForEachClass( p, reprId ) + { + // find min-level repr + reprBest = -1; + levMin = ABC_INFINITY; + Gia_ClassForEachObj( p, reprId, objId ) + if ( levMin > Gia_ObjLevelId(p, objId) ) + { + levMin = Gia_ObjLevelId(p, objId); + reprBest = objId; + } + assert( reprBest > 0 ); + Gia_ClassForEachObj( p, reprId, objId ) + pReprMap[objId] = reprBest; + } + return pReprMap; +} + + + +/**Function************************************************************* + + Synopsis [Find terminal AND nodes] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManDanglingAndNodes( Gia_Man_t * p ) +{ + Vec_Int_t * vTerms; + Gia_Obj_t * pObj; + int i; + Gia_ManCleanMark0( p ); + Gia_ManForEachAnd( p, pObj, i ) + { + Gia_ObjFanin0(pObj)->fMark0 = 1; + Gia_ObjFanin1(pObj)->fMark1 = 1; + } + vTerms = Vec_IntAlloc( 1000 ); + Gia_ManForEachAnd( p, pObj, i ) + if ( !pObj->fMark0 ) + Vec_IntPush( vTerms, i ); + Gia_ManCleanMark0( p ); + return vTerms; +} + +/**Function************************************************************* + + Synopsis [Reconstruct AIG starting with terminals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManRebuidRepr_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int * pReprMap ) +{ + int objId, reprLit = -1; + if ( ~pObj->Value ) + return pObj->Value; + assert( Gia_ObjIsAnd(pObj) ); + objId = Gia_ObjId( p, pObj ); + if ( Gia_ObjIsClass(p, objId) ) + { + assert( pReprMap[objId] > 0 ); + reprLit = Gia_ManRebuidRepr_rec( pNew, p, Gia_ManObj(p, pReprMap[objId]), pReprMap ); + assert( reprLit > 1 ); + } + else + assert( Gia_ObjIsNone(p, objId) ); + Gia_ManRebuidRepr_rec( pNew, p, Gia_ObjFanin0(pObj), pReprMap ); + Gia_ManRebuidRepr_rec( pNew, p, Gia_ObjFanin1(pObj), pReprMap ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + assert( reprLit != (int)pObj->Value ); + if ( reprLit > 1 ) + pNew->pReprs[ Abc_Lit2Var(pObj->Value) ].iRepr = Abc_Lit2Var(reprLit); + return pObj->Value; +} +Gia_Man_t * Gia_ManRebuidRepr( Gia_Man_t * p, int * pReprMap ) +{ + Vec_Int_t * vTerms; + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + vTerms = Gia_ManDanglingAndNodes( p ); + Gia_ManForEachObjVec( vTerms, p, pObj, i ) + Gia_ManRebuidRepr_rec( pNew, p, pObj, pReprMap ); + Vec_IntFree( vTerms ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Gia_ManNormalizeChoices( Aig_Man_t * pAig ) +{ + int * pReprMap; + Aig_Man_t * pNew; + Gia_Man_t * pGia, * pTemp; + // create GIA with representatives + assert( Aig_ManRegNum(pAig) == 0 ); + assert( pAig->pReprs != NULL ); + pGia = Gia_ManFromAigSimple( pAig ); + Gia_ManReprFromAigRepr2( pAig, pGia ); + // verify that representatives are correct + Gia_ManCheckReprs( pGia ); + // find min-level repr for each class + pReprMap = Gia_ManFindMinLevelMap( pGia ); + // reconstruct using correct order + pGia = Gia_ManRebuidRepr( pTemp = pGia, pReprMap ); + Gia_ManStop( pTemp ); + ABC_FREE( pReprMap ); + // create choices + + // verify that choices are correct +// Gia_ManVerifyChoices( pGia ); + // copy the result back into AIG + pNew = Gia_ManToAigSimple( pGia ); + Gia_ManReprToAigRepr( pNew, pGia ); + return pNew; +} +void Gia_ManNormalizeChoicesTest( Aig_Man_t * pAig ) +{ + Aig_Man_t * pNew = Gia_ManNormalizeChoices( pAig ); + Aig_ManStop( pNew ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |