summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abcNtk.c2
-rw-r--r--src/base/abci/abc.c44
-rw-r--r--src/base/main/mainMC.c147
3 files changed, 187 insertions, 6 deletions
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index b66c3f32..4d543547 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -522,7 +522,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
int i, k;
assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) );
- assert( Abc_ObjIsNode(pNode) || (Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pNode)) );
+ assert( Abc_ObjIsNode(pNode) || (Abc_NtkIsStrash(pNtk) && (Abc_AigNodeIsConst(pNode) || Abc_ObjIsCi(pNode))) );
// start the network
pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 39fdb9fb..d9defa1b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14291,9 +14291,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Fra_SecSetDefaultParams( pSecPar );
- pSecPar->TimeLimit = 600;
+ pSecPar->TimeLimit = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FTarmfwvh" ) ) != EOF )
{
switch ( c )
{
@@ -14308,6 +14308,17 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pSecPar->nFramesMax < 0 )
goto usage;
break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pSecPar->TimeLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pSecPar->TimeLimit < 0 )
+ goto usage;
+ break;
case 'a':
pSecPar->fPhaseAbstract ^= 1;
break;
@@ -14350,9 +14361,10 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: dsec [-F num] [-armfwvh] <file1> <file2>\n" );
+ fprintf( pErr, "usage: dsec [-F num] [-T num] [-armfwvh] <file1> <file2>\n" );
fprintf( pErr, "\t performs inductive sequential equivalence checking\n" );
fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
+ fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", pSecPar->TimeLimit );
fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" );
fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" );
@@ -14459,6 +14471,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
// perform verification
Abc_NtkDarProve( pNtk, pSecPar );
+
+ // Fra_SmlWriteCounterExample( stdout, Aig_Man_t * pAig, Fra_Cex_t * p )
+
return 0;
usage:
@@ -15617,20 +15632,25 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
char * pFileName;
int c;
int fMapped;
+ int fTest;
extern void * Ioa_ReadBlif( char * pFileName, int fCheck );
extern Aig_Man_t * Ntl_ManExtract( void * p );
extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime );
// set defaults
fMapped = 0;
+ fTest = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "mth" ) ) != EOF )
{
switch ( c )
{
case 'm':
fMapped ^= 1;
break;
+ case 't':
+ fTest ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -15650,6 +15670,19 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
}
fclose( pFile );
+ if ( fTest )
+ {
+ extern void Ntl_ManFree( void * p );
+ extern void Ntl_ManPrintStats( void * p );
+ void * pTemp = Ioa_ReadBlif( pFileName, 1 );
+ if ( pTemp )
+ {
+ Ntl_ManPrintStats( pTemp );
+ Ntl_ManFree( pTemp );
+ }
+ return 0;
+ }
+
Abc_FrameClearDesign();
pAbc->pAbc8Ntl = Ioa_ReadBlif( pFileName, 1 );
if ( pAbc->pAbc8Ntl == NULL )
@@ -15672,9 +15705,10 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( stdout, "usage: *r [-mh]\n" );
+ fprintf( stdout, "usage: *r [-mth]\n" );
fprintf( stdout, "\t reads the design with whiteboxes\n" );
fprintf( stdout, "\t-m : toggle extracting mapped network [default = %s]\n", fMapped? "yes": "no" );
+ fprintf( stdout, "\t-t : toggle reading in the test mode [default = %s]\n", fTest? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c
new file mode 100644
index 00000000..3f6b81a4
--- /dev/null
+++ b/src/base/main/mainMC.c
@@ -0,0 +1,147 @@
+/**CFile****************************************************************
+
+ FileName [mainMC.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [The main package.]
+
+ Synopsis [The main file for the model checker.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mainInt.h"
+#include "aig.h"
+#include "saig.h"
+#include "fra.h"
+#include "ioa.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [The main() procedure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int main( int argc, char * argv[] )
+{
+ Fra_Sec_t SecPar, * pSecPar = &SecPar;
+ FILE * pFile;
+ Aig_Man_t * pAig;
+ int RetValue;
+ // BMC parameters
+ int nFrames = 30;
+ int nSizeMax = 200000;
+ int nBTLimit = 10000;
+ int fRewrite = 0;
+ int fNewAlgo = 1;
+ int fVerbose = 0;
+
+ if ( argc != 2 )
+ {
+ printf( " Expecting one command-line argument (an input file in AIGER format).\n" );
+ printf( " usage: %s <file.aig>", argv[0] );
+ return 0;
+ }
+ pFile = fopen( argv[1], "r" );
+ if ( pFile == NULL )
+ {
+ printf( " Cannot open input AIGER file \"%s\".\n", argv[1] );
+ printf( " usage: %s <file.aig>", argv[0] );
+ return 0;
+ }
+ fclose( pFile );
+ pAig = Ioa_ReadAiger( argv[1], 1 );
+ if ( pAig == NULL )
+ {
+ printf( " Parsing the AIGER file \"%s\" has failed.\n", argv[1] );
+ printf( " usage: %s <file.aig>", argv[0] );
+ return 0;
+ }
+
+ // perform BMC
+ Aig_ManSetRegNum( pAig, pAig->nRegs );
+ RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL );
+
+ // perform full-blown SEC
+ if ( RetValue != 0 )
+ {
+ extern void Dar_LibStart();
+ extern void Dar_LibStop();
+ extern void Cnf_ClearMemory();
+
+ Fra_SecSetDefaultParams( pSecPar );
+ pSecPar->nFramesMax = 2; // the max number of frames used for induction
+
+ Dar_LibStart();
+ RetValue = Fra_FraigSec( pAig, pSecPar );
+ Dar_LibStop();
+ Cnf_ClearMemory();
+ }
+
+ // perform BMC again
+ if ( RetValue == -1 )
+ {
+ }
+
+ // decide how to report the output
+ pFile = stdout;
+
+ // report the result
+ if ( RetValue == 0 )
+ {
+// fprintf(stdout, "s SATIFIABLE\n");
+ Fra_SmlWriteCounterExample( pFile, pAig, pAig->pSeqModel );
+ if ( pFile != stdout )
+ fclose(pFile);
+ Aig_ManStop( pAig );
+ exit(10);
+ }
+ else if ( RetValue == 1 )
+ {
+// fprintf(stdout, "s UNSATISFIABLE\n");
+ fprintf( pFile, "0\n" );
+ if ( pFile != stdout )
+ fclose(pFile);
+ Aig_ManStop( pAig );
+ exit(20);
+ }
+ else // if ( RetValue == -1 )
+ {
+// fprintf(stdout, "s UNKNOWN\n");
+ if ( pFile != stdout )
+ fclose(pFile);
+ Aig_ManStop( pAig );
+ exit(0);
+ }
+ return 0;
+}
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 06:56:59 +0000