1 files changed, 680 insertions, 113 deletions

diff --git a/src/opt/fret/fretInit.c b/src/opt/fret/fretInit.c
index 53df7386..47d338cb 100644
--- a/src/opt/fret/fretInit.c
+++ b/src/opt/fret/fretInit.c
@@ -23,6 +23,10 @@
 #include "io.h"
 #include "fretime.h"
 #include "mio.h"
+#include "hop.h"
+
+#undef DEBUG_PRINT_INIT_NTK
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION PROTOTYPES                          ///
@@ -31,20 +35,24 @@
 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, 
-                                                         Abc_Obj_t *pUseThisPi, Vec_Ptr_t *vOtherPis, 
-                                                         int recurse);
+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 );
 
-extern void * Abc_FrameReadLibGen();                    
-extern Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup );
+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.]
@@ -69,6 +77,40 @@ Abc_FlowRetime_InitState( Abc_Ntk_t * 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*************************************************************
 
@@ -152,6 +194,58 @@ void Abc_FlowRetime_UpdateForwardInit_rec( Abc_Obj_t * pObj ) {
   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*************************************************************
 
@@ -196,11 +290,13 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
   int i, rAnd, rVar, dcAnd, dcVar;
   DdManager * dd = pNtk->pManFunc;
   DdNode *pBdd = pObj->pData, *pVar;
+  Hop_Man_t *pHop = pNtk->pManFunc;
   
   assert(!Abc_ObjIsLatch(pObj));
+  assert(Abc_ObjRegular(pObj));
 
   // (i) constant nodes
-  if (Abc_NtkHasAig(pNtk) && Abc_AigNodeIsConst(pObj)) {
+  if (Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pObj)) {
     Abc_FlowRetime_SetInitValue(pObj, 1, 0);
     return;
   }
@@ -258,10 +354,37 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
     return;
   }
 
-  // ------ AIG network
-  else if ( Abc_NtkHasAig( pNtk )) {
 
-    assert(Abc_AigNodeIsAnd(pObj));
+  // ------ 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);
@@ -361,7 +484,9 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
   Vec_Ptr_t *vObj = Vec_PtrAlloc(100);
 
   // create the network used for the initial state computation
-  if (Abc_NtkHasMapping(pNtk))
+  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 );
@@ -371,14 +496,12 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
     // 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)) {
-      
-      if (Abc_NtkHasAig(pNtk))
-        pObj = Abc_ObjNot( pPi );
-      else
-        pObj = Abc_NtkCreateNodeInv( pManMR->pInitNtk, pPi );
-
+      pObj = Abc_NtkCreateNodeInv( pManMR->pInitNtk, pPi );
       Vec_PtrPush(vObj, pObj);
     }
     else if (Abc_LatchIsInit1(pLatch)) {
@@ -397,14 +520,9 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
     pManMR->fSolutionIsDc = 0;
 
   // mitre output
-  if (Abc_NtkHasAig(pNtk)) {
-    // create AND-by-AND
-    pObj = Vec_PtrPop( vObj );
-    while( Vec_PtrSize(vObj) )
-      pObj = Abc_AigAnd( pManMR->pInitNtk->pManFunc, pObj, Vec_PtrPop( vObj ) ); 
-  } else
-    // create n-input AND gate
-    pObj = Abc_NtkCreateNodeAnd( pManMR->pInitNtk, vObj );
+
+  // create n-input AND gate
+  pObj = Abc_NtkCreateNodeAnd( pManMR->pInitNtk, vObj );
 
   Abc_ObjAddFanin( Abc_NtkCreatePo( pManMR->pInitNtk ), pObj );
 
@@ -418,7 +536,7 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
 
   Description []
                
-  SideEffects []
+  SideEffects [Sets object copies in init ntk.]
 
   SeeAlso     []
 
@@ -427,13 +545,13 @@ 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) {
-    Abc_NtkDelete(pManMR->pInitNtk);
     Vec_PtrFree(vDelete);
     Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj );
     vprintf("\tno init state computation: all-don't-care solution\n");
@@ -441,15 +559,10 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   }
 
   // check that network is combinational
-  // mark superfluous BI nodes for deletion
   Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i ) {
     assert(!Abc_ObjIsLatch(pObj));
     assert(!Abc_ObjIsBo(pObj));
-    
-    if (Abc_ObjIsBi(pObj)) {
-      Abc_ObjBetterTransferFanout( pObj, Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );
-      Vec_PtrPush( vDelete, pObj );
-    }
+    assert(!Abc_ObjIsBi(pObj));
   }
   
   // delete superfluous nodes
@@ -464,9 +577,13 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   Abc_NtkAddDummyPiNames(pManMR->pInitNtk);
   if (Abc_NtkIsLogic(pManMR->pInitNtk))
     Abc_NtkCleanup(pManMR->pInitNtk, 0);
-  else if (Abc_NtkIsStrash(pManMR->pInitNtk)) {  
-    Abc_NtkReassignIds(pManMR->pInitNtk);
-  }
+
+#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);
@@ -474,17 +591,19 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   // 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 );  
+
+  pSatNtk = pManMR->pInitNtk;
   
   // solve
-  result = Abc_NtkMiterSat( pManMR->pInitNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
+  result = Abc_NtkMiterSat( pSatNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
 
   if (!result) { 
     vprintf("SUCCESS\n");
   } else  {    
     vprintf("FAILURE\n");
-    printf("WARNING: no equivalent init state. setting all initial states to don't-cares\n");
-    Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj );
-    Abc_NtkDelete(pManMR->pInitNtk);
     return 0;
   }
 
@@ -495,6 +614,9 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
     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
@@ -513,9 +635,6 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   Abc_NtkForEachLatch( pNtk, pObj, i ) assert( !Abc_LatchIsInitNone( pObj ) );
 #endif
 
-  // deallocate
-  Abc_NtkDelete( pManMR->pInitNtk );
-
   return 1;
 }
 
@@ -534,7 +653,9 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
 void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) {
   Abc_Obj_t *pOrigObj,  *pInitObj;
   Vec_Ptr_t *vBo = Vec_PtrAlloc(100);
-  Vec_Ptr_t *vOldPis = 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)
@@ -542,18 +663,43 @@ void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) {
     if (Abc_ObjIsBo(pOrigObj)) {
       pInitObj = FDATA(pOrigObj)->pInitObj;
       assert(Abc_ObjIsPi(pInitObj));
-      Vec_PtrPush(vBo, pOrigObj);
 
-      Abc_FlowRetime_UpdateBackwardInit_rec( Abc_ObjFanin0( pOrigObj ), pInitObj, vOldPis, 0 );
-    }
+      // DEBUG
+      // printf("update : freeing PI %d\n", pInitObj->Id);
+      
+      // create a buffer instead
+      pBuf = Abc_NtkCreateNodeBuf( pInitNtk, NULL );
+      Abc_FlowRetime_ClearInitToOrig( pBuf );
 
-  // add PIs to network (at latches)
-  Abc_NtkForEachLatch( pNtk, pOrigObj, i )
-    Abc_FlowRetime_UpdateBackwardInit_rec( pOrigObj, NULL, vOldPis, 0 );
+      Abc_ObjBetterTransferFanout( pInitObj, pBuf, 0 );
+      FDATA(pOrigObj)->pInitObj = pBuf;
+      pOrigObj->fMarkA = 1;
+
+      Vec_PtrPush(vBo, pOrigObj);
+      Vec_PtrPush(vPi, pInitObj);
+    }
   
-  // connect nodes in init state network
+  // 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( vBo, pOrigObj, i )
-    Abc_FlowRetime_UpdateBackwardInit_rec( Abc_ObjFanin0( pOrigObj ), NULL, NULL, 1 );
+    Abc_FlowRetime_UpdateBackwardInit_rec( pOrigObj );
   
   // clear flags
   Abc_NtkForEachObj( pNtk, pOrigObj, i )
@@ -561,12 +707,95 @@ void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) {
 
   // deallocate
   Vec_PtrFree( vBo );
-  Vec_PtrFree( vOldPis );
+  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( pInitNtk->pManFunc, 2, fCompl );
+    assert(pData);
+    pInitObj->pData = Abc_SopRegister( 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( 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 
@@ -587,87 +816,43 @@ void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) {
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj, 
-                                                  Abc_Obj_t *pUseThisPi, Vec_Ptr_t *vOtherPis, 
-                                                  int fRecurse) {
-  Abc_Obj_t *pInitObj, *pOrigFanin, *pInitFanin;
-  void      *pData;
+Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj) {
+  Abc_Obj_t *pOrigFanin, *pInitFanin, *pInitObj;
   int i;
-  Abc_Ntk_t *pNtk = Abc_ObjNtk( pOrigObj );
+
+  assert(pOrigObj);
 
   // should never reach primary IOs
   assert(!Abc_ObjIsPi(pOrigObj));
   assert(!Abc_ObjIsPo(pOrigObj));
 
-  // if fanin is latch, it becomes a primary input
-  if (Abc_ObjIsLatch( pOrigObj )) {
-    if (pOrigObj->fMarkA)  return FDATA(pOrigObj)->pInitObj;
-
-    assert(vOtherPis);
-    
-    if (pUseThisPi) { 
-      // reuse curent PI     
-      pInitObj = pUseThisPi; }
-    else { 
-      // reuse previous PI
-      pInitObj = (Abc_Obj_t*)Vec_PtrPop(vOtherPis); 
-    }
-    
-    // remember link from original node to init ntk
-    Abc_ObjSetData( pOrigObj, pInitObj ); 
-
-    pOrigObj->fMarkA = 1;
-    return (FDATA(pOrigObj)->pInitObj = pInitObj);
-  } 
+  // skip bias nodes
+  if (FTEST(pOrigObj, BIAS_NODE)) 
+    return NULL;
 
   // does an init node already exist?
   if(!pOrigObj->fMarkA) {
 
-    if (Abc_NtkHasMapping( pNtk )) {
-      if (!pOrigObj->pData) {
-        // assume terminal...
-        assert(Abc_ObjFaninNum(pOrigObj) == 1);
-        pInitObj = Abc_NtkCreateNodeBuf( pManMR->pInitNtk, NULL );
-      } else {
-        pInitObj = Abc_NtkCreateObj( pManMR->pInitNtk, Abc_ObjType(pOrigObj) );
-        pData = Mio_GateReadSop(pOrigObj->pData);
-        assert( Abc_SopGetVarNum(pData) == Abc_ObjFaninNum(pOrigObj) );
-
-        pInitObj->pData = Abc_SopRegister( pManMR->pInitNtk->pManFunc, pData );
-      }
-    } else {
-      pData = Abc_ObjCopy( pOrigObj );   // save ptr to flow data    
-      if (Abc_NtkIsStrash( pNtk ) && Abc_AigNodeIsConst( pOrigObj ))
-        pInitObj = Abc_AigConst1( pManMR->pInitNtk );
-      else
-        pInitObj = Abc_NtkDupObj( pManMR->pInitNtk, pOrigObj, 0 );
-      Abc_ObjSetCopy( pOrigObj, pData ); // restore ptr to flow data
-
-      // copy complementation
-      pInitObj->fCompl0 = pOrigObj->fCompl0;
-      pInitObj->fCompl1 = pOrigObj->fCompl1;
-      pInitObj->fPhase = pOrigObj->fPhase;
-    }
+    pInitObj = Abc_FlowRetime_CopyNodeToInitNtk( pOrigObj );
 
-    // if we didn't use given PI, immediately transfer fanouts
-    // and add to list for later reuse
-    if (pUseThisPi) {
-      Abc_ObjBetterTransferFanout( pUseThisPi, pInitObj, 0 );
-      Vec_PtrPush( vOtherPis, pUseThisPi );
-    }
+    Abc_FlowRetime_SetInitToOrig( pInitObj, pOrigObj );
+    FDATA(pOrigObj)->pInitObj = pInitObj;
 
     pOrigObj->fMarkA = 1;
-    FDATA(pOrigObj)->pInitObj = pInitObj;
   } else {
     pInitObj = FDATA(pOrigObj)->pInitObj;
   }
+  assert(pInitObj);
     
   // have we already connected this object?
-  if (fRecurse && !pOrigObj->fMarkB) {
+  if (!pOrigObj->fMarkB) {
 
     // create and/or connect fanins
     Abc_ObjForEachFanin( pOrigObj, pOrigFanin, i ) {
-      pInitFanin = Abc_FlowRetime_UpdateBackwardInit_rec( pOrigFanin, NULL, NULL, fRecurse );
+      // 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 );
     }
 
@@ -745,6 +930,72 @@ void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj ) {
   Abc_FlowRetime_SimulateNode( pObj );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Constrains backward retiming for initializability.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool 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( 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, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
+
+  Abc_NtkDelete( pPartNtk );
+ 
+  return !result;
+}
+
 
 /**Function*************************************************************
 
@@ -758,5 +1009,321 @@ void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj ) {
 
 ***********************************************************************/
 void Abc_FlowRetime_ConstrainInit( ) {
-  // unimplemented
+  Vec_Ptr_t *vNodes;
+  int low, high, mid;
+  int i, n, lag;
+  Abc_Obj_t *pObj = NULL, *pOrigObj;
+  InitConstraint_t *pConstraint = 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( 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, *pNext, *pNext2;
+  InitConstraint_t *pConstraint;
+  int i, j, k, l, id;
+  const int nConstraints = Vec_PtrSize( pManMR->vInitConstraints );
+
+  pManMR->pDataArray = 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( 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;
 }