summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c36
-rw-r--r--src/base/abci/abcDar.c76
2 files changed, 99 insertions, 13 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 26d72934..7247f8ed 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3131,7 +3131,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: fx [-S num] [-D num] [-N num] [-sdzcvh]\n");
+ fprintf( pErr, "usage: fx [-SDN num] [-sdzcvh]\n");
fprintf( pErr, "\t performs unate fast extract on the current network\n");
fprintf( pErr, "\t-S num : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax );
fprintf( pErr, "\t-D num : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax );
@@ -13876,19 +13876,24 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int nFramesP;
int nConfMax;
+ int nVarsMax;
+ int fNewAlgor;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nFramesP = 0;
+ nFramesP = 0;
nConfMax = 10000;
- fVerbose = 0;
+ nVarsMax = 5000;
+ fNewAlgor = 0;
+ fVerbose = 1;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "PCSnvh" ) ) != EOF )
{
switch ( c )
{
@@ -13914,6 +13919,20 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConfMax < 0 )
goto usage;
break;
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nVarsMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nVarsMax < 0 )
+ goto usage;
+ break;
+ case 'n':
+ fNewAlgor ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -13943,7 +13962,10 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
- pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose );
+ if ( fNewAlgor )
+ pNtkRes = Abc_NtkDarLcorrNew( pNtk, nVarsMax, nConfMax, fVerbose );
+ else
+ pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -13954,10 +13976,12 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: lcorr [-P num] [-C num] [-vh]\n" );
+ fprintf( pErr, "usage: lcorr [-PCS num] [-nvh]\n" );
fprintf( pErr, "\t computes latch correspondence using 1-step induction\n" );
fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
fprintf( pErr, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
+ fprintf( pErr, "\t-S num : the max number of SAT variables [default = %d]\n", nVarsMax );
+ fprintf( pErr, "\t-n : toggle new algorithm [default = %s]\n", fNewAlgor? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index b84c5191..ac5ee882 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1316,6 +1316,50 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
/**Function*************************************************************
+ Synopsis [Computes latch correspondence.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose )
+{
+ Ssw_Pars_t Pars, * pPars = &Pars;
+ Aig_Man_t * pMan, * pTemp;
+ Abc_Ntk_t * pNtkAig = NULL;
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ return NULL;
+ Ssw_ManSetDefaultParams( pPars );
+ pPars->fLatchCorrOpt = 1;
+// pPars->nFramesAddSim = 0;
+ pPars->nBTLimit = nConfMax;
+ pPars->nSatVarMax = nVarsMax;
+ pPars->fVerbose = fVerbose;
+ pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
+ Aig_ManStop( pTemp );
+ if ( pMan )
+ {
+ if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
+ pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+ else
+ {
+ Abc_Obj_t * pObj;
+ int i;
+ pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+ Abc_NtkForEachLatch( pNtkAig, pObj, i )
+ Abc_LatchSetInit0( pObj );
+ }
+ Aig_ManStop( pMan );
+ }
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
@@ -1342,6 +1386,8 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
{
int iFrame;
RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, 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 );
@@ -1350,17 +1396,19 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
else // if ( RetValue == 0 )
{
Fra_Cex_t * pCex = pNtk->pSeqModel;
- printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
}
}
else
{
Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
{
Fra_Cex_t * pCex = pNtk->pSeqModel;
- printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
RetValue = 0;
}
else
@@ -1388,7 +1436,7 @@ PRT( "Time", clock() - clk );
int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
{
Aig_Man_t * pMan;
- int RetValue, Depth, clk = clock();
+ int RetValue, iFrame, clk = clock();
// derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
@@ -1397,11 +1445,16 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
return -1;
}
assert( pMan->nRegs > 0 );
- RetValue = Inter_ManPerformInterpolation( pMan, pPars, &Depth );
+ RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
if ( RetValue == 1 )
printf( "Property proved. " );
else if ( RetValue == 0 )
- printf( "Property DISPROVED with counter-example at depth %d. ", Depth );
+ {
+ printf( "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness). ", iFrame );
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+ }
else if ( RetValue == -1 )
printf( "Property UNDECIDED. " );
else
@@ -1440,7 +1493,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
Prove_ParamsSetDefault( pParams );
RetValue = Abc_NtkIvyProve( &pNtkComb, pParams );
// transfer model if given
- pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
+// pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
Abc_NtkDelete( pNtkComb );
// return the result, if solved
if ( RetValue == 1 )
@@ -1485,11 +1538,15 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
else
{
RetValue = Fra_FraigSec( pMan, pSecPar );
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
{
Fra_Cex_t * pCex = pNtk->pSeqModel;
- printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace).\n", pCex->iPo, pCex->iFrame );
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame );
+ if ( !Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel ) )
+ printf( "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
}
}
Aig_ManStop( pMan );
@@ -1842,6 +1899,8 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
if ( pCex )
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pCex;
RetValue = 1;
}
@@ -2341,6 +2400,9 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
if ( pMan == NULL )
return;
Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose, 0 );
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
Aig_ManStop( pMan );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 15:48:54 +0000