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

Replaced 'bmc' by 'bmc2' in 'dprove'. Added switches to 'dprove' to control BMC frames and conflicts.

This commit is contained in:
Alan Mishchenko 2012-01-19 14:24:56 -08:00
parent 0111d43b54
commit fffd733f94
5 changed files with 51 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/saig/saigBmc.c
View File

@ -211,7 +211,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
*piFrame = nFrames;
if ( fVerbose )
{
printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
printf( "Running \"bmc\". AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ",

2
src/aig/saig/saigBmc2.c
View File

@ -762,7 +762,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
if ( fVerbose )
{
printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
printf( "Running \"bmc2\". AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n",

2
src/aig/saig/saigBmc3.c
View File

@ -1114,7 +1114,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
p->pPars = pPars;
if ( pPars->fVerbose )
{
printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d. Map = %6d. Sect =%3d.\n",
printf( "Running \"bmc3\". AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d. Map = %6d. Sect =%3d.\n",
Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), (Vec_IntSize(p->vMapping)-Aig_ManObjNumMax(pAig))/5, Vec_VecSize(p->vSects) );
printf( "Params: Start = %d. FramesMax = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n",

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

@ -17620,14 +17620,16 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c;
char * pLogFileName = NULL;
int nBmcFramesMax = 20;
int nBmcConfMax = 2000;
extern void Fra_SecSetDefaultParams( Fra_Sec_t * p );
extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar );
extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, int nBmcConfMax );
// set defaults
Fra_SecSetDefaultParams( pSecPar );
// pSecPar->TimeLimit = 300;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRTLarmfijkoupwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "cbAEFCGDVBRTLarmfijkoupwvh" ) ) != EOF )
{
switch ( c )
{
@ -17637,6 +17639,28 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'b':
pSecPar->fTryBmc ^= 1;
break;
case 'A':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
goto usage;
}
nBmcFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nBmcFramesMax < 0 )
goto usage;
break;
case 'E':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-E\" should be followed by an integer.\n" );
goto usage;
}
nBmcConfMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nBmcConfMax < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
@ -17787,7 +17811,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// perform verification
pAbc->Status = Abc_NtkDarProve( pNtk, pSecPar );
pAbc->Status = Abc_NtkDarProve( pNtk, pSecPar, nBmcFramesMax, nBmcConfMax );
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "dprove" );
@ -17806,8 +17830,10 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: dprove [-FCGDVBRT num] [-L file] [-cbarmfijoupvwh]\n" );
Abc_Print( -2, "usage: dprove [-AEFCGDVBRT num] [-L file] [-cbarmfijoupvwh]\n" );
Abc_Print( -2, "\t performs SEC on the sequential miter\n" );
Abc_Print( -2, "\t-A num : the limit on the depth of BMC [default = %d]\n", nBmcFramesMax );
Abc_Print( -2, "\t-E num : the conflict limit during BMC [default = %d]\n", nBmcConfMax );
Abc_Print( -2, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
Abc_Print( -2, "\t-C num : the conflict limit at a node during induction [default = %d]\n", pSecPar->nBTLimit );
Abc_Print( -2, "\t-G num : the global conflict limit during induction [default = %d]\n", pSecPar->nBTLimitGlobal );

34
src/base/abci/abcDar.c
View File

@ -2204,10 +2204,10 @@ int Abc_NtkDarDemiterDual( Abc_Ntk_t * pNtk, int fVerbose )
SeeAlso []
***********************************************************************/
int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, int nBmcConfMax )
{
Aig_Man_t * pMan;
int RetValue = -1, clkTotal = clock();
int iFrame = -1, RetValue = -1, clkTotal = clock();
if ( pSecPar->fTryComb || Abc_NtkLatchNum(pNtk) == 0 )
{
Prove_Params_t Params, * pParams = &Params;
@ -2250,20 +2250,6 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
return RetValue;
}
}
if ( pSecPar->fTryBmc )
{
RetValue = Abc_NtkDarBmc( pNtk, 0, 20, 100000, -1, 0, 2000, -1, 0, 1, 0, 0, NULL );
if ( RetValue == 0 )
{
printf( "Networks are not equivalent.\n" );
if ( pSecPar->fReportSolution )
{
printf( "SOLUTION: FAIL " );
ABC_PRT( "Time", clock() - clkTotal );
}
return RetValue;
}
}
// derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
@ -2272,6 +2258,22 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
return -1;
}
assert( pMan->nRegs > 0 );
if ( pSecPar->fTryBmc )
{
RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame );
if ( RetValue == 0 )
{
printf( "Networks are not equivalent.\n" );
if ( pSecPar->fReportSolution )
{
printf( "SOLUTION: FAIL " );
ABC_PRT( "Time", clock() - clkTotal );
}
Aig_ManStop( pMan );
return RetValue;
}
}
// perform verification
if ( pSecPar->fUseNewProver )
{