luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Trying to explicitly compute don't-cares during optimization.

This commit is contained in:
Alan Mishchenko 2020-11-01 14:23:17 -08:00
parent 3a7b3d27f1
commit ce95366e51
6 changed files with 185 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/base/abci/abc.c
View File

@ -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 <num>] [-daeijvwh]\n" );
Abc_Print( -2, "usage: mfs2 [-WFDMLCZNI <num>] [-daeijlvwh]\n" );
Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" );
Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
Abc_Print( -2, "\t-F <num> : 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 <num>] [-daebvwh]\n" );
Abc_Print( -2, "usage: &mfs [-WFDMLCN <num>] [-daeblvwh]\n" );
Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" );
Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
Abc_Print( -2, "\t-F <num> : 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");

3
src/base/io/ioUtil.c
View File

@ -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" )) )

1
src/opt/sfm/sfm.h
View File

@ -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

75
src/opt/sfm/sfmCore.c
View File

@ -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 )

3
src/opt/sfm/sfmInt.h
View File

@ -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 );

104
src/opt/sfm/sfmSat.c
View File

@ -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<<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.]