summaryrefslogtreecommitdiffstats
path: root/src/temp/ivy
diff options
context:
space:
mode:
Diffstat (limited to 'src/temp/ivy')
-rw-r--r--src/temp/ivy/ivy.h30
-rw-r--r--src/temp/ivy/ivyCheck.c6
-rw-r--r--src/temp/ivy/ivyCut.c93
-rw-r--r--src/temp/ivy/ivyDfs.c99
-rw-r--r--src/temp/ivy/ivyFanout.c1
-rw-r--r--src/temp/ivy/ivyIsop.c188
-rw-r--r--src/temp/ivy/ivyMan.c29
-rw-r--r--src/temp/ivy/ivyObj.c38
-rw-r--r--src/temp/ivy/ivyRwrAlg.c4
-rw-r--r--src/temp/ivy/ivyRwrPre.c94
-rw-r--r--src/temp/ivy/ivySeq.c708
-rw-r--r--src/temp/ivy/ivyTable.c4
-rw-r--r--src/temp/ivy/ivyUtil.c73
-rw-r--r--src/temp/ivy/module.make1
14 files changed, 1191 insertions, 177 deletions
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index 8c5f130b..7fb054f7 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -80,6 +80,8 @@ struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit)
int nRefs; // reference counter
Ivy_Obj_t * pFanin0; // fanin
Ivy_Obj_t * pFanin1; // fanin
+ Ivy_Obj_t * pFanout; // fanout
+ Ivy_Obj_t * pEquiv; // equivalent node
};
// the AIG manager
@@ -136,6 +138,9 @@ struct Ivy_Store_t_
Ivy_Cut_t pCuts[IVY_CUT_LIMIT]; // storage for cuts
};
+#define IVY_LEAF_MASK 255
+#define IVY_LEAF_BITS 8
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -170,9 +175,9 @@ static inline Ivy_Edge_t Ivy_EdgeNotCond( Ivy_Edge_t Edge, int fCond ) { ret
static inline Ivy_Edge_t Ivy_EdgeFromNode( Ivy_Obj_t * pNode ) { return Ivy_EdgeCreate( Ivy_Regular(pNode)->Id, Ivy_IsComplement(pNode) ); }
static inline Ivy_Obj_t * Ivy_EdgeToNode( Ivy_Man_t * p, Ivy_Edge_t Edge ){ return Ivy_NotCond( Ivy_ManObj(p, Ivy_EdgeId(Edge)), Ivy_EdgeIsComplement(Edge) ); }
-static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << 4) | Lat; }
-static inline int Ivy_LeafId( int Leaf ) { return Leaf >> 4; }
-static inline int Ivy_LeafLat( int Leaf ) { return Leaf & 15; }
+static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << IVY_LEAF_BITS) | Lat; }
+static inline int Ivy_LeafId( int Leaf ) { return Leaf >> IVY_LEAF_BITS; }
+static inline int Ivy_LeafLat( int Leaf ) { return Leaf & IVY_LEAF_MASK; }
static inline int Ivy_ManPiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PI]; }
static inline int Ivy_ManPoNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PO]; }
@@ -261,12 +266,16 @@ static inline int Ivy_ObjFanoutC( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout
static inline Ivy_Obj_t * Ivy_ObjCreateGhost( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init )
{
Ivy_Obj_t * pGhost, * pTemp;
+ assert( Type != IVY_AND || !Ivy_ObjIsConst1(Ivy_Regular(p0)) );
+ assert( p1 == NULL || !Ivy_ObjIsConst1(Ivy_Regular(p1)) );
+ assert( Type == IVY_PI || Ivy_Regular(p0) != Ivy_Regular(p1) );
+ assert( Type != IVY_LATCH || !Ivy_IsComplement(p0) );
+// assert( p1 == NULL || (!Ivy_ObjIsLatch(Ivy_Regular(p0)) || !Ivy_ObjIsLatch(Ivy_Regular(p1))) );
pGhost = Ivy_ManGhost(p);
pGhost->Type = Type;
pGhost->Init = Init;
pGhost->pFanin0 = p0;
pGhost->pFanin1 = p1;
- assert( Type == IVY_PI || Ivy_ObjFanin0(pGhost) != Ivy_ObjFanin1(pGhost) );
if ( p1 && Ivy_ObjFaninId0(pGhost) > Ivy_ObjFaninId1(pGhost) )
pTemp = pGhost->pFanin0, pGhost->pFanin0 = pGhost->pFanin1, pGhost->pFanin1 = pTemp;
return pGhost;
@@ -384,6 +393,7 @@ extern Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches );
extern void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone );
extern Vec_Vec_t * Ivy_ManLevelize( Ivy_Man_t * p );
extern Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p );
+extern int Ivy_ManIsAcyclic( Ivy_Man_t * p );
/*=== ivyDsd.c ==========================================================*/
extern int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree );
extern void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree );
@@ -400,11 +410,14 @@ extern void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, V
extern Ivy_Obj_t * Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+/*=== ivyIsop.c ==========================================================*/
+extern int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover );
+extern void Ivy_TruthManStop();
/*=== ivyMan.c ==========================================================*/
extern Ivy_Man_t * Ivy_ManStart();
extern void Ivy_ManStop( Ivy_Man_t * p );
extern int Ivy_ManCleanup( Ivy_Man_t * p );
-extern int Ivy_ManPropagateBuffers( Ivy_Man_t * p );
+extern int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel );
extern void Ivy_ManPrintStats( Ivy_Man_t * p );
extern void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits );
/*=== ivyMem.c ==========================================================*/
@@ -425,8 +438,8 @@ extern void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern void Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew );
extern void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop );
extern void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop );
-extern void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop );
-extern void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode );
+extern void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel );
+extern void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel );
/*=== ivyOper.c =========================================================*/
extern Ivy_Obj_t * Ivy_Oper( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type );
extern Ivy_Obj_t * Ivy_And( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
@@ -442,6 +455,8 @@ extern Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbo
extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
extern int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
extern int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose );
+/*=== ivySeq.c =========================================================*/
+extern int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose );
/*=== ivyTable.c ========================================================*/
extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern void Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj );
@@ -456,6 +471,7 @@ extern unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_In
extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p );
extern int Ivy_ManLevels( Ivy_Man_t * p );
extern void Ivy_ManResetLevels( Ivy_Man_t * p );
+extern int Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew );
extern int Ivy_ObjIsMuxType( Ivy_Obj_t * pObj );
diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c
index 4331c07e..36222f72 100644
--- a/src/temp/ivy/ivyCheck.c
+++ b/src/temp/ivy/ivyCheck.c
@@ -107,8 +107,8 @@ int Ivy_ManCheck( Ivy_Man_t * p )
printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
return 0;
}
-// if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) )
-// printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) );
+ if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) )
+ printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) );
pObj2 = Ivy_TableLookup( p, pObj );
if ( pObj2 != pObj )
printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
@@ -124,6 +124,8 @@ int Ivy_ManCheck( Ivy_Man_t * p )
printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
return 0;
}
+ if ( !Ivy_ManIsAcyclic(p) )
+ return 0;
return 1;
}
diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c
index 7d1ec63a..56f872e9 100644
--- a/src/temp/ivy/ivyCut.c
+++ b/src/temp/ivy/ivyCut.c
@@ -24,6 +24,8 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+static inline int Ivy_NodeCutHashValue( int NodeId ) { return 1 << (NodeId % 31); }
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -580,6 +582,88 @@ static inline int Ivy_NodeCutExtend( Ivy_Cut_t * pCut, int iNew )
/**Function*************************************************************
+ Synopsis [Returns 1 if the cut can be constructed; 0 otherwise.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Ivy_NodeCutPrescreen( Ivy_Cut_t * pCut, int Id0, int Id1 )
+{
+ int i;
+ if ( pCut->nSize < pCut->nSizeMax )
+ return 1;
+ for ( i = 0; i < pCut->nSize; i++ )
+ if ( pCut->pArray[i] == Id0 || pCut->pArray[i] == Id1 )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives new cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Ivy_NodeCutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
+{
+ unsigned uHash = 0;
+ int i, k;
+ assert( pCut->nSize > 0 );
+ assert( IdNew0 < IdNew1 );
+ for ( i = k = 0; i < pCut->nSize; i++ )
+ {
+ if ( pCut->pArray[i] == IdOld )
+ continue;
+ if ( IdNew0 <= pCut->pArray[i] )
+ {
+ if ( IdNew0 < pCut->pArray[i] )
+ {
+ pCutNew->pArray[ k++ ] = IdNew0;
+ uHash |= Ivy_NodeCutHashValue( IdNew0 );
+ }
+ IdNew0 = 0x7FFFFFFF;
+ }
+ if ( IdNew1 <= pCut->pArray[i] )
+ {
+ if ( IdNew1 < pCut->pArray[i] )
+ {
+ pCutNew->pArray[ k++ ] = IdNew1;
+ uHash |= Ivy_NodeCutHashValue( IdNew1 );
+ }
+ IdNew1 = 0x7FFFFFFF;
+ }
+ pCutNew->pArray[ k++ ] = pCut->pArray[i];
+ uHash |= Ivy_NodeCutHashValue( pCut->pArray[i] );
+ }
+ if ( IdNew0 < 0x7FFFFFFF )
+ {
+ pCutNew->pArray[ k++ ] = IdNew0;
+ uHash |= Ivy_NodeCutHashValue( IdNew0 );
+ }
+ if ( IdNew1 < 0x7FFFFFFF )
+ {
+ pCutNew->pArray[ k++ ] = IdNew1;
+ uHash |= Ivy_NodeCutHashValue( IdNew1 );
+ }
+ pCutNew->nSize = k;
+ pCutNew->uHash = uHash;
+ assert( pCutNew->nSize <= pCut->nSizeMax );
+// for ( i = 1; i < pCutNew->nSize; i++ )
+// assert( pCutNew->pArray[i-1] < pCutNew->pArray[i] );
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Check if the cut exists.]
Description [Returns 1 if the cut exists.]
@@ -789,7 +873,7 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves
Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut;
Ivy_Man_t * pMan = p;
Ivy_Obj_t * pLeaf;
- int i, k;
+ int i, k, iLeaf0, iLeaf1;
assert( nLeaves <= IVY_CUT_INPUT );
@@ -818,6 +902,7 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves
pLeaf = Ivy_ManObj( p, pCut->pArray[k] );
if ( Ivy_ObjIsCi(pLeaf) )
continue;
+/*
*pCutNew = *pCut;
Ivy_NodeCutShrink( pCutNew, pLeaf->Id );
if ( !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId0(pLeaf) ) )
@@ -825,6 +910,12 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves
if ( Ivy_ObjIsNode(pLeaf) && !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId1(pLeaf) ) )
continue;
Ivy_NodeCutHash( pCutNew );
+*/
+ iLeaf0 = Ivy_ObjFaninId0(pLeaf);
+ iLeaf1 = Ivy_ObjFaninId1(pLeaf);
+ if ( !Ivy_NodeCutPrescreen( pCut, iLeaf0, iLeaf1 ) )
+ continue;
+ Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 );
Ivy_NodeCutFindOrAddFilter( pCutStore, pCutNew );
if ( pCutStore->nCuts == IVY_CUT_LIMIT )
break;
diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c
index fb938c42..30671baf 100644
--- a/src/temp/ivy/ivyDfs.c
+++ b/src/temp/ivy/ivyDfs.c
@@ -250,6 +250,105 @@ Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p )
return vLevelsR;
}
+/**Function*************************************************************
+
+ Synopsis [Recursively detects combinational loops.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode )
+{
+ if ( Ivy_ObjIsCi(pNode) || Ivy_ObjIsConst1(pNode) )
+ return 1;
+ assert( Ivy_ObjIsNode( pNode ) );
+ // make sure the node is not visited
+ assert( !Ivy_ObjIsTravIdPrevious(p, pNode) );
+ // check if the node is part of the combinational loop
+ if ( Ivy_ObjIsTravIdCurrent(p, pNode) )
+ {
+ fprintf( stdout, "Manager contains combinational loop!\n" );
+ fprintf( stdout, "Node \"%d\" is encountered twice on the following path:\n", Ivy_ObjId(pNode) );
+ fprintf( stdout, " %d", Ivy_ObjId(pNode) );
+ return 0;
+ }
+ // mark this node as a node on the current path
+ Ivy_ObjSetTravIdCurrent( p, pNode );
+ // check if the fanin is visited
+ if ( !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin0(pNode)) )
+ {
+ // traverse the fanin's cone searching for the loop
+ if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pNode)) )
+ {
+ // return as soon as the loop is detected
+ fprintf( stdout, " <-- %d", Ivy_ObjId(Ivy_ObjFanin0(pNode)) );
+ return 0;
+ }
+ }
+ // check if the fanin is visited
+ if ( !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin1(pNode)) )
+ {
+ // traverse the fanin's cone searching for the loop
+ if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin1(pNode)) )
+ {
+ // return as soon as the loop is detected
+ fprintf( stdout, " <-- %d", Ivy_ObjId(Ivy_ObjFanin1(pNode)) );
+ return 0;
+ }
+ }
+ // mark this node as a visited node
+ Ivy_ObjSetTravIdPrevious( p, pNode );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Detects combinational loops.]
+
+ Description [This procedure is based on the idea suggested by Donald Chai.
+ As we traverse the network and visit the nodes, we need to distinquish
+ three types of nodes: (1) those that are visited for the first time,
+ (2) those that have been visited in this traversal but are currently not
+ on the traversal path, (3) those that have been visited and are currently
+ on the travesal path. When the node of type (3) is encountered, it means
+ that there is a combinational loop. To mark the three types of nodes,
+ two new values of the traversal IDs are used.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManIsAcyclic( Ivy_Man_t * p )
+{
+ Ivy_Obj_t * pNode;
+ int fAcyclic, i;
+ // set the traversal ID for this DFS ordering
+ Ivy_ManIncrementTravId( p );
+ Ivy_ManIncrementTravId( p );
+ // pNode->TravId == pNet->nTravIds means "pNode is on the path"
+ // pNode->TravId == pNet->nTravIds - 1 means "pNode is visited but is not on the path"
+ // pNode->TravId < pNet->nTravIds - 1 means "pNode is not visited"
+ // traverse the network to detect cycles
+ fAcyclic = 1;
+ Ivy_ManForEachCo( p, pNode, i )
+ {
+ if ( Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin0(pNode)) )
+ continue;
+ // traverse the output logic cone
+ if ( fAcyclic = Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pNode)) )
+ continue;
+ // stop as soon as the first loop is detected
+ fprintf( stdout, " (cone of CO \"%d\")\n", Ivy_ObjFaninId0(pNode) );
+ break;
+ }
+ return fAcyclic;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyFanout.c b/src/temp/ivy/ivyFanout.c
index 5911e051..2295516d 100644
--- a/src/temp/ivy/ivyFanout.c
+++ b/src/temp/ivy/ivyFanout.c
@@ -153,6 +153,7 @@ void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
assert( *ppSpot == pFanout );
*ppSpot = NULL;
}
+// printf( " %d", Ivy_ObjFanoutNum(p, pObj) );
}
/**Function*************************************************************
diff --git a/src/temp/ivy/ivyIsop.c b/src/temp/ivy/ivyIsop.c
index f53e513d..2d0101a7 100644
--- a/src/temp/ivy/ivyIsop.c
+++ b/src/temp/ivy/ivyIsop.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "ivy.h"
+#include "mem.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -33,7 +34,8 @@ struct Ivy_Sop_t_
static Mem_Flex_t * s_Man = NULL;
-static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes );
+static unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes );
+static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -41,7 +43,7 @@ static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy
/**Function*************************************************************
- Synopsis []
+ Synopsis [Deallocates memory used for computing ISOPs from TTs.]
Description []
@@ -50,14 +52,15 @@ static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy
SeeAlso []
***********************************************************************/
-void Ivy_TruthManStart()
+void Ivy_TruthManStop()
{
- s_Man = Mem_FlexStart();
+ Mem_FlexStop( s_Man, 0 );
+ s_Man = NULL;
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Computes ISOP from TT.]
Description []
@@ -66,15 +69,37 @@ void Ivy_TruthManStart()
SeeAlso []
***********************************************************************/
-void Ivy_TruthManStop()
+int Ivy_TruthIsopOne( unsigned * puTruth, int nVars, Vec_Int_t * vCover )
{
- Mem_FlexStop( s_Man, 0 );
- s_Man = NULL;
+ Ivy_Sop_t cRes, * pcRes = &cRes;
+ unsigned * pResult;
+ int i;
+ assert( nVars >= 0 && nVars < 16 );
+ // if nVars < 5, make sure it does not depend on those vars
+ for ( i = nVars; i < 5; i++ )
+ assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
+ // prepare memory manager
+ if ( s_Man == NULL )
+ s_Man = Mem_FlexStart();
+ else
+ Mem_FlexRestart( s_Man );
+ // compute ISOP
+ pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes );
+// Extra_PrintBinary( stdout, puTruth, 1 << nVars ); printf( "\n" );
+// Extra_PrintBinary( stdout, pResult, 1 << nVars ); printf( "\n" );
+ assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+//printf( "%d ", Mem_FlexReadMemUsage(s_Man) );
+//printf( "%d ", pcRes->nCubes );
+ // copy the truth table
+ Vec_IntClear( vCover );
+ for ( i = 0; i < pcRes->nCubes; i++ )
+ Vec_IntPush( vCover, pcRes->pCubes[i] );
+ return 0;
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Computes ISOP from TT.]
Description []
@@ -83,13 +108,51 @@ void Ivy_TruthManStop()
SeeAlso []
***********************************************************************/
-Vec_Int_t * Ivy_TruthIsop( unsigned * uTruth, int nVars )
+int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover )
{
+ Ivy_Sop_t cRes, * pcRes = &cRes;
+ unsigned * pResult;
+ int i;
+ assert( nVars >= 0 && nVars < 16 );
+ // if nVars < 5, make sure it does not depend on those vars
+ for ( i = nVars; i < 5; i++ )
+ assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
+ // prepare memory manager
+ if ( s_Man == NULL )
+ s_Man = Mem_FlexStart();
+ else
+ Mem_FlexRestart( s_Man );
+ // compute ISOP
+ pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes );
+// Extra_PrintBinary( stdout, puTruth, 1 << nVars ); printf( "\n" );
+// Extra_PrintBinary( stdout, pResult, 1 << nVars ); printf( "\n" );
+ assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+//printf( "%d ", Mem_FlexReadMemUsage(s_Man) );
+//printf( "%d ", pcRes->nCubes );
+ // copy the truth table
+ Vec_IntClear( vCover );
+ for ( i = 0; i < pcRes->nCubes; i++ )
+ Vec_IntPush( vCover, pcRes->pCubes[i] );
+
+ // try other polarity
+ Mem_FlexRestart( s_Man );
+ Extra_TruthNot( puTruth, puTruth, nVars );
+ pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes );
+ assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+ Extra_TruthNot( puTruth, puTruth, nVars );
+ if ( Vec_IntSize(vCover) < pcRes->nCubes )
+ return 0;
+
+ // copy the truth table
+ Vec_IntClear( vCover );
+ for ( i = 0; i < pcRes->nCubes; i++ )
+ Vec_IntPush( vCover, pcRes->pCubes[i] );
+ return 1;
}
/**Function*************************************************************
- Synopsis [Computes ISOP for 5 variables or less.]
+ Synopsis [Computes ISOP 6 variables or more.]
Description []
@@ -103,54 +166,59 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
Ivy_Sop_t cRes0, cRes1, cRes2;
Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
unsigned * puRes0, * puRes1, * puRes2;
- unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp0, * pTemp1;
- int i, k, Var, nWords;
- assert( nVars > 5 );
+ unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
+ int i, k, Var, nWords, nWordsAll;
assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) );
+ // allocate room for the resulting truth table
+ nWordsAll = Extra_TruthWordNum( nVars );
+ pTemp = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWordsAll );
+ // check for constants
if ( Extra_TruthIsConst0( puOn, nVars ) )
{
pcRes->nCubes = 0;
pcRes->pCubes = NULL;
- return puOn;
+ Extra_TruthClear( pTemp, nVars );
+ return pTemp;
}
if ( Extra_TruthIsConst1( puOnDc, nVars ) )
{
pcRes->nCubes = 1;
pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
pcRes->pCubes[0] = 0;
- return puOnDc;
+ Extra_TruthFill( pTemp, nVars );
+ return pTemp;
}
+ assert( nVars > 0 );
// find the topmost var
for ( Var = nVars-1; Var >= 0; Var-- )
if ( Extra_TruthVarInSupport( puOn, nVars, Var ) ||
Extra_TruthVarInSupport( puOnDc, nVars, Var ) )
break;
assert( Var >= 0 );
+ // consider a simple case when one-word computation can be used
if ( Var < 5 )
{
- unsigned * puRes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
- *puRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var + 1, pcRes );
- return puRes;
+ unsigned uRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes );
+ for ( i = 0; i < nWordsAll; i++ )
+ pTemp[i] = uRes;
+ return pTemp;
}
- nWords = Extra_TruthWordNum( Var+1 );
+ assert( Var >= 5 );
+ nWords = Extra_TruthWordNum( Var );
// cofactor
- puOn0 = puOn;
- puOn1 = puOn + nWords;
- puOnDc0 = puOnDc;
- puOnDc1 = puOnDc + nWords;
- // intermediate copies
- pTemp0 = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWords );
- pTemp1 = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWords );
+ puOn0 = puOn; puOn1 = puOn + nWords;
+ puOnDc0 = puOnDc; puOnDc1 = puOnDc + nWords;
+ pTemp0 = pTemp; pTemp1 = pTemp + nWords;
// solve for cofactors
- Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var + 1 );
- puRes0 = Ivy_TruthIsop5_rec( pTemp0, uOnDc0, Var-1, pcRes0 );
- Extra_TruthSharp( pTemp0, puOn1, puOnDc0, Var + 1 );
- puRes1 = Ivy_TruthIsop5_rec( pTemp1, uOnDc1, Var-1, pcRes1 );
- Extra_TruthSharp( pTemp0, puOn0, puRes0, Var + 1 );
- Extra_TruthSharp( pTemp1, puOn1, puRes1, Var + 1 );
- Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var + 1 );
- Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var + 1 );
- puRes2 = Ivy_TruthIsop5_rec( pTemp0, pTemp1, Var-1, pcRes2 );
+ Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
+ puRes0 = Ivy_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0 );
+ Extra_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
+ puRes1 = Ivy_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1 );
+ Extra_TruthSharp( pTemp0, puOn0, puRes0, Var );
+ Extra_TruthSharp( pTemp1, puOn1, puRes1, Var );
+ Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var );
+ Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
+ puRes2 = Ivy_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2 );
// create the resulting cover
pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes );
@@ -159,13 +227,21 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
for ( i = 0; i < pcRes1->nCubes; i++ )
pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0));
- for ( i = 0; i < pcRes1->nCubes; i++ )
+ for ( i = 0; i < pcRes2->nCubes; i++ )
pcRes->pCubes[k++] = pcRes2->pCubes[i];
assert( k == pcRes->nCubes );
// create the resulting truth table
- Extra_TruthSharp( pTemp0, Var, uRes0, uRes1, Var + 1 );
- Extra_TruthOr( pTemp0, pTemp0, uRes2, Var + 1 );
- return pTemp0;
+ Extra_TruthOr( pTemp0, puRes0, puRes2, Var );
+ Extra_TruthOr( pTemp1, puRes1, puRes2, Var );
+ // copy the table if needed
+ nWords <<= 1;
+ for ( i = 1; i < nWordsAll/nWords; i++ )
+ for ( k = 0; k < nWords; k++ )
+ pTemp[i*nWords + k] = pTemp[k];
+ // verify in the end
+// assert( Extra_TruthIsImply( puOn, pTemp, nVars ) );
+// assert( Extra_TruthIsImply( pTemp, puOnDc, nVars ) );
+ return pTemp;
}
/**Function*************************************************************
@@ -184,12 +260,11 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
Ivy_Sop_t cRes0, cRes1, cRes2;
Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
- unsigned uRes0, uRes1, uRes2;
- unsigned uOn0, uOn1, uOnDc0, uOnDc1;
+ unsigned uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
int i, k, Var;
assert( nVars <= 5 );
- assert( uOn & ~uOnDc == 0 );
- if ( Extra_TruthIsConst0( uOn == 0 )
+ assert( (uOn & ~uOnDc) == 0 );
+ if ( uOn == 0 )
{
pcRes->nCubes = 0;
pcRes->pCubes = NULL;
@@ -202,6 +277,7 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
pcRes->pCubes[0] = 0;
return 0xFFFFFFFF;
}
+ assert( nVars > 0 );
// find the topmost var
for ( Var = nVars-1; Var >= 0; Var-- )
if ( Extra_TruthVarInSupport( &uOn, 5, Var ) ||
@@ -209,16 +285,16 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
break;
assert( Var >= 0 );
// cofactor
- uOn0 = uOn1 = uOn;
+ uOn0 = uOn1 = uOn;
uOnDc0 = uOnDc1 = uOnDc;
- Extra_TruthCofactor0( &uOn0, 5, Var );
- Extra_TruthCofactor1( &uOn1, 5, Var );
- Extra_TruthCofactor0( &uOnDc0, 5, Var );
- Extra_TruthCofactor1( &uOnDc1, 5, Var );
+ Extra_TruthCofactor0( &uOn0, Var + 1, Var );
+ Extra_TruthCofactor1( &uOn1, Var + 1, Var );
+ Extra_TruthCofactor0( &uOnDc0, Var + 1, Var );
+ Extra_TruthCofactor1( &uOnDc1, Var + 1, Var );
// solve for cofactors
- uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var-1, pcRes0 );
- uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var-1, pcRes1 );
- uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var-1, pcRes2 );
+ uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0 );
+ uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1 );
+ uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2 );
// create the resulting cover
pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes );
@@ -227,10 +303,14 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
for ( i = 0; i < pcRes1->nCubes; i++ )
pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0));
- for ( i = 0; i < pcRes1->nCubes; i++ )
+ for ( i = 0; i < pcRes2->nCubes; i++ )
pcRes->pCubes[k++] = pcRes2->pCubes[i];
assert( k == pcRes->nCubes );
- return (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]) | uRes2;
+ // derive the final truth table
+ uRes2 |= (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]);
+// assert( (uOn & ~uRes2) == 0 );
+// assert( (uRes2 & ~uOnDc) == 0 );
+ return uRes2;
}
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index d1aca8a6..c5b66ad0 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -109,9 +109,10 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
Ivy_Obj_t * pNode;
int i, nNodesOld;
nNodesOld = Ivy_ManNodeNum(p);
- Ivy_ManForEachNode( p, pNode, i )
- if ( Ivy_ObjRefs(pNode) == 0 )
- Ivy_ObjDelete_rec( p, pNode, 1 );
+ Ivy_ManForEachObj( p, pNode, i )
+ if ( Ivy_ObjIsNode(pNode) || Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) )
+ if ( Ivy_ObjRefs(pNode) == 0 )
+ Ivy_ObjDelete_rec( p, pNode, 1 );
return nNodesOld - Ivy_ManNodeNum(p);
}
@@ -126,7 +127,7 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
SeeAlso []
***********************************************************************/
-int Ivy_ManPropagateBuffers( Ivy_Man_t * p )
+int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
{
Ivy_Obj_t * pNode;
int nSteps;
@@ -135,7 +136,7 @@ int Ivy_ManPropagateBuffers( Ivy_Man_t * p )
pNode = Vec_PtrEntryLast(p->vBufs);
while ( Ivy_ObjIsBuf(pNode) )
pNode = Ivy_ObjReadFirstFanout( p, pNode );
- Ivy_NodeFixBufferFanins( p, pNode );
+ Ivy_NodeFixBufferFanins( p, pNode, fUpdateLevel );
}
// printf( "Number of steps = %d\n", nSteps );
return nSteps;
@@ -200,6 +201,9 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits )
pObj = Ivy_ManPo( p, Ivy_ManPoNum(p) - nLatches + i );
pLatch = Ivy_Latch( p, Ivy_ObjChild0(pObj), Init );
Ivy_ObjDisconnect( p, pObj );
+ // recycle the old PO object
+ Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+ Ivy_ManRecycleMemory( p, pObj );
// convert the corresponding PI to a buffer and connect it to the latch
pObj = Ivy_ManPi( p, Ivy_ManPiNum(p) - nLatches + i );
pObj->Type = IVY_BUF;
@@ -215,8 +219,21 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits )
p->nObjs[IVY_PO] -= nLatches;
p->nObjs[IVY_BUF] += nLatches;
p->nDeleted -= 2 * nLatches;
+ // remove dangling nodes
+ Ivy_ManCleanup(p);
+/*
+ // check for dangling nodes
+ Ivy_ManForEachObj( p, pObj, i )
+ if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsPo(pObj) && !Ivy_ObjIsConst1(pObj) )
+ {
+ assert( Ivy_ObjRefs(pObj) > 0 );
+ assert( Ivy_ObjRefs(pObj) == Ivy_ObjFanoutNum(p, pObj) );
+ }
+*/
// perform hashing by propagating the buffers
- Ivy_ManPropagateBuffers( p );
+ Ivy_ManPropagateBuffers( p, 0 );
+ // fix the levels
+ Ivy_ManResetLevels( p );
// check the resulting network
if ( !Ivy_ManCheck(p) )
printf( "Ivy_ManMakeSeq(): The check has failed.\n" );
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index de67c560..735d79c3 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -300,7 +300,7 @@ void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
SeeAlso []
***********************************************************************/
-void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop )
+void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel )
{
int nRefsOld;
// the object to be replaced cannot be complemented
@@ -315,26 +315,32 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) );
assert( !Ivy_IsComplement(pObjNew) );
- // if the new node's arrival time is different, recursively update arrival time of the fanouts
- if ( p->vFanouts && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
+ if ( fUpdateLevel )
{
- assert( Ivy_ObjIsNode(pObjOld) );
- pObjOld->Level = pObjNew->Level;
- Ivy_ObjUpdateLevel_rec( p, pObjOld );
- }
- // if the new node's required time has changed, recursively update required time of the fanins
- if ( p->vRequired )
- {
- int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id);
- if ( ReqNew < Vec_IntEntry(p->vRequired, pObjNew->Id) )
+ // if the new node's arrival time is different, recursively update arrival time of the fanouts
+ if ( p->vFanouts && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
+ {
+ assert( Ivy_ObjIsNode(pObjOld) );
+ pObjOld->Level = pObjNew->Level;
+ Ivy_ObjUpdateLevel_rec( p, pObjOld );
+ }
+ // if the new node's required time has changed, recursively update required time of the fanins
+ if ( p->vRequired )
{
- Vec_IntWriteEntry( p->vRequired, pObjNew->Id, ReqNew );
- Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew );
+ int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id);
+ if ( ReqNew < Vec_IntEntry(p->vRequired, pObjNew->Id) )
+ {
+ Vec_IntWriteEntry( p->vRequired, pObjNew->Id, ReqNew );
+ Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew );
+ }
}
}
// delete the old object
if ( fDeleteOld )
Ivy_ObjDelete_rec( p, pObjOld, fFreeTop );
+ // make sure object is pointing to itself
+ assert( Ivy_ObjFanin0(pObjNew) == NULL || pObjOld != Ivy_ObjFanin0(pObjNew) );
+ assert( Ivy_ObjFanin1(pObjNew) == NULL || pObjOld != Ivy_ObjFanin1(pObjNew) );
// transfer the old object
assert( Ivy_ObjRefs(pObjNew) == 0 );
nRefsOld = pObjOld->nRefs;
@@ -370,7 +376,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
SeeAlso []
***********************************************************************/
-void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode )
+void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel )
{
Ivy_Obj_t * pFanReal0, * pFanReal1, * pResult;
if ( Ivy_ObjIsPo(pNode) )
@@ -394,7 +400,7 @@ void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode )
else
assert( 0 );
// perform the replacement
- Ivy_ObjReplace( p, pNode, pResult, 1, 0 );
+ Ivy_ObjReplace( p, pNode, pResult, 1, 0, fUpdateLevel );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyRwrAlg.c b/src/temp/ivy/ivyRwrAlg.c
index 234827ff..fc48deb0 100644
--- a/src/temp/ivy/ivyRwrAlg.c
+++ b/src/temp/ivy/ivyRwrAlg.c
@@ -80,7 +80,7 @@ int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost )
// the case of constant 0 cone
if ( RetValue == -1 )
{
- Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0 );
+ Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0, 1 );
continue;
}
assert( Vec_PtrSize(vLeaves) > 2 );
@@ -94,7 +94,7 @@ int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost )
if ( Ivy_ObjLevel(Ivy_Regular(pResult)) > LevelR && Ivy_ObjRefs(Ivy_Regular(pResult)) == 0 )
Ivy_ObjDelete_rec(Ivy_Regular(pResult), 1), CountUndo++;
else
- Ivy_ObjReplace( pObj, pResult, 1, 0 ), CountUsed++;
+ Ivy_ObjReplace( pObj, pResult, 1, 0, 1 ), CountUsed++;
}
printf( "Used = %d. Undo = %d.\n", CountUsed, CountUndo );
Vec_PtrFree( vFront );
diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwrPre.c
index d2a1697e..537b64ff 100644
--- a/src/temp/ivy/ivyRwrPre.c
+++ b/src/temp/ivy/ivyRwrPre.c
@@ -27,9 +27,8 @@
////////////////////////////////////////////////////////////////////////
static unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums );
-static int Ivy_NodeMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pObj );
static int Ivy_NodeRewrite( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost );
-static Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut,
+static Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot,
Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth );
static int Ivy_GraphToNetworkCount( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
@@ -74,7 +73,7 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
Ivy_ManForEachNode( p, pNode, i )
{
// fix the fanin buffer problem
- Ivy_NodeFixBufferFanins( p, pNode );
+ Ivy_NodeFixBufferFanins( p, pNode, 1 );
if ( Ivy_ObjIsBuf(pNode) )
continue;
// stop if all nodes have been tried once
@@ -120,8 +119,8 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
// fix the levels
if ( fUpdateLevel )
Vec_IntFree( p->vRequired ), p->vRequired = NULL;
-// else
-// Ivy_ManResetLevels( p );
+ else
+ Ivy_ManResetLevels( p );
// check
if ( i = Ivy_ManCleanup(p) )
printf( "Cleanup after rewriting removed %d dangling nodes.\n", i );
@@ -182,7 +181,11 @@ clk = clock();
if ( Ivy_ObjIsBuf( Ivy_ManObj(pMan, pCut->pArray[i]) ) )
break;
if ( i != pCut->nSize )
+ {
+ p->nCutsBad++;
continue;
+ }
+ p->nCutsGood++;
// get the fanin permutation
clk2 = clock();
uTruth = 0xFFFF & Ivy_NodeGetTruth( pNode, pCut->pArray, pCut->nSize ); // truth table
@@ -211,7 +214,7 @@ clk2 = clock();
Ivy_ObjRefsInc( Ivy_Regular(pFanin) );
// label MFFC with current ID
Ivy_ManIncrementTravId( pMan );
- nNodesSaved = Ivy_NodeMffcLabel( pMan, pNode );
+ nNodesSaved = Ivy_ObjMffcLabel( pMan, pNode );
// unmark the fanin boundary
Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
@@ -219,7 +222,7 @@ p->timeMffc += clock() - clk2;
// evaluate the cut
clk2 = clock();
- pGraph = Rwt_CutEvaluate( pMan, p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth );
+ pGraph = Rwt_CutEvaluate( pMan, p, pNode, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth );
p->timeEval += clock() - clk2;
// check if the cut is better than the current best one
@@ -289,75 +292,6 @@ p->timeRes += clock() - clk;
return GainBest;
}
-
-/**Function*************************************************************
-
- Synopsis [References/references the node and returns MFFC size.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ivy_NodeRefDeref( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fReference, int fLabel )
-{
- Ivy_Obj_t * pNode0, * pNode1;
- int Counter;
- // label visited nodes
- if ( fLabel )
- Ivy_ObjSetTravIdCurrent( p, pNode );
- // skip the CI
- if ( Ivy_ObjIsCi(pNode) )
- return 0;
- assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) );
- // process the internal node
- pNode0 = Ivy_ObjFanin0(pNode);
- pNode1 = Ivy_ObjFanin1(pNode);
- Counter = Ivy_ObjIsNode(pNode);
- if ( fReference )
- {
- if ( pNode0->nRefs++ == 0 )
- Counter += Ivy_NodeRefDeref( p, pNode0, fReference, fLabel );
- if ( pNode1 && pNode1->nRefs++ == 0 )
- Counter += Ivy_NodeRefDeref( p, pNode1, fReference, fLabel );
- }
- else
- {
- assert( pNode0->nRefs > 0 );
- assert( pNode1 == NULL || pNode1->nRefs > 0 );
- if ( --pNode0->nRefs == 0 )
- Counter += Ivy_NodeRefDeref( p, pNode0, fReference, fLabel );
- if ( pNode1 && --pNode1->nRefs == 0 )
- Counter += Ivy_NodeRefDeref( p, pNode1, fReference, fLabel );
- }
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes the size of MFFC and labels nodes with the current TravId.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ivy_NodeMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pNode )
-{
- int nConeSize1, nConeSize2;
- assert( !Ivy_IsComplement( pNode ) );
- assert( Ivy_ObjIsNode( pNode ) );
- nConeSize1 = Ivy_NodeRefDeref( p, pNode, 0, 1 ); // dereference
- nConeSize2 = Ivy_NodeRefDeref( p, pNode, 1, 0 ); // reference
- assert( nConeSize1 == nConeSize2 );
- assert( nConeSize1 > 0 );
- return nConeSize1;
-}
-
/**Function*************************************************************
Synopsis [Computes the truth table.]
@@ -418,7 +352,7 @@ unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums )
SeeAlso []
***********************************************************************/
-Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth )
+Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth )
{
Vec_Ptr_t * vSubgraphs;
Dec_Graph_t * pGraphBest, * pGraphCur;
@@ -596,12 +530,12 @@ void Ivy_GraphUpdateNetwork( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGr
printf( "%d", Ivy_ObjRefs(Ivy_Regular(pRootNew)) );
printf( " " );
*/
- Ivy_ObjReplace( p, pRoot, pRootNew, 1, 0 );
+ Ivy_ObjReplace( p, pRoot, pRootNew, 1, 0, 1 );
// compare the gains
nNodesNew = Ivy_ManNodeNum(p);
assert( nGain <= nNodesOld - nNodesNew );
// propagate the buffer
- Ivy_ManPropagateBuffers( p );
+ Ivy_ManPropagateBuffers( p, 1 );
}
/**Function*************************************************************
@@ -649,7 +583,7 @@ void Ivy_GraphUpdateNetwork3( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pG
printf( "%d", Ivy_ObjRefs(Ivy_Regular(pRootNew)) );
printf( " " );
*/
- Ivy_ObjReplace( p, pRoot, pRootNew, 0, 0 );
+ Ivy_ObjReplace( p, pRoot, pRootNew, 0, 0, 1 );
//printf( "Replace = %d. ", Ivy_ManNodeNum(p) );
// delete remaining dangling nodes
diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c
index 1cfa8c4b..8fd1b63b 100644
--- a/src/temp/ivy/ivySeq.c
+++ b/src/temp/ivy/ivySeq.c
@@ -13,17 +13,28 @@
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
-
+
Revision [$Id: ivySeq.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ivy.h"
+#include "deco.h"
+#include "rwt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+static int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUseZeroCost );
+static void Ivy_GraphPrepare( Dec_Graph_t * pGraph, Ivy_Cut_t * pCut, Vec_Ptr_t * vFanins, char * pPerm );
+static unsigned Ivy_CutGetTruth( Ivy_Man_t * p, Ivy_Obj_t * pObj, int * pNums, int nNums );
+static Dec_Graph_t * Rwt_CutEvaluateSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, char * pPerm, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int * pGainBest, unsigned uTruth );
+static int Ivy_GraphToNetworkSeqCountSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax );
+static Ivy_Obj_t * Ivy_GraphToNetworkSeq( Ivy_Man_t * p, Dec_Graph_t * pGraph );
+static void Ivy_GraphUpdateNetworkSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain );
+static Ivy_Store_t * Ivy_CutComputeForNode( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves );
+
static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); }
////////////////////////////////////////////////////////////////////////
@@ -32,6 +43,295 @@ static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); }
/**Function*************************************************************
+ Synopsis [Performs incremental rewriting of the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
+{
+ Rwt_Man_t * pManRwt;
+ Ivy_Obj_t * pNode;
+ int i, nNodes, nGain;
+ int clk, clkStart = clock();
+ // start the rewriting manager
+ pManRwt = Rwt_ManStart( 0 );
+ p->pData = pManRwt;
+ if ( pManRwt == NULL )
+ return 0;
+ // create fanouts
+ if ( p->vFanouts == NULL )
+ Ivy_ManStartFanout( p );
+ // resynthesize each node once
+ nNodes = Ivy_ManObjIdMax(p);
+ Ivy_ManForEachNode( p, pNode, i )
+ {
+ assert( !Ivy_ObjIsBuf(pNode) );
+ assert( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) );
+ assert( !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) );
+ // fix the fanin buffer problem
+// Ivy_NodeFixBufferFanins( p, pNode );
+// if ( Ivy_ObjIsBuf(pNode) )
+// continue;
+ // stop if all nodes have been tried once
+ if ( i > nNodes )
+ break;
+ if ( i == 8648 )
+ {
+ int x = 0;
+ }
+ // for each cut, try to resynthesize it
+ nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost );
+ if ( nGain > 0 || nGain == 0 && fUseZeroCost )
+ {
+ Dec_Graph_t * pGraph = Rwt_ManReadDecs(pManRwt);
+ int fCompl = Rwt_ManReadCompl(pManRwt);
+ // complement the FF if needed
+clk = clock();
+ if ( fCompl ) Dec_GraphComplement( pGraph );
+ Ivy_GraphUpdateNetworkSeq( p, pNode, pGraph, nGain );
+ if ( fCompl ) Dec_GraphComplement( pGraph );
+Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
+/*
+ if ( !Ivy_ManIsAcyclic(p) )
+ {
+ int x = 0;
+ }
+*/
+ }
+ }
+Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
+ // print stats
+ if ( fVerbose )
+ Rwt_ManPrintStats( pManRwt );
+ // delete the managers
+ Rwt_ManStop( pManRwt );
+ p->pData = NULL;
+ // fix the levels
+ Ivy_ManResetLevels( p );
+ // check
+ if ( !Ivy_ManCheck(p) )
+ printf( "Ivy_ManRewritePre(): The check has failed.\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs rewriting for one node.]
+
+ Description [This procedure considers all the cuts computed for the node
+ and tries to rewrite each of them using the "forest" of different AIG
+ structures precomputed and stored in the RWR manager.
+ Determines the best rewriting and computes the gain in the number of AIG
+ nodes in the final network. In the end, p->vFanins contains information
+ about the best cut that can be used for rewriting, while p->pGraph gives
+ the decomposition dag (represented using decomposition graph data structure).
+ Returns gain in the number of nodes or -1 if node cannot be rewritten.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUseZeroCost )
+{
+ int fVeryVerbose = 0;
+ Dec_Graph_t * pGraph;
+ Ivy_Store_t * pStore;
+ Ivy_Cut_t * pCut;
+ Ivy_Obj_t * pFanin;
+ unsigned uPhase, uTruthBest, uTruth;
+ char * pPerm;
+ int nNodesSaved, nNodesSaveCur;
+ int i, c, GainCur, GainBest = -1;
+ int clk, clk2;
+
+ p->nNodesConsidered++;
+ // get the node's cuts
+clk = clock();
+ pStore = Ivy_CutComputeForNode( pMan, pNode, 5 );
+p->timeCut += clock() - clk;
+
+ // go through the cuts
+clk = clock();
+ for ( c = 1; c < pStore->nCuts; c++ )
+ {
+ pCut = pStore->pCuts + c;
+ // consider only 4-input cuts
+ if ( pCut->nSize != 4 )
+ continue;
+ // skip the cuts with buffers
+ for ( i = 0; i < (int)pCut->nSize; i++ )
+ if ( Ivy_ObjIsBuf( Ivy_ManObj(pMan, Ivy_LeafId(pCut->pArray[i])) ) )
+ break;
+ if ( i != pCut->nSize )
+ {
+ p->nCutsBad++;
+ continue;
+ }
+ p->nCutsGood++;
+ // get the fanin permutation
+clk2 = clock();
+ uTruth = 0xFFFF & Ivy_CutGetTruth( pMan, pNode, pCut->pArray, pCut->nSize ); // truth table
+p->timeTruth += clock() - clk2;
+ pPerm = p->pPerms4[ p->pPerms[uTruth] ];
+ uPhase = p->pPhases[uTruth];
+ // collect fanins with the corresponding permutation/phase
+ Vec_PtrClear( p->vFaninsCur );
+ Vec_PtrFill( p->vFaninsCur, (int)pCut->nSize, 0 );
+ for ( i = 0; i < (int)pCut->nSize; i++ )
+ {
+ pFanin = Ivy_ManObj( pMan, Ivy_LeafId( pCut->pArray[pPerm[i]] ) );
+ assert( Ivy_ObjIsNode(pFanin) || Ivy_ObjIsCi(pFanin) || Ivy_ObjIsConst1(pFanin) );
+ pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) );
+ Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
+ }
+clk2 = clock();
+ // mark the fanin boundary
+ Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+ Ivy_ObjRefsInc( Ivy_Regular(pFanin) );
+ // label MFFC with current ID
+ Ivy_ManIncrementTravId( pMan );
+ nNodesSaved = Ivy_ObjMffcLabel( pMan, pNode );
+ // unmark the fanin boundary
+ Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+ Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
+p->timeMffc += clock() - clk2;
+/*
+if ( pNode->Id == 8648 )
+{
+ int i;
+ printf( "Trying cut : {" );
+ for ( i = 0; i < pCut->nSize; i++ )
+ printf( " %d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
+// printf( " }\n" );
+ printf( " } " );
+ Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" );
+}
+*/
+
+ // evaluate the cut
+clk2 = clock();
+ pGraph = Rwt_CutEvaluateSeq( pMan, p, pNode, pCut, pPerm, p->vFaninsCur, nNodesSaved, &GainCur, uTruth );
+p->timeEval += clock() - clk2;
+
+
+ // check if the cut is better than the current best one
+ if ( pGraph != NULL && GainBest < GainCur )
+ {
+ // save this form
+ nNodesSaveCur = nNodesSaved;
+ GainBest = GainCur;
+ p->pGraph = pGraph;
+ p->pCut = pCut;
+ p->pPerm = pPerm;
+ p->fCompl = ((uPhase & (1<<4)) > 0);
+ uTruthBest = uTruth;
+ // collect fanins in the
+ Vec_PtrClear( p->vFanins );
+ Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+ Vec_PtrPush( p->vFanins, pFanin );
+ }
+ }
+p->timeRes += clock() - clk;
+
+ if ( GainBest == -1 )
+ return -1;
+
+ // copy the leaves
+ Ivy_GraphPrepare( p->pGraph, p->pCut, p->vFanins, p->pPerm );
+
+ p->nScores[p->pMap[uTruthBest]]++;
+ p->nNodesGained += GainBest;
+ if ( fUseZeroCost || GainBest > 0 )
+ p->nNodesRewritten++;
+
+/*
+ if ( GainBest > 0 )
+ {
+ Ivy_Cut_t * pCut = p->pCut;
+ printf( "Useful cut : {" );
+ for ( i = 0; i < pCut->nSize; i++ )
+ printf( " %5d[%2d](%2d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]),
+ Ivy_ObjRefs( Ivy_ManObj(pMan, Ivy_LeafId(pCut->pArray[i])) ) );
+ printf( " }\n" );
+ }
+*/
+
+ // report the progress
+ if ( fVeryVerbose && GainBest > 0 )
+ {
+ printf( "Node %6d : ", Ivy_ObjId(pNode) );
+ printf( "Fanins = %d. ", p->vFanins->nSize );
+ printf( "Save = %d. ", nNodesSaveCur );
+ printf( "Add = %d. ", nNodesSaveCur-GainBest );
+ printf( "GAIN = %d. ", GainBest );
+ printf( "Cone = %d. ", p->pGraph? Dec_GraphNodeNum(p->pGraph) : 0 );
+ printf( "Class = %d. ", p->pMap[uTruthBest] );
+ printf( "\n" );
+ }
+ return GainBest;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Evaluates the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Graph_t * Rwt_CutEvaluateSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, char * pPerm, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int * pGainBest, unsigned uTruth )
+{
+ Vec_Ptr_t * vSubgraphs;
+ Dec_Graph_t * pGraphBest, * pGraphCur;
+ Rwt_Node_t * pNode;
+ int nNodesAdded, GainBest, i;
+ // find the matching class of subgraphs
+ vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[uTruth] );
+ p->nSubgraphs += vSubgraphs->nSize;
+ // determine the best subgraph
+ GainBest = -1;
+ Vec_PtrForEachEntry( vSubgraphs, pNode, i )
+ {
+ // get the current graph
+ pGraphCur = (Dec_Graph_t *)pNode->pNext;
+
+// if ( pRoot->Id == 8648 )
+// Dec_GraphPrint( stdout, pGraphCur, NULL, NULL );
+ // copy the leaves
+// Vec_PtrForEachEntry( vFaninsCur, pFanin, k )
+// Dec_GraphNode(pGraphCur, k)->pFunc = pFanin;
+ Ivy_GraphPrepare( pGraphCur, pCut, vFaninsCur, pPerm );
+
+ // detect how many unlabeled nodes will be reused
+ nNodesAdded = Ivy_GraphToNetworkSeqCountSeq( pMan, pRoot, pGraphCur, nNodesSaved );
+ if ( nNodesAdded == -1 )
+ continue;
+ assert( nNodesSaved >= nNodesAdded );
+ // count the gain at this node
+ if ( GainBest < nNodesSaved - nNodesAdded )
+ {
+ GainBest = nNodesSaved - nNodesAdded;
+ pGraphBest = pGraphCur;
+ }
+ }
+ if ( GainBest == -1 )
+ return NULL;
+ *pGainBest = GainBest;
+ return pGraphBest;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -41,8 +341,250 @@ static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); }
SeeAlso []
***********************************************************************/
+void Ivy_GraphPrepare( Dec_Graph_t * pGraph, Ivy_Cut_t * pCut, Vec_Ptr_t * vFanins, char * pPerm )
+{
+ Dec_Node_t * pNode, * pNode0, * pNode1;
+ int i;
+ assert( Dec_GraphLeaveNum(pGraph) == pCut->nSize );
+ assert( Vec_PtrSize(vFanins) == pCut->nSize );
+ // label the leaves with latch numbers
+ Dec_GraphForEachLeaf( pGraph, pNode, i )
+ {
+ pNode->pFunc = Vec_PtrEntry( vFanins, i );
+ pNode->nLat2 = Ivy_LeafLat( pCut->pArray[pPerm[i]] );
+ }
+ // propagate latches through the nodes
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ // get the children of this node
+ pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node );
+ pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node );
+ // distribute the latches
+ pNode->nLat2 = IVY_MIN( pNode0->nLat2, pNode1->nLat2 );
+ pNode->nLat0 = pNode0->nLat2 - pNode->nLat2;
+ pNode->nLat1 = pNode1->nLat2 - pNode->nLat2;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of new nodes added when using this graph.]
+
+ Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+ of the leaves of the graph before calling this procedure.
+ Returns -1 if the number of nodes and levels exceeded the given limit or
+ the number of levels exceeded the maximum allowed level.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_GraphToNetworkSeqCountSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax )
+{
+ Dec_Node_t * pNode, * pNode0, * pNode1;
+ Ivy_Obj_t * pAnd, * pAnd0, * pAnd1;
+ int i, k, Counter, fCompl;
+ // check for constant function or a literal
+ if ( Dec_GraphIsConst(pGraph) || Dec_GraphIsVar(pGraph) )
+ return 0;
+ // compute the AIG size after adding the internal nodes
+ Counter = 0;
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ // get the children of this node
+ pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node );
+ pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node );
+ // get the AIG nodes corresponding to the children
+ pAnd0 = pNode0->pFunc;
+ pAnd1 = pNode1->pFunc;
+ // skip the latches
+ for ( k = 0; pAnd0 && k < (int)pNode->nLat0; k++ )
+ {
+ fCompl = Ivy_IsComplement(pAnd0);
+ pAnd0 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Regular(pAnd0), NULL, IVY_LATCH, IVY_INIT_DC) );
+ if ( pAnd0 )
+ pAnd0 = Ivy_NotCond( pAnd0, fCompl );
+ }
+ for ( k = 0; pAnd1 && k < (int)pNode->nLat1; k++ )
+ {
+ fCompl = Ivy_IsComplement(pAnd1);
+ pAnd1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Regular(pAnd1), NULL, IVY_LATCH, IVY_INIT_DC) );
+ if ( pAnd1 )
+ pAnd1 = Ivy_NotCond( pAnd1, fCompl );
+ }
+ // get the new node
+ if ( pAnd0 && pAnd1 )
+ {
+ // if they are both present, find the resulting node
+ pAnd0 = Ivy_NotCond( pAnd0, pNode->eEdge0.fCompl );
+ pAnd1 = Ivy_NotCond( pAnd1, pNode->eEdge1.fCompl );
+ assert( !Ivy_ObjIsLatch(Ivy_Regular(pAnd0)) || !Ivy_ObjIsLatch(Ivy_Regular(pAnd1)) );
+ if ( Ivy_Regular(pAnd0) == Ivy_Regular(pAnd1) || Ivy_ObjIsConst1(Ivy_Regular(pAnd0)) || Ivy_ObjIsConst1(Ivy_Regular(pAnd1)) )
+ pAnd = Ivy_And( p, pAnd0, pAnd1 );
+ else
+ pAnd = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pAnd0, pAnd1, IVY_AND, IVY_INIT_NONE) );
+ // return -1 if the node is the same as the original root
+ if ( Ivy_Regular(pAnd) == pRoot )
+ return -1;
+ }
+ else
+ pAnd = NULL;
+ // count the number of added nodes
+ if ( pAnd == NULL || Ivy_ObjIsTravIdCurrent(p, Ivy_Regular(pAnd)) )
+ {
+ if ( ++Counter > NodeMax )
+ return -1;
+ }
+ pNode->pFunc = pAnd;
+ }
+ return Counter;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the decomposition graph into the AIG.]
+
+ Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+ of the leaves of the graph before calling this procedure.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_GraphToNetworkSeq( Ivy_Man_t * p, Dec_Graph_t * pGraph )
+{
+ Ivy_Obj_t * pAnd0, * pAnd1;
+ Dec_Node_t * pNode;
+ int i, k;
+ // check for constant function
+ if ( Dec_GraphIsConst(pGraph) )
+ return Ivy_NotCond( Ivy_ManConst1(p), Dec_GraphIsComplement(pGraph) );
+ // check for a literal
+ if ( Dec_GraphIsVar(pGraph) )
+ {
+ // get the variable node
+ pNode = Dec_GraphVar(pGraph);
+ // add the remaining latches
+ for ( k = 0; k < (int)pNode->nLat2; k++ )
+ pNode->pFunc = Ivy_Latch( p, pNode->pFunc, IVY_INIT_DC );
+ return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+ }
+ // build the AIG nodes corresponding to the AND gates of the graph
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+ // add the latches
+ for ( k = 0; k < (int)pNode->nLat0; k++ )
+ pAnd0 = Ivy_Latch( p, pAnd0, IVY_INIT_DC );
+ for ( k = 0; k < (int)pNode->nLat1; k++ )
+ pAnd1 = Ivy_Latch( p, pAnd1, IVY_INIT_DC );
+ // create the node
+ pNode->pFunc = Ivy_And( p, pAnd0, pAnd1 );
+ }
+ // add the remaining latches
+ for ( k = 0; k < (int)pNode->nLat2; k++ )
+ pNode->pFunc = Ivy_Latch( p, pNode->pFunc, IVY_INIT_DC );
+ // complement the result if necessary
+ return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Replaces MFFC of the node by the new factored form.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_GraphUpdateNetworkSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain )
+{
+ Ivy_Obj_t * pRootNew;
+ int nNodesNew, nNodesOld;
+ nNodesOld = Ivy_ManNodeNum(p);
+ // create the new structure of nodes
+ pRootNew = Ivy_GraphToNetworkSeq( p, pGraph );
+ Ivy_ObjReplace( p, pRoot, pRootNew, 1, 0, 0 );
+ // compare the gains
+ nNodesNew = Ivy_ManNodeNum(p);
+ assert( nGain <= nNodesOld - nNodesNew );
+ // propagate the buffer
+ Ivy_ManPropagateBuffers( p, 0 );
+}
+
+
+
+
+
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Ivy_CutGetTruth_rec( Ivy_Man_t * p, int Leaf, int * pNums, int nNums )
+{
+ static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+ unsigned uTruth0, uTruth1;
+ Ivy_Obj_t * pObj;
+ int i;
+ for ( i = 0; i < nNums; i++ )
+ if ( Leaf == pNums[i] )
+ return uMasks[i];
+ pObj = Ivy_ManObj( p, Ivy_LeafId(Leaf) );
+ if ( Ivy_ObjIsLatch(pObj) )
+ {
+ assert( !Ivy_ObjFaninC0(pObj) );
+ Leaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pObj), Ivy_LeafLat(Leaf) + 1 );
+ return Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums );
+ }
+ assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
+ Leaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pObj), Ivy_LeafLat(Leaf) );
+ uTruth0 = Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums );
+ if ( Ivy_ObjFaninC0(pObj) )
+ uTruth0 = ~uTruth0;
+ if ( Ivy_ObjIsBuf(pObj) )
+ return uTruth0;
+ Leaf = Ivy_LeafCreate( Ivy_ObjFaninId1(pObj), Ivy_LeafLat(Leaf) );
+ uTruth1 = Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums );
+ if ( Ivy_ObjFaninC1(pObj) )
+ uTruth1 = ~uTruth1;
+ return uTruth0 & uTruth1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes the truth table.]
+ Description []
+
+ SideEffects []
+ SeeAlso []
+
+***********************************************************************/
+unsigned Ivy_CutGetTruth( Ivy_Man_t * p, Ivy_Obj_t * pObj, int * pNums, int nNums )
+{
+ assert( Ivy_ObjIsNode(pObj) );
+ assert( nNums < 6 );
+ return Ivy_CutGetTruth_rec( p, Ivy_LeafCreate(pObj->Id, 0), pNums, nNums );
+}
@@ -50,6 +592,28 @@ static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); }
/**Function*************************************************************
+ Synopsis [Returns 1 if the cut can be constructed; 0 otherwise.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Ivy_CutPrescreen( Ivy_Cut_t * pCut, int Id0, int Id1 )
+{
+ int i;
+ if ( pCut->nSize < pCut->nSizeMax )
+ return 1;
+ for ( i = 0; i < pCut->nSize; i++ )
+ if ( pCut->pArray[i] == Id0 || pCut->pArray[i] == Id1 )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
Synopsis [Derives new cut.]
Description []
@@ -59,7 +623,7 @@ static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); }
SeeAlso []
***********************************************************************/
-static inline int Ivy_CutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
+static inline int Ivy_CutDeriveNew2( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
{
unsigned uHash = 0;
int i, k;
@@ -126,6 +690,130 @@ static inline int Ivy_CutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int I
/**Function*************************************************************
+ Synopsis [Derives new cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Ivy_CutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
+{
+ unsigned uHash = 0;
+ int i, k;
+ assert( pCut->nSize > 0 );
+ assert( IdNew0 < IdNew1 );
+ for ( i = k = 0; i < pCut->nSize; i++ )
+ {
+ if ( pCut->pArray[i] == IdOld )
+ continue;
+ if ( IdNew0 <= pCut->pArray[i] )
+ {
+ if ( IdNew0 < pCut->pArray[i] )
+ {
+ pCutNew->pArray[ k++ ] = IdNew0;
+ uHash |= Ivy_CutHashValue( IdNew0 );
+ }
+ IdNew0 = 0x7FFFFFFF;
+ }
+ if ( IdNew1 <= pCut->pArray[i] )
+ {
+ if ( IdNew1 < pCut->pArray[i] )
+ {
+ pCutNew->pArray[ k++ ] = IdNew1;
+ uHash |= Ivy_CutHashValue( IdNew1 );
+ }
+ IdNew1 = 0x7FFFFFFF;
+ }
+ pCutNew->pArray[ k++ ] = pCut->pArray[i];
+ uHash |= Ivy_CutHashValue( pCut->pArray[i] );
+ }
+ if ( IdNew0 < 0x7FFFFFFF )
+ {
+ pCutNew->pArray[ k++ ] = IdNew0;
+ uHash |= Ivy_CutHashValue( IdNew0 );
+ }
+ if ( IdNew1 < 0x7FFFFFFF )
+ {
+ pCutNew->pArray[ k++ ] = IdNew1;
+ uHash |= Ivy_CutHashValue( IdNew1 );
+ }
+ pCutNew->nSize = k;
+ pCutNew->uHash = uHash;
+ assert( pCutNew->nSize <= pCut->nSizeMax );
+// for ( i = 1; i < pCutNew->nSize; i++ )
+// assert( pCutNew->pArray[i-1] < pCutNew->pArray[i] );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find the hash value of the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Ivy_NodeCutHash( Ivy_Cut_t * pCut )
+{
+ int i;
+ pCut->uHash = 0;
+ for ( i = 0; i < pCut->nSize; i++ )
+ pCut->uHash |= (1 << (pCut->pArray[i] % 31));
+ return pCut->uHash;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives new cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Ivy_CutDeriveNew3( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
+{
+ int i, k;
+ assert( pCut->nSize > 0 );
+ assert( IdNew0 < IdNew1 );
+ for ( i = k = 0; i < pCut->nSize; i++ )
+ {
+ if ( pCut->pArray[i] == IdOld )
+ continue;
+ if ( IdNew0 <= pCut->pArray[i] )
+ {
+ if ( IdNew0 < pCut->pArray[i] )
+ pCutNew->pArray[ k++ ] = IdNew0;
+ IdNew0 = 0x7FFFFFFF;
+ }
+ if ( IdNew1 <= pCut->pArray[i] )
+ {
+ if ( IdNew1 < pCut->pArray[i] )
+ pCutNew->pArray[ k++ ] = IdNew1;
+ IdNew1 = 0x7FFFFFFF;
+ }
+ pCutNew->pArray[ k++ ] = pCut->pArray[i];
+ }
+ if ( IdNew0 < 0x7FFFFFFF )
+ pCutNew->pArray[ k++ ] = IdNew0;
+ if ( IdNew1 < 0x7FFFFFFF )
+ pCutNew->pArray[ k++ ] = IdNew1;
+ pCutNew->nSize = k;
+ assert( pCutNew->nSize <= pCut->nSizeMax );
+ Ivy_NodeCutHash( pCutNew );
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if pDom is contained in pCut.]
Description []
@@ -295,9 +983,12 @@ void Ivy_CutPrintForNodes( Ivy_Store_t * pCutStore )
***********************************************************************/
static inline int Ivy_CutReadLeaf( Ivy_Obj_t * pFanin )
{
+ int iLeaf;
assert( !Ivy_IsComplement(pFanin) );
if ( !Ivy_ObjIsLatch(pFanin) )
return Ivy_LeafCreate( pFanin->Id, 0 );
+ iLeaf = Ivy_CutReadLeaf( Ivy_ObjFanin0(pFanin) );
+ assert( Ivy_LeafLat(iLeaf) < IVY_LEAF_MASK );
return 1 + Ivy_CutReadLeaf( Ivy_ObjFanin0(pFanin) );
}
@@ -345,13 +1036,20 @@ Ivy_Store_t * Ivy_CutComputeForNode( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeave
for ( k = 0; k < pCut->nSize; k++ )
{
pLeaf = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[k]) );
- if ( Ivy_ObjIsCi(pLeaf) )
+ if ( Ivy_ObjIsCi(pLeaf) || Ivy_ObjIsConst1(pLeaf) )
continue;
assert( Ivy_ObjIsNode(pLeaf) );
nLats = Ivy_LeafLat(pCut->pArray[k]);
+
// get the fanins fanins
- iLeaf0 = nLats + Ivy_CutReadLeaf( Ivy_ObjFanin0(pLeaf) );
- iLeaf1 = nLats + Ivy_CutReadLeaf( Ivy_ObjFanin1(pLeaf) );
+ iLeaf0 = Ivy_CutReadLeaf( Ivy_ObjFanin0(pLeaf) );
+ iLeaf1 = Ivy_CutReadLeaf( Ivy_ObjFanin1(pLeaf) );
+ assert( nLats + Ivy_LeafLat(iLeaf0) < IVY_LEAF_MASK && nLats + Ivy_LeafLat(iLeaf1) < IVY_LEAF_MASK );
+ iLeaf0 = nLats + iLeaf0;
+ iLeaf1 = nLats + iLeaf1;
+ if ( !Ivy_CutPrescreen( pCut, iLeaf0, iLeaf1 ) )
+ continue;
+ // the given cut exist
if ( iLeaf0 > iLeaf1 )
Temp = iLeaf0, iLeaf0 = iLeaf1, iLeaf1 = Temp;
// create the new cut
diff --git a/src/temp/ivy/ivyTable.c b/src/temp/ivy/ivyTable.c
index f2617699..fe9c3570 100644
--- a/src/temp/ivy/ivyTable.c
+++ b/src/temp/ivy/ivyTable.c
@@ -74,8 +74,8 @@ Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj )
return NULL;
assert( Ivy_ObjIsLatch(pObj) || Ivy_ObjFaninId0(pObj) > 0 );
assert( Ivy_ObjFaninId1(pObj) == 0 || Ivy_ObjFaninId0(pObj) < Ivy_ObjFaninId1(pObj) );
-// if ( Ivy_ObjFanin0(pObj)->nRefs == 0 || (!Ivy_ObjIsLatch(pObj) && Ivy_ObjFanin1(pObj)->nRefs == 0) )
-// return NULL;
+ if ( Ivy_ObjFanin0(pObj)->nRefs == 0 || (Ivy_ObjChild1(pObj) && Ivy_ObjFanin1(pObj)->nRefs == 0) )
+ return NULL;
for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
{
pEntry = Ivy_ManObj( p, p->pTable[i] );
diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c
index 3b77bf41..77a55a39 100644
--- a/src/temp/ivy/ivyUtil.c
+++ b/src/temp/ivy/ivyUtil.c
@@ -265,7 +265,7 @@ int Ivy_ManLevels( Ivy_Man_t * p )
***********************************************************************/
int Ivy_ManResetLevels_rec( Ivy_Obj_t * pObj )
{
- if ( pObj->Level || Ivy_ObjIsCi(pObj) )
+ if ( pObj->Level || Ivy_ObjIsCi(pObj) || Ivy_ObjIsConst1(pObj) )
return pObj->Level;
if ( Ivy_ObjIsBuf(pObj) )
return pObj->Level = Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
@@ -292,12 +292,81 @@ void Ivy_ManResetLevels( Ivy_Man_t * p )
int i;
Ivy_ManForEachObj( p, pObj, i )
pObj->Level = 0;
- Ivy_ManForEachPo( p, pObj, i )
+ Ivy_ManForEachCo( p, pObj, i )
Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
}
/**Function*************************************************************
+ Synopsis [References/references the node and returns MFFC size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ObjRefDeref( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fReference, int fLabel )
+{
+ Ivy_Obj_t * pNode0, * pNode1;
+ int Counter;
+ // label visited nodes
+ if ( fLabel )
+ Ivy_ObjSetTravIdCurrent( p, pNode );
+ // skip the CI
+ if ( Ivy_ObjIsPi(pNode) )
+ return 0;
+ assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) || Ivy_ObjIsLatch(pNode) );
+ // process the internal node
+ pNode0 = Ivy_ObjFanin0(pNode);
+ pNode1 = Ivy_ObjFanin1(pNode);
+ Counter = Ivy_ObjIsNode(pNode);
+ if ( fReference )
+ {
+ if ( pNode0->nRefs++ == 0 )
+ Counter += Ivy_ObjRefDeref( p, pNode0, fReference, fLabel );
+ if ( pNode1 && pNode1->nRefs++ == 0 )
+ Counter += Ivy_ObjRefDeref( p, pNode1, fReference, fLabel );
+ }
+ else
+ {
+ assert( pNode0->nRefs > 0 );
+ assert( pNode1 == NULL || pNode1->nRefs > 0 );
+ if ( --pNode0->nRefs == 0 )
+ Counter += Ivy_ObjRefDeref( p, pNode0, fReference, fLabel );
+ if ( pNode1 && --pNode1->nRefs == 0 )
+ Counter += Ivy_ObjRefDeref( p, pNode1, fReference, fLabel );
+ }
+ return Counter;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Labels MFFC with the current label.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pNode )
+{
+ int nConeSize1, nConeSize2;
+ assert( !Ivy_IsComplement( pNode ) );
+ assert( Ivy_ObjIsNode( pNode ) );
+ nConeSize1 = Ivy_ObjRefDeref( p, pNode, 0, 1 ); // dereference
+ nConeSize2 = Ivy_ObjRefDeref( p, pNode, 1, 0 ); // reference
+ assert( nConeSize1 == nConeSize2 );
+ assert( nConeSize1 > 0 );
+ return nConeSize1;
+}
+
+/**Function*************************************************************
+
Synopsis [Recursively updates fanout levels.]
Description []
diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make
index a8f6a824..e7ba865a 100644
--- a/src/temp/ivy/module.make
+++ b/src/temp/ivy/module.make
@@ -5,6 +5,7 @@ SRC += src/temp/ivy/ivyBalance.c \
src/temp/ivy/ivyDfs.c \
src/temp/ivy/ivyDsd.c \
src/temp/ivy/ivyFanout.c \
+ src/temp/ivy/ivyIsop.c \
src/temp/ivy/ivyMan.c \
src/temp/ivy/ivyMem.c \
src/temp/ivy/ivyMulti.c \