summaryrefslogtreecommitdiffstats
path: root/src/temp/ivy
diff options
context:
space:
mode:
Diffstat (limited to 'src/temp/ivy')
-rw-r--r--src/temp/ivy/ivy.h12
-rw-r--r--src/temp/ivy/ivyCheck.c51
-rw-r--r--src/temp/ivy/ivyDfs.c231
-rw-r--r--src/temp/ivy/ivyHaig.c248
-rw-r--r--src/temp/ivy/ivyMan.c7
-rw-r--r--src/temp/ivy/ivyObj.c27
-rw-r--r--src/temp/ivy/ivyRwr.c (renamed from src/temp/ivy/ivyRwrPre.c)4
-rw-r--r--src/temp/ivy/ivySeq.c42
-rw-r--r--src/temp/ivy/ivyShow.c326
-rw-r--r--src/temp/ivy/ivyTable.c7
-rw-r--r--src/temp/ivy/ivyUtil.c92
-rw-r--r--src/temp/ivy/module.make2
12 files changed, 938 insertions, 111 deletions
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index 2409284e..a3cb714e 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -114,6 +114,7 @@ struct Ivy_Man_t_
void * pData; // the temporary data
void * pCopy; // the temporary data
Ivy_Man_t * pHaig; // history AIG if present
+ int nClassesSkip; // the number of skipped classes
// memory management
Vec_Ptr_t * vChunks; // allocated memory pieces
Vec_Ptr_t * vPages; // memory pages used by nodes
@@ -395,7 +396,9 @@ extern Ivy_Obj_t * Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t *
extern Ivy_Obj_t * Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init );
/*=== ivyCheck.c ========================================================*/
extern int Ivy_ManCheck( Ivy_Man_t * p );
+extern int Ivy_ManCheckFanoutNums( Ivy_Man_t * p );
extern int Ivy_ManCheckFanouts( Ivy_Man_t * p );
+extern int Ivy_ManCheckChoices( Ivy_Man_t * p );
/*=== ivyCut.c ==========================================================*/
extern void Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize );
extern Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves );
@@ -406,6 +409,7 @@ extern void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront,
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 );
+extern int Ivy_ManSetLevels( Ivy_Man_t * p, int fHaig );
/*=== ivyDsd.c ==========================================================*/
extern int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree );
extern void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree );
@@ -422,10 +426,10 @@ extern void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, V
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 );
/*=== ivyHaig.c ==========================================================*/
-extern void Ivy_ManHaigStart( Ivy_Man_t * p );
+extern void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose );
extern void Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew );
extern void Ivy_ManHaigStop( Ivy_Man_t * p );
-extern void Ivy_ManHaigPrintStats( Ivy_Man_t * p );
+extern void Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose );
extern void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew );
extern void Ivy_ManHaigSimulate( Ivy_Man_t * p );
@@ -477,6 +481,8 @@ extern int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int f
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 );
+/*=== ivyShow.c =========================================================*/
+extern void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig );
/*=== 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 );
@@ -497,6 +503,8 @@ extern void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj,
extern int Ivy_ObjIsMuxType( Ivy_Obj_t * pObj );
extern Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObjT, Ivy_Obj_t ** ppObjE );
extern Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj );
+extern void Ivy_ObjPrintVerbose( Ivy_Obj_t * pObj, int fHaig );
+extern void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig );
#ifdef __cplusplus
}
diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c
index ebae64ff..55448f19 100644
--- a/src/temp/ivy/ivyCheck.c
+++ b/src/temp/ivy/ivyCheck.c
@@ -142,6 +142,29 @@ int Ivy_ManCheck( Ivy_Man_t * p )
SeeAlso []
***********************************************************************/
+int Ivy_ManCheckFanoutNums( Ivy_Man_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i, Counter = 0;
+ Ivy_ManForEachObj( p, pObj, i )
+ if ( Ivy_ObjIsNode(pObj) )
+ Counter += (Ivy_ObjRefs(pObj) == 0);
+ if ( Counter )
+ printf( "Sequential AIG has %d dangling nodes.\n", Counter );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Verifies the fanouts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Ivy_ManCheckFanouts( Ivy_Man_t * p )
{
Vec_Ptr_t * vFanouts;
@@ -215,6 +238,34 @@ int Ivy_ManCheckFanouts( Ivy_Man_t * p )
return RetValue;
}
+/**Function*************************************************************
+
+ Synopsis [Checks that each choice node has exactly one node with fanouts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManCheckChoices( Ivy_Man_t * p )
+{
+ Ivy_Obj_t * pObj, * pTemp;
+ int i;
+ Ivy_ManForEachObj( p->pHaig, pObj, i )
+ {
+ if ( Ivy_ObjRefs(pObj) == 0 )
+ continue;
+ // count the number of nodes in the loop
+ assert( !Ivy_IsComplement(pObj->pEquiv) );
+ for ( pTemp = pObj->pEquiv; pTemp && pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+ if ( Ivy_ObjRefs(pTemp) > 1 )
+ printf( "Node %d has member %d in its equiv class with %d fanouts.\n", pObj->Id, pTemp->Id, Ivy_ObjRefs(pTemp) );
+ }
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c
index 314bed8d..c27cba31 100644
--- a/src/temp/ivy/ivyDfs.c
+++ b/src/temp/ivy/ivyDfs.c
@@ -39,18 +39,35 @@
SeeAlso []
***********************************************************************/
-void Ivy_ManDfs_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
+void Ivy_ManDfs_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
{
- if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
- return;
if ( Ivy_ObjIsMarkA(pObj) )
return;
Ivy_ObjSetMarkA(pObj);
+ if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
+ {
+ if ( p->pHaig == NULL && pObj->pEquiv )
+ Ivy_ManDfs_rec( p, Ivy_Regular(pObj->pEquiv), vNodes );
+ return;
+ }
+//printf( "visiting node %d\n", pObj->Id );
+/*
+ if ( pObj->Id == 87 || pObj->Id == 90 )
+ {
+ int y = 0;
+ }
+*/
assert( Ivy_ObjIsBuf(pObj) || Ivy_ObjIsAnd(pObj) || Ivy_ObjIsExor(pObj) );
- Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+ Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
if ( !Ivy_ObjIsBuf(pObj) )
- Ivy_ManDfs_rec( Ivy_ObjFanin1(pObj), vNodes );
+ Ivy_ManDfs_rec( p, Ivy_ObjFanin1(pObj), vNodes );
+ if ( p->pHaig == NULL && pObj->pEquiv )
+ Ivy_ManDfs_rec( p, Ivy_Regular(pObj->pEquiv), vNodes );
Vec_IntPush( vNodes, pObj->Id );
+
+//printf( "adding node %d with fanins %d and %d and equiv %d (refs = %d)\n",
+// pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id,
+// pObj->pEquiv? Ivy_Regular(pObj->pEquiv)->Id: -1, Ivy_ObjRefs(pObj) );
}
/**Function*************************************************************
@@ -76,9 +93,11 @@ Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p )
// collect the nodes
vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
Ivy_ManForEachPo( p, pObj, i )
- Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+ Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
// unmark the collected nodes
- Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+// Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+// Ivy_ObjClearMarkA(pObj);
+ Ivy_ManForEachObj( p, pObj, i )
Ivy_ObjClearMarkA(pObj);
// make sure network does not have dangling nodes
assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
@@ -101,7 +120,7 @@ Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches )
Vec_Int_t * vNodes, * vLatches;
Ivy_Obj_t * pObj;
int i;
- assert( Ivy_ManLatchNum(p) > 0 );
+// assert( Ivy_ManLatchNum(p) > 0 );
// make sure the nodes are not marked
Ivy_ManForEachObj( p, pObj, i )
assert( !pObj->fMarkA && !pObj->fMarkB );
@@ -112,15 +131,23 @@ Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches )
// collect the nodes
vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
Ivy_ManForEachPo( p, pObj, i )
- Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+ Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
- Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+ Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
// unmark the collected nodes
- Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+// Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+// Ivy_ObjClearMarkA(pObj);
+ Ivy_ManForEachObj( p, pObj, i )
Ivy_ObjClearMarkA(pObj);
// make sure network does not have dangling nodes
// assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
- *pvLatches = vLatches;
+
+// temporary!!!
+
+ if ( pvLatches == NULL )
+ Vec_IntFree( vLatches );
+ else
+ *pvLatches = vLatches;
return vNodes;
}
@@ -261,47 +288,64 @@ Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p )
SeeAlso []
***********************************************************************/
-int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode )
+int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj )
{
- if ( Ivy_ObjIsCi(pNode) || Ivy_ObjIsConst1(pNode) )
+ // skip the node if it is already visited
+ if ( Ivy_ObjIsTravIdPrevious(p, pObj) )
return 1;
- assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(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) )
+ if ( Ivy_ObjIsTravIdCurrent(p, pObj) )
{
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) );
+ fprintf( stdout, "Node \"%d\" is encountered twice on the following path:\n", Ivy_ObjId(pObj) );
+ fprintf( stdout, " %d", Ivy_ObjId(pObj) );
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)) )
+ Ivy_ObjSetTravIdCurrent( p, pObj );
+ // explore equivalent nodes if pObj is the main node
+ if ( p->pHaig == NULL && pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
{
- // traverse the fanin's cone searching for the loop
- if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pNode)) )
+ Ivy_Obj_t * pTemp;
+ assert( !Ivy_IsComplement(pObj->pEquiv) );
+ for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
{
- // return as soon as the loop is detected
- fprintf( stdout, " <-- %d", Ivy_ObjId(Ivy_ObjFanin0(pNode)) );
- return 0;
+ // traverse the fanin's cone searching for the loop
+ if ( !Ivy_ManIsAcyclic_rec(p, pTemp) )
+ {
+ // return as soon as the loop is detected
+ fprintf( stdout, " -> (%d", Ivy_ObjId(pObj) );
+ for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+ fprintf( stdout, " %d", Ivy_ObjId(pTemp) );
+ fprintf( stdout, ")" );
+ return 0;
+ }
}
}
- // check if the fanin is visited
- if ( Ivy_ObjIsNode(pNode) && !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin1(pNode)) )
+ // quite if it is a CI node
+ if ( Ivy_ObjIsCi(pObj) || Ivy_ObjIsConst1(pObj) )
{
- // 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, pObj );
+ return 1;
+ }
+ assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
+ // traverse the fanin's cone searching for the loop
+ if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pObj)) )
+ {
+ // return as soon as the loop is detected
+ fprintf( stdout, " -> %d", Ivy_ObjId(pObj) );
+ return 0;
+ }
+ // traverse the fanin's cone searching for the loop
+ if ( Ivy_ObjIsNode(pObj) && !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin1(pObj)) )
+ {
+ // return as soon as the loop is detected
+ fprintf( stdout, " -> %d", Ivy_ObjId(pObj) );
+ return 0;
}
// mark this node as a visited node
- Ivy_ObjSetTravIdPrevious( p, pNode );
+ Ivy_ObjSetTravIdPrevious( p, pObj );
return 1;
}
@@ -325,30 +369,123 @@ int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode )
***********************************************************************/
int Ivy_ManIsAcyclic( Ivy_Man_t * p )
{
- Ivy_Obj_t * pNode;
+ Ivy_Obj_t * pObj;
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"
+ // pObj->TravId == pNet->nTravIds means "pObj is on the path"
+ // pObj->TravId == pNet->nTravIds - 1 means "pObj is visited but is not on the path"
+ // pObj->TravId < pNet->nTravIds - 1 means "pObj is not visited"
// traverse the network to detect cycles
fAcyclic = 1;
- Ivy_ManForEachCo( p, pNode, i )
+ Ivy_ManForEachCo( p, pObj, i )
{
- if ( Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin0(pNode)) )
- continue;
// traverse the output logic cone
- if ( fAcyclic = Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pNode)) )
+ if ( fAcyclic = Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pObj)) )
continue;
// stop as soon as the first loop is detected
- fprintf( stdout, " (cone of CO \"%d\")\n", Ivy_ObjFaninId0(pNode) );
+ fprintf( stdout, " (cone of %s \"%d\")\n", Ivy_ObjIsLatch(pObj)? "latch" : "PO", Ivy_ObjId(pObj) );
break;
}
return fAcyclic;
}
+/**Function*************************************************************
+
+ Synopsis [Sets the levels of the nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManSetLevels_rec( Ivy_Obj_t * pObj, int fHaig )
+{
+ // quit if the node is visited
+ if ( Ivy_ObjIsMarkA(pObj) )
+ return pObj->Level;
+ Ivy_ObjSetMarkA(pObj);
+ // quit if this is a CI
+ if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
+ return 0;
+ assert( Ivy_ObjIsBuf(pObj) || Ivy_ObjIsAnd(pObj) || Ivy_ObjIsExor(pObj) );
+ // get levels of the fanins
+ Ivy_ManSetLevels_rec( Ivy_ObjFanin0(pObj), fHaig );
+ if ( !Ivy_ObjIsBuf(pObj) )
+ Ivy_ManSetLevels_rec( Ivy_ObjFanin1(pObj), fHaig );
+ // get level of the node
+ if ( Ivy_ObjIsBuf(pObj) )
+ pObj->Level = 1 + Ivy_ObjFanin0(pObj)->Level;
+ else if ( Ivy_ObjIsNode(pObj) )
+ pObj->Level = Ivy_ObjLevelNew( pObj );
+ else assert( 0 );
+ // get level of other choices
+ if ( fHaig && pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
+ {
+ Ivy_Obj_t * pTemp;
+ unsigned LevelMax = pObj->Level;
+ for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+ {
+ Ivy_ManSetLevels_rec( pTemp, fHaig );
+ LevelMax = IVY_MAX( LevelMax, pTemp->Level );
+ }
+ // get this level
+ pObj->Level = LevelMax;
+ for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+ pTemp->Level = LevelMax;
+ }
+ return pObj->Level;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets the levels of the nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManSetLevels( Ivy_Man_t * p, int fHaig )
+{
+ Ivy_Obj_t * pObj;
+ int i, LevelMax;
+ // check if CIs have choices
+ if ( fHaig )
+ {
+ Ivy_ManForEachCi( p, pObj, i )
+ if ( pObj->pEquiv )
+ printf( "CI %d has a choice, which will not be visualized.\n", pObj->Id );
+ }
+ // clean the levels
+ Ivy_ManForEachObj( p, pObj, i )
+ pObj->Level = 0;
+ // compute the levels
+ LevelMax = 0;
+ Ivy_ManForEachCo( p, pObj, i )
+ {
+ Ivy_ManSetLevels_rec( Ivy_ObjFanin0(pObj), fHaig );
+ LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level );
+ }
+ // compute levels of nodes without fanout
+ Ivy_ManForEachObj( p, pObj, i )
+ if ( (Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj)) && Ivy_ObjRefs(pObj) == 0 )
+ {
+ Ivy_ManSetLevels_rec( pObj, fHaig );
+ LevelMax = IVY_MAX( LevelMax, (int)pObj->Level );
+ }
+ // clean the marks
+ Ivy_ManForEachObj( p, pObj, i )
+ Ivy_ObjClearMarkA(pObj);
+ return LevelMax;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyHaig.c b/src/temp/ivy/ivyHaig.c
index 7ce71a60..ca68c3c6 100644
--- a/src/temp/ivy/ivyHaig.c
+++ b/src/temp/ivy/ivyHaig.c
@@ -26,16 +26,17 @@
/*
HAIGing rules in working AIG:
- - The node points to the representative of its class
- - The pointer can be complemented if they have different polarity
+ - Each node in the working AIG has a pointer to the corresponding node in HAIG
+ (this node is not necessarily the representative of the equivalence class of HAIG nodes)
+ - This pointer is complemented if the AIG node and its corresponding HAIG node have different phase
Choice node rules in HAIG:
- Equivalent nodes are linked into a ring
- - Exactly one node in the ring has fanouts (this node is called representative)
- - Pointer going from a node to the next node in the ring is complemented
- if the first node is complemented, compared to the representative node
- - The representative node always has non-complemented pointer to the next node
- - New nodes are inserted into the ring before the representative node
+ - Exactly one node in the ring has fanouts (this node is called the representative)
+ - The pointer going from a node to the next node in the ring is complemented
+ if the first node is complemented, compared to the representative node of the equivalence class
+ - (consequence of the above) The representative node always has non-complemented pointer to the next node
+ - New nodes are inserted into the ring immediately after the representative node
*/
// returns the representative node of the given HAIG node
@@ -52,7 +53,7 @@ static inline Ivy_Obj_t * Ivy_HaigObjRepr( Ivy_Obj_t * pObj )
if ( Ivy_ObjRefs(pTemp) > 0 )
break;
// return the representative node
- assert( pTemp != pObj );
+ assert( Ivy_ObjRefs(pTemp) > 0 );
return Ivy_NotCond( pTemp, Ivy_IsComplement(pObj->pEquiv) );
}
@@ -65,8 +66,8 @@ static inline int Ivy_HaigObjCountClass( Ivy_Obj_t * pObj )
assert( Ivy_ObjRefs(pObj) > 0 );
if ( pObj->pEquiv == NULL )
return 1;
- Counter = 1;
assert( !Ivy_IsComplement(pObj->pEquiv) );
+ Counter = 1;
for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
Counter++;
return Counter;
@@ -87,10 +88,28 @@ static inline int Ivy_HaigObjCountClass( Ivy_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Ivy_ManHaigStart( Ivy_Man_t * p )
+void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose )
{
+ Vec_Int_t * vLatches;
+ Ivy_Obj_t * pObj;
+ int i;
assert( p->pHaig == NULL );
p->pHaig = Ivy_ManDup( p );
+
+ if ( fVerbose )
+ {
+ printf( "Starting : " );
+ Ivy_ManPrintStats( p->pHaig );
+ }
+
+ // collect latches of design D and set their values to be DC
+ vLatches = Vec_IntAlloc( 100 );
+ Ivy_ManForEachLatch( p->pHaig, pObj, i )
+ {
+ pObj->Init = IVY_INIT_DC;
+ Vec_IntPush( vLatches, pObj->Id );
+ }
+ p->pHaig->pData = vLatches;
}
/**Function*************************************************************
@@ -131,6 +150,7 @@ void Ivy_ManHaigStop( Ivy_Man_t * p )
Ivy_Obj_t * pObj;
int i;
assert( p->pHaig != NULL );
+ Vec_IntFree( p->pHaig->pData );
Ivy_ManStop( p->pHaig );
p->pHaig = NULL;
// remove dangling pointers to the HAIG objects
@@ -151,17 +171,54 @@ void Ivy_ManHaigStop( Ivy_Man_t * p )
***********************************************************************/
void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj )
{
+ Ivy_Obj_t * pEquiv0, * pEquiv1;
assert( p->pHaig != NULL );
assert( !Ivy_IsComplement(pObj) );
if ( Ivy_ObjType(pObj) == IVY_BUF )
pObj->pEquiv = Ivy_ObjChild0Equiv(pObj);
else if ( Ivy_ObjType(pObj) == IVY_LATCH )
- pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init );
+ {
+// pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init );
+ pEquiv0 = Ivy_ObjChild0Equiv(pObj);
+ pEquiv0 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv0)), Ivy_IsComplement(pEquiv0) );
+ pObj->pEquiv = Ivy_Latch( p->pHaig, pEquiv0, pObj->Init );
+ }
else if ( Ivy_ObjType(pObj) == IVY_AND )
- pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+ {
+// pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+ pEquiv0 = Ivy_ObjChild0Equiv(pObj);
+ pEquiv0 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv0)), Ivy_IsComplement(pEquiv0) );
+ pEquiv1 = Ivy_ObjChild1Equiv(pObj);
+ pEquiv1 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv1)), Ivy_IsComplement(pEquiv1) );
+ pObj->pEquiv = Ivy_And( p->pHaig, pEquiv0, pEquiv1 );
+ }
else assert( 0 );
// make sure the node points to the representative
- pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) );
+// pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the old node is in the TFI of the new node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ObjIsInTfi_rec( Ivy_Obj_t * pObjNew, Ivy_Obj_t * pObjOld, int Levels )
+{
+ if ( pObjNew == pObjOld )
+ return 1;
+ if ( Levels == 0 || Ivy_ObjIsCi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
+ return 0;
+ if ( Ivy_ObjIsInTfi_rec( Ivy_ObjFanin0(pObjNew), pObjOld, Levels - 1 ) )
+ return 1;
+ if ( Ivy_ObjIsNode(pObjNew) && Ivy_ObjIsInTfi_rec( Ivy_ObjFanin1(pObjNew), pObjOld, Levels - 1 ) )
+ return 1;
+ return 0;
}
/**Function*************************************************************
@@ -180,10 +237,16 @@ void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pO
Ivy_Obj_t * pObjOldHaig, * pObjNewHaig;
Ivy_Obj_t * pObjOldHaigR, * pObjNewHaigR;
int fCompl;
+//printf( "\nCreating choice for %d and %d in AIG\n", pObjOld->Id, Ivy_Regular(pObjNew)->Id );
+
assert( p->pHaig != NULL );
- // get pointers to the classes
+ assert( !Ivy_IsComplement(pObjOld) );
+ // get pointers to the representatives of pObjOld and pObjNew
pObjOldHaig = pObjOld->pEquiv;
pObjNewHaig = Ivy_NotCond( Ivy_Regular(pObjNew)->pEquiv, Ivy_IsComplement(pObjNew) );
+ // get the classes
+ pObjOldHaig = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObjOldHaig)), Ivy_IsComplement(pObjOldHaig) );
+ pObjNewHaig = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObjNewHaig)), Ivy_IsComplement(pObjNewHaig) );
// get regular pointers
pObjOldHaigR = Ivy_Regular(pObjOldHaig);
pObjNewHaigR = Ivy_Regular(pObjNewHaig);
@@ -192,17 +255,41 @@ void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pO
// if the class is the same, nothing to do
if ( pObjOldHaigR == pObjNewHaigR )
return;
- // combine classes
- // assume the second node does not belong to a class
- assert( pObjNewHaigR->pEquiv == NULL );
+ // if the second node belongs to a class, do not merge classes (for the time being)
+ if ( Ivy_ObjRefs(pObjOldHaigR) == 0 || pObjNewHaigR->pEquiv != NULL ||
+ Ivy_ObjRefs(pObjNewHaigR) > 0 || Ivy_ObjIsInTfi_rec(pObjNewHaigR, pObjOldHaigR, 10) )
+ {
+/*
+ if ( pObjNewHaigR->pEquiv != NULL )
+ printf( "c" );
+ if ( Ivy_ObjRefs(pObjNewHaigR) > 0 )
+ printf( "f" );
+ printf( " " );
+*/
+ p->pHaig->nClassesSkip++;
+ return;
+ }
+
// add this node to the class of pObjOldHaig
+ assert( Ivy_ObjRefs(pObjOldHaigR) > 0 );
+ assert( !Ivy_IsComplement(pObjOldHaigR->pEquiv) );
if ( pObjOldHaigR->pEquiv == NULL )
pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl );
else
pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR->pEquiv, fCompl );
pObjOldHaigR->pEquiv = pObjNewHaigR;
+//printf( "Setting choice node %d -> %d.\n", pObjOldHaigR->Id, pObjNewHaigR->Id );
// update the class of the new node
- Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) );
+// Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) );
+//printf( "Creating choice for %d and %d in HAIG\n", pObjOldHaigR->Id, pObjNewHaigR->Id );
+
+// if ( pObjOldHaigR->Id == 13 )
+// {
+// Ivy_ManShow( p, 0 );
+// Ivy_ManShow( p->pHaig, 1 );
+// }
+// if ( !Ivy_ManIsAcyclic( p->pHaig ) )
+// printf( "HAIG contains a cycle\n" );
}
/**Function*************************************************************
@@ -227,17 +314,16 @@ int Ivy_ManHaigCountChoices( Ivy_Man_t * p, int * pnChoices )
if ( Ivy_ObjIsTerm(pObj) || i == 0 )
continue;
if ( Ivy_ObjRefs(pObj) == 0 )
- {
- assert( pObj->pEquiv == Ivy_HaigObjRepr(pObj) );
continue;
- }
Counter = Ivy_HaigObjCountClass( pObj );
nChoiceNodes += (int)(Counter > 1);
nChoices += Counter - 1;
+// if ( Counter > 1 )
+// printf( "Choice node %d %s\n", pObj->Id, Ivy_ObjIsLatch(pObj)? "(latch)": "" );
}
*pnChoices = nChoices;
return nChoiceNodes;
-}
+}
/**Function*************************************************************
@@ -250,19 +336,35 @@ int Ivy_ManHaigCountChoices( Ivy_Man_t * p, int * pnChoices )
SeeAlso []
***********************************************************************/
-void Ivy_ManHaigPrintStats( Ivy_Man_t * p )
+void Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose )
{
int nChoices, nChoiceNodes;
+
assert( p->pHaig != NULL );
- printf( "Original : " );
- Ivy_ManPrintStats( p );
- printf( "HAIG : " );
- Ivy_ManPrintStats( p->pHaig );
-
- // print choice node stats
- nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices );
- printf( "Total choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
- Ivy_ManHaigSimulate( p );
+
+ if ( fVerbose )
+ {
+ printf( "Final : " );
+ Ivy_ManPrintStats( p );
+ printf( "HAIG : " );
+ Ivy_ManPrintStats( p->pHaig );
+
+ // print choice node stats
+ nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices );
+ printf( "Total choice nodes = %d. Total choices = %d. Skipped classes = %d.\n",
+ nChoiceNodes, nChoices, p->pHaig->nClassesSkip );
+ }
+
+ if ( Ivy_ManIsAcyclic( p->pHaig ) )
+ {
+ if ( fVerbose )
+ printf( "HAIG is acyclic\n" );
+ }
+ else
+ printf( "HAIG contains a cycle\n" );
+
+ if ( fVerbose )
+ Ivy_ManHaigSimulate( p );
}
@@ -289,6 +391,32 @@ static inline Ivy_Init_t Ivy_ManHaigSimulateAnd( Ivy_Init_t In0, Ivy_Init_t In1
/**Function*************************************************************
+ Synopsis [Applies the simulation rules.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Ivy_Init_t Ivy_ManHaigSimulateChoice( Ivy_Init_t In0, Ivy_Init_t In1 )
+{
+ assert( In0 != IVY_INIT_NONE && In1 != IVY_INIT_NONE );
+ if ( (In0 == IVY_INIT_0 && In1 == IVY_INIT_1) || (In0 == IVY_INIT_1 && In1 == IVY_INIT_0) )
+ {
+ printf( "Compatibility fails.\n" );
+ return IVY_INIT_0;
+ }
+ if ( In0 == IVY_INIT_DC && In1 == IVY_INIT_DC )
+ return IVY_INIT_DC;
+ if ( In0 != IVY_INIT_DC )
+ return In0;
+ return In1;
+}
+
+/**Function*************************************************************
+
Synopsis [Simulate HAIG using modified 3-valued simulation.]
Description []
@@ -300,39 +428,85 @@ static inline Ivy_Init_t Ivy_ManHaigSimulateAnd( Ivy_Init_t In0, Ivy_Init_t In1
***********************************************************************/
void Ivy_ManHaigSimulate( Ivy_Man_t * p )
{
- Vec_Int_t * vNodes, * vLatches;
- Ivy_Obj_t * pObj;
+ Vec_Int_t * vNodes, * vLatches, * vLatchesD;
+ Ivy_Obj_t * pObj, * pTemp;
Ivy_Init_t In0, In1;
int i, k, Counter;
+ int fVerbose = 0;
+
+ // check choices
+ Ivy_ManCheckChoices( p );
+
+ // switch to HAIG
assert( p->pHaig != NULL );
p = p->pHaig;
+
+if ( fVerbose )
+Ivy_ManForEachPi( p, pObj, i )
+printf( "Setting PI %d\n", pObj->Id );
+
// collect latches and nodes in the DFS order
vNodes = Ivy_ManDfsSeq( p, &vLatches );
+
+if ( fVerbose )
+Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+printf( "Collected node %d with fanins %d and %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id );
+
// set the PI values
- Ivy_ManConst1(p)->Init = IVY_INIT_0;
+ Ivy_ManConst1(p)->Init = IVY_INIT_1;
Ivy_ManForEachPi( p, pObj, i )
pObj->Init = IVY_INIT_0;
+
// set the latch values
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
pObj->Init = IVY_INIT_DC;
+ // set the latches of D to be determinate
+ vLatchesD = p->pData;
+ Ivy_ManForEachNodeVec( p, vLatchesD, pObj, i )
+ pObj->Init = IVY_INIT_0;
+
// perform several rounds of simulation
- for ( k = 0; k < 5; k++ )
+ for ( k = 0; k < 10; k++ )
{
// count the number of non-determinate values
Counter = 0;
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
Counter += ( pObj->Init == IVY_INIT_DC );
- printf( "Iter %d : Non-determinate = %d\n", k, Counter );
+ printf( "Iter %d : Non-determinate = %d\n", k, Counter );
+
// simulate the internal nodes
Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
{
+if ( fVerbose )
+printf( "Processing node %d with fanins %d and %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id );
In0 = Ivy_InitNotCond( Ivy_ObjFanin0(pObj)->Init, Ivy_ObjFaninC0(pObj) );
In1 = Ivy_InitNotCond( Ivy_ObjFanin1(pObj)->Init, Ivy_ObjFaninC1(pObj) );
pObj->Init = Ivy_ManHaigSimulateAnd( In0, In1 );
+ // simulate the equivalence class if the node is a representative
+ if ( pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
+ {
+if ( fVerbose )
+printf( "Processing choice node %d\n", pObj->Id );
+ In0 = pObj->Init;
+ assert( !Ivy_IsComplement(pObj->pEquiv) );
+ for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+ {
+if ( fVerbose )
+printf( "Processing secondary node %d\n", pTemp->Id );
+ In1 = Ivy_InitNotCond( pTemp->Init, Ivy_IsComplement(pTemp->pEquiv) );
+ In0 = Ivy_ManHaigSimulateChoice( In0, In1 );
+ }
+ pObj->Init = In0;
+ }
}
+
// simulate the latches
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+ {
pObj->Level = Ivy_ObjFanin0(pObj)->Init;
+if ( fVerbose )
+printf( "Using latch %d with fanin %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id );
+ }
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
pObj->Init = pObj->Level, pObj->Level = 0;
}
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index e3b8a5b8..786949e7 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -58,7 +58,7 @@ Ivy_Man_t * Ivy_ManStart()
Ivy_ManStartMemory( p );
// create the constant node
p->pConst1 = Ivy_ManFetchMemory( p );
- p->pConst1->fPhase = 1;
+// p->pConst1->fPhase = 1;
Vec_PtrPush( p->vObjs, p->pConst1 );
p->nCreated = 1;
// start the table
@@ -118,6 +118,9 @@ Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
// free arrays
Vec_IntFree( vNodes );
Vec_IntFree( vLatches );
+ // make sure structural hashing did not change anything
+ assert( Ivy_ManNodeNum(p) == Ivy_ManNodeNum(pNew) );
+ assert( Ivy_ManLatchNum(p) == Ivy_ManLatchNum(pNew) );
// check the resulting network
if ( !Ivy_ManCheck(pNew) )
printf( "Ivy_ManMakeSeq(): The check has failed.\n" );
@@ -182,7 +185,7 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
SideEffects []
- SeeAlso []
+ SeeAlso []
***********************************************************************/
int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index e8924b5b..36af3920 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -114,6 +114,11 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
// update node counters of the manager
p->nObjs[Ivy_ObjType(pObj)]++;
p->nCreated++;
+
+// printf( "Adding %sAIG node: ", p->pHaig==NULL? "H":" " );
+// Ivy_ObjPrintVerbose( pObj, p->pHaig==NULL );
+// printf( "\n" );
+
// if HAIG is defined, create a corresponding node
if ( p->pHaig )
Ivy_ManHaigCreateObj( p, pObj );
@@ -192,8 +197,6 @@ void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj )
// add the first fanin
pObj->pFanin0 = NULL;
pObj->pFanin1 = NULL;
-
-// Ivy_ManCheckFanouts( p );
}
/**Function*************************************************************
@@ -324,7 +327,14 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
assert( pObjOld != Ivy_Regular(pObjNew) );
// if HAIG is defined, create the choice node
if ( p->pHaig )
+ {
+// if ( pObjOld->Id == 31 )
+// {
+// Ivy_ManShow( p, 0 );
+// Ivy_ManShow( p->pHaig, 1 );
+// }
Ivy_ManHaigCreateChoice( p, pObjOld, pObjNew );
+ }
// if the new object is complemented or already used, add the buffer
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) );
@@ -388,6 +398,19 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
Vec_PtrPush( p->vBufs, pObjOld );
// Ivy_ManCheckFanouts( p );
// printf( "\n" );
+/*
+ if ( p->pHaig )
+ {
+ int x;
+ Ivy_ManShow( p, 0 );
+ Ivy_ManShow( p->pHaig, 1 );
+ x = 0;
+ }
+*/
+// if ( Ivy_ManCheckFanoutNums(p) )
+// {
+// int x = 0;
+// }
}
/**Function*************************************************************
diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwr.c
index 64331579..3f8720ba 100644
--- a/src/temp/ivy/ivyRwrPre.c
+++ b/src/temp/ivy/ivyRwr.c
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [ivyRwtPre.c]
+ FileName [ivyRwt.c]
SystemName [ABC: Logic synthesis and verification system.]
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - May 11, 2006.]
- Revision [$Id: ivyRwtPre.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+ Revision [$Id: ivyRwt.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c
index 11660e42..44a35d33 100644
--- a/src/temp/ivy/ivySeq.c
+++ b/src/temp/ivy/ivySeq.c
@@ -58,6 +58,9 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
Ivy_Obj_t * pNode;
int i, nNodes, nGain;
int clk, clkStart = clock();
+ // set the DC latch values
+ Ivy_ManForEachLatch( p, pNode, i )
+ pNode->Init = IVY_INIT_DC;
// start the rewriting manager
pManRwt = Rwt_ManStart( 0 );
p->pData = pManRwt;
@@ -92,12 +95,6 @@ clk = clock();
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 );
@@ -109,6 +106,8 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
p->pData = NULL;
// fix the levels
Ivy_ManResetLevels( p );
+// if ( Ivy_ManCheckFanoutNums(p) )
+// printf( "Ivy_ManRewritePre(): The check has failed.\n" );
// check
if ( !Ivy_ManCheck(p) )
printf( "Ivy_ManRewritePre(): The check has failed.\n" );
@@ -139,7 +138,8 @@ int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int
Dec_Graph_t * pGraph;
Ivy_Store_t * pStore;
Ivy_Cut_t * pCut;
- Ivy_Obj_t * pFanin;
+ Ivy_Obj_t * pFanin;//, * pFanout;
+ Vec_Ptr_t * vFanout;
unsigned uPhase, uTruthBest, uTruth;
char * pPerm;
int nNodesSaved, nNodesSaveCur;
@@ -154,6 +154,7 @@ p->timeCut += clock() - clk;
// go through the cuts
clk = clock();
+ vFanout = Vec_PtrAlloc( 100 );
for ( c = 1; c < pStore->nCuts; c++ )
{
pCut = pStore->pCuts + c;
@@ -193,6 +194,9 @@ clk2 = clock();
// label MFFC with current ID
Ivy_ManIncrementTravId( pMan );
nNodesSaved = Ivy_ObjMffcLabel( pMan, pNode );
+ // label fanouts with the current ID
+// Ivy_ObjForEachFanout( pMan, pNode, vFanout, pFanout, i )
+// Ivy_ObjSetTravIdCurrent( pMan, pFanout );
// unmark the fanin boundary
Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
@@ -233,11 +237,19 @@ p->timeEval += clock() - clk2;
Vec_PtrPush( p->vFanins, pFanin );
}
}
+ Vec_PtrFree( vFanout );
p->timeRes += clock() - clk;
if ( GainBest == -1 )
return -1;
+/*
+ printf( "Node %5d. Using cut : {", Ivy_ObjId(pNode) );
+ for ( i = 0; i < pCut->nSize; i++ )
+ printf( " %d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
+ printf( " }\n" );
+*/
+
// copy the leaves
Ivy_GraphPrepare( p->pGraph, p->pCut, p->vFanins, p->pPerm );
@@ -250,10 +262,9 @@ p->timeRes += clock() - clk;
if ( GainBest > 0 )
{
Ivy_Cut_t * pCut = p->pCut;
- printf( "Useful cut : {" );
+ printf( "Node %5d. Using cut : {", Ivy_ObjId(pNode) );
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( " %5d(%2d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
printf( " }\n" );
}
*/
@@ -974,18 +985,19 @@ void Ivy_CutPrintForNodes( Ivy_Store_t * pCutStore )
SideEffects []
- SeeAlso []
+ SeeAlso []
***********************************************************************/
static inline int Ivy_CutReadLeaf( Ivy_Obj_t * pFanin )
{
- int iLeaf;
+ int nLats, 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) );
+ iLeaf = Ivy_CutReadLeaf(Ivy_ObjFanin0(pFanin));
+ nLats = Ivy_LeafLat(iLeaf);
+ assert( nLats < IVY_LEAF_MASK );
+ return 1 + iLeaf;
}
/**Function*************************************************************
diff --git a/src/temp/ivy/ivyShow.c b/src/temp/ivy/ivyShow.c
new file mode 100644
index 00000000..3105081e
--- /dev/null
+++ b/src/temp/ivy/ivyShow.c
@@ -0,0 +1,326 @@
+/**CFile****************************************************************
+
+ FileName [ivyShow.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis [Visualization of HAIG.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - May 11, 2006.]
+
+ Revision [$Id: ivyShow.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig )
+{
+ extern void Abc_ShowFile( char * FileNameDot );
+ static Counter = 0;
+ char FileNameDot[200];
+ FILE * pFile;
+ // create the file name
+// Ivy_ShowGetFileName( pMan->pName, FileNameDot );
+ sprintf( FileNameDot, "temp%02d.dot", Counter++ );
+ // check that the file can be opened
+ if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+ {
+ fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+ return;
+ }
+ fclose( pFile );
+ // generate the file
+ Ivy_WriteDotAig( pMan, FileNameDot, fHaig );
+ // visualize the file
+ Abc_ShowFile( FileNameDot );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the graph structure of AIG for DOT.]
+
+ Description [Useful for graph visualization using tools such as GraphViz:
+ http://www.graphviz.org/]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig )
+{
+ FILE * pFile;
+ Ivy_Obj_t * pNode, * pTemp, * pPrev;
+ int LevelMax, Level, i;
+
+ if ( Ivy_ManNodeNum(pMan) > 200 )
+ {
+ fprintf( stdout, "Cannot visualize AIG with more than 200 nodes.\n" );
+ return;
+ }
+ if ( (pFile = fopen( pFileName, "w" )) == NULL )
+ {
+ fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
+ return;
+ }
+
+ // compute levels
+ LevelMax = 1 + Ivy_ManSetLevels( pMan, fHaig );
+
+ // write the DOT header
+ fprintf( pFile, "# %s\n", "AIG structure generated by IVY package" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "digraph AIG {\n" );
+ fprintf( pFile, "size = \"7.5,10\";\n" );
+// fprintf( pFile, "ranksep = 0.5;\n" );
+// fprintf( pFile, "nodesep = 0.5;\n" );
+ fprintf( pFile, "center = true;\n" );
+// fprintf( pFile, "orientation = landscape;\n" );
+// fprintf( pFile, "edge [fontsize = 10];\n" );
+// fprintf( pFile, "edge [dir = none];\n" );
+ fprintf( pFile, "edge [dir = back];\n" );
+ fprintf( pFile, "\n" );
+
+ // labels on the left of the picture
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " node [shape = plaintext];\n" );
+ fprintf( pFile, " edge [style = invis];\n" );
+ fprintf( pFile, " LevelTitle1 [label=\"\"];\n" );
+ fprintf( pFile, " LevelTitle2 [label=\"\"];\n" );
+ // generate node names with labels
+ for ( Level = LevelMax; Level >= 0; Level-- )
+ {
+ // the visible node name
+ fprintf( pFile, " Level%d", Level );
+ fprintf( pFile, " [label = " );
+ // label name
+ fprintf( pFile, "\"" );
+ fprintf( pFile, "\"" );
+ fprintf( pFile, "];\n" );
+ }
+
+ // genetate the sequence of visible/invisible nodes to mark levels
+ fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" );
+ for ( Level = LevelMax; Level >= 0; Level-- )
+ {
+ // the visible node name
+ fprintf( pFile, " Level%d", Level );
+ // the connector
+ if ( Level != 0 )
+ fprintf( pFile, " ->" );
+ else
+ fprintf( pFile, ";" );
+ }
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate title box on top
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ fprintf( pFile, " LevelTitle1;\n" );
+ fprintf( pFile, " title1 [shape=plaintext,\n" );
+ fprintf( pFile, " fontsize=20,\n" );
+ fprintf( pFile, " fontname = \"Times-Roman\",\n" );
+ fprintf( pFile, " label=\"" );
+ fprintf( pFile, "%s", "AIG structure visualized by ABC" );
+ fprintf( pFile, "\\n" );
+ fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" );
+ fprintf( pFile, "Time was %s. ", Extra_TimeStamp() );
+ fprintf( pFile, "\"\n" );
+ fprintf( pFile, " ];\n" );
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate statistics box
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ fprintf( pFile, " LevelTitle2;\n" );
+ fprintf( pFile, " title2 [shape=plaintext,\n" );
+ fprintf( pFile, " fontsize=18,\n" );
+ fprintf( pFile, " fontname = \"Times-Roman\",\n" );
+ fprintf( pFile, " label=\"" );
+ fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Ivy_ManNodeNum(pMan), LevelMax );
+ fprintf( pFile, "\\n" );
+ fprintf( pFile, "\"\n" );
+ fprintf( pFile, " ];\n" );
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate the COs
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ // the labeling node of this level
+ fprintf( pFile, " Level%d;\n", LevelMax );
+ // generate the CO nodes
+ Ivy_ManForEachCo( pMan, pNode, i )
+ {
+ if ( fHaig || pNode->pEquiv == NULL )
+ fprintf( pFile, " Node%d%s [label = \"%d%s\"", pNode->Id,
+ (Ivy_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") );
+ else
+ fprintf( pFile, " Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id,
+ (Ivy_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":""),
+ Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
+ fprintf( pFile, ", shape = %s", (Ivy_ObjIsLatch(pNode)? "box":"invtriangle") );
+ fprintf( pFile, ", color = coral, fillcolor = coral" );
+ fprintf( pFile, "];\n" );
+ }
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate nodes of each rank
+ for ( Level = LevelMax - 1; Level > 0; Level-- )
+ {
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ // the labeling node of this level
+ fprintf( pFile, " Level%d;\n", Level );
+ Ivy_ManForEachObj( pMan, pNode, i )
+ {
+ if ( (int)pNode->Level != Level )
+ continue;
+ if ( fHaig || pNode->pEquiv == NULL )
+ fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
+ else
+ fprintf( pFile, " Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id,
+ Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
+ fprintf( pFile, ", shape = ellipse" );
+ fprintf( pFile, "];\n" );
+ }
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+ }
+
+ // generate the CI nodes
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ // the labeling node of this level
+ fprintf( pFile, " Level%d;\n", 0 );
+ // generate constant node
+ if ( Ivy_ObjRefs(Ivy_ManConst1(pMan)) > 0 )
+ {
+ pNode = Ivy_ManConst1(pMan);
+ // check if the costant node is present
+ fprintf( pFile, " Node%d [label = \"Const1\"", pNode->Id );
+ fprintf( pFile, ", shape = ellipse" );
+ fprintf( pFile, ", color = coral, fillcolor = coral" );
+ fprintf( pFile, "];\n" );
+ }
+ // generate the CI nodes
+ Ivy_ManForEachCi( pMan, pNode, i )
+ {
+ if ( fHaig || pNode->pEquiv == NULL )
+ fprintf( pFile, " Node%d%s [label = \"%d%s\"", pNode->Id,
+ (Ivy_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_out":"") );
+ else
+ fprintf( pFile, " Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id,
+ (Ivy_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_out":""),
+ Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
+ fprintf( pFile, ", shape = %s", (Ivy_ObjIsLatch(pNode)? "box":"triangle") );
+ fprintf( pFile, ", color = coral, fillcolor = coral" );
+ fprintf( pFile, "];\n" );
+ }
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate invisible edges from the square down
+ fprintf( pFile, "title1 -> title2 [style = invis];\n" );
+ Ivy_ManForEachCo( pMan, pNode, i )
+ fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") );
+
+ // generate edges
+ Ivy_ManForEachObj( pMan, pNode, i )
+ {
+ if ( !Ivy_ObjIsNode(pNode) && !Ivy_ObjIsCo(pNode) && !Ivy_ObjIsBuf(pNode) )
+ continue;
+ // generate the edge from this node to the next
+ fprintf( pFile, "Node%d%s", pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") );
+ fprintf( pFile, " -> " );
+ fprintf( pFile, "Node%d%s", Ivy_ObjFaninId0(pNode), (Ivy_ObjIsLatch(Ivy_ObjFanin0(pNode))? "_out":"") );
+ fprintf( pFile, " [" );
+ fprintf( pFile, "style = %s", Ivy_ObjFaninC0(pNode)? "dotted" : "bold" );
+// if ( Ivy_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 )
+// fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) );
+ fprintf( pFile, "]" );
+ fprintf( pFile, ";\n" );
+ if ( !Ivy_ObjIsNode(pNode) )
+ continue;
+ // generate the edge from this node to the next
+ fprintf( pFile, "Node%d", pNode->Id );
+ fprintf( pFile, " -> " );
+ fprintf( pFile, "Node%d%s", Ivy_ObjFaninId1(pNode), (Ivy_ObjIsLatch(Ivy_ObjFanin1(pNode))? "_out":"") );
+ fprintf( pFile, " [" );
+ fprintf( pFile, "style = %s", Ivy_ObjFaninC1(pNode)? "dotted" : "bold" );
+// if ( Ivy_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 )
+// fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
+ fprintf( pFile, "]" );
+ fprintf( pFile, ";\n" );
+ // generate the edges between the equivalent nodes
+ if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 )
+ {
+ pPrev = pNode;
+ for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) )
+ {
+ fprintf( pFile, "Node%d", pPrev->Id );
+ fprintf( pFile, " -> " );
+ fprintf( pFile, "Node%d", pTemp->Id );
+ fprintf( pFile, " [style = %s]", Ivy_IsComplement(pTemp->pEquiv)? "dotted" : "bold" );
+ fprintf( pFile, ";\n" );
+ pPrev = pTemp;
+ }
+ // connect the last node with the first
+ fprintf( pFile, "Node%d", pPrev->Id );
+ fprintf( pFile, " -> " );
+ fprintf( pFile, "Node%d", pNode->Id );
+ fprintf( pFile, " [style = %s]", Ivy_IsComplement(pPrev->pEquiv)? "dotted" : "bold" );
+ fprintf( pFile, ";\n" );
+ }
+ }
+
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyTable.c b/src/temp/ivy/ivyTable.c
index fe9c3570..2ac0ae49 100644
--- a/src/temp/ivy/ivyTable.c
+++ b/src/temp/ivy/ivyTable.c
@@ -167,7 +167,7 @@ void Ivy_TableUpdate( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ObjIdNew )
return;
pPlace = Ivy_TableFind( p, pObj );
assert( *pPlace == pObj->Id ); // node should be in the table
- *pPlace = ObjIdNew;
+ *pPlace = ObjIdNew;
}
/**Function*************************************************************
@@ -203,7 +203,7 @@ int Ivy_TableCountEntries( Ivy_Man_t * p )
void Ivy_TableResize( Ivy_Man_t * p )
{
int * pTableOld, * pPlace;
- int nTableSizeOld, Counter, e, clk;
+ int nTableSizeOld, Counter, nEntries, e, clk;
clk = clock();
// save the old table
pTableOld = p->pTable;
@@ -224,7 +224,8 @@ clk = clock();
assert( *pPlace == 0 ); // should not be in the table
*pPlace = pTableOld[e];
}
- assert( Counter == Ivy_ManHashObjNum(p) );
+ nEntries = Ivy_ManHashObjNum(p);
+// assert( Counter == nEntries );
// printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
// PRT( "Time", clock() - clk );
// replace the table and the parameters
diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c
index a23e76c9..3c53bd21 100644
--- a/src/temp/ivy/ivyUtil.c
+++ b/src/temp/ivy/ivyUtil.c
@@ -612,6 +612,98 @@ Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) );
}
+/**Function*************************************************************
+
+ Synopsis [Prints node in HAIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_ObjPrintVerbose( Ivy_Obj_t * pObj, int fHaig )
+{
+ Ivy_Obj_t * pTemp;
+ assert( !Ivy_IsComplement(pObj) );
+ printf( "Node %5d : ", Ivy_ObjId(pObj) );
+ if ( Ivy_ObjIsConst1(pObj) )
+ printf( "constant 1" );
+ else if ( Ivy_ObjIsPi(pObj) )
+ printf( "PI" );
+ else if ( Ivy_ObjIsPo(pObj) )
+ printf( "PO" );
+ else if ( Ivy_ObjIsLatch(pObj) )
+ printf( "latch %d%s", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
+ else if ( Ivy_ObjIsBuf(pObj) )
+ printf( "buffer %d%s", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
+ else
+ printf( "AND( %5d%s, %5d%s )",
+ Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " "),
+ Ivy_ObjFanin1(pObj)->Id, (Ivy_ObjFaninC1(pObj)? "\'" : " ") );
+ printf( " (refs = %3d)", Ivy_ObjRefs(pObj) );
+ if ( !fHaig )
+ {
+ if ( pObj->pEquiv == NULL )
+ printf( " HAIG node not given" );
+ else
+ printf( " HAIG node = %d%s", Ivy_Regular(pObj->pEquiv)->Id, (Ivy_IsComplement(pObj->pEquiv)? "\'" : " ") );
+ return;
+ }
+ if ( pObj->pEquiv == NULL )
+ return;
+ // there are choices
+ if ( Ivy_ObjRefs(pObj) > 0 )
+ {
+ // print equivalence class
+ printf( " { %5d ", pObj->Id );
+ assert( !Ivy_IsComplement(pObj->pEquiv) );
+ for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+ printf( " %5d%s", pTemp->Id, (Ivy_IsComplement(pTemp->pEquiv)? "\'" : " ") );
+ printf( " }" );
+ return;
+ }
+ // this is a secondary node
+ for ( pTemp = Ivy_Regular(pObj->pEquiv); Ivy_ObjRefs(pTemp) == 0; pTemp = Ivy_Regular(pTemp->pEquiv) );
+ assert( Ivy_ObjRefs(pTemp) > 0 );
+ printf( " class of %d", pTemp->Id );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints node in HAIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig )
+{
+ Vec_Int_t * vNodes;
+ Ivy_Obj_t * pObj;
+ int i;
+ printf( "PIs: " );
+ Ivy_ManForEachPi( p, pObj, i )
+ printf( " %d", pObj->Id );
+ printf( "\n" );
+ printf( "POs: " );
+ Ivy_ManForEachPo( p, pObj, i )
+ printf( " %d", pObj->Id );
+ printf( "\n" );
+ printf( "Latches: " );
+ Ivy_ManForEachLatch( p, pObj, i )
+ printf( " %d=%d%s", pObj->Id, Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
+ printf( "\n" );
+ vNodes = Ivy_ManDfsSeq( p, NULL );
+ Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+ Ivy_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
+ printf( "\n" );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make
index e7ba865a..c208c8ee 100644
--- a/src/temp/ivy/module.make
+++ b/src/temp/ivy/module.make
@@ -12,7 +12,7 @@ SRC += src/temp/ivy/ivyBalance.c \
src/temp/ivy/ivyObj.c \
src/temp/ivy/ivyOper.c \
src/temp/ivy/ivyResyn.c \
- src/temp/ivy/ivyRwrPre.c \
+ src/temp/ivy/ivyRwr.c \
src/temp/ivy/ivySeq.c \
src/temp/ivy/ivyTable.c \
src/temp/ivy/ivyUtil.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 13:04:32 +0000