/**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