Skip to content

A
abc
Commit d080336b by Alan Mishchenko
Options

Added new feature to bmc3.

parent 8f74276e
Showing with 87 additions and 35 deletions
src/aig/saig/saig.h
......@@ -58,18 +58,21 @@ struct Sec_MtrStatus_t_
typedef struct Saig_ParBmc_t_ Saig_ParBmc_t;
struct Saig_ParBmc_t_
{
int nStart; // starting timeframe
int nFramesMax; // maximum number of timeframes
int nConfLimit; // maximum number of conflicts at a node
int nTimeOut; // approximate timeout in seconds
int nPisAbstract; // the number of PIs to abstract
int fSolveAll; // does not stop at the first SAT output
int fDropSatOuts; // replace sat outputs by constant 0
int nFfToAddMax; // max number of flops to add during CBA
int fVerbose; // verbose
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
int nStart; // starting timeframe
int nFramesMax; // maximum number of timeframes
int nConfLimit; // maximum number of conflicts at a node
int nConfLimitJump; // maximum number of conflicts after jumping
int nFramesJump; // the number of tiemframes to jump
int nTimeOut; // approximate timeout in seconds
int nPisAbstract; // the number of PIs to abstract
int fSolveAll; // does not stop at the first SAT output
int fDropSatOuts; // replace sat outputs by constant 0
int nFfToAddMax; // max number of flops to add during CBA
int fVerbose; // verbose
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
};
typedef struct Saig_ParBbr_t_ Saig_ParBbr_t;
struct Saig_ParBbr_t_
......
src/aig/saig/saigBmc3.c
......@@ -1073,6 +1073,8 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
p->nStart = 0; // maximum number of timeframes
p->nFramesMax = 2000; // maximum number of timeframes
p->nConfLimit = 2000; // maximum number of conflicts at a node
p->nConfLimitJump = 0; // maximum number of conflicts after jumping
p->nFramesJump = 0; // the number of tiemframes to jump
p->nTimeOut = 0; // approximate timeout in seconds
p->nPisAbstract = 0; // the number of PIs to abstract
p->fSolveAll = 0; // stops on the first SAT instance
......@@ -1097,7 +1099,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
{
Gia_ManBmc_t * p;
Aig_Obj_t * pObj;
int RetValue = -1, fFirst = 1;
int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
int nOutDigits = Aig_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock();
if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 )
......@@ -1133,7 +1135,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
return 0;
}
// consider the next timeframe
if ( RetValue == -1 && pPars->nStart == 0 )
if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame )
pPars->iFrame = f-1;
// resize the array
Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 );
......@@ -1173,7 +1175,7 @@ clkOther += clock() - clk2;
return 1;
}
}
if ( pPars->nStart && f < pPars->nStart )
if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
continue;
// solve SAT
clk = clock();
......@@ -1211,6 +1213,7 @@ clkOther += clock() - clk2;
continue;
}
// solve this output
fUnfinished = 0;
sat_solver_compress( p->pSat );
status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_False )
......@@ -1232,7 +1235,7 @@ clkOther += clock() - clk2;
//ABC_PRT( "CNF generation runtime", clkOther );
if ( pPars->fVerbose )
{
printf( "%3d : ", f );
printf( "%3d %s : ", f, fUnfinished ? "-" : "+" );
printf( "Var =%8.0f. ", (double)p->nSatVars );
printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
......@@ -1261,6 +1264,19 @@ clkOther += clock() - clk2;
else
{
assert( status == l_Undef );
if ( pPars->nTimeOut && ((float)pPars->nTimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{
printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut );
Saig_Bmc3ManStop( p );
return RetValue;
}
if ( pPars->nFramesJump )
{
pPars->nConfLimit = pPars->nConfLimitJump;
nJumpFrame = f + pPars->nFramesJump;
fUnfinished = 1;
break;
}
Saig_Bmc3ManStop( p );
return RetValue;
}
......@@ -1278,7 +1294,7 @@ clkOther += clock() - clk2;
fFirst = 0;
// printf( "Outputs of frames up to %d are trivially UNSAT.\n", f );
}
printf( "%3d : ", f );
printf( "%3d %s : ", f, fUnfinished ? "-" : "+" );
printf( "Var =%8.0f. ", (double)p->nSatVars );
printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
......@@ -1293,7 +1309,9 @@ clkOther += clock() - clk2;
}
}
// consider the next timeframe
if ( RetValue == -1 && pPars->nStart == 0 )
if ( nJumpFrame && pPars->nStart == 0 )
pPars->iFrame = nJumpFrame - pPars->nFramesJump;
else if ( RetValue == -1 && pPars->nStart == 0 )
pPars->iFrame = f;
//ABC_PRT( "CNF generation runtime", clkOther );
if ( pPars->fVerbose )
......
src/base/abci/abc.c
......@@ -19017,7 +19017,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCILsdrvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCDJILsdrvh" ) ) != EOF )
{
switch ( c )
{
......@@ -19065,6 +19065,28 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nConfLimit < 0 )
goto usage;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
pPars->nConfLimitJump = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nConfLimitJump < 0 )
goto usage;
break;
case 'J':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesJump = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesJump < 0 )
goto usage;
break;
case 'I':
if ( globalUtilOptind >= argc )
{
......@@ -19144,12 +19166,14 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: bmc3 [-SFTCI num] [-L file] [-sdvh]\n" );
Abc_Print( -2, "usage: bmc3 [-SFTCDJI num] [-L file] [-sdvh]\n" );
Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" );
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of time frames [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-C num : max conflicts at an output [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump );
Abc_Print( -2, "\t-J num : the number of timeframes to jump (0 = not used) [default = %d]\n", pPars->nFramesJump );
Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n", pPars->nPisAbstract );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-s : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" );
......
src/map/if/ifDec10f.c
......@@ -27,6 +27,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define CLU_MAX 16
// the bit count for the first 256 integer numbers
static int BitCount8[256] = {
0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
......@@ -55,18 +57,7 @@ static word Truth6[6] = {
0xFFFF0000FFFF0000,
0xFFFFFFFF00000000
};
static word Truth10[10][16] = {
0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,
0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,
0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,
0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,
0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,
0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,
0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,
0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,
0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,
0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF
};
static word TruthAll[CLU_MAX][1 << (CLU_MAX-6)];
extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
......@@ -76,10 +67,26 @@ extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
// moving up means moving from LSB -> MSB
// groups list vars indices from MSB to LSB
// group representation
// nVars | nCofs | v5 | v4 | v3 | v2 | v1 | v0
// if nCofs > 2, v0 is the shared variable
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
void If_CluInitTruthTables()
{
int i, k;
assert( CLU_MAX <= 16 );
for ( i = 0; i < 6; i++ )
for ( k = 0; k < (1 << (CLU_MAX-6)); k++ )
TruthAll[i][k] = Truth6[i];
for ( i = 6; i < CLU_MAX; i++ )
for ( k = 0; k < (1 << (CLU_MAX-6)); k++ )
TruthAll[i][k] = ((k >> i) & 1) ? ~0 : 0;
}
// variable permutation for large functions
static inline int If_CluWordNum( int nVars )
{
......@@ -131,7 +138,7 @@ static inline void If_CluSwapAdjacent( word * pOut, word * pIn, int iVar, int nV
// moves one var (v) to the given position (p)
void If_CluMoveVarOneUp( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int v, int p )
{
word pG[16], * pIn = pF, * pOut = pG, * pTemp;
word pG[32], * pIn = pF, * pOut = pG, * pTemp;
int iPlace0, iPlace1, Count = 0;
assert( v >= 0 && v < nVars );
assert( Var2Pla[v] >= p );
......@@ -156,7 +163,7 @@ void If_CluMoveVarOneUp( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int
// moves one var (v) to the given position (p)
void If_CluMoveVarOneDown( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int v, int p )
{
word pG[16], * pIn = pF, * pOut = pG, * pTemp;
word pG[32], * pIn = pF, * pOut = pG, * pTemp;
int iPlace0, iPlace1, Count = 0;
assert( v >= 0 && v < nVars );
assert( Var2Pla[v] <= p );
......@@ -194,7 +201,7 @@ int If_CluCountCofs( word * pF, int * V2P, int * P2V, int nVars, int nBSsize )
word iCofs[16], iCof;
int i, c, nMints = (1 << nBSsize), nCofs = 1;
assert( nBSsize >= 3 && nBSsize <= 5 );
assert( nVars - nBSsize >= 0 && nVars - nBSsize <= 6 );
assert( nVars - nBSsize > 0 && nVars - nBSsize <= 6 );
if ( nVars - nBSsize == 6 )
Mask = ~0;
iCofs[0] = pF[0] & Mask;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment