diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abc.c | 12 | ||||
-rw-r--r-- | src/base/abci/abcDelay.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcIf.c | 59 | ||||
-rw-r--r-- | src/map/if/if.h | 2 | ||||
-rw-r--r-- | src/map/if/ifCore.c | 13 | ||||
-rw-r--r-- | src/map/if/ifCut.c | 143 | ||||
-rw-r--r-- | src/map/if/ifMan.c | 1 | ||||
-rw-r--r-- | src/map/if/ifMap.c | 4 | ||||
-rw-r--r-- | src/opt/mfs/mfsCore.c | 2 | ||||
-rw-r--r-- | src/opt/mfs/mfsInt.h | 4 | ||||
-rw-r--r-- | src/opt/mfs/mfsInter.c | 102 | ||||
-rw-r--r-- | src/opt/mfs/mfsMan.c | 1 | ||||
-rw-r--r-- | src/sat/bsat/module.make | 1 |
13 files changed, 330 insertions, 16 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index aea02c0e..368ee2a8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10750,7 +10750,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nAreaIters = 2; pPars->DelayTarget = -1; pPars->Epsilon = (float)0.001; - pPars->fPreprocess = 1; + pPars->fPreprocess = 1; pPars->fArea = 0; pPars->fFancy = 0; pPars->fExpRed = 1; @@ -10898,8 +10898,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) // get LUT size from the library pPars->nLutSize = pPars->pLutLib->LutMax; // if variable pin delay, force truth table computation - if ( pPars->pLutLib->fVarPinDelays ) - pPars->fTruth = 1; +// if ( pPars->pLutLib->fVarPinDelays ) +// pPars->fTruth = 1; } if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE ) @@ -10924,11 +10924,15 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( (c = Abc_NtkGetChoiceNum( pNtk )) ) { printf( "Performing LUT mapping with %d choices.\n", c ); - pPars->fTruth = 1; +// pPars->fTruth = 1; + pPars->fExpRed = 0; } // enable truth table computation if cut minimization is selected if ( pPars->fCutMin ) + { pPars->fTruth = 1; + pPars->fExpRed = 0; + } // complain if truth tables are requested but the cut size is too large if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE ) diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c index 67e051f3..553bb2fc 100644 --- a/src/base/abci/abcDelay.c +++ b/src/base/abci/abcDelay.c @@ -96,7 +96,7 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD ***********************************************************************/ float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib ) { - int fUseSorting = 0; + int fUseSorting = 1; int pPinPerm[32]; float pPinDelays[32]; If_Lib_t * pLutLib; diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index 742a3a02..bf351a47 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -252,8 +252,8 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t // create a new node pNodeNew = Abc_NtkCreateNode( pNtkNew ); pCutBest = If_ObjCutBest( pIfObj ); - if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays ) - If_CutRotatePins( pIfMan, pCutBest ); +// if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays ) +// If_CutRotatePins( pIfMan, pCutBest ); if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv ) { If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i ) @@ -346,6 +346,54 @@ Hop_Obj_t * Abc_NodeIfToHop_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_ return gFunc; } + +/**Function************************************************************* + + Synopsis [Recursively derives the truth table for the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Abc_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited ) +{ + If_Cut_t * pCut; + If_Obj_t * pTemp; + Hop_Obj_t * gFunc, * gFunc0, * gFunc1; + // get the best cut + pCut = If_ObjCutBest(pIfObj); + // if the cut is visited, return the result + if ( If_CutData(pCut) ) + return If_CutData(pCut); + // mark the node as visited + Vec_PtrPush( vVisited, pCut ); + // insert the worst case + If_CutSetData( pCut, (void *)1 ); + // skip in case of primary input + if ( If_ObjIsCi(pIfObj) ) + return If_CutData(pCut); + // compute the functions of the children + for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv ) + { + gFunc0 = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin0, vVisited ); + if ( gFunc0 == (void *)1 ) + continue; + gFunc1 = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin1, vVisited ); + if ( gFunc1 == (void *)1 ) + continue; + // both branches are solved + gFunc = Hop_And( pHopMan, Hop_NotCond(gFunc0, pTemp->fCompl0), Hop_NotCond(gFunc1, pTemp->fCompl1) ); + if ( pTemp->fPhase != pIfObj->fPhase ) + gFunc = Hop_Not(gFunc); + If_CutSetData( pCut, gFunc ); + break; + } + return If_CutData(pCut); +} + /**Function************************************************************* Synopsis [Derives the truth table for one cut.] @@ -371,7 +419,12 @@ Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * If_CutSetData( If_ObjCutBest(pLeaf), Hop_IthVar(pHopMan, i) ); // recursively compute the function while collecting visited cuts Vec_PtrClear( pIfMan->vTemp ); - gFunc = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); + gFunc = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); + if ( gFunc == (void *)1 ) + { + printf( "Abc_NodeIfToHop(): Computing local AIG has failed.\n" ); + return NULL; + } // printf( "%d ", Vec_PtrSize(p->vTemp) ); // clean the cuts If_CutForEachLeaf( pIfMan, pCut, pLeaf, i ) diff --git a/src/map/if/if.h b/src/map/if/if.h index 32d458dc..6c33e03f 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -166,6 +166,8 @@ struct If_Man_t_ int nSmallSupp; // the small support // timing manager Tim_Man_t * pManTim; + // statistics +// int timeTruth; }; // priority cut diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c index 16a14153..99b99af7 100644 --- a/src/map/if/ifCore.c +++ b/src/map/if/ifCore.c @@ -110,14 +110,14 @@ int If_ManPerformMappingComb( If_Man_t * p ) If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0, "Delay" ); // try to improve area by expanding and reducing the cuts - if ( p->pPars->fExpRed && !p->pPars->fTruth ) + if ( p->pPars->fExpRed ) If_ManImproveMapping( p ); // area flow oriented mapping for ( i = 0; i < p->pPars->nFlowIters; i++ ) { If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 0, "Flow" ); - if ( p->pPars->fExpRed && !p->pPars->fTruth ) + if ( p->pPars->fExpRed ) If_ManImproveMapping( p ); } @@ -125,7 +125,7 @@ int If_ManPerformMappingComb( If_Man_t * p ) for ( i = 0; i < p->pPars->nAreaIters; i++ ) { If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 0, "Area" ); - if ( p->pPars->fExpRed && !p->pPars->fTruth ) + if ( p->pPars->fExpRed ) If_ManImproveMapping( p ); } @@ -139,6 +139,13 @@ int If_ManPerformMappingComb( If_Man_t * p ) // printf( "Cross cut memory = %d.\n", Mem_FixedReadMaxEntriesUsed(p->pMemSet) ); s_MappingTime = clock() - clkTotal; // printf( "Special POs = %d.\n", If_ManCountSpecialPos(p) ); + { + extern int If_CutGetCones( If_Man_t * p ); + extern int If_CutCountTotalFanins( If_Man_t * p ); +// If_CutGetCones( p ); +// If_CutCountTotalFanins( p ); + } + return 1; } diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c index cc842c19..08653d95 100644 --- a/src/map/if/ifCut.c +++ b/src/map/if/ifCut.c @@ -980,6 +980,149 @@ float If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut ) return aResult; } +/**Function************************************************************* + + Synopsis [Computes the cone of the cut in AIG with choices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_CutGetCutMinLevel( If_Man_t * p, If_Cut_t * pCut ) +{ + If_Obj_t * pLeaf; + int i, nMinLevel = IF_INFINITY; + If_CutForEachLeaf( p, pCut, pLeaf, i ) + nMinLevel = IF_MIN( nMinLevel, (int)pLeaf->Level ); + return nMinLevel; +} + +/**Function************************************************************* + + Synopsis [Computes the cone of the cut in AIG with choices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_CutGetCone_rec( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut ) +{ + If_Obj_t * pTemp; + int i, RetValue; + // check if the node is in the cut + for ( i = 0; i < (int)pCut->nLeaves; i++ ) + if ( pCut->pLeaves[i] == pObj->Id ) + return 1; + else if ( pCut->pLeaves[i] > pObj->Id ) + break; + // return if we reached the boundary + if ( If_ObjIsCi(pObj) ) + return 0; + // check the choice node + for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv ) + { + // check if the node itself is bound + RetValue = If_CutGetCone_rec( p, If_ObjFanin0(pTemp), pCut ); + if ( RetValue ) + RetValue &= If_CutGetCone_rec( p, If_ObjFanin1(pTemp), pCut ); + if ( RetValue ) + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Computes the cone of the cut in AIG with choices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_CutGetCones( If_Man_t * p ) +{ + If_Obj_t * pObj; + int i, Counter = 0; + int clk = clock(); + If_ManForEachObj( p, pObj, i ) + { + if ( If_ObjIsAnd(pObj) && pObj->nRefs ) + { + Counter += !If_CutGetCone_rec( p, pObj, If_ObjCutBest(pObj) ); +// printf( "%d ", If_CutGetCutMinLevel( p, If_ObjCutBest(pObj) ) ); + } + } + printf( "Cound not find boundary for %d nodes.\n", Counter ); + PRT( "Cones", clock() - clk ); + return 1; +} + + +/**Function************************************************************* + + Synopsis [Computes the cone of the cut in AIG with choices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_CutFoundFanins_rec( If_Obj_t * pObj, Vec_Int_t * vLeaves ) +{ + if ( pObj->nRefs || If_ObjIsCi(pObj) ) + { + Vec_IntPushUnique( vLeaves, pObj->Id ); + return; + } + If_CutFoundFanins_rec( If_ObjFanin0(pObj), vLeaves ); + If_CutFoundFanins_rec( If_ObjFanin1(pObj), vLeaves ); +} + +/**Function************************************************************* + + Synopsis [Computes the cone of the cut in AIG with choices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_CutCountTotalFanins( If_Man_t * p ) +{ + If_Obj_t * pObj; + Vec_Int_t * vLeaves; + int i, nFaninsTotal = 0, Counter = 0; + int clk = clock(); + vLeaves = Vec_IntAlloc( 100 ); + If_ManForEachObj( p, pObj, i ) + { + if ( If_ObjIsAnd(pObj) && pObj->nRefs ) + { + nFaninsTotal += If_ObjCutBest(pObj)->nLeaves; + Vec_IntClear( vLeaves ); + If_CutFoundFanins_rec( If_ObjFanin0(pObj), vLeaves ); + If_CutFoundFanins_rec( If_ObjFanin1(pObj), vLeaves ); + Counter += Vec_IntSize(vLeaves); + } + } + printf( "Total cut inputs = %d. Total fanins incremental = %d.\n", nFaninsTotal, Counter ); + PRT( "Fanins", clock() - clk ); + Vec_IntFree( vLeaves ); + return 1; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 1528b08c..7bb7fcd1 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -124,6 +124,7 @@ void If_ManRestart( If_Man_t * p ) ***********************************************************************/ void If_ManStop( If_Man_t * p ) { +// PRT( "Truth", p->timeTruth ); // printf( "Small support = %d.\n", p->nSmallSupp ); Vec_PtrFree( p->vCis ); Vec_PtrFree( p->vCos ); diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index 1ac5ef21..fafd454d 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -119,7 +119,11 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep // compute the truth table pCut->fCompl = 0; if ( p->pPars->fTruth ) + { +// int clk = clock(); If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 ); +// p->timeTruth += clock() - clk; + } // compute the application-specific cost and depth pCut->fUser = (p->pPars->pFuncCost != NULL); pCut->Cost = p->pPars->pFuncCost? p->pPars->pFuncCost(pCut) : 0; diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 7e6cd454..4a2e96e7 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -68,7 +68,7 @@ clk = clock(); p->timeCnf += clock() - clk; // create the SAT problem clk = clock(); - p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0 ); + p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0, 0 ); if ( p->pSat == NULL ) { p->nNodesBad++; diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index f98f6239..b7fa6ef0 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -85,6 +85,7 @@ struct Mfs_Man_t_ int nNodesBad; int nTotalDivs; int nTimeOuts; + int nDcMints; // node/edge stats int nTotalNodesBeg; int nTotalNodesEnd; @@ -115,8 +116,9 @@ struct Mfs_Man_t_ /*=== mfsDiv.c ==========================================================*/ extern Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax ); /*=== mfsInter.c ==========================================================*/ -extern sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands ); +extern sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, int fInvert ); extern Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ); +extern int Abc_NtkMfsInterplateEval( Mfs_Man_t * p, int * pCands, int nCands ); /*=== mfsMan.c ==========================================================*/ extern Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars ); extern void Mfs_ManStop( Mfs_Man_t * p ); diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c index 24617cd9..5944fd5b 100644 --- a/src/opt/mfs/mfsInter.c +++ b/src/opt/mfs/mfsInter.c @@ -82,7 +82,7 @@ int Abc_MfsSatAddXor( sat_solver * pSat, int iVarA, int iVarB, int iVarC ) SeeAlso [] ***********************************************************************/ -sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands ) +sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, int fInvert ) { sat_solver * pSat; Aig_Obj_t * pObjPo; @@ -90,7 +90,7 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands ) // get the literal for the output of F pObjPo = Aig_ManPo( p->pAigWin, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) - 1 ); - Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], 0 ); + Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert ); // collect the outputs of the divisors Vec_IntClear( p->vProjVars ); @@ -210,6 +210,100 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands ) SeeAlso [] ***********************************************************************/ +unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, int fInvert ) +{ + sat_solver * pSat; + Sto_Man_t * pCnf = NULL; + unsigned * puTruth; + int nFanins, status; + int c, i, * pGloVars; + + // derive the SAT solver for interpolation + pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, fInvert ); + + // solve the problem + status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( status != l_False ) + { + p->nTimeOuts++; + return NULL; + } + // get the learned clauses + pCnf = sat_solver_store_release( pSat ); + sat_solver_delete( pSat ); + + // set the global variables + pGloVars = Int_ManSetGlobalVars( p->pMan, nCands ); + for ( c = 0; c < nCands; c++ ) + { + // get the variable number of this divisor + i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; + // get the corresponding SAT variable + pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); + } + + // derive the interpolant + nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth ); + Sto_ManFree( pCnf ); + assert( nFanins == nCands ); + return puTruth; +} + +/**Function************************************************************* + + Synopsis [Performs interpolation.] + + Description [Derives the new function of the node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsInterplateEval( Mfs_Man_t * p, int * pCands, int nCands ) +{ + unsigned * pTruth, uTruth0[2], uTruth1[2]; + int nCounter; + pTruth = Abc_NtkMfsInterplateTruth( p, pCands, nCands, 0 ); + if ( nCands == 6 ) + { + uTruth1[0] = pTruth[0]; + uTruth1[1] = pTruth[1]; + } + else + { + uTruth1[0] = pTruth[0]; + uTruth1[1] = pTruth[0]; + } + pTruth = Abc_NtkMfsInterplateTruth( p, pCands, nCands, 1 ); + if ( nCands == 6 ) + { + uTruth0[0] = ~pTruth[0]; + uTruth0[1] = ~pTruth[1]; + } + else + { + uTruth0[0] = ~pTruth[0]; + uTruth0[1] = ~pTruth[0]; + } + nCounter = Extra_WordCountOnes( uTruth0[0] ^ uTruth1[0] ); + nCounter += Extra_WordCountOnes( uTruth0[1] ^ uTruth1[1] ); +// printf( "%d ", nCounter ); + return nCounter; +} + + +/**Function************************************************************* + + Synopsis [Performs interpolation.] + + Description [Derives the new function of the node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ) { extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); @@ -222,8 +316,10 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ) int nFanins, status; int c, i, * pGloVars; +// p->nDcMints += Abc_NtkMfsInterplateEval( p, pCands, nCands ); + // derive the SAT solver for interpolation - pSat = Abc_MfsCreateSolverResub( p, pCands, nCands ); + pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, 0 ); // solve the problem status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 99a60ef6..5f947aeb 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -122,6 +122,7 @@ void Mfs_ManPrint( Mfs_Man_t * p ) p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) ); else Abc_NtkMfsPrintResubStats( p ); +// printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) ); } else { diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make index 1e52cc0a..f6805600 100644 --- a/src/sat/bsat/module.make +++ b/src/sat/bsat/module.make @@ -1,6 +1,7 @@ SRC += src/sat/bsat/satMem.c \ src/sat/bsat/satInter.c \ src/sat/bsat/satInterA.c \ + src/sat/bsat/satInterP.c \ src/sat/bsat/satSolver.c \ src/sat/bsat/satStore.c \ src/sat/bsat/satTrace.c \ |