From d401cfa6793a76758917fece545103377f3814ca Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 5 Oct 2005 08:01:00 -0700 Subject: Version abc51005 --- src/base/abci/abcVanEijk.c | 789 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 789 insertions(+) create mode 100644 src/base/abci/abcVanEijk.c (limited to 'src/base/abci/abcVanEijk.c') diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c new file mode 100644 index 00000000..d0179514 --- /dev/null +++ b/src/base/abci/abcVanEijk.c @@ -0,0 +1,789 @@ +/**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 ); +static Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ); +static void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ); +static Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ); +static Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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 ); + + // 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( pNtk, 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; + + 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 ); + Abc_NtkCleanNext(pNtkSingle); + pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 0, 0 ); + if ( fVerbose ) + printf( "The number of ANDs in %d timeframes = %d.\n", nFrames, 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 ); + 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( "\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 ); + if ( fShortNames ) + { + pNtkFrames->pName = util_strsav(pNtk->pName); + pNtkFrames->pSpec = util_strsav(pNtk->pSpec); + } + else + { + sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames + fAddLast ); + pNtkFrames->pName = util_strsav(Buffer); + } + // map the constant nodes + Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkFrames->pManFunc); + // 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 ); + Vec_PtrPush( pNtkFrames->vCis, pLatchNew ); + Vec_PtrPush( pNtkFrames->vCos, pLatchNew ); + Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) ); + pLatch->pNext = NULL; + } + // remove dangling nodes + Abc_AigCleanup( pNtkFrames->pManFunc ); + // 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->pManFunc); + 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->pManFunc)->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 * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pClass, * pNode, * pRepr, * pObj; + Abc_Obj_t * pMiter, * pTotal; + Vec_Ptr_t * vCone; + int i, k; + + // start the network + pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); + pNtkNew->pName = util_strsav("exdc"); + pNtkNew->pSpec = NULL; + + // map the constant nodes + Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc); + // for each CI, create PI + Abc_NtkForEachCi( pNtk, pObj, i ) + Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName( Abc_NtkCi(pNtkInit,i) ) ); + // 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->pManFunc) ); + 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 ); + } + + // 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( Abc_NtkPo(pNtkInit,i) ) ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( Abc_NtkLatch(pNtkInit,i), "_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 /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3