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

Updates to delay optimization project.

This commit is contained in:
Alan Mishchenko 2016-12-29 21:26:02 +07:00
parent 4488ab83d0
commit 54b4692d4b
7 changed files with 216 additions and 173 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -41010,7 +41010,7 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
Sbd_Par_t Pars, * pPars = &Pars;
Sbd_ParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCacvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "KSWFMCacvwh" ) ) != EOF )
{
switch ( c )
{
@ -41025,6 +41025,17 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nLutSize < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLutNum = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLutNum < 0 )
goto usage;
break;
case 'W':
if ( globalUtilOptind >= argc )
{
@ -41107,9 +41118,10 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &mfsd [-KWFMC <num>] [-acvwh]\n" );
Abc_Print( -2, "usage: &mfsd [-KSWFMC <num>] [-acvwh]\n" );
Abc_Print( -2, "\t performs SAT-based delay-oriented AIG optimization\n" );
Abc_Print( -2, "\t-K <num> : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n", pPars->nLutSize );
Abc_Print( -2, "\t-S <num> : the LUT structure size (1 <= num <= 2) [default = %d]\n", pPars->nLutNum );
Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevels );
Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nTfoFanMax );
Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );

2
src/opt/dau/dauGia.c
View File

@ -241,7 +241,7 @@ int Dau_DsdBalance( Gia_Man_t * pGia, int * pFans, int nFans, int fAnd )
if ( pGia->pHTable == NULL )
{
if ( fAnd )
iFan = Gia_ManAppendAnd( pGia, iFan0, iFan1 );
iFan = Gia_ManAppendAnd2( pGia, iFan0, iFan1 );
else if ( pGia->pMuxes )
{
int fCompl = Abc_LitIsCompl(iFan0) ^ Abc_LitIsCompl(iFan1);

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

@ -39,6 +39,7 @@ typedef struct Sbd_Par_t_ Sbd_Par_t;
struct Sbd_Par_t_
{
int nLutSize; // target LUT size
int nLutNum; // target LUT count
int nTfoLevels; // the number of TFO levels (windowing)
int nTfoFanMax; // the max number of fanouts (windowing)
int nWinSizeMax; // maximum window size (windowing)

288
src/opt/sbd/sbdCore.c
View File

@ -1,12 +1,12 @@
/**CFile****************************************************************
FileName [sbd.c]
FileName [sbdCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based optimization using internal don't-cares.]
Synopsis []
Synopsis [Core procedures.]
Author [Alan Mishchenko]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: sbdCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@ -30,7 +30,6 @@ ABC_NAMESPACE_IMPL_START
#define SBD_MAX_LUTSIZE 6
typedef struct Sbd_Man_t_ Sbd_Man_t;
struct Sbd_Man_t_
{
@ -44,13 +43,13 @@ struct Sbd_Man_t_
Vec_Int_t * vCover; // temporary
Vec_Int_t * vLits; // temporary
Vec_Int_t * vLits2; // temporary
int nConsts; // constants
int nChanges; // changes
int nLuts[3]; // 0=const, 1=1lut, 2=2lut
abctime timeWin;
abctime timeCnf;
abctime timeSat;
abctime timeCov;
abctime timeEnu;
abctime timeQbf;
abctime timeOther;
abctime timeTotal;
Sbd_Sto_t * pSto;
@ -98,6 +97,7 @@ void Sbd_ParSetDefault( Sbd_Par_t * pPars )
{
memset( pPars, 0, sizeof(Sbd_Par_t) );
pPars->nLutSize = 4; // target LUT size
pPars->nLutNum = 2; // target LUT count
pPars->nTfoLevels = 2; // the number of TFO levels (windowing)
pPars->nTfoFanMax = 4; // the max number of fanouts (windowing)
pPars->nWinSizeMax = 0; // maximum window size (windowing)
@ -489,24 +489,26 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
***********************************************************************/
int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
{
extern int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds );
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
extern void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot );
int nMintCount = 1;
Vec_Ptr_t * vSims;
word * pSims = Sbd_ObjSim0( p, Pivot );
word * pCtrl = Sbd_ObjSim2( p, Pivot );
int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
int RetValue, i, iObj, Ind, fFindOnset, nCares[2] = {0};
abctime clk = Abc_Clock();
extern int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds );
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
p->timeCnf += Abc_Clock() - clk;
if ( p->pSat == NULL )
{
if ( p->pPars->fVerbose )
printf( "Found stuck-at-%d node %d.\n", 0, Pivot );
//if ( p->pPars->fVerbose )
// printf( "Found stuck-at-%d node %d.\n", 0, Pivot );
Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
p->nConsts++;
p->nLuts[0]++;
return 0;
}
//return -1;
@ -526,7 +528,7 @@ int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
nCares[0] = nCares[0] < nMintCount ? nMintCount - nCares[0] : 0;
nCares[1] = nCares[1] < nMintCount ? nMintCount - nCares[1] : 0;
if ( p->pPars->fVerbose )
if ( p->pPars->fVeryVerbose )
printf( "Computing %d offset and %d onset minterms for node %d.\n", nCares[0], nCares[1], Pivot );
if ( Vec_IntSize(p->vLits) >= nCares[0] + nCares[1] )
@ -565,10 +567,10 @@ int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
Vec_PtrFree( vSims );
if ( RetValue >= 0 )
{
if ( p->pPars->fVerbose )
if ( p->pPars->fVeryVerbose )
printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
p->nConsts++;
p->nLuts[0]++;
return RetValue;
}
// set controlability of these minterms
@ -1153,7 +1155,7 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
{
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset );
abctime clk = Abc_Clock();
abctime clk, clkSat = 0, clkEnu = 0, clkAll;
word Onset[64] = {0}, Offset[64] = {0}, Cube;
word CoverRows[64] = {0}, CoverCols[64] = {0};
int nIters, nItersMax = 32;
@ -1165,20 +1167,25 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
int nConsts = 4;
int RetValue;
sat_solver_delete_p( &p->pSat );
clk = Abc_Clock();
//sat_solver_delete_p( &p->pSat );
p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
p->timeCnf += Abc_Clock() - clk;
clkAll = Abc_Clock();
assert( nConsts <= 8 );
clk = Abc_Clock();
RetValue = Sbd_ManCollectConstantsNew( p->pSat, p->vDivVars, nConsts, PivotVar, Onset, Offset );
clkSat += Abc_Clock() - clk;
if ( RetValue >= 0 )
{
if ( p->pPars->fVerbose )
if ( p->pPars->fVeryVerbose )
printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
p->nConsts++;
p->nLuts[0]++;
return RetValue;
}
RetValue = 0;
// create rows of the table
nRows = 0;
@ -1200,36 +1207,35 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
// solve the covering problem
for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ )
{
if ( p->pPars->fVerbose )
if ( p->pPars->fVeryVerbose )
Sbd_ManMatrPrint( p, CoverCols, nDivs, nRows );
clk = Abc_Clock();
if ( !Sbd_ManFindCands( p, CoverCols, nDivs ) )
{
if ( p->pPars->fVerbose )
if ( p->pPars->fVeryVerbose )
printf( "Cannot find a feasible cover.\n" );
//clkEnu += Abc_Clock() - clk;
//clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
//p->timeSat += clkSat;
//p->timeCov += clkAll;
//p->timeEnu += clkEnu;
clkEnu += Abc_Clock() - clk;
clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
p->timeSat += clkSat;
p->timeCov += clkAll;
p->timeEnu += clkEnu;
return 0;
}
//clkEnu += Abc_Clock() - clk;
if ( p->pPars->fVerbose )
if ( p->pPars->fVeryVerbose )
printf( "Candidate support: " ),
Vec_IntPrint( p->vDivSet );
clk = Abc_Clock();
*pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
//clkSat += Abc_Clock() - clk;
clkSat += Abc_Clock() - clk;
if ( *pTruth == SBD_SAT_UNDEC )
printf( "Node %d: Undecided.\n", Pivot );
else if ( *pTruth == SBD_SAT_SAT )
{
if ( p->pPars->fVerbose )
if ( p->pPars->fVeryVerbose )
{
int i;
printf( "Node %d: SAT.\n", Pivot );
@ -1255,15 +1261,21 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
}
else
{
if ( p->pPars->fVerbose )
if ( p->pPars->fVeryVerbose )
{
printf( "Node %d: UNSAT. ", Pivot );
Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivSet) ), printf( "\n" );
}
return 1;
p->nLuts[1]++;
RetValue = 1;
break;
}
}
return 0;
clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
p->timeSat += clkSat;
p->timeCov += clkAll;
p->timeEnu += clkEnu;
return RetValue;
}
int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
@ -1277,37 +1289,41 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset );
abctime clk = Abc_Clock();
word Truth;
int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
int nDivs = Vec_IntSize( p->vDivVars );
//int nDivs = Vec_IntSize( p->vDivVars );
int Delay = Vec_IntEntry( p->vLutLevs, Pivot );
int i, k, iObj, nIters;
int i, k, iObj, nIters, RetValue;
int nLeaves, pLeaves[SBD_DIV_MAX];
int pNodesTop[SBD_DIV_MAX], pNodesBot[SBD_DIV_MAX], pNodeRefs[SBD_DIV_MAX];
int pNodesTop[SBD_DIV_MAX], pNodesBot[SBD_DIV_MAX];//, pNodeRefs[SBD_DIV_MAX];
int nNodesTop = 0, nNodesBot = 0, nNodesDiff = 0;
sat_solver_delete_p( &p->pSat );
//sat_solver_delete_p( &p->pSat );
p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
p->timeCnf += Abc_Clock() - clk;
// extract one cut
nLeaves = Sbd_StoObjBestCut( p->pSto, Pivot, pLeaves );
if ( nLeaves == -1 )
return 0;
// solve the covering problem
for ( nIters = 0; nIters < nLeaves; nIters++ )
{
word Truth;
// try to remove one variable from divisors
Vec_IntClear( p->vDivSet );
for ( i = 0; i < nLeaves; i++ )
if ( i != nIters && pLeaves[i] != -1 )
Vec_IntPush( p->vDivSet, Vec_IntEntry(p->vObj2Var, pLeaves[i]) );
assert( Vec_IntSize(p->vDivSet) < nLeaves );
// compute truth table
clk = Abc_Clock();
Truth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
p->timeSat += Abc_Clock() - clk;
if ( Truth == SBD_SAT_UNDEC )
printf( "Node %d: Undecided.\n", Pivot );
else if ( Truth == SBD_SAT_SAT )
@ -1315,16 +1331,34 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
else
pLeaves[nIters] = -1;
}
Vec_IntClear( p->vDivSet );
for ( i = 0; i < nLeaves; i++ )
if ( pLeaves[i] != -1 )
Vec_IntPush( p->vDivSet, pLeaves[i] );
printf( "Reduced %d -> %d\n", nLeaves, Vec_IntSize(p->vDivSet) );
//printf( "Reduced %d -> %d\n", nLeaves, Vec_IntSize(p->vDivSet) );
if ( Vec_IntSize(p->vDivSet) <= p->pPars->nLutSize )
{
*pnStrs = 1;
// remap divisors
Vec_IntForEachEntry( p->vDivSet, iObj, i )
Vec_IntWriteEntry( p->vDivSet, i, Vec_IntEntry(p->vObj2Var, iObj) );
// compute truth table
clk = Abc_Clock();
Truth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
p->timeSat += Abc_Clock() - clk;
assert( Truth != SBD_SAT_UNDEC && Truth != SBD_SAT_SAT );
// create structure
Strs->fLut = 1;
Strs->nVarIns = Vec_IntSize( p->vDivSet );
for ( i = 0; i < Strs->nVarIns; i++ )
Strs->VarIns[i] = i;
Strs->Res = Truth;
p->nLuts[1]++;
//Extra_PrintBinary( stdout, (unsigned *)&Truth, 1 << Strs->nVarIns ), printf( "\n" );
return 1;
}
assert( Vec_IntSize(p->vDivSet) > p->pPars->nLutSize );
//Delay++;
// count number of nodes on each level
nNodesTop = 0, nNodesBot = 0;
Vec_IntForEachEntry( p->vDivSet, iObj, i )
@ -1336,8 +1370,8 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
pNodesTop[nNodesTop++] = i;
else // if ( DelayDiff < -2 )
pNodesBot[nNodesBot++] = i;
Vec_IntWriteEntry( p->vDivSet, iObj, Vec_IntEntry(p->vObj2Var, pLeaves[i]) );
pNodeRefs[i] = Gia_ObjRefNumId( p->pGia, iObj );
Vec_IntWriteEntry( p->vDivSet, i, Vec_IntEntry(p->vObj2Var, iObj) );
//pNodeRefs[i] = Gia_ObjRefNumId( p->pGia, iObj );
}
if ( i < Vec_IntSize(p->vDivSet) )
return 0;
@ -1379,9 +1413,15 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
Strs[2+k].Res = 0;
}
return Sbd_ProblemSolve( p->pGia, p->vMirrors,
Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,
p->vDivSet, *pnStrs, Strs );
clk = Abc_Clock();
RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors,
Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,
p->vDivSet, *pnStrs, Strs );
p->timeQbf += Abc_Clock() - clk;
if ( RetValue )
p->nLuts[2]++;
return RetValue;
}
@ -1622,7 +1662,6 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
// update delay of the initial node
assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
p->nChanges++;
return 0;
}
@ -1677,13 +1716,14 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
// remember this function
assert( Vec_IntEntry(p->vMirrors, Pivot) == -1 );
Vec_IntWriteEntry( p->vMirrors, Pivot, iLit );
if ( p->pPars->fVerbose )
if ( p->pPars->fVeryVerbose )
printf( "Replacing node %d by literal %d.\n", Pivot, iLit );
// extend data-structure to accommodate new nodes
assert( Vec_IntSize(p->vLutLevs) == iObjLast );
for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
Sbd_StoRefObj( p->pSto, i, i == Gia_ManObjNum(p->pGia)-1 ? Pivot : -1 );
Sbd_StoDerefObj( p->pSto, Pivot );
for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
{
int Delay = Sbd_StoComputeCutsNode( p->pSto, i );
@ -1703,7 +1743,6 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
// update delay of the initial node
assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
p->nChanges++;
return 0;
}
@ -1781,11 +1820,10 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
***********************************************************************/
void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
{
// extern void Sbd_ManSolveSelect( Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots );
Sbd_Str_t Strs[4];
int nStrs = 0;
int i, RetValue, nStrs = 0;
word Truth = 0;
int RetValue; word Truth = 0;
if ( !p->pSto )
{
if ( Sbd_ManMergeCuts( p, Pivot ) )
@ -1795,83 +1833,39 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
// if ( Pivot != 15 )
// return;
if ( p->pPars->fVerbose )
printf( "\nLooking at node %d\n", Pivot );
if ( Sbd_ManWindow( p, Pivot ) )
return;
// Sbd_ManSolveSelect( p->pGia, p->vMirrors, Pivot, p->vDivVars, p->vDivValues, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots );
RetValue = Sbd_ManCheckConst( p, Pivot );
if ( RetValue >= 0 )
{
Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
//printf( " --> Pivot %4d. Constant %d.\n", Pivot, RetValue );
if ( p->pPars->fVerbose ) printf( "Node %5d: Detected constant %d.\n", Pivot, RetValue );
}
else if ( Sbd_ManExplore3( p, Pivot, &nStrs, Strs ) )
else if ( p->pPars->nLutNum >= 1 && Sbd_ManExplore2( p, Pivot, &Truth ) )
{
Strs->fLut = 1;
Strs->nVarIns = Vec_IntSize( p->vDivSet );
for ( i = 0; i < Strs->nVarIns; i++ )
Strs->VarIns[i] = i;
Strs->Res = Truth;
Sbd_ManImplement2( p, Pivot, 1, Strs );
if ( p->pPars->fVerbose ) printf( "Node %5d: Detected LUT%d\n", Pivot, p->pPars->nLutSize );
}
else if ( p->pPars->nLutNum >= 2 && Sbd_ManExplore3( p, Pivot, &nStrs, Strs ) )
{
//Sbd_ManImplement( p, Pivot, Truth );
Sbd_ManImplement2( p, Pivot, nStrs, Strs );
//printf( " --> Pivot %4d. Supp %d.\n", Pivot, Vec_IntSize(p->vDivSet) );
if ( p->pPars->fVerbose ) printf( "Node %5d: Detected %d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize );
}
/*
else if ( Sbd_ManExplore2( p, Pivot, &Truth ) )
{
int i;
Sbd_Str_t Strs;
Strs.fLut = 1;
Strs.nVarIns = Vec_IntSize( p->vDivSet );
for ( i = 0; i < Strs.nVarIns; i++ )
Strs.VarIns[i] = i;
Strs.Res = Truth;
//Sbd_ManImplement( p, Pivot, Truth );
Sbd_ManImplement2( p, Pivot, 1, &Strs );
//printf( " --> Pivot %4d. Supp %d.\n", Pivot, Vec_IntSize(p->vDivSet) );
}
*/
/*
else
{
extern int Sbd_ProblemSolve(
Gia_Man_t * p, Vec_Int_t * vMirrors,
int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var,
Vec_Int_t * vTfo, Vec_Int_t * vRoots,
Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0
);
// Sbd_Str_t Strs[2] = { {1, 4, {0, 1, 2, 8}}, {1, 4, {3, 4, 5, 6}} };
// Sbd_Str_t Strs[2] = { {1, 4, {1, 4, 5, 7}}, {1, 4, {0, 1, 2, 3}} };
Sbd_Str_t Strs[3] = { {1, 4, {8, 4, 5, 7}}, {1, 4, {0, 1, 2, 3}}, {0, 4, {0, 1, 2, 3}} };
Vec_Int_t * vDivSet = Vec_IntAlloc( 8 );
int i, RetValue;
for ( i = 0; i < 6; i++ )
Vec_IntPush( vDivSet, i+1 );
RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors,
Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,
vDivSet, 3, Strs );
if ( RetValue )
{
printf( "Solving succeded.\n" );
//Sbd_ManImplement2( p, Pivot, Truth, nLuts, nSels, nVarsDivs, pVarsDivs, Truths );
}
Vec_IntFree( vDivSet );
}
*/
}
Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
Sbd_Man_t * p = Sbd_ManStart( pGia, pPars );
int nNodesOld = Gia_ManObjNum(pGia);//, Count = 0;
int nNodesOld = Gia_ManObjNum(pGia);
int k, Pivot;
assert( pPars->nLutSize <= 6 );
//Sbd_ManMergeTest( p );
// prepare references
Gia_ManForEachObj( p->pGia, pObj, Pivot )
Sbd_StoRefObj( p->pSto, Pivot, -1 );
@ -1886,32 +1880,6 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
{
Pivot = Gia_ObjId( pGia, pObj );
if ( Pivot >= nNodesOld )
continue;
if ( Gia_ObjIsAnd(pObj) )
Sbd_NtkPerformOne( p, Pivot );
else if ( Gia_ObjIsCi(pObj) )
{
int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj) );
Vec_IntWriteEntry( p->vLutLevs, Pivot, arrTime );
}
else if ( Gia_ObjIsCo(pObj) )
{
int arrTime = Vec_IntEntry( p->vLutLevs, Gia_ObjFaninId0(pObj, Pivot) );
Tim_ManSetCoArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj), arrTime );
}
else if ( !Gia_ObjIsConst0(pObj) )
assert( 0 );
}
//Tim_ManPrint( pGia->pManTime );
Tim_ManStop( (Tim_Man_t *)pGia->pManTime );
pGia->pManTime = pTimOld;
Vec_IntFree( vNodes );
}
else
{
Gia_ManForEachObj( pGia, pObj, Pivot )
{
if ( Pivot == nNodesOld )
break;
if ( Gia_ObjIsAnd(pObj) )
{
@ -1920,23 +1888,61 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
if ( Delay > 1 )
Sbd_NtkPerformOne( p, Pivot );
}
else if ( !Gia_ObjIsCo(pObj) )
else if ( Gia_ObjIsCi(pObj) )
{
int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj) );
Vec_IntWriteEntry( p->vLutLevs, Pivot, arrTime );
Sbd_StoComputeCutsCi( p->pSto, Pivot, arrTime, arrTime );
}
else if ( Gia_ObjIsCo(pObj) )
{
int arrTime = Vec_IntEntry( p->vLutLevs, Gia_ObjFaninId0(pObj, Pivot) );
Tim_ManSetCoArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj), arrTime );
}
else if ( Gia_ObjIsConst0(pObj) )
Sbd_StoComputeCutsConst0( p->pSto, 0 );
else assert( 0 );
}
//Tim_ManPrint( pGia->pManTime );
Tim_ManStop( (Tim_Man_t *)pGia->pManTime );
pGia->pManTime = pTimOld;
Vec_IntFree( vNodes );
}
else
{
Sbd_StoComputeCutsConst0( p->pSto, 0 );
Gia_ManForEachObj( pGia, pObj, Pivot )
{
if ( Pivot >= nNodesOld )
break;
if ( Gia_ObjIsCi(pObj) )
Sbd_StoComputeCutsCi( p->pSto, Pivot, 0, 0 );
else if ( Gia_ObjIsAnd(pObj) )
{
int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
if ( Delay > 1 )
Sbd_NtkPerformOne( p, Pivot );
}
//if ( nNodesOld != Gia_ManObjNum(pGia) )
// break;
}
}
printf( "Found %d constants and %d replacements with delay %d. ", p->nConsts, p->nChanges, Sbd_ManDelay(p) );
printf( "Found %d constants, %d one-LUT and %d two-LUT replacements with delay %d. ",
p->nLuts[0], p->nLuts[1], p->nLuts[2], Sbd_ManDelay(p) );
p->timeTotal = Abc_Clock() - p->timeTotal;
Abc_PrintTime( 1, "Time", p->timeTotal );
pNew = Sbd_ManDerive( pGia, p->vMirrors );
// print runtime statistics
p->timeOther = p->timeTotal - p->timeWin - p->timeCnf - p->timeSat - p->timeCov - p->timeEnu;
if ( 0 )
p->timeOther = p->timeTotal - p->timeWin - p->timeCnf - p->timeSat - p->timeCov - p->timeEnu - p->timeQbf;
if ( p->pPars->fVerbose )
{
ABC_PRTP( "Win", p->timeWin , p->timeTotal );
ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal );
ABC_PRTP( "Sat", p->timeSat , p->timeTotal );
ABC_PRTP( "Cov", p->timeCov , p->timeTotal );
ABC_PRTP( "Enu", p->timeEnu , p->timeTotal );
ABC_PRTP( "Qbf", p->timeQbf , p->timeTotal );
ABC_PRTP( "Oth", p->timeOther, p->timeTotal );
ABC_PRTP( "ALL", p->timeTotal, p->timeTotal );
}

62
src/opt/sbd/sbdCut.c
View File

@ -40,8 +40,9 @@ struct Sbd_Cut_t_
int iFunc; // functionality
int Cost; // cut cost
int CostLev; // cut cost
unsigned nSlowLeaves : 14; // slow leaves
unsigned nTreeLeaves : 14; // tree leaves
unsigned nTreeLeaves : 9; // tree leaves
unsigned nSlowLeaves : 9; // slow leaves
unsigned nTopLeaves : 10; // top leaves
unsigned nLeaves : 4; // leaf count
int pLeaves[SBD_MAX_CUTSIZE]; // leaves
};
@ -442,13 +443,6 @@ static inline int Sbd_CutCountBits( word i )
i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
return (i*(0x0101010101010101))>>56;
}
static inline int Sbd_CutSlowLeaves( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
{
int i, Count = 0, Delay = Vec_IntEntry(p->vDelays, iObj);
for ( i = 0; i < (int)pCut->nLeaves; i++ )
Count += (Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay >= -1);
return Count;
}
static inline int Sbd_CutCost( Sbd_Sto_t * p, Sbd_Cut_t * pCut )
{
int i, Cost = 0;
@ -470,6 +464,20 @@ static inline int Sbd_CutTreeLeaves( Sbd_Sto_t * p, Sbd_Cut_t * pCut )
Cost += Vec_IntEntry( p->vRefs, pCut->pLeaves[i] ) == 1;
return Cost;
}
static inline int Sbd_CutSlowLeaves( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
{
int i, Count = 0, Delay = Vec_IntEntry(p->vDelays, iObj);
for ( i = 0; i < (int)pCut->nLeaves; i++ )
Count += (Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay >= -1);
return Count;
}
static inline int Sbd_CutTopLeaves( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
{
int i, Count = 0, Delay = Vec_IntEntry(p->vDelays, iObj);
for ( i = 0; i < (int)pCut->nLeaves; i++ )
Count += (Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay == -2);
return Count;
}
static inline void Sbd_CutAddUnit( Sbd_Sto_t * p, int iObj )
{
Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
@ -481,6 +489,14 @@ static inline void Sbd_CutAddUnit( Sbd_Sto_t * p, int iObj )
Vec_IntPush( vThis, iObj );
Vec_IntPush( vThis, 2 );
}
static inline void Sbd_CutAddZero( Sbd_Sto_t * p, int iObj )
{
Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
assert( Vec_IntSize(vThis) == 0 );
Vec_IntPush( vThis, 1 );
Vec_IntPush( vThis, 0 );
Vec_IntPush( vThis, 0 );
}
static inline int Sbd_StoPrepareSet( Sbd_Sto_t * p, int iObj, int Index )
{
Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
@ -495,8 +511,9 @@ static inline int Sbd_StoPrepareSet( Sbd_Sto_t * p, int iObj, int Index )
pCutTemp->Sign = Sbd_CutGetSign( pCutTemp );
pCutTemp->Cost = Sbd_CutCost( p, pCutTemp );
pCutTemp->CostLev = Sbd_CutCostLev( p, pCutTemp );
pCutTemp->nSlowLeaves = Sbd_CutSlowLeaves( p, iObj, pCutTemp );
pCutTemp->nTreeLeaves = Sbd_CutTreeLeaves( p, pCutTemp );
pCutTemp->nSlowLeaves = Sbd_CutSlowLeaves( p, iObj, pCutTemp );
pCutTemp->nTopLeaves = Sbd_CutTopLeaves( p, iObj, pCutTemp );
}
return pList[0];
}
@ -542,6 +559,7 @@ static inline void Sbd_StoComputeSpec( Sbd_Sto_t * p, int iObj, Sbd_Cut_t ** pCu
int i;
for ( i = 0; i < nCuts; i++ )
{
pCuts[i]->nTopLeaves = Sbd_CutTopLeaves( p, iObj, pCuts[i] );
pCuts[i]->nSlowLeaves = Sbd_CutSlowLeaves( p, iObj, pCuts[i] );
p->nCutsSpec += (pCuts[i]->nSlowLeaves == 0);
}
@ -555,8 +573,8 @@ static inline void Sbd_CutPrint( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
printf( " %*d", nDigits, pCut->pLeaves[i] );
for ( ; i < (int)p->nCutSize; i++ )
printf( " %*s", nDigits, " " );
printf( " } Cost = %3d CostL = %3d Slow = %d Tree = %d ",
pCut->Cost, pCut->CostLev, pCut->nSlowLeaves, pCut->nTreeLeaves );
printf( " } Cost = %3d CostL = %3d Tree = %d Slow = %d Top = %d ",
pCut->Cost, pCut->CostLev, pCut->nTreeLeaves, pCut->nSlowLeaves, pCut->nTopLeaves );
printf( "%c ", pCut->nSlowLeaves == 0 ? '*' : ' ' );
for ( i = 0; i < (int)pCut->nLeaves; i++ )
printf( "%3d ", Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay );
@ -607,7 +625,7 @@ void Sbd_StoMergeCuts( Sbd_Sto_t * p, int iObj )
p->nCutsR = nCutsR;
p->Pivot = iObj;
// debug printout
if ( 1 )
if ( 0 )
{
printf( "*** Obj = %4d Delay = %4d NumCuts = %4d\n", iObj, Vec_IntEntry(p->vDelays, iObj), nCutsR );
for ( i = 0; i < nCutsR; i++ )
@ -687,6 +705,11 @@ void Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, int Level )
Vec_WecPushLevel( p->vCuts );
}
}
void Sbd_StoComputeCutsConst0( Sbd_Sto_t * p, int iObj )
{
Sbd_StoComputeCutsObj( p, iObj, 0, 0 );
Sbd_CutAddZero( p, iObj );
}
void Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level )
{
Sbd_StoComputeCutsObj( p, iObj, Delay, Level );
@ -732,11 +755,14 @@ int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int * pLeaves )
Sbd_Cut_t * pCutBest = NULL; int i;
assert( p->Pivot == iObj );
for ( i = 0; i < p->nCutsR; i++ )
{
if ( (int)p->ppCuts[i]->nLeaves > p->nLutSize && (pCutBest == NULL || Sbd_CutCompare2(pCutBest, p->ppCuts[i]) == 1) )
if ( (int)p->ppCuts[i]->nLeaves > p->nLutSize &&
(int)p->ppCuts[i]->nSlowLeaves == 0 &&
(int)p->ppCuts[i]->nTopLeaves <= p->nLutSize-1 &&
(pCutBest == NULL || Sbd_CutCompare2(pCutBest, p->ppCuts[i]) == 1) )
pCutBest = p->ppCuts[i];
}
Sbd_CutPrint( p, iObj, pCutBest );
if ( pCutBest == NULL )
return -1;
//Sbd_CutPrint( p, iObj, pCutBest );
assert( pCutBest->nLeaves <= SBD_DIV_MAX );
for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
pLeaves[i] = pCutBest->pLeaves[i];
@ -751,7 +777,7 @@ void Sbd_StoComputeCutsTest( Gia_Man_t * pGia )
Gia_ManForEachObj( p->pGia, pObj, iObj )
Sbd_StoRefObj( p, iObj, -1 );
// compute cuts
Sbd_StoComputeCutsObj( p, 0, 0, 0 );
Sbd_StoComputeCutsConst0( p, 0 );
Gia_ManForEachCiId( p->pGia, iObj, i )
Sbd_StoComputeCutsCi( p, iObj, 0, 0 );
Gia_ManForEachAnd( p->pGia, pObj, iObj )

3
src/opt/sbd/sbdInt.h
View File

@ -84,7 +84,8 @@ struct Sbd_Str_t_
extern Sbd_Sto_t * Sbd_StoAlloc( Gia_Man_t * pGia, Vec_Int_t * vMirrors, int nLutSize, int nCutSize, int nCutNum, int fCutMin, int fVerbose );
extern void Sbd_StoFree( Sbd_Sto_t * p );
extern void Sbd_StoRefObj( Sbd_Sto_t * p, int iObj, int iMirror );
extern void Sbd_StoDefefObj( Sbd_Sto_t * p, int iObj );
extern void Sbd_StoDerefObj( Sbd_Sto_t * p, int iObj );
extern void Sbd_StoComputeCutsConst0( Sbd_Sto_t * p, int iObj );
extern void Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, int Level );
extern void Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level );
extern int Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj );

17
src/opt/sbd/sbdLut.c
View File

@ -157,7 +157,7 @@ void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits
for ( m = 0; m < nIters; m++, iLit++ )
if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) )
Abc_TtSetBit( &pStr->Res, m );
Abc_TtStretch6( &pStr->Res, pStr->nVarIns, 6 );
pStr->Res = Abc_Tt6Stretch( pStr->Res, pStr->nVarIns );
}
else
{
@ -192,13 +192,12 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
{
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
int fVerbose = 1;
int fVerbose = 0;
abctime clk = Abc_Clock();
Vec_Int_t * vLits = Vec_IntAlloc( 100 );
sat_solver * pSatCec = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 1 );
sat_solver * pSatQbf = sat_solver_new();
//int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
int nVars = Vec_IntSize( vDivSet );
int nPars = Sbd_ProblemCountParams( nStrs, pStr0 );
@ -248,8 +247,6 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
if ( status == l_False ) // solution found
break;
assert( status == l_True );
// Vec_IntForEachEntry( vWinObjs, iVar, i )
// printf( "Node = %4d. SatVar = %4d. Value = %d.\n", iVar, i, sat_solver_var_value(pSatCec, i) );
if ( fVerbose )
{
@ -292,16 +289,16 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
}
if ( Vec_IntSize(vLits) > 0 )
{
Sbd_ProblemPrintSolution( nStrs, pStr0, vLits );
//Sbd_ProblemPrintSolution( nStrs, pStr0, vLits );
Sbd_ProblemCollectSolution( nStrs, pStr0, vLits );
RetValue = 1;
}
else
printf( "Solution does not exist.\n" );
sat_solver_delete( pSatCec );
sat_solver_delete( pSatQbf );
Vec_IntFree( vLits );
if ( fVerbose )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return RetValue;
}