summaryrefslogtreecommitdiffstats
path: root/src/temp/ivy
diff options
context:
space:
mode:
Diffstat (limited to 'src/temp/ivy')
-rw-r--r--src/temp/ivy/ivy.h11
-rw-r--r--src/temp/ivy/ivyFraig.c5
-rw-r--r--src/temp/ivy/ivyHaig.c16
-rw-r--r--src/temp/ivy/ivyMan.c129
-rw-r--r--src/temp/ivy/ivyObj.c15
-rw-r--r--src/temp/ivy/ivySeq.c4
-rw-r--r--src/temp/ivy/ivyUtil.c35
7 files changed, 189 insertions, 26 deletions
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index e7c9bc2e..eb5f50e4 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -183,10 +183,10 @@ static inline int Ivy_InfoHasBit( unsigned * p, int i ) { return (p[(i
static inline void Ivy_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Ivy_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
-static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) & ~01); }
-static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) ^ 01); }
-static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((unsigned)(p) ^ (c)); }
-static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int )(((unsigned)p) & 01); }
+static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned long)(p) & ~01); }
+static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned long)(p) ^ 01); }
+static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((unsigned long)(p) ^ (c)); }
+static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int )(((unsigned long)p) & 01); }
static inline Ivy_Obj_t * Ivy_ManConst0( Ivy_Man_t * p ) { return Ivy_Not(p->pConst1); }
static inline Ivy_Obj_t * Ivy_ManConst1( Ivy_Man_t * p ) { return p->pConst1; }
@@ -471,6 +471,7 @@ extern int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t *
extern Ivy_Man_t * Ivy_ManStart();
extern Ivy_Man_t * Ivy_ManStartFrom( Ivy_Man_t * p );
extern Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p );
+extern Ivy_Man_t * Ivy_ManFrames( Ivy_Man_t * pMan, int nLatches, int nFrames, int fInit, Vec_Ptr_t ** pvMapping );
extern void Ivy_ManStop( Ivy_Man_t * p );
extern int Ivy_ManCleanup( Ivy_Man_t * p );
extern int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel );
@@ -538,7 +539,7 @@ 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_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig );
extern void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig );
#ifdef __cplusplus
diff --git a/src/temp/ivy/ivyFraig.c b/src/temp/ivy/ivyFraig.c
index 9c729b23..694d5a30 100644
--- a/src/temp/ivy/ivyFraig.c
+++ b/src/temp/ivy/ivyFraig.c
@@ -1807,7 +1807,7 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
***********************************************************************/
void Ivy_FraigSweep( Ivy_FraigMan_t * p )
{
- Ivy_Obj_t * pObj;
+ Ivy_Obj_t * pObj;//, * pTemp;
int i, k = 0;
p->nClassesZero = p->lClasses.pHead? (Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0) : 0;
p->nClassesBeg = p->lClasses.nItems;
@@ -1817,6 +1817,9 @@ p->nClassesBeg = p->lClasses.nItems;
{
Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
pObj->pEquiv = Ivy_FraigAnd( p, pObj );
+ assert( pObj->pEquiv != NULL );
+// pTemp = Ivy_Regular(pObj->pEquiv);
+// assert( Ivy_Regular(pObj->pEquiv)->Type );
}
Extra_ProgressBarStop( p->pProgress );
p->nClassesEnd = p->lClasses.nItems;
diff --git a/src/temp/ivy/ivyHaig.c b/src/temp/ivy/ivyHaig.c
index ca68c3c6..87021600 100644
--- a/src/temp/ivy/ivyHaig.c
+++ b/src/temp/ivy/ivyHaig.c
@@ -44,7 +44,7 @@ static inline Ivy_Obj_t * Ivy_HaigObjRepr( Ivy_Obj_t * pObj )
{
Ivy_Obj_t * pTemp;
assert( !Ivy_IsComplement(pObj) );
- // if the node has no equivalent or has fanout, it is representative
+ // if the node has no equivalent node or has fanout, it is representative
if ( pObj->pEquiv == NULL || Ivy_ObjRefs(pObj) > 0 )
return pObj;
// the node belongs to a class and is not a representative
@@ -110,6 +110,14 @@ void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose )
Vec_IntPush( vLatches, pObj->Id );
}
p->pHaig->pData = vLatches;
+/*
+ {
+ int x;
+ Ivy_ManShow( p, 0, NULL );
+ Ivy_ManShow( p->pHaig, 1, NULL );
+ x = 0;
+ }
+*/
}
/**Function*************************************************************
@@ -257,7 +265,7 @@ void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pO
return;
// 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) )
+ Ivy_ObjRefs(pObjNewHaigR) > 0 ) //|| Ivy_ObjIsInTfi_rec(pObjNewHaigR, pObjOldHaigR, 10) )
{
/*
if ( pObjNewHaigR->pEquiv != NULL )
@@ -363,8 +371,8 @@ void Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose )
else
printf( "HAIG contains a cycle\n" );
- if ( fVerbose )
- Ivy_ManHaigSimulate( p );
+// if ( fVerbose )
+// Ivy_ManHaigSimulate( p );
}
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index e2689580..8099b834 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -46,9 +46,9 @@ Ivy_Man_t * Ivy_ManStart()
p = ALLOC( Ivy_Man_t, 1 );
memset( p, 0, sizeof(Ivy_Man_t) );
// perform initializations
- p->Ghost.Id = -1;
- p->nTravIds = 1;
- p->fCatchExor = 1;
+ p->Ghost.Id = -1;
+ p->nTravIds = 1;
+ p->fCatchExor = 1;
// allocate arrays for nodes
p->vPis = Vec_PtrAlloc( 100 );
p->vPos = Vec_PtrAlloc( 100 );
@@ -166,6 +166,72 @@ Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
SeeAlso []
***********************************************************************/
+Ivy_Man_t * Ivy_ManFrames( Ivy_Man_t * pMan, int nLatches, int nFrames, int fInit, Vec_Ptr_t ** pvMapping )
+{
+ Vec_Ptr_t * vMapping;
+ Ivy_Man_t * pNew;
+ Ivy_Obj_t * pObj;
+ int i, f, nPis, nPos, nIdMax;
+ assert( Ivy_ManLatchNum(pMan) == 0 );
+ assert( nFrames > 0 );
+ // prepare the mapping
+ nPis = Ivy_ManPiNum(pMan) - nLatches;
+ nPos = Ivy_ManPoNum(pMan) - nLatches;
+ nIdMax = Ivy_ManObjIdMax(pMan);
+ // create the new manager
+ pNew = Ivy_ManStart();
+ // set the starting values of latch inputs
+ for ( i = 0; i < nLatches; i++ )
+ Ivy_ManPo(pMan, nPos+i)->pEquiv = fInit? Ivy_Not(Ivy_ManConst1(pNew)) : Ivy_ObjCreatePi(pNew);
+ // add timeframes
+ vMapping = Vec_PtrStart( nIdMax * nFrames + 1 );
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // create PIs
+ Ivy_ManConst1(pMan)->pEquiv = Ivy_ManConst1(pNew);
+ for ( i = 0; i < nPis; i++ )
+ Ivy_ManPi(pMan, i)->pEquiv = Ivy_ObjCreatePi(pNew);
+ // transfer values to latch outputs
+ for ( i = 0; i < nLatches; i++ )
+ Ivy_ManPi(pMan, nPis+i)->pEquiv = Ivy_ManPo(pMan, nPos+i)->pEquiv;
+ // perform strashing
+ Ivy_ManForEachNode( pMan, pObj, i )
+ pObj->pEquiv = Ivy_And( pNew, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+ // create POs
+ for ( i = 0; i < nPos; i++ )
+ Ivy_ManPo(pMan, i)->pEquiv = Ivy_ObjCreatePo( pNew, Ivy_ObjChild0Equiv(Ivy_ManPo(pMan, i)) );
+ // set the results of latch inputs
+ for ( i = 0; i < nLatches; i++ )
+ Ivy_ManPo(pMan, nPos+i)->pEquiv = Ivy_ObjChild0Equiv(Ivy_ManPo(pMan, nPos+i));
+ // save the pointers in this frame
+ Ivy_ManForEachObj( pMan, pObj, i )
+ Vec_PtrWriteEntry( vMapping, f * nIdMax + i, pObj->pEquiv );
+ }
+ // connect latches
+ if ( !fInit )
+ for ( i = 0; i < nLatches; i++ )
+ Ivy_ObjCreatePo( pNew, Ivy_ManPo(pMan, nPos+i)->pEquiv );
+ // remove dangling nodes
+ Ivy_ManCleanup(pNew);
+ *pvMapping = vMapping;
+ // check the resulting network
+ if ( !Ivy_ManCheck(pNew) )
+ printf( "Ivy_ManFrames(): The check has failed.\n" );
+ return pNew;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Stops the AIG manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Ivy_ManStop( Ivy_Man_t * p )
{
if ( p->time1 ) { PRT( "Update lev ", p->time1 ); }
@@ -291,6 +357,46 @@ int Ivy_ManCleanupSeq( Ivy_Man_t * p )
return RetValue;
}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if latches form self-loop.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManLatchIsSelfFeed_rec( Ivy_Obj_t * pLatch, Ivy_Obj_t * pLatchRoot )
+{
+ if ( !Ivy_ObjIsLatch(pLatch) && !Ivy_ObjIsBuf(pLatch) )
+ return 0;
+ if ( pLatch == pLatchRoot )
+ return 1;
+ return Ivy_ManLatchIsSelfFeed_rec( Ivy_ObjFanin0(pLatch), pLatchRoot );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if latches form self-loop.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManLatchIsSelfFeed( Ivy_Obj_t * pLatch )
+{
+ if ( !Ivy_ObjIsLatch(pLatch) )
+ return 0;
+ return Ivy_ManLatchIsSelfFeed_rec( Ivy_ObjFanin0(pLatch), pLatch );
+}
+
+
/**Function*************************************************************
Synopsis [Returns the number of dangling nodes removed.]
@@ -305,23 +411,30 @@ int Ivy_ManCleanupSeq( Ivy_Man_t * p )
int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
{
Ivy_Obj_t * pNode;
- int LimitFactor = 20;
+ int LimitFactor = 100;
+ int NodeBeg = Ivy_ManNodeNum(p);
int nSteps;
for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
{
pNode = Vec_PtrEntryLast(p->vBufs);
while ( Ivy_ObjIsBuf(pNode) )
pNode = Ivy_ObjReadFirstFanout( p, pNode );
+ // check if this buffer should remain
+ if ( Ivy_ManLatchIsSelfFeed(pNode) )
+ {
+ Vec_PtrPop(p->vBufs);
+ continue;
+ }
//printf( "Propagating buffer %d with input %d and output %d\n", Ivy_ObjFaninId0(pNode), Ivy_ObjFaninId0(Ivy_ObjFanin0(pNode)), pNode->Id );
//printf( "Latch num %d\n", Ivy_ManLatchNum(p) );
Ivy_NodeFixBufferFanins( p, pNode, fUpdateLevel );
- if ( nSteps > Ivy_ManNodeNum(p) * LimitFactor )
+ if ( nSteps > NodeBeg * LimitFactor )
{
- printf( "This circuit cannot be forward retimed completely. Structural hashing is not finished after %d forward latch moves.\n", Ivy_ManNodeNum(p) * LimitFactor );
+ printf( "This circuit cannot be forward retimed completely. Structural hashing is not finished after %d forward latch moves.\n", NodeBeg * LimitFactor );
break;
}
}
-// printf( "Number of steps = %d\n", nSteps );
+ printf( "Number of steps = %d. Nodes beg = %d. Nodes end = %d.\n", nSteps, NodeBeg, Ivy_ManNodeNum(p) );
return nSteps;
}
@@ -416,6 +529,8 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits )
*/
// perform hashing by propagating the buffers
Ivy_ManPropagateBuffers( p, 0 );
+ if ( Ivy_ManBufNum(p) )
+ printf( "The number of remaining buffers is %d.\n", Ivy_ManBufNum(p) );
// fix the levels
Ivy_ManResetLevels( p );
// check the resulting network
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index d9887c5b..59dda19c 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -124,7 +124,7 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
p->nCreated++;
// printf( "Adding %sAIG node: ", p->pHaig==NULL? "H":" " );
-// Ivy_ObjPrintVerbose( pObj, p->pHaig==NULL );
+// Ivy_ObjPrintVerbose( p, pObj, p->pHaig==NULL );
// printf( "\n" );
// if HAIG is defined, create a corresponding node
@@ -234,7 +234,7 @@ void Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew
if ( p->fFanout )
Ivy_ObjAddFanout( p, Ivy_Regular(pFaninNew), pObj );
// get rid of old fanin
- if ( !Ivy_ObjIsPi(pFaninOld) && Ivy_ObjRefs(pFaninOld) == 0 )
+ if ( !Ivy_ObjIsPi(pFaninOld) && !Ivy_ObjIsConst1(pFaninOld) && Ivy_ObjRefs(pFaninOld) == 0 )
Ivy_ObjDelete_rec( p, pFaninOld, 1 );
}
@@ -333,6 +333,8 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
assert( !Ivy_ObjIsBuf(Ivy_Regular(pObjNew)) );
// the object cannot be the same
assert( pObjOld != Ivy_Regular(pObjNew) );
+//printf( "Replacing %d by %d.\n", Ivy_Regular(pObjOld)->Id, Ivy_Regular(pObjNew)->Id );
+
// if HAIG is defined, create the choice node
if ( p->pHaig )
{
@@ -410,8 +412,8 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
if ( p->pHaig )
{
int x;
- Ivy_ManShow( p, 0 );
- Ivy_ManShow( p->pHaig, 1 );
+ Ivy_ManShow( p, 0, NULL );
+ Ivy_ManShow( p->pHaig, 1, NULL );
x = 0;
}
*/
@@ -458,6 +460,11 @@ void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel
pResult = Ivy_Latch( p, pFanReal0, Ivy_ObjInit(pNode) );
else
assert( 0 );
+
+//printf( "===== Replacing %d by %d.\n", pNode->Id, pResult->Id );
+//Ivy_ObjPrintVerbose( p, pNode, 0 ); printf( "\n" );
+//Ivy_ObjPrintVerbose( p, pResult, 0 ); printf( "\n" );
+
// perform the replacement
Ivy_ObjReplace( p, pNode, pResult, 1, 0, fUpdateLevel );
}
diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c
index 44a35d33..c1f3da2b 100644
--- a/src/temp/ivy/ivySeq.c
+++ b/src/temp/ivy/ivySeq.c
@@ -242,12 +242,14 @@ p->timeRes += clock() - clk;
if ( GainBest == -1 )
return -1;
-
/*
+ {
+ Ivy_Cut_t * pCut = p->pCut;
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
diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c
index 3c53bd21..0e44c216 100644
--- a/src/temp/ivy/ivyUtil.c
+++ b/src/temp/ivy/ivyUtil.c
@@ -623,9 +623,10 @@ Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Ivy_ObjPrintVerbose( Ivy_Obj_t * pObj, int fHaig )
+void Ivy_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig )
{
Ivy_Obj_t * pTemp;
+ int fShowFanouts = 0;
assert( !Ivy_IsComplement(pObj) );
printf( "Node %5d : ", Ivy_ObjId(pObj) );
if ( Ivy_ObjIsConst1(pObj) )
@@ -635,14 +636,40 @@ void Ivy_ObjPrintVerbose( Ivy_Obj_t * pObj, int fHaig )
else if ( Ivy_ObjIsPo(pObj) )
printf( "PO" );
else if ( Ivy_ObjIsLatch(pObj) )
- printf( "latch %d%s", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(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)? "\'" : " ") );
+ 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 ( fShowFanouts )
+ {
+ Vec_Ptr_t * vFanouts;
+ Ivy_Obj_t * pFanout;
+ int i;
+ vFanouts = Vec_PtrAlloc( 10 );
+ printf( "\nFanouts:\n" );
+ Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
+ {
+ printf( " " );
+ printf( "Node %5d : ", Ivy_ObjId(pFanout) );
+ if ( Ivy_ObjIsPo(pFanout) )
+ printf( "PO" );
+ else if ( Ivy_ObjIsLatch(pFanout) )
+ printf( "latch (%d%s)", Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " ") );
+ else if ( Ivy_ObjIsBuf(pFanout) )
+ printf( "buffer (%d%s)", Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " ") );
+ else
+ printf( "AND( %5d%s, %5d%s )",
+ Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " "),
+ Ivy_ObjFanin1(pFanout)->Id, (Ivy_ObjFaninC1(pFanout)? "\'" : " ") );
+ printf( "\n" );
+ }
+ Vec_PtrFree( vFanouts );
+ return;
+ }
if ( !fHaig )
{
if ( pObj->pEquiv == NULL )
@@ -700,7 +727,7 @@ void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig )
printf( "\n" );
vNodes = Ivy_ManDfsSeq( p, NULL );
Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
- Ivy_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
+ Ivy_ObjPrintVerbose( p, pObj, fHaig ), printf( "\n" );
printf( "\n" );
}