From 28467823812f63a40f9a322b1fefc7decce4b766 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 22 Aug 2007 08:01:00 -0700 Subject: Version abc70822 --- src/aig/fra/fraClass.c | 172 ++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 162 insertions(+), 10 deletions(-) (limited to 'src/aig/fra/fraClass.c') diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index a9d727da..d6db125b 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -114,9 +114,18 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ) int i; Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 ); memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) ); + if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 ) + { + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( p->pAig->pReprs[i] != NULL ) + printf( "Classes are not cleared!\n" ); + assert( p->pAig->pReprs[i] == NULL ); + } + } if ( vFailed ) - Vec_PtrForEachEntry( vFailed, pObj, i ) - p->pAig->pReprs[pObj->Id] = NULL; + Vec_PtrForEachEntry( vFailed, pObj, i ) + p->pAig->pReprs[pObj->Id] = NULL; } /**Function************************************************************* @@ -206,7 +215,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass ) assert( Fra_ClassObjRepr(pTemp) == pClass[0] ); printf( "{ " ); for ( i = 0; pTemp = pClass[i]; i++ ) - printf( "%d ", pTemp->Id, Fra_ClassObjRepr(pTemp)? Fra_ClassObjRepr(pTemp)->Id : -1 ); + printf( "%d(%d) ", pTemp->Id, pTemp->Level ); printf( "}\n" ); } @@ -227,8 +236,11 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ) Aig_Obj_t * pObj; int i; - printf( "Const = %5d. Class = %5d. Lit = %5d.\n", + printf( "Const = %5d. Class = %5d. Lit = %5d. ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) ); + if ( p->vImps && Vec_IntSize(p->vImps) > 0 ) + printf( "Imp = %5d. ", Vec_IntSize(p->vImps) ); + printf( "\n" ); if ( fVeryVerbose ) { @@ -283,10 +295,10 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr ) { if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) continue; + // skip the node with more that the given number of levels +// if ( pObj->Level > 3 ) +// continue; } -//printf( "%3d : ", pObj->Id ); -//Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 ); -//printf( "\n" ); // hash the node by its simulation info iEntry = p->pFuncNodeHash( pObj, nTableSize ); // check if the node belongs to the class of constant 1 @@ -494,7 +506,6 @@ int Fra_ClassesRefine( Fra_Cla_t * p ) vTemp = p->vClassesTemp; p->vClassesTemp = p->vClasses; p->vClasses = vTemp; - p->fRefinement = (nRefis > 0); return nRefis; } @@ -531,7 +542,6 @@ int Fra_ClassesRefine1( Fra_Cla_t * p ) Vec_PtrShrink( p->vClasses1, k ); if ( Vec_PtrSize(p->vClassNew) == 0 ) return 0; - p->fRefinement = 1; /* printf( "Refined const-1 class: {" ); Vec_PtrForEachEntry( p->vClassNew, pObj, i ) @@ -675,6 +685,95 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) free( pWeights ); } +/**Function************************************************************* + + Synopsis [Postprocesses the classes by selecting representative lowest in top order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesSelectRepr( Fra_Cla_t * p ) +{ + Aig_Obj_t ** pClass, * pNodeMin; + int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur; + // reassign representatives in each class + Vec_PtrForEachEntry( p->vClasses, pClass, i ) + { + // collect support sizes and find the min-support node + pNodeMin = NULL; + nSuppSizeMin = AIG_INFINITY; + for ( c = 0; pClass[c]; c++ ) + { + nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] ); +// nSuppSizeCur = 1; + if ( nSuppSizeMin > nSuppSizeCur || + (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) ) + { + nSuppSizeMin = nSuppSizeCur; + pNodeMin = pClass[c]; + cMinSupp = c; + } + } + // skip the case when the repr did not change + if ( cMinSupp == 0 ) + continue; + // make the new node the representative of the class + pClass[cMinSupp] = pClass[0]; + pClass[0] = pNodeMin; + // set the representative + for ( c = 0; pClass[c]; c++ ) + Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL ); + } +} + + + +static inline Aig_Obj_t * Fra_ObjEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return ppEquivs[pObj->Id]; } +static inline void Fra_ObjSetEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ppEquivs[pObj->Id] = pNode; } + +static inline Aig_Obj_t * Fra_ObjChild0Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)); } +static inline Aig_Obj_t * Fra_ObjChild1Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)); } + +/**Function************************************************************* + + Synopsis [Add the node and its constraints to the new AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, Aig_Obj_t ** ppEquivs ) +{ + Aig_Obj_t * pObjNew, * pObjRepr, * pObjReprNew, * pMiter;//, * pObjNew2; + // skip nodes without representative + if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL ) + return; + assert( pObjRepr->Id < pObj->Id ); + // get the new node + pObjNew = Fra_ObjEqu( ppEquivs, pObj ); + // get the new node of the representative + pObjReprNew = Fra_ObjEqu( ppEquivs, pObjRepr ); + // if this is the same node, no need to add constraints + if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) ) + return; + // these are different nodes - perform speculative reduction +// pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase ); + // set the new node +// Fra_ObjSetEqu( ppEquivs, pObj, pObjNew2 ); + // add the constraint + pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) ); + pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) ); + pMiter = Aig_Not( pMiter ); + Aig_ObjCreatePo( pManFraig, pMiter ); +} + /**Function************************************************************* Synopsis [Derives AIG for the partitioned problem.] @@ -688,7 +787,60 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) ***********************************************************************/ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ) { - + Aig_Man_t * pManFraig; + Aig_Obj_t * pObj, * pObjNew; + Aig_Obj_t ** pLatches, ** ppEquivs; + int i, k, f, nFramesAll = nFramesK + 1; + assert( Aig_ManRegNum(p->pAig) > 0 ); + assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); + assert( nFramesK > 0 ); + // start the fraig package + pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * nFramesAll ); + // allocate place for the node mapping + ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p->pAig) + 1 ); + Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) ); + // create latches for the first frame + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) ); + // add timeframes + pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) ); + for ( f = 0; f < nFramesAll; f++ ) + { + // create PIs for this frame + Aig_ManForEachPiSeq( p->pAig, pObj, i ) + Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) ); + // set the constraints on the latch outputs + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs ); + // add internal nodes of this frame + Aig_ManForEachNode( p->pAig, pObj, i ) + { + pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) ); + Fra_ObjSetEqu( ppEquivs, pObj, pObjNew ); + Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs ); + } + if ( f == nFramesAll - 1 ) + break; + if ( f == nFramesAll - 2 ) + pManFraig->nAsserts = Aig_ManPoNum(pManFraig); + // save the latch input values + k = 0; + Aig_ManForEachLiSeq( p->pAig, pObj, i ) + pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj ); + // insert them to the latch output values + k = 0; + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] ); + } + free( pLatches ); + free( ppEquivs ); + // mark the asserts + assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 ); +printf( "Assert miters = %6d. Output miters = %6d.\n", + pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts ); + // remove dangling nodes + Aig_ManCleanup( pManFraig ); + return pManFraig; } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3