diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abc/abcNtk.c | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 44 | ||||
-rw-r--r-- | src/base/main/mainMC.c | 147 |
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 /// +//////////////////////////////////////////////////////////////////////// + + |