| /**CFile**************************************************************** |
| |
| FileName [abcRr.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Network and node package.] |
| |
| Synopsis [Redundancy removal.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: abcRr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "base/abc/abc.h" |
| #include "proof/fraig/fraig.h" |
| #include "opt/sim/sim.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| typedef struct Abc_RRMan_t_ Abc_RRMan_t; |
| struct Abc_RRMan_t_ |
| { |
| // the parameters |
| Abc_Ntk_t * pNtk; // the network |
| int nFaninLevels; // the number of fanin levels |
| int nFanoutLevels; // the number of fanout levels |
| // the node/fanin/fanout |
| Abc_Obj_t * pNode; // the node |
| Abc_Obj_t * pFanin; // the fanin |
| Abc_Obj_t * pFanout; // the fanout |
| // the intermediate cones |
| Vec_Ptr_t * vFaninLeaves; // the leaves of the fanin cone |
| Vec_Ptr_t * vFanoutRoots; // the roots of the fanout cone |
| // the window |
| Vec_Ptr_t * vLeaves; // the leaves of the window |
| Vec_Ptr_t * vCone; // the internal nodes of the window |
| Vec_Ptr_t * vRoots; // the roots of the window |
| Abc_Ntk_t * pWnd; // the window derived for the edge |
| // the miter |
| Abc_Ntk_t * pMiter; // the miter derived from the window |
| Prove_Params_t * pParams; // the miter proving parameters |
| // statistical variables |
| int nNodesOld; // the old number of nodes |
| int nLevelsOld; // the old number of levels |
| int nEdgesTried; // the number of nodes tried |
| int nEdgesRemoved; // the number of nodes proved |
| abctime timeWindow; // the time to construct the window |
| abctime timeMiter; // the time to construct the miter |
| abctime timeProve; // the time to prove the miter |
| abctime timeUpdate; // the network update time |
| abctime timeTotal; // the total runtime |
| }; |
| |
| static Abc_RRMan_t * Abc_RRManStart(); |
| static void Abc_RRManStop( Abc_RRMan_t * p ); |
| static void Abc_RRManPrintStats( Abc_RRMan_t * p ); |
| static void Abc_RRManClean( Abc_RRMan_t * p ); |
| static int Abc_NtkRRProve( Abc_RRMan_t * p ); |
| static int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Abc_Obj_t * pFanout ); |
| static int Abc_NtkRRWindow( Abc_RRMan_t * p ); |
| |
| static int Abc_NtkRRTfi_int( Vec_Ptr_t * vLeaves, int LevelLimit ); |
| static int Abc_NtkRRTfo_int( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int LevelLimit, Abc_Obj_t * pEdgeFanin, Abc_Obj_t * pEdgeFanout ); |
| static int Abc_NtkRRTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vRoots, int LevelLimit ); |
| static void Abc_NtkRRTfi_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, int LevelLimit ); |
| static Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vRoots ); |
| |
| static void Abc_NtkRRSimulateStart( Abc_Ntk_t * pNtk ); |
| static void Abc_NtkRRSimulateStop( Abc_Ntk_t * pNtk ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Removes stuck-at redundancies.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFanouts, int fVerbose ) |
| { |
| ProgressBar * pProgress; |
| Abc_RRMan_t * p; |
| Abc_Obj_t * pNode, * pFanin, * pFanout; |
| int i, k, m, nNodes, RetValue; |
| abctime clk, clkTotal = Abc_Clock(); |
| // start the manager |
| p = Abc_RRManStart(); |
| p->pNtk = pNtk; |
| p->nFaninLevels = nFaninLevels; |
| p->nFanoutLevels = nFanoutLevels; |
| p->nNodesOld = Abc_NtkNodeNum(pNtk); |
| p->nLevelsOld = Abc_AigLevel(pNtk); |
| // remember latch values |
| // Abc_NtkForEachLatch( pNtk, pNode, i ) |
| // pNode->pNext = pNode->pData; |
| // go through the nodes |
| Abc_NtkCleanCopy(pNtk); |
| nNodes = Abc_NtkObjNumMax(pNtk); |
| Abc_NtkRRSimulateStart(pNtk); |
| pProgress = Extra_ProgressBarStart( stdout, nNodes ); |
| Abc_NtkForEachNode( pNtk, pNode, i ) |
| { |
| Extra_ProgressBarUpdate( pProgress, i, NULL ); |
| // stop if all nodes have been tried once |
| if ( i >= nNodes ) |
| break; |
| // skip the constant node |
| // if ( Abc_NodeIsConst(pNode) ) |
| // continue; |
| // skip persistant nodes |
| if ( Abc_NodeIsPersistant(pNode) ) |
| continue; |
| // skip the nodes with many fanouts |
| if ( Abc_ObjFanoutNum(pNode) > 1000 ) |
| continue; |
| // construct the window |
| if ( !fUseFanouts ) |
| { |
| Abc_ObjForEachFanin( pNode, pFanin, k ) |
| { |
| // skip the nodes with only one fanout (tree nodes) |
| if ( Abc_ObjFanoutNum(pFanin) == 1 ) |
| continue; |
| /* |
| if ( pFanin->Id == 228 && pNode->Id == 2649 ) |
| { |
| int k = 0; |
| } |
| */ |
| p->nEdgesTried++; |
| Abc_RRManClean( p ); |
| p->pNode = pNode; |
| p->pFanin = pFanin; |
| p->pFanout = NULL; |
| |
| clk = Abc_Clock(); |
| RetValue = Abc_NtkRRWindow( p ); |
| p->timeWindow += Abc_Clock() - clk; |
| if ( !RetValue ) |
| continue; |
| /* |
| if ( pFanin->Id == 228 && pNode->Id == 2649 ) |
| { |
| Abc_NtkShowAig( p->pWnd, 0 ); |
| } |
| */ |
| clk = Abc_Clock(); |
| RetValue = Abc_NtkRRProve( p ); |
| p->timeMiter += Abc_Clock() - clk; |
| if ( !RetValue ) |
| continue; |
| //printf( "%d -> %d (%d)\n", pFanin->Id, pNode->Id, k ); |
| |
| clk = Abc_Clock(); |
| Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout ); |
| p->timeUpdate += Abc_Clock() - clk; |
| |
| p->nEdgesRemoved++; |
| break; |
| } |
| continue; |
| } |
| // use the fanouts |
| Abc_ObjForEachFanin( pNode, pFanin, k ) |
| Abc_ObjForEachFanout( pNode, pFanout, m ) |
| { |
| // skip the nodes with only one fanout (tree nodes) |
| // if ( Abc_ObjFanoutNum(pFanin) == 1 && Abc_ObjFanoutNum(pNode) == 1 ) |
| // continue; |
| |
| p->nEdgesTried++; |
| Abc_RRManClean( p ); |
| p->pNode = pNode; |
| p->pFanin = pFanin; |
| p->pFanout = pFanout; |
| |
| clk = Abc_Clock(); |
| RetValue = Abc_NtkRRWindow( p ); |
| p->timeWindow += Abc_Clock() - clk; |
| if ( !RetValue ) |
| continue; |
| |
| clk = Abc_Clock(); |
| RetValue = Abc_NtkRRProve( p ); |
| p->timeMiter += Abc_Clock() - clk; |
| if ( !RetValue ) |
| continue; |
| |
| clk = Abc_Clock(); |
| Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout ); |
| p->timeUpdate += Abc_Clock() - clk; |
| |
| p->nEdgesRemoved++; |
| break; |
| } |
| } |
| Abc_NtkRRSimulateStop(pNtk); |
| Extra_ProgressBarStop( pProgress ); |
| p->timeTotal = Abc_Clock() - clkTotal; |
| if ( fVerbose ) |
| Abc_RRManPrintStats( p ); |
| Abc_RRManStop( p ); |
| // restore latch values |
| // Abc_NtkForEachLatch( pNtk, pNode, i ) |
| // pNode->pData = pNode->pNext, pNode->pNext = NULL; |
| // put the nodes into the DFS order and reassign their IDs |
| Abc_NtkReassignIds( pNtk ); |
| Abc_NtkLevel( pNtk ); |
| // check |
| if ( !Abc_NtkCheck( pNtk ) ) |
| { |
| printf( "Abc_NtkRR: The network check has failed.\n" ); |
| return 0; |
| } |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Start the manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_RRMan_t * Abc_RRManStart() |
| { |
| Abc_RRMan_t * p; |
| p = ABC_ALLOC( Abc_RRMan_t, 1 ); |
| memset( p, 0, sizeof(Abc_RRMan_t) ); |
| p->vFaninLeaves = Vec_PtrAlloc( 100 ); // the leaves of the fanin cone |
| p->vFanoutRoots = Vec_PtrAlloc( 100 ); // the roots of the fanout cone |
| p->vLeaves = Vec_PtrAlloc( 100 ); // the leaves of the window |
| p->vCone = Vec_PtrAlloc( 100 ); // the internal nodes of the window |
| p->vRoots = Vec_PtrAlloc( 100 ); // the roots of the window |
| p->pParams = ABC_ALLOC( Prove_Params_t, 1 ); |
| memset( p->pParams, 0, sizeof(Prove_Params_t) ); |
| Prove_ParamsSetDefault( p->pParams ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Stop the manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_RRManStop( Abc_RRMan_t * p ) |
| { |
| Abc_RRManClean( p ); |
| Vec_PtrFree( p->vFaninLeaves ); |
| Vec_PtrFree( p->vFanoutRoots ); |
| Vec_PtrFree( p->vLeaves ); |
| Vec_PtrFree( p->vCone ); |
| Vec_PtrFree( p->vRoots ); |
| ABC_FREE( p->pParams ); |
| ABC_FREE( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Stop the manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_RRManPrintStats( Abc_RRMan_t * p ) |
| { |
| double Ratio = 100.0*(p->nNodesOld - Abc_NtkNodeNum(p->pNtk))/p->nNodesOld; |
| printf( "Redundancy removal statistics:\n" ); |
| printf( "Edges tried = %6d.\n", p->nEdgesTried ); |
| printf( "Edges removed = %6d. (%5.2f %%)\n", p->nEdgesRemoved, 100.0*p->nEdgesRemoved/p->nEdgesTried ); |
| printf( "Node gain = %6d. (%5.2f %%)\n", p->nNodesOld - Abc_NtkNodeNum(p->pNtk), Ratio ); |
| printf( "Level gain = %6d.\n", p->nLevelsOld - Abc_AigLevel(p->pNtk) ); |
| ABC_PRT( "Windowing ", p->timeWindow ); |
| ABC_PRT( "Miter ", p->timeMiter ); |
| ABC_PRT( " Construct ", p->timeMiter - p->timeProve ); |
| ABC_PRT( " Prove ", p->timeProve ); |
| ABC_PRT( "Update ", p->timeUpdate ); |
| ABC_PRT( "TOTAL ", p->timeTotal ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Clean the manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_RRManClean( Abc_RRMan_t * p ) |
| { |
| p->pNode = NULL; |
| p->pFanin = NULL; |
| p->pFanout = NULL; |
| Vec_PtrClear( p->vFaninLeaves ); |
| Vec_PtrClear( p->vFanoutRoots ); |
| Vec_PtrClear( p->vLeaves ); |
| Vec_PtrClear( p->vCone ); |
| Vec_PtrClear( p->vRoots ); |
| if ( p->pWnd ) Abc_NtkDelete( p->pWnd ); |
| if ( p->pMiter ) Abc_NtkDelete( p->pMiter ); |
| p->pWnd = NULL; |
| p->pMiter = NULL; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if the miter is constant 0.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkRRProve( Abc_RRMan_t * p ) |
| { |
| Abc_Ntk_t * pWndCopy; |
| int RetValue; |
| abctime clk; |
| // Abc_NtkShowAig( p->pWnd, 0 ); |
| pWndCopy = Abc_NtkDup( p->pWnd ); |
| Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL ); |
| if ( !Abc_NtkIsDfsOrdered(pWndCopy) ) |
| Abc_NtkReassignIds(pWndCopy); |
| p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0, 0, 0 ); |
| Abc_NtkDelete( pWndCopy ); |
| clk = Abc_Clock(); |
| RetValue = Abc_NtkMiterProve( &p->pMiter, p->pParams ); |
| p->timeProve += Abc_Clock() - clk; |
| if ( RetValue == 1 ) |
| return 1; |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Updates the network after redundancy removal.] |
| |
| Description [This procedure assumes that non-control value of the fanin |
| was proved redundant. It is okay to concentrate on non-control values |
| because the control values can be seen as redundancy of the fanout edge.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Abc_Obj_t * pFanout ) |
| { |
| Abc_Obj_t * pNodeNew = NULL, * pFanoutNew = NULL; |
| assert( pFanout == NULL ); |
| assert( !Abc_ObjIsComplement(pNode) ); |
| assert( !Abc_ObjIsComplement(pFanin) ); |
| assert( !Abc_ObjIsComplement(pFanout) ); |
| // find the node after redundancy removal |
| if ( pFanin == Abc_ObjFanin0(pNode) ) |
| pNodeNew = Abc_ObjChild1(pNode); |
| else if ( pFanin == Abc_ObjFanin1(pNode) ) |
| pNodeNew = Abc_ObjChild0(pNode); |
| else assert( 0 ); |
| // replace |
| if ( pFanout == NULL ) |
| { |
| Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pNode, pNodeNew, 1 ); |
| return 1; |
| } |
| // find the fanout after redundancy removal |
| if ( pNode == Abc_ObjFanin0(pFanout) ) |
| pFanoutNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC0(pFanout)), Abc_ObjChild1(pFanout) ); |
| else if ( pNode == Abc_ObjFanin1(pFanout) ) |
| pFanoutNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC1(pFanout)), Abc_ObjChild0(pFanout) ); |
| else assert( 0 ); |
| // replace |
| Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pFanout, pFanoutNew, 1 ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Constructs window for checking RR.] |
| |
| Description [If the window (p->pWnd) with the given scope (p->nFaninLevels, |
| p->nFanoutLevels) cannot be constructed, returns 0. Otherwise, returns 1. |
| The levels are measured from the fanin node (pFanin) and the fanout node |
| (pEdgeFanout), respectively.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkRRWindow( Abc_RRMan_t * p ) |
| { |
| Abc_Obj_t * pObj, * pEdgeFanin, * pEdgeFanout; |
| int i, LevelMin, LevelMax, RetValue; |
| |
| // get the edge |
| pEdgeFanout = p->pFanout? p->pFanout : p->pNode; |
| pEdgeFanin = p->pFanout? p->pNode : p->pFanin; |
| // get the minimum and maximum levels of the window |
| LevelMin = Abc_MaxInt( 0, ((int)p->pFanin->Level) - p->nFaninLevels ); |
| LevelMax = (int)pEdgeFanout->Level + p->nFanoutLevels; |
| |
| // start the TFI leaves with the fanin |
| Abc_NtkIncrementTravId( p->pNtk ); |
| Abc_NodeSetTravIdCurrent( p->pFanin ); |
| Vec_PtrPush( p->vFaninLeaves, p->pFanin ); |
| // mark the TFI cone and collect the leaves down to the given level |
| while ( Abc_NtkRRTfi_int(p->vFaninLeaves, LevelMin) ); |
| |
| // mark the leaves with the new TravId |
| Abc_NtkIncrementTravId( p->pNtk ); |
| Vec_PtrForEachEntry( Abc_Obj_t *, p->vFaninLeaves, pObj, i ) |
| Abc_NodeSetTravIdCurrent( pObj ); |
| // traverse the TFO cone of the leaves (while skipping the edge) |
| // (a) mark the nodes in the cone using the current TravId |
| // (b) collect the nodes that have external fanouts into p->vFanoutRoots |
| while ( Abc_NtkRRTfo_int(p->vFaninLeaves, p->vFanoutRoots, LevelMax, pEdgeFanin, pEdgeFanout) ); |
| |
| // mark the fanout roots |
| Vec_PtrForEachEntry( Abc_Obj_t *, p->vFanoutRoots, pObj, i ) |
| pObj->fMarkA = 1; |
| // collect roots reachable from the fanout (p->vRoots) |
| RetValue = Abc_NtkRRTfo_rec( pEdgeFanout, p->vRoots, LevelMax + 1 ); |
| // unmark the fanout roots |
| Vec_PtrForEachEntry( Abc_Obj_t *, p->vFanoutRoots, pObj, i ) |
| pObj->fMarkA = 0; |
| |
| // return if the window is infeasible |
| if ( RetValue == 0 ) |
| return 0; |
| |
| // collect the DFS-ordered new cone (p->vCone) and new leaves (p->vLeaves) |
| // using the previous marks coming from the TFO cone |
| Abc_NtkIncrementTravId( p->pNtk ); |
| Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i ) |
| Abc_NtkRRTfi_rec( pObj, p->vLeaves, p->vCone, LevelMin ); |
| |
| // create a new network |
| p->pWnd = Abc_NtkWindow( p->pNtk, p->vLeaves, p->vCone, p->vRoots ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Marks the nodes in the TFI and collects their leaves.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkRRTfi_int( Vec_Ptr_t * vLeaves, int LevelLimit ) |
| { |
| Abc_Obj_t * pObj, * pNext; |
| int i, k, LevelMax, nSize; |
| assert( LevelLimit >= 0 ); |
| // find the maximum level of leaves |
| LevelMax = 0; |
| Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i ) |
| if ( LevelMax < (int)pObj->Level ) |
| LevelMax = pObj->Level; |
| // if the nodes are all PIs, LevelMax == 0 |
| if ( LevelMax <= LevelLimit ) |
| return 0; |
| // expand the nodes with the minimum level |
| nSize = Vec_PtrSize(vLeaves); |
| Vec_PtrForEachEntryStop( Abc_Obj_t *, vLeaves, pObj, i, nSize ) |
| { |
| if ( LevelMax != (int)pObj->Level ) |
| continue; |
| Abc_ObjForEachFanin( pObj, pNext, k ) |
| { |
| if ( Abc_NodeIsTravIdCurrent(pNext) ) |
| continue; |
| Abc_NodeSetTravIdCurrent( pNext ); |
| Vec_PtrPush( vLeaves, pNext ); |
| } |
| } |
| // remove old nodes (cannot remove a PI) |
| k = 0; |
| Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i ) |
| { |
| if ( LevelMax == (int)pObj->Level ) |
| continue; |
| Vec_PtrWriteEntry( vLeaves, k++, pObj ); |
| } |
| Vec_PtrShrink( vLeaves, k ); |
| if ( Vec_PtrSize(vLeaves) > 2000 ) |
| return 0; |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Marks the nodes in the TFO and collects their roots.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkRRTfo_int( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int LevelLimit, Abc_Obj_t * pEdgeFanin, Abc_Obj_t * pEdgeFanout ) |
| { |
| Abc_Obj_t * pObj, * pNext; |
| int i, k, LevelMin, nSize, fObjIsRoot; |
| // find the minimum level of leaves |
| LevelMin = ABC_INFINITY; |
| Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i ) |
| if ( LevelMin > (int)pObj->Level ) |
| LevelMin = pObj->Level; |
| // if the minimum level exceed the limit, we are done |
| if ( LevelMin > LevelLimit ) |
| return 0; |
| // expand the nodes with the minimum level |
| nSize = Vec_PtrSize(vLeaves); |
| Vec_PtrForEachEntryStop( Abc_Obj_t *, vLeaves, pObj, i, nSize ) |
| { |
| if ( LevelMin != (int)pObj->Level ) |
| continue; |
| fObjIsRoot = 0; |
| Abc_ObjForEachFanout( pObj, pNext, k ) |
| { |
| // check if the fanout is outside of the cone |
| if ( Abc_ObjIsCo(pNext) || pNext->Level > (unsigned)LevelLimit ) |
| { |
| fObjIsRoot = 1; |
| continue; |
| } |
| // skip the edge under check |
| if ( pObj == pEdgeFanin && pNext == pEdgeFanout ) |
| continue; |
| // skip the visited fanouts |
| if ( Abc_NodeIsTravIdCurrent(pNext) ) |
| continue; |
| Abc_NodeSetTravIdCurrent( pNext ); |
| Vec_PtrPush( vLeaves, pNext ); |
| } |
| if ( fObjIsRoot ) |
| Vec_PtrPush( vRoots, pObj ); |
| } |
| // remove old nodes |
| k = 0; |
| Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i ) |
| { |
| if ( LevelMin == (int)pObj->Level ) |
| continue; |
| Vec_PtrWriteEntry( vLeaves, k++, pObj ); |
| } |
| Vec_PtrShrink( vLeaves, k ); |
| if ( Vec_PtrSize(vLeaves) > 2000 ) |
| return 0; |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects the roots in the TFO of the node.] |
| |
| Description [Note that this procedure can be improved by |
| marking and skipping the visited nodes.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkRRTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vRoots, int LevelLimit ) |
| { |
| Abc_Obj_t * pFanout; |
| int i; |
| // if we encountered a node outside of the TFO cone of the fanins, quit |
| if ( Abc_ObjIsCo(pNode) || pNode->Level > (unsigned)LevelLimit ) |
| return 0; |
| // if we encountered a node on the boundary, add it to the roots |
| if ( pNode->fMarkA ) |
| { |
| Vec_PtrPushUnique( vRoots, pNode ); |
| return 1; |
| } |
| // mark the node with the current TravId (needed to have all internal nodes marked) |
| Abc_NodeSetTravIdCurrent( pNode ); |
| // traverse the fanouts |
| Abc_ObjForEachFanout( pNode, pFanout, i ) |
| if ( !Abc_NtkRRTfo_rec( pFanout, vRoots, LevelLimit ) ) |
| return 0; |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects the leaves and cone of the roots.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_NtkRRTfi_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, int LevelLimit ) |
| { |
| Abc_Obj_t * pFanin; |
| int i; |
| // skip visited nodes |
| if ( Abc_NodeIsTravIdCurrent(pNode) ) |
| return; |
| // add node to leaves if it is not in TFI cone of the leaves (marked before) or below the limit |
| if ( !Abc_NodeIsTravIdPrevious(pNode) || (int)pNode->Level <= LevelLimit ) |
| { |
| Abc_NodeSetTravIdCurrent( pNode ); |
| Vec_PtrPush( vLeaves, pNode ); |
| return; |
| } |
| // mark the node as visited |
| Abc_NodeSetTravIdCurrent( pNode ); |
| // call for the node's fanins |
| Abc_ObjForEachFanin( pNode, pFanin, i ) |
| Abc_NtkRRTfi_rec( pFanin, vLeaves, vCone, LevelLimit ); |
| // add the node to the cone in topological order |
| Vec_PtrPush( vCone, pNode ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vRoots ) |
| { |
| Abc_Ntk_t * pNtkNew; |
| Abc_Obj_t * pObj; |
| int fCheck = 1; |
| int i; |
| assert( Abc_NtkIsStrash(pNtk) ); |
| // start the network |
| pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); |
| // duplicate the name and the spec |
| pNtkNew->pName = Extra_UtilStrsav( "temp" ); |
| // map the constant nodes |
| Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); |
| // create and map the PIs |
| Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i ) |
| pObj->pCopy = Abc_NtkCreatePi(pNtkNew); |
| // copy the AND gates |
| Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, i ) |
| pObj->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); |
| // compare the number of nodes before and after |
| if ( Vec_PtrSize(vCone) != Abc_NtkNodeNum(pNtkNew) ) |
| printf( "Warning: Structural hashing during windowing reduced %d nodes (this is a bug).\n", |
| Vec_PtrSize(vCone) - Abc_NtkNodeNum(pNtkNew) ); |
| // create the POs |
| Vec_PtrForEachEntry( Abc_Obj_t *, vRoots, pObj, i ) |
| { |
| assert( !Abc_ObjIsComplement(pObj->pCopy) ); |
| Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pObj->pCopy ); |
| } |
| // add the PI/PO names |
| Abc_NtkAddDummyPiNames( pNtkNew ); |
| Abc_NtkAddDummyPoNames( pNtkNew ); |
| // check |
| if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) |
| { |
| printf( "Abc_NtkWindow: The network check has failed.\n" ); |
| return NULL; |
| } |
| return pNtkNew; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Starts simulation to detect non-redundant edges.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_NtkRRSimulateStart( Abc_Ntk_t * pNtk ) |
| { |
| Abc_Obj_t * pObj; |
| unsigned uData, uData0, uData1; |
| int i; |
| Abc_AigConst1(pNtk)->pData = (void *)~((unsigned)0); |
| Abc_NtkForEachCi( pNtk, pObj, i ) |
| pObj->pData = (void *)(ABC_PTRUINT_T)SIM_RANDOM_UNSIGNED; |
| Abc_NtkForEachNode( pNtk, pObj, i ) |
| { |
| if ( i == 0 ) continue; |
| uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData; |
| uData1 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pData; |
| uData = Abc_ObjFaninC0(pObj)? ~uData0 : uData0; |
| uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1; |
| assert( pObj->pData == NULL ); |
| pObj->pData = (void *)(ABC_PTRUINT_T)uData; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Stops simulation to detect non-redundant edges.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_NtkRRSimulateStop( Abc_Ntk_t * pNtk ) |
| { |
| Abc_Obj_t * pObj; |
| int i; |
| Abc_NtkForEachObj( pNtk, pObj, i ) |
| pObj->pData = NULL; |
| } |
| |
| |
| |
| |
| |
| |
| |
| static void Sim_TraverseNodes_rec( Abc_Obj_t * pRoot, Vec_Str_t * vTargets, Vec_Ptr_t * vNodes ); |
| static void Sim_CollectNodes_rec( Abc_Obj_t * pRoot, Vec_Ptr_t * vField ); |
| static void Sim_SimulateCollected( Vec_Str_t * vTargets, Vec_Ptr_t * vNodes, Vec_Ptr_t * vField ); |
| |
| /**Function************************************************************* |
| |
| Synopsis [Simulation to detect non-redundant edges.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Str_t * Abc_NtkRRSimulate( Abc_Ntk_t * pNtk ) |
| { |
| Vec_Ptr_t * vNodes, * vField; |
| Vec_Str_t * vTargets; |
| Abc_Obj_t * pObj; |
| unsigned uData, uData0, uData1; |
| int PrevCi, Phase, i, k; |
| |
| // start the candidates |
| vTargets = Vec_StrStart( Abc_NtkObjNumMax(pNtk) + 1 ); |
| Abc_NtkForEachNode( pNtk, pObj, i ) |
| { |
| Phase = ((Abc_ObjFanoutNum(Abc_ObjFanin1(pObj)) > 1) << 1); |
| Phase |= (Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) > 1); |
| Vec_StrWriteEntry( vTargets, pObj->Id, (char)Phase ); |
| } |
| |
| // simulate patters and store them in copy |
| Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)~((unsigned)0); |
| Abc_NtkForEachCi( pNtk, pObj, i ) |
| pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)SIM_RANDOM_UNSIGNED; |
| Abc_NtkForEachNode( pNtk, pObj, i ) |
| { |
| if ( i == 0 ) continue; |
| uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData; |
| uData1 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pData; |
| uData = Abc_ObjFaninC0(pObj)? ~uData0 : uData0; |
| uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1; |
| pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)uData; |
| } |
| // store the result in data |
| Abc_NtkForEachCo( pNtk, pObj, i ) |
| { |
| uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData; |
| if ( Abc_ObjFaninC0(pObj) ) |
| pObj->pData = (void *)(ABC_PTRUINT_T)~uData0; |
| else |
| pObj->pData = (void *)(ABC_PTRUINT_T)uData0; |
| } |
| |
| // refine the candidates |
| for ( PrevCi = 0; PrevCi < Abc_NtkCiNum(pNtk); PrevCi = i ) |
| { |
| vNodes = Vec_PtrAlloc( 10 ); |
| Abc_NtkIncrementTravId( pNtk ); |
| for ( i = PrevCi; i < Abc_NtkCiNum(pNtk); i++ ) |
| { |
| Sim_TraverseNodes_rec( Abc_NtkCi(pNtk, i), vTargets, vNodes ); |
| if ( Vec_PtrSize(vNodes) > 128 ) |
| break; |
| } |
| // collect the marked nodes in the topological order |
| vField = Vec_PtrAlloc( 10 ); |
| Abc_NtkIncrementTravId( pNtk ); |
| Abc_NtkForEachCo( pNtk, pObj, k ) |
| Sim_CollectNodes_rec( pObj, vField ); |
| |
| // simulate these nodes |
| Sim_SimulateCollected( vTargets, vNodes, vField ); |
| // prepare for the next loop |
| Vec_PtrFree( vNodes ); |
| } |
| |
| // clean |
| Abc_NtkForEachObj( pNtk, pObj, i ) |
| pObj->pData = NULL; |
| return vTargets; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects nodes starting from the given node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_TraverseNodes_rec( Abc_Obj_t * pRoot, Vec_Str_t * vTargets, Vec_Ptr_t * vNodes ) |
| { |
| Abc_Obj_t * pFanout; |
| char Entry; |
| int k; |
| if ( Abc_NodeIsTravIdCurrent(pRoot) ) |
| return; |
| Abc_NodeSetTravIdCurrent( pRoot ); |
| // save the reached targets |
| Entry = Vec_StrEntry(vTargets, pRoot->Id); |
| if ( Entry & 1 ) |
| Vec_PtrPush( vNodes, Abc_ObjNot(pRoot) ); |
| if ( Entry & 2 ) |
| Vec_PtrPush( vNodes, pRoot ); |
| // explore the fanouts |
| Abc_ObjForEachFanout( pRoot, pFanout, k ) |
| Sim_TraverseNodes_rec( pFanout, vTargets, vNodes ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects nodes starting from the given node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_CollectNodes_rec( Abc_Obj_t * pRoot, Vec_Ptr_t * vField ) |
| { |
| Abc_Obj_t * pFanin; |
| int i; |
| if ( Abc_NodeIsTravIdCurrent(pRoot) ) |
| return; |
| if ( !Abc_NodeIsTravIdPrevious(pRoot) ) |
| return; |
| Abc_NodeSetTravIdCurrent( pRoot ); |
| Abc_ObjForEachFanin( pRoot, pFanin, i ) |
| Sim_CollectNodes_rec( pFanin, vField ); |
| if ( !Abc_ObjIsCo(pRoot) ) |
| pRoot->pData = (void *)(ABC_PTRUINT_T)Vec_PtrSize(vField); |
| Vec_PtrPush( vField, pRoot ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Simulate the given nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_SimulateCollected( Vec_Str_t * vTargets, Vec_Ptr_t * vNodes, Vec_Ptr_t * vField ) |
| { |
| Abc_Obj_t * pObj, * pFanin0, * pFanin1, * pDisproved; |
| Vec_Ptr_t * vSims; |
| unsigned * pUnsigned, * pUnsignedF; |
| int i, k, Phase, fCompl; |
| // get simulation info |
| vSims = Sim_UtilInfoAlloc( Vec_PtrSize(vField), Vec_PtrSize(vNodes), 0 ); |
| // simulate the nodes |
| Vec_PtrForEachEntry( Abc_Obj_t *, vField, pObj, i ) |
| { |
| if ( Abc_ObjIsCi(pObj) ) |
| { |
| pUnsigned = (unsigned *)Vec_PtrEntry( vSims, i ); |
| for ( k = 0; k < Vec_PtrSize(vNodes); k++ ) |
| pUnsigned[k] = (unsigned)(ABC_PTRUINT_T)pObj->pCopy; |
| continue; |
| } |
| if ( Abc_ObjIsCo(pObj) ) |
| { |
| pUnsigned = (unsigned *)Vec_PtrEntry( vSims, i ); |
| pUnsignedF = (unsigned *)Vec_PtrEntry( vSims, (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData ); |
| if ( Abc_ObjFaninC0(pObj) ) |
| for ( k = 0; k < Vec_PtrSize(vNodes); k++ ) |
| pUnsigned[k] = ~pUnsignedF[k]; |
| else |
| for ( k = 0; k < Vec_PtrSize(vNodes); k++ ) |
| pUnsigned[k] = pUnsignedF[k]; |
| // update targets |
| for ( k = 0; k < Vec_PtrSize(vNodes); k++ ) |
| { |
| if ( pUnsigned[k] == (unsigned)(ABC_PTRUINT_T)pObj->pData ) |
| continue; |
| pDisproved = (Abc_Obj_t *)Vec_PtrEntry( vNodes, k ); |
| fCompl = Abc_ObjIsComplement(pDisproved); |
| pDisproved = Abc_ObjRegular(pDisproved); |
| Phase = Vec_StrEntry( vTargets, pDisproved->Id ); |
| if ( fCompl ) |
| Phase = (Phase & 2); |
| else |
| Phase = (Phase & 1); |
| Vec_StrWriteEntry( vTargets, pDisproved->Id, (char)Phase ); |
| } |
| continue; |
| } |
| // simulate the node |
| pFanin0 = Abc_ObjFanin0(pObj); |
| pFanin1 = Abc_ObjFanin1(pObj); |
| } |
| } |
| |
| |
| |
| /* |
| { |
| unsigned uData; |
| if ( pFanin == Abc_ObjFanin0(pNode) ) |
| { |
| uData = (unsigned)Abc_ObjFanin1(pNode)->pData; |
| uData = Abc_ObjFaninC1(pNode)? ~uData : uData; |
| } |
| else if ( pFanin == Abc_ObjFanin1(pNode) ) |
| { |
| uData = (unsigned)Abc_ObjFanin0(pNode)->pData; |
| uData = Abc_ObjFaninC0(pNode)? ~uData : uData; |
| } |
| uData ^= (unsigned)pNode->pData; |
| // Extra_PrintBinary( stdout, &uData, 32 ); printf( "\n" ); |
| if ( Extra_WordCountOnes(uData) > 8 ) |
| continue; |
| } |
| */ |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
