summaryrefslogtreecommitdiffstats
path: root/src/base/main/mainMC.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-05-27 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2008-05-27 08:01:00 -0700
commit9604ecb1745da3bde720cd7be5ee8f89dc6bd5ff (patch)
treea2d15a88daf45a5e4ce8d746c414daa744c5350a /src/base/main/mainMC.c
parent5b79c7898356740c9678d5cf043d6bbc304dc7b4 (diff)
downloadabc-9604ecb1745da3bde720cd7be5ee8f89dc6bd5ff.tar.gz
abc-9604ecb1745da3bde720cd7be5ee8f89dc6bd5ff.tar.bz2
abc-9604ecb1745da3bde720cd7be5ee8f89dc6bd5ff.zip
Version abc80527
Diffstat (limited to 'src/base/main/mainMC.c')
-rw-r--r--src/base/main/mainMC.c147
1 files changed, 147 insertions, 0 deletions
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 ///
+////////////////////////////////////////////////////////////////////////
+
+