From ce95366e513631b1b052b55c4f8e2e83ff7e4149 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 1 Nov 2020 14:23:17 -0800 Subject: Trying to explicitly compute don't-cares during optimization. --- src/base/abci/abc.c | 16 ++++++-- src/base/io/ioUtil.c | 3 +- src/opt/sfm/sfm.h | 1 + src/opt/sfm/sfmCore.c | 75 ++++++++++++++++++++++++++++++++++-- src/opt/sfm/sfmInt.h | 3 ++ src/opt/sfm/sfmSat.c | 104 +++++++++++++++++++++++++++++++++++++++++++++----- 6 files changed, 185 insertions(+), 17 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 71026b28..1f21d931 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -5429,7 +5429,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Sfm_ParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZNIdaeijvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZNIdaeijlvwh" ) ) != EOF ) { switch ( c ) { @@ -5547,6 +5547,9 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'j': fUseAllFfs ^= 1; break; + case 'l': + pPars->fUseDcs ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -5618,7 +5621,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: mfs2 [-WFDMLCZNI ] [-daeijvwh]\n" ); + Abc_Print( -2, "usage: mfs2 [-WFDMLCZNI ] [-daeijlvwh]\n" ); Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" ); Abc_Print( -2, "\t-W : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax ); Abc_Print( -2, "\t-F : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax ); @@ -5634,6 +5637,7 @@ usage: Abc_Print( -2, "\t-i : toggle using inductive don't-cares [default = %s]\n", fIndDCs? "yes": "no" ); Abc_Print( -2, "\t-j : toggle using all flops when \"-i\" is enabled [default = %s]\n", fUseAllFfs? "yes": "no" ); Abc_Print( -2, "\t-I : the number of additional frames inserted [default = %d]\n", nFramesAdd ); + Abc_Print( -2, "\t-l : toggle deriving don't-cares [default = %s]\n", pPars->fUseDcs? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -46004,7 +46008,7 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nDepthMax = 100; pPars->nWinSizeMax = 2000; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCNdaebvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCNdaeblvwh" ) ) != EOF ) { switch ( c ) { @@ -46097,6 +46101,9 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'b': pPars->fAllBoxes ^= 1; break; + case 'l': + pPars->fUseDcs ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -46141,7 +46148,7 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &mfs [-WFDMLCN ] [-daebvwh]\n" ); + Abc_Print( -2, "usage: &mfs [-WFDMLCN ] [-daeblvwh]\n" ); Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" ); Abc_Print( -2, "\t-W : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax ); Abc_Print( -2, "\t-F : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax ); @@ -46154,6 +46161,7 @@ usage: Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" ); Abc_Print( -2, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" ); Abc_Print( -2, "\t-b : toggle preserving all white boxes [default = %s]\n", pPars->fAllBoxes? "yes": "no" ); + Abc_Print( -2, "\t-l : toggle deriving don't-cares [default = %s]\n", pPars->fUseDcs? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index 01fe4f45..ddfcc91a 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -899,7 +899,8 @@ void Io_TransformSF2PLA( char * pNameIn, char * pNameOut ) break; if ( strstr(pBuffer, "SDF") ) { - fgets(pBuffer, Size, pFileIn); + char * pRes = fgets(pBuffer, Size, pFileIn); + assert( pRes != NULL ); if ( (pToken = strtok( pBuffer, " \t\r\n" )) ) fprintf( pFileOut, ".i %d\n", atoi(pToken) ); if ( (pToken = strtok( NULL, " \t\r\n" )) ) 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 /// //////////////////////////////////////////////////////////////////////// @@ -226,6 +218,100 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ) return SFM_SAT_SAT; } +/**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<vDivIds)) - (Abc_TtCountOnes(Truth[0]) + Abc_TtCountOnes(Truth[1])), + // 1<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.] -- cgit v1.2.3