summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-05-12 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2008-05-12 08:01:00 -0700
commitcb899ec848984b194a9c227c7a01f147454ce591 (patch)
tree74c5f6cd7c75961cf142b6a4c0002d8decd80d0a
parent47036e1e44fb5f4e1948cdc26ab10254ccaa161d (diff)
downloadabc-cb899ec848984b194a9c227c7a01f147454ce591.tar.gz
abc-cb899ec848984b194a9c227c7a01f147454ce591.tar.bz2
abc-cb899ec848984b194a9c227c7a01f147454ce591.zip
Version abc80512
-rw-r--r--src/aig/aig/aig.h1
-rw-r--r--src/aig/aig/aigDup.c44
-rw-r--r--src/aig/fra/fraLcr.c2
-rw-r--r--src/aig/fra/fraSec.c61
-rw-r--r--src/aig/saig/saig.h2
-rw-r--r--src/aig/saig/saigBmc.c94
-rw-r--r--src/aig/saig/saigInter.c8
-rw-r--r--src/base/abci/abc.c26
-rw-r--r--src/base/abci/abcDar.c6
-rw-r--r--src/base/main/main.c2
-rw-r--r--src/map/pcm/module.make0
-rw-r--r--src/map/ply/module.make0
12 files changed, 226 insertions, 20 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 1450ad21..bbb5cb6e 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -478,6 +478,7 @@ extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl );
+extern Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum );
/*=== aigFanout.c ==========================================================*/
extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 55dc5625..fc01e7f0 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -787,6 +787,50 @@ Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper )
return pNew;
}
+/**Function*************************************************************
+
+ Synopsis [Duplicates AIG with only one primary output.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj;
+ int i;
+ assert( Aig_ManRegNum(p) > 0 );
+ assert( iPoNum < Aig_ManPoNum(p)-Aig_ManRegNum(p) );
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+ // create the PIs
+ Aig_ManCleanData( p );
+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+ Aig_ManForEachPi( p, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pNew );
+ // set registers
+ pNew->nRegs = p->nRegs;
+ pNew->nTruePis = p->nTruePis;
+ pNew->nTruePos = 1;
+ // duplicate internal nodes
+ Aig_ManForEachNode( p, pObj, i )
+ pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ // create the PO
+ pObj = Aig_ManPo( p, iPoNum );
+ Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ // create register inputs with MUXes
+ Aig_ManForEachLiSeq( p, pObj, i )
+ Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ Aig_ManCleanup( pNew );
+ return pNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index 0f5cc207..e5222e2e 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -542,7 +542,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
if ( pnIter ) *pnIter = 0;
return Aig_ManDupOrdered(pAig);
}
- assert( Aig_ManRegNum(pAig) > 0 );
+ assert( Aig_ManRegNum(pAig) > 0 );
// simulate the AIG
clk2 = clock();
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 5146344c..db8027d9 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -120,7 +120,7 @@ clk = clock();
pNew = Aig_ManDupOrdered( pTemp = pNew );
// pNew = Aig_ManDupDfs( pTemp = pNew );
Aig_ManStop( pTemp );
- if ( TimeLimit )
+ if ( RetValue == -1 && TimeLimit )
{
TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
@@ -131,7 +131,7 @@ clk = clock();
goto finish;
}
}
- pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter, TimeLeft );
+ pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, fVeryVerbose, &nIter, TimeLeft );
if ( pNew == NULL )
{
pNew = pTemp;
@@ -156,7 +156,7 @@ PRT( "Time", clock() - clk );
}
}
- if ( TimeLimit )
+ if ( RetValue == -1 && TimeLimit )
{
TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
@@ -189,7 +189,7 @@ PRT( "Time", clock() - clk );
if ( RetValue >= 0 )
goto finish;
- if ( TimeLimit )
+ if ( RetValue == -1 && TimeLimit )
{
TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
@@ -226,7 +226,7 @@ PRT( "Time", clock() - clk );
if ( RetValue == -1 )
for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
{
- if ( TimeLimit )
+ if ( RetValue == -1 && TimeLimit )
{
TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
@@ -327,13 +327,13 @@ PRT( "Time", clock() - clkTotal );
// try interplation
clk = clock();
- if ( RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
+ if ( RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
{
extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
int Depth;
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
- RetValue = Saig_Interpolate( pNew, 10000, 0, 1, 0, &Depth );
+ RetValue = Saig_Interpolate( pNew, 5000, 0, 1, fVeryVerbose, &Depth );
if ( fVerbose )
{
if ( RetValue == 1 )
@@ -357,6 +357,53 @@ PRT( "Time", clock() - clk );
RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 );
}
+ // try one-output at a time
+ if ( RetValue == -1 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) > 1 )
+ {
+ Aig_Man_t * pNew2;
+ int i, TimeLimit2, RetValue2, fOneUnsolved = 0, iCount, Counter = 0;
+ // count unsolved outputs
+ for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
+ if ( !Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
+ Counter++;
+ printf( "*** The miter has %d outputs (out of %d total) unsolved in the multi-output form.\n",
+ Counter, Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) );
+ iCount = 0;
+ for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
+ {
+ // get the remaining time for this output
+ if ( TimeLimit )
+ {
+ TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+ TimeLeft = AIG_MAX( TimeLeft, 0.0 );
+ if ( TimeLeft == 0.0 )
+ {
+ printf( "Runtime limit exceeded.\n" );
+ goto finish;
+ }
+ TimeLimit2 = 1 + (int)TimeLeft;
+ }
+ else
+ TimeLimit2 = 0;
+ if ( Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
+ continue;
+ iCount++;
+ printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
+ pNew2 = Aig_ManDupOneOutput( pNew, i );
+ RetValue2 = Fra_FraigSec( pNew2, nFramesMax, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit2 );
+ Aig_ManStop( pNew2 );
+ if ( RetValue2 == 0 )
+ goto finish;
+ if ( RetValue2 == -1 )
+ fOneUnsolved = 1;
+ }
+ if ( fOneUnsolved )
+ RetValue = -1;
+ else
+ RetValue = 1;
+ printf( "*** Finished running separate outputs of the miter.\n" );
+ }
+
finish:
// report the miter
if ( RetValue == 1 )
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index f0eb7099..b9b7de40 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -76,7 +76,7 @@ static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) {
////////////////////////////////////////////////////////////////////////
/*=== saigBmc.c ==========================================================*/
-extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
+extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
/*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p );
/*=== saigInter.c ==========================================================*/
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 3a6aa611..f6a42c8b 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -82,6 +82,90 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
/**Function*************************************************************
+ Synopsis [Returns the number of internal nodes that are not counted yet.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ if ( !Aig_ObjIsNode(pObj) )
+ return 0;
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ return 0;
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) +
+ Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Create timeframes of the manager for BMC.]
+
+ Description [The resulting manager is combinational. The primary inputs
+ corresponding to register outputs are ordered first. POs correspond to
+ the property outputs in each time-frame.
+ The unrolling is stopped as soon as the number of nodes in the frames
+ exceeds the given maximum size.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax )
+{
+ Aig_Man_t * pFrames;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo;
+ int i, f, Counter = 0;
+ assert( Saig_ManRegNum(pAig) > 0 );
+ pFrames = Aig_ManStart( nSizeMax );
+ Aig_ManIncrementTravId( pFrames );
+ // map the constant node
+ Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+ // create variables for register outputs
+ Saig_ManForEachLo( pAig, pObj, i )
+ pObj->pData = Aig_ManConst0( pFrames );
+ // add timeframes
+ Counter = 0;
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // create PI nodes for this frame
+ Saig_ManForEachPi( pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pFrames );
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ // create POs for this frame
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+ pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+ Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
+ if ( Counter >= nSizeMax )
+ {
+ Aig_ManCleanup( pFrames );
+ return pFrames;
+ }
+ }
+ if ( f == nFrames - 1 )
+ break;
+ // save register inputs
+ Saig_ManForEachLi( pAig, pObj, i )
+ pObj->pData = Aig_ObjChild0Copy(pObj);
+ // transfer to register outputs
+ Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+ pObjLo->pData = pObjLi->pData;
+ }
+ Aig_ManCleanup( pFrames );
+ return pFrames;
+}
+
+/**Function*************************************************************
+
Synopsis [Performs BMC for the given AIG.]
Description []
@@ -91,7 +175,7 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
SeeAlso []
***********************************************************************/
-int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fRewrite, int fVerbose, int * piFrame )
+int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame )
{
sat_solver * pSat;
Cnf_Dat_t * pCnf;
@@ -101,7 +185,13 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fRewri
*piFrame = -1;
// derive the timeframes
clk = clock();
- pFrames = Saig_ManFramesBmc( pAig, nFrames );
+ if ( nSizeMax > 0 )
+ {
+ pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
+ nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
+ }
+ else
+ pFrames = Saig_ManFramesBmc( pAig, nFrames );
if ( fVerbose )
{
printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c
index c3bb0875..3adcc568 100644
--- a/src/aig/saig/saigInter.c
+++ b/src/aig/saig/saigInter.c
@@ -566,6 +566,14 @@ p->timeCnf += clock() - clk;
// iterate the interpolation procedure
for ( i = 0; ; i++ )
{
+ if ( p->nFrames + i >= 100 )
+ {
+ if ( fVerbose )
+ printf( "Reached limit (%d) on the number of timeframes.\n", 100 );
+ p->timeTotal = clock() - clkTotal;
+ Saig_ManagerFree( p );
+ return -1;
+ }
// perform interplation
clk = clock();
RetValue = Saig_PerformOneStep( p );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f914b9c4..5725aaf0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -12713,6 +12713,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fWriteImps = 0;
pPars->fUse1Hot = 0;
pPars->fVerbose = 0;
+ pPars->TimeLimit = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF )
{
@@ -14657,25 +14658,27 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
int nFrames;
+ int nSizeMax;
int nBTLimit;
int fRewrite;
int fNewAlgo;
int fVerbose;
- extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose );
+ extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nFrames = 10;
+ nFrames = 20;
+ nSizeMax = 100000;
nBTLimit = 10000;
fRewrite = 0;
fNewAlgo = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FCravh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FNCravh" ) ) != EOF )
{
switch ( c )
{
@@ -14690,6 +14693,17 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nFrames < 0 )
goto usage;
break;
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nSizeMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nSizeMax < 0 )
+ goto usage;
+ break;
case 'C':
if ( globalUtilOptind >= argc )
{
@@ -14731,13 +14745,14 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Does not work for combinational networks.\n" );
return 0;
}
- Abc_NtkDarBmc( pNtk, nFrames, nBTLimit, fRewrite, fNewAlgo, fVerbose );
+ Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nBTLimit, fRewrite, fNewAlgo, fVerbose );
return 0;
usage:
- fprintf( pErr, "usage: bmc [-F num] [-C num] [-ravh]\n" );
+ fprintf( pErr, "usage: bmc [-FNC num] [-ravh]\n" );
fprintf( pErr, "\t perform bounded model checking\n" );
fprintf( pErr, "\t-F num : the number of time frames [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-N num : the max number of nodes in the frames [default = %d]\n", nSizeMax );
fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
fprintf( pErr, "\t-a : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" );
@@ -17069,6 +17084,7 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fWriteImps = 0;
pPars->fUse1Hot = 0;
pPars->fVerbose = 0;
+ pPars->TimeLimit = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF )
{
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 75995a60..ef1fbebc 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1208,7 +1208,7 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
SeeAlso []
***********************************************************************/
-int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose )
+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();
@@ -1226,7 +1226,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, in
if ( fNewAlgo )
{
int iFrame;
- RetValue = Saig_ManBmcSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose, &iFrame );
+ RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( RetValue == 1 )
printf( "No output was asserted in %d frames. ", nFrames );
@@ -1337,7 +1337,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, i
}
if ( fTryBmc )
{
- RetValue = Abc_NtkDarBmc( pNtk, 10, 1000, 0, 1, 0 );
+ RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, 1000, 0, 1, 0 );
if ( RetValue == 0 )
return RetValue;
}
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 26740258..7ecbe48e 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -217,7 +217,7 @@ int main( int argc, char * argv[] )
break;
}
}
-
+
// if the memory should be freed, quit packages
if ( fStatus < 0 )
{
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/pcm/module.make
+++ /dev/null
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/ply/module.make
+++ /dev/null