diff options
Diffstat (limited to 'abc70930/src/opt/res')
| -rw-r--r-- | abc70930/src/opt/res/module.make | 7 | ||||
| -rw-r--r-- | abc70930/src/opt/res/res.h | 75 | ||||
| -rw-r--r-- | abc70930/src/opt/res/resCore.c | 415 | ||||
| -rw-r--r-- | abc70930/src/opt/res/resDivs.c | 285 | ||||
| -rw-r--r-- | abc70930/src/opt/res/resFilter.c | 434 | ||||
| -rw-r--r-- | abc70930/src/opt/res/resInt.h | 137 | ||||
| -rw-r--r-- | abc70930/src/opt/res/resSat.c | 407 | ||||
| -rw-r--r-- | abc70930/src/opt/res/resSim.c | 790 | ||||
| -rw-r--r-- | abc70930/src/opt/res/resSim_old.c | 521 | ||||
| -rw-r--r-- | abc70930/src/opt/res/resStrash.c | 117 | ||||
| -rw-r--r-- | abc70930/src/opt/res/resWin.c | 485 | ||||
| -rw-r--r-- | abc70930/src/opt/res/res_.c | 50 |
12 files changed, 3723 insertions, 0 deletions
diff --git a/abc70930/src/opt/res/module.make b/abc70930/src/opt/res/module.make new file mode 100644 index 00000000..52d8a315 --- /dev/null +++ b/abc70930/src/opt/res/module.make @@ -0,0 +1,7 @@ +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/abc70930/src/opt/res/res.h b/abc70930/src/opt/res/res.h new file mode 100644 index 00000000..3c3431bf --- /dev/null +++ b/abc70930/src/opt/res/res.h @@ -0,0 +1,75 @@ +/**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/abc70930/src/opt/res/resCore.c b/abc70930/src/opt/res/resCore.c new file mode 100644 index 00000000..27e9b3ea --- /dev/null +++ b/abc70930/src/opt/res/resCore.c @@ -0,0 +1,415 @@ +/**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/abc70930/src/opt/res/resDivs.c b/abc70930/src/opt/res/resDivs.c new file mode 100644 index 00000000..cc75b90f --- /dev/null +++ b/abc70930/src/opt/res/resDivs.c @@ -0,0 +1,285 @@ +/**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/abc70930/src/opt/res/resFilter.c b/abc70930/src/opt/res/resFilter.c new file mode 100644 index 00000000..f2ca41d3 --- /dev/null +++ b/abc70930/src/opt/res/resFilter.c @@ -0,0 +1,434 @@ +/**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/abc70930/src/opt/res/resInt.h b/abc70930/src/opt/res/resInt.h new file mode 100644 index 00000000..5aae46cc --- /dev/null +++ b/abc70930/src/opt/res/resInt.h @@ -0,0 +1,137 @@ +/**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/abc70930/src/opt/res/resSat.c b/abc70930/src/opt/res/resSat.c new file mode 100644 index 00000000..dd0e7a23 --- /dev/null +++ b/abc70930/src/opt/res/resSat.c @@ -0,0 +1,407 @@ +/**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/abc70930/src/opt/res/resSim.c b/abc70930/src/opt/res/resSim.c new file mode 100644 index 00000000..5c1dd2b6 --- /dev/null +++ b/abc70930/src/opt/res/resSim.c @@ -0,0 +1,790 @@ +/**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/abc70930/src/opt/res/resSim_old.c b/abc70930/src/opt/res/resSim_old.c new file mode 100644 index 00000000..23ce29e4 --- /dev/null +++ b/abc70930/src/opt/res/resSim_old.c @@ -0,0 +1,521 @@ +/**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/abc70930/src/opt/res/resStrash.c b/abc70930/src/opt/res/resStrash.c new file mode 100644 index 00000000..fde842a4 --- /dev/null +++ b/abc70930/src/opt/res/resStrash.c @@ -0,0 +1,117 @@ +/**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/abc70930/src/opt/res/resWin.c b/abc70930/src/opt/res/resWin.c new file mode 100644 index 00000000..a3648925 --- /dev/null +++ b/abc70930/src/opt/res/resWin.c @@ -0,0 +1,485 @@ +/**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/abc70930/src/opt/res/res_.c b/abc70930/src/opt/res/res_.c new file mode 100644 index 00000000..a50affd7 --- /dev/null +++ b/abc70930/src/opt/res/res_.c @@ -0,0 +1,50 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + + |