summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/sfm/sfm.h1
-rw-r--r--src/opt/sfm/sfmCore.c75
-rw-r--r--src/opt/sfm/sfmInt.h3
-rw-r--r--src/opt/sfm/sfmSat.c104
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 []
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 02:09:19 +0000