diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abci/abc.c | 24 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 8 | ||||
-rw-r--r-- | src/base/abci/module.make | 1 | ||||
-rw-r--r-- | src/base/io/ioWriteDot.c | 11 | ||||
-rw-r--r-- | src/base/main/main.c | 4 | ||||
-rw-r--r-- | src/base/main/main.h | 4 | ||||
-rw-r--r-- | src/base/main/mainFrame.c | 6 |
7 files changed, 40 insertions, 18 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 \ diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index 88028105..54beb8b6 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -275,10 +275,16 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho fprintf( pFile, " Level%d;\n", Level ); Vec_PtrForEachEntry( vNodes, pNode, i ) { + int SuppSize; + Vec_Ptr_t * vSupp; if ( (int)pNode->Level != Level ) continue; if ( Abc_ObjFaninNum(pNode) == 0 ) continue; + vSupp = Abc_NtkNodeSupport( pNtk, &pNode, 1 ); + SuppSize = Vec_PtrSize( vSupp ); + Vec_PtrFree( vSupp ); + // fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); if ( Abc_NtkIsStrash(pNtk) ) pSopString = ""; @@ -288,7 +294,10 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho pSopString = Abc_NtkPrintSop(Mio_GateReadSop(pNode->pData)); else pSopString = Abc_NtkPrintSop(pNode->pData); - fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString ); +// fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString ); + fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, + SuppSize, + pSopString ); fprintf( pFile, ", shape = ellipse" ); if ( pNode->fMarkB ) diff --git a/src/base/main/main.c b/src/base/main/main.c index 1f1f19ba..6f2e1d11 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -56,8 +56,10 @@ int main( int argc, char * argv[] ) // added to detect memory leaks: #ifdef _DEBUG +#ifdef ABC_CHECK_LEAKS _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF ); #endif +#endif // Npn_Experiment(); // Npn_Generate(); @@ -255,8 +257,10 @@ void Abc_Start() Abc_Frame_t * pAbc; // added to detect memory leaks: #ifdef _DEBUG +#ifdef ABC_CHECK_LEAKS _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF ); #endif +#endif // start the glocal frame pAbc = Abc_FrameGetGlobalFrame(); // source the resource file diff --git a/src/base/main/main.h b/src/base/main/main.h index 852b8f25..62dc394a 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -40,10 +40,6 @@ typedef struct Abc_Frame_t_ Abc_Frame_t; /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -// this include should be the first one in the list -// it is used to catch memory leaks on Windows -#include "leaks.h" - // data structure packages #include "extra.h" #include "vec.h" diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index eae8b7a6..462b5a02 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -114,8 +114,8 @@ Abc_Frame_t * Abc_FrameAllocate() // networks to be used by choice p->vStore = Vec_PtrAlloc( 16 ); // initialize decomposition manager - define_cube_size(20); - set_espresso_flags(); +// define_cube_size(20); +// set_espresso_flags(); // initialize the trace manager // Abc_HManStart(); return p; @@ -139,7 +139,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p ) extern void undefine_cube_size(); // extern void Ivy_TruthManStop(); // Abc_HManStop(); - undefine_cube_size(); +// undefine_cube_size(); Rwt_ManGlobalStop(); // Ivy_TruthManStop(); if ( p->pLibVer ) Abc_LibFree( p->pLibVer, NULL ); |