Version abc80126

6 files changed, 1375 insertions, 316 deletions

diff --git a/src/opt/fret/fretFlow.c b/src/opt/fret/fretFlow.c
index 599aa341..a9cef327 100644
--- a/src/opt/fret/fretFlow.c
+++ b/src/opt/fret/fretFlow.c
@@ -59,31 +59,32 @@ void dfsfast_preorder( Abc_Ntk_t *pNtk ) {
 
   // create reverse timing edges for backward traversal
 #if !defined(IGNORE_TIMING)
-  if (maxDelayCon)
+  if (pManMR->maxDelay) {
     Abc_NtkForEachObj( pNtk, pObj, i ) {
       Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, j ) {
-        vTimeIn = FDATA(pNext)->vTimeInEdges;
+        vTimeIn = FDATA(pNext)->vNodes;
         if (!vTimeIn) {
-          vTimeIn = FDATA(pNext)->vTimeInEdges = Vec_PtrAlloc(2);
+          vTimeIn = FDATA(pNext)->vNodes = Vec_PtrAlloc(2);
         }
         Vec_PtrPush(vTimeIn, pObj);
       }
     }
+  }
 #endif
 
   // clear histogram
-  memset(Vec_IntArray(vSinkDistHist), 0, sizeof(int)*Vec_IntSize(vSinkDistHist));
+  memset(Vec_IntArray(pManMR->vSinkDistHist), 0, sizeof(int)*Vec_IntSize(pManMR->vSinkDistHist));
 
   // seed queue : latches, PIOs, and blocks
   Abc_NtkForEachObj( pNtk, pObj, i )
     if (Abc_ObjIsPo(pObj) ||
         Abc_ObjIsLatch(pObj) || 
-        (fIsForward && FTEST(pObj, BLOCK))) {
+        (pManMR->fIsForward && FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask)) {
       Vec_PtrPush(qn, pObj);
       Vec_IntPush(qe, 'r');
       FDATA(pObj)->r_dist = 1;
     } else if (Abc_ObjIsPi(pObj) || 
-               (!fIsForward && FTEST(pObj, BLOCK))) {
+               (!pManMR->fIsForward && FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask)) {
       Vec_PtrPush(qn, pObj);
       Vec_IntPush(qe, 'e');
       FDATA(pObj)->e_dist = 1;
@@ -100,7 +101,7 @@ void dfsfast_preorder( Abc_Ntk_t *pNtk ) {
       d = FDATA(pObj)->r_dist;
 
       // 1. structural edges
-      if (fIsForward) {
+      if (pManMR->fIsForward) {
         Abc_ObjForEachFanin( pObj, pNext, i )
           if (!FDATA(pNext)->e_dist) {
             FDATA(pNext)->e_dist = d+1;
@@ -118,26 +119,26 @@ void dfsfast_preorder( Abc_Ntk_t *pNtk ) {
       if (d == 1) continue;
 
       // 2. reverse edges (forward retiming only)
-      if (fIsForward) {
+      if (pManMR->fIsForward) {
         Abc_ObjForEachFanout( pObj, pNext, i )
           if (!FDATA(pNext)->r_dist && !Abc_ObjIsLatch(pNext)) {
             FDATA(pNext)->r_dist = d+1;
             Vec_PtrPush(qn, pNext);
             Vec_IntPush(qe, 'r');
           }          
-      }
 
-      // 3. timimg edges (reverse)
+      // 3. timimg edges (forward retiming only)
 #if !defined(IGNORE_TIMING)
-      if (maxDelayCon && FDATA(pObj)->vTimeInEdges)
-        Vec_PtrForEachEntry( FDATA(pObj)->vTimeInEdges, pNext, i ) {
-          if (!FDATA(pNext)->r_dist) {
-            FDATA(pNext)->r_dist = d+1;
-            Vec_PtrPush(qn, pNext);
-            Vec_IntPush(qe, 'r');
+        if (pManMR->maxDelay && FDATA(pObj)->vNodes)
+          Vec_PtrForEachEntry( FDATA(pObj)->vNodes, pNext, i ) {
+            if (!FDATA(pNext)->r_dist) {
+              FDATA(pNext)->r_dist = d+1;
+              Vec_PtrPush(qn, pNext);
+              Vec_IntPush(qe, 'r');
+            }
           }
-        }
 #endif
+      }
       
     } else { // if 'e'
       if (Abc_ObjIsLatch(pObj)) continue;
@@ -152,39 +153,52 @@ void dfsfast_preorder( Abc_Ntk_t *pNtk ) {
       }
 
       // 2. reverse edges (backward retiming only)
-      if (!fIsForward) {
+      if (!pManMR->fIsForward) {
         Abc_ObjForEachFanin( pObj, pNext, i )
           if (!FDATA(pNext)->e_dist && !Abc_ObjIsLatch(pNext)) {
             FDATA(pNext)->e_dist = d+1;
             Vec_PtrPush(qn, pNext);
             Vec_IntPush(qe, 'e');
           }  
+
+      // 3. timimg edges (backward retiming only)
+#if !defined(IGNORE_TIMING)
+        if (pManMR->maxDelay && FDATA(pObj)->vNodes)
+          Vec_PtrForEachEntry( FDATA(pObj)->vNodes, pNext, i ) {
+            if (!FDATA(pNext)->e_dist) {
+              FDATA(pNext)->e_dist = d+1;
+              Vec_PtrPush(qn, pNext);
+              Vec_IntPush(qe, 'e');
+            }
+          }
+#endif
       }
     }
   }
  
-  // create reverse timing edges for backward traversal
+  // free time edges
 #if !defined(IGNORE_TIMING)
-  if (maxDelayCon)
+  if (pManMR->maxDelay) {
     Abc_NtkForEachObj( pNtk, pObj, i ) {
-      vTimeIn = FDATA(pObj)->vTimeInEdges;
+      vTimeIn = FDATA(pObj)->vNodes;
       if (vTimeIn) {
         Vec_PtrFree(vTimeIn);
-        FDATA(pObj)->vTimeInEdges = 0;
+        FDATA(pObj)->vNodes = 0;
       }
     }
+  }
 #endif
 
   Abc_NtkForEachObj( pNtk, pObj, i ) {
-    Vec_IntAddToEntry(vSinkDistHist, FDATA(pObj)->r_dist, 1);
-    Vec_IntAddToEntry(vSinkDistHist, FDATA(pObj)->e_dist, 1);
+    Vec_IntAddToEntry(pManMR->vSinkDistHist, FDATA(pObj)->r_dist, 1);
+    Vec_IntAddToEntry(pManMR->vSinkDistHist, FDATA(pObj)->e_dist, 1);
 
 #ifdef DEBUG_PREORDER
     printf("node %d\t: r=%d\te=%d\n", Abc_ObjId(pObj), FDATA(pObj)->r_dist, FDATA(pObj)->e_dist);
 #endif
   }
 
-  printf("\t\tpre-ordered (max depth=%d)\n", d+1);
+  // printf("\t\tpre-ordered (max depth=%d)\n", d+1);
 
   // deallocate
   Vec_PtrFree( qn );
@@ -195,11 +209,13 @@ int dfsfast_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   int i;
   Abc_Obj_t *pNext;
   
-  if (fSinkDistTerminate) return 0;
+  if (pManMR->fSinkDistTerminate) return 0;
 
-  if(FTEST(pObj, BLOCK) ||
+  // have we reached the sink?
+  if(FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask ||
      Abc_ObjIsPi(pObj)) {
-    assert(!fIsForward);
+    assert(pPred);
+    assert(!pManMR->fIsForward);
     return 1;
   }
 
@@ -210,7 +226,7 @@ int dfsfast_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
 #endif  
 
   // 1. structural edges
-  if (fIsForward)
+  if (pManMR->fIsForward)
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       if (!FTEST(pNext, VISITED_R) &&
           FDIST(pObj, e, pNext, r) &&
@@ -237,7 +253,7 @@ int dfsfast_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
     goto not_found;
 
   // 2. reverse edges (backward retiming only)
-  if (!fIsForward) { 
+  if (!pManMR->fIsForward) { 
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       if (!FTEST(pNext, VISITED_E) &&
           FDIST(pObj, e, pNext, e) &&
@@ -248,6 +264,21 @@ int dfsfast_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
         goto found;
       }
     }
+
+  // 3. timing edges (backward retiming only)
+#if !defined(IGNORE_TIMING)
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
+        if (!FTEST(pNext, VISITED_E) &&
+            FDIST(pObj, e, pNext, e) &&
+            dfsfast_e(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+          printf("o");
+#endif
+          goto found;
+        }
+      }
+#endif
   }
   
   // unwind
@@ -281,7 +312,7 @@ int dfsfast_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   int i;
   Abc_Obj_t *pNext, *pOldPred;
 
-  if (fSinkDistTerminate) return 0;
+  if (pManMR->fSinkDistTerminate) return 0;
 
 #ifdef DEBUG_VISITED
   printf("(%dr=%d) ", Abc_ObjId(pObj), FDATA(pObj)->r_dist);
@@ -289,8 +320,8 @@ int dfsfast_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
 
   // have we reached the sink?
   if (Abc_ObjIsLatch(pObj) ||
-      Abc_ObjIsPo(pObj) || 
-      (fIsForward && FTEST(pObj, BLOCK))) {
+      (pManMR->fIsForward && Abc_ObjIsPo(pObj)) || 
+      (pManMR->fIsForward && FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask)) {
     assert(pPred);
     return 1;
   }
@@ -330,7 +361,7 @@ int dfsfast_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   }
  
   // 2. reverse edges (forward retiming only)
-  if (fIsForward) {
+  if (pManMR->fIsForward) {
     Abc_ObjForEachFanin( pObj, pNext, i ) {
       if (!FTEST(pNext, VISITED_R) &&
           FDIST(pObj, r, pNext, r) &&
@@ -342,22 +373,22 @@ int dfsfast_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
         goto found;
       }
     }
-  }
   
-  // 3. timing edges
+  // 3. timing edges (forward retiming only)
 #if !defined(IGNORE_TIMING)
-  if (maxDelayCon) 
-    Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
-      if (!FTEST(pNext, VISITED_R) &&
-          FDIST(pObj, r, pNext, r) &&
-          dfsfast_r(pNext, pPred)) {
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
+        if (!FTEST(pNext, VISITED_R) &&
+            FDIST(pObj, r, pNext, r) &&
+            dfsfast_r(pNext, pPred)) {
 #ifdef DEBUG_PRINT_FLOWS
-        printf("o");
+          printf("o");
 #endif
-        goto found;
+          goto found;
+        }
       }
-    }
 #endif
+  }
   
   FUNSET(pObj, VISITED_R);
   dfsfast_r_retreat(pObj);
@@ -379,7 +410,7 @@ dfsfast_e_retreat(Abc_Obj_t *pObj) {
   int adj_dist, min_dist = MAX_DIST;
   
   // 1. structural edges
-  if (fIsForward)
+  if (pManMR->fIsForward)
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       adj_dist = FDATA(pNext)->r_dist;
       if (adj_dist) min_dist = MIN(min_dist, adj_dist);
@@ -399,11 +430,20 @@ dfsfast_e_retreat(Abc_Obj_t *pObj) {
   }
 
   // 3. reverse edges (backward retiming only)
-  if (!fIsForward) {
+  if (!pManMR->fIsForward) {
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       adj_dist = FDATA(pNext)->e_dist;
       if (adj_dist) min_dist = MIN(min_dist, adj_dist);
     }
+
+  // 4. timing edges (backward retiming only)
+#if !defined(IGNORE_TIMING)
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
+        adj_dist = FDATA(pNext)->e_dist;
+        if (adj_dist) min_dist = MIN(min_dist, adj_dist);
+      }
+#endif
   }
 
  update:
@@ -412,12 +452,12 @@ dfsfast_e_retreat(Abc_Obj_t *pObj) {
   // printf("[%de=%d->%d] ", Abc_ObjId(pObj), old_dist, min_dist+1);
   FDATA(pObj)->e_dist = min_dist;
 
-  assert(min_dist < Vec_IntSize(vSinkDistHist));
-  h = Vec_IntArray(vSinkDistHist);
+  assert(min_dist < Vec_IntSize(pManMR->vSinkDistHist));
+  h = Vec_IntArray(pManMR->vSinkDistHist);
   h[old_dist]--;
   h[min_dist]++;
   if (!h[old_dist]) {
-    fSinkDistTerminate = 1;
+    pManMR->fSinkDistTerminate = 1;
   }
 }
 
@@ -440,34 +480,34 @@ dfsfast_r_retreat(Abc_Obj_t *pObj) {
   }
 
   // 2. reverse edges (forward retiming only)
-  if (fIsForward) {
+  if (pManMR->fIsForward) {
     Abc_ObjForEachFanin( pObj, pNext, i )
       if (!Abc_ObjIsLatch(pNext)) {
         adj_dist = FDATA(pNext)->r_dist;
         if (adj_dist) min_dist = MIN(min_dist, adj_dist);
       }
-  }
 
-  // 3. timing edges
+  // 3. timing edges (forward retiming only)
 #if !defined(IGNORE_TIMING)
-  if (maxDelayCon) 
-    Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
-      adj_dist = FDATA(pNext)->r_dist;
-      if (adj_dist) min_dist = MIN(min_dist, adj_dist);
-    }
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
+        adj_dist = FDATA(pNext)->r_dist;
+        if (adj_dist) min_dist = MIN(min_dist, adj_dist);
+      }
 #endif
+  }
 
   ++min_dist;
   if (min_dist >= MAX_DIST) min_dist = 0;
   //printf("[%dr=%d->%d] ", Abc_ObjId(pObj), old_dist, min_dist+1);
   FDATA(pObj)->r_dist = min_dist;
 
-  assert(min_dist < Vec_IntSize(vSinkDistHist));
-  h = Vec_IntArray(vSinkDistHist);
+  assert(min_dist < Vec_IntSize(pManMR->vSinkDistHist));
+  h = Vec_IntArray(pManMR->vSinkDistHist);
   h[old_dist]--;
   h[min_dist]++;
   if (!h[old_dist]) {
-    fSinkDistTerminate = 1;
+    pManMR->fSinkDistTerminate = 1;
   }
 }
 
@@ -487,8 +527,10 @@ int dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   int i;
   Abc_Obj_t *pNext;
   
-  if (FTEST(pObj, BLOCK) || Abc_ObjIsPi(pObj)) {
-    assert(!fIsForward);
+  if (FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask || 
+      Abc_ObjIsPi(pObj)) {
+    assert(pPred);
+    assert(!pManMR->fIsForward);
     return 1;
   }
 
@@ -497,7 +539,7 @@ int dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   // printf(" %de\n", Abc_ObjId(pObj));
   
   // 1. structural edges
-  if (fIsForward)
+  if (pManMR->fIsForward)
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       if (!FTEST(pNext, VISITED_R) &&
           dfsplain_r(pNext, pPred)) {
@@ -521,8 +563,8 @@ int dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   if (Abc_ObjIsLatch(pObj))
     return 0;
 
-  // 2. follow reverse edges
-  if (!fIsForward) { // reverse retiming only
+  // 2. reverse edges (backward retiming only)
+  if (!pManMR->fIsForward) {
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       if (!FTEST(pNext, VISITED_E) &&
           dfsplain_e(pNext, pPred)) {
@@ -532,6 +574,20 @@ int dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
         goto found;
       }
     }
+
+  // 3. timing edges (backward retiming only)
+#if !defined(IGNORE_TIMING)
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
+        if (!FTEST(pNext, VISITED_E) &&
+            dfsplain_e(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+          printf("o");
+#endif
+          goto found;
+        }
+      }
+#endif
   }
   
   // unwind
@@ -562,8 +618,8 @@ int dfsplain_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
 
   // have we reached the sink?
   if (Abc_ObjIsLatch(pObj) || 
-      Abc_ObjIsPo(pObj) || 
-      (fIsForward && FTEST(pObj, BLOCK))) {
+      (pManMR->fIsForward && Abc_ObjIsPo(pObj)) || 
+      (pManMR->fIsForward && FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask)) {
     assert(pPred);
     return 1;
   }
@@ -603,7 +659,7 @@ int dfsplain_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   }
  
   // 2. follow reverse edges
-  if (fIsForward) { // forward retiming only
+  if (pManMR->fIsForward) { // forward retiming only
     Abc_ObjForEachFanin( pObj, pNext, i ) {
       if (!FTEST(pNext, VISITED_R) &&
           !Abc_ObjIsLatch(pNext) &&
@@ -614,21 +670,21 @@ int dfsplain_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
         goto found;
       }
     }
-  }
   
-  // 3. follow timing constraints
+  // 3. timing edges (forward only)
 #if !defined(IGNORE_TIMING)
-  if (maxDelayCon) 
-    Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
-      if (!FTEST(pNext, VISITED_R) &&
-          dfsplain_r(pNext, pPred)) {
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
+        if (!FTEST(pNext, VISITED_R) &&
+            dfsplain_r(pNext, pPred)) {
 #ifdef DEBUG_PRINT_FLOWS
-        printf("o");
+          printf("o");
 #endif
-        goto found;
+          goto found;
+        }
       }
-    }
 #endif
+  }
   
   return 0;
 
diff --git a/src/opt/fret/fretInit.c b/src/opt/fret/fretInit.c
index 30d1c553..53df7386 100644
--- a/src/opt/fret/fretInit.c
+++ b/src/opt/fret/fretInit.c
@@ -22,6 +22,7 @@
 #include "vec.h"
 #include "io.h"
 #include "fretime.h"
+#include "mio.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION PROTOTYPES                          ///
@@ -36,9 +37,6 @@ static Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj,
 static void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj );
 static void Abc_FlowRetime_SimulateSop( Abc_Obj_t * pObj, char *pSop );
 
-Abc_Ntk_t *pInitNtk;
-int        fSolutionIsDc;
-
 extern void * Abc_FrameReadLibGen();                    
 extern Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup );
 
@@ -62,9 +60,9 @@ extern Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup );
 void
 Abc_FlowRetime_InitState( Abc_Ntk_t * pNtk ) {
 
-  if (!fComputeInitState) return;
+  if (!pManMR->fComputeInitState) return;
 
-  if (fIsForward)
+  if (pManMR->fIsForward)
     Abc_FlowRetime_UpdateForwardInit( pNtk );
   else {
     Abc_FlowRetime_UpdateBackwardInit( pNtk );
@@ -118,7 +116,7 @@ void Abc_FlowRetime_UpdateForwardInit( Abc_Ntk_t * pNtk ) {
   Abc_Obj_t *pObj, *pFanin;
   int i;
 
-  printf("\t\tupdating init state\n");
+  vprintf("\t\tupdating init state\n");
 
   Abc_NtkIncrementTravId( pNtk );
 
@@ -195,7 +193,7 @@ static inline void Abc_FlowRetime_SetInitValue( Abc_Obj_t * pObj,
 void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
   Abc_Ntk_t *pNtk = Abc_ObjNtk(pObj);
   Abc_Obj_t * pFanin;
-  int i, j, rAnd, rOr, rVar, dcAnd, dcOr, dcVar, v;
+  int i, rAnd, rVar, dcAnd, dcVar;
   DdManager * dd = pNtk->pManFunc;
   DdNode *pBdd = pObj->pData, *pVar;
   
@@ -206,7 +204,7 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
     Abc_FlowRetime_SetInitValue(pObj, 1, 0);
     return;
   }
-  if (!Abc_NtkIsStrash( pNtk ))
+  if (!Abc_NtkIsStrash( pNtk ) && Abc_ObjIsNode(pObj)) {
     if (Abc_NodeIsConst0(pObj)) {
       Abc_FlowRetime_SetInitValue(pObj, 0, 0);
       return;
@@ -214,6 +212,7 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
       Abc_FlowRetime_SetInitValue(pObj, 1, 0);
       return;
     }
+  }
   
   // (ii) terminal nodes
   if (!Abc_ObjIsNode(pObj)) {
@@ -229,7 +228,7 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
 
   // ------ SOP network
   if ( Abc_NtkHasSop( pNtk )) {
-    Abc_FlowRetime_SimulateSop( pObj, Abc_ObjData(pObj) );
+    Abc_FlowRetime_SimulateSop( pObj, (char *)Abc_ObjData(pObj) );
     return;
   }
 
@@ -242,12 +241,12 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
     // do nothing for X values
     Abc_ObjForEachFanin(pObj, pFanin, i) {
       pVar = Cudd_bddIthVar( dd, i );
-      if (FTEST(pFanin, INIT_CARE))
-        if (FTEST(pFanin, INIT_0)) {
+      if (FTEST(pFanin, INIT_CARE)) {
+        if (FTEST(pFanin, INIT_0))
           pBdd = Cudd_Cofactor( dd, pBdd, Cudd_Not(pVar) ); 
-        } else {
+        else
           pBdd = Cudd_Cofactor( dd, pBdd, pVar ); 
-        }
+      }
     }
 
     // if function has not been reduced to 
@@ -285,7 +284,7 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
 
   // ------ MAPPED network
   else if ( Abc_NtkHasMapping( pNtk )) {
-    Abc_FlowRetime_SimulateSop( pObj, Mio_GateReadSop(pObj->pData) );
+    Abc_FlowRetime_SimulateSop( pObj, (char *)Mio_GateReadSop(pObj->pData) );
     return;
   }
 
@@ -307,7 +306,7 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
 void Abc_FlowRetime_SimulateSop( Abc_Obj_t * pObj, char *pSop ) {
   Abc_Obj_t * pFanin;
   char *pCube;
-  int i, j, rAnd, rOr, rVar, dcAnd, dcOr, dcVar, v;
+  int i, j, rAnd, rOr, rVar, dcAnd, dcOr, v;
 
   assert( pSop && !Abc_SopIsExorType(pSop) );
       
@@ -363,14 +362,14 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
 
   // create the network used for the initial state computation
   if (Abc_NtkHasMapping(pNtk))
-    pInitNtk = Abc_NtkAlloc( pNtk->ntkType, ABC_FUNC_SOP, 1 );
+    pManMR->pInitNtk = Abc_NtkAlloc( pNtk->ntkType, ABC_FUNC_SOP, 1 );
   else
-    pInitNtk = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+    pManMR->pInitNtk = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
 
   // mitre inputs
   Abc_NtkForEachLatch( pNtk, pLatch, i ) {
     // map latch to initial state network
-    pPi = Abc_NtkCreatePi( pInitNtk );
+    pPi = Abc_NtkCreatePi( pManMR->pInitNtk );
 
     // has initial state requirement?
     if (Abc_LatchIsInit0(pLatch)) {
@@ -378,7 +377,7 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
       if (Abc_NtkHasAig(pNtk))
         pObj = Abc_ObjNot( pPi );
       else
-        pObj = Abc_NtkCreateNodeInv( pInitNtk, pPi );
+        pObj = Abc_NtkCreateNodeInv( pManMR->pInitNtk, pPi );
 
       Vec_PtrPush(vObj, pObj);
     }
@@ -392,22 +391,24 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
 
   // are there any nodes not DC?
   if (!Vec_PtrSize(vObj)) {
-    fSolutionIsDc = 1;
+    pManMR->fSolutionIsDc = 1;
     return;
   } else 
-    fSolutionIsDc = 0;
+    pManMR->fSolutionIsDc = 0;
 
   // mitre output
   if (Abc_NtkHasAig(pNtk)) {
     // create AND-by-AND
     pObj = Vec_PtrPop( vObj );
     while( Vec_PtrSize(vObj) )
-      pObj = Abc_AigAnd( pInitNtk->pManFunc, pObj, Vec_PtrPop( vObj ) ); 
+      pObj = Abc_AigAnd( pManMR->pInitNtk->pManFunc, pObj, Vec_PtrPop( vObj ) ); 
   } else
     // create n-input AND gate
-    pObj = Abc_NtkCreateNodeAnd( pInitNtk, vObj );
+    pObj = Abc_NtkCreateNodeAnd( pManMR->pInitNtk, vObj );
+
+  Abc_ObjAddFanin( Abc_NtkCreatePo( pManMR->pInitNtk ), pObj );
 
-  Abc_ObjAddFanin( Abc_NtkCreatePo( pInitNtk ), pObj );
+  Vec_PtrFree( vObj );
 }
 
 
@@ -422,27 +423,26 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
+int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   int i;
   Abc_Obj_t *pObj, *pInitObj;
-  Abc_Ntk_t *pRestrNtk;
   Vec_Ptr_t *vDelete = Vec_PtrAlloc(0);
   int result;
 
-  assert(pInitNtk);
+  assert(pManMR->pInitNtk);
 
   // is the solution entirely DC's?
-  if (fSolutionIsDc) {
-    Abc_NtkDelete(pInitNtk);
+  if (pManMR->fSolutionIsDc) {
+    Abc_NtkDelete(pManMR->pInitNtk);
     Vec_PtrFree(vDelete);
     Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj );
-    printf("\tno init state computation: all-don't-care solution\n");
-    return;
+    vprintf("\tno init state computation: all-don't-care solution\n");
+    return 1;
   }
 
   // check that network is combinational
   // mark superfluous BI nodes for deletion
-  Abc_NtkForEachObj( pInitNtk, pObj, i ) {
+  Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i ) {
     assert(!Abc_ObjIsLatch(pObj));
     assert(!Abc_ObjIsBo(pObj));
     
@@ -460,34 +460,36 @@ void Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   Vec_PtrFree(vDelete);
 
   // do some final cleanup on the network
-  Abc_NtkAddDummyPoNames(pInitNtk);
-  Abc_NtkAddDummyPiNames(pInitNtk);
-  if (Abc_NtkIsLogic(pInitNtk))
-    Abc_NtkCleanup(pInitNtk, 0);
-  else if (Abc_NtkIsStrash(pInitNtk)) {  
-    Abc_NtkReassignIds(pInitNtk);
+  Abc_NtkAddDummyPoNames(pManMR->pInitNtk);
+  Abc_NtkAddDummyPiNames(pManMR->pInitNtk);
+  if (Abc_NtkIsLogic(pManMR->pInitNtk))
+    Abc_NtkCleanup(pManMR->pInitNtk, 0);
+  else if (Abc_NtkIsStrash(pManMR->pInitNtk)) {  
+    Abc_NtkReassignIds(pManMR->pInitNtk);
   }
   
-  printf("\tsolving for init state (%d nodes)... ", Abc_NtkObjNum(pInitNtk));
+  vprintf("\tsolving for init state (%d nodes)... ", Abc_NtkObjNum(pManMR->pInitNtk));
   fflush(stdout);
 
   // convert SOPs to BDD
-  if (Abc_NtkHasSop(pInitNtk))
-    Abc_NtkSopToBdd( pInitNtk );
+  if (Abc_NtkHasSop(pManMR->pInitNtk))
+    Abc_NtkSopToBdd( pManMR->pInitNtk );
   
   // solve
-  result = Abc_NtkMiterSat( pInitNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
+  result = Abc_NtkMiterSat( pManMR->pInitNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
 
-  if (!result) printf("SUCCESS\n");
-  else  {
-    printf("FAILURE\n");  
-    printf("\tsetting all initial states to don't-care\n");
+  if (!result) { 
+    vprintf("SUCCESS\n");
+  } else  {    
+    vprintf("FAILURE\n");
+    printf("WARNING: no equivalent init state. setting all initial states to don't-cares\n");
     Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj );
-    return;
+    Abc_NtkDelete(pManMR->pInitNtk);
+    return 0;
   }
 
   // clear initial values, associate PIs to latches
-  Abc_NtkForEachPi( pInitNtk, pInitObj, i ) Abc_ObjSetCopy( pInitObj, NULL );
+  Abc_NtkForEachPi( pManMR->pInitNtk, pInitObj, i ) Abc_ObjSetCopy( pInitObj, NULL );
   Abc_NtkForEachLatch( pNtk, pObj, i ) {
     pInitObj = Abc_ObjData( pObj );
     assert( Abc_ObjIsPi( pInitObj ));
@@ -496,10 +498,10 @@ void Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   }
 
   // copy solution from PIs to latches
-  assert(pInitNtk->pModel);
-  Abc_NtkForEachPi( pInitNtk, pInitObj, i ) {
+  assert(pManMR->pInitNtk->pModel);
+  Abc_NtkForEachPi( pManMR->pInitNtk, pInitObj, i ) {
     if ((pObj = Abc_ObjCopy( pInitObj ))) {
-      if ( pInitNtk->pModel[i] )
+      if ( pManMR->pInitNtk->pModel[i] )
         Abc_LatchSetInit1( pObj );
       else
         Abc_LatchSetInit0( pObj );
@@ -512,7 +514,9 @@ void Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
 #endif
 
   // deallocate
-  Abc_NtkDelete( pInitNtk );
+  Abc_NtkDelete( pManMR->pInitNtk );
+
+  return 1;
 }
 
 
@@ -528,11 +532,10 @@ void Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
 
 ***********************************************************************/
 void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) {
-  Abc_Obj_t *pOrigObj,  *pOrigFanin, *pInitObj, *pInitFanin;
+  Abc_Obj_t *pOrigObj,  *pInitObj;
   Vec_Ptr_t *vBo = Vec_PtrAlloc(100);
   Vec_Ptr_t *vOldPis = Vec_PtrAlloc(100);
-  void *pData;
-  int i, j;
+  int i;
 
   // remove PIs from network (from BOs)
   Abc_NtkForEachObj( pNtk, pOrigObj, i )
@@ -624,20 +627,20 @@ Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj,
       if (!pOrigObj->pData) {
         // assume terminal...
         assert(Abc_ObjFaninNum(pOrigObj) == 1);
-        pInitObj = Abc_NtkCreateNodeBuf( pInitNtk, NULL );
+        pInitObj = Abc_NtkCreateNodeBuf( pManMR->pInitNtk, NULL );
       } else {
-        pInitObj = Abc_NtkCreateObj( pInitNtk, Abc_ObjType(pOrigObj) );
+        pInitObj = Abc_NtkCreateObj( pManMR->pInitNtk, Abc_ObjType(pOrigObj) );
         pData = Mio_GateReadSop(pOrigObj->pData);
         assert( Abc_SopGetVarNum(pData) == Abc_ObjFaninNum(pOrigObj) );
 
-        pInitObj->pData = Abc_SopRegister( pInitNtk->pManFunc, pData );
+        pInitObj->pData = Abc_SopRegister( pManMR->pInitNtk->pManFunc, pData );
       }
     } else {
       pData = Abc_ObjCopy( pOrigObj );   // save ptr to flow data    
       if (Abc_NtkIsStrash( pNtk ) && Abc_AigNodeIsConst( pOrigObj ))
-        pInitObj = Abc_AigConst1( pInitNtk );
+        pInitObj = Abc_AigConst1( pManMR->pInitNtk );
       else
-        pInitObj = Abc_NtkDupObj( pInitNtk, pOrigObj, 0 );
+        pInitObj = Abc_NtkDupObj( pManMR->pInitNtk, pOrigObj, 0 );
       Abc_ObjSetCopy( pOrigObj, pData ); // restore ptr to flow data
 
       // copy complementation
@@ -695,7 +698,7 @@ void Abc_FlowRetime_VerifyBackwardInit( Abc_Ntk_t * pNtk ) {
   Abc_Obj_t *pObj, *pFanin;
   int i;
 
-  printf("\t\tupdating init state\n");
+  vprintf("\t\tupdating init state\n");
 
   Abc_NtkIncrementTravId( pNtk );
 
@@ -741,3 +744,19 @@ void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj ) {
   
   Abc_FlowRetime_SimulateNode( pObj );
 }
+
+
+/**Function*************************************************************
+
+  Synopsis    [Constrains backward retiming for initializability.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_ConstrainInit( ) {
+  // unimplemented
+}
diff --git a/src/opt/fret/fretMain.c b/src/opt/fret/fretMain.c
index 4ce78a9b..780c1f6f 100644
--- a/src/opt/fret/fretMain.c
+++ b/src/opt/fret/fretMain.c
@@ -28,9 +28,10 @@
 
 static void Abc_FlowRetime_AddDummyFanin( Abc_Obj_t * pObj );
 
+static void Abc_FlowRetime_MainLoop( );
+
 static void Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk );
 static void Abc_FlowRetime_MarkReachable_rec( Abc_Obj_t * pObj, char end );
-static int  Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk );
 static int  Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk );
 static void  Abc_FlowRetime_RemoveLatchBubbles( Abc_Obj_t * pLatch );
 
@@ -40,12 +41,12 @@ static int  Abc_FlowRetime_VerifyPathLatencies_rec( Abc_Obj_t * pObj, int markD
 extern void Abc_NtkMarkCone_rec( Abc_Obj_t * pObj, int fForward );
 extern Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup );
 
-int         fIsForward, fComputeInitState;
-int         fSinkDistTerminate;
-Vec_Int_t  *vSinkDistHist;
-int         maxDelayCon;
+void
+print_node3(Abc_Obj_t *pObj);
+
+MinRegMan_t *pManMR;
 
-int         fPathError = 0;
+int          fPathError = 0;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -63,53 +64,64 @@ int         fPathError = 0;
 
 ***********************************************************************/
 Abc_Ntk_t *
-Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState_,
+Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
                        int fForwardOnly, int fBackwardOnly, int nMaxIters,
-                       int maxDelay ) {
+                       int maxDelay, int fFastButConservative ) {
 
-  int i, j, nNodes, nLatches, flow, last, cut;
-  int iteration = 0;
-  Flow_Data_t *pDataArray;
+  int i;
   Abc_Obj_t   *pObj, *pNext;
 
-  fComputeInitState = fComputeInitState_;
+  // create manager
+  pManMR = ALLOC( MinRegMan_t, 1 );
+
+  pManMR->pNtk = pNtk;
+  pManMR->fVerbose = fVerbose;
+  pManMR->fComputeInitState = fComputeInitState;
+  pManMR->fGuaranteeInitState = 0;
+  pManMR->fForwardOnly = fForwardOnly;
+  pManMR->fBackwardOnly = fBackwardOnly;
+  pManMR->nMaxIters = nMaxIters;
+  pManMR->maxDelay = maxDelay;
+  pManMR->fComputeInitState = fComputeInitState;
+  pManMR->fConservTimingOnly = fFastButConservative;
+  pManMR->vNodes = Vec_PtrAlloc(100);
 
-  printf("Flow-based minimum-register retiming...\n");  
+  vprintf("Flow-based minimum-register retiming...\n");  
 
   if (!Abc_NtkHasOnlyLatchBoxes(pNtk)) {
     printf("\tERROR: Can not retime with black/white boxes\n");
     return pNtk;
   }
 
-  maxDelayCon = maxDelay;
-  if (maxDelayCon) {
-    printf("\tmax delay constraint = %d\n", maxDelayCon);
-    if (maxDelayCon < (i = Abc_NtkLevel(pNtk))) {
+  if (maxDelay) {
+    vprintf("\tmax delay constraint = %d\n", maxDelay);
+    if (maxDelay < (i = Abc_NtkLevel(pNtk))) {
       printf("ERROR: max delay constraint must be > current max delay (%d)\n", i);
       return pNtk;
     }
   }
 
   // print info about type of network
-  printf("\tnetlist type = ");
-  if (Abc_NtkIsNetlist( pNtk )) printf("netlist/");
-  else if (Abc_NtkIsLogic( pNtk )) printf("logic/");
-  else if (Abc_NtkIsStrash( pNtk )) printf("strash/");
-  else printf("***unknown***/");
-  if (Abc_NtkHasSop( pNtk )) printf("sop\n");
-  else if (Abc_NtkHasBdd( pNtk )) printf("bdd\n");
-  else if (Abc_NtkHasAig( pNtk )) printf("aig\n");
-  else if (Abc_NtkHasMapping( pNtk )) printf("mapped\n");
-  else printf("***unknown***\n");
-
-  printf("\tinitial reg count = %d\n", Abc_NtkLatchNum(pNtk));
+  vprintf("\tnetlist type = ");
+  if (Abc_NtkIsNetlist( pNtk )) { vprintf("netlist/"); }
+  else if (Abc_NtkIsLogic( pNtk )) { vprintf("logic/"); }
+  else if (Abc_NtkIsStrash( pNtk )) { vprintf("strash/"); }
+  else { vprintf("***unknown***/"); }
+  if (Abc_NtkHasSop( pNtk )) { vprintf("sop\n"); }
+  else if (Abc_NtkHasBdd( pNtk )) { vprintf("bdd\n"); }
+  else if (Abc_NtkHasAig( pNtk )) { vprintf("aig\n"); }
+  else if (Abc_NtkHasMapping( pNtk )) { vprintf("mapped\n"); }
+  else { vprintf("***unknown***\n"); }
+
+  vprintf("\tinitial reg count = %d\n", Abc_NtkLatchNum(pNtk));
+  vprintf("\tinitial levels = %d\n", Abc_NtkLevel(pNtk));
 
   // remove bubbles from latch boxes
-  Abc_FlowRetime_PrintInitStateInfo(pNtk);
-  printf("\tpushing bubbles out of latch boxes\n");
+  if (pManMR->fVerbose) Abc_FlowRetime_PrintInitStateInfo(pNtk);
+  vprintf("\tpushing bubbles out of latch boxes\n");
   Abc_NtkForEachLatch( pNtk, pObj, i )
     Abc_FlowRetime_RemoveLatchBubbles(pObj);
-  Abc_FlowRetime_PrintInitStateInfo(pNtk);
+  if (pManMR->fVerbose) Abc_FlowRetime_PrintInitStateInfo(pNtk);
 
   // check for box inputs/outputs
   Abc_NtkForEachLatch( pNtk, pObj, i ) {
@@ -129,100 +141,200 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState_,
     assert(!Abc_ObjFaninC0(pNext));
   }
 
-  nLatches = Abc_NtkLatchNum( pNtk );
-  nNodes = Abc_NtkObjNumMax( pNtk )+1;
+  pManMR->nLatches = Abc_NtkLatchNum( pNtk );
+  pManMR->nNodes = Abc_NtkObjNumMax( pNtk )+1;
    
   // build histogram
-  vSinkDistHist = Vec_IntStart( nNodes*2+10 );
+  pManMR->vSinkDistHist = Vec_IntStart( pManMR->nNodes*2+10 );
+
+  // initialize timing
+  if (maxDelay)
+    Abc_FlowRetime_InitTiming( pNtk );
 
   // create Flow_Data structure
-  pDataArray = (Flow_Data_t *)malloc(sizeof(Flow_Data_t)*nNodes);
-  memset(pDataArray, 0, sizeof(Flow_Data_t)*nNodes);
+  pManMR->pDataArray = ALLOC( Flow_Data_t, pManMR->nNodes );
+  Abc_FlowRetime_ClearFlows( 1 );
   Abc_NtkForEachObj( pNtk, pObj, i )
-    Abc_ObjSetCopy( pObj, (void *)(&pDataArray[i]) );
+    Abc_ObjSetCopy( pObj, (void *)(&pManMR->pDataArray[i]) );
+
+  // main loop!
+  Abc_FlowRetime_MainLoop();
+
+  // clear pCopy field
+  Abc_NtkForEachObj( pNtk, pObj, i ) {
+    Abc_ObjSetCopy( pObj, NULL );
+
+    // if not computing init state, set all latches to DC
+    if (!fComputeInitState && Abc_ObjIsLatch(pObj))
+      Abc_LatchSetInitDc(pObj);
+  }
+
+  // deallocate space
+  FREE( pManMR->pDataArray );
+  if (pManMR->vNodes) Vec_PtrFree(pManMR->vNodes);
+  if (pManMR->vSinkDistHist) Vec_IntFree(pManMR->vSinkDistHist);
+  if (pManMR->maxDelay) Abc_FlowRetime_FreeTiming( pNtk );
+
+  // restrash if necessary
+  if (Abc_NtkIsStrash(pNtk)) {
+    Abc_NtkReassignIds( pNtk );
+    pNtk = Abc_NtkRestrash( pNtk, 1 );
+  }
+  
+  vprintf("\tfinal reg count = %d\n", Abc_NtkLatchNum(pNtk));
+  vprintf("\tfinal levels = %d\n", Abc_NtkLevel(pNtk));
+
+#if defined(DEBUG_CHECK)
+  Abc_NtkDoCheck( pNtk );
+#endif
+
+  // free manager
+  FREE( pManMR );
+
+  return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Main loop.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_MainLoop( ) {
+  Abc_Ntk_t *pNtk = pManMR->pNtk;
+  // Abc_Obj_t *pObj; int i;
+  int last, flow = 0, cut;
 
   // (i) forward retiming loop
-  fIsForward = 1;
+  pManMR->fIsForward = 1;
+  pManMR->iteration = 0;
 
-  if (!fBackwardOnly) do {
-    if (iteration == nMaxIters) break;
+  if (!pManMR->fBackwardOnly) do {
+    if (pManMR->iteration == pManMR->nMaxIters) break;
+    pManMR->subIteration = 0;
 
-    printf("\tforward iteration %d\n", iteration);
+    vprintf("\tforward iteration %d\n", pManMR->iteration);
     last = Abc_NtkLatchNum( pNtk );
 
     Abc_FlowRetime_MarkBlocks( pNtk );
-    flow = Abc_FlowRetime_PushFlows( pNtk );
+
+    if (pManMR->maxDelay) {
+      // timing-constrained loop
+      Abc_FlowRetime_ConstrainConserv( pNtk );
+      while(Abc_FlowRetime_RefineConstraints( )) {
+        pManMR->subIteration++;
+        Abc_FlowRetime_ClearFlows( 0 );
+      }
+    } else {
+      flow = Abc_FlowRetime_PushFlows( pNtk, 1 );
+    }
+
     cut = Abc_FlowRetime_ImplementCut( pNtk );
 
-    // clear all
-    memset(pDataArray, 0, sizeof(Flow_Data_t)*nNodes);    
-    iteration++;
-  } while( flow != last );
+    vprintf("\t\tlevels = %d\n", Abc_NtkLevel(pNtk));
+
+#if 0
+    Abc_NtkForEachObj( pNtk, pObj, i ) pObj->Level = 0;
+
+    Abc_NtkLevel(pNtk);
+    Abc_NtkForEachObj( pNtk, pObj, i )
+      if (pObj->Level > pManMR->maxDelay) {
+        print_node( pObj );
+        Vec_PtrForEachEntry( FTIMEEDGES(pObj), p2,j ) {
+          printf(":%d ", p2->Id);
+        }
+      }
+    Abc_NtkLevelReverse(pNtk);
+    Abc_NtkForEachObj( pNtk, pObj, i )
+      if (pObj->Level > pManMR->maxDelay) {
+        print_node( pObj );
+      }
+#endif
+
+    Abc_FlowRetime_ClearFlows( 1 );
+
+    pManMR->iteration++;
+  } while( cut != last );
 
   // print info about initial states
-  if (fComputeInitState)
+  if (pManMR->fComputeInitState && pManMR->fVerbose)
     Abc_FlowRetime_PrintInitStateInfo( pNtk );
 
   // (ii) backward retiming loop
-  fIsForward = 0;
-  iteration = 0;
+  pManMR->fIsForward = 0;
+  pManMR->iteration = 0;
+
+  if (!pManMR->fForwardOnly) do {
+    // initializability loop
 
-  if (!fForwardOnly) {
-    if (fComputeInitState) {
+    if (pManMR->fComputeInitState) {
       Abc_FlowRetime_SetupBackwardInit( pNtk );
     }
 
     do {
-      if (iteration == nMaxIters) break;
+      if (pManMR->iteration == pManMR->nMaxIters) break;
+      pManMR->subIteration = 0;
 
-      printf("\tbackward iteration %d\n", iteration);
+      vprintf("\tbackward iteration %d\n", pManMR->iteration);
       last = Abc_NtkLatchNum( pNtk );
-      
+
       Abc_FlowRetime_MarkBlocks( pNtk );
-      flow = Abc_FlowRetime_PushFlows( pNtk );
-      cut = Abc_FlowRetime_ImplementCut( pNtk );
       
-      // clear all
-      memset(pDataArray, 0, sizeof(Flow_Data_t)*nNodes);    
-      iteration++;
-
-    } while( flow != last );
-    
-    // compute initial states
-    if (fComputeInitState) {
-      Abc_FlowRetime_SolveBackwardInit( pNtk );
-      Abc_FlowRetime_PrintInitStateInfo( pNtk );
-    }
-  }
-
-  // clear pCopy field
-  Abc_NtkForEachObj( pNtk, pObj, i ) {
-    Abc_ObjSetCopy( pObj, NULL );
+      if (pManMR->maxDelay) {
+        // timing-constrained loop
+        Abc_FlowRetime_ConstrainConserv( pNtk );
+        while(Abc_FlowRetime_RefineConstraints( )) {
+          pManMR->subIteration++;
+          Abc_FlowRetime_ClearFlows( 0 );
+        }
+      } else {
+        flow = Abc_FlowRetime_PushFlows( pNtk, 1 );
+      }
+      
+      cut = Abc_FlowRetime_ImplementCut( pNtk );
 
-    // if not computing init state, set all latches to DC
-    if (!fComputeInitState && Abc_ObjIsLatch(pObj))
-      Abc_LatchSetInitDc(pObj);
-  }
+      vprintf("\t\tlevels = %d\n", Abc_NtkLevelReverse(pNtk));
+      
+#if 0
+    Abc_NtkForEachObj( pNtk, pObj, i ) pObj->Level = 0;
 
-  // restrash if necessary
-  if (Abc_NtkIsStrash(pNtk)) {
-    Abc_NtkReassignIds( pNtk );
-    pNtk = Abc_NtkRestrash( pNtk, 1 );
-  }
-  
-#if defined(DEBUG_CHECK)
-  Abc_NtkDoCheck( pNtk );
+    Abc_NtkLevel(pNtk);
+    Abc_NtkForEachObj( pNtk, pObj, i )
+      if (pObj->Level > pManMR->maxDelay) {
+        print_node( pObj );
+      }
+    Abc_NtkLevelReverse(pNtk);
+    Abc_NtkForEachObj( pNtk, pObj, i )
+      if (pObj->Level > pManMR->maxDelay) {
+        print_node( pObj );
+      }
 #endif
 
-  // deallocate space
-  free(pDataArray);
-  if (vSinkDistHist) Vec_IntFree(vSinkDistHist);
-
-  printf("\tfinal reg count = %d\n", Abc_NtkLatchNum(pNtk));
+      Abc_FlowRetime_ClearFlows( 1 );
 
-  return pNtk;
+      pManMR->iteration++;
+    } while( cut != last );
+    
+    // compute initial states
+    if (!pManMR->fComputeInitState) break;
+
+    if (Abc_FlowRetime_SolveBackwardInit( pNtk )) {
+      if (pManMR->fVerbose) Abc_FlowRetime_PrintInitStateInfo( pNtk );
+      break;
+    } else {
+      if (!pManMR->fGuaranteeInitState) break;
+      Abc_FlowRetime_ConstrainInit( );
+    }
+  } while(1);
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Pushes latch bubbles outside of box.]
@@ -237,8 +349,8 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState_,
 ***********************************************************************/
 void
 Abc_FlowRetime_RemoveLatchBubbles( Abc_Obj_t * pLatch ) {
-  int i, j, k, bubble = 0;
-  Abc_Ntk_t *pNtk = Abc_ObjNtk( pLatch );
+  int bubble = 0;
+  Abc_Ntk_t *pNtk = pManMR->pNtk;
   Abc_Obj_t *pBi, *pBo, *pInv;
       
   pBi = Abc_ObjFanin0(pLatch);
@@ -284,7 +396,7 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) {
   int i;
   Abc_Obj_t *pObj;
 
-  if (fIsForward){
+  if (pManMR->fIsForward){
     // mark the frontier
     Abc_NtkForEachPo( pNtk, pObj, i )
       pObj->fMarkA = 1;
@@ -294,7 +406,7 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) {
       }
     // mark the nodes reachable from the PIs
     Abc_NtkForEachPi( pNtk, pObj, i )
-      Abc_NtkMarkCone_rec( pObj, fIsForward );
+      Abc_NtkMarkCone_rec( pObj, pManMR->fIsForward );
   } else {
     // mark the frontier
     Abc_NtkForEachPi( pNtk, pObj, i )
@@ -305,15 +417,14 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) {
       }
     // mark the nodes reachable from the POs
     Abc_NtkForEachPo( pNtk, pObj, i )
-      Abc_NtkMarkCone_rec( pObj, fIsForward );
+      Abc_NtkMarkCone_rec( pObj, pManMR->fIsForward );
   }
 
   // copy marks
   Abc_NtkForEachObj( pNtk, pObj, i ) {
     if (pObj->fMarkA) {
       pObj->fMarkA = 0;
-      if (!Abc_ObjIsLatch(pObj) && 
-          !Abc_ObjIsPi(pObj))
+      if (!Abc_ObjIsLatch(pObj) /* && !Abc_ObjIsPi(pObj) */ )
         FSET(pObj, BLOCK);
     }
   }
@@ -332,15 +443,17 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) {
 
 ***********************************************************************/
 int
-Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk ) {
+Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk, bool fVerbose ) {
   int i, j, flow = 0, last, srcDist = 0;
   Abc_Obj_t   *pObj, *pObj2;
 
-  fSinkDistTerminate = 0;
+  pManMR->constraintMask |= BLOCK;
+
+  pManMR->fSinkDistTerminate = 0;
   dfsfast_preorder( pNtk );
 
   // (i) fast max-flow computation
-  while(!fSinkDistTerminate && srcDist < MAX_DIST) {
+  while(!pManMR->fSinkDistTerminate && srcDist < MAX_DIST) {
     srcDist = MAX_DIST;
     Abc_NtkForEachLatch( pNtk, pObj, i )
       if (FDATA(pObj)->e_dist)    
@@ -357,7 +470,7 @@ Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk ) {
     }
   }
 
-  printf("\t\tmax-flow1 = %d \t", flow);
+  if (fVerbose) vprintf("\t\tmax-flow1 = %d \t", flow);
 
   // (ii) complete max-flow computation
   // also, marks source-reachable nodes
@@ -375,7 +488,7 @@ Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk ) {
     }
   } while (flow > last);
   
-  printf("max-flow2 = %d\n", flow);
+  if (fVerbose) vprintf("max-flow2 = %d\n", flow);
 
   return flow;
 }
@@ -396,10 +509,9 @@ Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk ) {
 void
 Abc_FlowRetime_FixLatchBoxes( Abc_Ntk_t *pNtk, Vec_Ptr_t *vBoxIns ) {
   int i;
-  Abc_Obj_t *pObj, *pNext, *pBo = NULL, *pBi = NULL;
+  Abc_Obj_t *pObj, *pBo = NULL, *pBi = NULL;
   Vec_Ptr_t *vFreeBi = Vec_PtrAlloc( 100 );
   Vec_Ptr_t *vFreeBo = Vec_PtrAlloc( 100 );
-  Vec_Ptr_t *vNodes;
 
   // 1. remove empty bi/bo pairs
   while(Vec_PtrSize( vBoxIns )) {
@@ -424,10 +536,10 @@ Abc_FlowRetime_FixLatchBoxes( Abc_Ntk_t *pNtk, Vec_Ptr_t *vBoxIns ) {
       Vec_PtrPush( vFreeBo, pBo );
 
       // free names
-      // if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pBi)))
-      //  Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pBi));
-      //if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pBo)))
-      //  Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pBo));
+      if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pBi)))
+        Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pBi));
+      if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pBo)))
+        Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pBo));
 
       // check for complete detachment
       assert(Abc_ObjFaninNum(pBi) == 0);
@@ -512,12 +624,12 @@ Abc_FlowRetime_VerifyPathLatencies( Abc_Ntk_t * pNtk ) {
   Abc_Obj_t *pObj;
   fPathError = 0;
 
-  printf("\t\tVerifying latency along all paths...");
+  vprintf("\t\tVerifying latency along all paths...");
 
   Abc_NtkForEachObj( pNtk, pObj, i ) {
     if (Abc_ObjIsBo(pObj)) {
       Abc_FlowRetime_VerifyPathLatencies_rec( pObj, 0 );
-    } else if (!fIsForward && Abc_ObjIsPi(pObj)) {
+    } else if (!pManMR->fIsForward && Abc_ObjIsPi(pObj)) {
       Abc_FlowRetime_VerifyPathLatencies_rec( pObj, 0 );
     }
 
@@ -531,7 +643,7 @@ Abc_FlowRetime_VerifyPathLatencies( Abc_Ntk_t * pNtk ) {
     }
   }
 
-  printf(" ok\n");
+  vprintf(" ok\n");
 
   Abc_NtkForEachObj( pNtk, pObj, i ) {
     pObj->fMarkA = 0;
@@ -554,20 +666,20 @@ Abc_FlowRetime_VerifyPathLatencies_rec( Abc_Obj_t * pObj, int markD ) {
     if (Abc_ObjIsLatch(pObj))
       markC = 1;      // latch in output
     
-    if (!fIsForward && !Abc_ObjIsPo(pObj) && !Abc_ObjFanoutNum(pObj))
+    if (!pManMR->fIsForward && !Abc_ObjIsPo(pObj) && !Abc_ObjFanoutNum(pObj))
       return -1; // dangling non-PO outputs : don't care what happens
     
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       // reached end of cycle?
       if ( Abc_ObjIsBo(pNext) ||
-           (fIsForward && Abc_ObjIsPo(pNext)) ) {
+           (pManMR->fIsForward && Abc_ObjIsPo(pNext)) ) {
         if (!markD && !Abc_ObjIsLatch(pObj)) {
           printf("\nERROR: no-latch path (end)\n");
           print_node(pNext);
           printf("\n");
           fPathError = 1;
         }
-      } else if (!fIsForward && Abc_ObjIsPo(pNext)) {
+      } else if (!pManMR->fIsForward && Abc_ObjIsPo(pNext)) {
         if (markD || Abc_ObjIsLatch(pObj)) {
           printf("\nERROR: extra-latch path to outputs\n");
           print_node(pNext);
@@ -625,7 +737,7 @@ void
 Abc_FlowRetime_CopyInitState( Abc_Obj_t * pSrc, Abc_Obj_t * pDest ) {
   Abc_Obj_t *pObj;
 
-  if (!fComputeInitState) return;
+  if (!pManMR->fComputeInitState) return;
 
   assert(Abc_ObjIsLatch(pSrc));
   assert(Abc_ObjFanin0(pDest) == pSrc);
@@ -638,7 +750,7 @@ Abc_FlowRetime_CopyInitState( Abc_Obj_t * pSrc, Abc_Obj_t * pDest ) {
     FSET(pDest, INIT_1);  
   }
   
-  if (!fIsForward) {
+  if (!pManMR->fIsForward) {
     pObj = Abc_ObjData(pSrc);
     assert(Abc_ObjIsPi(pObj));
     FDATA(pDest)->pInitObj = pObj;
@@ -684,8 +796,8 @@ Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) {
     Abc_ObjRemoveFanins( pObj );
 
     // free name
-    // if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pObj)))
-    //  Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pObj));
+    if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pObj)))
+      Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pObj));
   }
 
   // insert latches into netlist
@@ -693,33 +805,25 @@ Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) {
     if (Abc_ObjIsLatch( pObj )) continue;
     
     // a latch is required on every node that lies across the min-cit
-    assert(!fIsForward || !FTEST(pObj, VISITED_E) || FTEST(pObj, VISITED_R));
+    assert(!pManMR->fIsForward || !FTEST(pObj, VISITED_E) || FTEST(pObj, VISITED_R));
     if (FTEST(pObj, VISITED_R) && !FTEST(pObj, VISITED_E)) {
       assert(FTEST(pObj, FLOW));
 
       // count size of cut
       cut++;
-      if ((fIsForward && Abc_ObjIsBo(pObj)) || 
-          (!fIsForward && Abc_ObjIsBi(pObj)))
+      if ((pManMR->fIsForward && Abc_ObjIsBo(pObj)) || 
+          (!pManMR->fIsForward && Abc_ObjIsBi(pObj)))
         unmoved++;
       
       // only insert latch between fanouts that lie across min-cut
       // some fanout paths may be cut at deeper points
       Abc_ObjForEachFanout( pObj, pNext, j )
-        if (fIsForward) {
-          if (!FTEST(pNext, VISITED_R) || 
-              FTEST(pNext, BLOCK) || 
-              FTEST(pNext, CROSS_BOUNDARY) || 
-              Abc_ObjIsLatch(pNext))
-            Vec_PtrPush(vMove, pNext);
-        } else {
-          if (FTEST(pNext, VISITED_E) ||
-              FTEST(pNext, CROSS_BOUNDARY))
-            Vec_PtrPush(vMove, pNext);
-        }
+        if (Abc_FlowRetime_IsAcrossCut( pObj, pNext ))
+          Vec_PtrPush(vMove, pNext);
+
+      // check that move-set is non-zero
       if (Vec_PtrSize(vMove) == 0)
         print_node(pObj);
-
       assert(Vec_PtrSize(vMove) > 0);
       
       // insert one of re-useable registers
@@ -757,10 +861,11 @@ Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) {
   Vec_PtrFree( vMove );
   Vec_PtrFree( vBoxIns );
 
-  printf("\t\tmin-cut = %d (unmoved = %d)\n", cut, unmoved);
+  vprintf("\t\tmin-cut = %d (unmoved = %d)\n", cut, unmoved);
   return cut;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Adds dummy fanin.]
@@ -808,13 +913,14 @@ print_node(Abc_Obj_t *pObj) {
   if (pObj->fMarkC)
     strcat(m, "C");
 
-  printf("node %d type=%d (%x%s) fanouts {", Abc_ObjId(pObj), Abc_ObjType(pObj), FDATA(pObj)->mark, m);
+  printf("node %d type=%d lev=%d tedge=%d (%x%s) fanouts {", Abc_ObjId(pObj), Abc_ObjType(pObj),
+         pObj->Level, Vec_PtrSize(FTIMEEDGES(pObj)), FDATA(pObj)->mark, m);
   Abc_ObjForEachFanout( pObj, pNext, i )
-    printf("%d (%d),", Abc_ObjId(pNext), FDATA(pNext)->mark);
+    printf("%d[%d](%d),", Abc_ObjId(pNext), Abc_ObjType(pNext), FDATA(pNext)->mark);
   printf("} fanins {");
   Abc_ObjForEachFanin( pObj, pNext, i )
-    printf("%d (%d),", Abc_ObjId(pNext), FDATA(pNext)->mark);
-  printf("} ");
+    printf("%d[%d](%d),", Abc_ObjId(pNext), Abc_ObjType(pNext), FDATA(pNext)->mark);
+  printf("}\n");
 }
 
 void
@@ -831,7 +937,7 @@ print_node2(Abc_Obj_t *pObj) {
   if (pObj->fMarkC)
     strcat(m, "C");
 
-  printf("node %d type=%d fanouts {", Abc_ObjId(pObj), Abc_ObjType(pObj), m);
+  printf("node %d type=%d %s fanouts {", Abc_ObjId(pObj), Abc_ObjType(pObj), m);
   Abc_ObjForEachFanout( pObj, pNext, i )
     printf("%d ,", Abc_ObjId(pNext));
   printf("} fanins {");
@@ -840,6 +946,33 @@ print_node2(Abc_Obj_t *pObj) {
   printf("} ");
 }
 
+void
+print_node3(Abc_Obj_t *pObj) {
+  int i;
+  Abc_Obj_t * pNext;
+  char m[6];
+
+  m[0] = 0;
+  if (pObj->fMarkA)
+    strcat(m, "A");
+  if (pObj->fMarkB)
+    strcat(m, "B");
+  if (pObj->fMarkC)
+    strcat(m, "C");
+
+  printf("\nnode %d type=%d mark=%d %s\n", Abc_ObjId(pObj), Abc_ObjType(pObj), FDATA(pObj)->mark, m);
+  printf("fanouts\n");
+  Abc_ObjForEachFanout( pObj, pNext, i ) {
+    print_node(pNext);
+    printf("\n");
+  }
+  printf("fanins\n");
+  Abc_ObjForEachFanin( pObj, pNext, i ) {
+    print_node(pNext);
+    printf("\n");
+  }
+}
+
 
 /**Function*************************************************************
 
@@ -862,3 +995,65 @@ Abc_ObjBetterTransferFanout( Abc_Obj_t * pFrom, Abc_Obj_t * pTo, int compl ) {
     Abc_ObjPatchFanin( pNext, pFrom, Abc_ObjNotCond(pTo, compl) );
   }
 }
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns true is a connection spans the min-cut.]
+
+  Description [pNext is a direct fanout of pObj.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool
+Abc_FlowRetime_IsAcrossCut( Abc_Obj_t *pObj, Abc_Obj_t *pNext ) {
+
+  if (FTEST(pObj, VISITED_R) && !FTEST(pObj, VISITED_E)) {
+    if (pManMR->fIsForward) {
+      if (!FTEST(pNext, VISITED_R) || 
+          (FTEST(pNext, BLOCK_OR_CONS) & pManMR->constraintMask)|| 
+          FTEST(pNext, CROSS_BOUNDARY) || 
+          Abc_ObjIsLatch(pNext))
+        return 1;
+    } else {
+      if (FTEST(pNext, VISITED_E) ||
+          FTEST(pNext, CROSS_BOUNDARY))
+        return 1;
+    }
+  }
+  
+  return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Resets flow problem]
+
+  Description [If fClearAll is true, all marks will be cleared; this is
+               typically appropriate after the circuit structure has
+               been modified.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_ClearFlows( bool fClearAll ) {
+  int i;
+
+  if (fClearAll)
+    memset(pManMR->pDataArray, 0, sizeof(Flow_Data_t)*pManMR->nNodes);
+  else {
+    // clear only data related to flow problem
+    for(i=0; i<pManMR->nNodes; i++) {
+      pManMR->pDataArray[i].mark &= ~(VISITED | FLOW );
+      pManMR->pDataArray[i].e_dist = 0;
+      pManMR->pDataArray[i].r_dist = 0;
+      pManMR->pDataArray[i].pred = NULL;
+    }
+  }
+}
diff --git a/src/opt/fret/fretTime.c b/src/opt/fret/fretTime.c
new file mode 100644
index 00000000..f497df60
--- /dev/null
+++ b/src/opt/fret/fretTime.c
@@ -0,0 +1,763 @@
+/**CFile****************************************************************
+
+  FileName    [fretTime.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Flow-based retiming package.]
+
+  Synopsis    [Delay-constrained retiming code.]
+
+  Author      [Aaron Hurst]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2008.]
+
+  Revision    [$Id: fretTime.c,v 1.00 2008/01/01 00:00:00 ahurst Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "vec.h"
+#include "fretime.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_FlowRetime_Dfs_forw( Abc_Obj_t * pObj, Vec_Ptr_t *vNodes );
+static void Abc_FlowRetime_Dfs_back( Abc_Obj_t * pObj, Vec_Ptr_t *vNodes );
+
+static void Abc_FlowRetime_ConstrainExact_forw( Abc_Obj_t * pObj );
+static void Abc_FlowRetime_ConstrainExact_back( Abc_Obj_t * pObj );
+static void Abc_FlowRetime_ConstrainConserv_forw( Abc_Ntk_t * pNtk );
+static void Abc_FlowRetime_ConstrainConserv_back( Abc_Ntk_t * pNtk );
+
+
+void trace2(Abc_Obj_t *pObj) {
+  Abc_Obj_t *pNext;
+  int i;
+
+  print_node(pObj);
+  Abc_ObjForEachFanin(pObj, pNext, i) 
+    if (pNext->Level >= pObj->Level - 1) {
+      trace2(pNext);
+      break;
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Initializes timing]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_InitTiming( Abc_Ntk_t *pNtk ) {
+
+  pManMR->nConservConstraints = pManMR->nExactConstraints = 0;
+
+  pManMR->vExactNodes = Vec_PtrAlloc(1000);
+
+  pManMR->vTimeEdges = ALLOC( Vec_Ptr_t, Abc_NtkObjNumMax(pNtk)+1 );
+  assert(pManMR->vTimeEdges);
+  memset(pManMR->vTimeEdges, 0, (Abc_NtkObjNumMax(pNtk)+1) * sizeof(Vec_Ptr_t) );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Marks nodes with conservative constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_ConstrainConserv( Abc_Ntk_t * pNtk ) {  
+  Abc_Obj_t *pObj;
+  int i;
+  void *pArray;
+
+  // clear all exact constraints
+  pManMR->nExactConstraints = 0;
+  while( Vec_PtrSize( pManMR->vExactNodes )) {
+    pObj = Vec_PtrPop( pManMR->vExactNodes );
+    
+    if ( Vec_PtrSize( FTIMEEDGES(pObj) )) {
+      pArray =  Vec_PtrReleaseArray( FTIMEEDGES(pObj) );
+      FREE( pArray );
+    }
+  }
+
+#if !defined(IGNORE_TIMING)
+  if (pManMR->fIsForward) {
+    Abc_FlowRetime_ConstrainConserv_forw(pNtk);
+  } else {
+    Abc_FlowRetime_ConstrainConserv_back(pNtk);
+  }
+#endif
+
+  Abc_NtkForEachObj( pNtk, pObj, i)
+    assert( !Vec_PtrSize(FTIMEEDGES(pObj)) );
+}
+
+
+void Abc_FlowRetime_ConstrainConserv_forw( Abc_Ntk_t * pNtk ) {
+  Vec_Ptr_t *vNodes = pManMR->vNodes;
+  Abc_Obj_t *pObj, *pNext, *pBi, *pBo;
+  int i, j;
+  
+  assert(!Vec_PtrSize( vNodes ));
+  pManMR->nConservConstraints = 0;
+
+  // 1. hard constraints
+
+  // (i) collect TFO of PIs
+  Abc_NtkIncrementTravId(pNtk);
+  Abc_NtkForEachPi(pNtk, pObj, i)
+    Abc_FlowRetime_Dfs_forw( pObj, vNodes );
+
+  // ... propagate values
+  Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+    pObj->Level = 0;
+    Abc_ObjForEachFanin( pObj, pNext, j )
+    {
+      if ( Abc_NodeIsTravIdCurrent(pNext) &&
+           pObj->Level < pNext->Level )
+        pObj->Level = pNext->Level;
+    }
+    pObj->Level += Abc_ObjIsNode(pObj) ? 1 : 0;
+
+    if ( Abc_ObjIsBi(pObj) )
+      pObj->fMarkA = 1;
+
+    assert(pObj->Level <= pManMR->maxDelay);
+  }
+
+  // collect TFO of latches
+  // seed arrival times from BIs
+  Vec_PtrClear(vNodes);
+  Abc_NtkIncrementTravId(pNtk);
+  Abc_NtkForEachLatch(pNtk, pObj, i) {
+    pBo = Abc_ObjFanout0( pObj );
+    pBi = Abc_ObjFanin0( pObj );
+
+    Abc_NodeSetTravIdCurrent( pObj );
+    Abc_FlowRetime_Dfs_forw( pBo, vNodes );
+
+    if (pBi->fMarkA) {
+      pBi->fMarkA = 0;
+      pObj->Level = pBi->Level;
+      assert(pObj->Level <= pManMR->maxDelay);
+    } else
+      pObj->Level = 0;
+  }
+
+#if defined(DEBUG_CHECK)
+  // DEBUG: check DFS ordering
+  Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+    pObj->fMarkB = 1;
+    
+    Abc_ObjForEachFanin( pObj, pNext, j )
+      if ( Abc_NodeIsTravIdCurrent(pNext) && !Abc_ObjIsLatch(pNext))
+        assert(pNext->fMarkB);
+  }
+  Vec_PtrForEachEntryReverse(vNodes, pObj, i)
+    pObj->fMarkB = 0;
+#endif
+
+  // ... propagate values
+  Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+    pObj->Level = 0;
+    Abc_ObjForEachFanin( pObj, pNext, j )
+    {
+      if ( Abc_NodeIsTravIdCurrent(pNext) &&
+           pObj->Level < pNext->Level )
+        pObj->Level = pNext->Level;
+    }
+    pObj->Level += Abc_ObjIsNode(pObj) ? 1 : 0;
+
+    if (pObj->Level > pManMR->maxDelay) {
+      FSET(pObj, BLOCK);
+    }
+  }
+
+  // 2. conservative constraints
+
+  // first pass: seed latches with T=0
+  Abc_NtkForEachLatch(pNtk, pObj, i) {
+    pObj->Level = 0;
+  }
+
+  // ... propagate values
+  Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+    pObj->Level = 0;
+    Abc_ObjForEachFanin( pObj, pNext, j ) {
+      if ( Abc_NodeIsTravIdCurrent(pNext) &&
+           pObj->Level < pNext->Level )
+        pObj->Level = pNext->Level;
+    }
+    pObj->Level += Abc_ObjIsNode(pObj) ? 1 : 0;
+
+    if ( Abc_ObjIsBi(pObj) )
+      pObj->fMarkA = 1;
+
+    assert(pObj->Level <= pManMR->maxDelay);
+  }
+
+  Abc_NtkForEachLatch(pNtk, pObj, i) {
+    pBo = Abc_ObjFanout0( pObj );
+    pBi = Abc_ObjFanin0( pObj );
+
+    if (pBi->fMarkA) {
+      pBi->fMarkA = 0;
+      pObj->Level = pBi->Level;
+      assert(pObj->Level <= pManMR->maxDelay);
+    } else
+      pObj->Level = 0;
+  }
+
+  // ... propagate values
+  Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+    pObj->Level = 0;
+    Abc_ObjForEachFanin( pObj, pNext, j ) {
+      if ( Abc_NodeIsTravIdCurrent(pNext) &&
+           pObj->Level < pNext->Level )
+        pObj->Level = pNext->Level;
+    }
+    pObj->Level += Abc_ObjIsNode(pObj) ? 1 : 0;
+
+    // constrained?
+    if (pObj->Level > pManMR->maxDelay) {
+      FSET( pObj, CONSERVATIVE );
+      pManMR->nConservConstraints++;
+    } else
+      FUNSET( pObj, CONSERVATIVE );
+  }
+
+  Vec_PtrClear( vNodes );
+}
+
+
+void Abc_FlowRetime_ConstrainConserv_back( Abc_Ntk_t * pNtk ) {
+  Vec_Ptr_t *vNodes = pManMR->vNodes;
+  Abc_Obj_t *pObj, *pNext, *pBi, *pBo;
+  int i, j, l;
+  
+  assert(!Vec_PtrSize(vNodes));
+
+  pManMR->nConservConstraints = 0;
+
+  // 1. hard constraints
+
+  // (i) collect TFO of POs
+  Abc_NtkIncrementTravId(pNtk);
+  Abc_NtkForEachPo(pNtk, pObj, i)
+    Abc_FlowRetime_Dfs_back( pObj, vNodes );
+
+  // ... propagate values
+  Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+    pObj->Level = 0;
+    Abc_ObjForEachFanout( pObj, pNext, j )
+    {
+      l = pNext->Level + (Abc_ObjIsNode(pObj) ? 1 : 0);
+      if ( Abc_NodeIsTravIdCurrent(pNext) &&
+           pObj->Level < l )
+        pObj->Level = l;
+    }
+
+    if ( Abc_ObjIsBo(pObj) )
+      pObj->fMarkA = 1;
+
+    assert(pObj->Level <= pManMR->maxDelay);
+  }
+
+  // collect TFO of latches
+  // seed arrival times from BIs
+  Vec_PtrClear(vNodes);
+  Abc_NtkIncrementTravId(pNtk);
+  Abc_NtkForEachLatch(pNtk, pObj, i) {
+    pBo = Abc_ObjFanout0( pObj );
+    pBi = Abc_ObjFanin0( pObj );
+
+    Abc_NodeSetTravIdCurrent( pObj );
+    Abc_FlowRetime_Dfs_back( pBi, vNodes );
+
+    if (pBo->fMarkA) {
+      pBo->fMarkA = 0;
+      pObj->Level = pBo->Level;
+      assert(pObj->Level <= pManMR->maxDelay);
+    } else
+      pObj->Level = 0;
+  }
+
+#if defined(DEBUG_CHECK)
+  // DEBUG: check DFS ordering
+  Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+    pObj->fMarkB = 1;
+    
+    Abc_ObjForEachFanout( pObj, pNext, j )
+      if ( Abc_NodeIsTravIdCurrent(pNext) && !Abc_ObjIsLatch(pNext))
+        assert(pNext->fMarkB);
+  }
+  Vec_PtrForEachEntryReverse(vNodes, pObj, i)
+    pObj->fMarkB = 0;
+#endif
+
+  // ... propagate values
+  Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+    pObj->Level = 0;
+    Abc_ObjForEachFanout( pObj, pNext, j )
+    {
+      l = pNext->Level + (Abc_ObjIsNode(pObj) ? 1 : 0);
+      if ( Abc_NodeIsTravIdCurrent(pNext) &&
+           pObj->Level < l )
+        pObj->Level = l;
+    }
+
+    if (pObj->Level + (Abc_ObjIsNode(pObj)?1:0) > pManMR->maxDelay) {
+      FSET(pObj, BLOCK);
+    }
+  }
+
+  // 2. conservative constraints
+
+  // first pass: seed latches with T=0
+  Abc_NtkForEachLatch(pNtk, pObj, i) {
+    pObj->Level = 0;
+  }
+
+  // ... propagate values
+  Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+    pObj->Level = 0;
+    Abc_ObjForEachFanout( pObj, pNext, j ) {
+      l = pNext->Level + (Abc_ObjIsNode(pObj) ? 1 : 0);
+      if ( Abc_NodeIsTravIdCurrent(pNext) &&
+           pObj->Level < l )
+        pObj->Level = l;
+    }
+
+    if ( Abc_ObjIsBo(pObj) ) {
+      pObj->fMarkA = 1;
+    }
+         
+    assert(pObj->Level <= pManMR->maxDelay);
+  }
+
+  Abc_NtkForEachLatch(pNtk, pObj, i) {
+    pBo = Abc_ObjFanout0( pObj );
+    assert(Abc_ObjIsBo(pBo));
+    pBi = Abc_ObjFanin0( pObj );
+    assert(Abc_ObjIsBi(pBi));
+
+    if (pBo->fMarkA) {
+      pBo->fMarkA = 0;
+      pObj->Level = pBo->Level;
+    } else
+      pObj->Level = 0;
+  }
+
+  // ... propagate values
+  Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+    pObj->Level = 0;
+    Abc_ObjForEachFanout( pObj, pNext, j ) {
+      l = pNext->Level + (Abc_ObjIsNode(pObj) ? 1 : 0);
+      if ( Abc_NodeIsTravIdCurrent(pNext) &&
+           pObj->Level < l )
+        pObj->Level = l;
+    }
+
+    // constrained?
+    if (pObj->Level > pManMR->maxDelay) {
+      FSET( pObj, CONSERVATIVE );
+      pManMR->nConservConstraints++;
+    } else
+      FUNSET( pObj, CONSERVATIVE );
+  }
+
+  Vec_PtrClear( vNodes );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Introduces exact timing constraints for a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_ConstrainExact( Abc_Obj_t * pObj ) {
+
+  if (FTEST( pObj, CONSERVATIVE )) {
+    pManMR->nConservConstraints--;
+    FUNSET( pObj, CONSERVATIVE );
+  }
+
+#if !defined(IGNORE_TIMING)
+  if (pManMR->fIsForward) {
+    Abc_FlowRetime_ConstrainExact_forw(pObj);
+  } else {
+    Abc_FlowRetime_ConstrainExact_back(pObj);
+  }
+#endif
+}
+
+void Abc_FlowRetime_ConstrainExact_forw_rec( Abc_Obj_t * pObj, Vec_Ptr_t *vNodes, int latch ) {
+  Abc_Obj_t *pNext;
+  int i;
+
+  // terminate?
+  if (Abc_ObjIsLatch(pObj)) {
+    if (latch) return;
+    latch = 1;
+  }
+
+  // already visited?
+  if (!latch) {
+    if (pObj->fMarkA) return;
+    pObj->fMarkA = 1;
+  } else {
+    if (pObj->fMarkB) return;
+    pObj->fMarkB = 1;
+  }
+
+  // recurse
+  Abc_ObjForEachFanin(pObj, pNext, i) {
+    Abc_FlowRetime_ConstrainExact_forw_rec( pNext, vNodes, latch );
+  }
+
+  // add
+  pObj->Level = 0;
+  Vec_PtrPush(vNodes, Abc_ObjNotCond(pObj, latch));
+}
+
+void Abc_FlowRetime_ConstrainExact_forw( Abc_Obj_t * pObj ) {
+  Vec_Ptr_t *vNodes = pManMR->vNodes;
+  Abc_Obj_t *pNext, *pCur, *pReg;
+  // Abc_Ntk_t *pNtk = pManMR->pNtk;
+  int i, j;
+
+  assert( !Vec_PtrSize(vNodes) );
+  assert( !Abc_ObjIsLatch(pObj) );
+  assert( !Vec_PtrSize( FTIMEEDGES(pObj) ));
+  Vec_PtrPush( pManMR->vExactNodes, pObj );
+
+  // rev topo order
+  Abc_FlowRetime_ConstrainExact_forw_rec( pObj, vNodes, 0 );
+
+  Vec_PtrForEachEntryReverse( vNodes, pCur, i) {
+    pReg = Abc_ObjRegular( pCur );
+
+    if (pReg == pCur) {
+      assert(!Abc_ObjIsLatch(pReg));
+      Abc_ObjForEachFanin(pReg, pNext, j)
+        pNext->Level = MAX( pNext->Level, pReg->Level + (Abc_ObjIsNode(pReg)?1:0));
+      assert(pReg->Level <= pManMR->maxDelay);
+      pReg->Level = 0;
+      pReg->fMarkA = pReg->fMarkB = 0;
+    }
+  }
+  Vec_PtrForEachEntryReverse( vNodes, pCur, i) {
+    pReg = Abc_ObjRegular( pCur );
+    if (pReg != pCur) {
+      Abc_ObjForEachFanin(pReg, pNext, j)
+        if (!Abc_ObjIsLatch(pNext))
+          pNext->Level = MAX( pNext->Level, pReg->Level + (Abc_ObjIsNode(pReg)?1:0));
+
+      if (pReg->Level == pManMR->maxDelay) {
+        Vec_PtrPush( FTIMEEDGES(pObj), pReg);
+        pManMR->nExactConstraints++;
+      }
+      pReg->Level = 0;
+      pReg->fMarkA = pReg->fMarkB = 0;
+    }
+  }
+
+  Vec_PtrClear( vNodes );
+}
+
+void Abc_FlowRetime_ConstrainExact_back_rec( Abc_Obj_t * pObj, Vec_Ptr_t *vNodes, int latch ) {
+  Abc_Obj_t *pNext;
+  int i;
+
+  // terminate?
+  if (Abc_ObjIsLatch(pObj)) {
+    if (latch) return;
+    latch = 1;
+  }
+
+  // already visited?
+  if (!latch) {
+    if (pObj->fMarkA) return;
+    pObj->fMarkA = 1;
+  } else {
+    if (pObj->fMarkB) return;
+    pObj->fMarkB = 1;
+  }
+
+  // recurse
+  Abc_ObjForEachFanout(pObj, pNext, i) {
+    Abc_FlowRetime_ConstrainExact_back_rec( pNext, vNodes, latch );
+  }
+
+  // add
+  pObj->Level = 0;
+  Vec_PtrPush(vNodes, Abc_ObjNotCond(pObj, latch));
+}
+
+
+void Abc_FlowRetime_ConstrainExact_back( Abc_Obj_t * pObj ) {
+  Vec_Ptr_t *vNodes = pManMR->vNodes;
+  Abc_Obj_t *pNext, *pCur, *pReg;
+  // Abc_Ntk_t *pNtk = pManMR->pNtk;
+  int i, j;
+
+  assert( !Vec_PtrSize( vNodes ));
+  assert( !Abc_ObjIsLatch(pObj) );
+  assert( !Vec_PtrSize( FTIMEEDGES(pObj) ));
+  Vec_PtrPush( pManMR->vExactNodes, pObj );
+
+  // rev topo order
+  Abc_FlowRetime_ConstrainExact_back_rec( pObj, vNodes, 0 );
+
+  Vec_PtrForEachEntryReverse( vNodes, pCur, i) {
+    pReg = Abc_ObjRegular( pCur );
+
+    if (pReg == pCur) {
+      assert(!Abc_ObjIsLatch(pReg));
+      Abc_ObjForEachFanout(pReg, pNext, j)
+        pNext->Level = MAX( pNext->Level, pReg->Level + (Abc_ObjIsNode(pReg)?1:0));
+      assert(pReg->Level <= pManMR->maxDelay);
+      pReg->Level = 0;
+      pReg->fMarkA = pReg->fMarkB = 0;
+    }
+  }
+  Vec_PtrForEachEntryReverse( vNodes, pCur, i) {
+    pReg = Abc_ObjRegular( pCur );
+    if (pReg != pCur) {
+      Abc_ObjForEachFanout(pReg, pNext, j)
+        if (!Abc_ObjIsLatch(pNext))
+          pNext->Level = MAX( pNext->Level, pReg->Level + (Abc_ObjIsNode(pReg)?1:0));
+
+      if (pReg->Level == pManMR->maxDelay) {
+        Vec_PtrPush( FTIMEEDGES(pObj), pReg);
+        pManMR->nExactConstraints++;
+      }
+      pReg->Level = 0;
+      pReg->fMarkA = pReg->fMarkB = 0;
+    }
+  }
+
+  Vec_PtrClear( vNodes );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Introduces all exact timing constraints in a network]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_ConstrainExactAll( Abc_Ntk_t * pNtk ) {
+  int i;
+  Abc_Obj_t *pObj;
+  void *pArray;
+  
+  // free existing constraints
+  Abc_NtkForEachObj( pNtk, pObj, i )    
+    if ( Vec_PtrSize( FTIMEEDGES(pObj) )) {
+      pArray =  Vec_PtrReleaseArray( FTIMEEDGES(pObj) );
+      FREE( pArray );
+    }
+  pManMR->nExactConstraints = 0;
+  
+  // generate all constraints
+  Abc_NtkForEachObj(pNtk, pObj, i)
+    if (!Abc_ObjIsLatch(pObj) && FTEST( pObj, CONSERVATIVE ) && !FTEST( pObj, BLOCK ))
+      if (!Vec_PtrSize( FTIMEEDGES( pObj ) ))
+        Abc_FlowRetime_ConstrainExact( pObj );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates exact constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_FreeTiming( Abc_Ntk_t *pNtk ) {
+  Abc_Obj_t *pObj;
+  void *pArray;
+
+  while( Vec_PtrSize( pManMR->vExactNodes )) {
+    pObj = Vec_PtrPop( pManMR->vExactNodes );
+    
+    if ( Vec_PtrSize( FTIMEEDGES(pObj) )) {
+      pArray =  Vec_PtrReleaseArray( FTIMEEDGES(pObj) );
+      FREE( pArray );
+    }
+  }
+
+  Vec_PtrFree(pManMR->vExactNodes);
+  FREE( pManMR->vTimeEdges );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_Dfs_forw( Abc_Obj_t * pObj, Vec_Ptr_t *vNodes ) {
+  Abc_Obj_t *pNext;
+  int i;
+
+  if (Abc_ObjIsLatch(pObj)) return;
+
+  Abc_NodeSetTravIdCurrent( pObj );
+  
+  Abc_ObjForEachFanout( pObj, pNext, i )
+    if (!Abc_NodeIsTravIdCurrent( pNext ))
+      Abc_FlowRetime_Dfs_forw( pNext, vNodes );
+
+  Vec_PtrPush( vNodes, pObj );
+}
+
+
+void Abc_FlowRetime_Dfs_back( Abc_Obj_t * pObj, Vec_Ptr_t *vNodes ) {
+  Abc_Obj_t *pNext;
+  int i;
+
+  if (Abc_ObjIsLatch(pObj)) return;
+
+  Abc_NodeSetTravIdCurrent( pObj );
+  
+  Abc_ObjForEachFanin( pObj, pNext, i )
+    if (!Abc_NodeIsTravIdCurrent( pNext ))
+      Abc_FlowRetime_Dfs_back( pNext, vNodes );
+
+  Vec_PtrPush( vNodes, pObj );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Main timing-constrained routine.]
+
+  Description [Refines constraints that are limiting area improvement.
+               These are identified by computing
+               the min-cuts both with and without the conservative
+               constraints: these two situation represent an
+               over- and under-constrained version of the timing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_FlowRetime_RefineConstraints( ) {
+  Abc_Ntk_t *pNtk = pManMR->pNtk;
+  int i, flow, count = 0;
+  Abc_Obj_t *pObj;
+  int maxTighten = 99999;
+
+  vprintf("\t\tsubiter %d : constraints = {cons, exact} = %d, %d\n", 
+         pManMR->subIteration, pManMR->nConservConstraints, pManMR->nExactConstraints);
+
+  // 1. overconstrained
+  pManMR->constraintMask = BLOCK | CONSERVATIVE;
+  vprintf("\t\trefinement: over ");
+  fflush(stdout);
+  flow = Abc_FlowRetime_PushFlows( pNtk, 0 );
+  vprintf("= %d ", flow);
+
+  // remember nodes
+  if (pManMR->fIsForward) {
+    Abc_NtkForEachObj( pNtk, pObj, i )
+      if (!FTEST(pObj, VISITED_R))
+        pObj->fMarkC = 1;
+  } else {
+    Abc_NtkForEachObj( pNtk, pObj, i )
+      if (!FTEST(pObj, VISITED_E))
+        pObj->fMarkC = 1;
+  }
+
+  if (pManMR->fConservTimingOnly) {
+    vprintf(" done\n");
+    return 0;
+  }
+
+  // 2. underconstrained
+  pManMR->constraintMask = BLOCK;
+  Abc_FlowRetime_ClearFlows( 0 );
+  vprintf("under = ");
+  fflush(stdout);
+  flow = Abc_FlowRetime_PushFlows( pNtk, 0 );
+  vprintf("%d refined nodes = ", flow);
+  fflush(stdout);
+
+  // find area-limiting constraints
+  if (pManMR->fIsForward) {
+    Abc_NtkForEachObj( pNtk, pObj, i ) {
+      if (pObj->fMarkC &&
+          FTEST(pObj, VISITED_R) &&
+          FTEST(pObj, CONSERVATIVE) && 
+          count < maxTighten) {
+        count++;
+        Abc_FlowRetime_ConstrainExact( pObj );
+      }
+      pObj->fMarkC = 0;
+    }
+  } else {
+    Abc_NtkForEachObj( pNtk, pObj, i ) {
+      if (pObj->fMarkC &&
+          FTEST(pObj, VISITED_E) &&
+          FTEST(pObj, CONSERVATIVE) &&
+          count < maxTighten) {
+        count++;
+        Abc_FlowRetime_ConstrainExact( pObj );
+      }
+      pObj->fMarkC = 0;
+    }
+  }
+  
+  vprintf("%d\n", count);
+  
+  return (count > 0);
+}
+
+
diff --git a/src/opt/fret/fretime.h b/src/opt/fret/fretime.h
index f12bd30b..167543ce 100644
--- a/src/opt/fret/fretime.h
+++ b/src/opt/fret/fretime.h
@@ -23,7 +23,7 @@
 
 #include "abc.h"
 
-#define IGNORE_TIMING
+// #define IGNORE_TIMING
 // #define DEBUG_PRINT_FLOWS
 // #define DEBUG_VISITED
 // #define DEBUG_PREORDER
@@ -45,49 +45,29 @@
 #define INIT_0          0x20
 #define INIT_1          0x40
 #define INIT_CARE (INIT_0 | INIT_1)
+#define CONSERVATIVE    0x80
+#define BLOCK_OR_CONS (BLOCK | CONSERVATIVE)
 
-typedef struct Untimed_Flow_Data_t_ {
-  unsigned int mark : 8;
+typedef struct Flow_Data_t_ {
+  unsigned int mark : 16;
 
   union {
     Abc_Obj_t   *pred;
     /* unsigned int var; */
     Abc_Obj_t   *pInitObj;
+    Vec_Ptr_t   *vNodes;
   };
 
   unsigned int e_dist : 16;
   unsigned int r_dist : 16;
-} Untimed_Flow_Data_t;
-
-typedef struct Timed_Flow_Data_t_ {
-  unsigned int mark : 8;
-
-  union {
-    Abc_Obj_t   *pred;
-    Vec_Ptr_t   *vTimeInEdges;
-    /* unsigned int var; */
-    Abc_Obj_t   *pInitObj;
-  };
-
-  unsigned int e_dist : 16;
-  unsigned int r_dist : 16;
-
-  Vec_Ptr_t    vTimeEdges;
-
-} Timed_Flow_Data_t;
-
-#if defined(IGNORE_TIMING)
-typedef Untimed_Flow_Data_t Flow_Data_t;
-#else
-typedef Timed_Flow_Data_t Flow_Data_t;
-#endif
+} Flow_Data_t;
 
 // useful macros for manipulating Flow_Data structure...
 #define FDATA( x )     ((Flow_Data_t *)Abc_ObjCopy(x))
 #define FSET( x, y )   ((Flow_Data_t *)Abc_ObjCopy(x))->mark |= y
 #define FUNSET( x, y ) ((Flow_Data_t *)Abc_ObjCopy(x))->mark &= ~y
 #define FTEST( x, y )  (((Flow_Data_t *)Abc_ObjCopy(x))->mark & y)
-#define FTIMEEDGES( x )  &(((Timed_Flow_Data_t *)Abc_ObjCopy(x))->vTimeEdges)
+#define FTIMEEDGES( x )  &(pManMR->vTimeEdges[Abc_ObjId( x )])
 
 static inline void FSETPRED(Abc_Obj_t *pObj, Abc_Obj_t *pPred) {
   assert(!Abc_ObjIsLatch(pObj)); // must preserve field to maintain init state linkage
@@ -97,21 +77,56 @@ static inline Abc_Obj_t * FGETPRED(Abc_Obj_t *pObj) {
   return FDATA(pObj)->pred;
 }
 
+
+typedef struct MinRegMan_t_ {
+ 
+  // problem description:
+  int         maxDelay;
+  bool        fComputeInitState, fGuaranteeInitState;
+  int         nNodes, nLatches;
+  bool        fForwardOnly, fBackwardOnly;
+  bool        fConservTimingOnly;
+  int         nMaxIters;
+  bool        fVerbose;
+  Abc_Ntk_t  *pNtk;
+
+  int         nPreRefine;
+
+  // problem state
+  bool        fIsForward;
+  bool        fSinkDistTerminate;
+  int         nExactConstraints, nConservConstraints;
+  int         fSolutionIsDc;
+  int         constraintMask;
+  int         iteration, subIteration;
+  
+  // problem data
+  Vec_Int_t   *vSinkDistHist;
+  Flow_Data_t *pDataArray;
+  Vec_Ptr_t   *vTimeEdges;
+  Vec_Ptr_t   *vExactNodes;
+  Abc_Ntk_t   *pInitNtk;
+  Vec_Ptr_t   *vNodes; // re-useable struct
+
+} MinRegMan_t ;
+
+#define vprintf if (pManMR->fVerbose) printf 
+
 /*=== fretMain.c ==========================================================*/
+ 
+extern MinRegMan_t *pManMR;
 
 Abc_Ntk_t *    Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
                                       int fForward, int fBackward, int nMaxIters,
-                                      int maxDelay);
+                                      int maxDelay, int fFastButConservative);
 
 void print_node(Abc_Obj_t *pObj);
 
 void Abc_ObjBetterTransferFanout( Abc_Obj_t * pFrom, Abc_Obj_t * pTo, int compl );
 
-extern int         fIsForward;
-extern int         fSinkDistTerminate;
-extern Vec_Int_t  *vSinkDistHist;
-extern int         maxDelayCon;
-extern int         fComputeInitState;
+int  Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk, bool fVerbose );
+bool Abc_FlowRetime_IsAcrossCut( Abc_Obj_t *pCur, Abc_Obj_t *pNext );
+void Abc_FlowRetime_ClearFlows( bool fClearAll );
 
 /*=== fretFlow.c ==========================================================*/
 
@@ -132,9 +147,19 @@ void Abc_FlowRetime_UpdateForwardInit( Abc_Ntk_t * pNtk );
 void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk );
 
 void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk );
-void Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk );
+int  Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk );
+
+void Abc_FlowRetime_ConstrainInit(  );
+
+/*=== fretTime.c ==========================================================*/
+
+void Abc_FlowRetime_InitTiming( Abc_Ntk_t *pNtk );
+void Abc_FlowRetime_FreeTiming( Abc_Ntk_t *pNtk );
+
+bool Abc_FlowRetime_RefineConstraints( );
 
-extern Abc_Ntk_t *pInitNtk;
-extern int        fSolutionIsDc;
+void Abc_FlowRetime_ConstrainConserv( Abc_Ntk_t * pNtk );
+void Abc_FlowRetime_ConstrainExact( Abc_Obj_t * pObj );
+void Abc_FlowRetime_ConstrainExactAll( Abc_Ntk_t * pNtk );
 
 #endif
diff --git a/src/opt/fret/module.make b/src/opt/fret/module.make
index 72fdfec9..fda6a73d 100644
--- a/src/opt/fret/module.make
+++ b/src/opt/fret/module.make
@@ -1,4 +1,5 @@
 SRC +=    src/opt/fret/fretMain.c \
     src/opt/fret/fretFlow.c \
-        src/opt/fret/fretInit.c
+        src/opt/fret/fretInit.c \
+    src/opt/fret/fretTime.c