/**CFile**************************************************************** FileName [abcVanEijk.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Network and node package.] Synopsis [Implementation of van Eijk's method for finding signal correspondence: C. A. J. van Eijk. "Sequential equivalence checking based on structural similarities", IEEE Trans. CAD, vol. 19(7), July 2000, pp. 814-819.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - October 2, 2005.] Revision [$Id: abcVanEijk.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "abc.h" #include "fraig.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// static Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ); static Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveBase( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames ); static Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveFirst( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame ); static int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame, Vec_Ptr_t * vClasses ); static void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses ); static int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses ); static void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses ); extern Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ); extern void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ); extern Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ); static Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ); //////////////////////////////////////////////////////////////////////// /// INLINED FUNCTIONS /// //////////////////////////////////////////////////////////////////////// // sets the correspondence of the node in the frame static inline void Abc_NodeVanEijkWriteCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame, Abc_Obj_t * pEntry ) { Vec_PtrWriteEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id, pEntry ); } // returns the correspondence of the node in the frame static inline Abc_Obj_t * Abc_NodeVanEijkReadCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) { return Vec_PtrEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id ); } // returns the hash value of the node in the frame static inline Abc_Obj_t * Abc_NodeVanEijkHash( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) { return Abc_ObjRegular( Abc_NodeVanEijkReadCorresp(pNode, vCorresp, iFrame)->pCopy ); } // returns the representative node of the class to which the node belongs static inline Abc_Obj_t * Abc_NodeVanEijkRepr( Abc_Obj_t * pNode ) { if ( pNode->pNext == NULL ) return NULL; while ( pNode->pNext ) pNode = pNode->pNext; return pNode; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Derives classes of sequentially equivalent nodes.] Description [Performs sequential sweep by combining the equivalent nodes. Adds EXDC network to the current network to record the subset of unreachable states computed by identifying the equivalent nodes.] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ) { Fraig_Params_t Params; Abc_Ntk_t * pNtkSingle; Vec_Ptr_t * vClasses; Abc_Ntk_t * pNtkNew; assert( Abc_NtkIsStrash(pNtk) ); // FRAIG the network to get rid of combinational equivalences Fraig_ParamsSetDefaultFull( &Params ); pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 ); Abc_AigSetNodePhases( pNtkSingle ); Abc_NtkCleanNext(pNtkSingle); // get the equivalence classes vClasses = Abc_NtkVanEijkClasses( pNtkSingle, nFrames, fVerbose ); if ( Vec_PtrSize(vClasses) > 0 ) { // transform the network by merging nodes in the equivalence classes pNtkNew = Abc_NtkVanEijkFrames( pNtkSingle, NULL, 1, 0, 1 ); // pNtkNew = Abc_NtkDup( pNtkSingle ); // derive the EXDC network if asked if ( fExdc ) pNtkNew->pExdc = Abc_NtkVanEijkDeriveExdc( pNtkSingle, vClasses ); } else pNtkNew = Abc_NtkDup( pNtkSingle ); Abc_NtkVanEijkClassesTest( pNtkSingle, vClasses ); Vec_PtrFree( vClasses ); Abc_NtkDelete( pNtkSingle ); return pNtkNew; } /**Function************************************************************* Synopsis [Derives the classes of sequentially equivalent nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVerbose ) { Fraig_Man_t * pFraig; Abc_Ntk_t * pNtkMulti; Vec_Ptr_t * vCorresp, * vClasses; int nIter, RetValue; int nAddFrames = 0; if ( fVerbose ) printf( "The number of ANDs after FRAIGing = %d.\n", Abc_NtkNodeNum(pNtkSingle) ); // get the AIG of the base case vCorresp = Vec_PtrAlloc( 100 ); pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames + nAddFrames, 0, 0 ); if ( fVerbose ) printf( "The number of ANDs in %d timeframes = %d.\n", nFrames + nAddFrames, Abc_NtkNodeNum(pNtkMulti) ); // FRAIG the initialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys) pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 1 ); Fraig_ManFree( pFraig ); // find initial equivalence classes vClasses = Abc_NtkVanEijkClassesDeriveBase( pNtkSingle, vCorresp, nFrames + nAddFrames ); if ( fVerbose ) printf( "The number of classes in the base case = %5d. Pairs = %8d.\n", Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) ); Abc_NtkDelete( pNtkMulti ); // refine the classes using iterative FRAIGing for ( nIter = 1; Vec_PtrSize(vClasses) > 0; nIter++ ) { // derive the network with equivalence classes Abc_NtkVanEijkClassesOrder( vClasses ); pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 1, 0 ); // simulate with classes (TO DO) // FRAIG the unitialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys) pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 0 ); Fraig_ManFree( pFraig ); // refine the classes RetValue = Abc_NtkVanEijkClassesRefine( pNtkSingle, vCorresp, nFrames, vClasses ); Abc_NtkDelete( pNtkMulti ); if ( fVerbose ) printf( "The number of classes after %2d iterations = %5d. Pairs = %8d.\n", nIter, Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) ); // quit if there is no change if ( RetValue == 0 ) break; } Vec_PtrFree( vCorresp ); if ( fVerbose ) { Abc_Obj_t * pObj, * pClass; int i, Counter; printf( "The classes are: " ); Vec_PtrForEachEntry( vClasses, pClass, i ) { Counter = 0; for ( pObj = pClass; pObj; pObj = pObj->pNext ) Counter++; printf( " %d", Counter ); /* printf( " = {" ); for ( pObj = pClass; pObj; pObj = pObj->pNext ) printf( " %d", pObj->Id ); printf( " } " ); */ } printf( "\n" ); } return vClasses; } /**Function************************************************************* Synopsis [Computes the equivalence classes of nodes using the base case.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveBase( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vCorresp, int nFrames ) { Vec_Ptr_t * vClasses; int i, RetValue; // derive the classes for the last frame vClasses = Abc_NtkVanEijkClassesDeriveFirst( pNtkSingle, vCorresp, nFrames - 1 ); // refine the classes using other timeframes for ( i = 0; i < nFrames - 1; i++ ) { if ( Vec_PtrSize(vClasses) == 0 ) break; RetValue = Abc_NtkVanEijkClassesRefine( pNtkSingle, vCorresp, i, vClasses ); // if ( RetValue ) // printf( " yes%s", (i==nFrames-2 ? "\n":"") ); // else // printf( " no%s", (i==nFrames-2 ? "\n":"") ); } return vClasses; } /**Function************************************************************* Synopsis [Computes the equivalence classes of nodes.] Description [Original network (pNtk) is mapped into the unfolded frames using given array of nodes (vCorresp). Each node in the unfolded frames is mapped into a FRAIG node (pNode->pCopy). This procedure uses next pointers (pNode->pNext) to combine the nodes into equivalence classes. Each class is represented by its representative node with the minimum level. Only the last frame is considered.] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveFirst( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame ) { Abc_Obj_t * pNode, * pKey, ** ppSlot; stmm_table * tTable; stmm_generator * gen; Vec_Ptr_t * vClasses; int i; // start the table hashing FRAIG nodes into classes of original network nodes tTable = stmm_init_table( st_ptrcmp, st_ptrhash ); // create the table Abc_NtkCleanNext( pNtk ); Abc_NtkForEachObj( pNtk, pNode, i ) { if ( Abc_ObjIsPo(pNode) ) continue; pKey = Abc_NodeVanEijkHash( pNode, vCorresp, iFrame ); if ( !stmm_find_or_add( tTable, (char *)pKey, (char ***)&ppSlot ) ) *ppSlot = NULL; pNode->pNext = *ppSlot; *ppSlot = pNode; } // collect only non-trivial classes vClasses = Vec_PtrAlloc( 100 ); stmm_foreach_item( tTable, gen, (char **)&pKey, (char **)&pNode ) if ( pNode->pNext ) Vec_PtrPush( vClasses, pNode ); stmm_free_table( tTable ); return vClasses; } /**Function************************************************************* Synopsis [Refines the classes using one frame.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame, Vec_Ptr_t * vClasses ) { Abc_Obj_t * pHeadSame, ** ppTailSame; Abc_Obj_t * pHeadDiff, ** ppTailDiff; Abc_Obj_t * pNode, * pClass, * pKey; int i, k, fChange = 0; Vec_PtrForEachEntry( vClasses, pClass, i ) { // assert( pClass->pNext ); pKey = Abc_NodeVanEijkHash( pClass, vCorresp, iFrame ); for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext ) if ( Abc_NodeVanEijkHash(pNode, vCorresp, iFrame) != pKey ) break; if ( pNode == NULL ) continue; fChange = 1; // create two classes pHeadSame = NULL; ppTailSame = &pHeadSame; pHeadDiff = NULL; ppTailDiff = &pHeadDiff; for ( pNode = pClass; pNode; pNode = pNode->pNext ) if ( Abc_NodeVanEijkHash(pNode, vCorresp, iFrame) != pKey ) *ppTailDiff = pNode, ppTailDiff = &pNode->pNext; else *ppTailSame = pNode, ppTailSame = &pNode->pNext; *ppTailSame = NULL; *ppTailDiff = NULL; assert( pHeadSame && pHeadDiff ); // put the updated class back Vec_PtrWriteEntry( vClasses, i, pHeadSame ); // append the new class to be processed later Vec_PtrPush( vClasses, pHeadDiff ); } // remove trivial classes k = 0; Vec_PtrForEachEntry( vClasses, pClass, i ) if ( pClass->pNext ) Vec_PtrWriteEntry( vClasses, k++, pClass ); Vec_PtrShrink( vClasses, k ); return fChange; } /**Function************************************************************* Synopsis [Orders nodes in the equivalence classes.] Description [Finds a min-level representative of each class and puts it last.] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses ) { Abc_Obj_t * pClass, * pNode, * pPrev, * pNodeMin, * pPrevMin; int i; // go through the classes Vec_PtrForEachEntry( vClasses, pClass, i ) { assert( pClass->pNext ); pPrevMin = NULL; pNodeMin = pClass; for ( pPrev = pClass, pNode = pClass->pNext; pNode; pPrev = pNode, pNode = pNode->pNext ) if ( pNodeMin->Level >= pNode->Level ) { pPrevMin = pPrev; pNodeMin = pNode; } if ( pNodeMin->pNext == NULL ) // already last continue; // update the class if ( pNodeMin == pClass ) Vec_PtrWriteEntry( vClasses, i, pNodeMin->pNext ); else pPrevMin->pNext = pNodeMin->pNext; // attach the min node assert( pPrev->pNext == NULL ); pPrev->pNext = pNodeMin; pNodeMin->pNext = NULL; } Vec_PtrForEachEntry( vClasses, pClass, i ) assert( pClass->pNext ); } /**Function************************************************************* Synopsis [Counts pairs of equivalent nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses ) { Abc_Obj_t * pClass, * pNode; int i, nPairs = 0; Vec_PtrForEachEntry( vClasses, pClass, i ) { assert( pClass->pNext ); for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext ) nPairs++; } return nPairs; } /**Function************************************************************* Synopsis [Sanity check for the class representation.] Description [Checks that pNode->pNext is only used in the classes.] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses ) { Abc_Obj_t * pClass, * pObj; int i; Abc_NtkCleanCopy( pNtkSingle ); Vec_PtrForEachEntry( vClasses, pClass, i ) for ( pObj = pClass; pObj; pObj = pObj->pNext ) if ( pObj->pNext ) pObj->pCopy = (Abc_Obj_t *)1; Abc_NtkForEachObj( pNtkSingle, pObj, i ) assert( (pObj->pCopy != NULL) == (pObj->pNext != NULL) ); Abc_NtkCleanCopy( pNtkSingle ); } /**Function************************************************************* Synopsis [Performs DFS for one node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkVanEijkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) { Abc_Obj_t * pRepr; // skip CI and const if ( Abc_ObjFaninNum(pNode) < 2 ) return; // if this node is already visited, skip if ( Abc_NodeIsTravIdCurrent( pNode ) ) return; // mark the node as visited Abc_NodeSetTravIdCurrent( pNode ); assert( Abc_ObjIsNode( pNode ) ); // check if the node belongs to the class if ( pRepr = Abc_NodeVanEijkRepr(pNode) ) Abc_NtkVanEijkDfs_rec( pRepr, vNodes ); else { Abc_NtkVanEijkDfs_rec( Abc_ObjFanin0(pNode), vNodes ); Abc_NtkVanEijkDfs_rec( Abc_ObjFanin1(pNode), vNodes ); } // add the node after the fanins have been added Vec_PtrPush( vNodes, pNode ); } /**Function************************************************************* Synopsis [Finds DFS ordering of nodes using equivalence classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Ptr_t * Abc_NtkVanEijkDfs( Abc_Ntk_t * pNtk ) { Vec_Ptr_t * vNodes; Abc_Obj_t * pObj; int i; vNodes = Vec_PtrAlloc( 100 ); Abc_NtkIncrementTravId( pNtk ); Abc_NtkForEachCo( pNtk, pObj, i ) Abc_NtkVanEijkDfs_rec( Abc_ObjFanin0(pObj), vNodes ); return vNodes; } /**Function************************************************************* Synopsis [Derives the timeframes of the network.] Description [Returns mapping of the orig nodes into the frame nodes (vCorresp).] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ) { char Buffer[100]; Abc_Ntk_t * pNtkFrames; Abc_Obj_t * pLatch, * pLatchNew; Vec_Ptr_t * vOrder; int i; assert( nFrames > 0 ); assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkIsDfsOrdered(pNtk) ); // clean the array of connections if ( vCorresp ) Vec_PtrFill( vCorresp, (nFrames + fAddLast)*Abc_NtkObjNumMax(pNtk), NULL ); // start the new network pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); if ( fShortNames ) { pNtkFrames->pName = Extra_UtilStrsav(pNtk->pName); pNtkFrames->pSpec = Extra_UtilStrsav(pNtk->pSpec); } else { sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames + fAddLast ); pNtkFrames->pName = Extra_UtilStrsav(Buffer); } // map the constant nodes Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames); // create new latches and remember them in the new latches Abc_NtkForEachLatch( pNtk, pLatch, i ) Abc_NtkDupObj( pNtkFrames, pLatch ); // collect nodes in such a way each class representative goes first vOrder = Abc_NtkVanEijkDfs( pNtk ); // create the timeframes for ( i = 0; i < nFrames; i++ ) Abc_NtkVanEijkAddFrame( pNtkFrames, pNtk, i, vCorresp, vOrder, fShortNames ); Vec_PtrFree( vOrder ); // add one more timeframe without class info if ( fAddLast ) Abc_NtkVanEijkAddFrame( pNtkFrames, pNtk, nFrames, vCorresp, NULL, fShortNames ); // connect the new latches to the outputs of the last frame Abc_NtkForEachLatch( pNtk, pLatch, i ) { pLatchNew = Abc_NtkLatch(pNtkFrames, i); Abc_ObjAddFanin( pLatchNew, pLatch->pCopy ); Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) ); pLatch->pNext = NULL; } // remove dangling nodes // Abc_AigCleanup( pNtkFrames->pManFunc ); // otherwise some external nodes may have dandling pointers // make sure that everything is okay if ( !Abc_NtkCheck( pNtkFrames ) ) printf( "Abc_NtkVanEijkFrames: The network check has failed.\n" ); return pNtkFrames; } /**Function************************************************************* Synopsis [Adds one time frame to the new network.] Description [If the ordering of nodes is given, uses it. Otherwise, uses the DSF order of the nodes in the network.] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ) { char Buffer[10]; Abc_Obj_t * pNode, * pLatch, * pRepr; Vec_Ptr_t * vTemp; int i; // create the prefix to be added to the node names sprintf( Buffer, "_%02d", iFrame ); // add the new PI nodes Abc_NtkForEachPi( pNtk, pNode, i ) { pNode->pCopy = Abc_NtkCreatePi(pNtkFrames); if ( fShortNames ) Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) ); else Abc_NtkLogicStoreNamePlus( pNode->pCopy, Abc_ObjName(pNode), Buffer ); } // remember the CI mapping if ( vCorresp ) { pNode = Abc_AigConst1(pNtk); Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); Abc_NtkForEachCi( pNtk, pNode, i ) Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); } // go through the nodes in the given order or in the natural order if ( vOrder ) { // add the internal nodes Vec_PtrForEachEntry( vOrder, pNode, i ) { if ( pRepr = Abc_NodeVanEijkRepr(pNode) ) pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pNode->fPhase ^ pRepr->fPhase ); else pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); assert( Abc_ObjRegular(pNode->pCopy) != NULL ); if ( vCorresp ) Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); } } else { // add the internal nodes Abc_AigForEachAnd( pNtk, pNode, i ) { pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); assert( Abc_ObjRegular(pNode->pCopy) != NULL ); if ( vCorresp ) Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); } } // add the new POs Abc_NtkForEachPo( pNtk, pNode, i ) { pNode->pCopy = Abc_NtkCreatePo(pNtkFrames); Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) ); if ( fShortNames ) Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) ); else Abc_NtkLogicStoreNamePlus( pNode->pCopy, Abc_ObjName(pNode), Buffer ); } // transfer the implementation of the latch drivers to the latches vTemp = Vec_PtrAlloc( 100 ); Abc_NtkForEachLatch( pNtk, pLatch, i ) Vec_PtrPush( vTemp, Abc_ObjChild0Copy(pLatch) ); Abc_NtkForEachLatch( pNtk, pLatch, i ) pLatch->pCopy = Vec_PtrEntry( vTemp, i ); Vec_PtrFree( vTemp ); Abc_AigForEachAnd( pNtk, pNode, i ) pNode->pCopy = NULL; } /**Function************************************************************* Synopsis [Fraigs the network with or without initialization.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ) { Fraig_Man_t * pMan; Fraig_Params_t Params; ProgressBar * pProgress; Abc_Obj_t * pNode; int i; assert( Abc_NtkIsStrash(pMulti) ); // create the FRAIG manager Fraig_ParamsSetDefaultFull( &Params ); pMan = Fraig_ManCreate( &Params ); // clean the copy fields in the old network Abc_NtkCleanCopy( pMulti ); // map the constant nodes Abc_AigConst1(pMulti)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan); if ( fInit ) { // map the PI nodes Abc_NtkForEachPi( pMulti, pNode, i ) pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i); // map the latches Abc_NtkForEachLatch( pMulti, pNode, i ) pNode->pCopy = (Abc_Obj_t *)Fraig_NotCond( Fraig_ManReadConst1(pMan), !Abc_LatchIsInit1(pNode) ); } else { // map the CI nodes Abc_NtkForEachCi( pMulti, pNode, i ) pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i); } // perform fraiging pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pMulti) ); Abc_AigForEachAnd( pMulti, pNode, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ), Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) ); } Extra_ProgressBarStop( pProgress ); return pMan; } /**Function************************************************************* Synopsis [Create EXDC from the equivalence classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) { Abc_Ntk_t * pNtkNew; Abc_Obj_t * pClass, * pNode, * pRepr, * pObj;//, *pObjNew; Abc_Obj_t * pMiter, * pTotal; Vec_Ptr_t * vCone; int i, k; assert( Abc_NtkIsStrash(pNtk) ); // start the network pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); pNtkNew->pName = Extra_UtilStrsav("exdc"); pNtkNew->pSpec = NULL; // map the constant nodes Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); // for each CI, create PI Abc_NtkForEachCi( pNtk, pObj, i ) Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) ); // cannot add latches here because pLatch->pCopy pointers are used // create the cones for each pair of nodes in an equivalence class pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); Vec_PtrForEachEntry( vClasses, pClass, i ) { assert( pClass->pNext ); // get the cone for the representative node pRepr = Abc_NodeVanEijkRepr( pClass ); if ( Abc_ObjFaninNum(pRepr) == 2 ) { vCone = Abc_NtkDfsNodes( pNtk, &pRepr, 1 ); Vec_PtrForEachEntry( vCone, pObj, k ) pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); Vec_PtrFree( vCone ); assert( pObj == pRepr ); } // go through the node pairs (representative is last in the list) for ( pNode = pClass; pNode != pRepr; pNode = pNode->pNext ) { // get the cone for the node assert( Abc_ObjFaninNum(pNode) == 2 ); vCone = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); Vec_PtrForEachEntry( vCone, pObj, k ) pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); Vec_PtrFree( vCone ); assert( pObj == pNode ); // complement if there is phase difference pNode->pCopy = Abc_ObjNotCond( pNode->pCopy, pNode->fPhase ^ pRepr->fPhase ); // add the miter pMiter = Abc_AigXor( pNtkNew->pManFunc, pRepr->pCopy, pNode->pCopy ); } // add the miter to the final pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter ); } /* // create the only PO pObjNew = Abc_NtkCreatePo( pNtkNew ); // add the PO name Abc_NtkLogicStoreName( pObjNew, "DC" ); // add the PO Abc_ObjAddFanin( pObjNew, pTotal ); // quontify the PIs existentially pNtkNew = Abc_NtkMiterQuantifyPis( pNtkNew ); // get the new PO pObjNew = Abc_NtkPo( pNtkNew, 0 ); // remember the miter output pTotal = Abc_ObjChild0( pObjNew ); // remove the PO Abc_NtkDeleteObj( pObjNew ); // make the old network point to the new things Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); Abc_NtkForEachCi( pNtk, pObj, i ) pObj->pCopy = Abc_NtkPi( pNtkNew, i ); */ // for each CO, create PO (skip POs equal to CIs because of name conflict) Abc_NtkForEachPo( pNtk, pObj, i ) if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pObj) ); Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( pObj, "_in") ); // link to the POs of the network Abc_NtkForEachPo( pNtk, pObj, i ) if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) Abc_ObjAddFanin( pObj->pCopy, pTotal ); Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_ObjAddFanin( pObj->pCopy, pTotal ); // remove the extra nodes Abc_AigCleanup( pNtkNew->pManFunc ); // check the result if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkVanEijkDeriveExdc: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); return NULL; } return pNtkNew; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////