diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 34 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 28 |
2 files changed, 45 insertions, 17 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f57d06ca..88d57e40 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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 ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 0bfd515e..4a74ad7e 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -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,28 +2250,30 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ) return RetValue; } } + // derive the AIG manager + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + { + printf( "Converting miter into AIG has failed.\n" ); + return -1; + } + assert( pMan->nRegs > 0 ); + if ( pSecPar->fTryBmc ) { - RetValue = Abc_NtkDarBmc( pNtk, 0, 20, 100000, -1, 0, 2000, -1, 0, 1, 0, 0, NULL ); + 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 ); + printf( "SOLUTION: FAIL " ); + ABC_PRT( "Time", clock() - clkTotal ); } + Aig_ManStop( pMan ); return RetValue; } } - // derive the AIG manager - pMan = Abc_NtkToDar( pNtk, 0, 1 ); - if ( pMan == NULL ) - { - printf( "Converting miter into AIG has failed.\n" ); - return -1; - } - assert( pMan->nRegs > 0 ); // perform verification if ( pSecPar->fUseNewProver ) { |