diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2010-12-03 01:20:51 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2010-12-03 01:20:51 -0800 |
commit | 2adc30f56b76323d60b98f8ec0a5a7ad2c11e5fb (patch) | |
tree | 118d74179a92425ea7c46d77bf3cb3302c149fe1 /src/base/abci | |
parent | c9a625248607a090116cfdede47a5a80c227cb56 (diff) | |
download | abc-2adc30f56b76323d60b98f8ec0a5a7ad2c11e5fb.tar.gz abc-2adc30f56b76323d60b98f8ec0a5a7ad2c11e5fb.tar.bz2 abc-2adc30f56b76323d60b98f8ec0a5a7ad2c11e5fb.zip |
Initial integration of PDR
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 70 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 50 |
2 files changed, 119 insertions, 1 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 493b6419..fca9f68c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -273,6 +273,7 @@ static int Abc_CommandUnfold ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandFold ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBm ( 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_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -671,6 +672,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "fold", Abc_CommandFold, 1 ); Cmd_CommandAdd( pAbc, "Verification", "bm", Abc_CommandBm, 1 ); Cmd_CommandAdd( pAbc, "Verification", "testcex", Abc_CommandTestCex, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "pdr", Abc_CommandPdr, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*r", Abc_CommandAbc8Read, 0 ); @@ -19518,7 +19520,7 @@ int Abc_CommandBm( Abc_Frame_t * pAbc, int argc, char ** argv ) p_equivalence = 1; break; default: - Abc_Print( -2, "Unkown switch.\n"); + Abc_Print( -2, "Unknown switch.\n"); goto usage; } } @@ -19584,6 +19586,9 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv ) { case 'h': goto usage; + default: + Abc_Print( -2, "Unknown switch.\n"); + goto usage; } } @@ -19643,6 +19648,69 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex ); + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + Abc_Cex_t * pCex; + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + Abc_Print( -2, "Unknown switch.\n"); + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( -2, "There is no current network.\n"); + return 0; + } + if ( Abc_NtkLatchNum(pNtk) == 0 ) + { + Abc_Print( -2, "The current network is combinational.\n"); + return 0; + } + if ( Abc_NtkPoNum(pNtk) != 1 ) + { + Abc_Print( -2, "The number of POs is different from 1.\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 + pAbc->Status = Abc_NtkDarPdr( pNtk, &pCex ); + pAbc->nFrames = pCex ? pCex->iFrame : -1; + Abc_FrameReplaceCex( pAbc, &pCex ); + return 0; + +usage: + Abc_Print( -2, "usage: pdr -h\n" ); + Abc_Print( -2, "\t model checking using property driven reachability (aka ic3)\n" ); + Abc_Print( -2, "\t pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" ); + Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} /**Function************************************************************* diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 6d4482eb..13205183 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2245,6 +2245,56 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar ) return RetValue; } +typedef struct Pdr_Par_t_ Pdr_Par_t; +struct Pdr_Par_t_ +{ + int fAbstract; // perform abstraction + int fVerbose; // enable verbose output + int fVeryVerbose; // enable verbose output +}; + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex ) +{ +// extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ); +// extern int Pdr_ManSolve( Aig_Man_t * pAig, Abc_Cex_t ** ppCex, Pdr_Par_t * pPars ); + int RetValue = -1, clk = clock(); + Pdr_Par_t Pars, * pPars = &Pars; + Aig_Man_t * pMan; +// Pdr_ManSetDefaultParams( pPars ); + *ppCex = NULL; + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + { + printf( "Converting network into AIG has failed.\n" ); + return -1; + } +// RetValue = Pdr_ManSolve( pMan, ppCex, pPars ); + if ( RetValue == 1 ) + printf( "Property proved. " ); + else if ( RetValue == 0 ) + printf( "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness). ", ppCex? (*ppCex)->iFrame : -1 ); + else if ( RetValue == -1 ) + printf( "Property UNDECIDED. " ); + else + assert( 0 ); +ABC_PRT( "Time", clock() - clk ); + + if ( *ppCex && !Ssw_SmlRunCounterExample( pMan, *ppCex ) ) + printf( "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" ); + Aig_ManStop( pMan ); + return RetValue; +} /**Function************************************************************* |