From fffd733f948622f39bacd2545100dd799f5a3140 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 19 Jan 2012 14:24:56 -0800 Subject: Replaced 'bmc' by 'bmc2' in 'dprove'. Added switches to 'dprove' to control BMC frames and conflicts. --- src/aig/saig/saigBmc.c | 2 +- src/aig/saig/saigBmc2.c | 2 +- src/aig/saig/saigBmc3.c | 2 +- src/base/abci/abc.c | 34 ++++++++++++++++++++++++++++++---- src/base/abci/abcDar.c | 28 +++++++++++++++------------- 5 files changed, 48 insertions(+), 20 deletions(-) (limited to 'src') diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index cb506054..011a746e 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -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. ", diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index 8d9f4ac8..169b9404 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -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", diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 2dd7cbe3..2035ac72 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -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", 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 ) { -- cgit v1.2.3