summaryrefslogtreecommitdiffstats
path: root/src/opt/fret
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-01-30 20:01:00 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2008-01-30 20:01:00 -0800
commit0c6505a26a537dc911b6566f82d759521e527c08 (patch)
treef2687995efd4943fe3b1307fce7ef5942d0a57b3 /src/opt/fret
parent4d30a1e4f1edecff86d5066ce4653a370e59e5e1 (diff)
downloadabc-0c6505a26a537dc911b6566f82d759521e527c08.tar.gz
abc-0c6505a26a537dc911b6566f82d759521e527c08.tar.bz2
abc-0c6505a26a537dc911b6566f82d759521e527c08.zip
Version abc80130_2
Diffstat (limited to 'src/opt/fret')
-rw-r--r--src/opt/fret/fretFlow.c696
-rw-r--r--src/opt/fret/fretInit.c762
-rw-r--r--src/opt/fret/fretMain.c1059
-rw-r--r--src/opt/fret/fretTime.c763
-rw-r--r--src/opt/fret/fretime.h165
-rw-r--r--src/opt/fret/module.make5
6 files changed, 3450 insertions, 0 deletions
diff --git a/src/opt/fret/fretFlow.c b/src/opt/fret/fretFlow.c
new file mode 100644
index 00000000..a9cef327
--- /dev/null
+++ b/src/opt/fret/fretFlow.c
@@ -0,0 +1,696 @@
+/**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 "abc.h"
+#include "vec.h"
+#include "fretime.h"
+
+////////////////////////////////////////////////////////////////////////
+/// 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( FTIMEEDGES(pObj), pNext, j ) {
+ vTimeIn = FDATA(pNext)->vNodes;
+ if (!vTimeIn) {
+ vTimeIn = FDATA(pNext)->vNodes = Vec_PtrAlloc(2);
+ }
+ Vec_PtrPush(vTimeIn, pObj);
+ }
+ }
+ }
+#endif
+
+ // clear histogram
+ 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( 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( 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( 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( 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( 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( 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( 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( 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;
+}
diff --git a/src/opt/fret/fretInit.c b/src/opt/fret/fretInit.c
new file mode 100644
index 00000000..53df7386
--- /dev/null
+++ b/src/opt/fret/fretInit.c
@@ -0,0 +1,762 @@
+/**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 "abc.h"
+#include "vec.h"
+#include "io.h"
+#include "fretime.h"
+#include "mio.h"
+
+////////////////////////////////////////////////////////////////////////
+/// 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,
+ Abc_Obj_t *pUseThisPi, Vec_Ptr_t *vOtherPis,
+ int recurse);
+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 );
+
+
+////////////////////////////////////////////////////////////////////////
+/// 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 []
+
+***********************************************************************/
+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 [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;
+ DdManager * dd = pNtk->pManFunc;
+ DdNode *pBdd = pObj->pData, *pVar;
+
+ assert(!Abc_ObjIsLatch(pObj));
+
+ // (i) constant nodes
+ if (Abc_NtkHasAig(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;
+ }
+
+ // ------ 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;
+ }
+
+ // ------ AIG network
+ else if ( Abc_NtkHasAig( pNtk )) {
+
+ assert(Abc_AigNodeIsAnd(pObj));
+ 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_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 );
+
+ // has initial state requirement?
+ if (Abc_LatchIsInit0(pLatch)) {
+
+ if (Abc_NtkHasAig(pNtk))
+ pObj = Abc_ObjNot( pPi );
+ else
+ 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
+ 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 );
+
+ Abc_ObjAddFanin( Abc_NtkCreatePo( pManMR->pInitNtk ), pObj );
+
+ Vec_PtrFree( vObj );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Solves backward initial state computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
+ int i;
+ Abc_Obj_t *pObj, *pInitObj;
+ Vec_Ptr_t *vDelete = Vec_PtrAlloc(0);
+ 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");
+ return 1;
+ }
+
+ // 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 );
+ }
+ }
+
+ // 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);
+ else if (Abc_NtkIsStrash(pManMR->pInitNtk)) {
+ Abc_NtkReassignIds(pManMR->pInitNtk);
+ }
+
+ vprintf("\tsolving for init state (%d nodes)... ", Abc_NtkObjNum(pManMR->pInitNtk));
+ fflush(stdout);
+
+ // convert SOPs to BDD
+ if (Abc_NtkHasSop(pManMR->pInitNtk))
+ Abc_NtkSopToBdd( pManMR->pInitNtk );
+
+ // solve
+ result = Abc_NtkMiterSat( pManMR->pInitNtk, (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;
+ }
+
+ // 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 );
+ }
+
+ // 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
+
+ // deallocate
+ Abc_NtkDelete( pManMR->pInitNtk );
+
+ 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 *vOldPis = Vec_PtrAlloc(100);
+ 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));
+ Vec_PtrPush(vBo, pOrigObj);
+
+ Abc_FlowRetime_UpdateBackwardInit_rec( Abc_ObjFanin0( pOrigObj ), pInitObj, vOldPis, 0 );
+ }
+
+ // add PIs to network (at latches)
+ Abc_NtkForEachLatch( pNtk, pOrigObj, i )
+ Abc_FlowRetime_UpdateBackwardInit_rec( pOrigObj, NULL, vOldPis, 0 );
+
+ // connect nodes in init state network
+ Vec_PtrForEachEntry( vBo, pOrigObj, i )
+ Abc_FlowRetime_UpdateBackwardInit_rec( Abc_ObjFanin0( pOrigObj ), NULL, NULL, 1 );
+
+ // clear flags
+ Abc_NtkForEachObj( pNtk, pOrigObj, i )
+ pOrigObj->fMarkA = pOrigObj->fMarkB = 0;
+
+ // deallocate
+ Vec_PtrFree( vBo );
+ Vec_PtrFree( vOldPis );
+}
+
+
+/**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 *pUseThisPi, Vec_Ptr_t *vOtherPis,
+ int fRecurse) {
+ Abc_Obj_t *pInitObj, *pOrigFanin, *pInitFanin;
+ void *pData;
+ int i;
+ Abc_Ntk_t *pNtk = Abc_ObjNtk( 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);
+ }
+
+ // 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;
+ }
+
+ // 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 );
+ }
+
+ pOrigObj->fMarkA = 1;
+ FDATA(pOrigObj)->pInitObj = pInitObj;
+ } else {
+ pInitObj = FDATA(pOrigObj)->pInitObj;
+ }
+
+ // have we already connected this object?
+ if (fRecurse && !pOrigObj->fMarkB) {
+
+ // create and/or connect fanins
+ Abc_ObjForEachFanin( pOrigObj, pOrigFanin, i ) {
+ pInitFanin = Abc_FlowRetime_UpdateBackwardInit_rec( pOrigFanin, NULL, NULL, fRecurse );
+ 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 []
+
+***********************************************************************/
+void Abc_FlowRetime_ConstrainInit( ) {
+ // unimplemented
+}
diff --git a/src/opt/fret/fretMain.c b/src/opt/fret/fretMain.c
new file mode 100644
index 00000000..780c1f6f
--- /dev/null
+++ b/src/opt/fret/fretMain.c
@@ -0,0 +1,1059 @@
+/**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 "abc.h"
+#include "vec.h"
+#include "fretime.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_FlowRetime_AddDummyFanin( Abc_Obj_t * pObj );
+
+static void Abc_FlowRetime_MainLoop( );
+
+static void Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk );
+static void Abc_FlowRetime_MarkReachable_rec( Abc_Obj_t * pObj, char end );
+static int Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk );
+static void Abc_FlowRetime_RemoveLatchBubbles( Abc_Obj_t * pLatch );
+
+static void Abc_FlowRetime_VerifyPathLatencies( Abc_Ntk_t * pNtk );
+static int Abc_FlowRetime_VerifyPathLatencies_rec( Abc_Obj_t * pObj, int markD );
+
+extern void Abc_NtkMarkCone_rec( Abc_Obj_t * pObj, int fForward );
+extern Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup );
+
+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 fForwardOnly, int fBackwardOnly, int nMaxIters,
+ int maxDelay, int fFastButConservative ) {
+
+ int i;
+ Abc_Obj_t *pObj, *pNext;
+
+ // create manager
+ pManMR = ALLOC( MinRegMan_t, 1 );
+
+ pManMR->pNtk = pNtk;
+ pManMR->fVerbose = fVerbose;
+ pManMR->fComputeInitState = fComputeInitState;
+ pManMR->fGuaranteeInitState = 0;
+ pManMR->fForwardOnly = fForwardOnly;
+ pManMR->fBackwardOnly = fBackwardOnly;
+ pManMR->nMaxIters = nMaxIters;
+ pManMR->maxDelay = maxDelay;
+ pManMR->fComputeInitState = fComputeInitState;
+ pManMR->fConservTimingOnly = fFastButConservative;
+ pManMR->vNodes = Vec_PtrAlloc(100);
+
+ 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 must be > current max delay (%d)\n", 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 Flow_Data structure
+ pManMR->pDataArray = ALLOC( Flow_Data_t, pManMR->nNodes );
+ Abc_FlowRetime_ClearFlows( 1 );
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ Abc_ObjSetCopy( pObj, (void *)(&pManMR->pDataArray[i]) );
+
+ // main loop!
+ Abc_FlowRetime_MainLoop();
+
+ // clear pCopy field
+ Abc_NtkForEachObj( pNtk, pObj, i ) {
+ Abc_ObjSetCopy( pObj, NULL );
+
+ // if not computing init state, set all latches to DC
+ if (!fComputeInitState && Abc_ObjIsLatch(pObj))
+ Abc_LatchSetInitDc(pObj);
+ }
+
+ // deallocate space
+ FREE( pManMR->pDataArray );
+ if (pManMR->vNodes) Vec_PtrFree(pManMR->vNodes);
+ if (pManMR->vSinkDistHist) Vec_IntFree(pManMR->vSinkDistHist);
+ if (pManMR->maxDelay) Abc_FlowRetime_FreeTiming( pNtk );
+
+ // restrash if necessary
+ if (Abc_NtkIsStrash(pNtk)) {
+ Abc_NtkReassignIds( pNtk );
+ pNtk = Abc_NtkRestrash( pNtk, 1 );
+ }
+
+ vprintf("\tfinal reg count = %d\n", Abc_NtkLatchNum(pNtk));
+ vprintf("\tfinal levels = %d\n", Abc_NtkLevel(pNtk));
+
+#if defined(DEBUG_CHECK)
+ Abc_NtkDoCheck( pNtk );
+#endif
+
+ // free manager
+ FREE( pManMR );
+
+ return pNtk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Main loop.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void
+Abc_FlowRetime_MainLoop( ) {
+ Abc_Ntk_t *pNtk = pManMR->pNtk;
+ // Abc_Obj_t *pObj; int i;
+ int last, flow = 0, cut;
+
+ // (i) forward retiming loop
+ 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 );
+
+ vprintf("\t\tlevels = %d\n", Abc_NtkLevel(pNtk));
+
+#if 0
+ Abc_NtkForEachObj( pNtk, pObj, i ) pObj->Level = 0;
+
+ Abc_NtkLevel(pNtk);
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if (pObj->Level > pManMR->maxDelay) {
+ print_node( pObj );
+ Vec_PtrForEachEntry( FTIMEEDGES(pObj), p2,j ) {
+ printf(":%d ", p2->Id);
+ }
+ }
+ Abc_NtkLevelReverse(pNtk);
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if (pObj->Level > pManMR->maxDelay) {
+ print_node( pObj );
+ }
+#endif
+
+ Abc_FlowRetime_ClearFlows( 1 );
+
+ pManMR->iteration++;
+ } while( cut != last );
+
+ // print info about initial states
+ if (pManMR->fComputeInitState && pManMR->fVerbose)
+ Abc_FlowRetime_PrintInitStateInfo( pNtk );
+
+ // (ii) backward retiming loop
+ pManMR->fIsForward = 0;
+ pManMR->iteration = 0;
+
+ if (!pManMR->fForwardOnly) do {
+ // initializability loop
+
+ 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_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 );
+
+ vprintf("\t\tlevels = %d\n", Abc_NtkLevelReverse(pNtk));
+
+#if 0
+ Abc_NtkForEachObj( pNtk, pObj, i ) pObj->Level = 0;
+
+ Abc_NtkLevel(pNtk);
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if (pObj->Level > pManMR->maxDelay) {
+ print_node( pObj );
+ }
+ Abc_NtkLevelReverse(pNtk);
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if (pObj->Level > pManMR->maxDelay) {
+ print_node( pObj );
+ }
+#endif
+
+ Abc_FlowRetime_ClearFlows( 1 );
+
+ pManMR->iteration++;
+ } while( cut != last );
+
+ // compute initial states
+ if (!pManMR->fComputeInitState) break;
+
+ if (Abc_FlowRetime_SolveBackwardInit( pNtk )) {
+ if (pManMR->fVerbose) Abc_FlowRetime_PrintInitStateInfo( pNtk );
+ break;
+ } else {
+ if (!pManMR->fGuaranteeInitState) break;
+ Abc_FlowRetime_ConstrainInit( );
+ }
+ } while(1);
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Pushes latch bubbles outside of box.]
+
+ 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_NtkHasAig( 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){
+ // 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 {
+ // 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 );
+ }
+
+ // 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, bool fVerbose ) {
+ int i, j, flow = 0, last, srcDist = 0;
+ Abc_Obj_t *pObj, *pObj2;
+
+ 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);
+
+ 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);
+ 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 assert(Abc_ObjIsLatch(pBo));
+ }
+
+ // 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;
+
+ // 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);
+
+ }
+ 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_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_NtkHasAig(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 compl ) {
+ Abc_Obj_t *pNext;
+
+ while(Abc_ObjFanoutNum(pFrom) > 0) {
+ pNext = Abc_ObjFanout0(pFrom);
+ Abc_ObjPatchFanin( pNext, pFrom, Abc_ObjNotCond(pTo, compl) );
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns true is a connection spans the min-cut.]
+
+ Description [pNext is a direct fanout of pObj.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+bool
+Abc_FlowRetime_IsAcrossCut( Abc_Obj_t *pObj, Abc_Obj_t *pNext ) {
+
+ if (FTEST(pObj, VISITED_R) && !FTEST(pObj, VISITED_E)) {
+ if (pManMR->fIsForward) {
+ if (!FTEST(pNext, VISITED_R) ||
+ (FTEST(pNext, BLOCK_OR_CONS) & pManMR->constraintMask)||
+ FTEST(pNext, CROSS_BOUNDARY) ||
+ Abc_ObjIsLatch(pNext))
+ return 1;
+ } else {
+ if (FTEST(pNext, VISITED_E) ||
+ FTEST(pNext, CROSS_BOUNDARY))
+ return 1;
+ }
+ }
+
+ return 0;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Resets flow problem]
+
+ Description [If fClearAll is true, all marks will be cleared; this is
+ typically appropriate after the circuit structure has
+ been modified.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_FlowRetime_ClearFlows( bool fClearAll ) {
+ int i;
+
+ if (fClearAll)
+ memset(pManMR->pDataArray, 0, sizeof(Flow_Data_t)*pManMR->nNodes);
+ else {
+ // clear only data related to flow problem
+ for(i=0; i<pManMR->nNodes; i++) {
+ pManMR->pDataArray[i].mark &= ~(VISITED | FLOW );
+ pManMR->pDataArray[i].e_dist = 0;
+ pManMR->pDataArray[i].r_dist = 0;
+ pManMR->pDataArray[i].pred = NULL;
+ }
+ }
+}
diff --git a/src/opt/fret/fretTime.c b/src/opt/fret/fretTime.c
new file mode 100644
index 00000000..f497df60
--- /dev/null
+++ b/src/opt/fret/fretTime.c
@@ -0,0 +1,763 @@
+/**CFile****************************************************************
+
+ FileName [fretTime.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Flow-based retiming package.]
+
+ Synopsis [Delay-constrained retiming code.]
+
+ Author [Aaron Hurst]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - January 1, 2008.]
+
+ Revision [$Id: fretTime.c,v 1.00 2008/01/01 00:00:00 ahurst Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "vec.h"
+#include "fretime.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_FlowRetime_Dfs_forw( Abc_Obj_t * pObj, Vec_Ptr_t *vNodes );
+static void Abc_FlowRetime_Dfs_back( Abc_Obj_t * pObj, Vec_Ptr_t *vNodes );
+
+static void Abc_FlowRetime_ConstrainExact_forw( Abc_Obj_t * pObj );
+static void Abc_FlowRetime_ConstrainExact_back( Abc_Obj_t * pObj );
+static void Abc_FlowRetime_ConstrainConserv_forw( Abc_Ntk_t * pNtk );
+static void Abc_FlowRetime_ConstrainConserv_back( Abc_Ntk_t * pNtk );
+
+
+void trace2(Abc_Obj_t *pObj) {
+ Abc_Obj_t *pNext;
+ int i;
+
+ print_node(pObj);
+ Abc_ObjForEachFanin(pObj, pNext, i)
+ if (pNext->Level >= pObj->Level - 1) {
+ trace2(pNext);
+ break;
+ }
+}
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+ Synopsis [Initializes timing]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_FlowRetime_InitTiming( Abc_Ntk_t *pNtk ) {
+
+ pManMR->nConservConstraints = pManMR->nExactConstraints = 0;
+
+ pManMR->vExactNodes = Vec_PtrAlloc(1000);
+
+ pManMR->vTimeEdges = ALLOC( Vec_Ptr_t, Abc_NtkObjNumMax(pNtk)+1 );
+ assert(pManMR->vTimeEdges);
+ memset(pManMR->vTimeEdges, 0, (Abc_NtkObjNumMax(pNtk)+1) * sizeof(Vec_Ptr_t) );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Marks nodes with conservative constraints.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_FlowRetime_ConstrainConserv( Abc_Ntk_t * pNtk ) {
+ Abc_Obj_t *pObj;
+ int i;
+ void *pArray;
+
+ // clear all exact constraints
+ pManMR->nExactConstraints = 0;
+ while( Vec_PtrSize( pManMR->vExactNodes )) {
+ pObj = Vec_PtrPop( pManMR->vExactNodes );
+
+ if ( Vec_PtrSize( FTIMEEDGES(pObj) )) {
+ pArray = Vec_PtrReleaseArray( FTIMEEDGES(pObj) );
+ FREE( pArray );
+ }
+ }
+
+#if !defined(IGNORE_TIMING)
+ if (pManMR->fIsForward) {
+ Abc_FlowRetime_ConstrainConserv_forw(pNtk);
+ } else {
+ Abc_FlowRetime_ConstrainConserv_back(pNtk);
+ }
+#endif
+
+ Abc_NtkForEachObj( pNtk, pObj, i)
+ assert( !Vec_PtrSize(FTIMEEDGES(pObj)) );
+}
+
+
+void Abc_FlowRetime_ConstrainConserv_forw( Abc_Ntk_t * pNtk ) {
+ Vec_Ptr_t *vNodes = pManMR->vNodes;
+ Abc_Obj_t *pObj, *pNext, *pBi, *pBo;
+ int i, j;
+
+ assert(!Vec_PtrSize( vNodes ));
+ pManMR->nConservConstraints = 0;
+
+ // 1. hard constraints
+
+ // (i) collect TFO of PIs
+ Abc_NtkIncrementTravId(pNtk);
+ Abc_NtkForEachPi(pNtk, pObj, i)
+ Abc_FlowRetime_Dfs_forw( pObj, vNodes );
+
+ // ... propagate values
+ Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+ pObj->Level = 0;
+ Abc_ObjForEachFanin( pObj, pNext, j )
+ {
+ if ( Abc_NodeIsTravIdCurrent(pNext) &&
+ pObj->Level < pNext->Level )
+ pObj->Level = pNext->Level;
+ }
+ pObj->Level += Abc_ObjIsNode(pObj) ? 1 : 0;
+
+ if ( Abc_ObjIsBi(pObj) )
+ pObj->fMarkA = 1;
+
+ assert(pObj->Level <= pManMR->maxDelay);
+ }
+
+ // collect TFO of latches
+ // seed arrival times from BIs
+ Vec_PtrClear(vNodes);
+ Abc_NtkIncrementTravId(pNtk);
+ Abc_NtkForEachLatch(pNtk, pObj, i) {
+ pBo = Abc_ObjFanout0( pObj );
+ pBi = Abc_ObjFanin0( pObj );
+
+ Abc_NodeSetTravIdCurrent( pObj );
+ Abc_FlowRetime_Dfs_forw( pBo, vNodes );
+
+ if (pBi->fMarkA) {
+ pBi->fMarkA = 0;
+ pObj->Level = pBi->Level;
+ assert(pObj->Level <= pManMR->maxDelay);
+ } else
+ pObj->Level = 0;
+ }
+
+#if defined(DEBUG_CHECK)
+ // DEBUG: check DFS ordering
+ Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+ pObj->fMarkB = 1;
+
+ Abc_ObjForEachFanin( pObj, pNext, j )
+ if ( Abc_NodeIsTravIdCurrent(pNext) && !Abc_ObjIsLatch(pNext))
+ assert(pNext->fMarkB);
+ }
+ Vec_PtrForEachEntryReverse(vNodes, pObj, i)
+ pObj->fMarkB = 0;
+#endif
+
+ // ... propagate values
+ Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+ pObj->Level = 0;
+ Abc_ObjForEachFanin( pObj, pNext, j )
+ {
+ if ( Abc_NodeIsTravIdCurrent(pNext) &&
+ pObj->Level < pNext->Level )
+ pObj->Level = pNext->Level;
+ }
+ pObj->Level += Abc_ObjIsNode(pObj) ? 1 : 0;
+
+ if (pObj->Level > pManMR->maxDelay) {
+ FSET(pObj, BLOCK);
+ }
+ }
+
+ // 2. conservative constraints
+
+ // first pass: seed latches with T=0
+ Abc_NtkForEachLatch(pNtk, pObj, i) {
+ pObj->Level = 0;
+ }
+
+ // ... propagate values
+ Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+ pObj->Level = 0;
+ Abc_ObjForEachFanin( pObj, pNext, j ) {
+ if ( Abc_NodeIsTravIdCurrent(pNext) &&
+ pObj->Level < pNext->Level )
+ pObj->Level = pNext->Level;
+ }
+ pObj->Level += Abc_ObjIsNode(pObj) ? 1 : 0;
+
+ if ( Abc_ObjIsBi(pObj) )
+ pObj->fMarkA = 1;
+
+ assert(pObj->Level <= pManMR->maxDelay);
+ }
+
+ Abc_NtkForEachLatch(pNtk, pObj, i) {
+ pBo = Abc_ObjFanout0( pObj );
+ pBi = Abc_ObjFanin0( pObj );
+
+ if (pBi->fMarkA) {
+ pBi->fMarkA = 0;
+ pObj->Level = pBi->Level;
+ assert(pObj->Level <= pManMR->maxDelay);
+ } else
+ pObj->Level = 0;
+ }
+
+ // ... propagate values
+ Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+ pObj->Level = 0;
+ Abc_ObjForEachFanin( pObj, pNext, j ) {
+ if ( Abc_NodeIsTravIdCurrent(pNext) &&
+ pObj->Level < pNext->Level )
+ pObj->Level = pNext->Level;
+ }
+ pObj->Level += Abc_ObjIsNode(pObj) ? 1 : 0;
+
+ // constrained?
+ if (pObj->Level > pManMR->maxDelay) {
+ FSET( pObj, CONSERVATIVE );
+ pManMR->nConservConstraints++;
+ } else
+ FUNSET( pObj, CONSERVATIVE );
+ }
+
+ Vec_PtrClear( vNodes );
+}
+
+
+void Abc_FlowRetime_ConstrainConserv_back( Abc_Ntk_t * pNtk ) {
+ Vec_Ptr_t *vNodes = pManMR->vNodes;
+ Abc_Obj_t *pObj, *pNext, *pBi, *pBo;
+ int i, j, l;
+
+ assert(!Vec_PtrSize(vNodes));
+
+ pManMR->nConservConstraints = 0;
+
+ // 1. hard constraints
+
+ // (i) collect TFO of POs
+ Abc_NtkIncrementTravId(pNtk);
+ Abc_NtkForEachPo(pNtk, pObj, i)
+ Abc_FlowRetime_Dfs_back( pObj, vNodes );
+
+ // ... propagate values
+ Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+ pObj->Level = 0;
+ Abc_ObjForEachFanout( pObj, pNext, j )
+ {
+ l = pNext->Level + (Abc_ObjIsNode(pObj) ? 1 : 0);
+ if ( Abc_NodeIsTravIdCurrent(pNext) &&
+ pObj->Level < l )
+ pObj->Level = l;
+ }
+
+ if ( Abc_ObjIsBo(pObj) )
+ pObj->fMarkA = 1;
+
+ assert(pObj->Level <= pManMR->maxDelay);
+ }
+
+ // collect TFO of latches
+ // seed arrival times from BIs
+ Vec_PtrClear(vNodes);
+ Abc_NtkIncrementTravId(pNtk);
+ Abc_NtkForEachLatch(pNtk, pObj, i) {
+ pBo = Abc_ObjFanout0( pObj );
+ pBi = Abc_ObjFanin0( pObj );
+
+ Abc_NodeSetTravIdCurrent( pObj );
+ Abc_FlowRetime_Dfs_back( pBi, vNodes );
+
+ if (pBo->fMarkA) {
+ pBo->fMarkA = 0;
+ pObj->Level = pBo->Level;
+ assert(pObj->Level <= pManMR->maxDelay);
+ } else
+ pObj->Level = 0;
+ }
+
+#if defined(DEBUG_CHECK)
+ // DEBUG: check DFS ordering
+ Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+ pObj->fMarkB = 1;
+
+ Abc_ObjForEachFanout( pObj, pNext, j )
+ if ( Abc_NodeIsTravIdCurrent(pNext) && !Abc_ObjIsLatch(pNext))
+ assert(pNext->fMarkB);
+ }
+ Vec_PtrForEachEntryReverse(vNodes, pObj, i)
+ pObj->fMarkB = 0;
+#endif
+
+ // ... propagate values
+ Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+ pObj->Level = 0;
+ Abc_ObjForEachFanout( pObj, pNext, j )
+ {
+ l = pNext->Level + (Abc_ObjIsNode(pObj) ? 1 : 0);
+ if ( Abc_NodeIsTravIdCurrent(pNext) &&
+ pObj->Level < l )
+ pObj->Level = l;
+ }
+
+ if (pObj->Level + (Abc_ObjIsNode(pObj)?1:0) > pManMR->maxDelay) {
+ FSET(pObj, BLOCK);
+ }
+ }
+
+ // 2. conservative constraints
+
+ // first pass: seed latches with T=0
+ Abc_NtkForEachLatch(pNtk, pObj, i) {
+ pObj->Level = 0;
+ }
+
+ // ... propagate values
+ Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+ pObj->Level = 0;
+ Abc_ObjForEachFanout( pObj, pNext, j ) {
+ l = pNext->Level + (Abc_ObjIsNode(pObj) ? 1 : 0);
+ if ( Abc_NodeIsTravIdCurrent(pNext) &&
+ pObj->Level < l )
+ pObj->Level = l;
+ }
+
+ if ( Abc_ObjIsBo(pObj) ) {
+ pObj->fMarkA = 1;
+ }
+
+ assert(pObj->Level <= pManMR->maxDelay);
+ }
+
+ Abc_NtkForEachLatch(pNtk, pObj, i) {
+ pBo = Abc_ObjFanout0( pObj );
+ assert(Abc_ObjIsBo(pBo));
+ pBi = Abc_ObjFanin0( pObj );
+ assert(Abc_ObjIsBi(pBi));
+
+ if (pBo->fMarkA) {
+ pBo->fMarkA = 0;
+ pObj->Level = pBo->Level;
+ } else
+ pObj->Level = 0;
+ }
+
+ // ... propagate values
+ Vec_PtrForEachEntryReverse(vNodes, pObj, i) {
+ pObj->Level = 0;
+ Abc_ObjForEachFanout( pObj, pNext, j ) {
+ l = pNext->Level + (Abc_ObjIsNode(pObj) ? 1 : 0);
+ if ( Abc_NodeIsTravIdCurrent(pNext) &&
+ pObj->Level < l )
+ pObj->Level = l;
+ }
+
+ // constrained?
+ if (pObj->Level > pManMR->maxDelay) {
+ FSET( pObj, CONSERVATIVE );
+ pManMR->nConservConstraints++;
+ } else
+ FUNSET( pObj, CONSERVATIVE );
+ }
+
+ Vec_PtrClear( vNodes );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Introduces exact timing constraints for a node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_FlowRetime_ConstrainExact( Abc_Obj_t * pObj ) {
+
+ if (FTEST( pObj, CONSERVATIVE )) {
+ pManMR->nConservConstraints--;
+ FUNSET( pObj, CONSERVATIVE );
+ }
+
+#if !defined(IGNORE_TIMING)
+ if (pManMR->fIsForward) {
+ Abc_FlowRetime_ConstrainExact_forw(pObj);
+ } else {
+ Abc_FlowRetime_ConstrainExact_back(pObj);
+ }
+#endif
+}
+
+void Abc_FlowRetime_ConstrainExact_forw_rec( Abc_Obj_t * pObj, Vec_Ptr_t *vNodes, int latch ) {
+ Abc_Obj_t *pNext;
+ int i;
+
+ // terminate?
+ if (Abc_ObjIsLatch(pObj)) {
+ if (latch) return;
+ latch = 1;
+ }
+
+ // already visited?
+ if (!latch) {
+ if (pObj->fMarkA) return;
+ pObj->fMarkA = 1;
+ } else {
+ if (pObj->fMarkB) return;
+ pObj->fMarkB = 1;
+ }
+
+ // recurse
+ Abc_ObjForEachFanin(pObj, pNext, i) {
+ Abc_FlowRetime_ConstrainExact_forw_rec( pNext, vNodes, latch );
+ }
+
+ // add
+ pObj->Level = 0;
+ Vec_PtrPush(vNodes, Abc_ObjNotCond(pObj, latch));
+}
+
+void Abc_FlowRetime_ConstrainExact_forw( Abc_Obj_t * pObj ) {
+ Vec_Ptr_t *vNodes = pManMR->vNodes;
+ Abc_Obj_t *pNext, *pCur, *pReg;
+ // Abc_Ntk_t *pNtk = pManMR->pNtk;
+ int i, j;
+
+ assert( !Vec_PtrSize(vNodes) );
+ assert( !Abc_ObjIsLatch(pObj) );
+ assert( !Vec_PtrSize( FTIMEEDGES(pObj) ));
+ Vec_PtrPush( pManMR->vExactNodes, pObj );
+
+ // rev topo order
+ Abc_FlowRetime_ConstrainExact_forw_rec( pObj, vNodes, 0 );
+
+ Vec_PtrForEachEntryReverse( vNodes, pCur, i) {
+ pReg = Abc_ObjRegular( pCur );
+
+ if (pReg == pCur) {
+ assert(!Abc_ObjIsLatch(pReg));
+ Abc_ObjForEachFanin(pReg, pNext, j)
+ pNext->Level = MAX( pNext->Level, pReg->Level + (Abc_ObjIsNode(pReg)?1:0));
+ assert(pReg->Level <= pManMR->maxDelay);
+ pReg->Level = 0;
+ pReg->fMarkA = pReg->fMarkB = 0;
+ }
+ }
+ Vec_PtrForEachEntryReverse( vNodes, pCur, i) {
+ pReg = Abc_ObjRegular( pCur );
+ if (pReg != pCur) {
+ Abc_ObjForEachFanin(pReg, pNext, j)
+ if (!Abc_ObjIsLatch(pNext))
+ pNext->Level = MAX( pNext->Level, pReg->Level + (Abc_ObjIsNode(pReg)?1:0));
+
+ if (pReg->Level == pManMR->maxDelay) {
+ Vec_PtrPush( FTIMEEDGES(pObj), pReg);
+ pManMR->nExactConstraints++;
+ }
+ pReg->Level = 0;
+ pReg->fMarkA = pReg->fMarkB = 0;
+ }
+ }
+
+ Vec_PtrClear( vNodes );
+}
+
+void Abc_FlowRetime_ConstrainExact_back_rec( Abc_Obj_t * pObj, Vec_Ptr_t *vNodes, int latch ) {
+ Abc_Obj_t *pNext;
+ int i;
+
+ // terminate?
+ if (Abc_ObjIsLatch(pObj)) {
+ if (latch) return;
+ latch = 1;
+ }
+
+ // already visited?
+ if (!latch) {
+ if (pObj->fMarkA) return;
+ pObj->fMarkA = 1;
+ } else {
+ if (pObj->fMarkB) return;
+ pObj->fMarkB = 1;
+ }
+
+ // recurse
+ Abc_ObjForEachFanout(pObj, pNext, i) {
+ Abc_FlowRetime_ConstrainExact_back_rec( pNext, vNodes, latch );
+ }
+
+ // add
+ pObj->Level = 0;
+ Vec_PtrPush(vNodes, Abc_ObjNotCond(pObj, latch));
+}
+
+
+void Abc_FlowRetime_ConstrainExact_back( Abc_Obj_t * pObj ) {
+ Vec_Ptr_t *vNodes = pManMR->vNodes;
+ Abc_Obj_t *pNext, *pCur, *pReg;
+ // Abc_Ntk_t *pNtk = pManMR->pNtk;
+ int i, j;
+
+ assert( !Vec_PtrSize( vNodes ));
+ assert( !Abc_ObjIsLatch(pObj) );
+ assert( !Vec_PtrSize( FTIMEEDGES(pObj) ));
+ Vec_PtrPush( pManMR->vExactNodes, pObj );
+
+ // rev topo order
+ Abc_FlowRetime_ConstrainExact_back_rec( pObj, vNodes, 0 );
+
+ Vec_PtrForEachEntryReverse( vNodes, pCur, i) {
+ pReg = Abc_ObjRegular( pCur );
+
+ if (pReg == pCur) {
+ assert(!Abc_ObjIsLatch(pReg));
+ Abc_ObjForEachFanout(pReg, pNext, j)
+ pNext->Level = MAX( pNext->Level, pReg->Level + (Abc_ObjIsNode(pReg)?1:0));
+ assert(pReg->Level <= pManMR->maxDelay);
+ pReg->Level = 0;
+ pReg->fMarkA = pReg->fMarkB = 0;
+ }
+ }
+ Vec_PtrForEachEntryReverse( vNodes, pCur, i) {
+ pReg = Abc_ObjRegular( pCur );
+ if (pReg != pCur) {
+ Abc_ObjForEachFanout(pReg, pNext, j)
+ if (!Abc_ObjIsLatch(pNext))
+ pNext->Level = MAX( pNext->Level, pReg->Level + (Abc_ObjIsNode(pReg)?1:0));
+
+ if (pReg->Level == pManMR->maxDelay) {
+ Vec_PtrPush( FTIMEEDGES(pObj), pReg);
+ pManMR->nExactConstraints++;
+ }
+ pReg->Level = 0;
+ pReg->fMarkA = pReg->fMarkB = 0;
+ }
+ }
+
+ Vec_PtrClear( vNodes );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Introduces all exact timing constraints in a network]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_FlowRetime_ConstrainExactAll( Abc_Ntk_t * pNtk ) {
+ int i;
+ Abc_Obj_t *pObj;
+ void *pArray;
+
+ // free existing constraints
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if ( Vec_PtrSize( FTIMEEDGES(pObj) )) {
+ pArray = Vec_PtrReleaseArray( FTIMEEDGES(pObj) );
+ FREE( pArray );
+ }
+ pManMR->nExactConstraints = 0;
+
+ // generate all constraints
+ Abc_NtkForEachObj(pNtk, pObj, i)
+ if (!Abc_ObjIsLatch(pObj) && FTEST( pObj, CONSERVATIVE ) && !FTEST( pObj, BLOCK ))
+ if (!Vec_PtrSize( FTIMEEDGES( pObj ) ))
+ Abc_FlowRetime_ConstrainExact( pObj );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates exact constraints.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_FlowRetime_FreeTiming( Abc_Ntk_t *pNtk ) {
+ Abc_Obj_t *pObj;
+ void *pArray;
+
+ while( Vec_PtrSize( pManMR->vExactNodes )) {
+ pObj = Vec_PtrPop( pManMR->vExactNodes );
+
+ if ( Vec_PtrSize( FTIMEEDGES(pObj) )) {
+ pArray = Vec_PtrReleaseArray( FTIMEEDGES(pObj) );
+ FREE( pArray );
+ }
+ }
+
+ Vec_PtrFree(pManMR->vExactNodes);
+ FREE( pManMR->vTimeEdges );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_FlowRetime_Dfs_forw( Abc_Obj_t * pObj, Vec_Ptr_t *vNodes ) {
+ Abc_Obj_t *pNext;
+ int i;
+
+ if (Abc_ObjIsLatch(pObj)) return;
+
+ Abc_NodeSetTravIdCurrent( pObj );
+
+ Abc_ObjForEachFanout( pObj, pNext, i )
+ if (!Abc_NodeIsTravIdCurrent( pNext ))
+ Abc_FlowRetime_Dfs_forw( pNext, vNodes );
+
+ Vec_PtrPush( vNodes, pObj );
+}
+
+
+void Abc_FlowRetime_Dfs_back( Abc_Obj_t * pObj, Vec_Ptr_t *vNodes ) {
+ Abc_Obj_t *pNext;
+ int i;
+
+ if (Abc_ObjIsLatch(pObj)) return;
+
+ Abc_NodeSetTravIdCurrent( pObj );
+
+ Abc_ObjForEachFanin( pObj, pNext, i )
+ if (!Abc_NodeIsTravIdCurrent( pNext ))
+ Abc_FlowRetime_Dfs_back( pNext, vNodes );
+
+ Vec_PtrPush( vNodes, pObj );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Main timing-constrained routine.]
+
+ Description [Refines constraints that are limiting area improvement.
+ These are identified by computing
+ the min-cuts both with and without the conservative
+ constraints: these two situation represent an
+ over- and under-constrained version of the timing.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+bool Abc_FlowRetime_RefineConstraints( ) {
+ Abc_Ntk_t *pNtk = pManMR->pNtk;
+ int i, flow, count = 0;
+ Abc_Obj_t *pObj;
+ int maxTighten = 99999;
+
+ vprintf("\t\tsubiter %d : constraints = {cons, exact} = %d, %d\n",
+ pManMR->subIteration, pManMR->nConservConstraints, pManMR->nExactConstraints);
+
+ // 1. overconstrained
+ pManMR->constraintMask = BLOCK | CONSERVATIVE;
+ vprintf("\t\trefinement: over ");
+ fflush(stdout);
+ flow = Abc_FlowRetime_PushFlows( pNtk, 0 );
+ vprintf("= %d ", flow);
+
+ // remember nodes
+ if (pManMR->fIsForward) {
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if (!FTEST(pObj, VISITED_R))
+ pObj->fMarkC = 1;
+ } else {
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if (!FTEST(pObj, VISITED_E))
+ pObj->fMarkC = 1;
+ }
+
+ if (pManMR->fConservTimingOnly) {
+ vprintf(" done\n");
+ return 0;
+ }
+
+ // 2. underconstrained
+ pManMR->constraintMask = BLOCK;
+ Abc_FlowRetime_ClearFlows( 0 );
+ vprintf("under = ");
+ fflush(stdout);
+ flow = Abc_FlowRetime_PushFlows( pNtk, 0 );
+ vprintf("%d refined nodes = ", flow);
+ fflush(stdout);
+
+ // find area-limiting constraints
+ if (pManMR->fIsForward) {
+ Abc_NtkForEachObj( pNtk, pObj, i ) {
+ if (pObj->fMarkC &&
+ FTEST(pObj, VISITED_R) &&
+ FTEST(pObj, CONSERVATIVE) &&
+ count < maxTighten) {
+ count++;
+ Abc_FlowRetime_ConstrainExact( pObj );
+ }
+ pObj->fMarkC = 0;
+ }
+ } else {
+ Abc_NtkForEachObj( pNtk, pObj, i ) {
+ if (pObj->fMarkC &&
+ FTEST(pObj, VISITED_E) &&
+ FTEST(pObj, CONSERVATIVE) &&
+ count < maxTighten) {
+ count++;
+ Abc_FlowRetime_ConstrainExact( pObj );
+ }
+ pObj->fMarkC = 0;
+ }
+ }
+
+ vprintf("%d\n", count);
+
+ return (count > 0);
+}
+
+
diff --git a/src/opt/fret/fretime.h b/src/opt/fret/fretime.h
new file mode 100644
index 00000000..167543ce
--- /dev/null
+++ b/src/opt/fret/fretime.h
@@ -0,0 +1,165 @@
+/**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 "abc.h"
+
+// #define IGNORE_TIMING
+// #define DEBUG_PRINT_FLOWS
+// #define DEBUG_VISITED
+// #define DEBUG_PREORDER
+// #define DEBUG_CHECK
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define MAX_DIST 30000
+
+// flags in Flow_Data structure...
+#define VISITED_E 0x01
+#define VISITED_R 0x02
+#define VISITED (VISITED_E | VISITED_R)
+#define FLOW 0x04
+#define CROSS_BOUNDARY 0x08
+#define BLOCK 0x10
+#define INIT_0 0x20
+#define INIT_1 0x40
+#define INIT_CARE (INIT_0 | INIT_1)
+#define CONSERVATIVE 0x80
+#define BLOCK_OR_CONS (BLOCK | CONSERVATIVE)
+
+typedef struct Flow_Data_t_ {
+ unsigned int mark : 16;
+
+ union {
+ Abc_Obj_t *pred;
+ /* unsigned int var; */
+ Abc_Obj_t *pInitObj;
+ Vec_Ptr_t *vNodes;
+ };
+
+ unsigned int e_dist : 16;
+ unsigned int r_dist : 16;
+} Flow_Data_t;
+
+// useful macros for manipulating Flow_Data structure...
+#define FDATA( x ) ((Flow_Data_t *)Abc_ObjCopy(x))
+#define FSET( x, y ) ((Flow_Data_t *)Abc_ObjCopy(x))->mark |= y
+#define FUNSET( x, y ) ((Flow_Data_t *)Abc_ObjCopy(x))->mark &= ~y
+#define FTEST( x, y ) (((Flow_Data_t *)Abc_ObjCopy(x))->mark & y)
+#define FTIMEEDGES( x ) &(pManMR->vTimeEdges[Abc_ObjId( x )])
+
+static inline void FSETPRED(Abc_Obj_t *pObj, Abc_Obj_t *pPred) {
+ assert(!Abc_ObjIsLatch(pObj)); // must preserve field to maintain init state linkage
+ FDATA(pObj)->pred = pPred;
+}
+static inline Abc_Obj_t * FGETPRED(Abc_Obj_t *pObj) {
+ return FDATA(pObj)->pred;
+}
+
+
+typedef struct MinRegMan_t_ {
+
+ // problem description:
+ int maxDelay;
+ bool fComputeInitState, fGuaranteeInitState;
+ int nNodes, nLatches;
+ bool fForwardOnly, fBackwardOnly;
+ bool fConservTimingOnly;
+ int nMaxIters;
+ bool fVerbose;
+ Abc_Ntk_t *pNtk;
+
+ int nPreRefine;
+
+ // problem state
+ bool fIsForward;
+ bool fSinkDistTerminate;
+ int nExactConstraints, nConservConstraints;
+ int fSolutionIsDc;
+ int constraintMask;
+ int iteration, subIteration;
+
+ // problem data
+ Vec_Int_t *vSinkDistHist;
+ Flow_Data_t *pDataArray;
+ Vec_Ptr_t *vTimeEdges;
+ Vec_Ptr_t *vExactNodes;
+ Abc_Ntk_t *pInitNtk;
+ Vec_Ptr_t *vNodes; // re-useable struct
+
+} MinRegMan_t ;
+
+#define vprintf if (pManMR->fVerbose) printf
+
+/*=== fretMain.c ==========================================================*/
+
+extern MinRegMan_t *pManMR;
+
+Abc_Ntk_t * Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
+ int fForward, int fBackward, int nMaxIters,
+ int maxDelay, int fFastButConservative);
+
+void print_node(Abc_Obj_t *pObj);
+
+void Abc_ObjBetterTransferFanout( Abc_Obj_t * pFrom, Abc_Obj_t * pTo, int compl );
+
+int Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk, bool fVerbose );
+bool Abc_FlowRetime_IsAcrossCut( Abc_Obj_t *pCur, Abc_Obj_t *pNext );
+void Abc_FlowRetime_ClearFlows( bool fClearAll );
+
+/*=== fretFlow.c ==========================================================*/
+
+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( );
+
+/*=== fretTime.c ==========================================================*/
+
+void Abc_FlowRetime_InitTiming( Abc_Ntk_t *pNtk );
+void Abc_FlowRetime_FreeTiming( Abc_Ntk_t *pNtk );
+
+bool 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 );
+
+#endif
diff --git a/src/opt/fret/module.make b/src/opt/fret/module.make
new file mode 100644
index 00000000..fda6a73d
--- /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
+