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-31 20:21:46 +07:00
parent 54b4692d4b
commit 01924ca118
9 changed files with 444 additions and 196 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

53
src/aig/gia/gia.h
View File

@ -665,21 +665,6 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
}
return Gia_ObjId( p, pObj ) << 1;
}
static inline int Gia_ManAppendAnd2( Gia_Man_t * p, int iLit0, int iLit1 )
{
if ( !p->fGiaSimple )
{
if ( iLit0 < 2 )
return iLit0 ? iLit1 : 0;
if ( iLit1 < 2 )
return iLit1 ? iLit0 : 0;
if ( iLit0 == iLit1 )
return iLit1;
if ( iLit0 == Abc_LitNot(iLit1) )
return 0;
}
return Gia_ManAppendAnd( p, iLit0, iLit1 );
}
static inline int Gia_ManAppendXorReal( Gia_Man_t * p, int iLit0, int iLit1 )
{
Gia_Obj_t * pObj = Gia_ManAppendObj( p );
@ -780,6 +765,44 @@ static inline int Gia_ManAppendXor( Gia_Man_t * p, int iLit0, int iLit1 )
{
return Gia_ManAppendMux( p, iLit0, Abc_LitNot(iLit1), iLit1 );
}
static inline int Gia_ManAppendAnd2( Gia_Man_t * p, int iLit0, int iLit1 )
{
if ( !p->fGiaSimple )
{
if ( iLit0 < 2 )
return iLit0 ? iLit1 : 0;
if ( iLit1 < 2 )
return iLit1 ? iLit0 : 0;
if ( iLit0 == iLit1 )
return iLit1;
if ( iLit0 == Abc_LitNot(iLit1) )
return 0;
}
return Gia_ManAppendAnd( p, iLit0, iLit1 );
}
static inline int Gia_ManAppendOr2( Gia_Man_t * p, int iLit0, int iLit1 )
{
return Abc_LitNot(Gia_ManAppendAnd2( p, Abc_LitNot(iLit0), Abc_LitNot(iLit1) ));
}
static inline int Gia_ManAppendMux2( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
{
int iTemp0 = Gia_ManAppendAnd2( p, Abc_LitNot(iCtrl), iData0 );
int iTemp1 = Gia_ManAppendAnd2( p, iCtrl, iData1 );
return Abc_LitNotCond( Gia_ManAppendAnd2( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), 1 );
}
static inline int Gia_ManAppendMaj2( Gia_Man_t * p, int iData0, int iData1, int iData2 )
{
int iTemp0 = Gia_ManAppendOr2( p, iData1, iData2 );
int iTemp1 = Gia_ManAppendAnd2( p, iData0, iTemp0 );
int iTemp2 = Gia_ManAppendAnd2( p, iData1, iData2 );
return Gia_ManAppendOr2( p, iTemp1, iTemp2 );
}
static inline int Gia_ManAppendXor2( Gia_Man_t * p, int iLit0, int iLit1 )
{
return Gia_ManAppendMux2( p, iLit0, Abc_LitNot(iLit1), iLit1 );
}
static inline void Gia_ManPatchCoDriver( Gia_Man_t * p, int iCoIndex, int iLit0 )
{
Gia_Obj_t * pObjCo = Gia_ManCo( p, iCoIndex );

28
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, "KSWFMCacvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "KSNPWFMCacvwh" ) ) != EOF )
{
switch ( c )
{
@ -41036,6 +41036,28 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nLutNum < 0 )
goto usage;
break;
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
pPars->nCutSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nCutSize < 0 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nCutNum = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nCutNum < 0 )
goto usage;
break;
case 'W':
if ( globalUtilOptind >= argc )
{
@ -41118,10 +41140,12 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &mfsd [-KSWFMC <num>] [-acvwh]\n" );
Abc_Print( -2, "usage: &mfsd [-KSNPWFMC <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-N <num> : the cut size considered for optimization (2 <= num <= 10) [default = %d]\n", pPars->nCutSize );
Abc_Print( -2, "\t-P <num> : the number of cuts computed at a node (1 <= num <= 500) [default = %d]\n", pPars->nCutNum );
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

@ -249,7 +249,7 @@ int Dau_DsdBalance( Gia_Man_t * pGia, int * pFans, int nFans, int fAnd )
iFan = Abc_LitNotCond( iFan, fCompl );
}
else
iFan = Gia_ManAppendXor( pGia, iFan0, iFan1 );
iFan = Gia_ManAppendXor2( pGia, iFan0, iFan1 );
}
else
{

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

@ -40,6 +40,8 @@ struct Sbd_Par_t_
{
int nLutSize; // target LUT size
int nLutNum; // target LUT count
int nCutSize; // target cut size
int nCutNum; // target cut count
int nTfoLevels; // the number of TFO levels (windowing)
int nTfoFanMax; // the max number of fanouts (windowing)
int nWinSizeMax; // maximum window size (windowing)

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

@ -43,12 +43,14 @@ struct Sbd_Man_t_
Vec_Int_t * vCover; // temporary
Vec_Int_t * vLits; // temporary
Vec_Int_t * vLits2; // temporary
int nLuts[3]; // 0=const, 1=1lut, 2=2lut
int nLuts[6]; // 0=const, 1=1lut, 2=2lut, 3=3lut
int nTried;
int nUsed;
abctime timeWin;
abctime timeCut;
abctime timeCov;
abctime timeCnf;
abctime timeSat;
abctime timeCov;
abctime timeEnu;
abctime timeQbf;
abctime timeOther;
abctime timeTotal;
@ -76,8 +78,6 @@ static inline word * Sbd_ObjSim1( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP(
static inline word * Sbd_ObjSim2( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[2], p->pPars->nWords * i ); }
static inline word * Sbd_ObjSim3( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[3], p->pPars->nWords * i ); }
extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -96,17 +96,19 @@ extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_
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)
pPars->nBTLimit = 0; // maximum number of SAT conflicts
pPars->nWords = 1; // simulation word count
pPars->fArea = 0; // area-oriented optimization
pPars->fCover = 0; // use complete cover procedure
pPars->fVerbose = 0; // verbose flag
pPars->fVeryVerbose = 0; // verbose flag
pPars->nLutSize = 4; // target LUT size
pPars->nLutNum = 3; // target LUT count
pPars->nCutSize = (pPars->nLutSize - 1) * pPars->nLutNum + 1; // target cut size
pPars->nCutNum = 128; // target cut count
pPars->nTfoLevels = 5; // the number of TFO levels (windowing)
pPars->nTfoFanMax = 4; // the max number of fanouts (windowing)
pPars->nWinSizeMax = 2000; // maximum window size (windowing)
pPars->nBTLimit = 0; // maximum number of SAT conflicts
pPars->nWords = 1; // simulation word count
pPars->fArea = 0; // area-oriented optimization
pPars->fCover = 0; // use complete cover procedure
pPars->fVerbose = 0; // verbose flag
pPars->fVeryVerbose = 0; // verbose flag
}
/**Function*************************************************************
@ -227,7 +229,7 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
for ( w = 0; w < p->pPars->nWords; w++ )
Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 );
// cut enumeration
p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, 2*pPars->nLutSize-1, 64, 1, 1 );
p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, 1, 1 );
return p;
}
void Sbd_ManStop( Sbd_Man_t * p )
@ -437,6 +439,8 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
Gia_ManIncrementTravId( p->pGia );
Gia_ObjSetTravIdCurrentId(p->pGia, 0);
Sbd_ManWindowSim_rec( p, Pivot );
if ( p->pPars->nWinSizeMax && Vec_IntSize(p->vWinObjs) > p->pPars->nWinSizeMax )
return 0;
Sbd_ManUpdateOrder( p, Pivot );
assert( Vec_IntSize(p->vDivVars) == Vec_IntSize(p->vDivValues) );
assert( Vec_IntSize(p->vDivVars) < Vec_IntSize(p->vWinObjs) );
@ -461,6 +465,8 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
Vec_IntWriteEntry( p->vObj2Var, Abc_Lit2Var(Node), Vec_IntSize(p->vWinObjs) );
Vec_IntPush( p->vWinObjs, Abc_Lit2Var(Node) );
}
if ( p->pPars->nWinSizeMax && Vec_IntSize(p->vWinObjs) > p->pPars->nWinSizeMax )
return 0;
// compute controlability for node
if ( Vec_IntSize(p->vTfo) == 0 )
Abc_TtFill( Sbd_ObjSim2(p, Pivot), p->pPars->nWords );
@ -473,7 +479,7 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
// propagate controlability to fanins for the TFI nodes starting from the pivot
Sbd_ManPropagateControl( p, Pivot );
assert( Vec_IntSize(p->vDivValues) <= 64 );
return (int)(Vec_IntSize(p->vDivValues) > 64);
return (int)(Vec_IntSize(p->vDivValues) <= 64);
}
/**Function*************************************************************
@ -489,10 +495,6 @@ 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 );
@ -984,7 +986,7 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
{
int fVerbose = 0;
abctime clk, clkSat = 0, clkEnu = 0, clkAll = Abc_Clock();
abctime clk;
int nIters, nItersMax = 32;
word MatrS[64] = {0}, MatrC[2][64] = {{0}}, Cubes[2][2][64] = {{{0}}}, Cover[64] = {0}, Cube, CubeNew[2];
@ -1089,14 +1091,10 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
{
if ( p->pPars->fVerbose )
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;
p->timeCov += Abc_Clock() - clk;
return RetValue;
}
clkEnu += Abc_Clock() - clk;
p->timeCov += Abc_Clock() - clk;
if ( p->pPars->fVerbose )
printf( "Candidate support: " ),
@ -1104,7 +1102,7 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
clk = Abc_Clock();
*pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
clkSat += Abc_Clock() - clk;
p->timeSat += Abc_Clock() - clk;
if ( *pTruth == SBD_SAT_UNDEC )
printf( "Node %d: Undecided.\n", Pivot );
@ -1143,19 +1141,12 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
}
//break;
}
//printf( "Node %4d : Iter = %4d Start table = %4d Final table = %4d\n", Pivot, nIters, nRowsOld, nRows );
clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
p->timeSat += clkSat;
p->timeCov += clkAll;
p->timeEnu += clkEnu;
return RetValue;
}
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, clkSat = 0, clkEnu = 0, clkAll;
abctime clk;
word Onset[64] = {0}, Offset[64] = {0}, Cube;
word CoverRows[64] = {0}, CoverCols[64] = {0};
int nIters, nItersMax = 32;
@ -1171,12 +1162,11 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
//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;
p->timeSat += Abc_Clock() - clk;
if ( RetValue >= 0 )
{
if ( p->pPars->fVeryVerbose )
@ -1215,21 +1205,18 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
{
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;
p->timeCov += Abc_Clock() - clk;
return 0;
}
p->timeCov += Abc_Clock() - clk;
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;
p->timeSat += Abc_Clock() - clk;
if ( *pTruth == SBD_SAT_UNDEC )
printf( "Node %d: Undecided.\n", Pivot );
@ -1271,65 +1258,42 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
break;
}
}
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 )
int Sbd_ManExploreCut( Sbd_Man_t * p, int Pivot, int nLeaves, int * pLeaves, int * pnStrs, Sbd_Str_t * Strs, int * pFreeVar )
{
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
);
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 Delay = Vec_IntEntry( p->vLutLevs, Pivot );
int i, k, iObj, nIters, RetValue;
int pNodesTop[SBD_DIV_MAX], pNodesBot[SBD_DIV_MAX], pNodesBot1[SBD_DIV_MAX], pNodesBot2[SBD_DIV_MAX];
int nNodesTop = 0, nNodesBot = 0, nNodesBot1 = 0, nNodesBot2 = 0, nNodesDiff = 0, nNodesDiff1 = 0, nNodesDiff2 = 0;
int i, k, iObj, nIters, RetValue = 0;
int nLeaves, pLeaves[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 );
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
// try to remove fanins
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 )
if ( i != nLeaves-1-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 );
Truth = Sbd_ManSolve( p->pSat, PivotVar, (*pFreeVar)++, 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 )
continue;
{
int DelayDiff = Vec_IntEntry(p->vLutLevs, pLeaves[nLeaves-1-nIters]) - Delay;
if ( DelayDiff > -2 )
return 0;
}
else
pLeaves[nIters] = -1;
pLeaves[nLeaves-1-nIters] = -1;
}
Vec_IntClear( p->vDivSet );
for ( i = 0; i < nLeaves; i++ )
@ -1338,13 +1302,14 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
//printf( "Reduced %d -> %d\n", nLeaves, Vec_IntSize(p->vDivSet) );
if ( Vec_IntSize(p->vDivSet) <= p->pPars->nLutSize )
{
word Truth;
*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 );
Truth = Sbd_ManSolve( p->pSat, PivotVar, (*pFreeVar)++, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
p->timeSat += Abc_Clock() - clk;
assert( Truth != SBD_SAT_UNDEC && Truth != SBD_SAT_SAT );
// create structure
@ -1360,7 +1325,7 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
assert( Vec_IntSize(p->vDivSet) > p->pPars->nLutSize );
// count number of nodes on each level
nNodesTop = 0, nNodesBot = 0;
nNodesTop = nNodesBot = nNodesBot1 = nNodesBot2 = 0;
Vec_IntForEachEntry( p->vDivSet, iObj, i )
{
int DelayDiff = Vec_IntEntry(p->vLutLevs, iObj) - Delay;
@ -1369,60 +1334,227 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
if ( DelayDiff == -2 )
pNodesTop[nNodesTop++] = i;
else // if ( DelayDiff < -2 )
{
pNodesBot[nNodesBot++] = i;
if ( DelayDiff == -3 )
pNodesBot1[nNodesBot1++] = i;
else // if ( DelayDiff < -3 )
pNodesBot2[nNodesBot2++] = i;
}
Vec_IntWriteEntry( p->vDivSet, i, Vec_IntEntry(p->vObj2Var, iObj) );
//pNodeRefs[i] = Gia_ObjRefNumId( p->pGia, iObj );
}
assert( nNodesBot == nNodesBot1 + nNodesBot2 );
if ( i < Vec_IntSize(p->vDivSet) )
return 0;
if ( nNodesTop > p->pPars->nLutSize-1 )
return 0;
if ( nNodesBot > p->pPars->nLutSize )
// try 44
if ( Vec_IntSize(p->vDivSet) <= 2*p->pPars->nLutSize-1 )
{
// move left-over to the top
while ( nNodesBot > p->pPars->nLutSize )
pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot];
assert( nNodesBot == p->pPars->nLutSize );
int nMoved = 0;
if ( nNodesBot > p->pPars->nLutSize ) // need to move bottom left-over to the top
{
while ( nNodesBot > p->pPars->nLutSize )
pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot], nMoved++;
assert( nNodesBot == p->pPars->nLutSize );
}
assert( nNodesBot <= p->pPars->nLutSize );
assert( nNodesTop <= p->pPars->nLutSize-1 );
}
nNodesDiff = p->pPars->nLutSize-1 - nNodesTop;
// number of structures
*pnStrs = 2 + nNodesDiff;
Strs[0].fLut = 1;
Strs[0].nVarIns = p->pPars->nLutSize;
for ( i = 0; i < nNodesTop; i++ )
Strs[0].VarIns[i] = pNodesTop[i];
for ( ; i < p->pPars->nLutSize; i++ )
Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop;
Strs[0].Res = 0;
Strs[0].fLut = 1;
Strs[0].nVarIns = p->pPars->nLutSize;
for ( i = 0; i < nNodesTop; i++ )
Strs[0].VarIns[i] = pNodesTop[i];
for ( ; i < p->pPars->nLutSize; i++ )
Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop;
Strs[0].Res = 0;
Strs[1].fLut = 1;
Strs[1].nVarIns = nNodesBot;
for ( i = 0; i < nNodesBot; i++ )
Strs[1].VarIns[i] = pNodesBot[i];
Strs[1].Res = 0;
for ( k = 0; k < nNodesDiff; k++ )
{
Strs[2+k].fLut = 0;
Strs[2+k].nVarIns = nNodesBot;
Strs[1].fLut = 1;
Strs[1].nVarIns = nNodesBot;
for ( i = 0; i < nNodesBot; i++ )
Strs[2+k].VarIns[i] = pNodesBot[i];
Strs[2+k].Res = 0;
Strs[1].VarIns[i] = pNodesBot[i];
Strs[1].Res = 0;
nNodesDiff = p->pPars->nLutSize-1 - nNodesTop;
assert( nNodesDiff >= 0 && nNodesDiff <= 3 );
for ( k = 0; k < nNodesDiff; k++ )
{
Strs[2+k].fLut = 0;
Strs[2+k].nVarIns = nNodesBot;
for ( i = 0; i < nNodesBot; i++ )
Strs[2+k].VarIns[i] = pNodesBot[i];
Strs[2+k].Res = 0;
}
*pnStrs = 2 + nNodesDiff;
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]++;
while ( nMoved-- )
pNodesBot[nNodesBot++] = pNodesTop[--nNodesTop];
}
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 )
return RetValue;
if ( p->pPars->nLutNum < 3 )
return 0;
if ( Vec_IntSize(p->vDivSet) < 2*p->pPars->nLutSize-1 )
return 0;
if ( RetValue )
p->nLuts[2]++;
// try 444 -- LUT(LUT, LUT)
if ( nNodesTop <= p->pPars->nLutSize-2 )
{
int nMoved = 0;
if ( nNodesBot > 2*p->pPars->nLutSize ) // need to move bottom left-over to the top
{
while ( nNodesBot > 2*p->pPars->nLutSize )
pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot], nMoved++;
assert( nNodesBot == 2*p->pPars->nLutSize );
}
assert( nNodesBot > p->pPars->nLutSize );
assert( nNodesBot <= 2*p->pPars->nLutSize );
assert( nNodesTop <= p->pPars->nLutSize-2 );
Strs[0].fLut = 1;
Strs[0].nVarIns = p->pPars->nLutSize;
for ( i = 0; i < nNodesTop; i++ )
Strs[0].VarIns[i] = pNodesTop[i];
for ( ; i < p->pPars->nLutSize; i++ )
Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop;
Strs[0].Res = 0;
Strs[1].fLut = 1;
Strs[1].nVarIns = p->pPars->nLutSize;
for ( i = 0; i < Strs[1].nVarIns; i++ )
Strs[1].VarIns[i] = pNodesBot[i];
Strs[1].Res = 0;
Strs[2].fLut = 1;
Strs[2].nVarIns = p->pPars->nLutSize;
for ( i = 0; i < Strs[2].nVarIns; i++ )
Strs[2].VarIns[i] = pNodesBot[nNodesBot-p->pPars->nLutSize+i];
Strs[2].Res = 0;
nNodesDiff = p->pPars->nLutSize-2 - nNodesTop;
assert( nNodesDiff >= 0 && nNodesDiff <= 2 );
for ( k = 0; k < nNodesDiff; k++ )
{
Strs[3+k].fLut = 0;
Strs[3+k].nVarIns = nNodesBot;
for ( i = 0; i < nNodesBot; i++ )
Strs[3+k].VarIns[i] = pNodesBot[i];
Strs[3+k].Res = 0;
}
*pnStrs = 3 + nNodesDiff;
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[3]++;
while ( nMoved-- )
pNodesBot[nNodesBot++] = pNodesTop[--nNodesTop];
}
if ( RetValue )
return RetValue;
// try 444 -- LUT(LUT(LUT))
if ( nNodesBot1 + nNodesTop <= 2*p->pPars->nLutSize-2 )
{
if ( nNodesBot2 > p->pPars->nLutSize ) // need to move bottom left-over to the top
{
while ( nNodesBot2 > p->pPars->nLutSize )
pNodesBot1[nNodesBot1++] = pNodesBot2[--nNodesBot2];
assert( nNodesBot2 == p->pPars->nLutSize );
}
if ( nNodesBot1 > p->pPars->nLutSize-1 ) // need to move bottom left-over to the top
{
while ( nNodesBot1 > p->pPars->nLutSize-1 )
pNodesTop[nNodesTop++] = pNodesBot1[--nNodesBot1];
assert( nNodesBot1 == p->pPars->nLutSize-1 );
}
assert( nNodesBot2 <= p->pPars->nLutSize );
assert( nNodesBot1 <= p->pPars->nLutSize-1 );
assert( nNodesTop <= p->pPars->nLutSize-1 );
Strs[0].fLut = 1;
Strs[0].nVarIns = p->pPars->nLutSize;
for ( i = 0; i < nNodesTop; i++ )
Strs[0].VarIns[i] = pNodesTop[i];
Strs[0].VarIns[i++] = Vec_IntSize(p->vDivSet)+1;
for ( ; i < p->pPars->nLutSize; i++ )
Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+2 + i-nNodesTop;
Strs[0].Res = 0;
nNodesDiff1 = p->pPars->nLutSize-1 - nNodesTop;
Strs[1].fLut = 1;
Strs[1].nVarIns = p->pPars->nLutSize;
for ( i = 0; i < nNodesBot1; i++ )
Strs[1].VarIns[i] = pNodesBot1[i];
Strs[1].VarIns[i++] = Vec_IntSize(p->vDivSet)+2;
for ( ; i < p->pPars->nLutSize; i++ )
Strs[1].VarIns[i] = Vec_IntSize(p->vDivSet)+2+nNodesDiff1 + i-nNodesBot1;
Strs[1].Res = 0;
nNodesDiff2 = p->pPars->nLutSize-1 - nNodesBot1;
Strs[2].fLut = 1;
Strs[2].nVarIns = nNodesBot2;
for ( i = 0; i < Strs[2].nVarIns; i++ )
Strs[2].VarIns[i] = pNodesBot2[i];
Strs[2].Res = 0;
nNodesDiff = nNodesDiff1 + nNodesDiff2;
assert( nNodesDiff >= 0 && nNodesDiff <= 3 );
for ( k = 0; k < nNodesDiff; k++ )
{
Strs[3+k].fLut = 0;
Strs[3+k].nVarIns = nNodesBot2;
for ( i = 0; i < nNodesBot2; i++ )
Strs[3+k].VarIns[i] = pNodesBot2[i];
Strs[3+k].Res = 0;
if ( k >= nNodesDiff1 )
continue;
Strs[3+k].nVarIns += nNodesBot1;
for ( i = 0; i < nNodesBot1; i++ )
Strs[3+k].VarIns[nNodesBot2 + i] = pNodesBot1[i];
}
*pnStrs = 3 + nNodesDiff;
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[4]++;
}
return RetValue;
}
int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
{
int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
int FreeVarStart = FreeVar;
int nSize, nLeaves, pLeaves[SBD_DIV_MAX];
//sat_solver_delete_p( &p->pSat );
abctime clk = Abc_Clock();
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
for ( nSize = p->pPars->nLutSize + 1; nSize <= p->pPars->nCutSize; nSize++ )
{
nLeaves = Sbd_StoObjBestCut( p->pSto, Pivot, nSize, pLeaves );
if ( nLeaves == -1 )
continue;
assert( nLeaves == nSize );
if ( Sbd_ManExploreCut( p, Pivot, nLeaves, pLeaves, pnStrs, Strs, &FreeVar ) )
return 1;
}
assert( FreeVar - FreeVarStart <= SBD_FVAR_MAX );
return 0;
}
/**Function*************************************************************
@ -1722,7 +1854,10 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
// extend data-structure to accommodate new nodes
assert( Vec_IntSize(p->vLutLevs) == iObjLast );
for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
{
Vec_IntPush( p->vMirrors, -1 );
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++ )
{
@ -1730,7 +1865,6 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
assert( i == Vec_IntSize(p->vLutLevs) );
Vec_IntPush( p->vLutLevs, Delay );
Vec_IntPush( p->vObj2Var, 0 );
Vec_IntPush( p->vMirrors, -1 );
Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 );
//Sbd_ManFindCut( p, i, p->vLits );
for ( k = 0; k < 4; k++ )
@ -1820,22 +1954,16 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
***********************************************************************/
void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
{
Sbd_Str_t Strs[4];
int i, RetValue, nStrs = 0;
word Truth = 0;
if ( !p->pSto )
{
if ( Sbd_ManMergeCuts( p, Pivot ) )
return;
}
// if ( Pivot != 15 )
// return;
if ( Sbd_ManWindow( p, Pivot ) )
Sbd_Str_t Strs[SBD_DIV_MAX]; word Truth = 0;
int RetValue, nStrs = 0;
if ( !p->pSto && Sbd_ManMergeCuts( p, Pivot ) )
return;
if ( !Sbd_ManWindow( p, Pivot ) )
return;
//if ( Vec_IntSize(p->vWinObjs) > 100 )
// printf( "Obj %d : Win = %d TFO = %d. Roots = %d.\n", Pivot, Vec_IntSize(p->vWinObjs), Vec_IntSize(p->vTfo), Vec_IntSize(p->vRoots) );
p->nTried++;
p->nUsed++;
RetValue = Sbd_ManCheckConst( p, Pivot );
if ( RetValue >= 0 )
{
@ -1844,6 +1972,7 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
}
else if ( p->pPars->nLutNum >= 1 && Sbd_ManExplore2( p, Pivot, &Truth ) )
{
int i;
Strs->fLut = 1;
Strs->nVarIns = Vec_IntSize( p->vDivSet );
for ( i = 0; i < Strs->nVarIns; i++ )
@ -1855,8 +1984,17 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
else if ( p->pPars->nLutNum >= 2 && Sbd_ManExplore3( p, Pivot, &nStrs, Strs ) )
{
Sbd_ManImplement2( p, Pivot, nStrs, Strs );
if ( p->pPars->fVerbose ) printf( "Node %5d: Detected %d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize );
if ( !p->pPars->fVerbose )
return;
if ( Vec_IntSize(p->vDivSet) <= 4 )
printf( "Node %5d: Detected %d\n", Pivot, p->pPars->nLutSize );
else if ( Vec_IntSize(p->vDivSet) <= 6 || (Vec_IntSize(p->vDivSet) == 7 && nStrs == 2) )
printf( "Node %5d: Detected %d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize );
else
printf( "Node %5d: Detected %d%d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize, p->pPars->nLutSize );
}
else
p->nUsed--;
}
Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
{
@ -1875,6 +2013,7 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( pGia );
Tim_Man_t * pTimOld = (Tim_Man_t *)pGia->pManTime;
pGia->pManTime = Tim_ManDup( pTimOld, 1 );
//Tim_ManPrint( pGia->pManTime );
Tim_ManIncrementTravId( (Tim_Man_t *)pGia->pManTime );
Gia_ManForEachObjVec( vNodes, pGia, pObj, k )
{
@ -1883,9 +2022,11 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
break;
if ( Gia_ObjIsAnd(pObj) )
{
abctime clk = Abc_Clock();
int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
p->timeCut += Abc_Clock() - clk;
Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
if ( Delay > 1 )
if ( Delay > 1 )//&& Gia_ObjRefNumId(p->pGia, Pivot) > 1 )
Sbd_NtkPerformOne( p, Pivot );
}
else if ( Gia_ObjIsCi(pObj) )
@ -1903,7 +2044,6 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
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 );
@ -1919,29 +2059,33 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
Sbd_StoComputeCutsCi( p->pSto, Pivot, 0, 0 );
else if ( Gia_ObjIsAnd(pObj) )
{
abctime clk = Abc_Clock();
int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
p->timeCut += Abc_Clock() - clk;
Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
if ( Delay > 1 )
if ( Delay > 1 )//&& Gia_ObjRefNumId(p->pGia, Pivot) > 1 )
Sbd_NtkPerformOne( p, Pivot );
}
//if ( nNodesOld != Gia_ManObjNum(pGia) )
// break;
}
}
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) );
printf( "K = %d. S = %d. N = %d. P = %d. ",
p->pPars->nLutSize, p->pPars->nLutNum, p->pPars->nCutSize, p->pPars->nCutNum );
printf( "Try = %d. Use = %d. C = %d. 1 = %d. 2 = %d. 3a = %d. 3b = %d. Lev = %d. ",
p->nTried, p->nUsed, p->nLuts[0], p->nLuts[1], p->nLuts[2], p->nLuts[3], p->nLuts[4], 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 - p->timeQbf;
if ( p->pPars->fVerbose )
p->timeOther = p->timeTotal - p->timeWin - p->timeCut - p->timeCov - p->timeCnf - p->timeSat - p->timeQbf;
//if ( p->pPars->fVerbose )
{
ABC_PRTP( "Win", p->timeWin , p->timeTotal );
ABC_PRTP( "Cut", p->timeCut , p->timeTotal );
ABC_PRTP( "Cov", p->timeCov , 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 );

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

@ -27,9 +27,9 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define SBD_MAX_CUTSIZE 8
#define SBD_MAX_CUTNUM 1001
#define SBD_MAX_TT_WORDS ((SBD_MAX_CUTSIZE > 6) ? 1 << (SBD_MAX_CUTSIZE-6) : 1)
#define SBD_MAX_CUTSIZE 10
#define SBD_MAX_CUTNUM 501
#define SBD_MAX_TT_WORDS ((SBD_MAX_CUTSIZE > 6) ? 1 << (SBD_MAX_CUTSIZE-6) : 1)
#define SBD_CUT_NO_LEAF 0xF
@ -568,6 +568,7 @@ static inline void Sbd_CutPrint( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
{
int i, nDigits = Abc_Base10Log(Gia_ManObjNum(p->pGia));
int Delay = Vec_IntEntry(p->vDelays, iObj);
if ( pCut == NULL ) { printf( "No cut.\n" ); return; }
printf( "%d {", pCut->nLeaves );
for ( i = 0; i < (int)pCut->nLeaves; i++ )
printf( " %*d", nDigits, pCut->pLeaves[i] );
@ -724,45 +725,88 @@ int Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj )
Sbd_StoMergeCuts( p, iObj );
return Vec_IntEntry( p->vDelays, iObj );
}
int Sbd_StoObjRefs( Sbd_Sto_t * p, int iObj )
{
return Vec_IntEntry(p->vRefs, iObj);
}
void Sbd_StoRefObj( Sbd_Sto_t * p, int iObj, int iMirror )
{
Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
assert( iObj == Vec_IntSize(p->vRefs) );
assert( iMirror < iObj );
Vec_IntPush( p->vRefs, iMirror > 0 ? Vec_IntEntry(p->vRefs, iMirror) : 0 );
Vec_IntPush( p->vRefs, 0 );
//printf( "Ref %d\n", iObj );
if ( iMirror > 0 )
{
Vec_IntWriteEntry( p->vRefs, iObj, Vec_IntEntry(p->vRefs, iMirror) );
Vec_IntWriteEntry( p->vRefs, iMirror, 1 );
}
if ( Gia_ObjIsAnd(pObj) )
{
Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 );
Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId1(pObj, iObj), 1 );
int Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
int Lit1m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) );
int Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
int Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
Vec_IntAddToEntry( p->vRefs, Fan0, 1 );
Vec_IntAddToEntry( p->vRefs, Fan1, 1 );
}
else if ( Gia_ObjIsCo(pObj) )
{
int Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
assert( Lit0m == -1 );
Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 );
}
}
void Sbd_StoDerefObj( Sbd_Sto_t * p, int iObj )
{
Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
Gia_Obj_t * pObj;
int Lit0m, Lit1m, Fan0, Fan1;
return;
pObj = Gia_ManObj(p->pGia, iObj);
if ( Vec_IntEntry(p->vRefs, iObj) == 0 )
printf( "Ref count mismatch at node %d\n", iObj );
assert( Vec_IntEntry(p->vRefs, iObj) > 0 );
Vec_IntAddToEntry( p->vRefs, iObj, -1 );
if ( Vec_IntEntry( p->vRefs, iObj ) > 0 )
return;
if ( Gia_ObjIsCi(pObj) )
return;
//printf( "Deref %d\n", iObj );
assert( Gia_ObjIsAnd(pObj) );
Sbd_StoDerefObj( p, Gia_ObjFaninId0(pObj, iObj) );
Sbd_StoDerefObj( p, Gia_ObjFaninId1(pObj, iObj) );
Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
Lit1m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) );
Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
if ( Fan0 ) Sbd_StoDerefObj( p, Fan0 );
if ( Fan1 ) Sbd_StoDerefObj( p, Fan1 );
}
int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int * pLeaves )
int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves )
{
int fVerbose = 0;
Sbd_Cut_t * pCutBest = NULL; int i;
assert( p->Pivot == iObj );
if ( fVerbose && iObj % 1000 == 0 )
printf( "Node %6d : \n", iObj );
for ( i = 0; i < p->nCutsR; i++ )
{
if ( fVerbose && iObj % 1000 == 0 )
Sbd_CutPrint( p, iObj, p->ppCuts[i] );
if ( nSize && (int)p->ppCuts[i]->nLeaves != nSize )
continue;
if ( (int)p->ppCuts[i]->nLeaves > p->nLutSize &&
(int)p->ppCuts[i]->nSlowLeaves == 0 &&
(int)p->ppCuts[i]->nSlowLeaves <= 1 &&
(int)p->ppCuts[i]->nTopLeaves <= p->nLutSize-1 &&
(pCutBest == NULL || Sbd_CutCompare2(pCutBest, p->ppCuts[i]) == 1) )
pCutBest = p->ppCuts[i];
}
if ( fVerbose && iObj % 1000 == 0 )
{
printf( "Best cut of size %d:\n", nSize );
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];

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

@ -52,9 +52,10 @@ ABC_NAMESPACE_HEADER_START
#define SBD_SAT_UNDEC 0x1234567812345678
#define SBD_SAT_SAT 0x8765432187654321
#define SBD_LUTS_MAX 2
#define SBD_SIZE_MAX 4
#define SBD_DIV_MAX 8
#define SBD_LUTS_MAX 2
#define SBD_SIZE_MAX 4
#define SBD_DIV_MAX 10
#define SBD_FVAR_MAX 100
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
@ -81,16 +82,28 @@ struct Sbd_Str_t_
////////////////////////////////////////////////////////////////////////
/*=== sbdCut.c ==========================================================*/
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_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 );
extern int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int * pLeaves );
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 int Sbd_StoObjRefs( Sbd_Sto_t * p, int iObj );
extern void Sbd_StoRefObj( Sbd_Sto_t * p, int iObj, int iMirror );
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 );
extern int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves );
/*=== sbdWin.c ==========================================================*/
extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp );
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_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds );
extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset );
/*=== sbdQbf.c ==========================================================*/
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
);
ABC_NAMESPACE_HEADER_END

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

@ -96,7 +96,6 @@ int Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars,
}
}
}
//printf( "Stop par = %d.\n", VarPar );
return 1;
}
void Sbd_ProblemAddClausesInit( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 )

5
src/opt/sbd/sbdWin.c
View File

@ -54,7 +54,6 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf )
{
Gia_Obj_t * pObj;
int nAddVars = 64;
int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue;
int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo);
int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
@ -67,7 +66,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
pSat = sat_solver_new();
else
sat_solver_restart( pSat );
sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + nAddVars );
sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + SBD_FVAR_MAX );
// create constant 0 clause
sat_solver_addclause( pSat, &iLit, &iLit + 1 );
// add clauses for all nodes
@ -139,7 +138,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
sat_solver_delete( pSat );
return NULL;
}
assert( sat_solver_nvars(pSat) == nVars + nAddVars );
assert( sat_solver_nvars(pSat) == nVars + SBD_FVAR_MAX );
}
else if ( fQbf )
{