summaryrefslogtreecommitdiffstats
path: root/src/aig/nwk
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-04-22 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2008-04-22 08:01:00 -0700
commite2e9aed11dd841801dae3cdf47db06946e7ffb28 (patch)
tree021c72bb7918dd10c3c8de87748c11ed910a2aaa /src/aig/nwk
parent7ec48bc20de6209f311715f4b1479cb2e0a4d906 (diff)
downloadabc-e2e9aed11dd841801dae3cdf47db06946e7ffb28.tar.gz
abc-e2e9aed11dd841801dae3cdf47db06946e7ffb28.tar.bz2
abc-e2e9aed11dd841801dae3cdf47db06946e7ffb28.zip
Version abc80422
Diffstat (limited to 'src/aig/nwk')
-rw-r--r--src/aig/nwk/nwkFlow.c28
-rw-r--r--src/aig/nwk/nwkFlow_depth.c626
2 files changed, 644 insertions, 10 deletions
diff --git a/src/aig/nwk/nwkFlow.c b/src/aig/nwk/nwkFlow.c
index 3a7e6df6..48496158 100644
--- a/src/aig/nwk/nwkFlow.c
+++ b/src/aig/nwk/nwkFlow.c
@@ -20,6 +20,14 @@
#include "nwk.h"
+/*
+ This code is based on the papers:
+ A. Hurst, A. Mishchenko, and R. Brayton, "Fast minimum-register retiming
+ via binary maximum-flow", Proc. FMCAD '07, pp. 181-187.
+ A. Hurst, A. Mishchenko, and R. Brayton, "Scalable min-area retiming
+ under simultaneous delay and initial state constraints". Proc. DAC'08.
+*/
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -368,7 +376,7 @@ int Nwk_ManVerifyCut_rec( Nwk_Obj_t * pObj )
return 0;
return 1;
}
-
+
/**Function*************************************************************
Synopsis [Verifies the forward cut.]
@@ -453,7 +461,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos
Counter++;
}
if ( fVerbose )
- printf( "Forward: Max-flow1 = %5d. ", Counter );
+ printf( "Forward: Max-flow = %4d -> ", Counter );
// continue flow computation from each LO
Nwk_ManIncrementTravIdFlow( pMan );
Nwk_ManForEachLoSeq( pMan, pObj, i )
@@ -464,7 +472,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos
Counter2++;
}
if ( fVerbose )
- printf( "Max-flow2 = %5d. ", Counter+Counter2 );
+ printf( "%4d. ", Counter+Counter2 );
// repeat flow computation from each LO
if ( Counter2 > 0 )
{
@@ -489,10 +497,10 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos
}
}
Nwk_ManCleanMarks( pMan );
- assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) );
+// assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) );
if ( fVerbose )
{
- printf( "Min-cut = %5d. Unmoved regs = %5d. ", Vec_PtrSize(vNodes), Counter );
+ printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
PRT( "Time", clock() - clk );
}
return vNodes;
@@ -536,8 +544,8 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
Nwk_ManIncrementTravIdFlow( pMan );
Counter++;
}
- if ( fVerbose )
- printf( "Backward: Max-flow1 = %5d. ", Counter );
+ if ( fVerbose )
+ printf( "Backward: Max-flow = %4d -> ", Counter );
// continue flow computation from each LI driver
Nwk_ManIncrementTravIdFlow( pMan );
Nwk_ManForEachLiSeq( pMan, pObj, i )
@@ -548,7 +556,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
Counter2++;
}
if ( fVerbose )
- printf( "Max-flow2 = %5d. ", Counter+Counter2 );
+ printf( "%4d. ", Counter+Counter2 );
// repeat flow computation from each LI driver
if ( Counter2 > 0 )
{
@@ -576,10 +584,10 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
if ( Nwk_ObjVisitedBotOnly( Nwk_ObjFanin0(pObj) ) )
Counter++;
Nwk_ManCleanMarks( pMan );
- assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) );
+// assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) );
if ( fVerbose )
{
- printf( "Min-cut = %5d. Unmoved regs = %5d. ", Vec_PtrSize(vNodes), Counter );
+ printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
PRT( "Time", clock() - clk );
}
return vNodes;
diff --git a/src/aig/nwk/nwkFlow_depth.c b/src/aig/nwk/nwkFlow_depth.c
new file mode 100644
index 00000000..a457631c
--- /dev/null
+++ b/src/aig/nwk/nwkFlow_depth.c
@@ -0,0 +1,626 @@
+/**CFile****************************************************************
+
+ FileName [nwkFlow.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [Max-flow/min-cut computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: nwkFlow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+
+/*
+ This code is based on the papers:
+ A. Hurst, A. Mishchenko, and R. Brayton, "Fast minimum-register retiming
+ via binary maximum-flow", Proc. FMCAD '07, pp. 181-187.
+ A. Hurst, A. Mishchenko, and R. Brayton, "Scalable min-area retiming
+ under simultaneous delay and initial state constraints". Proc. DAC'08.
+*/
+
+int DepthFwd, DepthBwd, DepthFwdMax, DepthBwdMax;
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// predecessors
+static inline Nwk_Obj_t * Nwk_ObjPred( Nwk_Obj_t * pObj ) { return pObj->pCopy; }
+static inline int Nwk_ObjSetPred( Nwk_Obj_t * pObj, Nwk_Obj_t * p ) { pObj->pCopy = p; return 1; }
+// sink
+static inline int Nwk_ObjIsSink( Nwk_Obj_t * pObj ) { return pObj->MarkA; }
+static inline void Nwk_ObjSetSink( Nwk_Obj_t * pObj ) { pObj->MarkA = 1; }
+// flow
+static inline int Nwk_ObjHasFlow( Nwk_Obj_t * pObj ) { return pObj->MarkB; }
+static inline void Nwk_ObjSetFlow( Nwk_Obj_t * pObj ) { pObj->MarkB = 1; }
+static inline void Nwk_ObjClearFlow( Nwk_Obj_t * pObj ) { pObj->MarkB = 0; }
+
+// representation of visited nodes
+// pObj->TravId < pNtk->nTravIds-2 --- not visited
+// pObj->TravId == pNtk->nTravIds-2 --- visited bot only
+// pObj->TravId == pNtk->nTravIds-1 --- visited top only
+// pObj->TravId == pNtk->nTravIds --- visited bot and top
+static inline int Nwk_ObjVisitedBotOnly( Nwk_Obj_t * pObj )
+{
+ return pObj->TravId == pObj->pMan->nTravIds - 2;
+}
+static inline int Nwk_ObjVisitedBot( Nwk_Obj_t * pObj )
+{
+ return pObj->TravId == pObj->pMan->nTravIds - 2 || pObj->TravId == pObj->pMan->nTravIds;
+}
+static inline int Nwk_ObjVisitedTop( Nwk_Obj_t * pObj )
+{
+ return pObj->TravId == pObj->pMan->nTravIds - 1 || pObj->TravId == pObj->pMan->nTravIds;
+}
+static inline void Nwk_ObjSetVisitedBot( Nwk_Obj_t * pObj )
+{
+ if ( pObj->TravId < pObj->pMan->nTravIds - 2 )
+ pObj->TravId = pObj->pMan->nTravIds - 2;
+ else if ( pObj->TravId == pObj->pMan->nTravIds - 1 )
+ pObj->TravId = pObj->pMan->nTravIds;
+ else
+ assert( 0 );
+}
+static inline void Nwk_ObjSetVisitedTop( Nwk_Obj_t * pObj )
+{
+ if ( pObj->TravId < pObj->pMan->nTravIds - 2 )
+ pObj->TravId = pObj->pMan->nTravIds - 1;
+ else if ( pObj->TravId == pObj->pMan->nTravIds - 2 )
+ pObj->TravId = pObj->pMan->nTravIds;
+ else
+ assert( 0 );
+}
+static inline Nwk_ManIncrementTravIdFlow( Nwk_Man_t * pMan )
+{
+ Nwk_ManIncrementTravId( pMan );
+ Nwk_ManIncrementTravId( pMan );
+ Nwk_ManIncrementTravId( pMan );
+}
+
+static int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+static int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+
+static int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+static int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Marks TFI of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ManMarkTfiCone_rec( Nwk_Obj_t * pObj )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( pObj->MarkA )
+ return;
+ pObj->MarkA = 1;
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ Nwk_ManMarkTfiCone_rec( pNext );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks TFO of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ManMarkTfoCone_rec( Nwk_Obj_t * pObj )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( pObj->MarkA )
+ return;
+ pObj->MarkA = 1;
+ Nwk_ObjForEachFanout( pObj, pNext, i )
+ Nwk_ManMarkTfoCone_rec( pNext );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Fast forward flow pushing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushForwardFast_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+ return 0;
+ Nwk_ObjSetTravIdCurrent( pObj );
+ if ( Nwk_ObjHasFlow(pObj) )
+ return 0;
+ if ( Nwk_ObjIsSink(pObj) )
+ {
+ Nwk_ObjSetFlow(pObj);
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ Nwk_ObjForEachFanout( pObj, pNext, i )
+ if ( Nwk_ManPushForwardFast_rec( pNext, pObj ) )
+ {
+ Nwk_ObjSetFlow(pObj);
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Fast backward flow pushing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushBackwardFast_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+ return 0;
+ Nwk_ObjSetTravIdCurrent( pObj );
+ if ( Nwk_ObjHasFlow(pObj) )
+ return 0;
+ if ( Nwk_ObjIsSink(pObj) )
+ {
+ Nwk_ObjSetFlow(pObj);
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ if ( Nwk_ManPushBackwardFast_rec( pNext, pObj ) )
+ {
+ Nwk_ObjSetFlow(pObj);
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Pushing the flow through the bottom part of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( Nwk_ObjVisitedBot(pObj) )
+ return 0;
+ Nwk_ObjSetVisitedBot(pObj);
+ DepthFwd++;
+ if ( DepthFwdMax < DepthFwd )
+ DepthFwdMax = DepthFwd;
+ // propagate through the internal edge
+ if ( Nwk_ObjHasFlow(pObj) )
+ {
+ if ( Nwk_ObjPred(pObj) )
+ if ( Nwk_ManPushForwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) )
+ {
+ DepthFwd--;
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ }
+ else if ( Nwk_ManPushForwardTop_rec(pObj, pObj) )
+ {
+ DepthFwd--;
+ Nwk_ObjSetFlow( pObj );
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ // try to push through the fanins
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) )
+ {
+ DepthFwd--;
+ return 1;
+ }
+ DepthFwd--;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Pushing the flow through the top part of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( Nwk_ObjVisitedTop(pObj) )
+ return 0;
+ Nwk_ObjSetVisitedTop(pObj);
+ // check if this is the sink
+ if ( Nwk_ObjIsSink(pObj) )
+ return 1;
+ DepthFwd++;
+ if ( DepthFwdMax < DepthFwd )
+ DepthFwdMax = DepthFwd;
+ // try to push through the fanouts
+ Nwk_ObjForEachFanout( pObj, pNext, i )
+ if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) )
+ {
+ DepthFwd--;
+ return 1;
+ }
+ // redirect the flow
+ if ( Nwk_ObjHasFlow(pObj) && !Nwk_ObjIsCi(pObj) )
+ if ( Nwk_ManPushForwardBot_rec( pObj, Nwk_ObjPred(pObj) ) )
+ {
+ DepthFwd--;
+ Nwk_ObjClearFlow( pObj );
+ return Nwk_ObjSetPred( pObj, NULL );
+ }
+ DepthFwd--;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Pushing the flow through the bottom part of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+ if ( Nwk_ObjVisitedBot(pObj) )
+ return 0;
+ Nwk_ObjSetVisitedBot(pObj);
+ // propagate through the internal edge
+ if ( Nwk_ObjHasFlow(pObj) )
+ {
+ if ( Nwk_ObjPred(pObj) )
+ if ( Nwk_ManPushBackwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) )
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ else if ( Nwk_ManPushBackwardTop_rec(pObj, pObj) )
+ {
+ Nwk_ObjSetFlow( pObj );
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Pushing the flow through the top part of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( Nwk_ObjVisitedTop(pObj) )
+ return 0;
+ Nwk_ObjSetVisitedTop(pObj);
+ // check if this is the sink
+ if ( Nwk_ObjIsSink(pObj) )
+ return 1;
+ // try to push through the fanins
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ if ( Nwk_ManPushBackwardBot_rec( pNext, pPred ) )
+ return 1;
+ // try to push through the fanouts
+ Nwk_ObjForEachFanout( pObj, pNext, i )
+ if ( !Nwk_ObjIsCo(pObj) && Nwk_ManPushBackwardTop_rec( pNext, pPred ) )
+ return 1;
+ // redirect the flow
+ if ( Nwk_ObjHasFlow(pObj) )
+ if ( Nwk_ObjPred(pObj) && Nwk_ManPushBackwardBot_rec( pObj, Nwk_ObjPred(pObj) ) )
+ {
+ Nwk_ObjClearFlow( pObj );
+ return Nwk_ObjSetPred( pObj, NULL );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 0 if there is an unmarked path to a CI.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManVerifyCut_rec( Nwk_Obj_t * pObj )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( pObj->MarkA )
+ return 1;
+ if ( Nwk_ObjIsLo(pObj) )
+ return 0;
+ if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+ return 1;
+ Nwk_ObjSetTravIdCurrent( pObj );
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ if ( !Nwk_ManVerifyCut_rec( pNext ) )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Verifies the forward cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManRetimeVerifyCutForward( Nwk_Man_t * pMan, Vec_Ptr_t * vNodes )
+{
+ Nwk_Obj_t * pObj;
+ int i;
+ // mark the nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ assert( pObj->MarkA == 0 );
+ pObj->MarkA = 1;
+ }
+ // traverse from the COs
+ Nwk_ManIncrementTravId( pMan );
+ Nwk_ManForEachCo( pMan, pObj, i )
+ if ( !Nwk_ManVerifyCut_rec( pObj ) )
+ printf( "Nwk_ManRetimeVerifyCutForward(): Internal cut verification failed.\n" );
+ // unmark the nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ pObj->MarkA = 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Verifies the forward cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManRetimeVerifyCutBackward( Nwk_Man_t * pMan, Vec_Ptr_t * vNodes )
+{
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes minimum cut for forward retiming.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose )
+{
+ Vec_Ptr_t * vNodes;
+ Nwk_Obj_t * pObj;
+ int i, RetValue, Counter = 0, Counter2 = 0;
+ int clk = clock();
+ // set the sequential parameters
+ pMan->nLatches = nLatches;
+ pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
+ pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
+ // mark the COs and the TFO of PIs
+ Nwk_ManForEachCo( pMan, pObj, i )
+ pObj->MarkA = 1;
+ Nwk_ManForEachPiSeq( pMan, pObj, i )
+ Nwk_ManMarkTfoCone_rec( pObj );
+ // start flow computation from each LO
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Nwk_ManForEachLoSeq( pMan, pObj, i )
+ {
+ if ( !Nwk_ManPushForwardFast_rec( pObj, NULL ) )
+ continue;
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Counter++;
+ }
+ if ( fVerbose )
+ printf( "Forward: Max-flow = %4d -> ", Counter );
+ // continue flow computation from each LO
+ DepthFwdMax = DepthFwd = 0;
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Nwk_ManForEachLoSeq( pMan, pObj, i )
+ {
+ printf( "%d ", DepthFwdMax );
+ if ( !Nwk_ManPushForwardBot_rec( pObj, NULL ) )
+ continue;
+ assert( DepthFwd == 0 );
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Counter2++;
+ }
+ printf( "DepthMax = %d.\n", DepthFwdMax );
+ if ( fVerbose )
+ printf( "%4d. ", Counter+Counter2 );
+ // repeat flow computation from each LO
+ if ( Counter2 > 0 )
+ {
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Nwk_ManForEachLoSeq( pMan, pObj, i )
+ {
+ RetValue = Nwk_ManPushForwardBot_rec( pObj, NULL );
+ assert( !RetValue );
+ }
+ }
+ // cut is a set of nodes whose bottom is visited but top is not visited
+ vNodes = Vec_PtrAlloc( Counter+Counter2 );
+ Counter = 0;
+ Nwk_ManForEachObj( pMan, pObj, i )
+ {
+ if ( Nwk_ObjVisitedBotOnly(pObj) )
+ {
+ assert( Nwk_ObjHasFlow(pObj) );
+ assert( !Nwk_ObjIsCo(pObj) );
+ Vec_PtrPush( vNodes, pObj );
+ Counter += Nwk_ObjIsCi(pObj);
+ }
+ }
+ Nwk_ManCleanMarks( pMan );
+ assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) );
+ if ( fVerbose )
+ {
+ printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
+ PRT( "Time", clock() - clk );
+ }
+ return vNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes minimum cut for backward retiming.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose )
+{
+ Vec_Ptr_t * vNodes;
+ Nwk_Obj_t * pObj;
+ int i, RetValue, Counter = 0, Counter2 = 0;
+ int clk = clock();
+ // set the sequential parameters
+ pMan->nLatches = nLatches;
+ pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
+ pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
+ // mark the CIs, the TFI of POs, and the constant nodes
+ Nwk_ManForEachCi( pMan, pObj, i )
+ pObj->MarkA = 1;
+ Nwk_ManForEachPoSeq( pMan, pObj, i )
+ Nwk_ManMarkTfiCone_rec( pObj );
+ Nwk_ManForEachNode( pMan, pObj, i )
+ if ( Nwk_ObjFaninNum(pObj) == 0 )
+ pObj->MarkA = 1;
+ // start flow computation from each LI driver
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Nwk_ManForEachLiSeq( pMan, pObj, i )
+ {
+ if ( !Nwk_ManPushBackwardFast_rec( Nwk_ObjFanin0(pObj), NULL ) )
+ continue;
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Counter++;
+ }
+ if ( fVerbose )
+ printf( "Backward: Max-flow = %4d -> ", Counter );
+ // continue flow computation from each LI driver
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Nwk_ManForEachLiSeq( pMan, pObj, i )
+ {
+ if ( !Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL ) )
+ continue;
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Counter2++;
+ }
+ if ( fVerbose )
+ printf( "%4d. ", Counter+Counter2 );
+ // repeat flow computation from each LI driver
+ if ( Counter2 > 0 )
+ {
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Nwk_ManForEachLiSeq( pMan, pObj, i )
+ {
+ RetValue = Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL );
+ assert( !RetValue );
+ }
+ }
+ // cut is a set of nodes whose bottom is visited but top is not visited
+ vNodes = Vec_PtrAlloc( Counter+Counter2 );
+ Nwk_ManForEachObj( pMan, pObj, i )
+ {
+ if ( Nwk_ObjVisitedBotOnly(pObj) )
+ {
+ assert( Nwk_ObjHasFlow(pObj) );
+ assert( !Nwk_ObjIsCo(pObj) );
+ Vec_PtrPush( vNodes, pObj );
+ }
+ }
+ // count CO drivers
+ Counter = 0;
+ Nwk_ManForEachLiSeq( pMan, pObj, i )
+ if ( Nwk_ObjVisitedBotOnly( Nwk_ObjFanin0(pObj) ) )
+ Counter++;
+ Nwk_ManCleanMarks( pMan );
+ assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) );
+ if ( fVerbose )
+ {
+ printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
+ PRT( "Time", clock() - clk );
+ }
+ return vNodes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+