summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2010-12-03 01:20:51 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2010-12-03 01:20:51 -0800
commit2adc30f56b76323d60b98f8ec0a5a7ad2c11e5fb (patch)
tree118d74179a92425ea7c46d77bf3cb3302c149fe1 /src/base
parentc9a625248607a090116cfdede47a5a80c227cb56 (diff)
downloadabc-2adc30f56b76323d60b98f8ec0a5a7ad2c11e5fb.tar.gz
abc-2adc30f56b76323d60b98f8ec0a5a7ad2c11e5fb.tar.bz2
abc-2adc30f56b76323d60b98f8ec0a5a7ad2c11e5fb.zip
Initial integration of PDR
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abc.c70
-rw-r--r--src/base/abci/abcDar.c50
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*************************************************************