Merged in sterin/abc (pull request #13)

Restoring Aaron Hurst's "fretime" command

6 files changed, 4409 insertions, 0 deletions

diff --git a/src/opt/fret/fretFlow.c b/src/opt/fret/fretFlow.c
new file mode 100644
index 00000000..c9f70859
--- /dev/null
+++ b/src/opt/fret/fretFlow.c
@@ -0,0 +1,700 @@
+/**CFile****************************************************************
+
+  FileName    [fretFlow.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Flow-based retiming package.]
+
+  Synopsis    [Max-flow computation.]
+
+  Author      [Aaron Hurst]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2008.]
+
+  Revision    [$Id: fretFlow.c,v 1.00 2008/01/01 00:00:00 ahurst Exp $]
+
+***********************************************************************/
+
+#include "fretime.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void dfsfast_e_retreat( Abc_Obj_t *pObj );
+static void dfsfast_r_retreat( Abc_Obj_t *pObj );
+
+#define FDIST(xn, xe, yn, ye) (FDATA(xn)->xe##_dist == (FDATA(yn)->ye##_dist + 1))
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Fast DFS.]
+
+  Description [Uses sink-distance-histogram heuristic.  May not find all
+               flow paths: this occurs in a small number of cases where
+               the flow predecessor points to a non-adjacent node and
+               the distance ordering is perturbed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+void dfsfast_preorder( Abc_Ntk_t *pNtk ) {
+  Abc_Obj_t *pObj, *pNext;
+  Vec_Ptr_t *vTimeIn, *qn = Vec_PtrAlloc(Abc_NtkObjNum(pNtk));
+  Vec_Int_t *qe = Vec_IntAlloc(Abc_NtkObjNum(pNtk));
+  int i, j, d = 0, end;
+  int qpos = 0;
+
+  // create reverse timing edges for backward traversal
+#if !defined(IGNORE_TIMING)
+  if (pManMR->maxDelay) {
+    Abc_NtkForEachObj( pNtk, pObj, i ) {
+      Vec_PtrForEachEntry( Abc_Obj_t *, FTIMEEDGES(pObj), pNext, j ) {
+        vTimeIn = FDATA(pNext)->vNodes;
+        if (!vTimeIn) {
+          vTimeIn = FDATA(pNext)->vNodes = Vec_PtrAlloc(2);
+        }
+        Vec_PtrPush(vTimeIn, pObj);
+      }
+    }
+  }
+#endif
+
+  // clear histogram
+  assert(pManMR->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) || 
+        (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) || 
+               (!pManMR->fIsForward && FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask)) {
+      Vec_PtrPush(qn, pObj);
+      Vec_IntPush(qe, 'e');
+      FDATA(pObj)->e_dist = 1;
+    }
+
+  // until queue is empty...
+  while(qpos < Vec_PtrSize(qn)) {
+    pObj = (Abc_Obj_t *)Vec_PtrEntry(qn, qpos);
+    assert(pObj);
+    end = Vec_IntEntry(qe, qpos);
+    qpos++;
+    
+    if (end == 'r') {
+      d = FDATA(pObj)->r_dist;
+
+      // 1. structural edges
+      if (pManMR->fIsForward) {
+        Abc_ObjForEachFanin( pObj, pNext, i )
+          if (!FDATA(pNext)->e_dist) {
+            FDATA(pNext)->e_dist = d+1;
+            Vec_PtrPush(qn, pNext);
+            Vec_IntPush(qe, 'e');
+          }
+      } else
+        Abc_ObjForEachFanout( pObj, pNext, i )
+          if (!FDATA(pNext)->e_dist) {
+            FDATA(pNext)->e_dist = d+1;
+            Vec_PtrPush(qn, pNext);
+            Vec_IntPush(qe, 'e');
+          }
+
+      if (d == 1) continue;
+
+      // 2. reverse edges (forward retiming only)
+      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 (forward retiming only)
+#if !defined(IGNORE_TIMING)
+        if (pManMR->maxDelay && FDATA(pObj)->vNodes)
+          Vec_PtrForEachEntry(Abc_Obj_t *, 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;
+
+      d = FDATA(pObj)->e_dist;
+
+      // 1. through node
+      if (!FDATA(pObj)->r_dist) {
+        FDATA(pObj)->r_dist = d+1;
+        Vec_PtrPush(qn, pObj);
+        Vec_IntPush(qe, 'r');
+      }
+
+      // 2. reverse edges (backward retiming only)
+      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(Abc_Obj_t *, 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
+      }
+    }
+  }
+ 
+  // free time edges
+#if !defined(IGNORE_TIMING)
+  if (pManMR->maxDelay) {
+    Abc_NtkForEachObj( pNtk, pObj, i ) {
+      vTimeIn = FDATA(pObj)->vNodes;
+      if (vTimeIn) {
+        Vec_PtrFree(vTimeIn);
+        FDATA(pObj)->vNodes = 0;
+      }
+    }
+  }
+#endif
+
+  Abc_NtkForEachObj( pNtk, pObj, i ) {
+    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);
+
+  // deallocate
+  Vec_PtrFree( qn );
+  Vec_IntFree( qe );
+}
+
+int dfsfast_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
+  int i;
+  Abc_Obj_t *pNext;
+  
+  if (pManMR->fSinkDistTerminate) return 0;
+
+  // have we reached the sink?
+  if(FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask ||
+     Abc_ObjIsPi(pObj)) {
+    assert(pPred);
+    assert(!pManMR->fIsForward);
+    return 1;
+  }
+
+  FSET(pObj, VISITED_E);
+
+#ifdef DEBUG_VISITED
+  printf("(%de=%d) ", Abc_ObjId(pObj), FDATA(pObj)->e_dist);
+#endif  
+
+  // 1. structural edges
+  if (pManMR->fIsForward)
+    Abc_ObjForEachFanout( pObj, pNext, i ) {
+      if (!FTEST(pNext, VISITED_R) &&
+          FDIST(pObj, e, pNext, r) &&
+          dfsfast_r(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+        printf("o");
+#endif
+        goto found;
+      }
+    }
+  else
+    Abc_ObjForEachFanin( pObj, pNext, i ) {
+      if (!FTEST(pNext, VISITED_R) &&
+          FDIST(pObj, e, pNext, r) &&
+          dfsfast_r(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+        printf("o");
+#endif
+        goto found;
+      }
+    }  
+  
+  if (Abc_ObjIsLatch(pObj))
+    goto not_found;
+
+  // 2. reverse edges (backward retiming only)
+  if (!pManMR->fIsForward) { 
+    Abc_ObjForEachFanout( pObj, pNext, i ) {
+      if (!FTEST(pNext, VISITED_E) &&
+          FDIST(pObj, e, pNext, e) &&
+          dfsfast_e(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+        printf("i");
+#endif
+        goto found;
+      }
+    }
+
+  // 3. timing edges (backward retiming only)
+#if !defined(IGNORE_TIMING)
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry(Abc_Obj_t *, 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
+  if (FTEST(pObj, FLOW) && 
+      !FTEST(pObj, VISITED_R) &&
+      FDIST(pObj, e, pObj, r) &&
+      dfsfast_r(pObj, FGETPRED(pObj))) {
+
+    FUNSET(pObj, FLOW);
+    FSETPRED(pObj, NULL);
+#ifdef DEBUG_PRINT_FLOWS
+    printf("u");
+#endif
+    goto found;
+  }
+  
+ not_found:
+  FUNSET(pObj, VISITED_E);
+  dfsfast_e_retreat(pObj);
+  return 0;
+  
+ found:
+#ifdef DEBUG_PRINT_FLOWS
+  printf("%d ", Abc_ObjId(pObj));
+#endif 
+  FUNSET(pObj, VISITED_E);
+  return 1;
+}
+
+int dfsfast_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
+  int i;
+  Abc_Obj_t *pNext, *pOldPred;
+
+  if (pManMR->fSinkDistTerminate) return 0;
+
+#ifdef DEBUG_VISITED
+  printf("(%dr=%d) ", Abc_ObjId(pObj), FDATA(pObj)->r_dist);
+#endif  
+
+  // have we reached the sink?
+  if (Abc_ObjIsLatch(pObj) ||
+      (pManMR->fIsForward && Abc_ObjIsPo(pObj)) || 
+      (pManMR->fIsForward && FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask)) {
+    assert(pPred);
+    return 1;
+  }
+
+  FSET(pObj, VISITED_R);
+
+  if (FTEST(pObj, FLOW)) {
+
+    pOldPred = FGETPRED(pObj);
+    if (pOldPred && 
+        !FTEST(pOldPred, VISITED_E) &&
+        FDIST(pObj, r, pOldPred, e) &&
+        dfsfast_e(pOldPred, pOldPred)) {
+
+      FSETPRED(pObj, pPred);
+
+#ifdef DEBUG_PRINT_FLOWS
+      printf("fr");
+#endif
+      goto found;
+    }
+    
+  } else {
+
+    if (!FTEST(pObj, VISITED_E) &&
+        FDIST(pObj, r, pObj, e) &&
+        dfsfast_e(pObj, pObj)) {
+
+      FSET(pObj, FLOW);
+      FSETPRED(pObj, pPred);
+
+#ifdef DEBUG_PRINT_FLOWS
+      printf("f");
+#endif
+      goto found;
+    }
+  }
+ 
+  // 2. reverse edges (forward retiming only)
+  if (pManMR->fIsForward) {
+    Abc_ObjForEachFanin( pObj, pNext, i ) {
+      if (!FTEST(pNext, VISITED_R) &&
+          FDIST(pObj, r, pNext, r) &&
+          !Abc_ObjIsLatch(pNext) &&
+          dfsfast_r(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+        printf("i");
+#endif
+        goto found;
+      }
+    }
+  
+  // 3. timing edges (forward retiming only)
+#if !defined(IGNORE_TIMING)
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry(Abc_Obj_t*, FTIMEEDGES(pObj), pNext, i) {
+        if (!FTEST(pNext, VISITED_R) &&
+            FDIST(pObj, r, pNext, r) &&
+            dfsfast_r(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+          printf("o");
+#endif
+          goto found;
+        }
+      }
+#endif
+  }
+  
+  FUNSET(pObj, VISITED_R);
+  dfsfast_r_retreat(pObj);
+  return 0;
+
+ found:
+#ifdef DEBUG_PRINT_FLOWS
+  printf("%d ", Abc_ObjId(pObj));
+#endif
+  FUNSET(pObj, VISITED_R);
+  return 1;
+}
+
+void
+dfsfast_e_retreat(Abc_Obj_t *pObj) {
+  Abc_Obj_t *pNext;
+  int i, *h;
+  int old_dist = FDATA(pObj)->e_dist;
+  int adj_dist, min_dist = MAX_DIST;
+  
+  // 1. structural edges
+  if (pManMR->fIsForward)
+    Abc_ObjForEachFanout( pObj, pNext, i ) {
+      adj_dist = FDATA(pNext)->r_dist;
+      if (adj_dist) min_dist = MIN(min_dist, adj_dist);
+    }
+  else
+    Abc_ObjForEachFanin( pObj, pNext, i ) {
+      adj_dist = FDATA(pNext)->r_dist;
+      if (adj_dist) min_dist = MIN(min_dist, adj_dist);
+    }
+
+  if (Abc_ObjIsLatch(pObj)) goto update;
+
+  // 2. through
+  if (FTEST(pObj, FLOW)) {
+    adj_dist = FDATA(pObj)->r_dist;
+    if (adj_dist) min_dist = MIN(min_dist, adj_dist);
+  }
+
+  // 3. reverse edges (backward retiming only)
+  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(Abc_Obj_t*, FTIMEEDGES(pObj), pNext, i) {
+        adj_dist = FDATA(pNext)->e_dist;
+        if (adj_dist) min_dist = MIN(min_dist, adj_dist);
+      }
+#endif
+  }
+
+ update:
+  ++min_dist;
+  if (min_dist >= MAX_DIST) min_dist = 0;
+  // printf("[%de=%d->%d] ", Abc_ObjId(pObj), old_dist, min_dist+1);
+  FDATA(pObj)->e_dist = min_dist;
+
+  assert(min_dist < Vec_IntSize(pManMR->vSinkDistHist));
+  h = Vec_IntArray(pManMR->vSinkDistHist);
+  h[old_dist]--;
+  h[min_dist]++;
+  if (!h[old_dist]) {
+    pManMR->fSinkDistTerminate = 1;
+  }
+}
+
+void
+dfsfast_r_retreat(Abc_Obj_t *pObj) {
+  Abc_Obj_t *pNext;
+  int i, *h;
+  int old_dist = FDATA(pObj)->r_dist;
+  int adj_dist, min_dist = MAX_DIST;
+  
+  // 1. through or pred
+  if (FTEST(pObj, FLOW)) {
+    if (FGETPRED(pObj)) {
+      adj_dist = FDATA(FGETPRED(pObj))->e_dist;
+      if (adj_dist) min_dist = MIN(min_dist, adj_dist);
+    }
+  } else {
+    adj_dist = FDATA(pObj)->e_dist;
+    if (adj_dist) min_dist = MIN(min_dist, adj_dist);
+  }
+
+  // 2. reverse edges (forward retiming only)
+  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 (forward retiming only)
+#if !defined(IGNORE_TIMING)
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry(Abc_Obj_t*, 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(pManMR->vSinkDistHist));
+  h = Vec_IntArray(pManMR->vSinkDistHist);
+  h[old_dist]--;
+  h[min_dist]++;
+  if (!h[old_dist]) {
+    pManMR->fSinkDistTerminate = 1;
+  }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Plain DFS.]
+
+  Description [Does not use sink-distance-histogram heuristic.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+int dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
+  int i;
+  Abc_Obj_t *pNext;
+  
+  if (FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask || 
+      Abc_ObjIsPi(pObj)) {
+    assert(pPred);
+    assert(!pManMR->fIsForward);
+    return 1;
+  }
+
+  FSET(pObj, VISITED_E);
+  
+  // printf(" %de\n", Abc_ObjId(pObj));
+  
+  // 1. structural edges
+  if (pManMR->fIsForward)
+    Abc_ObjForEachFanout( pObj, pNext, i ) {
+      if (!FTEST(pNext, VISITED_R) &&
+          dfsplain_r(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+        printf("o");
+#endif
+        goto found;
+      }
+    }
+  else
+    Abc_ObjForEachFanin( pObj, pNext, i ) {
+      if (!FTEST(pNext, VISITED_R) &&
+          dfsplain_r(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+        printf("o");
+#endif
+        goto found;
+      }
+    }
+  
+  if (Abc_ObjIsLatch(pObj))
+    return 0;
+
+  // 2. reverse edges (backward retiming only)
+  if (!pManMR->fIsForward) {
+    Abc_ObjForEachFanout( pObj, pNext, i ) {
+      if (!FTEST(pNext, VISITED_E) &&
+          dfsplain_e(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+        printf("i");
+#endif
+        goto found;
+      }
+    }
+
+  // 3. timing edges (backward retiming only)
+#if !defined(IGNORE_TIMING)
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry(Abc_Obj_t*, FTIMEEDGES(pObj), pNext, i) {
+        if (!FTEST(pNext, VISITED_E) &&
+            dfsplain_e(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+          printf("o");
+#endif
+          goto found;
+        }
+      }
+#endif
+  }
+  
+  // unwind
+  if (FTEST(pObj, FLOW) && 
+      !FTEST(pObj, VISITED_R) &&
+      dfsplain_r(pObj, FGETPRED(pObj))) {
+    FUNSET(pObj, FLOW);
+    FSETPRED(pObj, NULL);
+#ifdef DEBUG_PRINT_FLOWS
+    printf("u");
+#endif
+    goto found;
+  }
+  
+  return 0;
+  
+ found:
+#ifdef DEBUG_PRINT_FLOWS
+  printf("%d ", Abc_ObjId(pObj));
+#endif
+
+  return 1;
+}
+
+int dfsplain_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
+  int i;
+  Abc_Obj_t *pNext, *pOldPred;
+
+  // have we reached the sink?
+  if (Abc_ObjIsLatch(pObj) || 
+      (pManMR->fIsForward && Abc_ObjIsPo(pObj)) || 
+      (pManMR->fIsForward && FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask)) {
+    assert(pPred);
+    return 1;
+  }
+
+  FSET(pObj, VISITED_R);
+
+  // printf(" %dr\n", Abc_ObjId(pObj));
+
+  if (FTEST(pObj, FLOW)) {
+
+    pOldPred = FGETPRED(pObj);
+    if (pOldPred && 
+        !FTEST(pOldPred, VISITED_E) &&
+        dfsplain_e(pOldPred, pOldPred)) {
+
+      FSETPRED(pObj, pPred);
+
+#ifdef DEBUG_PRINT_FLOWS
+      printf("fr");
+#endif
+      goto found;
+    }
+    
+  } else {
+
+    if (!FTEST(pObj, VISITED_E) &&
+        dfsplain_e(pObj, pObj)) {
+
+      FSET(pObj, FLOW);
+      FSETPRED(pObj, pPred);
+
+#ifdef DEBUG_PRINT_FLOWS
+      printf("f");
+#endif
+      goto found;
+    }
+  }
+ 
+  // 2. follow reverse edges
+  if (pManMR->fIsForward) { // forward retiming only
+    Abc_ObjForEachFanin( pObj, pNext, i ) {
+      if (!FTEST(pNext, VISITED_R) &&
+          !Abc_ObjIsLatch(pNext) &&
+          dfsplain_r(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+        printf("i");
+#endif
+        goto found;
+      }
+    }
+  
+  // 3. timing edges (forward only)
+#if !defined(IGNORE_TIMING)
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry(Abc_Obj_t*, FTIMEEDGES(pObj), pNext, i) {
+        if (!FTEST(pNext, VISITED_R) &&
+            dfsplain_r(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+          printf("o");
+#endif
+          goto found;
+        }
+      }
+#endif
+  }
+  
+  return 0;
+
+ found:
+#ifdef DEBUG_PRINT_FLOWS
+  printf("%d ", Abc_ObjId(pObj));
+#endif
+  return 1;
+}
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/fret/fretInit.c b/src/opt/fret/fretInit.c
new file mode 100644
index 00000000..0b3b3aec
--- /dev/null
+++ b/src/opt/fret/fretInit.c
@@ -0,0 +1,1343 @@
+/**CFile****************************************************************
+
+  FileName    [fretInit.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Flow-based retiming package.]
+
+  Synopsis    [Initialization for retiming package.]
+
+  Author      [Aaron Hurst]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2008.]
+
+  Revision    [$Id: fretInit.c,v 1.00 2008/01/01 00:00:00 ahurst Exp $]
+
+***********************************************************************/
+
+#include "fretime.h"
+
+#include "base/io/ioAbc.h"
+#include "map/mio/mio.h"
+#include "aig/hop/hop.h"
+
+#ifdef ABC_USE_CUDD
+#include "bdd/cudd/cuddInt.h"
+#endif
+
+ABC_NAMESPACE_IMPL_START
+
+
+#undef DEBUG_PRINT_INIT_NTK
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION PROTOTYPES                          ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_FlowRetime_UpdateForwardInit_rec( Abc_Obj_t * pObj );
+static void Abc_FlowRetime_VerifyBackwardInit( Abc_Ntk_t * pNtk );
+static void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj );
+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 );
+
+static void Abc_FlowRetime_SetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t *pOrig );
+static void Abc_FlowRetime_GetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t **pOrig, int *lag );
+static void Abc_FlowRetime_ClearInitToOrig( Abc_Obj_t *pInit );
+
+extern void * Abc_FrameReadLibGen();
+
+extern void Abc_NtkMarkCone_rec( Abc_Obj_t * pObj, int fForward );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates initial state information.]
+
+  Description [Assumes latch boxes in original position, latches in
+               new positions.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_InitState( Abc_Ntk_t * pNtk ) {
+
+  if (!pManMR->fComputeInitState) return;
+
+  if (pManMR->fIsForward)
+    Abc_FlowRetime_UpdateForwardInit( pNtk );
+  else {
+    Abc_FlowRetime_UpdateBackwardInit( pNtk );
+  }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints initial state information.]
+
+  Description [Prints distribution of 0,1,and X initial states.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+inline int
+Abc_FlowRetime_ObjFirstNonLatchBox( Abc_Obj_t * pOrigObj, Abc_Obj_t ** pResult ) {
+  int lag = 0;
+  Abc_Ntk_t *pNtk;
+  *pResult = pOrigObj;
+  pNtk = Abc_ObjNtk( pOrigObj );
+
+  Abc_NtkIncrementTravId( pNtk );
+
+  while( Abc_ObjIsBo(*pResult) || Abc_ObjIsLatch(*pResult) || Abc_ObjIsBi(*pResult) ) {
+    assert(Abc_ObjFaninNum(*pResult));
+    *pResult = Abc_ObjFanin0(*pResult);
+    
+    if (Abc_NodeIsTravIdCurrent(*pResult))
+      return -1;
+    Abc_NodeSetTravIdCurrent(*pResult);
+
+    if (Abc_ObjIsLatch(*pResult)) ++lag;
+  }
+
+  return lag;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints initial state information.]
+
+  Description [Prints distribution of 0,1,and X initial states.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_PrintInitStateInfo( Abc_Ntk_t * pNtk ) {
+  int i, n0=0, n1=0, nDC=0, nOther=0;
+  Abc_Obj_t *pLatch;
+
+  Abc_NtkForEachLatch( pNtk, pLatch, i ) {
+    if (Abc_LatchIsInit0(pLatch)) n0++;
+    else if (Abc_LatchIsInit1(pLatch)) n1++;
+    else if (Abc_LatchIsInitDc(pLatch)) nDC++;
+    else nOther++;
+  }     
+
+  printf("\tinitial states {0,1,x} = {%d, %d, %d}", n0, n1, nDC);
+  if (nOther)
+    printf(" + %d UNKNOWN", nOther);
+  printf("\n");
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes initial state after forward retiming.]
+
+  Description [Assumes box outputs in old positions stored w/ init values.
+               Uses three-value simulation to preserve don't cares.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_UpdateForwardInit( Abc_Ntk_t * pNtk ) {
+  Abc_Obj_t *pObj, *pFanin;
+  int i;
+
+  vprintf("\t\tupdating init state\n");
+
+  Abc_NtkIncrementTravId( pNtk );
+
+  Abc_NtkForEachLatch( pNtk, pObj, i ) {
+    pFanin = Abc_ObjFanin0(pObj);
+    Abc_FlowRetime_UpdateForwardInit_rec( pFanin );
+
+    if (FTEST(pFanin, INIT_0))
+      Abc_LatchSetInit0( pObj );
+    else if (FTEST(pFanin, INIT_1))
+      Abc_LatchSetInit1( pObj );
+    else
+      Abc_LatchSetInitDc( pObj );
+  }
+}
+
+void Abc_FlowRetime_UpdateForwardInit_rec( Abc_Obj_t * pObj ) {
+  Abc_Obj_t *pNext;
+  int i;
+
+  assert(!Abc_ObjIsPi(pObj)); // should never reach the inputs
+
+  if (Abc_ObjIsBo(pObj)) return;
+
+  // visited?
+  if (Abc_NodeIsTravIdCurrent(pObj)) return;
+  Abc_NodeSetTravIdCurrent(pObj);
+
+  Abc_ObjForEachFanin( pObj, pNext, i ) {
+    Abc_FlowRetime_UpdateForwardInit_rec( pNext );
+  }
+  
+  Abc_FlowRetime_SimulateNode( pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively evaluates HOP netlist.]
+
+  Description [Exponential.  There aren't enough flags on a HOP node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Abc_FlowRetime_EvalHop_rec( Hop_Man_t *pHop, Hop_Obj_t *pObj, int *f, int *dc ) {
+  int f1, dc1, f2, dc2;
+  Hop_Obj_t *pReg = Hop_Regular(pObj);
+  
+  // const 0
+  if (Hop_ObjIsConst1(pReg)) {
+    *f  = 1;
+    *f ^= (pReg == pObj ? 1 : 0);
+    *dc = 0;
+    return;
+  }
+
+  // PI
+  if (Hop_ObjIsPi(pReg)) {
+    *f  = pReg->fMarkA;
+    *f ^= (pReg == pObj ? 1 : 0);
+    *dc = pReg->fMarkB;
+    return;
+  }
+
+  // PO
+  if (Hop_ObjIsPo(pReg)) {
+    assert( pReg == pObj );
+    Abc_FlowRetime_EvalHop_rec(pHop, Hop_ObjChild0(pReg), f, dc);
+    return;
+  }
+
+  // AND
+  if (Hop_ObjIsAnd(pReg)) {
+    Abc_FlowRetime_EvalHop_rec(pHop, Hop_ObjChild0(pReg), &f1, &dc1);
+    Abc_FlowRetime_EvalHop_rec(pHop, Hop_ObjChild1(pReg), &f2, &dc2);
+
+    *dc = (dc1 & f2) | (dc2 & f1) | (dc1 & dc2);
+    *f  = f1 & f2;
+    *f ^= (pReg == pObj ? 1 : 0);
+    return;
+  }
+
+  assert(0);
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sets initial value flags.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_FlowRetime_SetInitValue( Abc_Obj_t * pObj,
+                                                int val, int dc ) {
+  
+  // store init value
+  FUNSET(pObj, INIT_CARE);
+  if (!dc){
+    if (val) {
+      FSET(pObj, INIT_1);
+    } else {
+      FSET(pObj, INIT_0);
+    }
+  }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Propogates initial state through a logic node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
+  Abc_Ntk_t *pNtk = Abc_ObjNtk(pObj);
+  Abc_Obj_t * pFanin;
+  int i, rAnd, rVar, dcAnd, dcVar;
+#ifdef ABC_USE_CUDD
+  DdManager * dd = pNtk->pManFunc;
+  DdNode *pBdd = pObj->pData, *pVar;
+#endif
+  Hop_Man_t *pHop = pNtk->pManFunc;
+  
+  assert(!Abc_ObjIsLatch(pObj));
+  assert(Abc_ObjRegular(pObj));
+
+  // (i) constant nodes
+  if (Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pObj)) {
+    Abc_FlowRetime_SetInitValue(pObj, 1, 0);
+    return;
+  }
+  if (!Abc_NtkIsStrash( pNtk ) && Abc_ObjIsNode(pObj)) {
+    if (Abc_NodeIsConst0(pObj)) {
+      Abc_FlowRetime_SetInitValue(pObj, 0, 0);
+      return;
+    } else if (Abc_NodeIsConst1(pObj)) {
+      Abc_FlowRetime_SetInitValue(pObj, 1, 0);
+      return;
+    }
+  }
+  
+  // (ii) terminal nodes
+  if (!Abc_ObjIsNode(pObj)) {
+    pFanin = Abc_ObjFanin0(pObj);
+    
+    Abc_FlowRetime_SetInitValue(pObj, 
+         (FTEST(pFanin, INIT_1) ? 1 : 0) ^ pObj->fCompl0, 
+         !FTEST(pFanin, INIT_CARE));    
+    return;
+  }
+
+  // (iii) logic nodes
+
+  // ------ SOP network
+  if ( Abc_NtkHasSop( pNtk )) {
+    Abc_FlowRetime_SimulateSop( pObj, (char *)Abc_ObjData(pObj) );
+    return;
+  }
+#ifdef ABC_USE_CUDD
+  // ------ BDD network
+  else if ( Abc_NtkHasBdd( pNtk )) {
+    assert(dd);
+    assert(pBdd);
+
+    // cofactor for 0,1 inputs
+    // 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))
+          pBdd = Cudd_Cofactor( dd, pBdd, Cudd_Not(pVar) ); 
+        else
+          pBdd = Cudd_Cofactor( dd, pBdd, pVar ); 
+      }
+    }
+
+    // if function has not been reduced to 
+    // a constant, propagate an X
+    rVar = (pBdd == Cudd_ReadOne(dd));
+    dcVar = !Cudd_IsConstant(pBdd);
+    
+    Abc_FlowRetime_SetInitValue(pObj, rVar, dcVar);
+    return;
+  }
+#endif // #ifdef ABC_USE_CUDD
+
+  // ------ AIG logic network
+  else if ( Abc_NtkHasAig( pNtk ) && !Abc_NtkIsStrash( pNtk )) {
+    
+    assert(Abc_ObjIsNode(pObj));
+    assert(pObj->pData);
+    assert(Abc_ObjFaninNum(pObj) <= Hop_ManPiNum(pHop) );
+    
+    // set vals at inputs
+    Abc_ObjForEachFanin(pObj, pFanin, i) {
+      Hop_ManPi(pHop, i)->fMarkA = FTEST(pFanin, INIT_1)?1:0;
+      Hop_ManPi(pHop, i)->fMarkB = FTEST(pFanin, INIT_CARE)?1:0;
+    }
+
+    Abc_FlowRetime_EvalHop_rec( pHop, pObj->pData, &rVar, &dcVar );
+   
+    Abc_FlowRetime_SetInitValue(pObj, rVar, dcVar);
+
+    // clear flags
+    Abc_ObjForEachFanin(pObj, pFanin, i) {
+      Hop_ManPi(pHop, i)->fMarkA = 0;
+      Hop_ManPi(pHop, i)->fMarkB = 0;
+    }
+
+    return;
+  }
+
+  // ------ strashed network
+  else if ( Abc_NtkIsStrash( pNtk )) {
+
+    assert(Abc_ObjType(pObj) == ABC_OBJ_NODE);
+    dcAnd = 0, rAnd = 1;
+    
+    pFanin = Abc_ObjFanin0(pObj);
+    dcAnd |= FTEST(pFanin, INIT_CARE) ? 0 : 1;
+    rVar = FTEST(pFanin, INIT_0) ? 0 : 1;
+    if (pObj->fCompl0) rVar ^= 1; // complimented?
+    rAnd &= rVar;
+    
+    pFanin = Abc_ObjFanin1(pObj);
+    dcAnd |= FTEST(pFanin, INIT_CARE) ? 0 : 1;
+    rVar = FTEST(pFanin, INIT_0) ? 0 : 1;
+    if (pObj->fCompl1) rVar ^= 1; // complimented?
+    rAnd &= rVar;
+    
+    if (!rAnd) dcAnd = 0; /* controlling value */
+    
+    Abc_FlowRetime_SetInitValue(pObj, rAnd, dcAnd);
+    return;
+  }
+
+  // ------ MAPPED network
+  else if ( Abc_NtkHasMapping( pNtk )) {
+    Abc_FlowRetime_SimulateSop( pObj, (char *)Mio_GateReadSop(pObj->pData) );
+    return;
+  }
+
+  assert(0);
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Propogates initial state through a SOP node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_SimulateSop( Abc_Obj_t * pObj, char *pSop ) {
+  Abc_Obj_t * pFanin;
+  char *pCube;
+  int i, j, rAnd, rOr, rVar, dcAnd, dcOr, v;
+
+  assert( pSop && !Abc_SopIsExorType(pSop) );
+      
+  rOr = 0, dcOr = 0;
+
+  i = Abc_SopGetVarNum(pSop);
+  Abc_SopForEachCube( pSop, i, pCube ) {
+    rAnd = 1, dcAnd = 0;
+    Abc_CubeForEachVar( pCube, v, j ) {
+      pFanin = Abc_ObjFanin(pObj, j);
+      if ( v == '0' )
+        rVar = FTEST(pFanin, INIT_0) ? 1 : 0;
+      else if ( v == '1' )
+        rVar = FTEST(pFanin, INIT_1) ? 1 : 0;
+      else
+        continue;
+      
+      if (FTEST(pFanin, INIT_CARE))
+        rAnd &= rVar;
+      else
+        dcAnd = 1;
+    }
+    if (!rAnd) dcAnd = 0; /* controlling value */
+    if (dcAnd) 
+      dcOr = 1;
+    else
+      rOr |= rAnd;
+  }
+  if (rOr) dcOr = 0; /* controlling value */
+  
+  // complement the result if necessary
+  if ( !Abc_SopGetPhase(pSop) )
+    rOr ^= 1;
+      
+  Abc_FlowRetime_SetInitValue(pObj, rOr, dcOr);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets up backward initial state computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
+  Abc_Obj_t *pLatch, *pObj, *pPi;
+  int i;
+  Vec_Ptr_t *vObj = Vec_PtrAlloc(100);
+
+  // create the network used for the initial state computation
+  if (Abc_NtkIsStrash(pNtk)) {
+    pManMR->pInitNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+  } else if (Abc_NtkHasMapping(pNtk))
+    pManMR->pInitNtk = Abc_NtkAlloc( pNtk->ntkType, ABC_FUNC_SOP, 1 );
+  else
+    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( pManMR->pInitNtk );
+
+    // DEBUG
+    // printf("setup : mapping latch %d to PI %d\n", pLatch->Id, pPi->Id);
+
+    // has initial state requirement?
+    if (Abc_LatchIsInit0(pLatch)) {
+      pObj = Abc_NtkCreateNodeInv( pManMR->pInitNtk, pPi );
+      Vec_PtrPush(vObj, pObj);
+    }
+    else if (Abc_LatchIsInit1(pLatch)) {
+      Vec_PtrPush(vObj, pPi);
+    }
+    
+    Abc_ObjSetData( pLatch, pPi );     // if not verifying init state
+    // FDATA(pLatch)->pInitObj = pPi;  // if verifying init state
+  }
+
+  // are there any nodes not DC?
+  if (!Vec_PtrSize(vObj)) {
+    pManMR->fSolutionIsDc = 1;
+    return;
+  } else 
+    pManMR->fSolutionIsDc = 0;
+
+  // mitre output
+
+  // create n-input AND gate
+  pObj = Abc_NtkCreateNodeAnd( pManMR->pInitNtk, vObj );
+
+  Abc_ObjAddFanin( Abc_NtkCreatePo( pManMR->pInitNtk ), pObj );
+
+  Vec_PtrFree( vObj );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Solves backward initial state computation.]
+
+  Description []
+               
+  SideEffects [Sets object copies in init ntk.]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
+  int i;
+  Abc_Obj_t *pObj, *pInitObj;
+  Vec_Ptr_t *vDelete = Vec_PtrAlloc(0);
+  Abc_Ntk_t *pSatNtk;
+  int result;
+
+  assert(pManMR->pInitNtk);
+
+  // is the solution entirely DC's?
+  if (pManMR->fSolutionIsDc) {
+    Vec_PtrFree(vDelete);
+    Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj );
+    vprintf("\tno init state computation: all-don't-care solution\n");
+    return 1;
+  }
+
+  // check that network is combinational
+  Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i ) {
+    assert(!Abc_ObjIsLatch(pObj));
+    assert(!Abc_ObjIsBo(pObj));
+    assert(!Abc_ObjIsBi(pObj));
+  }
+  
+  // delete superfluous nodes
+  while(Vec_PtrSize( vDelete )) {
+    pObj = (Abc_Obj_t *)Vec_PtrPop( vDelete );
+    Abc_NtkDeleteObj( pObj );
+  }
+  Vec_PtrFree(vDelete);
+
+  // do some final cleanup on the network
+  Abc_NtkAddDummyPoNames(pManMR->pInitNtk);
+  Abc_NtkAddDummyPiNames(pManMR->pInitNtk);
+  if (Abc_NtkIsLogic(pManMR->pInitNtk))
+    Abc_NtkCleanup(pManMR->pInitNtk, 0);
+
+#if defined(DEBUG_PRINT_INIT_NTK)
+  Abc_NtkLevelReverse( pManMR->pInitNtk );
+  Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i ) 
+    if (Abc_ObjLevel( pObj ) < 2)
+      Abc_ObjPrint(stdout, pObj);
+#endif
+  
+  vprintf("\tsolving for init state (%d nodes)... ", Abc_NtkObjNum(pManMR->pInitNtk));
+  fflush(stdout);
+#ifdef ABC_USE_CUDD
+  // convert SOPs to BDD
+  if (Abc_NtkHasSop(pManMR->pInitNtk))
+    Abc_NtkSopToBdd( pManMR->pInitNtk );
+  // convert AIGs to BDD
+  if (Abc_NtkHasAig(pManMR->pInitNtk))
+    Abc_NtkAigToBdd( pManMR->pInitNtk );
+#else
+  // convert SOPs to AIG
+  if (Abc_NtkHasSop(pManMR->pInitNtk))
+    Abc_NtkSopToAig( pManMR->pInitNtk );
+#endif
+  pSatNtk = pManMR->pInitNtk;
+  
+  // solve
+  result = Abc_NtkMiterSat( pSatNtk, (ABC_INT64_T)500000, (ABC_INT64_T)50000000, 0, NULL, NULL );
+
+  if (!result) { 
+    vprintf("SUCCESS\n");
+  } else  {    
+    vprintf("FAILURE\n");
+    return 0;
+  }
+
+  // clear initial values, associate PIs to latches
+  Abc_NtkForEachPi( pManMR->pInitNtk, pInitObj, i ) Abc_ObjSetCopy( pInitObj, NULL );
+  Abc_NtkForEachLatch( pNtk, pObj, i ) {
+    pInitObj = Abc_ObjData( pObj );
+    assert( Abc_ObjIsPi( pInitObj ));
+    Abc_ObjSetCopy( pInitObj, pObj );
+    Abc_LatchSetInitNone( pObj );
+
+    // DEBUG
+    // printf("solve : getting latch %d from PI %d\n", pObj->Id, pInitObj->Id);
+  }
+
+  // copy solution from PIs to latches
+  assert(pManMR->pInitNtk->pModel);
+  Abc_NtkForEachPi( pManMR->pInitNtk, pInitObj, i ) {
+    if ((pObj = Abc_ObjCopy( pInitObj ))) {
+      if ( pManMR->pInitNtk->pModel[i] )
+        Abc_LatchSetInit1( pObj );
+      else
+        Abc_LatchSetInit0( pObj );
+    }
+  }
+
+#if defined(DEBUG_CHECK)
+  // check that all latches have initial state
+  Abc_NtkForEachLatch( pNtk, pObj, i ) assert( !Abc_LatchIsInitNone( pObj ) );
+#endif
+
+  return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates backward initial state computation problem.]
+
+  Description [Assumes box outputs in old positions stored w/ init values.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) {
+  Abc_Obj_t *pOrigObj,  *pInitObj;
+  Vec_Ptr_t *vBo = Vec_PtrAlloc(100);
+  Vec_Ptr_t *vPi = Vec_PtrAlloc(100);
+  Abc_Ntk_t *pInitNtk = pManMR-> pInitNtk;
+  Abc_Obj_t *pBuf;
+  int i;
+
+  // remove PIs from network (from BOs)
+  Abc_NtkForEachObj( pNtk, pOrigObj, i )
+    if (Abc_ObjIsBo(pOrigObj)) {
+      pInitObj = FDATA(pOrigObj)->pInitObj;
+      assert(Abc_ObjIsPi(pInitObj));
+
+      // DEBUG
+      // printf("update : freeing PI %d\n", pInitObj->Id);
+      
+      // create a buffer instead
+      pBuf = Abc_NtkCreateNodeBuf( pInitNtk, NULL );
+      Abc_FlowRetime_ClearInitToOrig( pBuf );
+
+      Abc_ObjBetterTransferFanout( pInitObj, pBuf, 0 );
+      FDATA(pOrigObj)->pInitObj = pBuf;
+      pOrigObj->fMarkA = 1;
+
+      Vec_PtrPush(vBo, pOrigObj);
+      Vec_PtrPush(vPi, pInitObj);
+    }
+  
+  // check that PIs are all free
+  Abc_NtkForEachPi( pInitNtk, pInitObj, i) {
+    assert( Abc_ObjFanoutNum( pInitObj ) == 0);
+  }
+
+  // add PIs to to latches
+  Abc_NtkForEachLatch( pNtk, pOrigObj, i ) {
+    assert(Vec_PtrSize(vPi) > 0);
+    pInitObj = Vec_PtrPop(vPi);
+
+    // DEBUG
+    // printf("update : mapping latch %d to PI %d\n", pOrigObj->Id, pInitObj->Id);
+
+    pOrigObj->fMarkA = pOrigObj->fMarkB = 1;
+    FDATA(pOrigObj)->pInitObj = pInitObj;
+    Abc_ObjSetData(pOrigObj, pInitObj);
+  }  
+
+  // recursively build init network
+  Vec_PtrForEachEntry( Abc_Obj_t *, vBo, pOrigObj, i )
+    Abc_FlowRetime_UpdateBackwardInit_rec( pOrigObj );
+  
+  // clear flags
+  Abc_NtkForEachObj( pNtk, pOrigObj, i )
+    pOrigObj->fMarkA = pOrigObj->fMarkB = 0;
+
+  // deallocate
+  Vec_PtrFree( vBo );
+  Vec_PtrFree( vPi );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a corresponding node in the init state network]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t *Abc_FlowRetime_CopyNodeToInitNtk( Abc_Obj_t *pOrigObj ) {
+  Abc_Ntk_t *pNtk = pManMR->pNtk;
+  Abc_Ntk_t *pInitNtk = pManMR->pInitNtk;
+  Abc_Obj_t *pInitObj;
+  void *pData;
+  int fCompl[2];
+
+  assert(pOrigObj);
+
+  // what we do depends on the ntk types of original / init networks...
+  
+  // (0) convert BI/BO nodes to buffers
+  if (Abc_ObjIsBi( pOrigObj ) || Abc_ObjIsBo( pOrigObj ) ) {
+    pInitObj =  Abc_NtkCreateNodeBuf( pInitNtk, NULL );
+    Abc_FlowRetime_ClearInitToOrig( pInitObj );
+    return pInitObj;
+  }
+
+  // (i) strash node -> SOP node
+  if (Abc_NtkIsStrash( pNtk )) {
+
+    if (Abc_AigNodeIsConst( pOrigObj )) {
+      return Abc_NtkCreateNodeConst1( pInitNtk );
+    }
+    if (!Abc_ObjIsNode( pOrigObj )) {
+      assert(Abc_ObjFaninNum(pOrigObj) == 1);
+      pInitObj =  Abc_NtkCreateNodeBuf( pInitNtk, NULL );
+      Abc_FlowRetime_ClearInitToOrig( pInitObj );
+      return pInitObj;
+    }
+
+    assert( Abc_ObjIsNode(pOrigObj) );
+    pInitObj = Abc_NtkCreateObj( pInitNtk, ABC_OBJ_NODE );
+    
+    fCompl[0] = pOrigObj->fCompl0 ? 1 : 0;
+    fCompl[1] = pOrigObj->fCompl1 ? 1 : 0;
+    
+    pData =  Abc_SopCreateAnd( (Mem_Flex_t *)pInitNtk->pManFunc, 2, fCompl );
+    assert(pData);
+    pInitObj->pData = Abc_SopRegister( (Mem_Flex_t *)pInitNtk->pManFunc, pData );
+  } 
+
+  // (ii) mapped node -> SOP node
+  else if (Abc_NtkHasMapping( pNtk )) {
+    if (!pOrigObj->pData) {
+      // assume terminal...
+      assert(Abc_ObjFaninNum(pOrigObj) == 1);
+
+      pInitObj =  Abc_NtkCreateNodeBuf( pInitNtk, NULL );
+      Abc_FlowRetime_ClearInitToOrig( pInitObj );
+      return pInitObj;
+    }
+
+    pInitObj = Abc_NtkCreateObj( pInitNtk, Abc_ObjType(pOrigObj) );
+    pData = Mio_GateReadSop(pOrigObj->pData);
+    assert( Abc_SopGetVarNum(pData) == Abc_ObjFaninNum(pOrigObj) );
+    
+    pInitObj->pData = Abc_SopRegister( (Mem_Flex_t *)pInitNtk->pManFunc, pData );
+  } 
+
+  // (iii) otherwise, duplicate obj
+  else {
+    pInitObj = Abc_NtkDupObj( pInitNtk, pOrigObj, 0 );
+    
+    // copy phase
+    pInitObj->fPhase = pOrigObj->fPhase;
+  }
+
+  assert(pInitObj);
+  return pInitObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates backward initial state computation problem.]
+
+  Description [Creates a duplicate node in the initial state network 
+               corresponding to a node in the original circuit.  If
+               fRecurse is set, the procedure recurses on and connects
+               the new node to its fan-ins.  A latch in the original
+               circuit corresponds to a PI in the initial state network.
+               An existing PI may be supplied by pUseThisPi, and if the
+               node is a latch, it will be used; otherwise the PI is
+               saved in the list vOtherPis and subsequently used for
+               another latch.]
+               
+  SideEffects [Nodes that have a corresponding initial state node
+               are marked with fMarkA.  Nodes that have been fully
+               connected in the initial state network are marked with
+               fMarkB.]
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj) {
+  Abc_Obj_t *pOrigFanin, *pInitFanin, *pInitObj;
+  int i;
+
+  assert(pOrigObj);
+
+  // should never reach primary IOs
+  assert(!Abc_ObjIsPi(pOrigObj));
+  assert(!Abc_ObjIsPo(pOrigObj));
+
+  // skip bias nodes
+  if (FTEST(pOrigObj, BIAS_NODE)) 
+    return NULL;
+
+  // does an init node already exist?
+  if(!pOrigObj->fMarkA) {
+
+    pInitObj = Abc_FlowRetime_CopyNodeToInitNtk( pOrigObj );
+
+    Abc_FlowRetime_SetInitToOrig( pInitObj, pOrigObj );
+    FDATA(pOrigObj)->pInitObj = pInitObj;
+
+    pOrigObj->fMarkA = 1;
+  } else {
+    pInitObj = FDATA(pOrigObj)->pInitObj;
+  }
+  assert(pInitObj);
+    
+  // have we already connected this object?
+  if (!pOrigObj->fMarkB) {
+
+    // create and/or connect fanins
+    Abc_ObjForEachFanin( pOrigObj, pOrigFanin, i ) {
+      // should not reach BOs (i.e. the start of the next frame)
+      // the new latch bounday should lie before it
+      assert(!Abc_ObjIsBo( pOrigFanin ));
+      pInitFanin = Abc_FlowRetime_UpdateBackwardInit_rec( pOrigFanin );
+      Abc_ObjAddFanin( pInitObj, pInitFanin );
+    }
+
+    pOrigObj->fMarkB = 1;
+  }
+
+  return pInitObj;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies backward init state computation.]
+
+  Description [This procedure requires the BOs to store the original
+               latch values and the latches to store the new values:
+               both in the INIT_0 and INIT_1 flags in the Flow_Data
+               structure.  (This is not currently the case in the rest
+               of the code.)  Also, can not verify backward state
+               computations that span multiple combinational frames.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_VerifyBackwardInit( Abc_Ntk_t * pNtk ) {
+  Abc_Obj_t *pObj, *pFanin;
+  int i;
+
+  vprintf("\t\tupdating init state\n");
+
+  Abc_NtkIncrementTravId( pNtk );
+
+  Abc_NtkForEachObj( pNtk, pObj, i )
+    if (Abc_ObjIsBo( pObj )) {
+      pFanin = Abc_ObjFanin0(pObj);
+      Abc_FlowRetime_VerifyBackwardInit_rec( pFanin );
+
+      if (FTEST(pObj, INIT_CARE)) {
+        if(FTEST(pObj, INIT_CARE) != FTEST(pFanin, INIT_CARE)) {
+          printf("ERROR: expected val=%d care=%d and got val=%d care=%d\n",
+                 FTEST(pObj, INIT_1)?1:0, FTEST(pObj, INIT_CARE)?1:0, 
+                 FTEST(pFanin, INIT_1)?1:0, FTEST(pFanin, INIT_CARE)?1:0 );
+
+        }
+      }
+    }
+}
+
+void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj ) {
+  Abc_Obj_t *pNext;
+  int i;
+
+  assert(!Abc_ObjIsBo(pObj)); // should never reach the inputs
+  assert(!Abc_ObjIsPi(pObj)); // should never reach the inputs
+
+  // visited?
+  if (Abc_NodeIsTravIdCurrent(pObj)) return;
+  Abc_NodeSetTravIdCurrent(pObj);
+
+  if (Abc_ObjIsLatch(pObj)) {
+    FUNSET(pObj, INIT_CARE);
+    if (Abc_LatchIsInit0(pObj))
+      FSET(pObj, INIT_0);
+    else if (Abc_LatchIsInit1(pObj))
+      FSET(pObj, INIT_1);
+    return;
+  }
+
+  Abc_ObjForEachFanin( pObj, pNext, i ) {
+    Abc_FlowRetime_VerifyBackwardInit_rec( pNext );
+  }
+  
+  Abc_FlowRetime_SimulateNode( pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constrains backward retiming for initializability.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_FlowRetime_PartialSat(Vec_Ptr_t *vNodes, int cut) {
+  Abc_Ntk_t *pPartNtk, *pInitNtk = pManMR->pInitNtk;
+  Abc_Obj_t *pObj, *pNext, *pPartObj, *pPartNext, *pPo;
+  int i, j, result;
+
+  assert( Abc_NtkPoNum( pInitNtk ) == 1 );
+
+  pPartNtk = Abc_NtkAlloc( pInitNtk->ntkType, pInitNtk->ntkFunc, 0 );
+
+  // copy network
+  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) {
+    pObj->Level = i;
+    assert(!Abc_ObjIsPo( pObj ));
+
+    if (i < cut && !pObj->fMarkA) {
+      pPartObj = Abc_NtkCreatePi( pPartNtk );
+      Abc_ObjSetCopy( pObj, pPartObj );
+    } else {
+      // copy node
+      pPartObj = Abc_NtkDupObj( pPartNtk, pObj, 0 );
+      // copy complementation
+      pPartObj->fPhase = pObj->fPhase;
+   
+      // connect fanins
+      Abc_ObjForEachFanin( pObj, pNext, j ) {   
+        pPartNext = Abc_ObjCopy( pNext );
+        assert(pPartNext);
+        Abc_ObjAddFanin( pPartObj, pPartNext );
+      }
+    }
+
+    assert(pObj->pCopy == pPartObj);
+  }
+  
+  // create PO
+  pPo = Abc_NtkCreatePo( pPartNtk );
+  pNext = Abc_ObjFanin0( Abc_NtkPo( pInitNtk, 0 ) );
+  pPartNext = Abc_ObjCopy( pNext );
+  assert( pPartNext );
+  Abc_ObjAddFanin( pPo, pPartNext );
+  
+  // check network
+#if defined(DEBUG_CHECK)
+  Abc_NtkAddDummyPoNames(pPartNtk);
+  Abc_NtkAddDummyPiNames(pPartNtk);
+  Abc_NtkCheck( pPartNtk );
+#endif
+
+  result = Abc_NtkMiterSat( pPartNtk, (ABC_INT64_T)500000, (ABC_INT64_T)50000000, 0, NULL, NULL );
+
+  Abc_NtkDelete( pPartNtk );
+ 
+  return !result;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Constrains backward retiming for initializability.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_ConstrainInit( ) {
+  Vec_Ptr_t *vNodes;
+  int low, high, mid;
+  int i, n, lag;
+  Abc_Obj_t *pObj = NULL, *pOrigObj;
+  InitConstraint_t *pConstraint = ABC_ALLOC( InitConstraint_t, 1 );
+
+  memset( pConstraint, 0, sizeof(InitConstraint_t) );
+
+  assert(pManMR->pInitNtk);
+
+  vprintf("\tsearch for initial state conflict...\n");
+
+  vNodes = Abc_NtkDfs(pManMR->pInitNtk, 0);
+  n = Vec_PtrSize(vNodes);
+  // also add PIs to vNodes
+  Abc_NtkForEachPi(pManMR->pInitNtk, pObj, i) 
+    Vec_PtrPush(vNodes, pObj);
+  Vec_PtrReorder(vNodes, n);
+
+#if defined(DEBUG_CHECK)
+    assert(!Abc_FlowRetime_PartialSat( vNodes, 0 ));
+#endif
+
+  // grow initialization constraint
+  do {
+    vprintf("\t\t");
+
+    // find element to add to set...
+    low = 0, high = Vec_PtrSize(vNodes);
+    while (low != high-1) {
+      mid = (low + high) >> 1;
+      
+      if (!Abc_FlowRetime_PartialSat( vNodes, mid )) {
+        low = mid;
+        vprintf("-");
+      } else {
+        high = mid;
+        vprintf("*");
+      }
+      fflush(stdout);
+    }
+      
+#if defined(DEBUG_CHECK)
+    assert(Abc_FlowRetime_PartialSat( vNodes, high ));
+    assert(!Abc_FlowRetime_PartialSat( vNodes, low ));
+#endif
+    
+    // mark its TFO
+    pObj = Vec_PtrEntry( vNodes, low );
+    Abc_NtkMarkCone_rec( pObj, 1 );
+    vprintf("   conflict term = %d ", low);
+
+#if 0
+    printf("init ------\n");
+    Abc_ObjPrint(stdout, pObj);
+    printf("\n");
+    Abc_ObjPrintNeighborhood( pObj, 1 );
+    printf("------\n");
+#endif
+
+    // add node to constraint
+    Abc_FlowRetime_GetInitToOrig( pObj, &pOrigObj, &lag );
+    assert(pOrigObj);
+    vprintf(" <=> %d/%d\n", Abc_ObjId(pOrigObj), lag);
+
+#if 0    
+    printf("orig ------\n");
+    Abc_ObjPrint(stdout, pOrigObj);
+    printf("\n");
+    Abc_ObjPrintNeighborhood( pOrigObj, 1 );
+    printf("------\n");
+#endif
+    Vec_IntPush( &pConstraint->vNodes, Abc_ObjId(pOrigObj) );
+    Vec_IntPush( &pConstraint->vLags, lag );
+
+  } while (Abc_FlowRetime_PartialSat( vNodes, Vec_PtrSize(vNodes) ));
+
+  pConstraint->pBiasNode = NULL;
+
+  // add constraint
+  Vec_PtrPush( pManMR->vInitConstraints, pConstraint );
+
+  // clear marks
+  Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i)
+    pObj->fMarkA = 0;
+
+  // free
+  Vec_PtrFree( vNodes );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Removes nodes to bias against uninitializable cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_RemoveInitBias( ) {
+  // Abc_Ntk_t *pNtk = pManMR->pNtk;
+  Abc_Obj_t *pBiasNode;
+  InitConstraint_t *pConstraint;
+  int i;
+
+  Vec_PtrForEachEntry( InitConstraint_t *, pManMR->vInitConstraints, pConstraint, i ) {
+    pBiasNode = pConstraint->pBiasNode;
+    pConstraint->pBiasNode = NULL;
+
+    if (pBiasNode)
+      Abc_NtkDeleteObj(pBiasNode);
+  }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Connects the bias node to one of the constraint vertices.]
+
+  Description [ACK!
+               Currently this is dumb dumb hack.
+               What should we do with biases that belong on BOs?  These
+               move through the circuit.
+               Currently, the bias gets marked on the fan-in of BO
+               and the bias gets implemented on every BO fan-out of a
+               node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Abc_FlowRetime_ConnectBiasNode(Abc_Obj_t *pBiasNode, Abc_Obj_t *pObj, int biasLag) {
+  Abc_Obj_t *pCur, *pNext;
+  int i;
+  int lag;
+  Vec_Ptr_t *vNodes = Vec_PtrAlloc(1);
+  Vec_Int_t *vLags = Vec_IntAlloc(1);
+  Abc_Ntk_t *pNtk = Abc_ObjNtk( pObj );
+  
+  Vec_PtrPush( vNodes, pObj );
+  Vec_IntPush( vLags, 0 );
+
+  Abc_NtkIncrementTravId( pNtk );
+
+  while (Vec_PtrSize( vNodes )) {
+    pCur = Vec_PtrPop( vNodes );
+    lag = Vec_IntPop( vLags );
+
+    if (Abc_NodeIsTravIdCurrent( pCur )) continue;
+    Abc_NodeSetTravIdCurrent( pCur );
+
+    if (!Abc_ObjIsLatch(pCur) &&
+        !Abc_ObjIsBo(pCur) &&
+        Abc_FlowRetime_GetLag(pObj)+lag == biasLag ) {
+
+      // printf("biasing : ");
+      // Abc_ObjPrint(stdout,  pCur );
+#if 1
+      FSET( pCur, BLOCK );
+#else
+      Abc_ObjAddFanin( pCur, pBiasNode );
+#endif
+    }
+
+    Abc_ObjForEachFanout( pCur, pNext, i ) {
+      if (Abc_ObjIsBi(pNext) ||
+          Abc_ObjIsLatch(pNext) ||
+          Abc_ObjIsBo(pNext) ||
+          Abc_ObjIsBo(pCur)) {
+        Vec_PtrPush( vNodes, pNext );
+        Vec_IntPush( vLags, lag - Abc_ObjIsLatch(pNext) ? 1 : 0 );
+      }
+    }
+  }
+
+  Vec_PtrFree( vNodes );
+  Vec_IntFree( vLags );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds nodes to bias against uninitializable cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_AddInitBias( ) {
+  Abc_Ntk_t *pNtk = pManMR->pNtk;
+  Abc_Obj_t *pBiasNode, *pObj;
+  InitConstraint_t *pConstraint;
+  int i, j, id;
+  const int nConstraints = Vec_PtrSize( pManMR->vInitConstraints );
+
+  pManMR->pDataArray = ABC_REALLOC( Flow_Data_t, pManMR->pDataArray, pManMR->nNodes + (nConstraints*(pManMR->iteration+1)) );
+  memset(pManMR->pDataArray + pManMR->nNodes, 0, sizeof(Flow_Data_t)*(nConstraints*(pManMR->iteration+1)));
+
+  vprintf("\t\tcreating %d bias structures\n", nConstraints);
+
+  Vec_PtrForEachEntry(InitConstraint_t*, pManMR->vInitConstraints, pConstraint, i ) {
+    if (pConstraint->pBiasNode) continue;
+    
+ //   printf("\t\t\tbias %d...\n", i);
+    pBiasNode = Abc_NtkCreateBlackbox( pNtk );
+
+    Vec_IntForEachEntry( &pConstraint->vNodes, id, j ) {
+      pObj = Abc_NtkObj(pNtk, id);
+      Abc_FlowRetime_ConnectBiasNode(pBiasNode, pObj, Vec_IntEntry(&pConstraint->vLags, j));
+    }
+
+    // pConstraint->pBiasNode = pBiasNode;
+  }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Clears mapping from init node to original node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_ClearInitToOrig( Abc_Obj_t *pInit )
+{
+  int id = Abc_ObjId( pInit );
+  
+  // grow data structure if necessary
+  if (id >= pManMR->sizeInitToOrig) {
+    int oldSize = pManMR->sizeInitToOrig;
+    pManMR->sizeInitToOrig = 1.5*id + 10;
+    pManMR->pInitToOrig = realloc(pManMR->pInitToOrig, sizeof(NodeLag_t)*pManMR->sizeInitToOrig);
+    memset( &(pManMR->pInitToOrig[oldSize]), 0, sizeof(NodeLag_t)*(pManMR->sizeInitToOrig-oldSize) );
+  }
+  assert( pManMR->pInitToOrig );
+
+  pManMR->pInitToOrig[id].id = -1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sets mapping from init node to original node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_SetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t *pOrig)
+{
+  int lag;
+  int id = Abc_ObjId( pInit );
+  
+  // grow data structure if necessary
+  if (id >= pManMR->sizeInitToOrig) {
+    int oldSize = pManMR->sizeInitToOrig;
+    pManMR->sizeInitToOrig = 1.5*id + 10;
+    pManMR->pInitToOrig = realloc(pManMR->pInitToOrig, sizeof(NodeLag_t)*pManMR->sizeInitToOrig);
+    memset( &(pManMR->pInitToOrig[oldSize]), 0, sizeof(NodeLag_t)*(pManMR->sizeInitToOrig-oldSize) );
+  }
+  assert( pManMR->pInitToOrig );
+
+  // ignore BI, BO, and latch nodes
+  if (Abc_ObjIsBo(pOrig) || Abc_ObjIsBi(pOrig) || Abc_ObjIsLatch(pOrig)) {
+    Abc_FlowRetime_ClearInitToOrig(pInit);
+    return;
+  }
+
+  // move out of latch boxes
+  lag = Abc_FlowRetime_ObjFirstNonLatchBox(pOrig, &pOrig);
+
+  pManMR->pInitToOrig[id].id = Abc_ObjId(pOrig);
+  pManMR->pInitToOrig[id].lag = Abc_FlowRetime_GetLag(pOrig) + lag;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Gets mapping from init node to original node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_GetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t **pOrig, int *lag ) {
+
+  int id = Abc_ObjId( pInit );
+  int origId;
+
+  assert(id < pManMR->sizeInitToOrig);
+
+  origId = pManMR->pInitToOrig[id].id;
+
+  if (origId < 0) {
+    assert(Abc_ObjFaninNum(pInit));
+    Abc_FlowRetime_GetInitToOrig( Abc_ObjFanin0(pInit), pOrig, lag);
+    return;
+  }
+
+  *pOrig = Abc_NtkObj(pManMR->pNtk, origId);
+  *lag = pManMR->pInitToOrig[id].lag;
+}
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/fret/fretMain.c b/src/opt/fret/fretMain.c
new file mode 100644
index 00000000..847476aa
--- /dev/null
+++ b/src/opt/fret/fretMain.c
@@ -0,0 +1,1383 @@
+/**CFile****************************************************************
+
+  FileName    [fretMain.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Flow-based retiming package.]
+
+  Synopsis    [Main file for retiming package.]
+
+  Author      [Aaron Hurst]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2008.]
+
+  Revision    [$Id: fretMain.c,v 1.00 2008/01/01 00:00:00 ahurst Exp $]
+
+***********************************************************************/
+
+#include "fretime.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_FlowRetime_AddDummyFanin( Abc_Obj_t * pObj );
+
+static Abc_Ntk_t* 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_ImplementCut( Abc_Ntk_t * pNtk );
+static void  Abc_FlowRetime_RemoveLatchBubbles( Abc_Obj_t * pLatch );
+
+static Abc_Ntk_t* Abc_FlowRetime_NtkDup( Abc_Ntk_t * pNtk );
+
+static void Abc_FlowRetime_VerifyPathLatencies( Abc_Ntk_t * pNtk );
+static int  Abc_FlowRetime_VerifyPathLatencies_rec( Abc_Obj_t * pObj, int markD );
+
+static void Abc_FlowRetime_UpdateLags_forw_rec( Abc_Obj_t *pObj );
+static void Abc_FlowRetime_UpdateLags_back_rec( Abc_Obj_t *pObj );
+
+extern void Abc_NtkMarkCone_rec( Abc_Obj_t * pObj, int fForward );
+
+void
+print_node3(Abc_Obj_t *pObj);
+
+MinRegMan_t *pManMR;
+
+int          fPathError = 0;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs minimum-register retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t *
+Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, 
+                       int fComputeInitState, int fGuaranteeInitState, int fBlockConst,
+                       int fForwardOnly, int fBackwardOnly, int nMaxIters,
+                       int maxDelay, int fFastButConservative ) {
+
+  int i;
+  Abc_Obj_t   *pObj, *pNext;
+  InitConstraint_t *pData;
+
+  // create manager
+  pManMR = ABC_ALLOC( MinRegMan_t, 1 );
+
+  pManMR->pNtk = pNtk;
+  pManMR->fVerbose = fVerbose;
+  pManMR->fComputeInitState = fComputeInitState;
+  pManMR->fGuaranteeInitState = fGuaranteeInitState;
+  pManMR->fBlockConst = fBlockConst;
+  pManMR->fForwardOnly = fForwardOnly;
+  pManMR->fBackwardOnly = fBackwardOnly;
+  pManMR->nMaxIters = nMaxIters;
+  pManMR->maxDelay = maxDelay;
+  pManMR->fComputeInitState = fComputeInitState;
+  pManMR->fConservTimingOnly = fFastButConservative;
+  pManMR->vNodes = Vec_PtrAlloc(100);
+  pManMR->vInitConstraints = Vec_PtrAlloc(2);
+  pManMR->pInitNtk = NULL;
+  pManMR->pInitToOrig = NULL;
+  pManMR->sizeInitToOrig = 0;
+
+  vprintf("Flow-based minimum-register retiming...\n");  
+
+  if (!Abc_NtkHasOnlyLatchBoxes(pNtk)) {
+    printf("\tERROR: Can not retime with black/white boxes\n");
+    return pNtk;
+  }
+
+  if (maxDelay) {
+    vprintf("\tmax delay constraint = %d\n", maxDelay);
+    if (maxDelay < (i = Abc_NtkLevel(pNtk))) {
+      printf("ERROR: max delay constraint (%d) must be > current max delay (%d)\n", maxDelay, i);
+      return pNtk;
+    }
+  }
+
+  // print info about type of network
+  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
+  if (pManMR->fVerbose) Abc_FlowRetime_PrintInitStateInfo(pNtk);
+  vprintf("\tpushing bubbles out of latch boxes\n");
+  Abc_NtkForEachLatch( pNtk, pObj, i )
+    Abc_FlowRetime_RemoveLatchBubbles(pObj);
+  if (pManMR->fVerbose) Abc_FlowRetime_PrintInitStateInfo(pNtk);
+
+  // check for box inputs/outputs
+  Abc_NtkForEachLatch( pNtk, pObj, i ) {
+    assert(Abc_ObjFaninNum(pObj) == 1);
+    assert(Abc_ObjFanoutNum(pObj) == 1);
+    assert(!Abc_ObjFaninC0(pObj));
+
+    pNext = Abc_ObjFanin0(pObj);
+    assert(Abc_ObjIsBi(pNext));
+    assert(Abc_ObjFaninNum(pNext) <= 1);
+    if(Abc_ObjFaninNum(pNext) == 0) // every Bi should have a fanin
+      Abc_FlowRetime_AddDummyFanin( pNext );
+ 
+    pNext = Abc_ObjFanout0(pObj);
+    assert(Abc_ObjIsBo(pNext));
+    assert(Abc_ObjFaninNum(pNext) == 1);
+    assert(!Abc_ObjFaninC0(pNext));
+  }
+
+  pManMR->nLatches = Abc_NtkLatchNum( pNtk );
+  pManMR->nNodes = Abc_NtkObjNumMax( pNtk )+1;
+   
+  // build histogram
+  pManMR->vSinkDistHist = Vec_IntStart( pManMR->nNodes*2+10 );
+
+  // initialize timing
+  if (maxDelay)
+    Abc_FlowRetime_InitTiming( pNtk );
+
+  // create lag and Flow_Data structure
+  pManMR->vLags = Vec_IntStart(pManMR->nNodes);
+  memset(pManMR->vLags->pArray, 0, sizeof(int)*pManMR->nNodes);
+
+  pManMR->pDataArray = ABC_ALLOC( Flow_Data_t, pManMR->nNodes );
+  Abc_FlowRetime_ClearFlows( 1 );
+
+  // main loop!
+  pNtk = Abc_FlowRetime_MainLoop();
+
+  // cleanup node fields
+  Abc_NtkForEachObj( pNtk, pObj, i ) {
+    // if not computing init state, set all latches to DC
+    if (!fComputeInitState && Abc_ObjIsLatch(pObj))
+      Abc_LatchSetInitDc(pObj);
+  }
+
+  // deallocate space
+  ABC_FREE( pManMR->pDataArray );
+  if (pManMR->pInitToOrig) ABC_FREE( pManMR->pInitToOrig );
+  if (pManMR->vNodes) Vec_PtrFree(pManMR->vNodes);
+  if (pManMR->vLags) Vec_IntFree(pManMR->vLags);
+  if (pManMR->vSinkDistHist) Vec_IntFree(pManMR->vSinkDistHist);
+  if (pManMR->maxDelay) Abc_FlowRetime_FreeTiming( pNtk );
+  while( Vec_PtrSize( pManMR->vInitConstraints )) {
+    pData = Vec_PtrPop( pManMR->vInitConstraints );
+    //assert( pData->pBiasNode );
+    //Abc_NtkDeleteObj( pData->pBiasNode );
+    ABC_FREE( pData->vNodes.pArray );
+    ABC_FREE( pData );
+  }
+  ABC_FREE( pManMR->vInitConstraints );
+
+  // restrash if necessary
+  if (Abc_NtkIsStrash(pNtk)) {
+    Abc_NtkReassignIds( pNtk );
+    pNtk = Abc_FlowRetime_NtkSilentRestrash( 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
+  ABC_FREE( pManMR );
+
+  return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Main loop.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t *
+Abc_FlowRetime_MainLoop( ) {
+  Abc_Ntk_t *pNtk = pManMR->pNtk, *pNtkCopy = pNtk;
+  Abc_Obj_t *pObj; int i;
+  int last, flow = 0, cut;
+
+  // (i) forward retiming loop
+  pManMR->fIsForward = 1;
+  pManMR->iteration = 0;
+
+  if (!pManMR->fBackwardOnly) do {
+    if (pManMR->iteration == pManMR->nMaxIters) break;
+    pManMR->subIteration = 0;
+
+    vprintf("\tforward iteration %d\n", pManMR->iteration);
+    last = Abc_NtkLatchNum( pNtk );
+
+    Abc_FlowRetime_MarkBlocks( 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 );
+
+#if defined (DEBUG_PRINT_LEVELS)
+    vprintf("\t\tlevels = %d\n", Abc_NtkLevel(pNtk));
+#endif
+
+    Abc_FlowRetime_ClearFlows( 1 );
+
+    pManMR->iteration++;
+  } while( cut != last );
+  
+  // intermediate cleanup (for strashed networks)
+  if (Abc_NtkIsStrash(pNtk)) {
+    Abc_NtkReassignIds( pNtk );
+    pNtk = pManMR->pNtk = Abc_FlowRetime_NtkSilentRestrash( pNtk, 1 );
+  }
+
+  // print info about initial states
+  if (pManMR->fComputeInitState && pManMR->fVerbose)
+    Abc_FlowRetime_PrintInitStateInfo( pNtk );
+
+  // (ii) backward retiming loop
+  pManMR->fIsForward = 0;
+
+  if (!pManMR->fForwardOnly) do {
+    // initializability loop
+    pManMR->iteration = 0;
+
+    // copy/restore network
+    if (pManMR->fGuaranteeInitState) {
+      if ( pNtk != pNtkCopy )
+        Abc_NtkDelete( pNtk );
+      pNtk = pManMR->pNtk = Abc_FlowRetime_NtkDup( pNtkCopy );
+      vprintf("\trestoring network. regs = %d\n", Abc_NtkLatchNum( pNtk ));
+    }
+
+    if (pManMR->fComputeInitState) {
+      Abc_FlowRetime_SetupBackwardInit( pNtk );
+    }
+
+    do {
+      if (pManMR->iteration == pManMR->nMaxIters) break;
+      pManMR->subIteration = 0;
+
+      vprintf("\tbackward iteration %d\n", pManMR->iteration);
+      last = Abc_NtkLatchNum( pNtk );
+
+      Abc_FlowRetime_AddInitBias( );
+      Abc_FlowRetime_MarkBlocks( 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 );
+      }
+
+      Abc_FlowRetime_RemoveInitBias( );
+      cut = Abc_FlowRetime_ImplementCut( pNtk );
+
+#if defined(DEBUG_PRINT_LEVELS)
+      vprintf("\t\tlevels = %d\n", Abc_NtkLevelReverse(pNtk));
+#endif      
+
+      Abc_FlowRetime_ClearFlows( 1 );
+
+      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) {
+        printf("WARNING: no equivalent init state. setting all initial states to don't-cares\n");
+        Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj );
+        break;
+      }
+      Abc_FlowRetime_ConstrainInit( );
+    }
+    
+    Abc_NtkDelete(pManMR->pInitNtk);
+    pManMR->pInitNtk = NULL;
+  } while(1);
+
+//  assert(!pManMR->fComputeInitState || pManMR->pInitNtk);
+  if (pManMR->fComputeInitState)   Abc_NtkDelete(pManMR->pInitNtk);
+  if (pManMR->fGuaranteeInitState) ; /* Abc_NtkDelete(pNtkCopy); note: original ntk deleted later */
+
+  return pNtk;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Pushes latch bubbles outside of box.]
+
+  Description [If network is an AIG, a fCompl0 is allowed to remain on
+               the BI node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_RemoveLatchBubbles( Abc_Obj_t * pLatch ) {
+  int bubble = 0;
+  Abc_Ntk_t *pNtk = pManMR->pNtk;
+  Abc_Obj_t *pBi, *pBo, *pInv;
+      
+  pBi = Abc_ObjFanin0(pLatch);
+  pBo = Abc_ObjFanout0(pLatch);
+  assert(!Abc_ObjIsComplement(pBi));
+  assert(!Abc_ObjIsComplement(pBo));
+
+  // push bubbles on BO into latch box
+  if (Abc_ObjFaninC0(pBo) && Abc_ObjFanoutNum(pBo) > 0) {
+    bubble = 1;
+    if (Abc_LatchIsInit0(pLatch)) Abc_LatchSetInit1(pLatch);
+    else if (Abc_LatchIsInit1(pLatch)) Abc_LatchSetInit0(pLatch);  
+  }
+
+  // absorb bubbles on BI
+  pBi->fCompl0 ^= bubble ^ Abc_ObjFaninC0(pLatch);
+
+  // convert bubble to INV if not AIG
+  if (!Abc_NtkIsStrash( pNtk ) && Abc_ObjFaninC0(pBi)) {
+    pBi->fCompl0 = 0;
+    pInv = Abc_NtkCreateNodeInv( pNtk, Abc_ObjFanin0(pBi) );
+    Abc_ObjPatchFanin( pBi, Abc_ObjFanin0(pBi), pInv );
+  }
+
+  pBo->fCompl0 = 0;
+  pLatch->fCompl0 = 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Marks nodes in TFO/TFI of PI/PO.]
+
+  Description [Sets flow data flag BLOCK appropriately.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) {
+  int i;
+  Abc_Obj_t *pObj;
+
+  if (pManMR->fIsForward){
+    // --- forward retiming : block TFO of inputs    
+
+    // mark the frontier
+    Abc_NtkForEachPo( pNtk, pObj, i )
+      pObj->fMarkA = 1;
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+      {
+        pObj->fMarkA = 1;
+      }
+    // mark the nodes reachable from the PIs
+    Abc_NtkForEachPi( pNtk, pObj, i )
+      Abc_NtkMarkCone_rec( pObj, pManMR->fIsForward );
+  } else {
+    // --- backward retiming : block TFI of outputs
+
+    // mark the frontier
+    Abc_NtkForEachPi( pNtk, pObj, i )
+      pObj->fMarkA = 1;
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+      {
+        pObj->fMarkA = 1;
+      }
+    // mark the nodes reachable from the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+      Abc_NtkMarkCone_rec( pObj, pManMR->fIsForward );
+    // block constant nodes (if enabled)
+    if (pManMR->fBlockConst) {
+      Abc_NtkForEachObj( pNtk, pObj, i )
+        if ((Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pObj)) ||
+            (!Abc_NtkIsStrash(pNtk) && Abc_NodeIsConst(pObj))) {
+          FSET(pObj, BLOCK);
+        }
+    }
+  }
+
+  // copy marks
+  Abc_NtkForEachObj( pNtk, pObj, i ) {
+    if (pObj->fMarkA) {
+      pObj->fMarkA = 0;
+      if (!Abc_ObjIsLatch(pObj) /* && !Abc_ObjIsPi(pObj) */ )
+        FSET(pObj, BLOCK);
+    }
+  }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes maximum flow.]
+
+  Description []
+               
+  SideEffects [Leaves VISITED flags on source-reachable nodes.]
+
+  SeeAlso     []
+
+***********************************************************************/
+int
+Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk, int fVerbose ) {
+  int i, j, flow = 0, last, srcDist = 0;
+  Abc_Obj_t   *pObj, *pObj2;
+//  int clk = clock();
+
+  pManMR->constraintMask |= BLOCK;
+
+  pManMR->fSinkDistTerminate = 0;
+  dfsfast_preorder( pNtk );
+
+  // (i) fast max-flow computation
+  while(!pManMR->fSinkDistTerminate && srcDist < MAX_DIST) {
+    srcDist = MAX_DIST;
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+      if (FDATA(pObj)->e_dist)    
+        srcDist = MIN(srcDist, FDATA(pObj)->e_dist);
+    
+    Abc_NtkForEachLatch( pNtk, pObj, i ) {
+      if (srcDist == FDATA(pObj)->e_dist &&
+          dfsfast_e( pObj, NULL )) {
+#ifdef DEBUG_PRINT_FLOWS
+        printf("\n\n");
+#endif
+        flow++;
+      }
+    }
+  }
+
+  if (fVerbose) vprintf("\t\tmax-flow1 = %d \t", flow);
+
+  // (ii) complete max-flow computation
+  // also, marks source-reachable nodes
+  do {
+    last = flow;
+    Abc_NtkForEachLatch( pNtk, pObj, i ) {
+      if (dfsplain_e( pObj, NULL )) {
+#ifdef DEBUG_PRINT_FLOWS
+        printf("\n\n");
+#endif
+        flow++;
+        Abc_NtkForEachObj( pNtk, pObj2, j )
+          FUNSET( pObj2, VISITED );
+      }
+    }
+  } while (flow > last);
+  
+  if (fVerbose) vprintf("max-flow2 = %d\n", flow);
+
+//  PRT( "time", clock() - clk );
+  return flow;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Restores latch boxes.]
+
+  Description [Latchless BI/BO nodes are removed.  Latch boxes are 
+               restored around remaining latches.]
+               
+  SideEffects [Deletes nodes as appropriate.]
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_FixLatchBoxes( Abc_Ntk_t *pNtk, Vec_Ptr_t *vBoxIns ) {
+  int i;
+  Abc_Obj_t *pObj, *pBo = NULL, *pBi = NULL;
+  Vec_Ptr_t *vFreeBi = Vec_PtrAlloc( 100 );
+  Vec_Ptr_t *vFreeBo = Vec_PtrAlloc( 100 );
+
+  // 1. remove empty bi/bo pairs
+  while(Vec_PtrSize( vBoxIns )) {
+    pBi = (Abc_Obj_t *)Vec_PtrPop( vBoxIns );
+    assert(Abc_ObjIsBi(pBi));
+    assert(Abc_ObjFanoutNum(pBi) == 1);
+    // APH: broken by bias nodes assert(Abc_ObjFaninNum(pBi) == 1);
+    pBo = Abc_ObjFanout0(pBi);
+    assert(!Abc_ObjFaninC0(pBo));
+
+    if (Abc_ObjIsBo(pBo)) {
+      // an empty bi/bo pair
+
+      Abc_ObjRemoveFanins( pBo );
+      // transfer complement from BI, if present 
+      assert(!Abc_ObjIsComplement(Abc_ObjFanin0(pBi)));
+      Abc_ObjBetterTransferFanout( pBo, Abc_ObjFanin0(pBi), Abc_ObjFaninC0(pBi) );
+
+      Abc_ObjRemoveFanins( pBi );
+      pBi->fCompl0 = 0;
+      Vec_PtrPush( vFreeBi, pBi );
+      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));
+
+      // check for complete detachment
+      assert(Abc_ObjFaninNum(pBi) == 0);
+      assert(Abc_ObjFanoutNum(pBi) == 0);
+      assert(Abc_ObjFaninNum(pBo) == 0);
+      assert(Abc_ObjFanoutNum(pBo) == 0);
+    } else if (Abc_ObjIsLatch(pBo)) {
+    } else {
+      Abc_ObjPrint(stdout, pBi);
+      Abc_ObjPrint(stdout, pBo);
+      assert(0);
+    }
+  }
+
+  // 2. add bi/bos as necessary for latches
+  Abc_NtkForEachLatch( pNtk, pObj, i ) {
+    assert(Abc_ObjFaninNum(pObj) == 1);
+    if (Abc_ObjFanoutNum(pObj))
+      pBo = Abc_ObjFanout0(pObj);
+    else pBo = NULL;
+    pBi = Abc_ObjFanin0(pObj);
+    
+    // add BO
+    if (!pBo || !Abc_ObjIsBo(pBo)) {
+      pBo = (Abc_Obj_t *)Vec_PtrPop( vFreeBo );
+      if (Abc_ObjFanoutNum(pObj))  Abc_ObjTransferFanout( pObj, pBo );
+      Abc_ObjAddFanin( pBo, pObj );
+    }
+    // add BI
+    if (!Abc_ObjIsBi(pBi)) {
+      pBi = (Abc_Obj_t *)Vec_PtrPop( vFreeBi );
+      assert(Abc_ObjFaninNum(pBi) == 0);
+      Abc_ObjAddFanin( pBi, Abc_ObjFanin0(pObj) );
+      pBi->fCompl0 = pObj->fCompl0;
+      Abc_ObjRemoveFanins( pObj );
+      Abc_ObjAddFanin( pObj, pBi );
+    }
+  }
+
+  // delete remaining BIs and BOs
+  while(Vec_PtrSize( vFreeBi )) {
+    pObj = (Abc_Obj_t *)Vec_PtrPop( vFreeBi );
+    Abc_NtkDeleteObj( pObj );
+  }
+  while(Vec_PtrSize( vFreeBo )) {
+    pObj = (Abc_Obj_t *)Vec_PtrPop( vFreeBo );
+    Abc_NtkDeleteObj( pObj );
+  }
+
+#if defined(DEBUG_CHECK)
+  Abc_NtkForEachObj( pNtk, pObj, i ) {
+    if (Abc_ObjIsBo(pObj)) {
+      assert(Abc_ObjFaninNum(pObj) == 1);
+      assert(Abc_ObjIsLatch(Abc_ObjFanin0(pObj))); 
+    }
+    if (Abc_ObjIsBi(pObj)) {
+      assert(Abc_ObjFaninNum(pObj) == 1);
+      assert(Abc_ObjFanoutNum(pObj) == 1);
+      assert(Abc_ObjIsLatch(Abc_ObjFanout0(pObj))); 
+    }
+    if (Abc_ObjIsLatch(pObj)) {
+      assert(Abc_ObjFanoutNum(pObj) == 1);
+      assert(Abc_ObjFaninNum(pObj) == 1);
+    }
+  }
+#endif
+
+  Vec_PtrFree( vFreeBi );
+  Vec_PtrFree( vFreeBo );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks register count along all combinational paths.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_VerifyPathLatencies( Abc_Ntk_t * pNtk ) {
+  int i;
+  Abc_Obj_t *pObj;
+  fPathError = 0;
+
+  vprintf("\t\tVerifying latency along all paths...");
+
+  Abc_NtkForEachObj( pNtk, pObj, i ) {
+    if (Abc_ObjIsBo(pObj)) {
+      Abc_FlowRetime_VerifyPathLatencies_rec( pObj, 0 );
+    } else if (!pManMR->fIsForward && Abc_ObjIsPi(pObj)) {
+      Abc_FlowRetime_VerifyPathLatencies_rec( pObj, 0 );
+    }
+
+    if (fPathError) {
+      if (Abc_ObjFaninNum(pObj) > 0) {
+        printf("fanin ");
+        print_node(Abc_ObjFanin0(pObj));
+      }
+      printf("\n");
+      exit(0);
+    }
+  }
+
+  vprintf(" ok\n");
+
+  Abc_NtkForEachObj( pNtk, pObj, i ) {
+    pObj->fMarkA = 0;
+    pObj->fMarkB = 0;
+    pObj->fMarkC = 0;
+  }
+}
+
+
+int
+Abc_FlowRetime_VerifyPathLatencies_rec( Abc_Obj_t * pObj, int markD ) {
+  int i, j;
+  Abc_Obj_t *pNext;
+  int fCare = 0;
+  int markC = pObj->fMarkC;
+
+  if (!pObj->fMarkB) {
+    pObj->fMarkB = 1; // visited
+    
+    if (Abc_ObjIsLatch(pObj))
+      markC = 1;      // latch in output
+    
+    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) ||
+           (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 (!pManMR->fIsForward && Abc_ObjIsPo(pNext)) {
+        if (markD || Abc_ObjIsLatch(pObj)) {
+          printf("\nERROR: extra-latch path to outputs\n");
+          print_node(pNext);
+          printf("\n");
+          fPathError = 1;
+        }
+      } else {
+        j = Abc_FlowRetime_VerifyPathLatencies_rec( pNext, markD || Abc_ObjIsLatch(pObj) );
+        if (j >= 0) {
+          markC |= j;
+          fCare = 1;
+        }
+      }
+
+      if (fPathError) {
+        print_node(pObj);
+        printf("\n");
+        return 0;
+      }
+    }
+  }
+
+  if (!fCare) return -1;
+
+  if (markC && markD) {
+    printf("\nERROR: mult-latch path\n");
+    print_node(pObj);
+    printf("\n");
+    fPathError = 1;
+  }
+  if (!markC && !markD) {
+    printf("\nERROR: no-latch path (inter)\n");
+    print_node(pObj);
+    printf("\n");
+    fPathError = 1;
+  }
+
+  return (pObj->fMarkC = markC);
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Copies initial state from latches to BO nodes.]
+
+  Description [Initial states are marked on BO nodes with INIT_0 and
+               INIT_1 flags in their Flow_Data structures.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_CopyInitState( Abc_Obj_t * pSrc, Abc_Obj_t * pDest ) {
+  Abc_Obj_t *pObj;
+
+  if (!pManMR->fComputeInitState) return;
+
+  assert(Abc_ObjIsLatch(pSrc));
+  assert(Abc_ObjFanin0(pDest) == pSrc);
+  assert(!Abc_ObjFaninC0(pDest));
+
+  FUNSET(pDest, INIT_CARE);
+  if (Abc_LatchIsInit0(pSrc)) {
+    FSET(pDest, INIT_0);
+  } else if (Abc_LatchIsInit1(pSrc)) {
+    FSET(pDest, INIT_1);  
+  }
+  
+  if (!pManMR->fIsForward) {
+    pObj = Abc_ObjData(pSrc);
+    assert(Abc_ObjIsPi(pObj));
+    FDATA(pDest)->pInitObj = pObj;
+  }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Implements min-cut.]
+
+  Description [Requires source-reachable nodes to be marked VISITED.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int
+Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) {
+  int i, j, cut = 0, unmoved = 0;
+  Abc_Obj_t *pObj, *pReg, *pNext, *pBo = NULL, *pBi = NULL;
+  Vec_Ptr_t *vFreeRegs = Vec_PtrAlloc( Abc_NtkLatchNum(pNtk) );
+  Vec_Ptr_t *vBoxIns = Vec_PtrAlloc( Abc_NtkLatchNum(pNtk) );
+  Vec_Ptr_t *vMove = Vec_PtrAlloc( 100 );
+
+  // remove latches from netlist
+  Abc_NtkForEachLatch( pNtk, pObj, i ) {
+    pBo = Abc_ObjFanout0(pObj);
+    pBi = Abc_ObjFanin0(pObj);
+    assert(Abc_ObjIsBo(pBo) && Abc_ObjIsBi(pBi));
+    Vec_PtrPush( vBoxIns, pBi );
+
+    // copy initial state values to BO
+    Abc_FlowRetime_CopyInitState( pObj, pBo );
+
+    // re-use latch elsewhere
+    Vec_PtrPush( vFreeRegs, pObj );
+    FSET(pBo, CROSS_BOUNDARY);
+
+    // cut out of netlist
+    Abc_ObjPatchFanin( pBo, pObj, pBi );
+    Abc_ObjRemoveFanins( pObj );
+
+    // free name
+    if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pObj)))
+      Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pObj));
+  }
+
+  // insert latches into netlist
+  Abc_NtkForEachObj( pNtk, pObj, i ) {
+    if (Abc_ObjIsLatch( pObj )) continue;
+    if (FTEST(pObj, BIAS_NODE)) continue;
+    
+    // a latch is required on every node that lies across the min-cit
+    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 ((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 (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
+      assert(Vec_PtrSize( vFreeRegs ));
+      pReg = (Abc_Obj_t *)Vec_PtrPop( vFreeRegs );
+      
+      Abc_ObjAddFanin(pReg, pObj);
+      while(Vec_PtrSize( vMove )) {
+        pNext = (Abc_Obj_t *)Vec_PtrPop( vMove );
+        Abc_ObjPatchFanin( pNext, pObj, pReg );
+        if (Abc_ObjIsBi(pNext)) assert(Abc_ObjFaninNum(pNext) == 1);
+
+      }
+      // APH: broken by bias nodes  if (Abc_ObjIsBi(pObj)) assert(Abc_ObjFaninNum(pObj) == 1);
+    }
+  }
+
+#if defined(DEBUG_CHECK)        
+  Abc_FlowRetime_VerifyPathLatencies( pNtk );
+#endif
+
+  // delete remaining latches
+  while(Vec_PtrSize( vFreeRegs )) {
+    pReg = (Abc_Obj_t *)Vec_PtrPop( vFreeRegs );
+    Abc_NtkDeleteObj( pReg );
+  }
+  
+  // update initial states
+  Abc_FlowRetime_UpdateLags( );
+  Abc_FlowRetime_InitState( pNtk );
+
+  // restore latch boxes
+  Abc_FlowRetime_FixLatchBoxes( pNtk, vBoxIns );
+
+  Vec_PtrFree( vFreeRegs );
+  Vec_PtrFree( vMove );
+  Vec_PtrFree( vBoxIns );
+
+  vprintf("\t\tmin-cut = %d (unmoved = %d)\n", cut, unmoved);
+  return cut;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds dummy fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_AddDummyFanin( Abc_Obj_t * pObj ) {
+  Abc_Ntk_t *pNtk = Abc_ObjNtk( pObj );
+
+  if (Abc_NtkIsStrash(pNtk)) 
+    Abc_ObjAddFanin(pObj, Abc_AigConst1( pNtk ));
+  else
+    Abc_ObjAddFanin(pObj, Abc_NtkCreateNodeConst0( pNtk ));
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints information about a node.]
+
+  Description [Debuging.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+print_node(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("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](%d),", Abc_ObjId(pNext), Abc_ObjType(pNext), FDATA(pNext)->mark);
+  printf("} fanins {");
+  Abc_ObjForEachFanin( pObj, pNext, i )
+    printf("%d[%d](%d),", Abc_ObjId(pNext), Abc_ObjType(pNext), FDATA(pNext)->mark);
+  printf("}\n");
+}
+
+void
+print_node2(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("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 {");
+  Abc_ObjForEachFanin( pObj, pNext, i )
+    printf("%d ,", Abc_ObjId(pNext));
+  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*************************************************************
+
+  Synopsis    [Transfers fanout.]
+
+  Description [Does not produce an error if there is no fanout.
+               Complements as necessary.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void 
+Abc_ObjBetterTransferFanout( Abc_Obj_t * pFrom, Abc_Obj_t * pTo, int complement ) {
+  Abc_Obj_t *pNext;
+  
+  while(Abc_ObjFanoutNum(pFrom) > 0) {
+    pNext = Abc_ObjFanout0(pFrom);
+    Abc_ObjPatchFanin( pNext, pFrom, Abc_ObjNotCond(pTo, complement) );
+  }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns true is a connection spans the min-cut.]
+
+  Description [pNext is a direct fanout of pObj.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int
+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( int 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;
+    }
+  }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates network.]
+
+  Description [Duplicates any type of network. Preserves copy data.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Abc_Ntk_t* Abc_FlowRetime_NtkDup( Abc_Ntk_t * pNtk ) {
+  Abc_Ntk_t *pNtkCopy;
+  Abc_Obj_t *pObj, *pObjCopy, *pNext, *pNextCopy;
+  int i, j;
+
+  pNtkCopy = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+  pNtkCopy->pName = Extra_UtilStrsav(pNtk->pName);
+  pNtkCopy->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+
+  // copy each object
+  Abc_NtkForEachObj( pNtk, pObj, i) {
+
+    if (Abc_NtkIsStrash( pNtk ) && Abc_AigNodeIsConst( pObj ))
+      pObjCopy = Abc_AigConst1( pNtkCopy );
+    else
+      pObjCopy = Abc_NtkDupObj( pNtkCopy, pObj, 0 );
+
+    FDATA( pObj )->pCopy = pObjCopy;
+    FDATA( pObj )->mark = 0;
+
+    // assert( pManMR->fIsForward || pObj->Id == pObjCopy->Id );
+
+    // copy complementation
+    pObjCopy->fCompl0 = pObj->fCompl0;
+    pObjCopy->fCompl1 = pObj->fCompl1;
+    pObjCopy->fPhase = pObj->fPhase;
+  }
+
+  // connect fanin
+  Abc_NtkForEachObj( pNtk, pObj, i) {
+    pObjCopy = FDATA(pObj)->pCopy;
+    assert(pObjCopy);
+    Abc_ObjForEachFanin( pObj, pNext, j ) {
+      pNextCopy = FDATA(pNext)->pCopy;
+      assert(pNextCopy);
+      assert(pNext->Type == pNextCopy->Type);
+
+      Abc_ObjAddFanin(pObjCopy, pNextCopy);
+    }
+  }
+
+#if defined(DEBUG_CHECK) || 1
+  Abc_NtkForEachObj( pNtk, pObj, i) { 
+    pObjCopy = FDATA(pObj)->pCopy;
+    assert( Abc_ObjFanoutNum( pObj ) ==  Abc_ObjFanoutNum( pObjCopy ) );
+    assert( Abc_ObjFaninNum( pObj ) ==  Abc_ObjFaninNum( pObjCopy ) );
+  }
+#endif
+
+  assert(Abc_NtkObjNum( pNtk )   == Abc_NtkObjNum( pNtkCopy ) );
+  assert(Abc_NtkLatchNum( pNtk ) == Abc_NtkLatchNum( pNtkCopy ) );
+  assert(Abc_NtkPoNum( pNtk )    == Abc_NtkPoNum( pNtkCopy ) );
+  assert(Abc_NtkPiNum( pNtk )    == Abc_NtkPiNum( pNtkCopy ) );
+
+  return pNtkCopy;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Silent restrash.]
+
+  Description [Same functionality as Abc_NtkRestrash but w/o warnings.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_FlowRetime_NtkSilentRestrash( Abc_Ntk_t * pNtk, int fCleanup )
+{
+    Abc_Ntk_t * pNtkAig;
+    Abc_Obj_t * pObj;
+    int i, nNodes;//, RetValue;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // start the new network (constants and CIs of the old network will point to the their counterparts in the new network)
+    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // restrash the nodes (assuming a topological order of the old network)
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+    // finalize the network
+    Abc_NtkFinalize( pNtk, pNtkAig );
+    // perform cleanup if requested
+    if ( fCleanup )
+      nNodes = Abc_AigCleanup((Abc_Aig_t *)pNtkAig->pManFunc);
+    // duplicate EXDC 
+    if ( pNtk->pExdc )
+      pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+      {
+        printf( "Abc_NtkStrash: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+      }
+    return pNtkAig;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates lag values.]
+
+  Description [Recursive.  Forward retiming.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_UpdateLags_forw_rec( Abc_Obj_t *pObj ) {
+  Abc_Obj_t *pNext;
+  int i;
+
+  assert(!Abc_ObjIsPi(pObj));
+  assert(!Abc_ObjIsLatch(pObj));
+
+  if (Abc_ObjIsBo(pObj)) return;
+  if (Abc_NodeIsTravIdCurrent(pObj)) return;
+
+  Abc_NodeSetTravIdCurrent(pObj);
+
+  if (Abc_ObjIsNode(pObj)) {
+    Abc_FlowRetime_SetLag( pObj, -1+Abc_FlowRetime_GetLag(pObj) );
+  }
+
+  Abc_ObjForEachFanin( pObj, pNext, i ) {
+    Abc_FlowRetime_UpdateLags_forw_rec( pNext );
+  }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates lag values.]
+
+  Description [Recursive.  Backward retiming.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_UpdateLags_back_rec( Abc_Obj_t *pObj ) {
+  Abc_Obj_t *pNext;
+  int i;
+
+  assert(!Abc_ObjIsPo(pObj));
+  assert(!Abc_ObjIsLatch(pObj));
+
+  if (Abc_ObjIsBo(pObj)) return;
+  if (Abc_NodeIsTravIdCurrent(pObj)) return;
+
+  Abc_NodeSetTravIdCurrent(pObj);
+
+  if (Abc_ObjIsNode(pObj)) {
+    Abc_FlowRetime_SetLag( pObj, 1+Abc_FlowRetime_GetLag(pObj) );
+  }
+
+  Abc_ObjForEachFanout( pObj, pNext, i ) {
+    Abc_FlowRetime_UpdateLags_back_rec( pNext );
+  }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates lag values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_UpdateLags( ) {
+  Abc_Obj_t *pObj, *pNext;
+  int i, j;
+
+  Abc_NtkIncrementTravId( pManMR->pNtk );
+
+  Abc_NtkForEachLatch( pManMR->pNtk, pObj, i )
+    if (pManMR->fIsForward) {
+      Abc_ObjForEachFanin( pObj, pNext, j )          
+        Abc_FlowRetime_UpdateLags_forw_rec( pNext );
+    } else {
+      Abc_ObjForEachFanout( pObj, pNext, j )          
+        Abc_FlowRetime_UpdateLags_back_rec( pNext );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Gets lag value of a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int 
+Abc_FlowRetime_GetLag( Abc_Obj_t *pObj ) {
+  assert( !Abc_ObjIsLatch(pObj) );
+  assert( Abc_ObjId(pObj) < Vec_IntSize(pManMR->vLags) );
+
+  return Vec_IntEntry(pManMR->vLags, Abc_ObjId(pObj));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets lag value of a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void 
+Abc_FlowRetime_SetLag( Abc_Obj_t *pObj, int lag ) {
+  assert( Abc_ObjIsNode(pObj) );
+  assert( Abc_ObjId(pObj) < Vec_IntSize(pManMR->vLags) );
+
+  Vec_IntWriteEntry(pManMR->vLags, Abc_ObjId(pObj), lag);
+}
+
+
+static void Abc_ObjPrintNeighborhood_rec( Abc_Obj_t *pObj, Vec_Ptr_t *vNodes, int depth ) {
+  Abc_Obj_t *pObj2;
+  int i;
+  
+  if (pObj->fMarkC || depth < 0) return;
+
+  pObj->fMarkC = 1;
+  Vec_PtrPush( vNodes, pObj );
+
+  Abc_ObjPrint( stdout, pObj );
+
+  Abc_ObjForEachFanout(pObj, pObj2, i) {
+    Abc_ObjPrintNeighborhood_rec( pObj2, vNodes, depth-1 );
+  }
+  Abc_ObjForEachFanin(pObj, pObj2, i) {
+    Abc_ObjPrintNeighborhood_rec( pObj2, vNodes, depth-1 );
+  }
+}
+
+void Abc_ObjPrintNeighborhood( Abc_Obj_t *pObj, int depth ) {
+  Vec_Ptr_t *vNodes = Vec_PtrAlloc(100); 
+  Abc_Obj_t *pObj2;
+
+  Abc_ObjPrintNeighborhood_rec( pObj, vNodes, depth );
+
+  while(Vec_PtrSize(vNodes)) {
+    pObj2 = Vec_PtrPop(vNodes);
+    pObj2->fMarkC = 0;
+  }
+
+  Vec_PtrFree(vNodes);
+}
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/fret/fretTime.c b/src/opt/fret/fretTime.c
new file mode 100644
index 00000000..b423ace8
--- /dev/null
+++ b/src/opt/fret/fretTime.c
@@ -0,0 +1,766 @@
+/**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 "fretime.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        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 = ABC_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) );
+      ABC_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( Abc_Obj_t *,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( Abc_Obj_t *,vNodes, pObj, i) {
+    pObj->fMarkB = 1;
+    
+    Abc_ObjForEachFanin( pObj, pNext, j )
+      if ( Abc_NodeIsTravIdCurrent(pNext) && !Abc_ObjIsLatch(pNext))
+        assert(pNext->fMarkB);
+  }
+  Vec_PtrForEachEntryReverse( Abc_Obj_t *,vNodes, pObj, i)
+    pObj->fMarkB = 0;
+#endif
+
+  // ... propagate values
+  Vec_PtrForEachEntryReverse( Abc_Obj_t *,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( Abc_Obj_t *,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( Abc_Obj_t *,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( Abc_Obj_t *,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( Abc_Obj_t *,vNodes, pObj, i) {
+    pObj->fMarkB = 1;
+    
+    Abc_ObjForEachFanout( pObj, pNext, j )
+      if ( Abc_NodeIsTravIdCurrent(pNext) && !Abc_ObjIsLatch(pNext))
+        assert(pNext->fMarkB);
+  }
+  Vec_PtrForEachEntryReverse( Abc_Obj_t *,vNodes, pObj, i)
+    pObj->fMarkB = 0;
+#endif
+
+  // ... propagate values
+  Vec_PtrForEachEntryReverse( Abc_Obj_t *,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( Abc_Obj_t *,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( Abc_Obj_t *,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( Abc_Obj_t *, 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( Abc_Obj_t *, 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( Abc_Obj_t *, 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( Abc_Obj_t *, 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) );
+      ABC_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) );
+      ABC_FREE( pArray );
+    }
+  }
+
+  Vec_PtrFree(pManMR->vExactNodes);
+  ABC_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     []
+
+***********************************************************************/
+int 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);
+}
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/fret/fretime.h b/src/opt/fret/fretime.h
new file mode 100644
index 00000000..c7736070
--- /dev/null
+++ b/src/opt/fret/fretime.h
@@ -0,0 +1,212 @@
+/**CFile****************************************************************
+
+  FileName    [fretime.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Flow-based retiming package.]
+
+  Synopsis    [Header file for retiming package.]
+
+  Author      [Aaron Hurst]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2008.]
+
+  Revision    [$Id: fretime.h,v 1.00 2008/01/01 00:00:00 ahurst Exp $]
+
+***********************************************************************/
+
+#if !defined(RETIME_H_)
+#define RETIME_H_
+
+
+#include "base/abc/abc.h"
+#include "misc/vec/vec.h"
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+// #define IGNORE_TIMING
+// #define DEBUG_PRINT_FLOWS
+// #define DEBUG_VISITED
+// #define DEBUG_PREORDER
+#define DEBUG_CHECK
+// #define DEBUG_PRINT_LEVELS
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define MAX_DIST 30000
+
+// flags in Flow_Data structure...
+#define VISITED_E       0x001
+#define VISITED_R       0x002
+#define VISITED  (VISITED_E | VISITED_R)
+#define FLOW            0x004
+#define CROSS_BOUNDARY  0x008
+#define BLOCK           0x010
+#define INIT_0          0x020
+#define INIT_1          0x040
+#define INIT_CARE (INIT_0 | INIT_1)
+#define CONSERVATIVE    0x080
+#define BLOCK_OR_CONS (BLOCK | CONSERVATIVE)
+#define BIAS_NODE       0x100
+
+
+#define MAX(a,b) ((a)>(b)?(a):(b))
+#define MIN(a,b) ((a)<(b)?(a):(b))
+
+
+typedef struct Flow_Data_t_ {
+  unsigned int mark : 16;
+
+  union {
+    Abc_Obj_t   *pred;
+    /* unsigned int var; */
+    Abc_Obj_t   *pInitObj;
+    Abc_Obj_t   *pCopy;
+    Vec_Ptr_t   *vNodes;
+  };
+
+  unsigned int e_dist : 16;
+  unsigned int r_dist : 16;
+} Flow_Data_t;
+
+// useful macros for manipulating Flow_Data structure...
+#define FDATA( x )     (pManMR->pDataArray+Abc_ObjId(x))
+#define FSET( x, y )   FDATA(x)->mark |= y
+#define FUNSET( x, y ) FDATA(x)->mark &= ~y
+#define FTEST( x, y )  (FDATA(x)->mark & y)
+#define FTIMEEDGES( x )  &(pManMR->vTimeEdges[Abc_ObjId( x )])
+
+typedef struct NodeLag_T_ {
+  int id;
+  int lag;
+} NodeLag_t;
+
+typedef struct InitConstraint_t_ {
+  Abc_Obj_t *pBiasNode;
+
+  Vec_Int_t  vNodes;
+  Vec_Int_t  vLags;
+
+} InitConstraint_t;
+
+typedef struct MinRegMan_t_ {
+ 
+  // problem description:
+  int         maxDelay;
+  int        fComputeInitState, fGuaranteeInitState, fBlockConst;
+  int         nNodes, nLatches;
+  int        fForwardOnly, fBackwardOnly;
+  int        fConservTimingOnly;
+  int         nMaxIters;
+  int        fVerbose;
+  Abc_Ntk_t  *pNtk;
+
+  int         nPreRefine;
+
+  // problem state
+  int        fIsForward;
+  int        fSinkDistTerminate;
+  int         nExactConstraints, nConservConstraints;
+  int         fSolutionIsDc;
+  int         constraintMask;
+  int         iteration, subIteration;
+  Vec_Int_t  *vLags;
+  
+  // problem data
+  Vec_Int_t   *vSinkDistHist;
+  Flow_Data_t *pDataArray;
+  Vec_Ptr_t   *vTimeEdges;
+  Vec_Ptr_t   *vExactNodes;
+  Vec_Ptr_t   *vInitConstraints;
+  Abc_Ntk_t   *pInitNtk;
+  Vec_Ptr_t   *vNodes; // re-useable struct
+  
+  NodeLag_t   *pInitToOrig;
+  int          sizeInitToOrig;
+  
+} MinRegMan_t ;
+
+extern MinRegMan_t *pManMR;
+
+#define vprintf if (pManMR->fVerbose) printf 
+
+static inline void FSETPRED(Abc_Obj_t *pObj, Abc_Obj_t *pPred) {
+  assert(!Abc_ObjIsLatch(pObj)); // must preserve field to maintain init state linkage
+  FDATA(pObj)->pred = pPred;
+}
+static inline Abc_Obj_t * FGETPRED(Abc_Obj_t *pObj) {
+  return FDATA(pObj)->pred;
+}
+
+/*=== fretMain.c ==========================================================*/
+
+Abc_Ntk_t *    Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose,
+                                      int fComputeInitState, int fGuaranteeInitState, int fBlockConst,
+                                      int fForward, int fBackward, int nMaxIters,
+                                      int maxDelay, int fFastButConservative);
+
+void print_node(Abc_Obj_t *pObj);
+
+void Abc_ObjBetterTransferFanout( Abc_Obj_t * pFrom, Abc_Obj_t * pTo, int complement );
+
+int  Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk, int fVerbose );
+int Abc_FlowRetime_IsAcrossCut( Abc_Obj_t *pCur, Abc_Obj_t *pNext );
+void Abc_FlowRetime_ClearFlows( int fClearAll );
+
+int  Abc_FlowRetime_GetLag( Abc_Obj_t *pObj );
+void Abc_FlowRetime_SetLag( Abc_Obj_t *pObj, int lag );
+
+void Abc_FlowRetime_UpdateLags( );
+
+void Abc_ObjPrintNeighborhood( Abc_Obj_t *pObj, int depth );
+
+Abc_Ntk_t * Abc_FlowRetime_NtkSilentRestrash( Abc_Ntk_t * pNtk, int fCleanup );
+
+/*=== fretFlow.c ==========================================================*/
+
+int  dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred );
+int  dfsplain_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred );
+
+void dfsfast_preorder( Abc_Ntk_t *pNtk );
+int  dfsfast_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred );
+int  dfsfast_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred );
+
+/*=== fretInit.c ==========================================================*/
+
+void Abc_FlowRetime_PrintInitStateInfo( Abc_Ntk_t * pNtk );
+
+void Abc_FlowRetime_InitState( Abc_Ntk_t * pNtk );
+
+void Abc_FlowRetime_UpdateForwardInit( Abc_Ntk_t * pNtk );
+void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk );
+
+void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk );
+int  Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk );
+
+void Abc_FlowRetime_ConstrainInit(  );
+void Abc_FlowRetime_AddInitBias(  );
+void Abc_FlowRetime_RemoveInitBias(  );
+
+/*=== fretTime.c ==========================================================*/
+
+void Abc_FlowRetime_InitTiming( Abc_Ntk_t *pNtk );
+void Abc_FlowRetime_FreeTiming( Abc_Ntk_t *pNtk );
+
+int Abc_FlowRetime_RefineConstraints( );
+
+void Abc_FlowRetime_ConstrainConserv( Abc_Ntk_t * pNtk );
+void Abc_FlowRetime_ConstrainExact( Abc_Obj_t * pObj );
+void Abc_FlowRetime_ConstrainExactAll( Abc_Ntk_t * pNtk );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
diff --git a/src/opt/fret/module.make b/src/opt/fret/module.make
new file mode 100644
index 00000000..7a66f0e1
--- /dev/null
+++ b/src/opt/fret/module.make
@@ -0,0 +1,5 @@
+SRC +=    \
+    src/opt/fret/fretMain.c \
+    src/opt/fret/fretFlow.c \
+    src/opt/fret/fretInit.c \
+    src/opt/fret/fretTime.c