diff options
Diffstat (limited to 'src/opt/res')
| -rw-r--r-- | src/opt/res/module.make | 7 | ||||
| -rw-r--r-- | src/opt/res/res.h | 75 | ||||
| -rw-r--r-- | src/opt/res/resCore.c | 415 | ||||
| -rw-r--r-- | src/opt/res/resDivs.c | 285 | ||||
| -rw-r--r-- | src/opt/res/resFilter.c | 434 | ||||
| -rw-r--r-- | src/opt/res/resInt.h | 137 | ||||
| -rw-r--r-- | src/opt/res/resSat.c | 407 | ||||
| -rw-r--r-- | src/opt/res/resSim.c | 790 | ||||
| -rw-r--r-- | src/opt/res/resSim_old.c | 521 | ||||
| -rw-r--r-- | src/opt/res/resStrash.c | 117 | ||||
| -rw-r--r-- | src/opt/res/resWin.c | 485 | ||||
| -rw-r--r-- | src/opt/res/res_.c | 50 |
12 files changed, 0 insertions, 3723 deletions
diff --git a/src/opt/res/module.make b/src/opt/res/module.make deleted file mode 100644 index 52d8a315..00000000 --- a/src/opt/res/module.make +++ /dev/null @@ -1,7 +0,0 @@ -SRC += src/opt/res/resCore.c \ - src/opt/res/resDivs.c \ - src/opt/res/resFilter.c \ - src/opt/res/resSat.c \ - src/opt/res/resSim.c \ - src/opt/res/resStrash.c \ - src/opt/res/resWin.c diff --git a/src/opt/res/res.h b/src/opt/res/res.h deleted file mode 100644 index 3c3431bf..00000000 --- a/src/opt/res/res.h +++ /dev/null @@ -1,75 +0,0 @@ -/**CFile**************************************************************** - - FileName [res.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Resynthesis package.] - - Synopsis [External declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 15, 2007.] - - Revision [$Id: res.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __RES_H__ -#define __RES_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Res_Par_t_ Res_Par_t; -struct Res_Par_t_ -{ - // general parameters - int nWindow; // window size - int nGrowthLevel; // the maximum allowed growth in level after one iteration of resynthesis - int nSimWords; // the number of simulation words - int nCands; // the number of candidates to try - int fArea; // performs optimization for area - int fDelay; // performs optimization for delay - int fVerbose; // enable basic stats - int fVeryVerbose; // enable detailed stats -}; - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== resCore.c ==========================================================*/ -extern int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars ); - - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c deleted file mode 100644 index 27e9b3ea..00000000 --- a/src/opt/res/resCore.c +++ /dev/null @@ -1,415 +0,0 @@ -/**CFile**************************************************************** - - FileName [resCore.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Resynthesis package.] - - Synopsis [Top-level resynthesis procedure.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 15, 2007.] - - Revision [$Id: resCore.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "resInt.h" -#include "kit.h" -#include "satStore.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Res_Man_t_ Res_Man_t; -struct Res_Man_t_ -{ - // general parameters - Res_Par_t * pPars; - // specialized manager - Res_Win_t * pWin; // windowing manager - Abc_Ntk_t * pAig; // the strashed window - Res_Sim_t * pSim; // simulation manager - Sto_Man_t * pCnf; // the CNF of the SAT problem - Int_Man_t * pMan; // interpolation manager; - Vec_Int_t * vMem; // memory for intermediate SOPs - Vec_Vec_t * vResubs; // resubstitution candidates of the AIG - Vec_Vec_t * vResubsW; // resubstitution candidates of the window - Vec_Vec_t * vLevels; // levelized structure for updating - // statistics - int nWins; // the number of windows tried - int nWinNodes; // the total number of window nodes - int nDivNodes; // the total number of divisors - int nWinsTriv; // the total number of trivial windows - int nWinsUsed; // the total number of useful windows (with at least one candidate) - int nConstsUsed; // the total number of constant nodes under ODC - int nCandSets; // the total number of candidates - int nProvedSets; // the total number of proved groups - int nSimEmpty; // the empty simulation info - int nTotalNets; // the total number of nets - int nTotalNodes; // the total number of nodess - int nTotalNets2; // the total number of nets - int nTotalNodes2; // the total number of nodess - // runtime - int timeWin; // windowing - int timeDiv; // divisors - int timeAig; // strashing - int timeSim; // simulation - int timeCand; // resubstitution candidates - int timeSatTotal; // SAT solving total - int timeSatSat; // SAT solving (sat calls) - int timeSatUnsat; // SAT solving (unsat calls) - int timeSatSim; // SAT solving (simulation) - int timeInt; // interpolation - int timeUpd; // updating - int timeTotal; // total runtime -}; - -extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); - -extern int s_ResynTime; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocate resynthesis manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Res_Man_t * Res_ManAlloc( Res_Par_t * pPars ) -{ - Res_Man_t * p; - p = ALLOC( Res_Man_t, 1 ); - memset( p, 0, sizeof(Res_Man_t) ); - assert( pPars->nWindow > 0 && pPars->nWindow < 100 ); - assert( pPars->nCands > 0 && pPars->nCands < 100 ); - p->pPars = pPars; - p->pWin = Res_WinAlloc(); - p->pSim = Res_SimAlloc( pPars->nSimWords ); - p->pMan = Int_ManAlloc( 512 ); - p->vMem = Vec_IntAlloc( 0 ); - p->vResubs = Vec_VecStart( pPars->nCands ); - p->vResubsW = Vec_VecStart( pPars->nCands ); - p->vLevels = Vec_VecStart( 32 ); - return p; -} - -/**Function************************************************************* - - Synopsis [Deallocate resynthesis manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_ManFree( Res_Man_t * p ) -{ - if ( p->pPars->fVerbose ) - { - printf( "Reduction in nodes = %5d. (%.2f %%) ", - p->nTotalNodes-p->nTotalNodes2, - 100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes ); - printf( "Reduction in edges = %5d. (%.2f %%) ", - p->nTotalNets-p->nTotalNets2, - 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets ); - printf( "\n" ); - - printf( "Winds = %d. ", p->nWins ); - printf( "Nodes = %d. (Ave = %5.1f) ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins ); - printf( "Divs = %d. (Ave = %5.1f) ", p->nDivNodes, 1.0*p->nDivNodes/p->nWins ); - printf( "\n" ); - printf( "WinsTriv = %d. ", p->nWinsTriv ); - printf( "SimsEmpt = %d. ", p->nSimEmpty ); - printf( "Const = %d. ", p->nConstsUsed ); - printf( "WindUsed = %d. ", p->nWinsUsed ); - printf( "Cands = %d. ", p->nCandSets ); - printf( "Proved = %d.", p->nProvedSets ); - printf( "\n" ); - - PRTP( "Windowing ", p->timeWin, p->timeTotal ); - PRTP( "Divisors ", p->timeDiv, p->timeTotal ); - PRTP( "Strashing ", p->timeAig, p->timeTotal ); - PRTP( "Simulation ", p->timeSim, p->timeTotal ); - PRTP( "Candidates ", p->timeCand, p->timeTotal ); - PRTP( "SAT solver ", p->timeSatTotal, p->timeTotal ); - PRTP( " sat ", p->timeSatSat, p->timeTotal ); - PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); - PRTP( " simul ", p->timeSatSim, p->timeTotal ); - PRTP( "Interpol ", p->timeInt, p->timeTotal ); - PRTP( "Undating ", p->timeUpd, p->timeTotal ); - PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); - } - Res_WinFree( p->pWin ); - if ( p->pAig ) Abc_NtkDelete( p->pAig ); - Res_SimFree( p->pSim ); - if ( p->pCnf ) Sto_ManFree( p->pCnf ); - Int_ManFree( p->pMan ); - Vec_IntFree( p->vMem ); - Vec_VecFree( p->vResubs ); - Vec_VecFree( p->vResubsW ); - Vec_VecFree( p->vLevels ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Incrementally updates level of the nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels ) -{ - Abc_Obj_t * pObjNew, * pFanin; - int k; - // create the new node - pObjNew = Abc_NtkCreateNode( pObj->pNtk ); - pObjNew->pData = pFunc; - Vec_PtrForEachEntry( vFanins, pFanin, k ) - Abc_ObjAddFanin( pObjNew, pFanin ); - // replace the old node by the new node - // update the level of the node - Abc_NtkUpdate( pObj, pObjNew, vLevels ); -} - -/**Function************************************************************* - - Synopsis [Entrace into the resynthesis package.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars ) -{ - ProgressBar * pProgress; - Res_Man_t * p; - Abc_Obj_t * pObj; - Hop_Obj_t * pFunc; - Kit_Graph_t * pGraph; - Vec_Ptr_t * vFanins; - unsigned * puTruth; - int i, k, RetValue, nNodesOld, nFanins, nFaninsMax; - int clk, clkTotal = clock(); - - // start the manager - p = Res_ManAlloc( pPars ); - p->nTotalNets = Abc_NtkGetTotalFanins(pNtk); - p->nTotalNodes = Abc_NtkNodeNum(pNtk); - nFaninsMax = Abc_NtkGetFaninMax(pNtk); - - // perform the network sweep - Abc_NtkSweep( pNtk, 0 ); - - // convert into the AIG - if ( !Abc_NtkToAig(pNtk) ) - { - fprintf( stdout, "Converting to BDD has failed.\n" ); - Res_ManFree( p ); - return 0; - } - assert( Abc_NtkHasAig(pNtk) ); - - // set the number of levels - Abc_NtkLevel( pNtk ); - Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel ); - - // try resynthesizing nodes in the topological order - nNodesOld = Abc_NtkObjNumMax(pNtk); - pProgress = Extra_ProgressBarStart( stdout, nNodesOld ); - Abc_NtkForEachObj( pNtk, pObj, i ) - { - Extra_ProgressBarUpdate( pProgress, i, NULL ); - if ( !Abc_ObjIsNode(pObj) ) - continue; - if ( pObj->Id > nNodesOld ) - break; - - // create the window for this node -clk = clock(); - RetValue = Res_WinCompute( pObj, p->pPars->nWindow/10, p->pPars->nWindow%10, p->pWin ); -p->timeWin += clock() - clk; - if ( !RetValue ) - continue; - p->nWinsTriv += Res_WinIsTrivial( p->pWin ); - - if ( p->pPars->fVeryVerbose ) - { - printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level ); - printf( "Win = %3d/%3d/%4d/%3d ", - Vec_PtrSize(p->pWin->vLeaves), - Vec_PtrSize(p->pWin->vBranches), - Vec_PtrSize(p->pWin->vNodes), - Vec_PtrSize(p->pWin->vRoots) ); - } - - // collect the divisors -clk = clock(); - Res_WinDivisors( p->pWin, Abc_ObjRequiredLevel(pObj) - 1 ); -p->timeDiv += clock() - clk; - - p->nWins++; - p->nWinNodes += Vec_PtrSize(p->pWin->vNodes); - p->nDivNodes += Vec_PtrSize( p->pWin->vDivs); - - if ( p->pPars->fVeryVerbose ) - { - printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) ); - printf( "D+ = %3d ", p->pWin->nDivsPlus ); - } - - // create the AIG for the window -clk = clock(); - if ( p->pAig ) Abc_NtkDelete( p->pAig ); - p->pAig = Res_WndStrash( p->pWin ); -p->timeAig += clock() - clk; - - if ( p->pPars->fVeryVerbose ) - { - printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) ); - printf( "\n" ); - } - - // prepare simulation info -clk = clock(); - RetValue = Res_SimPrepare( p->pSim, p->pAig, Vec_PtrSize(p->pWin->vLeaves), 0 ); //p->pPars->fVerbose ); -p->timeSim += clock() - clk; - if ( !RetValue ) - { - p->nSimEmpty++; - continue; - } - - // consider the case of constant node - if ( p->pSim->fConst0 || p->pSim->fConst1 ) - { - p->nConstsUsed++; - - pFunc = p->pSim->fConst1? Hop_ManConst1(pNtk->pManFunc) : Hop_ManConst0(pNtk->pManFunc); - vFanins = Vec_VecEntry( p->vResubsW, 0 ); - Vec_PtrClear( vFanins ); - Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels ); - continue; - } - -// printf( " " ); - - // find resub candidates for the node -clk = clock(); - if ( p->pPars->fArea ) - RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 1 ); - else - RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 0 ); -p->timeCand += clock() - clk; - p->nCandSets += RetValue; - if ( RetValue == 0 ) - continue; - -// printf( "%d(%d) ", Vec_PtrSize(p->pWin->vDivs), RetValue ); - - p->nWinsUsed++; - - // iterate through candidate resubstitutions - Vec_VecForEachLevel( p->vResubs, vFanins, k ) - { - if ( Vec_PtrSize(vFanins) == 0 ) - break; - - // solve the SAT problem and get clauses -clk = clock(); - if ( p->pCnf ) Sto_ManFree( p->pCnf ); - p->pCnf = Res_SatProveUnsat( p->pAig, vFanins ); - if ( p->pCnf == NULL ) - { -p->timeSatSat += clock() - clk; -// printf( " Sat\n" ); -// printf( "-" ); - continue; - } -p->timeSatUnsat += clock() - clk; -// printf( "+" ); - - p->nProvedSets++; -// printf( " Unsat\n" ); -// continue; -// printf( "Proved %d.\n", k ); - - // write it into a file -// Sto_ManDumpClauses( p->pCnf, "trace.cnf" ); - - // interpolate the problem if it was UNSAT -clk = clock(); - nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth ); -p->timeInt += clock() - clk; - if ( nFanins != Vec_PtrSize(vFanins) - 2 ) - continue; - assert( puTruth ); -// Extra_PrintBinary( stdout, puTruth, 1 << nFanins ); printf( "\n" ); - - // transform interpolant into the AIG - pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem ); - - // derive the AIG for the decomposition tree - pFunc = Kit_GraphToHop( pNtk->pManFunc, pGraph ); - Kit_GraphFree( pGraph ); - - // update the network -clk = clock(); - Res_UpdateNetwork( pObj, Vec_VecEntry(p->vResubsW, k), pFunc, p->vLevels ); -p->timeUpd += clock() - clk; - break; - } -// printf( "\n" ); - } - Extra_ProgressBarStop( pProgress ); - Abc_NtkStopReverseLevels( pNtk ); - -p->timeSatSim += p->pSim->timeSat; -p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim; - - p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk); - p->nTotalNodes2 = Abc_NtkNodeNum(pNtk); - - // quit resubstitution manager -p->timeTotal = clock() - clkTotal; - Res_ManFree( p ); - -s_ResynTime += clock() - clkTotal; - // check the resulting network - if ( !Abc_NtkCheck( pNtk ) ) - { - fprintf( stdout, "Abc_NtkResynthesize(): Network check has failed.\n" ); - return 0; - } - return 1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c deleted file mode 100644 index cc75b90f..00000000 --- a/src/opt/res/resDivs.c +++ /dev/null @@ -1,285 +0,0 @@ -/**CFile**************************************************************** - - FileName [resDivs.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Resynthesis package.] - - Synopsis [Collect divisors for the given window.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 15, 2007.] - - Revision [$Id: resDivs.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "resInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Res_WinMarkTfi( Res_Win_t * p ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Adds candidate divisors of the node to its window.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ) -{ - Abc_Obj_t * pObj, * pFanout, * pFanin; - int k, f, m; - - // set the maximum level of the divisors - p->nLevDivMax = nLevDivMax; - - // mark the TFI with the current trav ID - Abc_NtkIncrementTravId( p->pNode->pNtk ); - Res_WinMarkTfi( p ); - - // mark with the current trav ID those nodes that should not be divisors: - // (1) the node and its TFO - // (2) the MFFC of the node - // (3) the node's fanins (these are treated as a special case) - Abc_NtkIncrementTravId( p->pNode->pNtk ); - Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax ); - Res_WinVisitMffc( p->pNode ); - Abc_ObjForEachFanin( p->pNode, pObj, k ) - Abc_NodeSetTravIdCurrent( pObj ); - - // at this point the nodes are marked with two trav IDs: - // nodes to be collected as divisors are marked with previous trav ID - // nodes to be avoided as divisors are marked with current trav ID - - // start collecting the divisors - Vec_PtrClear( p->vDivs ); - Vec_PtrForEachEntry( p->vLeaves, pObj, k ) - { - assert( (int)pObj->Level >= p->nLevLeafMin ); - if ( !Abc_NodeIsTravIdPrevious(pObj) ) - continue; - if ( (int)pObj->Level > p->nLevDivMax ) - continue; - Vec_PtrPush( p->vDivs, pObj ); - } - // add the internal nodes to the data structure - Vec_PtrForEachEntry( p->vNodes, pObj, k ) - { - if ( !Abc_NodeIsTravIdPrevious(pObj) ) - continue; - if ( (int)pObj->Level > p->nLevDivMax ) - continue; - Vec_PtrPush( p->vDivs, pObj ); - } - - // explore the fanouts of already collected divisors - p->nDivsPlus = 0; - Vec_PtrForEachEntry( p->vDivs, pObj, k ) - { - // consider fanouts of this node - Abc_ObjForEachFanout( pObj, pFanout, f ) - { - // stop if there are too many fanouts - if ( f > 20 ) - break; - // skip nodes that are already added - if ( Abc_NodeIsTravIdPrevious(pFanout) ) - continue; - // skip nodes in the TFO or in the MFFC of node - if ( Abc_NodeIsTravIdCurrent(pFanout) ) - continue; - // skip COs - if ( !Abc_ObjIsNode(pFanout) ) - continue; - // skip nodes with large level - if ( (int)pFanout->Level >= p->nLevDivMax ) - continue; - // skip nodes whose fanins are not divisors - Abc_ObjForEachFanin( pFanout, pFanin, m ) - if ( !Abc_NodeIsTravIdPrevious(pFanin) ) - break; - if ( m < Abc_ObjFaninNum(pFanout) ) - continue; - // add the node to the divisors - Vec_PtrPush( p->vDivs, pFanout ); - Vec_PtrPush( p->vNodes, pFanout ); - Abc_NodeSetTravIdPrevious( pFanout ); - p->nDivsPlus++; - } - } -/* - printf( "Node level = %d. ", Abc_ObjLevel(p->pNode) ); - Vec_PtrForEachEntryStart( p->vDivs, pObj, k, Vec_PtrSize(p->vDivs)-p->nDivsPlus ) - printf( "%d ", Abc_ObjLevel(pObj) ); - printf( "\n" ); -*/ -//printf( "%d ", p->nDivsPlus ); -} - -/**Function************************************************************* - - Synopsis [Marks the TFI cone of the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_WinMarkTfi_rec( Res_Win_t * p, Abc_Obj_t * pObj ) -{ - Abc_Obj_t * pFanin; - int i; - if ( Abc_NodeIsTravIdCurrent(pObj) ) - return; - Abc_NodeSetTravIdCurrent( pObj ); - assert( Abc_ObjIsNode(pObj) ); - // visit the fanins of the node - Abc_ObjForEachFanin( pObj, pFanin, i ) - Res_WinMarkTfi_rec( p, pFanin ); -} - -/**Function************************************************************* - - Synopsis [Marks the TFI cone of the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_WinMarkTfi( Res_Win_t * p ) -{ - Abc_Obj_t * pObj; - int i; - // mark the leaves - Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - Abc_NodeSetTravIdCurrent( pObj ); - // start from the node - Res_WinMarkTfi_rec( p, p->pNode ); -} - -/**Function************************************************************* - - Synopsis [Marks the TFO of the collected nodes up to the given level.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit ) -{ - Abc_Obj_t * pFanout; - int i; - if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit ) - return; - if ( Abc_NodeIsTravIdCurrent(pObj) ) - return; - Abc_NodeSetTravIdCurrent( pObj ); - Abc_ObjForEachFanout( pObj, pFanout, i ) - Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit ); -} - -/**Function************************************************************* - - Synopsis [Dereferences the node's MFFC.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_NodeDeref_rec( Abc_Obj_t * pNode ) -{ - Abc_Obj_t * pFanin; - int i, Counter = 1; - if ( Abc_ObjIsCi(pNode) ) - return 0; - Abc_NodeSetTravIdCurrent( pNode ); - Abc_ObjForEachFanin( pNode, pFanin, i ) - { - assert( pFanin->vFanouts.nSize > 0 ); - if ( --pFanin->vFanouts.nSize == 0 ) - Counter += Res_NodeDeref_rec( pFanin ); - } - return Counter; -} - -/**Function************************************************************* - - Synopsis [References the node's MFFC.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_NodeRef_rec( Abc_Obj_t * pNode ) -{ - Abc_Obj_t * pFanin; - int i, Counter = 1; - if ( Abc_ObjIsCi(pNode) ) - return 0; - Abc_ObjForEachFanin( pNode, pFanin, i ) - { - if ( pFanin->vFanouts.nSize++ == 0 ) - Counter += Res_NodeRef_rec( pFanin ); - } - return Counter; -} - -/**Function************************************************************* - - Synopsis [Labels MFFC of the node with the current trav ID.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_WinVisitMffc( Abc_Obj_t * pNode ) -{ - int Count1, Count2; - assert( Abc_ObjIsNode(pNode) ); - // dereference the node (mark with the current trav ID) - Count1 = Res_NodeDeref_rec( pNode ); - // reference it back - Count2 = Res_NodeRef_rec( pNode ); - assert( Count1 == Count2 ); - return Count1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/opt/res/resFilter.c b/src/opt/res/resFilter.c deleted file mode 100644 index f2ca41d3..00000000 --- a/src/opt/res/resFilter.c +++ /dev/null @@ -1,434 +0,0 @@ -/**CFile**************************************************************** - - FileName [resFilter.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Resynthesis package.] - - Synopsis [Filtering resubstitution candidates.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 15, 2007.] - - Revision [$Id: resFilter.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "resInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsigned uMask ); -static int Res_FilterCriticalFanin( Abc_Obj_t * pNode ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Finds sets of feasible candidates.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax, int fArea ) -{ - Abc_Obj_t * pFanin, * pFanin2, * pFaninTemp; - unsigned * pInfo, * pInfoDiv, * pInfoDiv2; - int Counter, RetValue, i, i2, d, d2, iDiv, iDiv2, k; - - // check that the info the node is one - pInfo = Vec_PtrEntry( pSim->vOuts, 1 ); - RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); - if ( RetValue == 0 ) - { -// printf( "Failed 1!\n" ); - return 0; - } - - // collect the fanin info - pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 ); - RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); - if ( RetValue == 0 ) - { -// printf( "Failed 2!\n" ); - return 0; - } - - // try removing each fanin -// printf( "Fanins: " ); - Counter = 0; - Vec_VecClear( vResubs ); - Vec_VecClear( vResubsW ); - Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) - { - if ( fArea && Abc_ObjFanoutNum(pFanin) > 1 ) - continue; - // get simulation info without this fanin - pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) ); - RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); - if ( RetValue ) - { -// printf( "Node %4d. Candidate fanin %4d.\n", pWin->pNode->Id, pFanin->Id ); - // collect the nodes - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); - Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k ) - { - if ( k != i ) - { - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); - Vec_VecPush( vResubsW, Counter, pFaninTemp ); - } - } - Counter++; - if ( Counter == Vec_VecSize(vResubs) ) - return Counter; - } - } - - // try replacing each critical fanin by a non-critical fanin - Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) - { - if ( Abc_ObjFanoutNum(pFanin) > 1 ) - continue; - // get simulation info without this fanin - pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) ); - // go over the set of divisors - for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) - { - pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); - iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); - if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) ) - continue; - // collect the nodes - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); - // collect the remaning fanins and the divisor - Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k ) - { - if ( k != i ) - { - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); - Vec_VecPush( vResubsW, Counter, pFaninTemp ); - } - } - // collect the divisor - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); - Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); - Counter++; - if ( Counter == Vec_VecSize(vResubs) ) - return Counter; - } - } - - // consider the case when two fanins can be added instead of one - if ( Abc_ObjFaninNum(pWin->pNode) < nFaninsMax ) - { - // try to replace each critical fanin by two non-critical fanins - Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) - { - if ( Abc_ObjFanoutNum(pFanin) > 1 ) - continue; - // get simulation info without this fanin - pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) ); - // go over the set of divisors - for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) - { - pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); - iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); - // go through the second divisor - for ( d2 = d + 1; d2 < Abc_NtkPoNum(pAig); d2++ ) - { - pInfoDiv2 = Vec_PtrEntry( pSim->vOuts, d2 ); - iDiv2 = d2 - (Abc_ObjFaninNum(pWin->pNode) + 2); - if ( !Abc_InfoIsOrOne3( pInfo, pInfoDiv, pInfoDiv2, pSim->nWordsOut ) ) - continue; - // collect the nodes - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); - // collect the remaning fanins and the divisor - Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k ) - { - if ( k != i ) - { - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); - Vec_VecPush( vResubsW, Counter, pFaninTemp ); - } - } - // collect the divisor - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d2) ); - Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); - Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv2) ); - Counter++; - if ( Counter == Vec_VecSize(vResubs) ) - return Counter; - } - } - } - } - - // try to replace two nets by one - if ( !fArea ) - { - Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) - { - for ( i2 = i + 1; i2 < Abc_ObjFaninNum(pWin->pNode); i2++ ) - { - pFanin2 = Abc_ObjFanin(pWin->pNode, i2); - // get simulation info without these fanins - pInfo = Res_FilterCollectFaninInfo( pWin, pSim, (~(1 << i)) & (~(1 << i2)) ); - // go over the set of divisors - for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) - { - pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); - iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); - if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) ) - continue; - // collect the nodes - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); - // collect the remaning fanins and the divisor - Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k ) - { - if ( k != i && k != i2 ) - { - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); - Vec_VecPush( vResubsW, Counter, pFaninTemp ); - } - } - // collect the divisor - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); - Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); - Counter++; - if ( Counter == Vec_VecSize(vResubs) ) - return Counter; - } - } - } - } - return Counter; -} - - -/**Function************************************************************* - - Synopsis [Finds sets of feasible candidates.] - - Description [This procedure is a special case of the above.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax ) -{ - Abc_Obj_t * pFanin; - unsigned * pInfo, * pInfoDiv, * pInfoDiv2; - int Counter, RetValue, d, d2, k, iDiv, iDiv2, iBest; - - // check that the info the node is one - pInfo = Vec_PtrEntry( pSim->vOuts, 1 ); - RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); - if ( RetValue == 0 ) - { -// printf( "Failed 1!\n" ); - return 0; - } - - // collect the fanin info - pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 ); - RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); - if ( RetValue == 0 ) - { -// printf( "Failed 2!\n" ); - return 0; - } - - // try removing fanins -// printf( "Fanins: " ); - Counter = 0; - Vec_VecClear( vResubs ); - Vec_VecClear( vResubsW ); - // get the best fanins - iBest = Res_FilterCriticalFanin( pWin->pNode ); - if ( iBest == -1 ) - return 0; - - // get the info without the critical fanin - pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << iBest) ); - RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); - if ( RetValue ) - { -// printf( "Can be done without one!\n" ); - // collect the nodes - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); - Abc_ObjForEachFanin( pWin->pNode, pFanin, k ) - { - if ( k != iBest ) - { - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); - Vec_VecPush( vResubsW, Counter, pFanin ); - } - } - Counter++; -// printf( "*" ); - return Counter; - } - - // go through the divisors - for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) - { - pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); - iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); - if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) ) - continue; -//if ( Abc_ObjLevel(pWin->pNode) <= Abc_ObjLevel( Vec_PtrEntry(pWin->vDivs, iDiv) ) ) -// printf( "Node level = %d. Divisor level = %d.\n", Abc_ObjLevel(pWin->pNode), Abc_ObjLevel( Vec_PtrEntry(pWin->vDivs, iDiv) ) ); - // collect the nodes - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); - // collect the remaning fanins and the divisor - Abc_ObjForEachFanin( pWin->pNode, pFanin, k ) - { - if ( k != iBest ) - { - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); - Vec_VecPush( vResubsW, Counter, pFanin ); - } - } - // collect the divisor - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); - Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); - Counter++; - - if ( Counter == Vec_VecSize(vResubs) ) - break; - } - - if ( Counter > 0 || Abc_ObjFaninNum(pWin->pNode) >= nFaninsMax ) - return Counter; - - // try to find the node pairs - for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) - { - pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); - iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); - // go through the second divisor - for ( d2 = d + 1; d2 < Abc_NtkPoNum(pAig); d2++ ) - { - pInfoDiv2 = Vec_PtrEntry( pSim->vOuts, d2 ); - iDiv2 = d2 - (Abc_ObjFaninNum(pWin->pNode) + 2); - - if ( !Abc_InfoIsOrOne3( pInfo, pInfoDiv, pInfoDiv2, pSim->nWordsOut ) ) - continue; - // collect the nodes - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); - // collect the remaning fanins and the divisor - Abc_ObjForEachFanin( pWin->pNode, pFanin, k ) - { - if ( k != iBest ) - { - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); - Vec_VecPush( vResubsW, Counter, pFanin ); - } - } - // collect the divisor - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d2) ); - Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); - Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv2) ); - Counter++; - - if ( Counter == Vec_VecSize(vResubs) ) - break; - } - if ( Counter == Vec_VecSize(vResubs) ) - break; - } - return Counter; -} - - -/**Function************************************************************* - - Synopsis [Finds sets of feasible candidates.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsigned uMask ) -{ - Abc_Obj_t * pFanin; - unsigned * pInfo; - int i; - pInfo = Vec_PtrEntry( pSim->vOuts, 0 ); - Abc_InfoClear( pInfo, pSim->nWordsOut ); - Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) - { - if ( uMask & (1 << i) ) - Abc_InfoOr( pInfo, Vec_PtrEntry(pSim->vOuts, 2+i), pSim->nWordsOut ); - } - return pInfo; -} - - -/**Function************************************************************* - - Synopsis [Returns the index of the most critical fanin.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_FilterCriticalFanin( Abc_Obj_t * pNode ) -{ - Abc_Obj_t * pFanin; - int i, iBest = -1, CostMax = 0, CostCur; - Abc_ObjForEachFanin( pNode, pFanin, i ) - { - if ( !Abc_ObjIsNode(pFanin) ) - continue; - if ( Abc_ObjFanoutNum(pFanin) > 1 ) - continue; - CostCur = Res_WinVisitMffc( pFanin ); - if ( CostMax < CostCur ) - { - CostMax = CostCur; - iBest = i; - } - } -// if ( CostMax > 0 ) -// printf( "<%d>", CostMax ); - return iBest; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h deleted file mode 100644 index 5aae46cc..00000000 --- a/src/opt/res/resInt.h +++ /dev/null @@ -1,137 +0,0 @@ -/**CFile**************************************************************** - - FileName [resInt.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Resynthesis package.] - - Synopsis [Internal declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 15, 2007.] - - Revision [$Id: resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __RES_INT_H__ -#define __RES_INT_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -#include "res.h" - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Res_Win_t_ Res_Win_t; -struct Res_Win_t_ -{ - // windowing parameters - Abc_Obj_t * pNode; // the node in the center - int nWinTfiMax; // the fanin levels - int nWinTfoMax; // the fanout levels - int nLevDivMax; // the maximum divisor level - // internal windowing parameters - int nFanoutLimit; // the limit on the fanout count of a TFO node (if more, the node is treated as a root) - int nLevTfiMinus; // the number of additional levels to search from TFO below the level of leaves - // derived windowing parameters - int nLevLeafMin; // the minimum level of a leaf - int nLevTravMin; // the minimum level to search from TFO - int nDivsPlus; // the number of additional divisors - // the window data - Vec_Ptr_t * vRoots; // outputs of the window - Vec_Ptr_t * vLeaves; // inputs of the window - Vec_Ptr_t * vBranches; // side nodes of the window - Vec_Ptr_t * vNodes; // internal nodes of the window - Vec_Ptr_t * vDivs; // candidate divisors of the node - // temporary data - Vec_Vec_t * vMatrix; // TFI nodes below the given node -}; - -typedef struct Res_Sim_t_ Res_Sim_t; -struct Res_Sim_t_ -{ - Abc_Ntk_t * pAig; // AIG for simulation - int nTruePis; // the number of true PIs of the window - int fConst0; // the node can be replaced by constant 0 - int fConst1; // the node can be replaced by constant 0 - // simulation parameters - int nWords; // the number of simulation words - int nPats; // the number of patterns - int nWordsIn; // the number of simulation words in the input patterns - int nPatsIn; // the number of patterns in the input patterns - int nBytesIn; // the number of bytes in the input patterns - int nWordsOut; // the number of simulation words in the output patterns - int nPatsOut; // the number of patterns in the output patterns - // simulation info - Vec_Ptr_t * vPats; // input simulation patterns - Vec_Ptr_t * vPats0; // input simulation patterns - Vec_Ptr_t * vPats1; // input simulation patterns - Vec_Ptr_t * vOuts; // output simulation info - int nPats0; // the number of 0-patterns accumulated - int nPats1; // the number of 1-patterns accumulated - // resub candidates - Vec_Vec_t * vCands; // resubstitution candidates - // statistics - int timeSat; -}; - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== resDivs.c ==========================================================*/ -extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ); -extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit ); -extern int Res_WinVisitMffc( Abc_Obj_t * pNode ); -/*=== resFilter.c ==========================================================*/ -extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax, int fArea ); -extern int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax ); -/*=== resSat.c ==========================================================*/ -extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ); -extern int Res_SatSimulate( Res_Sim_t * p, int nPats, int fOnSet ); -/*=== resSim.c ==========================================================*/ -extern Res_Sim_t * Res_SimAlloc( int nWords ); -extern void Res_SimFree( Res_Sim_t * p ); -extern int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose ); -/*=== resStrash.c ==========================================================*/ -extern Abc_Ntk_t * Res_WndStrash( Res_Win_t * p ); -/*=== resWnd.c ==========================================================*/ -extern void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels ); -/*=== resWnd.c ==========================================================*/ -extern Res_Win_t * Res_WinAlloc(); -extern void Res_WinFree( Res_Win_t * p ); -extern int Res_WinIsTrivial( Res_Win_t * p ); -extern int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p ); - - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c deleted file mode 100644 index dd0e7a23..00000000 --- a/src/opt/res/resSat.c +++ /dev/null @@ -1,407 +0,0 @@ -/**CFile**************************************************************** - - FileName [resSat.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Resynthesis package.] - - Synopsis [Interface with the SAT solver.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 15, 2007.] - - Revision [$Id: resSat.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "resInt.h" -#include "hop.h" -#include "satSolver.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -extern int Res_SatAddConst1( sat_solver * pSat, int iVar, int fCompl ); -extern int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl ); -extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Loads AIG into the SAT solver for checking resubstitution.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ) -{ - void * pCnf = NULL; - sat_solver * pSat; - Vec_Ptr_t * vNodes; - Abc_Obj_t * pObj; - int i, nNodes, status; - - // make sure fanins contain POs of the AIG - pObj = Vec_PtrEntry( vFanins, 0 ); - assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) ); - - // collect reachable nodes - vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize ); - - // assign unique numbers to each node - nNodes = 0; - Abc_AigConst1(pAig)->pCopy = (void *)nNodes++; - Abc_NtkForEachPi( pAig, pObj, i ) - pObj->pCopy = (void *)nNodes++; - Vec_PtrForEachEntry( vNodes, pObj, i ) - pObj->pCopy = (void *)nNodes++; - Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs - pObj->pCopy = (void *)nNodes++; - - // start the solver - pSat = sat_solver_new(); - sat_solver_store_alloc( pSat ); - - // add clause for the constant node - Res_SatAddConst1( pSat, (int)Abc_AigConst1(pAig)->pCopy, 0 ); - // add clauses for AND gates - Vec_PtrForEachEntry( vNodes, pObj, i ) - Res_SatAddAnd( pSat, (int)pObj->pCopy, - (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); - Vec_PtrFree( vNodes ); - // add clauses for POs - Vec_PtrForEachEntry( vFanins, pObj, i ) - Res_SatAddEqual( pSat, (int)pObj->pCopy, - (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); - // add trivial clauses - pObj = Vec_PtrEntry(vFanins, 0); - Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set - pObj = Vec_PtrEntry(vFanins, 1); - Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set - - // bookmark the clauses of A - sat_solver_store_mark_clauses_a( pSat ); - - // duplicate the clauses - pObj = Vec_PtrEntry(vFanins, 1); - Sat_SolverDoubleClauses( pSat, (int)pObj->pCopy ); - // add the equality constraints - Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 ) - Res_SatAddEqual( pSat, (int)pObj->pCopy, ((int)pObj->pCopy) + nNodes, 0 ); - - // bookmark the roots - sat_solver_store_mark_roots( pSat ); - - // solve the problem - status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); - if ( status == l_False ) - { - pCnf = sat_solver_store_release( pSat ); -// printf( "unsat\n" ); - } - else if ( status == l_True ) - { -// printf( "sat\n" ); - } - else - { -// printf( "undef\n" ); - } - sat_solver_delete( pSat ); - return pCnf; -} - -/**Function************************************************************* - - Synopsis [Loads AIG into the SAT solver for constrained simulation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, int fOnSet ) -{ - sat_solver * pSat; - Vec_Ptr_t * vFanins; - Vec_Ptr_t * vNodes; - Abc_Obj_t * pObj; - int i, nNodes; - - // start the array - vFanins = Vec_PtrAlloc( 2 ); - pObj = Abc_NtkPo( pAig, 0 ); - Vec_PtrPush( vFanins, pObj ); - pObj = Abc_NtkPo( pAig, 1 ); - Vec_PtrPush( vFanins, pObj ); - - // collect reachable nodes - vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize ); - - // assign unique numbers to each node - nNodes = 0; - Abc_AigConst1(pAig)->pCopy = (void *)nNodes++; - Abc_NtkForEachPi( pAig, pObj, i ) - pObj->pCopy = (void *)nNodes++; - Vec_PtrForEachEntry( vNodes, pObj, i ) - pObj->pCopy = (void *)nNodes++; - Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs - pObj->pCopy = (void *)nNodes++; - - // start the solver - pSat = sat_solver_new(); - - // add clause for the constant node - Res_SatAddConst1( pSat, (int)Abc_AigConst1(pAig)->pCopy, 0 ); - // add clauses for AND gates - Vec_PtrForEachEntry( vNodes, pObj, i ) - Res_SatAddAnd( pSat, (int)pObj->pCopy, - (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); - Vec_PtrFree( vNodes ); - // add clauses for the first PO - pObj = Abc_NtkPo( pAig, 0 ); - Res_SatAddEqual( pSat, (int)pObj->pCopy, - (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); - // add clauses for the second PO - pObj = Abc_NtkPo( pAig, 1 ); - Res_SatAddEqual( pSat, (int)pObj->pCopy, - (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); - - // add trivial clauses - pObj = Abc_NtkPo( pAig, 0 ); - Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set - - pObj = Abc_NtkPo( pAig, 1 ); - Res_SatAddConst1( pSat, (int)pObj->pCopy, !fOnSet ); // on-set - - Vec_PtrFree( vFanins ); - return pSat; -} - -/**Function************************************************************* - - Synopsis [Loads AIG into the SAT solver for constrained simulation.] - - Description [Returns 1 if the required number of patterns are found. - Returns 0 if the solver ran out of time or proved a constant. - In the latter, case one of the flags, fConst0 or fConst1, are set to 1.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet ) -{ - Vec_Int_t * vLits; - Vec_Ptr_t * vPats; - sat_solver * pSat; - int RetValue, i, k, value, status, Lit, Var, iPat; - int clk = clock(); - -//printf( "Looking for %s: ", fOnSet? "onset " : "offset" ); - - // decide what problem should be solved - Lit = toLitCond( (int)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet ); - if ( fOnSet ) - { - iPat = p->nPats1; - vPats = p->vPats1; - } - else - { - iPat = p->nPats0; - vPats = p->vPats0; - } - assert( iPat < nPatsLimit ); - - // derive the SAT solver - pSat = Res_SatSimulateConstr( p->pAig, fOnSet ); - pSat->fSkipSimplify = 1; - status = sat_solver_simplify( pSat ); - if ( status == 0 ) - { - if ( iPat == 0 ) - { -// if ( fOnSet ) -// p->fConst0 = 1; -// else -// p->fConst1 = 1; - RetValue = 0; - } - goto finish; - } - - // enumerate through the SAT assignments - RetValue = 1; - vLits = Vec_IntAlloc( 32 ); - for ( k = iPat; k < nPatsLimit; k++ ) - { - // solve with the assumption -// status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); - status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); - if ( status == l_False ) - { -//printf( "Const %d\n", !fOnSet ); - if ( k == 0 ) - { - if ( fOnSet ) - p->fConst0 = 1; - else - p->fConst1 = 1; - RetValue = 0; - } - break; - } - else if ( status == l_True ) - { - // save the pattern - Vec_IntClear( vLits ); - for ( i = 0; i < p->nTruePis; i++ ) - { - Var = (int)Abc_NtkPi(p->pAig,i)->pCopy; - value = (int)(pSat->model.ptr[Var] == l_True); - if ( value ) - Abc_InfoSetBit( Vec_PtrEntry(vPats, i), k ); - Lit = toLitCond( Var, value ); - Vec_IntPush( vLits, Lit ); -// printf( "%d", value ); - } -// printf( "\n" ); - - status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); - if ( status == 0 ) - { - k++; - RetValue = 1; - break; - } - } - else - { -//printf( "Undecided\n" ); - if ( k == 0 ) - RetValue = 0; - else - RetValue = 1; - break; - } - } - Vec_IntFree( vLits ); -//printf( "Found %d patterns\n", k - iPat ); - - // set the new number of patterns - if ( fOnSet ) - p->nPats1 = k; - else - p->nPats0 = k; - -finish: - - sat_solver_delete( pSat ); -p->timeSat += clock() - clk; - return RetValue; -} - - -/**Function************************************************************* - - Synopsis [Asserts equality of the variable to a constant.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_SatAddConst1( sat_solver * pSat, int iVar, int fCompl ) -{ - lit Lit = toLitCond( iVar, fCompl ); - if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Asserts equality of two variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) -{ - lit Lits[2]; - - Lits[0] = toLitCond( iVar0, 0 ); - Lits[1] = toLitCond( iVar1, !fCompl ); - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) - return 0; - - Lits[0] = toLitCond( iVar0, 1 ); - Lits[1] = toLitCond( iVar1, fCompl ); - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) - return 0; - - return 1; -} - -/**Function************************************************************* - - Synopsis [Adds constraints for the two-input AND-gate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ) -{ - lit Lits[3]; - - Lits[0] = toLitCond( iVar, 1 ); - Lits[1] = toLitCond( iVar0, fCompl0 ); - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) - return 0; - - Lits[0] = toLitCond( iVar, 1 ); - Lits[1] = toLitCond( iVar1, fCompl1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) - return 0; - - Lits[0] = toLitCond( iVar, 0 ); - Lits[1] = toLitCond( iVar0, !fCompl0 ); - Lits[2] = toLitCond( iVar1, !fCompl1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) ) - return 0; - - return 1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c deleted file mode 100644 index 5c1dd2b6..00000000 --- a/src/opt/res/resSim.c +++ /dev/null @@ -1,790 +0,0 @@ -/**CFile**************************************************************** - - FileName [resSim.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Resynthesis package.] - - Synopsis [Simulation engine.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 15, 2007.] - - Revision [$Id: resSim.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "resInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocate simulation engine.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Res_Sim_t * Res_SimAlloc( int nWords ) -{ - Res_Sim_t * p; - p = ALLOC( Res_Sim_t, 1 ); - memset( p, 0, sizeof(Res_Sim_t) ); - // simulation parameters - p->nWords = nWords; - p->nPats = p->nWords * 8 * sizeof(unsigned); - p->nWordsIn = p->nPats; - p->nBytesIn = p->nPats * sizeof(unsigned); - p->nPatsIn = p->nPats * 8 * sizeof(unsigned); - p->nWordsOut = p->nPats * p->nWords; - p->nPatsOut = p->nPats * p->nPats; - // simulation info - p->vPats = Vec_PtrAllocSimInfo( 1024, p->nWordsIn ); - p->vPats0 = Vec_PtrAllocSimInfo( 128, p->nWords ); - p->vPats1 = Vec_PtrAllocSimInfo( 128, p->nWords ); - p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut ); - // resub candidates - p->vCands = Vec_VecStart( 16 ); - return p; -} - -/**Function************************************************************* - - Synopsis [Allocate simulation engine.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis ) -{ - srand( 0xABC ); - - assert( Abc_NtkIsStrash(pAig) ); - p->pAig = pAig; - p->nTruePis = nTruePis; - if ( Vec_PtrSize(p->vPats) < Abc_NtkObjNumMax(pAig)+1 ) - { - Vec_PtrFree( p->vPats ); - p->vPats = Vec_PtrAllocSimInfo( Abc_NtkObjNumMax(pAig)+1, p->nWordsIn ); - } - if ( Vec_PtrSize(p->vPats0) < nTruePis ) - { - Vec_PtrFree( p->vPats0 ); - p->vPats0 = Vec_PtrAllocSimInfo( nTruePis, p->nWords ); - } - if ( Vec_PtrSize(p->vPats1) < nTruePis ) - { - Vec_PtrFree( p->vPats1 ); - p->vPats1 = Vec_PtrAllocSimInfo( nTruePis, p->nWords ); - } - if ( Vec_PtrSize(p->vOuts) < Abc_NtkPoNum(pAig) ) - { - Vec_PtrFree( p->vOuts ); - p->vOuts = Vec_PtrAllocSimInfo( Abc_NtkPoNum(pAig), p->nWordsOut ); - } - // clean storage info for patterns - Abc_InfoClear( Vec_PtrEntry(p->vPats0,0), p->nWords * nTruePis ); - Abc_InfoClear( Vec_PtrEntry(p->vPats1,0), p->nWords * nTruePis ); - p->nPats0 = 0; - p->nPats1 = 0; - p->fConst0 = 0; - p->fConst1 = 0; -} - -/**Function************************************************************* - - Synopsis [Free simulation engine.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimFree( Res_Sim_t * p ) -{ - Vec_PtrFree( p->vPats ); - Vec_PtrFree( p->vPats0 ); - Vec_PtrFree( p->vPats1 ); - Vec_PtrFree( p->vOuts ); - Vec_VecFree( p->vCands ); - free( p ); -} - - -/**Function************************************************************* - - Synopsis [Sets random PI simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_InfoRandomBytes( unsigned * p, int nWords ) -{ - int i, Num; - for ( i = nWords - 1; i >= 0; i-- ) - { - Num = rand(); - p[i] = (Num & 1)? 0xff : 0; - p[i] = (p[i] << 8) | ((Num & 2)? 0xff : 0); - p[i] = (p[i] << 8) | ((Num & 4)? 0xff : 0); - p[i] = (p[i] << 8) | ((Num & 8)? 0xff : 0); - } -// Extra_PrintBinary( stdout, p, 32 ); printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [Sets random PI simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimSetRandomBytes( Res_Sim_t * p ) -{ - Abc_Obj_t * pObj; - unsigned * pInfo; - int i; - Abc_NtkForEachPi( p->pAig, pObj, i ) - { - pInfo = Vec_PtrEntry( p->vPats, pObj->Id ); - if ( i < p->nTruePis ) - Abc_InfoRandomBytes( pInfo, p->nWordsIn ); - else - Abc_InfoRandom( pInfo, p->nWordsIn ); - } -/* - // double-check that all are byte-patterns - Abc_NtkForEachPi( p->pAig, pObj, i ) - { - if ( i == p->nTruePis ) - break; - pInfoC = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id ); - for ( k = 0; k < p->nBytesIn; k++ ) - assert( pInfoC[k] == 0 || pInfoC[k] == 0xff ); - } -*/ -} - -/**Function************************************************************* - - Synopsis [Sets random PI simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimSetDerivedBytes( Res_Sim_t * p, int fUseWalk ) -{ - Vec_Ptr_t * vPatsSource[2]; - int nPatsSource[2]; - Abc_Obj_t * pObj; - unsigned char * pInfo; - int i, k, z, s, nPats; - - // set several random patterns - assert( p->nBytesIn % 32 == 0 ); - nPats = p->nBytesIn/8; - Abc_NtkForEachPi( p->pAig, pObj, i ) - { - if ( i == p->nTruePis ) - break; - Abc_InfoRandomBytes( Vec_PtrEntry(p->vPats, pObj->Id), nPats/4 ); - } - - // set special patterns - if ( fUseWalk ) - { - for ( z = 0; z < 2; z++ ) - { - // set the zero pattern - Abc_NtkForEachPi( p->pAig, pObj, i ) - { - if ( i == p->nTruePis ) - break; - pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id ); - pInfo[nPats] = z ? 0xff : 0; - } - if ( ++nPats == p->nBytesIn ) - return; - // set the walking zero pattern - for ( k = 0; k < p->nTruePis; k++ ) - { - Abc_NtkForEachPi( p->pAig, pObj, i ) - { - if ( i == p->nTruePis ) - break; - pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id ); - pInfo[nPats] = ((i == k) ^ z) ? 0xff : 0; - } - if ( ++nPats == p->nBytesIn ) - return; - } - } - } - - // decide what patterns to set first - if ( p->nPats0 < p->nPats1 ) - { - nPatsSource[0] = p->nPats0; - vPatsSource[0] = p->vPats0; - nPatsSource[1] = p->nPats1; - vPatsSource[1] = p->vPats1; - } - else - { - nPatsSource[0] = p->nPats1; - vPatsSource[0] = p->vPats1; - nPatsSource[1] = p->nPats0; - vPatsSource[1] = p->vPats0; - } - for ( z = 0; z < 2; z++ ) - { - for ( s = nPatsSource[z] - 1; s >= 0; s-- ) - { -// if ( s == 0 ) -// printf( "Patterns:\n" ); - // set the given source pattern - for ( k = 0; k < p->nTruePis; k++ ) - { - Abc_NtkForEachPi( p->pAig, pObj, i ) - { - if ( i == p->nTruePis ) - break; - pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id ); - if ( (i == k) ^ Abc_InfoHasBit( Vec_PtrEntry(vPatsSource[z], i), s ) ) - { - pInfo[nPats] = 0xff; -// if ( s == 0 ) -// printf( "1" ); - } - else - { - pInfo[nPats] = 0; -// if ( s == 0 ) -// printf( "0" ); - } - } -// if ( s == 0 ) -// printf( "\n" ); - if ( ++nPats == p->nBytesIn ) - return; - } - } - } - // clean the rest - for ( z = nPats; z < p->nBytesIn; z++ ) - { - Abc_NtkForEachPi( p->pAig, pObj, i ) - { - if ( i == p->nTruePis ) - break; - pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id ); - memset( pInfo + nPats, 0, p->nBytesIn - nPats ); - } - } -/* - // double-check that all are byte-patterns - Abc_NtkForEachPi( p->pAig, pObj, i ) - { - if ( i == p->nTruePis ) - break; - pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id ); - for ( k = 0; k < p->nBytesIn; k++ ) - assert( pInfo[k] == 0 || pInfo[k] == 0xff ); - } -*/ -} - -/**Function************************************************************* - - Synopsis [Sets given PI simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimSetGiven( Res_Sim_t * p, Vec_Ptr_t * vInfo ) -{ - Abc_Obj_t * pObj; - unsigned * pInfo, * pInfo2; - int i, w; - Abc_NtkForEachPi( p->pAig, pObj, i ) - { - if ( i == p->nTruePis ) - break; - pInfo = Vec_PtrEntry( p->vPats, pObj->Id ); - pInfo2 = Vec_PtrEntry( vInfo, i ); - for ( w = 0; w < p->nWords; w++ ) - pInfo[w] = pInfo2[w]; - } -} - -/**Function************************************************************* - - Synopsis [Simulates one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimPerformOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ) -{ - unsigned * pInfo, * pInfo1, * pInfo2; - int k, fComp1, fComp2; - // simulate the internal nodes - assert( Abc_ObjIsNode(pNode) ); - pInfo = Vec_PtrEntry(vSimInfo, pNode->Id); - pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode)); - pInfo2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode)); - fComp1 = Abc_ObjFaninC0(pNode); - fComp2 = Abc_ObjFaninC1(pNode); - if ( fComp1 && fComp2 ) - for ( k = 0; k < nSimWords; k++ ) - pInfo[k] = ~pInfo1[k] & ~pInfo2[k]; - else if ( fComp1 && !fComp2 ) - for ( k = 0; k < nSimWords; k++ ) - pInfo[k] = ~pInfo1[k] & pInfo2[k]; - else if ( !fComp1 && fComp2 ) - for ( k = 0; k < nSimWords; k++ ) - pInfo[k] = pInfo1[k] & ~pInfo2[k]; - else // if ( fComp1 && fComp2 ) - for ( k = 0; k < nSimWords; k++ ) - pInfo[k] = pInfo1[k] & pInfo2[k]; -} - -/**Function************************************************************* - - Synopsis [Simulates one CO node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimTransferOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ) -{ - unsigned * pInfo, * pInfo1; - int k, fComp1; - // simulate the internal nodes - assert( Abc_ObjIsCo(pNode) ); - pInfo = Vec_PtrEntry(vSimInfo, pNode->Id); - pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode)); - fComp1 = Abc_ObjFaninC0(pNode); - if ( fComp1 ) - for ( k = 0; k < nSimWords; k++ ) - pInfo[k] = ~pInfo1[k]; - else - for ( k = 0; k < nSimWords; k++ ) - pInfo[k] = pInfo1[k]; -} - -/**Function************************************************************* - - Synopsis [Performs one round of simulation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimPerformRound( Res_Sim_t * p, int nWords ) -{ - Abc_Obj_t * pObj; - int i; - Abc_InfoFill( Vec_PtrEntry(p->vPats,0), nWords ); - Abc_AigForEachAnd( p->pAig, pObj, i ) - Res_SimPerformOne( pObj, p->vPats, nWords ); - Abc_NtkForEachPo( p->pAig, pObj, i ) - Res_SimTransferOne( pObj, p->vPats, nWords ); -} - - -/**Function************************************************************* - - Synopsis [Pads the extra space with duplicated simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimPadSimInfo( Vec_Ptr_t * vPats, int nPats, int nWords ) -{ - unsigned * pInfo; - int i, w, iWords; - assert( nPats > 0 && nPats < nWords * 8 * (int) sizeof(unsigned) ); - // pad the first word - if ( nPats < 8 * sizeof(unsigned) ) - { - Vec_PtrForEachEntry( vPats, pInfo, i ) - if ( pInfo[0] & 1 ) - pInfo[0] |= ((~0) << nPats); - nPats = 8 * sizeof(unsigned); - } - // pad the empty words - iWords = nPats / (8 * sizeof(unsigned)); - Vec_PtrForEachEntry( vPats, pInfo, i ) - { - for ( w = iWords; w < nWords; w++ ) - pInfo[w] = pInfo[0]; - } -} - -/**Function************************************************************* - - Synopsis [Duplicates the simulation info to fill the space.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimDeriveInfoReplicate( Res_Sim_t * p ) -{ - unsigned * pInfo, * pInfo2; - Abc_Obj_t * pObj; - int i, j, w; - Abc_NtkForEachPo( p->pAig, pObj, i ) - { - pInfo = Vec_PtrEntry( p->vPats, pObj->Id ); - pInfo2 = Vec_PtrEntry( p->vOuts, i ); - for ( j = 0; j < p->nPats; j++ ) - for ( w = 0; w < p->nWords; w++ ) - *pInfo2++ = pInfo[w]; - } -} - -/**Function************************************************************* - - Synopsis [Complement the simulation info if necessary.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimDeriveInfoComplement( Res_Sim_t * p ) -{ - unsigned * pInfo, * pInfo2; - Abc_Obj_t * pObj; - int i, j, w; - Abc_NtkForEachPo( p->pAig, pObj, i ) - { - pInfo = Vec_PtrEntry( p->vPats, pObj->Id ); - pInfo2 = Vec_PtrEntry( p->vOuts, i ); - for ( j = 0; j < p->nPats; j++, pInfo2 += p->nWords ) - if ( Abc_InfoHasBit( pInfo, j ) ) - for ( w = 0; w < p->nWords; w++ ) - pInfo2[w] = ~pInfo2[w]; - } -} - -/**Function************************************************************* - - Synopsis [Prints output patterns.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig ) -{ - Abc_Obj_t * pObj; - unsigned * pInfo2; - int i; - Abc_NtkForEachPo( pAig, pObj, i ) - { - pInfo2 = Vec_PtrEntry( p->vOuts, i ); - Extra_PrintBinary( stdout, pInfo2, p->nPatsOut ); - printf( "\n" ); - } -} - -/**Function************************************************************* - - Synopsis [Prints output patterns.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimPrintNodePatterns( Res_Sim_t * p, Abc_Ntk_t * pAig ) -{ - unsigned * pInfo; - pInfo = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id ); - Extra_PrintBinary( stdout, pInfo, p->nPats ); - printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [Counts the number of patters of different type.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimCountResults( Res_Sim_t * p, int * pnDcs, int * pnOnes, int * pnZeros, int fVerbose ) -{ - unsigned char * pInfoCare, * pInfoNode; - int i, nTotal = 0; - pInfoCare = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id ); - pInfoNode = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id ); - for ( i = 0; i < p->nBytesIn; i++ ) - { - if ( !pInfoCare[i] ) - (*pnDcs)++; - else if ( !pInfoNode[i] ) - (*pnZeros)++; - else - (*pnOnes)++; - } - nTotal += *pnDcs; - nTotal += *pnZeros; - nTotal += *pnOnes; - if ( fVerbose ) - { - printf( "Dc = %7.2f %% ", 100.0*(*pnDcs) /nTotal ); - printf( "On = %7.2f %% ", 100.0*(*pnOnes) /nTotal ); - printf( "Off = %7.2f %% ", 100.0*(*pnZeros)/nTotal ); - } -} - -/**Function************************************************************* - - Synopsis [Counts the number of patters of different type.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimCollectPatterns( Res_Sim_t * p, int fVerbose ) -{ - Abc_Obj_t * pObj; - unsigned char * pInfoCare, * pInfoNode, * pInfo; - int i, j; - pInfoCare = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id ); - pInfoNode = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id ); - for ( i = 0; i < p->nBytesIn; i++ ) - { - // skip don't-care patterns - if ( !pInfoCare[i] ) - continue; - // separate offset and onset patterns - assert( pInfoNode[i] == 0 || pInfoNode[i] == 0xff ); - if ( !pInfoNode[i] ) - { - if ( p->nPats0 >= p->nPats ) - continue; - Abc_NtkForEachPi( p->pAig, pObj, j ) - { - if ( j == p->nTruePis ) - break; - pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id ); - assert( pInfo[i] == 0 || pInfo[i] == 0xff ); - if ( pInfo[i] ) - Abc_InfoSetBit( Vec_PtrEntry(p->vPats0, j), p->nPats0 ); - } - p->nPats0++; - } - else - { - if ( p->nPats1 >= p->nPats ) - continue; - Abc_NtkForEachPi( p->pAig, pObj, j ) - { - if ( j == p->nTruePis ) - break; - pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id ); - assert( pInfo[i] == 0 || pInfo[i] == 0xff ); - if ( pInfo[i] ) - Abc_InfoSetBit( Vec_PtrEntry(p->vPats1, j), p->nPats1 ); - } - p->nPats1++; - } - if ( p->nPats0 >= p->nPats && p->nPats1 >= p->nPats ) - break; - } - if ( fVerbose ) - { - printf( "| " ); - printf( "On = %3d ", p->nPats1 ); - printf( "Off = %3d ", p->nPats0 ); - printf( "\n" ); - } -} - -/**Function************************************************************* - - Synopsis [Verifies the last pattern.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_SimVerifyValue( Res_Sim_t * p, int fOnSet ) -{ - Abc_Obj_t * pObj; - unsigned * pInfo, * pInfo2; - int i, value; - Abc_NtkForEachPi( p->pAig, pObj, i ) - { - if ( i == p->nTruePis ) - break; - if ( fOnSet ) - { - pInfo2 = Vec_PtrEntry( p->vPats1, i ); - value = Abc_InfoHasBit( pInfo2, p->nPats1 - 1 ); - } - else - { - pInfo2 = Vec_PtrEntry( p->vPats0, i ); - value = Abc_InfoHasBit( pInfo2, p->nPats0 - 1 ); - } - pInfo = Vec_PtrEntry( p->vPats, pObj->Id ); - pInfo[0] = value ? ~0 : 0; - } - Res_SimPerformRound( p, 1 ); - pObj = Abc_NtkPo( p->pAig, 1 ); - pInfo = Vec_PtrEntry( p->vPats, pObj->Id ); - assert( pInfo[0] == 0 || pInfo[0] == ~0 ); - return pInfo[0] > 0; -} - -/**Function************************************************************* - - Synopsis [Prepares simulation info for candidate filtering.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose ) -{ - int i, nOnes = 0, nZeros = 0, nDcs = 0; - if ( fVerbose ) - printf( "\n" ); - // prepare the manager - Res_SimAdjust( p, pAig, nTruePis ); - // estimate the number of patterns - Res_SimSetRandomBytes( p ); - Res_SimPerformRound( p, p->nWordsIn ); - Res_SimCountResults( p, &nDcs, &nOnes, &nZeros, fVerbose ); - // collect the patterns - Res_SimCollectPatterns( p, fVerbose ); - // add more patterns using constraint simulation - if ( p->nPats0 < 8 ) - { - if ( !Res_SatSimulate( p, 16, 0 ) ) - return p->fConst0 || p->fConst1; -// return 0; -// printf( "Value0 = %d\n", Res_SimVerifyValue( p, 0 ) ); - } - if ( p->nPats1 < 8 ) - { - if ( !Res_SatSimulate( p, 16, 1 ) ) - return p->fConst0 || p->fConst1; -// return 0; -// printf( "Value1 = %d\n", Res_SimVerifyValue( p, 1 ) ); - } - // generate additional patterns - for ( i = 0; i < 2; i++ ) - { - if ( p->nPats0 > p->nPats*7/8 && p->nPats1 > p->nPats*7/8 ) - break; - Res_SimSetDerivedBytes( p, i==0 ); - Res_SimPerformRound( p, p->nWordsIn ); - Res_SimCountResults( p, &nDcs, &nOnes, &nZeros, fVerbose ); - Res_SimCollectPatterns( p, fVerbose ); - } - // create bit-matrix info - if ( p->nPats0 < p->nPats ) - Res_SimPadSimInfo( p->vPats0, p->nPats0, p->nWords ); - if ( p->nPats1 < p->nPats ) - Res_SimPadSimInfo( p->vPats1, p->nPats1, p->nWords ); - // resimulate 0-patterns - Res_SimSetGiven( p, p->vPats0 ); - Res_SimPerformRound( p, p->nWords ); -//Res_SimPrintNodePatterns( p, pAig ); - Res_SimDeriveInfoReplicate( p ); - // resimulate 1-patterns - Res_SimSetGiven( p, p->vPats1 ); - Res_SimPerformRound( p, p->nWords ); -//Res_SimPrintNodePatterns( p, pAig ); - Res_SimDeriveInfoComplement( p ); - // print output patterns -// Res_SimPrintOutPatterns( p, pAig ); - return 1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/opt/res/resSim_old.c b/src/opt/res/resSim_old.c deleted file mode 100644 index 23ce29e4..00000000 --- a/src/opt/res/resSim_old.c +++ /dev/null @@ -1,521 +0,0 @@ -/**CFile**************************************************************** - - FileName [resSim.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Resynthesis package.] - - Synopsis [Simulation engine.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 15, 2007.] - - Revision [$Id: resSim.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "resInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocate simulation engine.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Res_Sim_t * Res_SimAlloc( int nWords ) -{ - Res_Sim_t * p; - p = ALLOC( Res_Sim_t, 1 ); - memset( p, 0, sizeof(Res_Sim_t) ); - // simulation parameters - p->nWords = nWords; - p->nPats = 8 * sizeof(unsigned) * p->nWords; - p->nWordsOut = p->nPats * p->nWords; - p->nPatsOut = p->nPats * p->nPats; - // simulation info - p->vPats = Vec_PtrAllocSimInfo( 1024, p->nWords ); - p->vPats0 = Vec_PtrAllocSimInfo( 128, p->nWords ); - p->vPats1 = Vec_PtrAllocSimInfo( 128, p->nWords ); - p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut ); - // resub candidates - p->vCands = Vec_VecStart( 16 ); - return p; -} - -/**Function************************************************************* - - Synopsis [Allocate simulation engine.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig ) -{ - srand( 0xABC ); - - assert( Abc_NtkIsStrash(pAig) ); - p->pAig = pAig; - if ( Vec_PtrSize(p->vPats) < Abc_NtkObjNumMax(pAig)+1 ) - { - Vec_PtrFree( p->vPats ); - p->vPats = Vec_PtrAllocSimInfo( Abc_NtkObjNumMax(pAig)+1, p->nWords ); - } - if ( Vec_PtrSize(p->vPats0) < Abc_NtkPiNum(pAig) ) - { - Vec_PtrFree( p->vPats0 ); - p->vPats0 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords ); - } - if ( Vec_PtrSize(p->vPats1) < Abc_NtkPiNum(pAig) ) - { - Vec_PtrFree( p->vPats1 ); - p->vPats1 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords ); - } - if ( Vec_PtrSize(p->vOuts) < Abc_NtkPoNum(pAig) ) - { - Vec_PtrFree( p->vOuts ); - p->vOuts = Vec_PtrAllocSimInfo( Abc_NtkPoNum(pAig), p->nWordsOut ); - } - // clean storage info for patterns - Abc_InfoClear( Vec_PtrEntry(p->vPats0,0), p->nWords * Abc_NtkPiNum(pAig) ); - Abc_InfoClear( Vec_PtrEntry(p->vPats1,0), p->nWords * Abc_NtkPiNum(pAig) ); - p->nPats0 = 0; - p->nPats1 = 0; -} - -/**Function************************************************************* - - Synopsis [Free simulation engine.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimFree( Res_Sim_t * p ) -{ - Vec_PtrFree( p->vPats ); - Vec_PtrFree( p->vPats0 ); - Vec_PtrFree( p->vPats1 ); - Vec_PtrFree( p->vOuts ); - Vec_VecFree( p->vCands ); - free( p ); -} - - -/**Function************************************************************* - - Synopsis [Sets random PI simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimSetRandom( Res_Sim_t * p ) -{ - Abc_Obj_t * pObj; - unsigned * pInfo; - int i; - Abc_NtkForEachPi( p->pAig, pObj, i ) - { - pInfo = Vec_PtrEntry( p->vPats, pObj->Id ); - Abc_InfoRandom( pInfo, p->nWords ); - } -} - -/**Function************************************************************* - - Synopsis [Sets given PI simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimSetGiven( Res_Sim_t * p, Vec_Ptr_t * vInfo ) -{ - Abc_Obj_t * pObj; - unsigned * pInfo, * pInfo2; - int i, w; - Abc_NtkForEachPi( p->pAig, pObj, i ) - { - pInfo = Vec_PtrEntry( p->vPats, pObj->Id ); - pInfo2 = Vec_PtrEntry( vInfo, i ); - for ( w = 0; w < p->nWords; w++ ) - pInfo[w] = pInfo2[w]; - } -} - -/**Function************************************************************* - - Synopsis [Simulates one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimPerformOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ) -{ - unsigned * pInfo, * pInfo1, * pInfo2; - int k, fComp1, fComp2; - // simulate the internal nodes - assert( Abc_ObjIsNode(pNode) ); - pInfo = Vec_PtrEntry(vSimInfo, pNode->Id); - pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode)); - pInfo2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode)); - fComp1 = Abc_ObjFaninC0(pNode); - fComp2 = Abc_ObjFaninC1(pNode); - if ( fComp1 && fComp2 ) - for ( k = 0; k < nSimWords; k++ ) - pInfo[k] = ~pInfo1[k] & ~pInfo2[k]; - else if ( fComp1 && !fComp2 ) - for ( k = 0; k < nSimWords; k++ ) - pInfo[k] = ~pInfo1[k] & pInfo2[k]; - else if ( !fComp1 && fComp2 ) - for ( k = 0; k < nSimWords; k++ ) - pInfo[k] = pInfo1[k] & ~pInfo2[k]; - else // if ( fComp1 && fComp2 ) - for ( k = 0; k < nSimWords; k++ ) - pInfo[k] = pInfo1[k] & pInfo2[k]; -} - -/**Function************************************************************* - - Synopsis [Simulates one CO node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimTransferOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ) -{ - unsigned * pInfo, * pInfo1; - int k, fComp1; - // simulate the internal nodes - assert( Abc_ObjIsCo(pNode) ); - pInfo = Vec_PtrEntry(vSimInfo, pNode->Id); - pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode)); - fComp1 = Abc_ObjFaninC0(pNode); - if ( fComp1 ) - for ( k = 0; k < nSimWords; k++ ) - pInfo[k] = ~pInfo1[k]; - else - for ( k = 0; k < nSimWords; k++ ) - pInfo[k] = pInfo1[k]; -} - -/**Function************************************************************* - - Synopsis [Performs one round of simulation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimPerformRound( Res_Sim_t * p ) -{ - Abc_Obj_t * pObj; - int i; - Abc_InfoFill( Vec_PtrEntry(p->vPats,0), p->nWords ); - Abc_AigForEachAnd( p->pAig, pObj, i ) - Res_SimPerformOne( pObj, p->vPats, p->nWords ); - Abc_NtkForEachPo( p->pAig, pObj, i ) - Res_SimTransferOne( pObj, p->vPats, p->nWords ); -} - -/**Function************************************************************* - - Synopsis [Processes simulation patterns.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimProcessPats( Res_Sim_t * p ) -{ - Abc_Obj_t * pObj; - unsigned * pInfoCare, * pInfoNode; - int i, j, nDcs = 0; - pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id ); - pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id ); - for ( i = 0; i < p->nPats; i++ ) - { - // skip don't-care patterns - if ( !Abc_InfoHasBit(pInfoCare, i) ) - { - nDcs++; - continue; - } - // separate offset and onset patterns - if ( !Abc_InfoHasBit(pInfoNode, i) ) - { - if ( p->nPats0 >= p->nPats ) - continue; - Abc_NtkForEachPi( p->pAig, pObj, j ) - if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) ) - Abc_InfoSetBit( Vec_PtrEntry(p->vPats0, j), p->nPats0 ); - p->nPats0++; - } - else - { - if ( p->nPats1 >= p->nPats ) - continue; - Abc_NtkForEachPi( p->pAig, pObj, j ) - if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) ) - Abc_InfoSetBit( Vec_PtrEntry(p->vPats1, j), p->nPats1 ); - p->nPats1++; - } - } -} - -/**Function************************************************************* - - Synopsis [Pads the extra space with duplicated simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimPadSimInfo( Vec_Ptr_t * vPats, int nPats, int nWords ) -{ - unsigned * pInfo; - int i, w, iWords; - assert( nPats > 0 && nPats < nWords * 8 * (int) sizeof(unsigned) ); - // pad the first word - if ( nPats < 8 * sizeof(unsigned) ) - { - Vec_PtrForEachEntry( vPats, pInfo, i ) - if ( pInfo[0] & 1 ) - pInfo[0] |= ((~0) << nPats); - nPats = 8 * sizeof(unsigned); - } - // pad the empty words - iWords = nPats / (8 * sizeof(unsigned)); - Vec_PtrForEachEntry( vPats, pInfo, i ) - { - for ( w = iWords; w < nWords; w++ ) - pInfo[w] = pInfo[0]; - } -} - -/**Function************************************************************* - - Synopsis [Duplicates the simulation info to fill the space.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimDeriveInfoReplicate( Res_Sim_t * p ) -{ - unsigned * pInfo, * pInfo2; - Abc_Obj_t * pObj; - int i, j, w; - Abc_NtkForEachPo( p->pAig, pObj, i ) - { - pInfo = Vec_PtrEntry( p->vPats, pObj->Id ); - pInfo2 = Vec_PtrEntry( p->vOuts, i ); - for ( j = 0; j < p->nPats; j++ ) - for ( w = 0; w < p->nWords; w++ ) - *pInfo2++ = pInfo[w]; - } -} - -/**Function************************************************************* - - Synopsis [Complement the simulation info if necessary.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimDeriveInfoComplement( Res_Sim_t * p ) -{ - unsigned * pInfo, * pInfo2; - Abc_Obj_t * pObj; - int i, j, w; - Abc_NtkForEachPo( p->pAig, pObj, i ) - { - pInfo = Vec_PtrEntry( p->vPats, pObj->Id ); - pInfo2 = Vec_PtrEntry( p->vOuts, i ); - for ( j = 0; j < p->nPats; j++, pInfo2 += p->nWords ) - if ( Abc_InfoHasBit( pInfo, j ) ) - for ( w = 0; w < p->nWords; w++ ) - pInfo2[w] = ~pInfo2[w]; - } -} - -/**Function************************************************************* - - Synopsis [Free simulation engine.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimReportOne( Res_Sim_t * p ) -{ - unsigned * pInfoCare, * pInfoNode; - int i, nDcs, nOnes, nZeros; - pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id ); - pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id ); - nDcs = nOnes = nZeros = 0; - for ( i = 0; i < p->nPats; i++ ) - { - // skip don't-care patterns - if ( !Abc_InfoHasBit(pInfoCare, i) ) - { - nDcs++; - continue; - } - // separate offset and onset patterns - if ( !Abc_InfoHasBit(pInfoNode, i) ) - nZeros++; - else - nOnes++; - } - printf( "On = %3d (%7.2f %%) ", nOnes, 100.0*nOnes/p->nPats ); - printf( "Off = %3d (%7.2f %%) ", nZeros, 100.0*nZeros/p->nPats ); - printf( "Dc = %3d (%7.2f %%) ", nDcs, 100.0*nDcs/p->nPats ); - printf( "P0 = %3d ", p->nPats0 ); - printf( "P1 = %3d ", p->nPats1 ); - if ( p->nPats0 < 4 || p->nPats1 < 4 ) - printf( "*" ); - printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [Prints output patterns.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig ) -{ - Abc_Obj_t * pObj; - unsigned * pInfo2; - int i; - Abc_NtkForEachPo( pAig, pObj, i ) - { - pInfo2 = Vec_PtrEntry( p->vOuts, i ); - Extra_PrintBinary( stdout, pInfo2, p->nPatsOut ); - printf( "\n" ); - } -} - -/**Function************************************************************* - - Synopsis [Prepares simulation info for candidate filtering.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose ) -{ - int Limit; - // prepare the manager - Res_SimAdjust( p, pAig ); - // collect 0/1 simulation info - for ( Limit = 0; Limit < 10; Limit++ ) - { - Res_SimSetRandom( p ); - Res_SimPerformRound( p ); - Res_SimProcessPats( p ); - if ( !(p->nPats0 < p->nPats || p->nPats1 < p->nPats) ) - break; - } -// printf( "%d ", Limit ); - // report the last set of patterns -// Res_SimReportOne( p ); -// printf( "\n" ); - // quit if there is not enough -// if ( p->nPats0 < 4 || p->nPats1 < 4 ) - if ( p->nPats0 < 4 || p->nPats1 < 4 ) - { -// Res_SimReportOne( p ); - return 0; - } - // create bit-matrix info - if ( p->nPats0 < p->nPats ) - Res_SimPadSimInfo( p->vPats0, p->nPats0, p->nWords ); - if ( p->nPats1 < p->nPats ) - Res_SimPadSimInfo( p->vPats1, p->nPats1, p->nWords ); - // resimulate 0-patterns - Res_SimSetGiven( p, p->vPats0 ); - Res_SimPerformRound( p ); - Res_SimDeriveInfoReplicate( p ); - // resimulate 1-patterns - Res_SimSetGiven( p, p->vPats1 ); - Res_SimPerformRound( p ); - Res_SimDeriveInfoComplement( p ); - // print output patterns -// Res_SimPrintOutPatterns( p, pAig ); - return 1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/opt/res/resStrash.c b/src/opt/res/resStrash.c deleted file mode 100644 index fde842a4..00000000 --- a/src/opt/res/resStrash.c +++ /dev/null @@ -1,117 +0,0 @@ -/**CFile**************************************************************** - - FileName [resStrash.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Resynthesis package.] - - Synopsis [Structural hashing of the nodes in the window.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 15, 2007.] - - Revision [$Id: resStrash.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "resInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -extern Abc_Obj_t * Abc_ConvertAigToAig( Abc_Ntk_t * pAig, Abc_Obj_t * pObjOld ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Structurally hashes the given window.] - - Description [The first PO is the observability condition. The second - is the node's function. The remaining POs are the candidate divisors.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Res_WndStrash( Res_Win_t * p ) -{ - Vec_Ptr_t * vPairs; - Abc_Ntk_t * pAig; - Abc_Obj_t * pObj, * pMiter; - int i; - assert( Abc_NtkHasAig(p->pNode->pNtk) ); -// Abc_NtkCleanCopy( p->pNode->pNtk ); - // create the network - pAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); - pAig->pName = Extra_UtilStrsav( "window" ); - // create the inputs - Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - pObj->pCopy = Abc_NtkCreatePi( pAig ); - Vec_PtrForEachEntry( p->vBranches, pObj, i ) - pObj->pCopy = Abc_NtkCreatePi( pAig ); - // go through the nodes in the topological order - Vec_PtrForEachEntry( p->vNodes, pObj, i ) - { - pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj ); - if ( pObj == p->pNode ) - pObj->pCopy = Abc_ObjNot( pObj->pCopy ); - } - // collect the POs - vPairs = Vec_PtrAlloc( 2 * Vec_PtrSize(p->vRoots) ); - Vec_PtrForEachEntry( p->vRoots, pObj, i ) - { - Vec_PtrPush( vPairs, pObj->pCopy ); - Vec_PtrPush( vPairs, NULL ); - } - // mark the TFO of the node - Abc_NtkIncrementTravId( p->pNode->pNtk ); - Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax ); - // update strashing of the node - p->pNode->pCopy = Abc_ObjNot( p->pNode->pCopy ); - Abc_NodeSetTravIdPrevious( p->pNode ); - // redo strashing in the TFO - Vec_PtrForEachEntry( p->vNodes, pObj, i ) - { - if ( Abc_NodeIsTravIdCurrent(pObj) ) - pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj ); - } - // collect the POs - Vec_PtrForEachEntry( p->vRoots, pObj, i ) - Vec_PtrWriteEntry( vPairs, 2 * i + 1, pObj->pCopy ); - // add the miter - pMiter = Abc_AigMiter( pAig->pManFunc, vPairs ); - Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pMiter ); - Vec_PtrFree( vPairs ); - // add the node - Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), p->pNode->pCopy ); - // add the fanins - Abc_ObjForEachFanin( p->pNode, pObj, i ) - Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy ); - // add the divisors - Vec_PtrForEachEntry( p->vDivs, pObj, i ) - Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy ); - // add the names - Abc_NtkAddDummyPiNames( pAig ); - Abc_NtkAddDummyPoNames( pAig ); - // check the resulting network - if ( !Abc_NtkCheck( pAig ) ) - fprintf( stdout, "Res_WndStrash(): Network check has failed.\n" ); - return pAig; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c deleted file mode 100644 index a3648925..00000000 --- a/src/opt/res/resWin.c +++ /dev/null @@ -1,485 +0,0 @@ -/**CFile**************************************************************** - - FileName [resWin.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Resynthesis package.] - - Synopsis [Windowing algorithm.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 15, 2007.] - - Revision [$Id: resWin.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "resInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocates the window.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Res_Win_t * Res_WinAlloc() -{ - Res_Win_t * p; - // start the manager - p = ALLOC( Res_Win_t, 1 ); - memset( p, 0, sizeof(Res_Win_t) ); - // set internal parameters - p->nFanoutLimit = 10; - p->nLevTfiMinus = 3; - // allocate storage - p->vRoots = Vec_PtrAlloc( 256 ); - p->vLeaves = Vec_PtrAlloc( 256 ); - p->vBranches = Vec_PtrAlloc( 256 ); - p->vNodes = Vec_PtrAlloc( 256 ); - p->vDivs = Vec_PtrAlloc( 256 ); - p->vMatrix = Vec_VecStart( 128 ); - return p; -} - -/**Function************************************************************* - - Synopsis [Frees the window.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_WinFree( Res_Win_t * p ) -{ - Vec_PtrFree( p->vRoots ); - Vec_PtrFree( p->vLeaves ); - Vec_PtrFree( p->vBranches ); - Vec_PtrFree( p->vNodes ); - Vec_PtrFree( p->vDivs ); - Vec_VecFree( p->vMatrix ); - free( p ); -} - - - -/**Function************************************************************* - - Synopsis [Collect the limited TFI cone of the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_WinCollectLeavesAndNodes( Res_Win_t * p ) -{ - Vec_Ptr_t * vFront; - Abc_Obj_t * pObj, * pTemp; - int i, k, m; - - assert( p->nWinTfiMax > 0 ); - assert( Vec_VecSize(p->vMatrix) > p->nWinTfiMax ); - - // start matrix with the node - Vec_VecClear( p->vMatrix ); - Vec_VecPush( p->vMatrix, 0, p->pNode ); - Abc_NtkIncrementTravId( p->pNode->pNtk ); - Abc_NodeSetTravIdCurrent( p->pNode ); - - // collect the leaves (nodes pTemp such that "p->pNode->Level - pTemp->Level > p->nWinTfiMax") - Vec_PtrClear( p->vLeaves ); - Vec_VecForEachLevelStartStop( p->vMatrix, vFront, i, 0, p->nWinTfiMax ) - { - Vec_PtrForEachEntry( vFront, pObj, k ) - { - Abc_ObjForEachFanin( pObj, pTemp, m ) - { - if ( Abc_NodeIsTravIdCurrent( pTemp ) ) - continue; - Abc_NodeSetTravIdCurrent( pTemp ); - if ( Abc_ObjIsCi(pTemp) || (int)(p->pNode->Level - pTemp->Level) > p->nWinTfiMax ) - Vec_PtrPush( p->vLeaves, pTemp ); - else - Vec_VecPush( p->vMatrix, p->pNode->Level - pTemp->Level, pTemp ); - } - } - } - if ( Vec_PtrSize(p->vLeaves) == 0 ) - return 0; - - // collect the nodes in the reverse order - Vec_PtrClear( p->vNodes ); - Vec_VecForEachLevelReverseStartStop( p->vMatrix, vFront, i, p->nWinTfiMax, 0 ) - { - Vec_PtrForEachEntry( vFront, pObj, k ) - Vec_PtrPush( p->vNodes, pObj ); - Vec_PtrClear( vFront ); - } - - // get the lowest leaf level - p->nLevLeafMin = ABC_INFINITY; - Vec_PtrForEachEntry( p->vLeaves, pObj, k ) - p->nLevLeafMin = ABC_MIN( p->nLevLeafMin, (int)pObj->Level ); - - // set minimum traversal level - p->nLevTravMin = ABC_MAX( ((int)p->pNode->Level) - p->nWinTfiMax - p->nLevTfiMinus, p->nLevLeafMin ); - assert( p->nLevTravMin >= 0 ); - return 1; -} - - - -/**Function************************************************************* - - Synopsis [Returns 1 if the node should be a root.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Res_WinComputeRootsCheck( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit ) -{ - Abc_Obj_t * pFanout; - int i; - // the node is the root if one of the following is true: - // (1) the node has more than fanouts than the limit - if ( Abc_ObjFanoutNum(pNode) > nFanoutLimit ) - return 1; - // (2) the node has CO fanouts - // (3) the node has fanouts above the cutoff level - Abc_ObjForEachFanout( pNode, pFanout, i ) - if ( Abc_ObjIsCo(pFanout) || (int)pFanout->Level > nLevelMax ) - return 1; - return 0; -} - -/**Function************************************************************* - - Synopsis [Recursively collects the root candidates.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_WinComputeRoots_rec( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots ) -{ - Abc_Obj_t * pFanout; - int i; - assert( Abc_ObjIsNode(pNode) ); - if ( Abc_NodeIsTravIdCurrent(pNode) ) - return; - Abc_NodeSetTravIdCurrent( pNode ); - // check if the node should be the root - if ( Res_WinComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) ) - Vec_PtrPush( vRoots, pNode ); - else // if not, explore its fanouts - Abc_ObjForEachFanout( pNode, pFanout, i ) - Res_WinComputeRoots_rec( pFanout, nLevelMax, nFanoutLimit, vRoots ); -} - -/**Function************************************************************* - - Synopsis [Recursively collects the root candidates.] - - Description [Returns 1 if the only root is this node.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_WinComputeRoots( Res_Win_t * p ) -{ - Vec_PtrClear( p->vRoots ); - Abc_NtkIncrementTravId( p->pNode->pNtk ); - Res_WinComputeRoots_rec( p->pNode, p->pNode->Level + p->nWinTfoMax, p->nFanoutLimit, p->vRoots ); - assert( Vec_PtrSize(p->vRoots) > 0 ); - if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode ) - return 0; - return 1; -} - - - -/**Function************************************************************* - - Synopsis [Marks the paths from the roots to the leaves.] - - Description [Returns 1 if the the node can reach a leaf.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_WinMarkPaths_rec( Abc_Obj_t * pNode, Abc_Obj_t * pPivot, int nLevelMin ) -{ - Abc_Obj_t * pFanin; - int i, RetValue; - // skip visited nodes - if ( Abc_NodeIsTravIdCurrent(pNode) ) - return 1; - if ( Abc_NodeIsTravIdPrevious(pNode) ) - return 0; - // assume that the node does not have access to the leaves - Abc_NodeSetTravIdPrevious( pNode ); - // skip nodes below the given level - if ( pNode == pPivot || (int)pNode->Level <= nLevelMin ) - return 0; - assert( Abc_ObjIsNode(pNode) ); - // check if the fanins have access to the leaves - RetValue = 0; - Abc_ObjForEachFanin( pNode, pFanin, i ) - RetValue |= Res_WinMarkPaths_rec( pFanin, pPivot, nLevelMin ); - // relabel the node if it has access to the leaves - if ( RetValue ) - Abc_NodeSetTravIdCurrent( pNode ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Marks the paths from the roots to the leaves.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_WinMarkPaths( Res_Win_t * p ) -{ - Abc_Obj_t * pObj; - int i; - // mark the leaves - Abc_NtkIncrementTravId( p->pNode->pNtk ); - Abc_NtkIncrementTravId( p->pNode->pNtk ); - Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - Abc_NodeSetTravIdCurrent( pObj ); - // traverse from the roots and mark the nodes that can reach leaves - // the nodes that do not reach leaves have previous trav ID - // the nodes that reach leaves have current trav ID - Vec_PtrForEachEntry( p->vRoots, pObj, i ) - Res_WinMarkPaths_rec( pObj, p->pNode, p->nLevTravMin ); -} - - - - -/**Function************************************************************* - - Synopsis [Recursively collects the roots.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_WinFinalizeRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots ) -{ - Abc_Obj_t * pFanout; - int i; - assert( Abc_ObjIsNode(pObj) ); - assert( Abc_NodeIsTravIdCurrent(pObj) ); - // check if the node has all fanouts marked - Abc_ObjForEachFanout( pObj, pFanout, i ) - if ( !Abc_NodeIsTravIdCurrent(pFanout) ) - break; - // if some of the fanouts are unmarked, add the node to the roots - if ( i < Abc_ObjFanoutNum(pObj) ) - Vec_PtrPushUnique( vRoots, pObj ); - else // otherwise, call recursively - Abc_ObjForEachFanout( pObj, pFanout, i ) - Res_WinFinalizeRoots_rec( pFanout, vRoots ); -} - -/**Function************************************************************* - - Synopsis [Finalizes the roots of the window.] - - Description [Roots of the window are the nodes that have at least - one fanout that it not in the TFO of the leaves.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_WinFinalizeRoots( Res_Win_t * p ) -{ - assert( !Abc_NodeIsTravIdCurrent(p->pNode) ); - // mark the node with the old traversal ID - Abc_NodeSetTravIdCurrent( p->pNode ); - // recollect the roots - Vec_PtrClear( p->vRoots ); - Res_WinFinalizeRoots_rec( p->pNode, p->vRoots ); - assert( Vec_PtrSize(p->vRoots) > 0 ); - if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode ) - return 0; - return 1; -} - - -/**Function************************************************************* - - Synopsis [Recursively adds missing nodes and leaves.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj, int nLevTravMin ) -{ - Abc_Obj_t * pFanin; - int i; - // skip the already collected leaves, nodes, and branches - if ( Abc_NodeIsTravIdCurrent(pObj) ) - return; - // if this is not an internal node - make it a new branch - if ( !Abc_NodeIsTravIdPrevious(pObj) ) - { - assert( Vec_PtrFind(p->vLeaves, pObj) == -1 ); - Abc_NodeSetTravIdCurrent( pObj ); - Vec_PtrPush( p->vBranches, pObj ); - return; - } - assert( Abc_ObjIsNode(pObj) ); // if this is a CI, then the window is incorrect! - Abc_NodeSetTravIdCurrent( pObj ); - // visit the fanins of the node - Abc_ObjForEachFanin( pObj, pFanin, i ) - Res_WinAddMissing_rec( p, pFanin, nLevTravMin ); - // collect the node - Vec_PtrPush( p->vNodes, pObj ); -} - -/**Function************************************************************* - - Synopsis [Adds to the window nodes and leaves in the TFI of the roots.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_WinAddMissing( Res_Win_t * p ) -{ - Abc_Obj_t * pObj; - int i; - // mark the leaves - Abc_NtkIncrementTravId( p->pNode->pNtk ); - Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - Abc_NodeSetTravIdCurrent( pObj ); - // mark the already collected nodes - Vec_PtrForEachEntry( p->vNodes, pObj, i ) - Abc_NodeSetTravIdCurrent( pObj ); - // explore from the roots - Vec_PtrClear( p->vBranches ); - Vec_PtrForEachEntry( p->vRoots, pObj, i ) - Res_WinAddMissing_rec( p, pObj, p->nLevTravMin ); -} - - - - -/**Function************************************************************* - - Synopsis [Returns 1 if the window is trivial (without TFO).] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_WinIsTrivial( Res_Win_t * p ) -{ - return Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode; -} - -/**Function************************************************************* - - Synopsis [Computes the window.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p ) -{ - assert( Abc_ObjIsNode(pNode) ); - assert( nWinTfiMax > 0 && nWinTfiMax < 10 ); - assert( nWinTfoMax >= 0 && nWinTfoMax < 10 ); - - // initialize the window - p->pNode = pNode; - p->nWinTfiMax = nWinTfiMax; - p->nWinTfoMax = nWinTfoMax; - - Vec_PtrClear( p->vBranches ); - Vec_PtrClear( p->vDivs ); - Vec_PtrClear( p->vRoots ); - Vec_PtrPush( p->vRoots, pNode ); - - // compute the leaves - if ( !Res_WinCollectLeavesAndNodes( p ) ) - return 0; - - // compute the candidate roots - if ( p->nWinTfoMax > 0 && Res_WinComputeRoots(p) ) - { - // mark the paths from the roots to the leaves - Res_WinMarkPaths( p ); - // refine the roots and add branches and missing nodes - if ( Res_WinFinalizeRoots( p ) ) - Res_WinAddMissing( p ); - } - - return 1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/opt/res/res_.c b/src/opt/res/res_.c deleted file mode 100644 index a50affd7..00000000 --- a/src/opt/res/res_.c +++ /dev/null @@ -1,50 +0,0 @@ -/**CFile**************************************************************** - - FileName [res_.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Resynthesis package.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 15, 2007.] - - Revision [$Id: res_.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "res.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |