Skip to content

A
abc
Commit 1d3ff533 by Yen-Sheng Ho
Options

added ipdr

parent bc010af4
Showing with 268 additions and 0 deletions
src/base/abci/abc.c
...@@ -333,6 +333,7 @@ static int Abc_CommandBm2 ( Abc_Frame_t * pAbc, int argc, cha ...@@ -333,6 +333,7 @@ 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_CommandSaucy ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTestCex ( 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_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 #ifdef ABC_USE_CUDD
static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, char ** argv );
#endif #endif
...@@ -983,6 +984,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -983,6 +984,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "saucy3", Abc_CommandSaucy, 1 ); Cmd_CommandAdd( pAbc, "Verification", "saucy3", Abc_CommandSaucy, 1 );
Cmd_CommandAdd( pAbc, "Verification", "testcex", Abc_CommandTestCex, 0 ); Cmd_CommandAdd( pAbc, "Verification", "testcex", Abc_CommandTestCex, 0 );
Cmd_CommandAdd( pAbc, "Verification", "pdr", Abc_CommandPdr, 0 ); Cmd_CommandAdd( pAbc, "Verification", "pdr", Abc_CommandPdr, 0 );
Cmd_CommandAdd( pAbc, "Verification", "ipdr", Abc_CommandIPdr, 0 );
#ifdef ABC_USE_CUDD #ifdef ABC_USE_CUDD
Cmd_CommandAdd( pAbc, "Verification", "reconcile", Abc_CommandReconcile, 1 ); Cmd_CommandAdd( pAbc, "Verification", "reconcile", Abc_CommandReconcile, 1 );
#endif #endif
...@@ -26418,6 +26420,272 @@ usage: ...@@ -26418,6 +26420,272 @@ usage:
return 1; 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 );
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_NtkDarPdr( 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;
}
#ifdef ABC_USE_CUDD #ifdef ABC_USE_CUDD
/**Function************************************************************* /**Function*************************************************************
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment