mirror of https://github.com/YosysHQ/abc.git
clean up
This commit is contained in:
Yen-Sheng Ho
parent
01e6beea8e
commit
fb2fbd70bd
|
|
@ -333,7 +333,6 @@ static int Abc_CommandBm2 ( Abc_Frame_t * pAbc, int argc, cha
|
|||
static int Abc_CommandSaucy ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandTestCex ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandPdr ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandIPdr ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
#ifdef ABC_USE_CUDD
|
||||
static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
#endif
|
||||
|
|
@ -984,7 +983,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
|||
Cmd_CommandAdd( pAbc, "Verification", "saucy3", Abc_CommandSaucy, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Verification", "testcex", Abc_CommandTestCex, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Verification", "pdr", Abc_CommandPdr, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Verification", "ipdr", Abc_CommandIPdr, 0 );
|
||||
#ifdef ABC_USE_CUDD
|
||||
Cmd_CommandAdd( pAbc, "Verification", "reconcile", Abc_CommandReconcile, 1 );
|
||||
#endif
|
||||
|
|
@ -26417,273 +26415,6 @@ usage:
|
|||
|
||||
|
||||
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_CommandIPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars );
|
||||
extern int Abc_NtkDarIPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars );
|
||||
Pdr_Par_t Pars, * pPars = &Pars;
|
||||
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
|
||||
int c;
|
||||
Pdr_ManSetDefaultParams( pPars );
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfsipdegjonctkvwzh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'M':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nRecycle = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nRecycle < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'F':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nFrameMax = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nFrameMax < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'C':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nConfLimit = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nConfLimit < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'D':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nConfGenLimit = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nConfGenLimit < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'Q':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nRestLimit = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nRestLimit < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'T':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nTimeOut = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nTimeOut < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'H':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nTimeOutOne = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nTimeOutOne < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'G':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nTimeOutGap = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nTimeOutGap < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'S':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nRandomSeed = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nRandomSeed < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'a':
|
||||
pPars->fSolveAll ^= 1;
|
||||
break;
|
||||
case 'x':
|
||||
pPars->fStoreCex ^= 1;
|
||||
break;
|
||||
case 'r':
|
||||
pPars->fTwoRounds ^= 1;
|
||||
break;
|
||||
case 'm':
|
||||
pPars->fMonoCnf ^= 1;
|
||||
break;
|
||||
case 'u':
|
||||
pPars->fNewXSim ^= 1;
|
||||
break;
|
||||
case 'y':
|
||||
pPars->fFlopPrio ^= 1;
|
||||
break;
|
||||
case 'f':
|
||||
pPars->fFlopOrder ^= 1;
|
||||
break;
|
||||
case 's':
|
||||
pPars->fShortest ^= 1;
|
||||
break;
|
||||
case 'i':
|
||||
pPars->fShiftStart ^= 1;
|
||||
break;
|
||||
case 'p':
|
||||
pPars->fReuseProofOblig ^= 1;
|
||||
break;
|
||||
case 'd':
|
||||
pPars->fDumpInv ^= 1;
|
||||
break;
|
||||
case 'e':
|
||||
pPars->fUseSupp ^= 1;
|
||||
break;
|
||||
case 'g':
|
||||
pPars->fSkipGeneral ^= 1;
|
||||
break;
|
||||
case 'j':
|
||||
pPars->fSimpleGeneral ^= 1;
|
||||
break;
|
||||
case 'o':
|
||||
pPars->fUsePropOut ^= 1;
|
||||
break;
|
||||
case 'n':
|
||||
pPars->fSkipDown ^= 1;
|
||||
break;
|
||||
case 'c':
|
||||
pPars->fCtgs ^= 1;
|
||||
break;
|
||||
case 't':
|
||||
pPars->fUseAbs ^= 1;
|
||||
break;
|
||||
case 'k':
|
||||
pPars->fUseSimpleRef ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
pPars->fVerbose ^= 1;
|
||||
break;
|
||||
case 'w':
|
||||
pPars->fVeryVerbose ^= 1;
|
||||
break;
|
||||
case 'z':
|
||||
pPars->fNotVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( pNtk == NULL )
|
||||
{
|
||||
Abc_Print( -2, "There is no current network.\n");
|
||||
return 0;
|
||||
}
|
||||
if ( Abc_NtkLatchNum(pNtk) == 0 )
|
||||
{
|
||||
Abc_Print( 0, "The current network is combinational.\n");
|
||||
return 0;
|
||||
}
|
||||
if ( !Abc_NtkIsStrash(pNtk) )
|
||||
{
|
||||
Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n");
|
||||
return 0;
|
||||
}
|
||||
// run the procedure
|
||||
pPars->fUseBridge = pAbc->fBridgeMode;
|
||||
pAbc->Status = Abc_NtkDarIPdr( pNtk, pPars );
|
||||
pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;
|
||||
Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap );
|
||||
if ( pNtk->vSeqModelVec )
|
||||
Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
|
||||
else
|
||||
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: ipdr [-MFCDQTHGS <num>] [-axrmuyfsipdegjonctkvwzh]\n" );
|
||||
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
|
||||
Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
|
||||
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
|
||||
Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle );
|
||||
Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax );
|
||||
Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit );
|
||||
Abc_Print( -2, "\t-D num : limit on conflicts during ind-generalization (0 = no limit) [default = %d]\n",pPars->nConfGenLimit );
|
||||
Abc_Print( -2, "\t-Q num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit );
|
||||
Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut );
|
||||
Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne );
|
||||
Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n", pPars->nTimeOutGap );
|
||||
Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed );
|
||||
Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" );
|
||||
Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" );
|
||||
Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" );
|
||||
Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" );
|
||||
Abc_Print( -2, "\t-u : toggle updated X-valued simulation [default = %s]\n", pPars->fNewXSim? "yes": "no" );
|
||||
Abc_Print( -2, "\t-y : toggle using structural flop priorities [default = %s]\n", pPars->fFlopPrio? "yes": "no" );
|
||||
Abc_Print( -2, "\t-f : toggle ordering flops by cost before generalization [default = %s]\n", pPars->fFlopOrder? "yes": "no" );
|
||||
Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" );
|
||||
Abc_Print( -2, "\t-i : toggle clause pushing from an intermediate timeframe [default = %s]\n", pPars->fShiftStart? "yes": "no" );
|
||||
Abc_Print( -2, "\t-p : toggle reusing proof-obligations in the last timeframe [default = %s]\n", pPars->fReuseProofOblig? "yes": "no" );
|
||||
Abc_Print( -2, "\t-d : toggle dumping invariant (valid if init state is all-0) [default = %s]\n", pPars->fDumpInv? "yes": "no" );
|
||||
Abc_Print( -2, "\t-e : toggle using only support variables in the invariant [default = %s]\n", pPars->fUseSupp? "yes": "no" );
|
||||
Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" );
|
||||
Abc_Print( -2, "\t-j : toggle using simplified generalization step [default = %s]\n", pPars->fSimpleGeneral? "yes": "no" );
|
||||
Abc_Print( -2, "\t-o : toggle using property output as inductive hypothesis [default = %s]\n", pPars->fUsePropOut? "yes": "no" );
|
||||
Abc_Print( -2, "\t-n : * toggle skipping \'down\' in generalization [default = %s]\n", pPars->fSkipDown? "yes": "no" );
|
||||
Abc_Print( -2, "\t-c : * toggle handling CTGs in \'down\' [default = %s]\n", pPars->fCtgs? "yes": "no" );
|
||||
Abc_Print( -2, "\t-t : toggle using abstraction [default = %s]\n", pPars->fUseAbs? "yes": "no" );
|
||||
Abc_Print( -2, "\t-k : toggle using simplified refinement [default = %s]\n", pPars->fUseSimpleRef? "yes": "no" );
|
||||
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n\n");
|
||||
Abc_Print( -2, "\t* Implementation of switches -S, -n, and -c is contributed by Zyad Hassan.\n");
|
||||
Abc_Print( -2, "\t The theory and experiments supporting this work can be found in the following paper:\n");
|
||||
Abc_Print( -2, "\t Zyad Hassan, Aaron R. Bradley, Fabio Somenzi, \"Better Generalization in IC3\", FMCAD 2013.\n");
|
||||
Abc_Print( -2, "\t (http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/papers/85-Better-Generalization-IC3.pdf)\n");
|
||||
|
||||
|
||||
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue