summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abc.c19
-rw-r--r--src/base/main/mainMC.c99
2 files changed, 91 insertions, 27 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d9defa1b..450a245f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -9298,7 +9298,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Prove_Params_t Params, * pParams = &Params;
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkTemp;
- int c, clk, RetValue;
+ int c, clk, RetValue, iOut = -1;
extern int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
@@ -9351,8 +9351,16 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
// verify that the pattern is correct
if ( RetValue == 0 )
{
+ Abc_Obj_t * pObj;
+ int i;
int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtkTemp->pModel );
- if ( pSimInfo[0] != 1 )
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ if ( pSimInfo[i] == 1 )
+ {
+ iOut = i;
+ break;
+ }
+ if ( i == Abc_NtkCoNum(pNtk) )
printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
free( pSimInfo );
}
@@ -9360,7 +9368,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( RetValue == -1 )
printf( "UNDECIDED " );
else if ( RetValue == 0 )
- printf( "SATISFIABLE " );
+ printf( "SATISFIABLE (output = %d) ", iOut );
else
printf( "UNSATISFIABLE " );
//printf( "\n" );
@@ -15634,6 +15642,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
int fMapped;
int fTest;
extern void * Ioa_ReadBlif( char * pFileName, int fCheck );
+ extern void Ioa_WriteBlif( void * p, char * pFileName );
extern Aig_Man_t * Ntl_ManExtract( void * p );
extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime );
@@ -15678,6 +15687,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pTemp )
{
Ntl_ManPrintStats( pTemp );
+// Ioa_WriteBlif( pTemp, "test_boxes.blif" );
Ntl_ManFree( pTemp );
}
return 0;
@@ -17888,6 +17898,8 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
+ printf( "Currently *cec works only for two designs given on command line.\n" );
+/*
// derive AIGs
pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl, 0 );
pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
@@ -17903,6 +17915,7 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
Aig_ManStop( pAig1 );
Aig_ManStop( pAig2 );
+*/
return 0;
usage:
diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c
index 3f6b81a4..84c75b7b 100644
--- a/src/base/main/mainMC.c
+++ b/src/base/main/mainMC.c
@@ -45,29 +45,36 @@
***********************************************************************/
int main( int argc, char * argv[] )
{
+ int fEnableBmcOnly = 0; // enable to make it BMC-only
+
+ int fEnableCounter = 1; // should be 1 in the final version
+ int fEnableComment = 0; // should be 0 in the final version
+
Fra_Sec_t SecPar, * pSecPar = &SecPar;
FILE * pFile;
Aig_Man_t * pAig;
- int RetValue;
+ int RetValue = -1;
+ int Depth = -1;
// BMC parameters
- int nFrames = 30;
- int nSizeMax = 200000;
+ int nFrames = 50;
+ int nSizeMax = 500000;
int nBTLimit = 10000;
int fRewrite = 0;
int fNewAlgo = 1;
int fVerbose = 0;
+ int clkTotal = clock();
if ( argc != 2 )
{
printf( " Expecting one command-line argument (an input file in AIGER format).\n" );
- printf( " usage: %s <file.aig>", argv[0] );
+ printf( " usage: %s <file.aig>\n", 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] );
+ printf( " usage: %s <file.aig>\n", argv[0] );
return 0;
}
fclose( pFile );
@@ -75,33 +82,47 @@ int main( int argc, char * argv[] )
if ( pAig == NULL )
{
printf( " Parsing the AIGER file \"%s\" has failed.\n", argv[1] );
- printf( " usage: %s <file.aig>", argv[0] );
+ printf( " usage: %s <file.aig>\n", 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 )
+ if ( !fEnableBmcOnly )
{
- 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
+ if ( pAig->nRegs != 0 )
+ 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->TimeLimit = 600;
+ pSecPar->nFramesMax = 4; // the max number of frames used for induction
+ pSecPar->fPhaseAbstract = 0; // disable phase-abstraction
+ pSecPar->fSilent = 1; // disable phase-abstraction
+
+ Dar_LibStart();
+ RetValue = Fra_FraigSec( pAig, pSecPar );
+ Dar_LibStop();
+ Cnf_ClearMemory();
+ }
}
// perform BMC again
- if ( RetValue == -1 )
+ if ( RetValue == -1 && pAig->nRegs != 0 )
{
+ int nFrames = 200;
+ int nSizeMax = 500000;
+ int nBTLimit = 10000000;
+ int fRewrite = 0;
+ RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth );
+ if ( RetValue != 0 )
+ RetValue = -1;
}
// decide how to report the output
@@ -111,7 +132,20 @@ int main( int argc, char * argv[] )
if ( RetValue == 0 )
{
// fprintf(stdout, "s SATIFIABLE\n");
+ fprintf( pFile, "1" );
+ if ( fEnableCounter )
+ {
+ printf( "\n" );
+ if ( pAig->pSeqModel )
Fra_SmlWriteCounterExample( pFile, pAig, pAig->pSeqModel );
+ }
+
+ if ( fEnableComment )
+ {
+ printf( " # File %10s. ", argv[1] );
+ PRT( "Time", clock() - clkTotal );
+ }
+
if ( pFile != stdout )
fclose(pFile);
Aig_ManStop( pAig );
@@ -120,7 +154,15 @@ int main( int argc, char * argv[] )
else if ( RetValue == 1 )
{
// fprintf(stdout, "s UNSATISFIABLE\n");
- fprintf( pFile, "0\n" );
+ fprintf( pFile, "0" );
+
+ if ( fEnableComment )
+ {
+ printf( " # File %10s. ", argv[1] );
+ PRT( "Time", clock() - clkTotal );
+ }
+ printf( "\n" );
+
if ( pFile != stdout )
fclose(pFile);
Aig_ManStop( pAig );
@@ -129,6 +171,15 @@ int main( int argc, char * argv[] )
else // if ( RetValue == -1 )
{
// fprintf(stdout, "s UNKNOWN\n");
+ fprintf( pFile, "2" );
+
+ if ( fEnableComment )
+ {
+ printf( " # File %10s. ", argv[1] );
+ PRT( "Time", clock() - clkTotal );
+ }
+ printf( "\n" );
+
if ( pFile != stdout )
fclose(pFile);
Aig_ManStop( pAig );
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-22 16:07:50 +0000