summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/aig/aig.h2
-rw-r--r--src/aig/aig/aigDfs.c2
-rw-r--r--src/aig/aig/aigDup.c2
-rw-r--r--src/aig/aig/aigMan.c1
-rw-r--r--src/aig/aig/aigPart.c81
-rw-r--r--src/aig/dar/darBalance.c2
-rw-r--r--src/aig/dar/darRefact.c4
-rw-r--r--src/aig/dar/darScript.c26
-rw-r--r--src/aig/fra/fra.h2
-rw-r--r--src/aig/fra/fraCec.c30
-rw-r--r--src/aig/mfx/mfxCore.c4
-rw-r--r--src/aig/ntl/ntlExtract.c2
-rw-r--r--src/aig/ntl/ntlInsert.c9
-rw-r--r--src/aig/ntl/ntlReadBlif.c4
-rw-r--r--src/aig/nwk/nwkBidec.c5
-rw-r--r--src/aig/nwk/nwkMap.c2
-rw-r--r--src/aig/nwk/nwkStrash.c10
-rw-r--r--src/aig/nwk/nwkTiming.c51
-rw-r--r--src/aig/tim/tim.c9
-rw-r--r--src/aig/tim/tim.h1
-rw-r--r--src/base/abci/abc.c36
-rw-r--r--src/base/abci/abcDar.c2
-rw-r--r--src/base/abci/abcVerify.c1
-rw-r--r--src/base/io/io.c4
-rw-r--r--src/map/if/ifLib.c2
-rw-r--r--src/map/if/ifMap.c2
26 files changed, 204 insertions, 92 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 18061a9c..f04a420d 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -528,7 +528,7 @@ extern Vec_Ptr_t * Aig_ManSupportsRegisters( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
extern Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit, int fVerbose );
extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
-extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
+extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize, int fSmart );
extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
extern Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
extern Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 9e43d7fd..34657a0b 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -418,7 +418,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
LevelMax = Aig_ObjLevel(pNext);
}
}
- else
+ else if ( !Aig_ObjIsConst1(pObj) )
assert( 0 );
Aig_ObjSetLevel( pObj, LevelMax );
}
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 043a95a8..ca1f1cc3 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -359,7 +359,7 @@ Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder )
}
}
Vec_PtrFree( vPios );
- assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+// assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
if ( p->pEquivs == NULL && p->pReprs == NULL && (nNodes = Aig_ManCleanup( pNew )) )
printf( "Aig_ManDupDfs(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
// duplicate the timing manager
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 0d5dfca9..58f0d797 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -208,6 +208,7 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vFlopNums) Vec_IntFree( p->vFlopNums );
if ( p->pManExdc ) Aig_ManStop( p->pManExdc );
if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots );
+ FREE( p->pData );
FREE( p->pSeqModel );
FREE( p->pName );
FREE( p->pSpec );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index f129ae23..ce7221ae 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1092,6 +1092,63 @@ Aig_Man_t * Aig_ManDupPartAll( Aig_Man_t * pOld, Vec_Int_t * vPart )
/**Function*************************************************************
+ Synopsis [Collects internal nodes in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManSupportNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vSupport )
+{
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ Vec_IntPush( vSupport, Aig_ObjPioNum(pObj) );
+ return;
+ }
+ Aig_ManSupportNodes_rec( p, Aig_ObjFanin0(pObj), vSupport );
+ Aig_ManSupportNodes_rec( p, Aig_ObjFanin1(pObj), vSupport );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects internal nodes and PIs in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManSupportNodes( Aig_Man_t * p, Vec_Ptr_t * vParts )
+{
+ Vec_Ptr_t * vPartSupps;
+ Vec_Int_t * vPart, * vSupport;
+ int i, k, iOut;
+ Aig_ManSetPioNumbers( p );
+ vPartSupps = Vec_PtrAlloc( Vec_PtrSize(vParts) );
+ Vec_PtrForEachEntry( vParts, vPart, i )
+ {
+ vSupport = Vec_IntAlloc( 100 );
+ Aig_ManIncrementTravId( p );
+ Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
+ Vec_IntForEachEntry( vPart, iOut, k )
+ Aig_ManSupportNodes_rec( p, Aig_ObjFanin0(Aig_ManPo(p, iOut)), vSupport );
+// Vec_IntSort( vSupport, 0 );
+ Vec_PtrPush( vPartSupps, vSupport );
+ }
+ Aig_ManCleanPioNumbers( p );
+ return vPartSupps;
+}
+
+/**Function*************************************************************
+
Synopsis [Create partitioned miter of the two AIGs.]
Description [Assumes that each output in the second AIG cannot have
@@ -1102,7 +1159,7 @@ Aig_Man_t * Aig_ManDupPartAll( Aig_Man_t * pOld, Vec_Int_t * vPart )
SeeAlso []
***********************************************************************/
-Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize )
+Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize, int fSmart )
{
Aig_Man_t * pNew;
Aig_Obj_t * pMiter;
@@ -1111,7 +1168,13 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
Vec_Int_t * vPart, * vPartSupp;
int i, k;
// partition the first manager
- vParts = Aig_ManPartitionSmart( p1, nPartSize, 0, &vPartSupps );
+ if ( fSmart )
+ vParts = Aig_ManPartitionSmart( p1, nPartSize, 0, &vPartSupps );
+ else
+ {
+ vParts = Aig_ManPartitionNaive( p1, nPartSize );
+ vPartSupps = Aig_ManSupportNodes( p1, vParts );
+ }
// derive miters
vMiters = Vec_PtrAlloc( Vec_PtrSize(vParts) );
for ( i = 0; i < Vec_PtrSize(vParts); i++ )
@@ -1121,7 +1184,6 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
vPartSupp = Vec_PtrEntry( vPartSupps, i );
// create the new miter
pNew = Aig_ManStart( 1000 );
-// pNew->pName = Extra_UtilStrsav( p1->pName );
// create the PIs
for ( k = 0; k < Vec_IntSize(vPartSupp); k++ )
Aig_ObjCreatePi( pNew );
@@ -1497,7 +1559,7 @@ void Aig_ManChoiceEval( Aig_Man_t * p )
***********************************************************************/
Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
{
- Aig_Man_t * pNew, * pThis, * pPrev;
+ Aig_Man_t * pNew, * pThis, * pPrev, * pTemp;
int i;
// start AIG with choices
pPrev = Vec_PtrEntry( vAigs, 0 );
@@ -1514,15 +1576,18 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
pPrev = pThis;
}
// derive the result of choicing
-//Aig_ManPrintStats( pNew );
pNew = Aig_ManRehash( pNew );
-//Aig_ManPrintStats( pNew );
// create the equivalent nodes lists
Aig_ManMarkValidChoices( pNew );
-//Aig_ManPrintStats( pNew );
+ // reconstruct the network
+ pNew = Aig_ManDupDfsOrder( pTemp = pNew, Vec_PtrEntry( vAigs, 0 ) );
+ Aig_ManStop( pTemp );
+ // duplicate the timing manager
+ pTemp = Vec_PtrEntry( vAigs, 0 );
+ if ( pTemp->pManTime )
+ pNew->pManTime = Tim_ManDup( pTemp->pManTime, 0 );
// reset levels
Aig_ManChoiceLevel( pNew );
-// Aig_ManChoiceEval( pNew );
return pNew;
}
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 6e78041a..574c72d9 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -187,7 +187,7 @@ void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int f
// get the two last nodes
pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 );
pObj2 = Vec_PtrEntry( vSuper, RightBound );
- if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 )
+ if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 || Aig_Regular(pObj1) == Aig_Regular(pObj2) )
return;
// find the first node that can be shared
for ( i = RightBound; i >= LeftBound; i-- )
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index e814840f..0637fee0 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -376,14 +376,14 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore );
if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) )
{
- p->GainBest = Vec_PtrSize(p->vCutNodes);
+ p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL );
p->pGraphBest = Kit_GraphCreateConst0();
Vec_PtrCopy( p->vLeavesBest, vCut );
return p->GainBest;
}
if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) )
{
- p->GainBest = Vec_PtrSize(p->vCutNodes);
+ p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL );
p->pGraphBest = Kit_GraphCreateConst1();
Vec_PtrCopy( p->vLeavesBest, vCut );
return p->GainBest;
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 69810125..6d6b761c 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -82,19 +82,27 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
pAig = Aig_ManDupDfs( pAig );
if ( fVerbose ) Aig_ManPrintStats( pAig );
+
+ // balance
+ if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) Aig_ManPrintStats( pAig );
+ }
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
-/*
+
// refactor
Dar_ManRefactor( pAig, pParsRef );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
-*/
+
// balance
if ( fBalance )
{
@@ -167,9 +175,9 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
// balance
if ( fBalance )
{
-// pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
-// Aig_ManStop( pTemp );
-// if ( fVerbose ) Aig_ManPrintStats( pAig );
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) Aig_ManPrintStats( pAig );
}
// rewrite
@@ -239,9 +247,9 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
// balance
if ( fBalance )
{
-// pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
-// Aig_ManStop( pTemp );
-// if ( fVerbose ) Aig_ManPrintStats( pAig );
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) Aig_ManPrintStats( pAig );
}
@@ -336,7 +344,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
Aig_ManForEachObj( pAig, pObj, i )
pObj->pHaig = pObj;
- pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose);
+ pAig = Dar_ManCompress (pAig, fBalance, fUpdateLevel, fVerbose);
Vec_PtrPush( vAigs, pAig );
//Aig_ManPrintStats( pAig );
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index dbe61522..7c2b95db 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -258,7 +258,7 @@ static inline int Fra_ImpCreate( int Left, int Right )
/*=== fraCec.c ========================================================*/
extern int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose );
extern int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose );
-extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fVerbose );
+extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose );
/*=== fraClass.c ========================================================*/
extern int Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
extern int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 779337bf..05f2493a 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -166,8 +166,7 @@ PRT( "Time", clock() - clk );
// duplicate the AIG
clk = clock();
-// pAig = Aig_ManDupDfs( pTemp = pAig );
- pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 );
+ pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 );
Aig_ManStop( pTemp );
if ( fVerbose )
{
@@ -247,22 +246,25 @@ PRT( "Time", clock() - clk );
SeeAlso []
***********************************************************************/
-int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fVerbose )
+int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose )
{
Aig_Man_t * pAig;
Vec_Ptr_t * vParts;
int i, RetValue = 1, nOutputs;
// create partitions
- vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize );
+ vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize, fSmart );
// solve the partitions
nOutputs = -1;
Vec_PtrForEachEntry( vParts, pAig, i )
{
nOutputs++;
if ( fVerbose )
+ {
printf( "Verifying part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r",
i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAig), Aig_ManPoNum(pAig),
Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
+ fflush( stdout );
+ }
RetValue = Fra_FraigMiterStatus( pAig );
if ( RetValue == 1 )
continue;
@@ -306,8 +308,9 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize
SeeAlso []
***********************************************************************/
-int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int fPartition, int fVerbose )
+int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose )
{
+ Aig_Man_t * pTemp;
//Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
int RetValue, clkTotal = clock();
@@ -324,10 +327,19 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int f
assert( Aig_ManPiNum(pMan1) == Aig_ManPiNum(pMan1) );
assert( Aig_ManPoNum(pMan1) == Aig_ManPoNum(pMan1) );
- if ( fPartition )
- RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, 100, fVerbose );
- else
- RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), fVerbose );
+ // make sure that the first miter has more nodes
+ if ( Aig_ManNodeNum(pMan1) < Aig_ManNodeNum(pMan2) )
+ {
+ pTemp = pMan1;
+ pMan1 = pMan2;
+ pMan2 = pTemp;
+ }
+ assert( Aig_ManNodeNum(pMan1) >= Aig_ManNodeNum(pMan2) );
+
+ if ( nPartSize )
+ RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nPartSize, fSmart, fVerbose );
+ else // no partitioning
+ RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), 0, fVerbose );
// report the miter
if ( RetValue == 1 )
diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c
index 6e47c986..bea7c6b0 100644
--- a/src/aig/mfx/mfxCore.c
+++ b/src/aig/mfx/mfxCore.c
@@ -312,6 +312,10 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
// free the manager
p->timeTotal = clock() - clk;
Mfx_ManStop( p );
+
+ // update network into the topological order
+// if ( pPars->fResub )
+// Nwk_ManTopological( pNtk );
return 1;
}
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 0654bb27..55356654 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -387,7 +387,7 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
// add box inputs/outputs to COs/CIs
if ( Ntl_ObjIsBox(pObj) )
{
- int LevelCur, LevelMax = -AIG_INFINITY;
+ int LevelCur, LevelMax = -TIME_ETERNITY;
Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) );
Ntl_ObjForEachFanin( pObj, pNetFanin, i )
{
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index 2eb48e84..f02b4716 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -137,6 +137,7 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
{
char Buffer[100];
+ Vec_Ptr_t * vObjs;
Vec_Int_t * vTruth;
Vec_Int_t * vCover;
Ntl_Mod_t * pRoot;
@@ -160,8 +161,13 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
vTruth = Vec_IntAlloc( 1 << 16 );
vCover = Vec_IntAlloc( 1 << 16 );
nDigits = Aig_Base10Log( Nwk_ManNodeNum(pNtk) );
- Nwk_ManForEachNode( pNtk, pObj, i )
+// Nwk_ManForEachObj( pNtk, pObj, i )
+ vObjs = Nwk_ManDfs( pNtk );
+ Vec_PtrForEachEntry( vObjs, pObj, i )
+// Nwk_ManForEachNode( pNtk, pObj, i )
{
+ if ( !Nwk_ObjIsNode(pObj) )
+ continue;
pNode = Ntl_ModelCreateNode( pRoot, Nwk_ObjFaninNum(pObj) );
pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
if ( Hop_IsComplement(pObj->pFunc) )
@@ -194,6 +200,7 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
}
pObj->pCopy = pNet;
}
+ Vec_PtrFree( vObjs );
Vec_IntFree( vCover );
Vec_IntFree( vTruth );
// mark CIs and outputs of the registers
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index e5a94610..81ea2a2c 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -974,9 +974,9 @@ static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput
// find the delay number
pTokenNum = Vec_PtrEntryLast(vTokens);
if ( !strcmp( pTokenNum, "-inf" ) )
- Delay = -AIG_INFINITY;
+ Delay = -TIME_ETERNITY;
else if ( !strcmp( pTokenNum, "inf" ) )
- Delay = AIG_INFINITY;
+ Delay = TIME_ETERNITY;
else
Delay = atof( pTokenNum );
if ( Delay == 0.0 && pTokenNum[0] != '0' )
diff --git a/src/aig/nwk/nwkBidec.c b/src/aig/nwk/nwkBidec.c
index 5d0b454e..e30d2c02 100644
--- a/src/aig/nwk/nwkBidec.c
+++ b/src/aig/nwk/nwkBidec.c
@@ -88,6 +88,11 @@ void Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose )
int clk = clock();
pPars->nVarsMax = Nwk_ManGetFaninMax( pNtk );
pPars->fVerbose = fVerbose;
+ if ( pPars->nVarsMax < 2 )
+ {
+ printf( "Resynthesis is not performed for networks whose nodes are less than 2 inputs.\n" );
+ return;
+ }
if ( pPars->nVarsMax > 15 )
{
if ( fVerbose )
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index 44aecc03..ee7f56ad 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -52,7 +52,7 @@ void Nwk_ManSetIfParsDefault( If_Par_t * pPars )
pPars->nFlowIters = 1;
pPars->nAreaIters = 2;
pPars->DelayTarget = -1;
- pPars->Epsilon = (float)0.01;
+ pPars->Epsilon = (float)0.001;
pPars->fPreprocess = 1;
pPars->fArea = 0;
pPars->fFancy = 0;
diff --git a/src/aig/nwk/nwkStrash.c b/src/aig/nwk/nwkStrash.c
index 3bcfcd41..b5e2b387 100644
--- a/src/aig/nwk/nwkStrash.c
+++ b/src/aig/nwk/nwkStrash.c
@@ -95,7 +95,8 @@ Aig_Obj_t * Nwk_ManStrashNode( Aig_Man_t * p, Nwk_Obj_t * pObj )
***********************************************************************/
Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
{
- Aig_Man_t * pMan;//, * pTemp;
+ Vec_Ptr_t * vObjs;
+ Aig_Man_t * pMan;
Aig_Obj_t * pObjNew;
Nwk_Obj_t * pObj;
int i, Level;
@@ -105,6 +106,10 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
pMan->pManTime = Tim_ManDup( pNtk->pManTime, 1 );
Tim_ManIncrementTravId( pMan->pManTime );
Nwk_ManForEachObj( pNtk, pObj, i )
+ pObj->pCopy = NULL;
+// Nwk_ManForEachObj( pNtk, pObj, i )
+ vObjs = Nwk_ManDfs( pNtk );
+ Vec_PtrForEachEntry( vObjs, pObj, i )
{
if ( Nwk_ObjIsCi(pObj) )
{
@@ -126,9 +131,8 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
assert( 0 );
pObj->pCopy = pObjNew;
}
+ Vec_PtrFree( vObjs );
Aig_ManCleanup( pMan );
-// pMan = Aig_ManDupOrdered( pTemp = pMan );
-// Aig_ManStop( pTemp );
return pMan;
}
diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c
index 5e4967da..9bf1d6a1 100644
--- a/src/aig/nwk/nwkTiming.c
+++ b/src/aig/nwk/nwkTiming.c
@@ -17,7 +17,7 @@
Revision [$Id: nwkTiming.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
-
+
#include "nwk.h"
////////////////////////////////////////////////////////////////////////
@@ -46,7 +46,7 @@ void Nwk_ManCleanTiming( Nwk_Man_t * pNtk )
Nwk_ManForEachObj( pNtk, pObj, i )
{
pObj->tArrival = pObj->tSlack = 0.0;
- pObj->tRequired = AIG_INFINITY;
+ pObj->tRequired = TIME_ETERNITY;
}
}
@@ -138,7 +138,7 @@ float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, int fUseSorting )
return Nwk_ObjArrival(pObj);
if ( Nwk_ObjIsCo(pObj) )
return Nwk_ObjArrival( Nwk_ObjFanin0(pObj) );
- tArrival = -AIG_INFINITY;
+ tArrival = -TIME_ETERNITY;
if ( pLutLib == NULL )
{
Nwk_ObjForEachFanin( pObj, pFanin, k )
@@ -196,7 +196,7 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, int fUseSorting )
assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) || Nwk_ObjIsCo(pObj) );
if ( Nwk_ObjIsCo(pObj) )
return Nwk_ObjRequired(pObj);
- tRequired = AIG_INFINITY;
+ tRequired = TIME_ETERNITY;
if ( pLutLib == NULL )
{
Nwk_ObjForEachFanout( pObj, pFanout, k )
@@ -333,7 +333,7 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
{
printf( "The max LUT size (%d) is less than the max fanin count (%d).\n",
pLutLib->LutMax, Nwk_ManGetFaninMax(pNtk) );
- return -AIG_INFINITY;
+ return -TIME_ETERNITY;
}
// compute the reverse order of all objects
@@ -356,7 +356,7 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
}
// get the latest arrival times
- tArrival = -AIG_INFINITY;
+ tArrival = -TIME_ETERNITY;
Nwk_ManForEachPo( pNtk, pObj, i )
if ( tArrival < Nwk_ObjArrival(pObj) )
tArrival = Nwk_ObjArrival(pObj);
@@ -388,11 +388,12 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
else if ( Nwk_ObjIsCo(pObj) )
{
if ( pNtk->pManTime )
+ {
tRequired = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId );
- else
- tRequired = Nwk_ObjRequired(pObj);
- if ( Nwk_ObjRequired(Nwk_ObjFanin0(pObj)) > tRequired )
- Nwk_ObjSetRequired( Nwk_ObjFanin0(pObj), tRequired );
+ Nwk_ObjSetRequired( pObj, tRequired );
+ }
+ if ( Nwk_ObjRequired(Nwk_ObjFanin0(pObj)) > Nwk_ObjRequired(pObj) )
+ Nwk_ObjSetRequired( Nwk_ObjFanin0(pObj), Nwk_ObjRequired(pObj) );
}
// set slack for this object
@@ -424,14 +425,12 @@ int Nwk_ManVerifyTiming( Nwk_Man_t * pNtk )
{
tArrival = Nwk_NodeComputeArrival( pObj, 1 );
tRequired = Nwk_NodeComputeRequired( pObj, 1 );
- if ( Nwk_ObjIsCi(pObj) && pNtk->pManTime )
- tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId );
- if ( Nwk_ObjIsCo(pObj) && pNtk->pManTime )
- tArrival = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId );
if ( !Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pObj), (float)0.01 ) )
- printf( "Nwk_ManVerifyTiming(): Arrival time of object %d is incorrect.\n", pObj->Id );
+ printf( "Nwk_ManVerifyTiming(): Object %d has different arrival time (%.2f) from computed (%.2f).\n",
+ pObj->Id, Nwk_ObjArrival(pObj), tArrival );
if ( !Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.01 ) )
- printf( "Nwk_ManVerifyTiming(): Required time of object %d is incorrect.\n", pObj->Id );
+ printf( "Nwk_ManVerifyTiming(): Object %d has different required time (%.2f) from computed (%.2f).\n",
+ pObj->Id, Nwk_ObjRequired(pObj), tRequired );
}
return 1;
}
@@ -586,9 +585,9 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj )
{
Tim_ManSetPoArrival( pManTime, pTemp->PioId, tArrival );
iBox = Tim_ManBoxForCo( pManTime, pNext->PioId );
- Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
if ( iBox >= 0 ) // this is not a true PO
{
+ Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox );
nTerms = Tim_ManBoxOutputNum( pManTime, iBox );
for ( i = 0; i < nTerms; i++ )
@@ -635,14 +634,6 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj )
float tRequired;
int i, k, iBox, iTerm1, nTerms;
assert( Nwk_ObjIsNode(pObj) );
-
-if ( pObj->Id == 1384 )
-{
- int x = 0;
-// Nwk_ObjPrint( Nwk_ManObj(pObj->pMan, 1384) );
-// Nwk_ObjPrint( Nwk_ManObj(pObj->pMan, 422) );
-}
-
// make sure the node's required time remained the same
tRequired = Nwk_NodeComputeRequired( pObj, 1 );
assert( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.01 ) );
@@ -667,16 +658,16 @@ if ( pObj->Id == 1384 )
if ( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pTemp), (float)0.01 ) )
continue;
Nwk_ObjSetRequired( pTemp, tRequired );
- // add the fanouts to the queue
+ // add the fanins to the queue
if ( Nwk_ObjIsCi(pTemp) )
{
if ( pManTime )
{
Tim_ManSetPiRequired( pManTime, pTemp->PioId, tRequired );
iBox = Tim_ManBoxForCi( pManTime, pNext->PioId );
- Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox );
if ( iBox >= 0 ) // this is not a true PO
{
+ Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox );
iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
nTerms = Tim_ManBoxInputNum( pManTime, iBox );
for ( i = 0; i < nTerms; i++ )
@@ -780,9 +771,9 @@ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj )
if ( pManTime )
{
iBox = Tim_ManBoxForCo( pManTime, pNext->PioId );
- Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
if ( iBox >= 0 ) // this is not a true PO
{
+ Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox );
nTerms = Tim_ManBoxOutputNum( pManTime, iBox );
for ( i = 0; i < nTerms; i++ )
@@ -850,12 +841,10 @@ int Nwk_ManVerifyLevel( Nwk_Man_t * pNtk )
***********************************************************************/
void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels )
{
-// float Temp;
assert( pObj->pMan == pObjNew->pMan );
assert( pObj != pObjNew );
assert( Nwk_ObjFanoutNum(pObj) > 0 );
assert( Nwk_ObjIsNode(pObj) && !Nwk_ObjIsCo(pObjNew) );
-// Temp = Nwk_NodeComputeRequired( pObj, 1 );
// transfer fanouts to the old node
Nwk_ObjTransferFanout( pObj, pObjNew );
// transfer the timing information
@@ -866,7 +855,7 @@ void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels )
pObjNew->tArrival = pObj->tArrival;
pObjNew->tRequired = pObj->tRequired;
// update required times of the old fanins
- pObj->tRequired = AIG_INFINITY;
+ pObj->tRequired = TIME_ETERNITY;
Nwk_NodeUpdateRequired( pObj );
// remove the old node
Nwk_ManDeleteNode_rec( pObj );
diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c
index d66dbd35..62e29fe9 100644
--- a/src/aig/tim/tim.c
+++ b/src/aig/tim/tim.c
@@ -31,7 +31,6 @@
#define AIG_MIN(a,b) (((a) < (b))? (a) : (b))
#define AIG_MAX(a,b) (((a) > (b))? (a) : (b))
#define AIG_ABS(a) (((a) >= 0)? (a) :-(a))
-#define AIG_INFINITY (100000000)
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -133,7 +132,7 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
{
p->pPis[i].Id = i;
p->pPis[i].iObj2Box = p->pPis[i].iObj2Num = -1;
- p->pPis[i].timeReq = AIG_INFINITY;
+ p->pPis[i].timeReq = TIME_ETERNITY;
p->pPis[i].timeArr = 0.0;
p->pPis[i].TravId = 0;
}
@@ -141,7 +140,7 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
{
p->pPos[i].Id = i;
p->pPos[i].iObj2Box = p->pPos[i].iObj2Num = -1;
- p->pPos[i].timeReq = AIG_INFINITY;
+ p->pPos[i].timeReq = TIME_ETERNITY;
p->pPos[i].timeArr = 0.0;
p->pPos[i].TravId = 0;
}
@@ -673,7 +672,7 @@ float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
Tim_ManBoxForEachOutput( p, pBox, pObjRes, i )
{
pDelays = pBox->pDelayTable + i * pBox->nInputs;
- DelayBest = -AIG_INFINITY;
+ DelayBest = -TIME_ETERNITY;
Tim_ManBoxForEachInput( p, pBox, pObj, k )
DelayBest = AIG_MAX( DelayBest, pObj->timeArr + pDelays[k] );
pObjRes->timeArr = DelayBest;
@@ -718,7 +717,7 @@ float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
// compute the required times for each input of the box (POs)
Tim_ManBoxForEachInput( p, pBox, pObjRes, i )
{
- DelayBest = AIG_INFINITY;
+ DelayBest = TIME_ETERNITY;
Tim_ManBoxForEachOutput( p, pBox, pObj, k )
{
pDelays = pBox->pDelayTable + k * pBox->nInputs;
diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h
index d092434e..d73a89d8 100644
--- a/src/aig/tim/tim.h
+++ b/src/aig/tim/tim.h
@@ -43,6 +43,7 @@ typedef struct Tim_Man_t_ Tim_Man_t;
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+#define TIME_ETERNITY 10000
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f0f7fb56..40967a65 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15094,7 +15094,7 @@ int Abc_CommandAbc8DC2( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose );
// set defaults
- fBalance = 0;
+ fBalance = 1;
fUpdateLevel = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
@@ -15768,19 +15768,21 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fVerbose;
int nConfLimit;
- int fPartition;
+ int fSmart;
+ int nPartSize;
extern Aig_Man_t * Ntl_ManCollapse( void * p );
extern void * Ntl_ManDup( void * pOld );
extern void Ntl_ManFree( void * p );
- extern int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int fPartition, int fVerbose );
+ extern int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
// set defaults
- fVerbose = 0;
nConfLimit = 10000;
- fPartition = 0;
+ nPartSize = 100;
+ fSmart = 0;
+ fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CPsvh" ) ) != EOF )
{
switch ( c )
{
@@ -15795,8 +15797,19 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConfLimit < 0 )
goto usage;
break;
- case 'p':
- fPartition ^= 1;
+ case 'P':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nPartSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nPartSize < 0 )
+ goto usage;
+ break;
+ case 's':
+ fSmart ^= 1;
break;
case 'v':
fVerbose ^= 1;
@@ -15836,16 +15849,17 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Ntl_ManFree( pTemp );
// perform verification
- Fra_FraigCecTop( pAig1, pAig2, nConfLimit, fPartition, fVerbose );
+ Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
Aig_ManStop( pAig1 );
Aig_ManStop( pAig2 );
return 0;
usage:
- fprintf( stdout, "usage: *cec [-C num] [-pvh] <file1> <file2>\n" );
+ fprintf( stdout, "usage: *cec [-C num] [-P num] [-svh] <file1> <file2>\n" );
fprintf( stdout, "\t performs combinational equivalence checking\n" );
fprintf( stdout, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
- fprintf( stdout, "\t-p : toggle automatic partitioning [default = %s]\n", fPartition? "yes": "no" );
+ fprintf( stdout, "\t-P num : the partition size for partitioned CEC [default = %d]\n", nPartSize );
+ fprintf( stdout, "\t-s : toggle smart and natural output partitioning [default = %s]\n", fSmart? "smart": "natural" );
fprintf( stdout, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
fprintf( stdout, "\tfile1 : (optional) the file with the first network\n");
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 9be147f4..4f27057b 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -946,7 +946,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVe
{
pMan1 = Abc_NtkToDar( pNtk1, 0, 0 );
pMan2 = Abc_NtkToDar( pNtk2, 0, 0 );
- RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, 100, fVerbose );
+ RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, 100, 1, fVerbose );
Aig_ManStop( pMan1 );
Aig_ManStop( pMan2 );
goto finish;
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 1d72a767..c05d539e 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -397,6 +397,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
printf( "Verifying part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r",
i+1, Vec_PtrSize(vParts), Abc_NtkPiNum(pMiterPart), Abc_NtkPoNum(pMiterPart),
Abc_NtkNodeNum(pMiterPart), Abc_AigLevel(pMiterPart) );
+ fflush( stdout );
// solve the problem
RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
if ( RetValue == -1 )
diff --git a/src/base/io/io.c b/src/base/io/io.c
index e1ff3b08..6b802bf1 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1408,7 +1408,7 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
// call the corresponding file writer
if ( !fUseLuts )
Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BENCH );
- else
+ else if ( pAbc->pNtkCur )
{
Abc_Ntk_t * pNtkTemp;
pNtkTemp = Abc_NtkToNetlist( pAbc->pNtkCur );
@@ -1416,6 +1416,8 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
Io_WriteBenchLut( pNtkTemp, pFileName );
Abc_NtkDelete( pNtkTemp );
}
+ else
+ printf( "There is no current network.\n" );
return 0;
usage:
diff --git a/src/map/if/ifLib.c b/src/map/if/ifLib.c
index c5353e19..455f43d9 100644
--- a/src/map/if/ifLib.c
+++ b/src/map/if/ifLib.c
@@ -90,7 +90,7 @@ If_Lib_t * If_LutLibRead( char * FileName )
return NULL;
}
- // check if var delays are specifies
+ // check if var delays are specified
if ( k > 1 )
p->fVarPinDelays = 1;
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 81521abf..573932d0 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -88,7 +88,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
{
// recompute the parameters of the best cut
pCut->Delay = If_CutDelay( p, pCut );
- assert( pCut->Delay <= pObj->Required + p->fEpsilon );
+// assert( pCut->Delay <= pObj->Required + p->fEpsilon );
pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
if ( p->pPars->fEdge )
pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 02:57:29 +0000