| /**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_ObjIsCi(pObj) ) |
| continue; |
| } |
| else |
| { |
| if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(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_ObjIsCi(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, 0 ); |
| // 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_ObjCreateCo( 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_ManCiNum(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_ObjCreateCi(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_ObjCreateCi(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_ManCoNum(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_ManCoNum(pManFraig) % nFramesAll == 0 ); |
| printf( "Assert miters = %6d. Output miters = %6d.\n", |
| pManFraig->nAsserts, Aig_ManCoNum(pManFraig) - pManFraig->nAsserts ); |
| // remove dangling nodes |
| Aig_ManCleanup( pManFraig ); |
| return pManFraig; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
