summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abc.c52
-rw-r--r--src/base/abci/abcDar.c27
-rw-r--r--src/base/abci/abcPrint.c9
3 files changed, 55 insertions, 33 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d6bbd5e6..1dce3257 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -215,7 +215,7 @@ static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandBmcInter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIndcut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandEnlarge ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandLocalize ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInduction ( 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 );
@@ -483,7 +483,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "int", Abc_CommandBmcInter, 0 );
Cmd_CommandAdd( pAbc, "Verification", "indcut", Abc_CommandIndcut, 0 );
Cmd_CommandAdd( pAbc, "Verification", "enlarge", Abc_CommandEnlarge, 1 );
- Cmd_CommandAdd( pAbc, "Verification", "loc", Abc_CommandLocalize, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "ind", Abc_CommandInduction, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*r", Abc_CommandAbc8Read, 0 );
@@ -620,7 +620,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
fDumpResult = 0;
fUseLutLib = 0;
fPrintTime = 0;
- fPrintMuxes = 1;
+ fPrintMuxes = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmh" ) ) != EOF )
{
@@ -7936,7 +7936,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/
-/*
+
pNtkRes = Abc_NtkDarTestNtk( pNtk );
if ( pNtkRes == NULL )
{
@@ -7945,9 +7945,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
- Abc_NtkDarTest( pNtk );
+
+// Abc_NtkDarTest( pNtk );
return 0;
usage:
@@ -13559,7 +13559,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsfuvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSIplfuvwh" ) ) != EOF )
{
switch ( c )
{
@@ -13640,15 +13640,23 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nFramesAddSim < 0 )
goto usage;
break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nItersStop = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nItersStop < 0 )
+ goto usage;
+ break;
case 'p':
pPars->fPolarFlip ^= 1;
break;
case 'l':
pPars->fLatchCorr ^= 1;
break;
- case 's':
- pPars->fSkipCheck ^= 1;
- break;
case 'f':
pPars->fSemiFormal ^= 1;
break;
@@ -13710,7 +13718,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsfuvwh]\n" );
+ fprintf( pErr, "usage: scorr [-PQFCLNSI <num>] [-plfuvwh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
@@ -13719,10 +13727,10 @@ usage:
fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
fprintf( pErr, "\t-N num : number of last POs treated as constraints (0=none) [default = %d]\n", pPars->nConstrs );
fprintf( pErr, "\t-S num : additional simulation frames for c-examples (0=none) [default = %d]\n", pPars->nFramesAddSim );
+ fprintf( pErr, "\t-I num : iteration number to stop and output SR-model (0=none) [default = %d]\n", pPars->nItersStop );
fprintf( pErr, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
- fprintf( pErr, "\t-s : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "yes": "no" );
- fprintf( pErr, "\t-f : toggle filtering using interative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
+// fprintf( pErr, "\t-f : toggle filtering using interative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
fprintf( pErr, "\t-u : toggle using uniqueness constraints [default = %s]\n", pPars->fUniqueness? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printout of flop equivalences [default = %s]\n", pPars->fFlopVerbose? "yes": "no" );
@@ -16560,7 +16568,7 @@ usage:
SeeAlso []
***********************************************************************/
-int Abc_CommandLocalize( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
@@ -16575,8 +16583,8 @@ int Abc_CommandLocalize( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nFramesMax = 50;
- nConfMax = 500;
+ nFramesMax = 100;
+ nConfMax = 1000;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF )
@@ -16639,8 +16647,8 @@ int Abc_CommandLocalize( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkDarLocalize( pNtk, nFramesMax, nConfMax, fVerbose );
return 0;
usage:
- fprintf( pErr, "usage: loc [-FC num] [-vh]\n" );
- fprintf( pErr, "\t performs localization for single-output miter\n" );
+ fprintf( pErr, "usage: ind [-FC num] [-vh]\n" );
+ fprintf( pErr, "\t runs K-step induction for the property output\n" );
fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
@@ -19121,7 +19129,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDplsvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDplvh" ) ) != EOF )
{
switch ( c )
{
@@ -19219,9 +19227,6 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'l':
pPars->fLatchCorr ^= 1;
break;
- case 's':
- pPars->fSkipCheck ^= 1;
- break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -19268,7 +19273,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( stdout, "usage: *scorr [-PQFCLNSD <num>] [-plsvh]\n" );
+ fprintf( stdout, "usage: *scorr [-PQFCLNSD <num>] [-plvh]\n" );
fprintf( stdout, "\t performs sequential sweep using K-step induction\n" );
fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
@@ -19280,7 +19285,6 @@ usage:
fprintf( stdout, "\t-D num : min size of a clock domain used for synthesis [default = %d]\n", pPars->nMinDomSize );
fprintf( stdout, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
- fprintf( stdout, "\t-s : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "yes": "no" );
fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index c64fb0f5..a142de31 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1465,7 +1465,7 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose )
{
Aig_Man_t * pMan;
- int RetValue = -1, clk = clock();
+ int status, RetValue = -1, clk = clock();
// derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
@@ -1494,6 +1494,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
}
else
{
+/*
Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
FREE( pNtk->pModel );
FREE( pNtk->pSeqModel );
@@ -1509,8 +1510,30 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
printf( "No output was asserted in %d frames. ", nFrames );
RetValue = 1;
}
+*/
+ int iFrame;
+ RetValue = Ssw_BmcDynamic( pMan, nFrames, nBTLimit, fVerbose, &iFrame );
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+ if ( RetValue == 1 )
+ printf( "No output was asserted in %d frames. ", iFrame );
+ else if ( RetValue == -1 )
+ printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
+ else // if ( RetValue == 0 )
+ {
+ Fra_Cex_t * pCex = pNtk->pSeqModel;
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
+ }
}
PRT( "Time", clock() - clk );
+ // verify counter-example
+ if ( pNtk->pSeqModel )
+ {
+ status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel );
+ if ( status == 0 )
+ printf( "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
+ }
Aig_ManStop( pMan );
return RetValue;
}
@@ -2128,7 +2151,7 @@ void Abc_NtkDarLocalize( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVe
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return;
- RetValue = Saig_ManLocalization( pTemp = pMan, nFramesMax, nConfMax, fVerbose );
+ RetValue = Saig_ManInduction( pTemp = pMan, nFramesMax, nConfMax, fVerbose );
Aig_ManStop( pTemp );
if ( RetValue == 1 )
{
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 2e01a141..23a44eb3 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -114,7 +114,6 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes )
{
int Num;
-
if ( fSaveBest )
Abc_NtkCompareAndSaveBest( pNtk );
if ( fDumpResult )
@@ -147,15 +146,11 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) );
if ( (Num = Abc_NtkGetChoiceNum(pNtk)) )
fprintf( pFile, " (choice = %d)", Num );
- if ( (Num = Abc_NtkGetExorNum(pNtk)) )
- fprintf( pFile, " (exor = %d)", Num );
-// if ( Num2 = Abc_NtkGetMuxNum(pNtk) )
-// fprintf( pFile, " (mux = %d)", Num2-Num );
-// if ( Num2 )
-// fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
if ( fPrintMuxes )
{
extern int Abc_NtkCountMuxes( Abc_Ntk_t * pNtk );
+ Num = Abc_NtkGetExorNum(pNtk);
+ fprintf( pFile, " (exor = %d)", Num );
fprintf( pFile, " (mux = %d)", Abc_NtkCountMuxes(pNtk)-Num );
fprintf( pFile, " (pure and = %d)", Abc_NtkNodeNum(pNtk) - (Abc_NtkCountMuxes(pNtk) * 3) );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-19 20:59:14 +0000