From e6f874477709536c246417583c60d386658dcc49 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 3 Feb 2011 21:34:46 -0800 Subject: Make PDR return the number of completed frames. --- src/base/abci/abc.c | 50 +++++++++++++++++++++++++------------------------- src/sat/pdr/pdr.h | 1 + src/sat/pdr/pdrCore.c | 7 +++++++ 3 files changed, 33 insertions(+), 25 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 804bd058..efdf3c94 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -369,9 +369,9 @@ static int Abc_CommandAbc9AbsRefine ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9PbaStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Reach ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Reach2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Reach3 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9ReachM ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9ReachP ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9ReachN ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Undo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -767,9 +767,9 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&pba_start", Abc_CommandAbc9PbaStart, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&posplit", Abc_CommandAbc9Posplit, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&reach", Abc_CommandAbc9Reach, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&reach2", Abc_CommandAbc9Reach2, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&reach3", Abc_CommandAbc9Reach3, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&reachm", Abc_CommandAbc9ReachM, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&reachp", Abc_CommandAbc9ReachP, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&reachn", Abc_CommandAbc9ReachN, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&undo", Abc_CommandAbc9Undo, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); @@ -20007,7 +20007,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) } // run the procedure pAbc->Status = Abc_NtkDarPdr( pNtk, pPars, &pCex ); - pAbc->nFrames = pCex ? pCex->iFrame : -1; + pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pCex ); return 0; @@ -27457,7 +27457,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9Reach( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAbc9ReachM( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_ParLlb_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); @@ -27582,24 +27582,24 @@ int Abc_CommandAbc9Reach( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9Reach(): There is no AIG.\n" ); + Abc_Print( -1, "Abc_CommandAbc9ReachM(): There is no AIG.\n" ); return 1; } if ( Gia_ManRegNum(pAbc->pGia) == 0 ) { - Abc_Print( -1, "Abc_CommandAbc9Reach(): The current AIG has no latches.\n" ); + Abc_Print( -1, "Abc_CommandAbc9ReachM(): The current AIG has no latches.\n" ); return 0; } pAbc->Status = Llb_ManModelCheckGia( pAbc->pGia, pPars ); pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); if ( pLogFileName ) - Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reach" ); + Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reachm" ); return 0; usage: - Abc_Print( -2, "usage: &reach [-TBFCHS num] [-L file] [-ripcsyzvwh]\n" ); - Abc_Print( -2, "\t model checking via BDD-based reachability (similar to IWLS'95)\n" ); + Abc_Print( -2, "usage: &reachm [-TBFCHS num] [-L file] [-ripcsyzvwh]\n" ); + Abc_Print( -2, "\t model checking via BDD-based reachability (dependence-matrix-based)\n" ); Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-B num : max number of nodes in the intermediate BDDs [default = %d]\n", pPars->nBddMax ); Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax ); @@ -27631,7 +27631,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9Reach2( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAbc9ReachP( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_ParLlb_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); @@ -27729,12 +27729,12 @@ int Abc_CommandAbc9Reach2( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9Reach(): There is no AIG.\n" ); + Abc_Print( -1, "Abc_CommandAbc9ReachP(): There is no AIG.\n" ); return 1; } if ( Gia_ManRegNum(pAbc->pGia) == 0 ) { - Abc_Print( -1, "Abc_CommandAbc9Reach(): The current AIG has no latches.\n" ); + Abc_Print( -1, "Abc_CommandAbc9ReachP(): The current AIG has no latches.\n" ); return 0; } pMan = Gia_ManToAigSimple( pAbc->pGia ); @@ -27742,13 +27742,13 @@ int Abc_CommandAbc9Reach2( Abc_Frame_t * pAbc, int argc, char ** argv ) pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel ); if ( pLogFileName ) - Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reach2" ); + Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reachp" ); Aig_ManStop( pMan ); return 0; usage: - Abc_Print( -2, "usage: &reach2 [-NFT num] [-L file] [-rbyzdvwh]\n" ); - Abc_Print( -2, "\t model checking via BDD-based reachability (min-cut-based)\n" ); + Abc_Print( -2, "usage: &reachp [-NFT num] [-L file] [-rbyzdvwh]\n" ); + Abc_Print( -2, "\t model checking via BDD-based reachability (partitioning-based)\n" ); Abc_Print( -2, "\t-N num : partitioning value (MinVol=nANDs/N/2; MaxVol=nANDs/N) [default = %d]\n", pPars->nPartValue ); // Abc_Print( -2, "\t-B num : the BDD node increase when hints kick in [default = %d]\n", pPars->nBddMax ); Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax ); @@ -27776,7 +27776,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9Reach3( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAbc9ReachN( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_ParLlb_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); @@ -27857,12 +27857,12 @@ int Abc_CommandAbc9Reach3( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9Reach(): There is no AIG.\n" ); + Abc_Print( -1, "Abc_CommandAbc9ReachN(): There is no AIG.\n" ); return 1; } if ( Gia_ManRegNum(pAbc->pGia) == 0 ) { - Abc_Print( -1, "Abc_CommandAbc9Reach(): The current AIG has no latches.\n" ); + Abc_Print( -1, "Abc_CommandAbc9ReachN(): The current AIG has no latches.\n" ); return 0; } pMan = Gia_ManToAigSimple( pAbc->pGia ); @@ -27870,13 +27870,13 @@ int Abc_CommandAbc9Reach3( Abc_Frame_t * pAbc, int argc, char ** argv ) pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel ); if ( pLogFileName ) - Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reach2" ); + Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reachn" ); Aig_ManStop( pMan ); return 0; usage: - Abc_Print( -2, "usage: &reach3 [-BFT num] [-L file] [-ryzvh]\n" ); - Abc_Print( -2, "\t model checking via BDD-based reachability (non-linear QS)\n" ); + Abc_Print( -2, "usage: &reachn [-BFT num] [-L file] [-ryzvh]\n" ); + Abc_Print( -2, "\t model checking via BDD-based reachability (non-linear-QS-based)\n" ); Abc_Print( -2, "\t-B num : the BDD node increase when hints kick in [default = %d]\n", pPars->nBddMax ); Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax ); Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit ); diff --git a/src/sat/pdr/pdr.h b/src/sat/pdr/pdr.h index 1099c621..27e76b6e 100644 --- a/src/sat/pdr/pdr.h +++ b/src/sat/pdr/pdr.h @@ -51,6 +51,7 @@ struct Pdr_Par_t_ int fShortest; // forces bug traces to be shortest int fVerbose; // verbose output int fVeryVerbose; // very verbose output + int iFrame; // explored up to this frame }; //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c index f1c10443..8b58bde1 100644 --- a/src/sat/pdr/pdrCore.c +++ b/src/sat/pdr/pdrCore.c @@ -56,6 +56,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->fShortest = 0; // forces bug traces to be shortest pPars->fVerbose = 0; // verbose output pPars->fVeryVerbose = 0; // very verbose output + pPars->iFrame = -1; // explored up to this frame } /**Function************************************************************* @@ -544,6 +545,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + p->pPars->iFrame = k; return -1; } if ( RetValue == 0 ) @@ -554,6 +556,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + p->pPars->iFrame = k; return -1; } if ( RetValue == 0 ) @@ -565,6 +568,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) } if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + p->pPars->iFrame = k; return 0; // SAT } } @@ -590,6 +594,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManVerifyInvariant( p ); if ( p->pPars->fDumpInv ) Pdr_ManDumpClauses( p, (char *)"inv.pla" ); + p->pPars->iFrame = k; return 1; // UNSAT } if ( p->pPars->fVerbose ) @@ -608,6 +613,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); printf( "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); + p->pPars->iFrame = k; return -1; } if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax ) @@ -615,6 +621,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax ); + p->pPars->iFrame = k; return -1; } } -- cgit v1.2.3