diff options
Diffstat (limited to 'src/opt/res/resCore.c')
-rw-r--r-- | src/opt/res/resCore.c | 259 |
1 files changed, 210 insertions, 49 deletions
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c index 17d1c62e..6340b175 100644 --- a/src/opt/res/resCore.c +++ b/src/opt/res/resCore.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "abc.h" -#include "res.h" +#include "resInt.h" #include "kit.h" #include "satStore.h" @@ -27,12 +27,120 @@ /// 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 + 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 nCandSets; // the total number of candidates + int nProvedSets; // the total number of proved groups + int nSimEmpty; // the empty simulation info + // runtime + int timeWin; // windowing + int timeDiv; // divisors + int timeAig; // strashing + int timeSim; // simulation + int timeCand; // resubstitution candidates + int timeSat; // SAT solving + int timeInt; // interpolation + int timeUpd; // updating + int timeTotal; // total runtime +}; + +extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); + //////////////////////////////////////////////////////////////////////// /// 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->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( "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( "SimEmpt = %d. ", p->nSimEmpty ); + printf( "Cands = %d. ", p->nCandSets ); + printf( "Proved = %d. ", p->nProvedSets ); + printf( "\n" ); + + PRT( "Windowing ", p->timeWin ); + PRT( "Divisors ", p->timeDiv ); + PRT( "Strashing ", p->timeAig ); + PRT( "Simulation ", p->timeSim ); + PRT( "Candidates ", p->timeCand ); + PRT( "SAT solver ", p->timeSat ); + PRT( "Interpol ", p->timeInt ); + PRT( "Undating ", p->timeUpd ); + PRT( "TOTAL ", 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->vLevels ); + free( p ); +} + +/**Function************************************************************* + Synopsis [Entrace into the resynthesis package.] Description [] @@ -42,31 +150,23 @@ SeeAlso [] ***********************************************************************/ -int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerbose, int fVeryVerbose ) +int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars ) { - Int_Man_t * pMan; - Sto_Man_t * pCnf; - Res_Win_t * pWin; - Res_Sim_t * pSim; - Abc_Ntk_t * pAig; + Res_Man_t * p; Abc_Obj_t * pObj; Hop_Obj_t * pFunc; Kit_Graph_t * pGraph; - Vec_Vec_t * vResubs; Vec_Ptr_t * vFanins; - Vec_Int_t * vMemory; unsigned * puTruth; - int i, k, nNodesOld, nFanins; + int i, k, RetValue, nNodesOld, nFanins; + int clk, clkTotal = clock(); assert( Abc_NtkHasAig(pNtk) ); - assert( nWindow > 0 && nWindow < 100 ); - vMemory = Vec_IntAlloc(0); - // start the interpolation manager - pMan = Int_ManAlloc( 512 ); - // start the window - pWin = Res_WinAlloc(); - pSim = Res_SimAlloc( nSimWords ); + + // start the manager + p = Res_ManAlloc( pPars ); // set the number of levels Abc_NtkLevel( pNtk ); + // try resynthesizing nodes in the topological order nNodesOld = Abc_NtkObjNumMax(pNtk); Abc_NtkForEachObj( pNtk, pObj, i ) @@ -75,52 +175,113 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerb continue; if ( pObj->Id > nNodesOld ) break; + // create the window for this node - if ( !Res_WinCompute(pObj, nWindow/10, nWindow%10, pWin) ) +clk = clock(); + RetValue = Res_WinCompute( pObj, p->pPars->nWindow/10, p->pPars->nWindow%10, p->pWin ); +p->timeWin += clock() - clk; + if ( !RetValue ) continue; + + p->nWins++; + p->nWinNodes += Vec_VecSizeSize( p->pWin->vLevels ); + // collect the divisors - Res_WinDivisors( pWin, pObj->Level - 1 ); +clk = clock(); + Res_WinDivisors( p->pWin, pObj->Level - 1 ); +p->timeDiv += clock() - clk; + p->nDivNodes += Vec_PtrSize( p->pWin->vDivs ); + // create the AIG for the window - pAig = Res_WndStrash( pWin ); +clk = clock(); + if ( p->pAig ) Abc_NtkDelete( p->pAig ); + p->pAig = Res_WndStrash( p->pWin ); +p->timeAig += clock() - clk; + + if ( p->pPars->fVeryVerbose ) + { + printf( "%5d : ", pObj->Id ); + printf( "Win = %3d/%4d/%3d ", Vec_PtrSize(p->pWin->vLeaves), Vec_VecSizeSize(p->pWin->vLevels), Vec_PtrSize(p->pWin->vRoots) ); + printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) ); + printf( "D+ = %3d ", p->pWin->nDivsPlus ); + printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) ); + printf( "\n" ); + } + // prepare simulation info - if ( !Res_SimPrepare( pSim, pAig ) ) +clk = clock(); + RetValue = Res_SimPrepare( p->pSim, p->pAig ); +p->timeSim += clock() - clk; + if ( !RetValue ) { - Abc_NtkDelete( pAig ); + p->nSimEmpty++; continue; } + // find resub candidates for the node - vResubs = Res_FilterCandidates( pWin, pSim ); - if ( vResubs ) +clk = clock(); + RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs ); +p->timeCand += clock() - clk; + p->nCandSets += RetValue; + if ( RetValue == 0 ) + continue; + + // iterate through candidate resubstitutions + Vec_VecForEachLevel( p->vResubs, vFanins, k ) { - // iterate through the resubstitutions - Vec_VecForEachLevel( vResubs, vFanins, k ) - { - extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); - pCnf = Res_SatProveUnsat( pAig, vFanins ); - if ( pCnf == NULL ) - continue; - // interplate this proof - nFanins = Int_ManInterpolate( pMan, pCnf, fVerbose, &puTruth ); - assert( nFanins == Vec_PtrSize(vFanins) - 2 ); - Sto_ManFree( pCnf ); - // transform interpolant into the AIG - pGraph = Kit_TruthToGraph( puTruth, nFanins, vMemory ); - // derive the AIG for the decomposition tree - pFunc = Kit_GraphToHop( pNtk->pManFunc, pGraph ); - Kit_GraphFree( pGraph ); - // update the network - if ( pFunc == NULL ) - Res_UpdateNetwork( pObj, vFanins, pFunc, pWin->vLevels ); + 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 ); +p->timeSat += clock() - clk; + if ( p->pCnf == NULL ) + { +// printf( " Sat\n" ); + continue; + } +// printf( " Unsat\n" ); + + // write it into a file +// Sto_ManDumpClauses( p->pCnf, "trace.cnf" ); + + p->nProvedSets++; + + // interplate the problem if it was UNSAT +clk = clock(); + RetValue = Int_ManInterpolate( p->pMan, p->pCnf, p->pPars->fVerbose, &puTruth ); +p->timeInt += clock() - clk; + assert( RetValue == Vec_PtrSize(vFanins) - 2 ); + + if ( puTruth ) + { + Extra_PrintBinary( stdout, puTruth, 1 << RetValue ); + printf( "\n" ); } - Vec_VecFree( vResubs ); + + continue; + + // 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, vFanins, pFunc, p->vLevels ); +p->timeUpd += clock() - clk; + break; } - Abc_NtkDelete( pAig ); } - Res_WinFree( pWin ); - Res_SimFree( pSim ); - Int_ManFree( pMan ); - Vec_IntFree( vMemory ); + + // quit resubstitution manager +p->timeTotal = clock() - clkTotal; + Res_ManFree( p ); + // check the resulting network if ( !Abc_NtkCheck( pNtk ) ) { |