summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c24
-rw-r--r--src/base/abci/abcDar.c8
-rw-r--r--src/base/abci/module.make1
3 files changed, 23 insertions, 10 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index aa8d6b30..d1aa2c82 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -297,6 +297,7 @@ void Abc_FrameClearDesign()
void Abc_Init( Abc_Frame_t * pAbc )
{
// Abc_NtkBddImplicationTest();
+// Ply_LutPairTest();
Cmd_CommandAdd( pAbc, "Printing", "print_stats", Abc_CommandPrintStats, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_exdc", Abc_CommandPrintExdc, 0 );
@@ -7072,6 +7073,9 @@ int Abc_CommandEspresso( Abc_Frame_t * pAbc, int argc, char ** argv )
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
+ printf( "This command is currently disabled.\n" );
+ return 0;
+
// set defaults
fVerbose = 0;
Extra_UtilGetoptReset();
@@ -7098,7 +7102,7 @@ int Abc_CommandEspresso( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "SOP minimization is possible for logic networks (run \"renode\").\n" );
return 1;
}
- Abc_NtkEspresso( pNtk, fVerbose );
+// Abc_NtkEspresso( pNtk, fVerbose );
return 0;
usage:
@@ -7764,6 +7768,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
*/
+
+
/*
// pNtkRes = Abc_NtkDar( pNtk );
// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
@@ -7776,8 +7782,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
*/
+
// Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
/*
if ( globalUtilOptind != 1 )
@@ -15337,9 +15345,10 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
int nBTLimit;
int fRewrite;
int fTransLoop;
+ int fUsePudlak;
int fVerbose;
- extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose );
+ extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -15349,9 +15358,10 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
nBTLimit = 20000;
fRewrite = 0;
fTransLoop = 1;
+ fUsePudlak = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Crtvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Crtpvh" ) ) != EOF )
{
switch ( c )
{
@@ -15372,6 +15382,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't':
fTransLoop ^= 1;
break;
+ case 'p':
+ fUsePudlak ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -15401,15 +15414,16 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
return 0;
}
- Abc_NtkDarBmcInter( pNtk, nBTLimit, fRewrite, fTransLoop, fVerbose );
+ Abc_NtkDarBmcInter( pNtk, nBTLimit, fRewrite, fTransLoop, fUsePudlak, fVerbose );
return 0;
usage:
- fprintf( pErr, "usage: int [-C num] [-rtvh]\n" );
+ fprintf( pErr, "usage: int [-C num] [-rtpvh]\n" );
fprintf( pErr, "\t uses interpolation to prove the property\n" );
fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit );
fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" );
+ fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "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 2a234b68..a691a205 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1270,7 +1270,7 @@ PRT( "Time", clock() - clk );
SeeAlso []
***********************************************************************/
-int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose )
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose )
{
Aig_Man_t * pMan;
int RetValue, Depth, clk = clock();
@@ -1282,7 +1282,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTra
return -1;
}
assert( pMan->nRegs > 0 );
- RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fVerbose, &Depth );
+ RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fUsePudlak, fVerbose, &Depth );
if ( RetValue == 1 )
printf( "Property proved. " );
else if ( RetValue == 0 )
@@ -2148,12 +2148,12 @@ Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanu
***********************************************************************/
void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
{
- extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+ extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return;
- Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
+ Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose, 0 );
Aig_ManStop( pMan );
}
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 777da95b..e83785fe 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -14,7 +14,6 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcDelay.c \
src/base/abci/abcDress.c \
src/base/abci/abcDsd.c \
- src/base/abci/abcEspresso.c \
src/base/abci/abcExtract.c \
src/base/abci/abcFpga.c \
src/base/abci/abcFpgaFast.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-07 12:20:55 +0000