diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-03 21:34:46 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-03 21:34:46 -0800 |
commit | e6f874477709536c246417583c60d386658dcc49 (patch) | |
tree | 7a1924587d09b15829f5ed7f1f235006052f6856 /src/base/abci | |
parent | 59d7455cf16cc2be722b5f224801bcd1b600134e (diff) | |
download | abc-e6f874477709536c246417583c60d386658dcc49.tar.gz abc-e6f874477709536c246417583c60d386658dcc49.tar.bz2 abc-e6f874477709536c246417583c60d386658dcc49.zip |
Make PDR return the number of completed frames.
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 50 |
1 files changed, 25 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 ); |