diff options
Diffstat (limited to 'src/proof/fra/fraClass.c')
| -rw-r--r-- | src/proof/fra/fraClass.c | 862 |
1 files changed, 862 insertions, 0 deletions
diff --git a/src/proof/fra/fraClass.c b/src/proof/fra/fraClass.c new file mode 100644 index 00000000..67351f6d --- /dev/null +++ b/src/proof/fra/fraClass.c @@ -0,0 +1,862 @@ +/**CFile**************************************************************** + + FileName [fraClass.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [New FRAIG package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraClass.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" + +ABC_NAMESPACE_IMPL_START + + +/* + The candidate equivalence classes are stored as a vector of pointers + to the array of pointers to the nodes in each class. + The first node of the class is its representative node. + The representative has the smallest topological order among the class nodes. + The nodes inside each class are ordered according to their topological order. + The classes are ordered according to the topological order of their representatives. + The array of pointers to the class nodes is terminated with a NULL pointer. + To enable dynamic addition of new classes (during class refinement), + each array has at least as many NULLs in the end, as there are nodes in the class. +*/ + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Aig_Obj_t * Fra_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj ) { return ppNexts[pObj->Id]; } +static inline void Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ) +{ + Fra_Cla_t * p; + p = ABC_ALLOC( Fra_Cla_t, 1 ); + memset( p, 0, sizeof(Fra_Cla_t) ); + p->pAig = pAig; + p->pMemRepr = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); + memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) ); + p->vClasses = Vec_PtrAlloc( 100 ); + p->vClasses1 = Vec_PtrAlloc( 100 ); + p->vClassesTemp = Vec_PtrAlloc( 100 ); + p->vClassOld = Vec_PtrAlloc( 100 ); + p->vClassNew = Vec_PtrAlloc( 100 ); + p->pFuncNodeHash = Fra_SmlNodeHash; + p->pFuncNodeIsConst = Fra_SmlNodeIsConst; + p->pFuncNodesAreEqual = Fra_SmlNodesAreEqual; + return p; +} + +/**Function************************************************************* + + Synopsis [Stop representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesStop( Fra_Cla_t * p ) +{ + ABC_FREE( p->pMemClasses ); + ABC_FREE( p->pMemRepr ); + if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp ); + if ( p->vClassNew ) Vec_PtrFree( p->vClassNew ); + if ( p->vClassOld ) Vec_PtrFree( p->vClassOld ); + if ( p->vClasses1 ) Vec_PtrFree( p->vClasses1 ); + if ( p->vClasses ) Vec_PtrFree( p->vClasses ); + if ( p->vImps ) Vec_IntFree( p->vImps ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Starts representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) ); + memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) ); + 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( Aig_Obj_t *, vFailed, pObj, i ) + p->pAig->pReprs[pObj->Id] = NULL; +} + +/**Function************************************************************* + + Synopsis [Prints simulation classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_ClassCount( Aig_Obj_t ** pClass ) +{ + Aig_Obj_t * pTemp; + int i; + for ( i = 0; (pTemp = pClass[i]); i++ ); + return i; +} + +/**Function************************************************************* + + Synopsis [Count the number of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_ClassesCountLits( Fra_Cla_t * p ) +{ + Aig_Obj_t ** pClass; + int i, nNodes, nLits = 0; + nLits = Vec_PtrSize( p->vClasses1 ); + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i ) + { + nNodes = Fra_ClassCount( pClass ); + assert( nNodes > 1 ); + nLits += nNodes - 1; + } + return nLits; +} + +/**Function************************************************************* + + Synopsis [Count the number of pairs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_ClassesCountPairs( Fra_Cla_t * p ) +{ + Aig_Obj_t ** pClass; + int i, nNodes, nPairs = 0; + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i ) + { + nNodes = Fra_ClassCount( pClass ); + assert( nNodes > 1 ); + nPairs += nNodes * (nNodes - 1) / 2; + } + return nPairs; +} + +/**Function************************************************************* + + Synopsis [Prints simulation classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_PrintClass( Fra_Cla_t * p, Aig_Obj_t ** pClass ) +{ + Aig_Obj_t * pTemp; + int i; + for ( i = 1; (pTemp = pClass[i]); i++ ) + assert( Fra_ClassObjRepr(pTemp) == pClass[0] ); + printf( "{ " ); + for ( i = 0; (pTemp = pClass[i]); i++ ) + printf( "%d(%d,%d) ", pTemp->Id, pTemp->Level, Aig_SupportSize(p->pAig,pTemp) ); + printf( "}\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints simulation classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ) +{ + Aig_Obj_t ** pClass; + Aig_Obj_t * pObj; + int i; + + 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 ) + { + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i ) + assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) ); + printf( "Constants { " ); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i ) + printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) ); + printf( "}\n" ); + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i ) + { + printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) ); + Fra_PrintClass( p, pClass ); + } + printf( "\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Creates initial simulation classes.] + + Description [Assumes that simulation info is assigned.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs ) +{ + Aig_Obj_t ** ppTable, ** ppNexts; + Aig_Obj_t * pObj, * pTemp; + int i, k, nTableSize, nEntries, nNodes, iEntry; + + // allocate the hash table hashing simulation info into nodes + nTableSize = Abc_PrimeCudd( Aig_ManObjNumMax(p->pAig) ); + ppTable = ABC_FALLOC( Aig_Obj_t *, nTableSize ); + ppNexts = ABC_FALLOC( Aig_Obj_t *, nTableSize ); + memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize ); + + // add all the nodes to the hash table + Vec_PtrClear( p->vClasses1 ); + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( fLatchCorr ) + { + if ( !Aig_ObjIsPi(pObj) ) + continue; + } + else + { + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + continue; + // skip the node with more that the given number of levels + if ( nMaxLevs && (int)pObj->Level > nMaxLevs ) + continue; + } + // hash the node by its simulation info + iEntry = p->pFuncNodeHash( pObj, nTableSize ); + // check if the node belongs to the class of constant 1 + if ( p->pFuncNodeIsConst( pObj ) ) + { + Vec_PtrPush( p->vClasses1, pObj ); + Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) ); + continue; + } + // add the node to the class + if ( ppTable[iEntry] == NULL ) + { + ppTable[iEntry] = pObj; + Fra_ObjSetNext( ppNexts, pObj, pObj ); + } + else + { + Fra_ObjSetNext( ppNexts, pObj, Fra_ObjNext(ppNexts,ppTable[iEntry]) ); + Fra_ObjSetNext( ppNexts, ppTable[iEntry], pObj ); + } + } + + // count the total number of nodes in the non-trivial classes + // mark the representative nodes of each equivalence class + nEntries = 0; + for ( i = 0; i < nTableSize; i++ ) + if ( ppTable[i] && ppTable[i] != Fra_ObjNext(ppNexts, ppTable[i]) ) + { + for ( pTemp = Fra_ObjNext(ppNexts, ppTable[i]), k = 1; + pTemp != ppTable[i]; + pTemp = Fra_ObjNext(ppNexts, pTemp), k++ ); + assert( k > 1 ); + nEntries += k; + // mark the node + assert( ppTable[i]->fMarkA == 0 ); + ppTable[i]->fMarkA = 1; + } + + // allocate room for classes + p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) ); + p->pMemClassesFree = p->pMemClasses + 2*nEntries; + + // copy the entries into storage in the topological order + Vec_PtrClear( p->vClasses ); + nEntries = 0; + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + continue; + // skip the nodes that are not representatives of non-trivial classes + if ( pObj->fMarkA == 0 ) + continue; + pObj->fMarkA = 0; + // add the class of nodes + Vec_PtrPush( p->vClasses, p->pMemClasses + 2*nEntries ); + // count the number of entries in this class + for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; + pTemp != pObj; + pTemp = Fra_ObjNext(ppNexts, pTemp), k++ ); + nNodes = k; + assert( nNodes > 1 ); + // add the nodes to the class in the topological order + p->pMemClasses[2*nEntries] = pObj; + for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; + pTemp != pObj; + pTemp = Fra_ObjNext(ppNexts, pTemp), k++ ) + { + p->pMemClasses[2*nEntries+nNodes-k] = pTemp; + Fra_ClassObjSetRepr( pTemp, pObj ); + } + // add as many empty entries + p->pMemClasses[2*nEntries + nNodes] = NULL; + // increment the number of entries + nEntries += k; + } + ABC_FREE( ppTable ); + ABC_FREE( ppNexts ); + // now it is time to refine the classes + Fra_ClassesRefine( p ); +// Fra_ClassesPrint( p, 0 ); +} + +/**Function************************************************************* + + Synopsis [Refines one class using simulation info.] + + Description [Returns the new class if refinement happened.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass ) +{ + Aig_Obj_t * pObj, ** ppThis; + int i; + assert( ppClass[0] != NULL && ppClass[1] != NULL ); + + // check if the class is going to be refined + for ( ppThis = ppClass + 1; (pObj = *ppThis); ppThis++ ) + if ( !p->pFuncNodesAreEqual(ppClass[0], pObj) ) + break; + if ( pObj == NULL ) + return NULL; + // split the class + Vec_PtrClear( p->vClassOld ); + Vec_PtrClear( p->vClassNew ); + Vec_PtrPush( p->vClassOld, ppClass[0] ); + for ( ppThis = ppClass + 1; (pObj = *ppThis); ppThis++ ) + if ( p->pFuncNodesAreEqual(ppClass[0], pObj) ) + Vec_PtrPush( p->vClassOld, pObj ); + else + Vec_PtrPush( p->vClassNew, pObj ); +/* + printf( "Refining class (" ); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i ) + printf( "%d,", pObj->Id ); + printf( ") + (" ); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) + printf( "%d,", pObj->Id ); + printf( ")\n" ); +*/ + // put the nodes back into the class memory + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i ) + { + ppClass[i] = pObj; + ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL; + Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL ); + } + ppClass += 2*Vec_PtrSize(p->vClassOld); + // put the new nodes into the class memory + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) + { + ppClass[i] = pObj; + ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL; + Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL ); + } + return ppClass; +} + +/**Function************************************************************* + + Synopsis [Iteratively refines the classes after simulation.] + + Description [Returns the number of refinements performed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses ) +{ + Aig_Obj_t ** pClass, ** pClass2; + int nRefis; + pClass = (Aig_Obj_t **)Vec_PtrEntryLast( vClasses ); + for ( nRefis = 0; (pClass2 = Fra_RefineClassOne( p, pClass )); nRefis++ ) + { + // if the original class is trivial, remove it + if ( pClass[1] == NULL ) + Vec_PtrPop( vClasses ); + // if the new class is trivial, stop + if ( pClass2[1] == NULL ) + { + nRefis++; + break; + } + // othewise, add the class and continue + assert( pClass2[0] != NULL ); + Vec_PtrPush( vClasses, pClass2 ); + pClass = pClass2; + } + return nRefis; +} + +/**Function************************************************************* + + Synopsis [Refines the classes after simulation.] + + Description [Assumes that simulation info is assigned. Returns the + number of classes refined.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_ClassesRefine( Fra_Cla_t * p ) +{ + Vec_Ptr_t * vTemp; + Aig_Obj_t ** pClass; + int i, nRefis; + // refine the classes + nRefis = 0; + Vec_PtrClear( p->vClassesTemp ); + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i ) + { + // add the class to the new array + assert( pClass[0] != NULL ); + Vec_PtrPush( p->vClassesTemp, pClass ); + // refine the class iteratively + nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp ); + } + // exchange the class representation + vTemp = p->vClassesTemp; + p->vClassesTemp = p->vClasses; + p->vClasses = vTemp; + return nRefis; +} + +/**Function************************************************************* + + Synopsis [Refines constant 1 equivalence class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped ) +{ + Aig_Obj_t * pObj, ** ppClass; + int i, k, nRefis = 1; + // check if there is anything to refine + if ( Vec_PtrSize(p->vClasses1) == 0 ) + return 0; + // make sure constant 1 class contains only non-constant nodes + assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pAig) ); + // collect all the nodes to be refined + k = 0; + Vec_PtrClear( p->vClassNew ); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i ) + { + if ( p->pFuncNodeIsConst( pObj ) ) + Vec_PtrWriteEntry( p->vClasses1, k++, pObj ); + else + Vec_PtrPush( p->vClassNew, pObj ); + } + Vec_PtrShrink( p->vClasses1, k ); + if ( Vec_PtrSize(p->vClassNew) == 0 ) + return 0; +/* + printf( "Refined const-1 class: {" ); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) + printf( " %d", pObj->Id ); + printf( " }\n" ); +*/ + if ( Vec_PtrSize(p->vClassNew) == 1 ) + { + Fra_ClassObjSetRepr( (Aig_Obj_t *)Vec_PtrEntry(p->vClassNew,0), NULL ); + return 1; + } + // create a new class composed of these nodes + ppClass = p->pMemClassesFree; + p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) + { + ppClass[i] = pObj; + ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL; + Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL ); + } + assert( ppClass[0] != NULL ); + Vec_PtrPush( p->vClasses, ppClass ); + // iteratively refine this class + if ( fRefineNewClass ) + nRefis += Fra_RefineClassLastIter( p, p->vClasses ); + else if ( pSkipped ) + (*pSkipped)++; + return nRefis; +} + +/**Function************************************************************* + + Synopsis [Starts representation of equivalence classes with one class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 ) +{ + Aig_Obj_t ** pClass; + p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 4 ); + pClass = p->pMemClasses; + assert( Id1 < Id2 ); + pClass[0] = Aig_ManObj( p->pAig, Id1 ); + pClass[1] = Aig_ManObj( p->pAig, Id2 ); + pClass[2] = NULL; + pClass[3] = NULL; + Fra_ClassObjSetRepr( pClass[1], pClass[0] ); + Vec_PtrPush( p->vClasses, pClass ); +} + +/**Function************************************************************* + + Synopsis [Creates latch correspondence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesLatchCorr( Fra_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, nEntries = 0; + Vec_PtrClear( p->pCla->vClasses1 ); + Aig_ManForEachLoSeq( p->pManAig, pObj, i ) + { + Vec_PtrPush( p->pCla->vClasses1, pObj ); + Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) ); + } + // allocate room for classes + p->pCla->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) ); + p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries; +} + +/**Function************************************************************* + + Synopsis [Postprocesses the classes by removing half of the less useful.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesPostprocess( Fra_Cla_t * p ) +{ + int Ratio = 2; + Fra_Sml_t * pComb; + Aig_Obj_t * pObj, * pRepr, ** ppClass; + int * pWeights, WeightMax = 0, i, k, c; + // perform combinational simulation + pComb = Fra_SmlSimulateComb( p->pAig, 32 ); + // compute the weight of each node in the classes + pWeights = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) ); + memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) ); + Aig_ManForEachObj( p->pAig, pObj, i ) + { + pRepr = Fra_ClassObjRepr( pObj ); + if ( pRepr == NULL ) + continue; + pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id ); + WeightMax = Abc_MaxInt( WeightMax, pWeights[i] ); + } + Fra_SmlStop( pComb ); + printf( "Before: Const = %6d. Class = %6d. ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) ); + // remove nodes from classes whose weight is less than WeightMax/Ratio + k = 0; + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i ) + { + if ( pWeights[pObj->Id] >= WeightMax/Ratio ) + Vec_PtrWriteEntry( p->vClasses1, k++, pObj ); + else + Fra_ClassObjSetRepr( pObj, NULL ); + } + Vec_PtrShrink( p->vClasses1, k ); + // in each class, compact the nodes + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i ) + { + k = 1; + for ( c = 1; ppClass[c]; c++ ) + { + if ( pWeights[ppClass[c]->Id] >= WeightMax/Ratio ) + ppClass[k++] = ppClass[c]; + else + Fra_ClassObjSetRepr( ppClass[c], NULL ); + } + ppClass[k] = NULL; + } + // remove classes with only repr + k = 0; + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i ) + if ( ppClass[1] != NULL ) + Vec_PtrWriteEntry( p->vClasses, k++, ppClass ); + Vec_PtrShrink( p->vClasses, k ); + printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) ); + ABC_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( Aig_Obj_t **, p->vClasses, pClass, i ) + { + // collect support sizes and find the min-support node + cMinSupp = -1; + pNodeMin = NULL; + nSuppSizeMin = ABC_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.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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_ManObjNumMax(p->pAig) * nFramesAll ); + pManFraig->pName = Abc_UtilStrsav( p->pAig->pName ); + pManFraig->pSpec = Abc_UtilStrsav( p->pAig->pSpec ); + // allocate place for the node mapping + ppEquivs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); + 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 = ABC_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++] ); + } + ABC_FREE( pLatches ); + ABC_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; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |