diff options
Diffstat (limited to 'src/opt/sfm')
-rw-r--r-- | src/opt/sfm/sfm.h | 1 | ||||
-rw-r--r-- | src/opt/sfm/sfmCore.c | 75 | ||||
-rw-r--r-- | src/opt/sfm/sfmInt.h | 3 | ||||
-rw-r--r-- | src/opt/sfm/sfmSat.c | 104 |
4 files changed, 171 insertions, 12 deletions
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index 1aa8b7d0..f9c95c83 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -66,6 +66,7 @@ struct Sfm_Par_t_ int fUseAndOr; // enable internal detection of AND/OR gates int fZeroCost; // enable zero-cost replacement int fUseSim; // enable simulation + int fUseDcs; // enable deriving don't-cares int fPrintDecs; // enable printing decompositions int fAllBoxes; // enable preserving all boxes int fLibVerbose; // enable library stats diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c index 27d584b4..fe69d480 100644 --- a/src/opt/sfm/sfmCore.c +++ b/src/opt/sfm/sfmCore.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "sfmInt.h" +#include "bool/kit/kit.h" ABC_NAMESPACE_IMPL_START @@ -79,6 +80,8 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p ) printf( "Attempts : " ); printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) ); printf( "Resub %6d out of %6d (%6.2f %%) ", p->nResubs, p->nTryResubs, 100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs) ); + if ( p->pPars->fUseDcs ) + printf( "Improves %6d out of %6d (%6.2f %%) ", p->nImproves,p->nTryImproves,100.0*p->nImproves/Abc_MaxInt(1, p->nTryImproves)); printf( "\n" ); printf( "Reduction: " ); @@ -213,7 +216,70 @@ finish: // update the network Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth ); return 1; - } +} + +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sfm_NodeResubOne( Sfm_Ntk_t * p, int iNode ) +{ + int fSkipUpdate = 0; + int fVeryVerbose = 0;//p->pPars->fVeryVerbose; + int i, iFanin; + word uTruth; + abctime clk; + assert( Sfm_ObjIsNode(p, iNode) ); + p->nTryImproves++; + // report init stats + if ( p->pPars->fVeryVerbose ) + printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Div=%3d. Fanins = %d. MFFC = %d\n", + iNode, Sfm_ObjLevel(p, iNode), 0, Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), + Sfm_ObjFaninNum(p, iNode), Sfm_ObjMffcSize(p, iNode) ); + // collect fanins + Vec_IntClear( p->vDivIds ); + Sfm_ObjForEachFanin( p, iNode, iFanin, i ) + Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iFanin) ); +clk = Abc_Clock(); + uTruth = Sfm_ComputeInterpolant2( p ); +p->timeSat += Abc_Clock() - clk; + // analyze outcomes + if ( uTruth == SFM_SAT_UNDEC ) + { + p->nTimeOuts++; + return 0; + } + assert( uTruth != SFM_SAT_SAT ); + if ( uTruth == Vec_WrdEntry(p->vTruths, iNode) ) + return 0; + else + { + word uTruth0 = Vec_WrdEntry(p->vTruths, iNode); + //word uTruth0N = ~uTruth0; + //word uTruthN = ~uTruth; + int Old = Kit_TruthLitNum((unsigned*)&uTruth0, Sfm_ObjFaninNum(p, iNode), p->vCover); + //int OldN = Kit_TruthLitNum((unsigned*)&uTruth0N, Sfm_ObjFaninNum(p, iNode), p->vCover); + int New = Kit_TruthLitNum((unsigned*)&uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover); + //int NewN = Kit_TruthLitNum((unsigned*)&uTruthN, Sfm_ObjFaninNum(p, iNode), p->vCover); + //if ( Abc_MinInt(New, NewN) > Abc_MinInt(Old, OldN) ) + if ( New > Old ) + return 0; + } + p->nImproves++; + if ( fSkipUpdate ) + return 0; + // update truth table + Vec_WrdWriteEntry( p->vTruths, iNode, uTruth ); + Sfm_TruthToCnf( uTruth, NULL, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) ); + return 1; +} int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode ) { int i, iFanin; @@ -230,15 +296,18 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode ) if ( Sfm_NodeResubSolve( p, iNode, i, 0 ) ) return 1; } - if ( p->pPars->fArea ) - return 0; // try removing redundant edges + if ( !p->pPars->fArea ) Sfm_ObjForEachFanin( p, iNode, iFanin, i ) if ( !(Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1) ) { if ( Sfm_NodeResubSolve( p, iNode, i, 1 ) ) return 1; } + // try simplifying local functions + if ( p->pPars->fUseDcs ) + if ( Sfm_NodeResubOne( p, iNode ) ) + return 1; /* // try replacing area critical fanins while adding two new fanins if ( Sfm_ObjFaninNum(p, iNode) < p->nFaninMax ) diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h index 80edd54d..08edf353 100644 --- a/src/opt/sfm/sfmInt.h +++ b/src/opt/sfm/sfmInt.h @@ -107,8 +107,10 @@ struct Sfm_Ntk_t_ sat_solver * pSat; // SAT solver int nSatVars; // the number of variables int nTryRemoves; // number of fanin removals + int nTryImproves;// number of node improvements int nTryResubs; // number of resubstitutions int nRemoves; // number of fanin removals + int nImproves; // number of node improvements int nResubs; // number of resubstitutions // counter-examples int nCexes; // number of CEXes @@ -218,6 +220,7 @@ extern void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNe /*=== sfmSat.c ==========================================================*/ extern int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ); extern word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ); +extern word Sfm_ComputeInterpolant2( Sfm_Ntk_t * p ); /*=== sfmTim.c ==========================================================*/ extern Sfm_Tim_t * Sfm_TimStart( Mio_Library_t * pLib, Scl_Con_t * pExt, Abc_Ntk_t * pNtk, int DeltaCrit ); extern void Sfm_TimStop( Sfm_Tim_t * p ); diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c index 6ccdd903..ed38e681 100644 --- a/src/opt/sfm/sfmSat.c +++ b/src/opt/sfm/sfmSat.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "sfmInt.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -27,15 +28,6 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static word s_Truths6[6] = { - ABC_CONST(0xAAAAAAAAAAAAAAAA), - ABC_CONST(0xCCCCCCCCCCCCCCCC), - ABC_CONST(0xF0F0F0F0F0F0F0F0), - ABC_CONST(0xFF00FF00FF00FF00), - ABC_CONST(0xFFFF0000FFFF0000), - ABC_CONST(0xFFFFFFFF00000000) -}; - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -228,6 +220,100 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ) /**Function************************************************************* + Synopsis [Takes SAT solver and returns interpolant.] + + Description [If interpolant does not exist, records difference variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sfm_ComputeInterpolantInt( Sfm_Ntk_t * p, word Truth[2] ) +{ + int fOnSet, iMint, iVar, nVars = sat_solver_nvars( p->pSat ); + int iVarPivot = Sfm_ObjSatVar( p, p->iPivotNode ); + int status, iNewLit, i, Div, nIter = 0; + Truth[0] = Truth[1] = 0; + sat_solver_setnvars( p->pSat, nVars + 1 ); + iNewLit = Abc_Var2Lit( nVars, 0 ); // iNewLit + assert( Vec_IntSize(p->vDivIds) <= 6 ); + Vec_IntFill( p->vValues, (1 << Vec_IntSize(p->vDivIds)) * Vec_IntSize(p->vDivVars), -1 ); + while ( 1 ) + { + // find care minterm + p->nSatCalls++; nIter++; + status = sat_solver_solve( p->pSat, &iNewLit, &iNewLit + 1, p->pPars->nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return l_Undef; + if ( status == l_False ) + return l_False; + assert( status == l_True ); + // collect values + iMint = 0; + fOnSet = sat_solver_var_value(p->pSat, iVarPivot); + Vec_IntClear( p->vLits ); + Vec_IntPush( p->vLits, Abc_LitNot(iNewLit) ); // NOT(iNewLit) + Vec_IntPush( p->vLits, Abc_LitNot(sat_solver_var_literal(p->pSat, iVarPivot)) ); + Vec_IntForEachEntry( p->vDivIds, Div, i ) + { + Vec_IntPush( p->vLits, Abc_LitNot(sat_solver_var_literal(p->pSat, Div)) ); + if ( sat_solver_var_value(p->pSat, Div) ) + iMint |= 1 << i; + } + if ( Truth[!fOnSet] & ((word)1 << iMint) ) + break; + assert( !(Truth[fOnSet] & ((word)1 << iMint)) ); + Truth[fOnSet] |= ((word)1 << iMint); + // remember variable values + Vec_IntForEachEntry( p->vDivVars, iVar, i ) + Vec_IntWriteEntry( p->vValues, iMint * Vec_IntSize(p->vDivVars) + i, sat_solver_var_value(p->pSat, iVar) ); + status = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) ); + if ( status == 0 ) + return l_False; + } + assert( status == l_True ); + // store the counter-example + assert( iMint < (1 << Vec_IntSize(p->vDivIds)) ); + Vec_IntForEachEntry( p->vDivVars, iVar, i ) + { + int Value = Vec_IntEntry(p->vValues, iMint * Vec_IntSize(p->vDivVars) + i); + assert( Value != -1 ); + if ( Value ^ sat_solver_var_value(p->pSat, iVar) ) // insert 1 + { + word * pSign = Vec_WrdEntryP( p->vDivCexes, i ); + assert( !Abc_InfoHasBit( (unsigned *)pSign, p->nCexes) ); + Abc_InfoXorBit( (unsigned *)pSign, p->nCexes ); + } + } + p->nCexes++; + return l_True; +} +word Sfm_ComputeInterpolant2( Sfm_Ntk_t * p ) +{ + word Res, ResP, ResN, Truth[2]; + int nCubesP = 0, nCubesN = 0; + int RetValue = Sfm_ComputeInterpolantInt( p, Truth ); + if ( RetValue == l_Undef ) + return SFM_SAT_UNDEC; + if ( RetValue == l_True ) + return SFM_SAT_SAT; + assert( RetValue == l_False ); + //printf( "Offset = %2d. Onset = %2d. DC = %2d. Total = %2d.\n", + // Abc_TtCountOnes(Truth[0]), Abc_TtCountOnes(Truth[1]), + // (1<<Vec_IntSize(p->vDivIds)) - (Abc_TtCountOnes(Truth[0]) + Abc_TtCountOnes(Truth[1])), + // 1<<Vec_IntSize(p->vDivIds) ); + Truth[0] = Abc_Tt6Stretch( Truth[0], Vec_IntSize(p->vDivIds) ); + Truth[1] = Abc_Tt6Stretch( Truth[1], Vec_IntSize(p->vDivIds) ); + ResP = Abc_Tt6Isop( Truth[1], ~Truth[0], Vec_IntSize(p->vDivIds), &nCubesP ); + ResN = Abc_Tt6Isop( Truth[0], ~Truth[1], Vec_IntSize(p->vDivIds), &nCubesN ); + Res = nCubesP <= nCubesN ? ResP : ~ResN; + //Dau_DsdPrintFromTruth( &Res, Vec_IntSize(p->vDivIds) ); + return Res; +} + +/**Function************************************************************* + Synopsis [Checks resubstitution.] Description [] |