Version abc80126

Makefile

@@ -23,8 +23,8 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
 
 default: $(PROG)
 
-#OPTFLAGS  := -DNDEBUG -O3
-OPTFLAGS  := -g -O
+OPTFLAGS  := -DNDEBUG -O3
+#OPTFLAGS  := -g -O
 
 CFLAGS   += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES)) 
 CXXFLAGS += $(CFLAGS) 

abc.dsp

@@ -1608,6 +1608,10 @@ SOURCE=.\src\opt\fret\fretInit.c
 
 SOURCE=.\src\opt\fret\fretMain.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fret\fretTime.c
+# End Source File
 # End Group
 # End Group
 # Begin Group "map"
@@ -2854,6 +2858,10 @@ SOURCE=.\src\aig\aig\aigCheck.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigCuts.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigDfs.c
 # End Source File
 # Begin Source File

src/aig/aig/aig.h

@@ -137,6 +137,7 @@ struct Aig_Man_t_
     void (*pImpFunc) (void*, void*); // implication checking precedure
     void *           pImpData;       // implication checking data
     void *           pManTime;       // the timing manager
+    void *           pManCuts;
     Vec_Ptr_t *      vMapped;
     Vec_Int_t *      vFlopNums;      
     void *           pSeqModel;
@@ -146,6 +147,56 @@ struct Aig_Man_t_
     int              time2;
 };
 
+// cut computation
+typedef struct Aig_ManCut_t_         Aig_ManCut_t;
+typedef struct Aig_Cut_t_            Aig_Cut_t;
+
+// the cut used to represent node in the AIG
+struct Aig_Cut_t_
+{
+    Aig_Cut_t *     pNext;           // the next cut in the table 
+    int             Cost;            // the cost of the cut
+    unsigned        uSign;           // cut signature
+    int             iNode;           // the node, for which it is the cut
+    short           nCutSize;        // the number of bytes in the cut
+    char            nLeafMax;        // the maximum number of fanins
+    char            nFanins;         // the current number of fanins
+    int             pFanins[0];      // the fanins (followed by the truth table)
+};
+
+// the CNF computation manager
+struct Aig_ManCut_t_
+{
+    // AIG manager
+    Aig_Man_t *     pAig;            // the input AIG manager
+    Aig_Cut_t **    pCuts;           // the cuts for each node in the output manager
+    // parameters
+    int             nCutsMax;        // the max number of cuts at the node
+    int             nLeafMax;        // the max number of leaves of a cut
+    int             fTruth;          // enables truth table computation
+    int             fVerbose;        // enables verbose output
+    // internal variables
+    int             nCutSize;        // the number of bytes needed to store one cut
+    int             nTruthWords;     // the number of truth table words
+    Aig_MmFixed_t * pMemCuts;        // memory manager for cuts
+    unsigned *      puTemp[4];       // used for the truth table computation
+};
+
+static inline Aig_Cut_t *  Aig_ObjCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj )                         { return p->pCuts[pObj->Id];  }
+static inline void         Aig_ObjSetCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj, Aig_Cut_t * pCuts )   { p->pCuts[pObj->Id] = pCuts; }
+
+static inline int          Aig_CutLeaveNum( Aig_Cut_t * pCut )          { return pCut->nFanins;                                    }
+static inline int *        Aig_CutLeaves( Aig_Cut_t * pCut )            { return pCut->pFanins;                                    }
+static inline unsigned *   Aig_CutTruth( Aig_Cut_t * pCut )             { return (unsigned *)(pCut->pFanins + pCut->nLeafMax);     }
+static inline Aig_Cut_t *  Aig_CutNext( Aig_Cut_t * pCut )              { return (Aig_Cut_t *)(((char *)pCut) + pCut->nCutSize);   }
+
+// iterator over cuts of the node
+#define Aig_ObjForEachCut( p, pObj, pCut, i )                           \
+    for ( i = 0, pCut = Aig_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Aig_CutNext(pCut) ) 
+// iterator over leaves of the cut
+#define Aig_CutForEachLeaf( p, pCut, pLeaf, i )                         \
+    for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -386,6 +437,9 @@ static inline int     Aig_ObjFanoutNext( Aig_Man_t * p, int iFan )   { assert(iF
 extern int             Aig_ManCheck( Aig_Man_t * p );
 extern void            Aig_ManCheckMarkA( Aig_Man_t * p );
 extern void            Aig_ManCheckPhase( Aig_Man_t * p );
+/*=== aigCuts.c ========================================================*/
+extern Aig_ManCut_t *  Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fTruth, int fVerbose );
+extern void            Aig_ManCutStop( Aig_ManCut_t * p );
 /*=== aigDfs.c ==========================================================*/
 extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsPio( Aig_Man_t * p );

src/aig/aig/aigCuts.c

+/**CFile****************************************************************
+
+  FileName    [aigCuts.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Computation of K-feasible priority cuts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigCuts.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the cut sweeping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_ManCut_t * Aig_ManCutStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fTruth, int fVerbose )
+{
+    Aig_ManCut_t * p;
+    assert( nCutsMax >= 2  );
+    assert( nLeafMax <= 16 );
+    // allocate the fraiging manager
+    p = ALLOC( Aig_ManCut_t, 1 );
+    memset( p, 0, sizeof(Aig_ManCut_t) );
+    p->nCutsMax = nCutsMax;
+    p->nLeafMax = nLeafMax;
+    p->fTruth   = fTruth;
+    p->fVerbose = fVerbose;
+    p->pAig     = pMan;
+    // allocate room for cuts and equivalent nodes
+    p->pCuts    = ALLOC( Aig_Cut_t *, Aig_ManObjNumMax(pMan) );
+    memset( p->pCuts, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pMan) );
+    // allocate memory manager
+    p->nTruthWords = Aig_TruthWordNum(nLeafMax);
+    p->nCutSize = sizeof(Aig_Cut_t) + sizeof(int) * nLeafMax + fTruth * sizeof(unsigned) * p->nTruthWords;
+    p->pMemCuts = Aig_MmFixedStart( p->nCutSize * p->nCutsMax, 512 );
+    // room for temporary truth tables
+    if ( fTruth )
+    {
+        p->puTemp[0] = ALLOC( unsigned, 4 * p->nTruthWords );
+        p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
+        p->puTemp[2] = p->puTemp[1] + p->nTruthWords;
+        p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
+    }
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCutStop( Aig_ManCut_t * p )
+{
+    Aig_MmFixedStop( p->pMemCuts, 0 );
+    FREE( p->puTemp[0] );
+    free( p->pCuts );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_CutPrint( Aig_Cut_t * pCut )
+{
+    int i;
+    printf( "{" );
+    for ( i = 0; i < pCut->nFanins; i++ )
+        printf( " %d", pCut->pFanins[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjCutPrint( Aig_ManCut_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Cut_t * pCut;
+    int i;
+    printf( "Cuts for node %d:\n", pObj->Id );
+    Aig_ObjForEachCut( p, pObj, pCut, i )
+        if ( pCut->nFanins )
+            Aig_CutPrint( pCut );
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the total number of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCutCount( Aig_ManCut_t * p, int * pnCutsK )
+{
+    Aig_Cut_t * pCut;
+    Aig_Obj_t * pObj;
+    int i, k, nCuts = 0, nCutsK = 0;
+    Aig_ManForEachNode( p->pAig, pObj, i )
+        Aig_ObjForEachCut( p, pObj, pCut, k )
+        {
+            if ( pCut->nFanins == 0 )
+                continue;
+            nCuts++;
+            if ( pCut->nFanins == p->nLeafMax )
+                nCutsK++;
+        }
+    if ( pnCutsK )
+        *pnCutsK = nCutsK;
+    return nCuts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the cost of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_CutFindCost( Aig_ManCut_t * p, Aig_Cut_t * pCut )
+{
+    Aig_Obj_t * pLeaf;
+    int i, Cost = 0;
+    assert( pCut->nFanins > 0 );
+    Aig_CutForEachLeaf( p->pAig, pCut, pLeaf, i )
+        Cost += pLeaf->nRefs;
+    return Cost * 1000 / pCut->nFanins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the cost of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline float Aig_CutFindCost2( Aig_ManCut_t * p, Aig_Cut_t * pCut )
+{
+    Aig_Obj_t * pLeaf;
+    float Cost = 0.0;
+    int i;
+    assert( pCut->nFanins > 0 );
+    Aig_CutForEachLeaf( p->pAig, pCut, pLeaf, i )
+        Cost += (float)1.0/pLeaf->nRefs;
+    return 1/Cost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the next free cut to use.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Cut_t * Aig_CutFindFree( Aig_ManCut_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Cut_t * pCut, * pCutMax;
+    int i;
+    pCutMax = NULL;
+    Aig_ObjForEachCut( p, pObj, pCut, i )
+    {
+        if ( pCut->nFanins == 0 )
+            return pCut;
+        if ( pCutMax == NULL || pCutMax->Cost < pCut->Cost )
+            pCutMax = pCut;
+    }
+    assert( pCutMax != NULL );
+    pCutMax->nFanins = 0;
+    return pCutMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the stretching phase of the cut w.r.t. the merged cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Aig_CutTruthPhase( Aig_Cut_t * pCut, Aig_Cut_t * pCut1 )
+{
+    unsigned uPhase = 0;
+    int i, k;
+    for ( i = k = 0; i < pCut->nFanins; i++ )
+    {
+        if ( k == pCut1->nFanins )
+            break;
+        if ( pCut->pFanins[i] < pCut1->pFanins[k] )
+            continue;
+        assert( pCut->pFanins[i] == pCut1->pFanins[k] );
+        uPhase |= (1 << i);
+        k++;
+    }
+    return uPhase;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Aig_CutComputeTruth( Aig_ManCut_t * p, Aig_Cut_t * pCut, Aig_Cut_t * pCut0, Aig_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+    // permute the first table
+    if ( fCompl0 ) 
+        Kit_TruthNot( p->puTemp[0], Aig_CutTruth(pCut0), p->nLeafMax );
+    else
+        Kit_TruthCopy( p->puTemp[0], Aig_CutTruth(pCut0), p->nLeafMax );
+    Kit_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nFanins, p->nLeafMax, Aig_CutTruthPhase(pCut, pCut0), 0 );
+    // permute the second table
+    if ( fCompl1 ) 
+        Kit_TruthNot( p->puTemp[1], Aig_CutTruth(pCut1), p->nLeafMax );
+    else
+        Kit_TruthCopy( p->puTemp[1], Aig_CutTruth(pCut1), p->nLeafMax );
+    Kit_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nFanins, p->nLeafMax, Aig_CutTruthPhase(pCut, pCut1), 0 );
+    // produce the resulting table
+    Kit_TruthAnd( Aig_CutTruth(pCut), p->puTemp[2], p->puTemp[3], p->nLeafMax );
+//    assert( pCut->nFanins >= Kit_TruthSupportSize( Aig_CutTruth(pCut), p->nLeafMax ) );
+    return Aig_CutTruth(pCut);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs support minimization for the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_CutSupportMinimize( Aig_ManCut_t * p, Aig_Cut_t * pCut )
+{
+    unsigned * pTruth;
+    int uSupp, nFansNew, i, k;
+    // get truth table
+    pTruth = Aig_CutTruth( pCut );
+    // get support 
+    uSupp = Kit_TruthSupport( pTruth, p->nLeafMax );
+    // get the new support size
+    nFansNew = Kit_WordCountOnes( uSupp );
+    // check if there are redundant variables
+    if ( nFansNew == pCut->nFanins )
+        return nFansNew;
+    assert( nFansNew < pCut->nFanins );
+    // minimize support
+    Kit_TruthShrink( p->puTemp[0], pTruth, nFansNew, p->nLeafMax, uSupp, 1 );
+    for ( i = k = 0; i < pCut->nFanins; i++ )
+        if ( uSupp & (1 << i) )
+            pCut->pFanins[k++] = pCut->pFanins[i];
+    assert( k == nFansNew );
+    pCut->nFanins = nFansNew;
+//    assert( nFansNew == Kit_TruthSupportSize( pTruth, p->nLeafMax ) );
+//Extra_PrintBinary( stdout, pTruth, (1<<p->nLeafMax) ); printf( "\n" );
+    return nFansNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pDom is contained in pCut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_CutCheckDominance( Aig_Cut_t * pDom, Aig_Cut_t * pCut )
+{
+    int i, k;
+    for ( i = 0; i < (int)pDom->nFanins; i++ )
+    {
+        for ( k = 0; k < (int)pCut->nFanins; k++ )
+            if ( pDom->pFanins[i] == pCut->pFanins[k] )
+                break;
+        if ( k == (int)pCut->nFanins ) // node i in pDom is not contained in pCut
+            return 0;
+    }
+    // every node in pDom is contained in pCut
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the cut is contained.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_CutFilter( Aig_ManCut_t * p, Aig_Obj_t * pObj, Aig_Cut_t * pCut )
+{ 
+    Aig_Cut_t * pTemp;
+    int i;
+    // go through the cuts of the node
+    Aig_ObjForEachCut( p, pObj, pTemp, i )
+    {
+        if ( pTemp->nFanins < 2 )
+            continue;
+        if ( pTemp == pCut )
+            continue;
+        if ( pTemp->nFanins > pCut->nFanins )
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
+                continue;
+            // check containment seriously
+            if ( Aig_CutCheckDominance( pCut, pTemp ) )
+            {
+                // remove contained cut
+                pTemp->nFanins = 0;
+            }
+         }
+        else
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
+                continue;
+            // check containment seriously
+            if ( Aig_CutCheckDominance( pTemp, pCut ) )
+            {
+                // remove the given
+                pCut->nFanins = 0;
+                return 1;
+            }
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_CutMergeOrdered( Aig_ManCut_t * p, Aig_Cut_t * pC0, Aig_Cut_t * pC1, Aig_Cut_t * pC )
+{ 
+    int i, k, c;
+    assert( pC0->nFanins >= pC1->nFanins );
+    // the case of the largest cut sizes
+    if ( pC0->nFanins == p->nLeafMax && pC1->nFanins == p->nLeafMax )
+    {
+        for ( i = 0; i < pC0->nFanins; i++ )
+            if ( pC0->pFanins[i] != pC1->pFanins[i] )
+                return 0;
+        for ( i = 0; i < pC0->nFanins; i++ )
+            pC->pFanins[i] = pC0->pFanins[i];
+        pC->nFanins = pC0->nFanins;
+        return 1;
+    }
+    // the case when one of the cuts is the largest
+    if ( pC0->nFanins == p->nLeafMax )
+    {
+        for ( i = 0; i < pC1->nFanins; i++ )
+        {
+            for ( k = pC0->nFanins - 1; k >= 0; k-- )
+                if ( pC0->pFanins[k] == pC1->pFanins[i] )
+                    break;
+            if ( k == -1 ) // did not find
+                return 0;
+        }
+        for ( i = 0; i < pC0->nFanins; i++ )
+            pC->pFanins[i] = pC0->pFanins[i];
+        pC->nFanins = pC0->nFanins;
+        return 1;
+    }
+
+    // compare two cuts with different numbers
+    i = k = 0;
+    for ( c = 0; c < p->nLeafMax; c++ )
+    {
+        if ( k == pC1->nFanins )
+        {
+            if ( i == pC0->nFanins )
+            {
+                pC->nFanins = c;
+                return 1;
+            }
+            pC->pFanins[c] = pC0->pFanins[i++];
+            continue;
+        }
+        if ( i == pC0->nFanins )
+        {
+            if ( k == pC1->nFanins )
+            {
+                pC->nFanins = c;
+                return 1;
+            }
+            pC->pFanins[c] = pC1->pFanins[k++];
+            continue;
+        }
+        if ( pC0->pFanins[i] < pC1->pFanins[k] )
+        {
+            pC->pFanins[c] = pC0->pFanins[i++];
+            continue;
+        }
+        if ( pC0->pFanins[i] > pC1->pFanins[k] )
+        {
+            pC->pFanins[c] = pC1->pFanins[k++];
+            continue;
+        }
+        pC->pFanins[c] = pC0->pFanins[i++]; 
+        k++;
+    }
+    if ( i < pC0->nFanins || k < pC1->nFanins )
+        return 0;
+    pC->nFanins = c;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the object for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_CutMerge( Aig_ManCut_t * p, Aig_Cut_t * pCut0, Aig_Cut_t * pCut1, Aig_Cut_t * pCut )
+{ 
+    assert( p->nLeafMax > 0 );
+    // merge the nodes
+    if ( pCut0->nFanins < pCut1->nFanins )
+    {
+        if ( !Aig_CutMergeOrdered( p, pCut1, pCut0, pCut ) )
+            return 0;
+    }
+    else
+    {
+        if ( !Aig_CutMergeOrdered( p, pCut0, pCut1, pCut ) )
+            return 0;
+    }
+    pCut->uSign = pCut0->uSign | pCut1->uSign;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Cut_t * Aig_ObjPrepareCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj, int fTriv )
+{
+    Aig_Cut_t * pCutSet, * pCut;
+    int i;
+    // create the cutset of the node
+    pCutSet = (Aig_Cut_t *)Aig_MmFixedEntryFetch( p->pMemCuts );
+    Aig_ObjSetCuts( p, pObj, pCutSet );
+    Aig_ObjForEachCut( p, pObj, pCut, i )
+    {
+        pCut->nFanins  = 0;
+        pCut->iNode    = pObj->Id;
+        pCut->nCutSize = p->nCutSize;
+        pCut->nLeafMax = p->nLeafMax;
+    }
+    // add unit cut if needed
+    if ( fTriv )
+    {
+        pCut = pCutSet;
+        pCut->Cost = 0;
+        pCut->iNode = pObj->Id;
+        pCut->nFanins = 1;
+        pCut->pFanins[0] = pObj->Id;
+        pCut->uSign = Aig_ObjCutSign( pObj->Id );
+        if ( p->fTruth )
+        memset( Aig_CutTruth(pCut), 0xAA, sizeof(unsigned) * p->nTruthWords );
+    }
+    return pCutSet;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives cuts for one node and sweeps this node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjComputeCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj, int fTriv )
+{
+    Aig_Cut_t * pCut0, * pCut1, * pCut, * pCutSet;
+    Aig_Obj_t * pFanin0 = Aig_ObjFanin0(pObj);
+    Aig_Obj_t * pFanin1 = Aig_ObjFanin1(pObj);
+    int i, k;
+    // the node is not processed yet
+    assert( Aig_ObjIsNode(pObj) );
+    assert( Aig_ObjCuts(p, pObj) == NULL );
+    // set up the first cut
+    pCutSet = Aig_ObjPrepareCuts( p, pObj, fTriv );
+    // compute pair-wise cut combinations while checking table
+    Aig_ObjForEachCut( p, pFanin0, pCut0, i )
+    if ( pCut0->nFanins > 0 )
+    Aig_ObjForEachCut( p, pFanin1, pCut1, k )
+    if ( pCut1->nFanins > 0 )
+    {
+        // make sure K-feasible cut exists
+        if ( Kit_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->nLeafMax )
+            continue;
+        // get the next cut of this node
+        pCut = Aig_CutFindFree( p, pObj );
+        // assemble the new cut
+        if ( !Aig_CutMerge( p, pCut0, pCut1, pCut ) )
+        {
+            assert( pCut->nFanins == 0 );
+            continue;
+        }
+        // check containment
+        if ( Aig_CutFilter( p, pObj, pCut ) )
+        {
+            assert( pCut->nFanins == 0 );
+            continue;
+        }
+        // create its truth table
+        if ( p->fTruth )
+            Aig_CutComputeTruth( p, pCut, pCut0, pCut1, Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
+        // assign the cost
+        pCut->Cost = Aig_CutFindCost( p, pCut );
+        assert( pCut->nFanins > 0 );
+        assert( pCut->Cost > 0 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for all nodes in the static AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fTruth, int fVerbose )
+{
+    Aig_ManCut_t * p;
+    Aig_Obj_t * pObj;
+    int i, clk = clock();
+    assert( pAig->pManCuts == NULL );
+    // start the manager
+    p = Aig_ManCutStart( pAig, nCutsMax, nLeafMax, fTruth, fVerbose );
+    // set elementary cuts at the PIs
+    Aig_ManForEachPi( pAig, pObj, i )
+        Aig_ObjPrepareCuts( p, pObj, 1 );
+    // process the nodes
+    Aig_ManForEachNode( pAig, pObj, i )
+        Aig_ObjComputeCuts( p, pObj, 1 );
+    // print stats
+    if ( fVerbose )
+    {
+        int nCuts, nCutsK;
+        nCuts = Aig_ManCutCount( p, &nCutsK );
+        printf( "Nodes = %6d. Total cuts = %6d. %d-input cuts = %6d.\n",
+            Aig_ManObjNum(pAig), nCuts, nLeafMax, nCutsK );
+        printf( "Cut size = %2d. Truth size = %2d. Total mem = %5.2f Mb  ",
+            p->nCutSize, 4*p->nTruthWords, 1.0*Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) );
+        PRT( "Runtime", clock() - clk );
+/*
+        Aig_ManForEachNode( pAig, pObj, i )
+            if ( i % 300 == 0 )
+                Aig_ObjCutPrint( p, pObj );
+*/
+    }
+    // remember the cut manager
+    pAig->pManCuts = p;
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/cnf/cnfCore.c

@@ -57,7 +57,7 @@ Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs )
 
     // generate cuts for all nodes, assign cost, and find best cuts
 clk = clock();
-    pMemCuts = Dar_ManComputeCuts( pAig, 10 );
+    pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 );
 p->timeCuts = clock() - clk;
 
     // find the mapping

src/aig/dar/dar.h

@@ -83,7 +83,7 @@ extern Aig_Man_t *     Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
 /*=== darCore.c ========================================================*/
 extern void            Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars );
 extern int             Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
-extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax );
+extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose );
 /*=== darRefact.c ========================================================*/
 extern void            Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
 extern int             Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );

src/aig/dar/darCore.c

@@ -195,6 +195,34 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the total number of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ManCutCount( Aig_Man_t * pAig, int * pnCutsK )
+{
+    Dar_Cut_t * pCut;
+    Aig_Obj_t * pObj;
+    int i, k, nCuts = 0, nCutsK = 0;
+    Aig_ManForEachNode( pAig, pObj, i )
+        Dar_ObjForEachCut( pObj, pCut, k )
+        {
+            nCuts++;
+            if ( pCut->nLeaves == 4 )
+                nCutsK++;
+        }
+    if ( pnCutsK )
+        *pnCutsK = nCutsK;
+    return nCuts;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -204,13 +232,13 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
   SeeAlso     []
 
 ***********************************************************************/
-Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax )
+Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose )
 {
     Dar_Man_t * p;
     Dar_RwrPar_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Aig_MmFixed_t * pMemCuts;
-    int i, nNodes;
+    int i, nNodes, clk = clock();
     // remove dangling nodes
     if ( (nNodes = Aig_ManCleanup( pAig )) )
     {
@@ -226,6 +254,23 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax )
     // compute cuts for each nodes in the topological order
     Aig_ManForEachNode( pAig, pObj, i )
         Dar_ObjComputeCuts( p, pObj );
+    // print verbose stats
+    if ( fVerbose )
+    {
+//        Aig_Obj_t * pObj;
+        int nCuts, nCutsK;//, i;
+        nCuts = Dar_ManCutCount( pAig, &nCutsK );
+        printf( "Nodes = %6d. Total cuts = %6d. 4-input cuts = %6d.\n",
+            Aig_ManObjNum(pAig), nCuts, nCutsK );
+        printf( "Cut size = %2d. Truth size = %2d. Total mem = %5.2f Mb  ",
+            sizeof(Dar_Cut_t), 4, 1.0*Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) );
+        PRT( "Runtime", clock() - clk );
+/*
+        Aig_ManForEachNode( pAig, pObj, i )
+            if ( i % 300 == 0 )
+                Dar_ObjCutPrint( pAig, pObj );
+*/
+    }
     // free the cuts
     pMemCuts = p->pMemCuts;
     p->pMemCuts = NULL;

src/aig/dar/darCut.c

@@ -30,6 +30,47 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_CutPrint( Dar_Cut_t * pCut )
+{
+    unsigned i;
+    printf( "{" );
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        printf( " %d", pCut->pLeaves[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ObjCutPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Dar_Cut_t * pCut;
+    int i;
+    printf( "Cuts for node %d:\n", pObj->Id );
+    Dar_ObjForEachCut( pObj, pCut, i )
+        Dar_CutPrint( pCut );
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the number of 1s in the machine word.]
 
   Description []

src/aig/dar/darInt.h

@@ -134,6 +134,7 @@ extern void            Dar_ManCutsStart( Dar_Man_t * p );
 extern void            Dar_ManCutsFree( Dar_Man_t * p );
 extern Dar_Cut_t *     Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj );
 extern Dar_Cut_t *     Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
+extern void            Dar_ObjCutPrint( Aig_Man_t * p, Aig_Obj_t * pObj );
 /*=== darData.c ===========================================================*/
 extern Vec_Int_t *     Dar_LibReadNodes();
 extern Vec_Int_t *     Dar_LibReadOuts();

src/aig/fra/fraClaus.c

@@ -33,6 +33,11 @@ struct Clu_Man_t_
     int              nFrames;        // the K of the K-step induction
     int              nPref;          // the number of timeframes to skip  
     int              nClausesMax;    // the max number of 4-clauses to consider
+    int              nLutSize;       // the max cut size
+    int              nLevels;        // the number of levels for cut computation
+    int              nCutsMax;       // the maximum number of cuts to compute at a node
+    int              nBatches;       // the number of clause batches to use
+    int              fStepUp;        // increase cut size for each batch
     int              fVerbose;       
     int              fVeryVerbose;
     // internal parameters
@@ -40,18 +45,25 @@ struct Clu_Man_t_
     int              nSimWordsPref;  // the number of simulation words in the prefix
     int              nSimFrames;     // the number of frames to simulate 
     int              nBTLimit;       // the largest number of backtracks (0 = infinite)
-    // the network
+    // the network 
     Aig_Man_t *      pAig;
     // SAT solvers
     sat_solver *     pSatMain;
     sat_solver *     pSatBmc;
     // CNF for the test solver
     Cnf_Dat_t *      pCnf;
+    int              fFail;
+    int              fFiltering; 
+    int              fNothingNew;
     // clauses
     Vec_Int_t *      vLits;
     Vec_Int_t *      vClauses;
     Vec_Int_t *      vCosts;
     int              nClauses;
+    // clauses proven
+    Vec_Int_t *      vLitsProven;
+    Vec_Int_t *      vClausesProven;
+    int              nClausesProven;
     // counter-examples
     Vec_Ptr_t *      vCexes;
     int              nCexes;
@@ -184,7 +196,7 @@ void transpose32a( unsigned a[32] )
 int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
 {
     unsigned Matrix[32];
-    unsigned * pSims[4], uWord;
+    unsigned * pSims[16], uWord;
     int nSeries, i, k, j;
     int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
     // compute parameters
@@ -229,7 +241,7 @@ int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
 ***********************************************************************/
 int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
 {
-    unsigned * pSims[4], uWord;
+    unsigned * pSims[16], uWord;
     int iMint, i, k, b;
     int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
     // compute parameters
@@ -258,6 +270,43 @@ int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
     return (int)uWord;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Return the number of combinations appearing in the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausProcessClausesCut3( Clu_Man_t * p, Fra_Sml_t * pSimMan, Aig_Cut_t * pCut, int * pScores )
+{
+    unsigned * pSims[16];
+    int iMint, i, k, b, nMints;
+    int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
+    // compute parameters
+    assert( pCut->nFanins > 1 && pCut->nFanins < 17 );
+    assert( nWordsForSim % 8 == 0 );
+    // get parameters
+    for ( i = 0; i < (int)pCut->nFanins; i++ )
+        pSims[i] = Fra_ObjSim( pSimMan, pCut->pFanins[i] ) + p->nSimWordsPref;
+    // add combinational patterns
+    nMints = (1 << pCut->nFanins);
+    memset( pScores, 0, sizeof(int) * nMints );
+    // go through the simulation patterns
+    for ( i = 0; i < nWordsForSim; i++ )
+        for ( k = 0; k < 32; k++ )
+        {
+            iMint = 0;
+            for ( b = 0; b < (int)pCut->nFanins; b++ )
+                if ( pSims[b][i] & (1 << k) )
+                    iMint |= (1 << b);
+            pScores[iMint]++;
+        }
+}
+
 
 /**Function*************************************************************
 
@@ -280,6 +329,8 @@ int Fra_ClausSelectClauses( Clu_Man_t * p )
     memset( pCostCount, 0, sizeof(int) * CostMax );
     Vec_IntForEachEntry( p->vCosts, Cost, i )
     {
+        if ( Cost == -1 )
+            continue;
         assert( Cost < CostMax );
         pCostCount[ Cost ]++;
     }
@@ -334,6 +385,26 @@ void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost
 
 /**Function*************************************************************
 
+  Synopsis    [Processes the clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausRecordClause2( Clu_Man_t * p, Aig_Cut_t * pCut, int iMint, int Cost )
+{
+    int i;
+    for ( i = 0; i < (int)pCut->nFanins; i++ )
+        Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pFanins[i]], (iMint&(1<<i)) ) );
+    Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
+    Vec_IntPush( p->vCosts, Cost );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if simulation info is composed of all zeros.]
 
   Description []
@@ -485,6 +556,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
 int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
 {
     Aig_MmFixed_t * pMemCuts;
+//    Aig_ManCut_t * pManCut;
     Fra_Sml_t * pComb, * pSeq;
     Aig_Obj_t * pObj;
     Dar_Cut_t * pCut;
@@ -519,7 +591,8 @@ PRT( "Lat-cla", clock() - clk );
 
     // generate cuts for all nodes, assign cost, and find best cuts
 clk = clock();
-    pMemCuts = Dar_ManComputeCuts( p->pAig, 10 );
+    pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 1 );
+//    pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 );
 if ( p->fVerbose )
 {
 PRT( "Cuts   ", clock() - clk );
@@ -572,6 +645,7 @@ clk = clock();
             }
     Fra_SmlStop( pComb );
     Aig_MmFixedStop( pMemCuts, 0 );
+//    Aig_ManCutStop( pManCut );
 if ( p->fVerbose )
 {
 PRT( "Infocmb", clock() - clk );
@@ -590,6 +664,174 @@ PRT( "Infocmb", clock() - clk );
 
 /**Function*************************************************************
 
+  Synopsis    [Processes the clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
+{
+//    Aig_MmFixed_t * pMemCuts;
+    Aig_ManCut_t * pManCut;
+    Fra_Sml_t * pComb, * pSeq;
+    Aig_Obj_t * pObj;
+    Aig_Cut_t * pCut;
+    int i, k, j, clk, nCuts = 0;
+    int ScoresSeq[1<<12], ScoresComb[1<<12];
+    assert( p->nLutSize < 13 );
+
+    // simulate the AIG
+clk = clock();
+    srand( 0xAABBAABB );
+    pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
+    if ( pSeq->fNonConstOut )
+    {
+        printf( "Property failed after sequential simulation!\n" );
+        Fra_SmlStop( pSeq );
+        return 0;
+    }
+if ( p->fVerbose )
+{
+PRT( "Sim-seq", clock() - clk );
+}
+
+    // perform combinational simulation
+clk = clock();
+    srand( 0xAABBAABB );
+    pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref  );
+if ( p->fVerbose )
+{
+PRT( "Sim-cmb", clock() - clk );
+}
+
+
+clk = clock();
+    if ( fRefs )
+    {
+    Fra_ClausCollectLatchClauses( p, pSeq );
+if ( p->fVerbose )
+{
+PRT( "Lat-cla", clock() - clk );
+}
+    }
+
+
+    // generate cuts for all nodes, assign cost, and find best cuts
+clk = clock();
+//    pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 1 );
+    pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose );
+if ( p->fVerbose )
+{
+PRT( "Cuts   ", clock() - clk );
+}
+
+    // collect combinational info for each cut
+clk = clock();
+    Aig_ManForEachNode( p->pAig, pObj, i )
+    {
+        if ( pObj->Level > (unsigned)p->nLevels )
+            continue;
+        Aig_ObjForEachCut( pManCut, pObj, pCut, k )
+            if ( pCut->nFanins > 1 )
+            {
+                nCuts++;
+                Fra_ClausProcessClausesCut3( p, pSeq, pCut, ScoresSeq );
+                Fra_ClausProcessClausesCut3( p, pComb, pCut, ScoresComb );
+                // write the clauses
+                for ( j = 0; j < (1<<pCut->nFanins); j++ )
+                    if ( ScoresComb[j] != 0 && ScoresSeq[j] == 0 )
+                        Fra_ClausRecordClause2( p, pCut, j, ScoresComb[j] );
+
+            }
+    }
+    Fra_SmlStop( pSeq );
+    Fra_SmlStop( pComb );
+//    Aig_MmFixedStop( pMemCuts, 0 );
+    Aig_ManCutStop( pManCut );
+    p->pAig->pManCuts = NULL;
+if ( p->fVerbose )
+{
+PRT( "Infosim", clock() - clk );
+}
+
+    if ( p->fVerbose )
+    printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n", 
+        Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
+
+    // filter out clauses that are contained in the already proven clauses
+    assert( p->nClauses == 0 );
+    p->nClauses = Vec_IntSize( p->vClauses );
+    if ( Vec_IntSize( p->vClausesProven ) > 0 )
+    {
+        int RetValue, k, Beg, End, * pStart;
+        // reset the solver
+        if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
+        p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
+        if ( p->pSatMain == NULL )
+        {
+            printf( "Error: Main solver is unsat.\n" );
+            return -1;
+        }  
+
+        // add the proven clauses
+        Beg = 0;
+        pStart = Vec_IntArray(p->vLitsProven);
+        Vec_IntForEachEntry( p->vClausesProven, End, i )
+        {
+            assert( End - Beg <= p->nLutSize );
+            // add the clause to all timeframes
+            RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
+            if ( RetValue == 0 )
+            {
+                printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
+                return -1;
+            }
+            Beg = End;
+        }
+        assert( End == Vec_IntSize(p->vLitsProven) );
+
+        // check the clauses
+        Beg = 0;
+        pStart = Vec_IntArray(p->vLits);
+        Vec_IntForEachEntry( p->vClauses, End, i )
+        {
+            assert( Vec_IntEntry( p->vCosts, i ) >= 0 );
+            assert( End - Beg <= p->nLutSize );
+            // check the clause
+            for ( k = Beg; k < End; k++ )
+                pStart[k] = lit_neg( pStart[k] );
+            RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            for ( k = Beg; k < End; k++ )
+                pStart[k] = lit_neg( pStart[k] );
+            // the clause holds
+            if ( RetValue == l_False )
+            {
+                Vec_IntWriteEntry( p->vCosts, i, -1 );
+                p->nClauses--;
+            }
+            Beg = End;
+        }
+        assert( End == Vec_IntSize(p->vLits) );
+        if ( p->fVerbose )
+        printf( "Already proved clauses filtered out %d candidate clauses (out of %d).\n", 
+            Vec_IntSize(p->vClauses) - p->nClauses, Vec_IntSize(p->vClauses) );
+    }
+
+    p->fFiltering = 0;
+    if ( p->nClauses > p->nClausesMax )
+    {
+        Fra_ClausSelectClauses( p );
+        p->fFiltering = 1;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Converts AIG into the SAT solver.]
 
   Description []
@@ -630,7 +872,7 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
                 continue;
             }
             assert( Vec_IntEntry( p->vCosts, i ) > 0 );
-            assert( End - Beg < 5 );
+            assert( End - Beg <= p->nLutSize );
 
             for ( k = Beg; k < End; k++ )
                 pStart[k] = lit_neg( pStart[k] );
@@ -760,7 +1002,7 @@ void Fra_ClausSimInfoRecord( Clu_Man_t * p, int * pModel )
 ***********************************************************************/
 int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits )
 {
-    unsigned * pSims[4], uWord;
+    unsigned * pSims[16], uWord;
     int nWords, iVar, i, w;
     for ( i = 0; i < nLits; i++ )
     {
@@ -803,7 +1045,8 @@ int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits )
 int Fra_ClausInductiveClauses( Clu_Man_t * p )
 {
 //    Aig_Obj_t * pObjLi, * pObjLo;
-    int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFail = 0, fFlag;//, Lits[2];
+    int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFlag;//, Lits[2];
+    p->fFail = 0;
 
     // reset the solver
     if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
@@ -839,6 +1082,54 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
             }
         }
 */
+
+
+    // add the proven clauses
+    nLitsTot = 2 * p->pCnf->nVars;
+    pStart = Vec_IntArray(p->vLitsProven);
+    for ( f = 0; f < p->nFrames; f++ )
+    {
+        Beg = 0;
+        Vec_IntForEachEntry( p->vClausesProven, End, i )
+        {
+            assert( End - Beg <= p->nLutSize );
+            // add the clause to all timeframes
+            RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
+            if ( RetValue == 0 )
+            {
+                printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
+                return -1;
+            }
+            Beg = End;
+        }
+        // increment literals
+        for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
+            p->vLitsProven->pArray[i] += nLitsTot;
+    }
+    // return clauses back to normal
+    nLitsTot = (p->nFrames) * nLitsTot;
+    for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
+        p->vLitsProven->pArray[i] -= nLitsTot;
+
+/*
+    // add the proven clauses
+    nLitsTot = 2 * p->pCnf->nVars;
+    pStart = Vec_IntArray(p->vLitsProven);
+    Beg = 0;
+    Vec_IntForEachEntry( p->vClausesProven, End, i )
+    {
+        assert( End - Beg <= p->nLutSize );
+        // add the clause to all timeframes
+        RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
+        if ( RetValue == 0 )
+        {
+            printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
+            return -1;
+        }
+        Beg = End;
+    }
+*/
+    
     // add the clauses
     nLitsTot = 2 * p->pCnf->nVars;
     pStart = Vec_IntArray(p->vLits);
@@ -853,7 +1144,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
                 continue;
             }
             assert( Vec_IntEntry( p->vCosts, i ) > 0 );
-            assert( End - Beg < 5 );
+            assert( End - Beg <= p->nLutSize );
             // add the clause to all timeframes
             RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
             if ( RetValue == 0 )
@@ -887,7 +1178,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
         if ( p->fVerbose )
         printf( " Property fails.  " );
 //        return -2;
-        fFail = 1;
+        p->fFail = 1;
     }
 
 /*
@@ -930,7 +1221,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
             continue;
         }
         assert( Vec_IntEntry( p->vCosts, i ) > 0 );
-        assert( End - Beg < 5 );
+        assert( End - Beg <= p->nLutSize );
 
         if ( Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg) )
         {
@@ -996,8 +1287,8 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
     for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
         p->vLits->pArray[i] -= nLitsTot;
 
-    if ( fFail )
-        return -2;
+//    if ( fFail )
+//        return -2;
     return Counter;
 }
 
@@ -1014,7 +1305,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int fVerbose, int fVeryVerbose )
+Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fVerbose, int fVeryVerbose )
 {
     Clu_Man_t * p;
     p = ALLOC( Clu_Man_t, 1 );
@@ -1023,6 +1314,11 @@ Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClaus
     p->nFrames       = nFrames;
     p->nPref         = nPref;
     p->nClausesMax   = nClausesMax;
+    p->nLutSize      = nLutSize;
+    p->nLevels       = nLevels;
+    p->nCutsMax      = nCutsMax;
+    p->nBatches      = nBatches;
+    p->fStepUp       = fStepUp;
     p->fVerbose      = fVerbose;
     p->fVeryVerbose  = fVeryVerbose;
     p->nSimWords     = 512;//1024;//64;
@@ -1033,6 +1329,9 @@ Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClaus
     p->vClauses      = Vec_IntAlloc( 1<<12 );
     p->vCosts        = Vec_IntAlloc( 1<<12 );
 
+    p->vLitsProven   = Vec_IntAlloc( 1<<14 );
+    p->vClausesProven= Vec_IntAlloc( 1<<12 );
+
     p->nCexesAlloc   = 1024;
     p->vCexes        = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig)+1, p->nCexesAlloc/32 );
     Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
@@ -1055,6 +1354,8 @@ void Fra_ClausFree( Clu_Man_t * p )
     if ( p->vCexes )    Vec_PtrFree( p->vCexes );
     if ( p->vLits )     Vec_IntFree( p->vLits );
     if ( p->vClauses )  Vec_IntFree( p->vClauses );
+    if ( p->vLitsProven )     Vec_IntFree( p->vLitsProven );
+    if ( p->vClausesProven )  Vec_IntFree( p->vClausesProven );
     if ( p->vCosts )    Vec_IntFree( p->vCosts );
     if ( p->pCnf )      Cnf_DataFree( p->pCnf );
     if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
@@ -1062,6 +1363,51 @@ void Fra_ClausFree( Clu_Man_t * p )
     free( p );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Converts AIG into the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausAddToStorage( Clu_Man_t * p )
+{
+    int * pStart; 
+    int Beg, End, Counter, i, k;
+    Beg = 0;
+    Counter = 0;
+    pStart = Vec_IntArray( p->vLits );
+    Vec_IntForEachEntry( p->vClauses, End, i )
+    {
+        if ( Vec_IntEntry( p->vCosts, i ) == -1 )
+        {
+            Beg = End;
+            continue;
+        }
+        assert( Vec_IntEntry( p->vCosts, i ) > 0 );
+        assert( End - Beg <= p->nLutSize );
+        for ( k = Beg; k < End; k++ )
+            Vec_IntPush( p->vLitsProven, pStart[k] );
+        Vec_IntPush( p->vClausesProven, Vec_IntSize(p->vLitsProven) );
+        Beg = End;
+        Counter++;
+    }
+    if ( p->fVerbose )
+    printf( "Added to storage %d proved clauses\n", Counter );
+
+    Vec_IntClear( p->vClauses );
+    Vec_IntClear( p->vLits );
+    Vec_IntClear( p->vCosts );
+    p->nClauses = 0;
+
+    p->fNothingNew = (int)(Counter == 0);
+}
+
 /**Function*************************************************************
 
   Synopsis    [Converts AIG into the SAT solver.]
@@ -1073,16 +1419,16 @@ void Fra_ClausFree( Clu_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
+int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
 {
     Clu_Man_t * p;
     int clk, clkTotal = clock();
-    int Iter, Counter, nPrefOld;
+    int b, Iter, Counter, nPrefOld;
 
     assert( Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
 
     // create the manager
-    p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, fVerbose, fVeryVerbose );
+    p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fVerbose, fVeryVerbose );
 
 clk = clock();
     // derive CNF
@@ -1123,67 +1469,85 @@ clk = clock();
         Fra_ClausFree( p );
         return 1;
     } 
-    // try solving without additional clauses
-    if ( Fra_ClausRunSat( p ) )
+
+
+    for ( b = 0; b < p->nBatches; b++ )
     {
-        printf( "Problem is inductive without strengthening.\n" );
-        Fra_ClausFree( p );
-        return 1;
-    }
-if ( fVerbose )
-{
-PRT( "SAT-ind", clock() - clk );
-}
+//        if ( fVerbose )
+        printf( "*** BATCH %d:  ", b+1 );
+        if ( b && (!p->fFiltering || p->fNothingNew || p->fStepUp) )
+            p->nLutSize++;
+        printf( "Using %d-cuts.\n", p->nLutSize );
+
+        // try solving without additional clauses
+        if ( Fra_ClausRunSat( p ) )
+        {
+            printf( "Problem is inductive without strengthening.\n" );
+            Fra_ClausFree( p );
+            return 1;
+        }
+        if ( fVerbose )
+        {
+        PRT( "SAT-ind", clock() - clk );
+        }
  
-    // collect the candidate inductive clauses using 4-cuts
-clk = clock();
-    nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
-    Fra_ClausProcessClauses( p, fRefs );
-    p->nPref = nPrefOld;
-    p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
+        // collect the candidate inductive clauses using 4-cuts
+        clk = clock();
+        nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
+    //    Fra_ClausProcessClauses( p, fRefs );
+        Fra_ClausProcessClauses2( p, fRefs );
+        p->nPref = nPrefOld;
+        p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
 
-//PRT( "Clauses", clock() - clk );
+    //PRT( "Clauses", clock() - clk );
 
 
-    // check clauses using BMC
-    if ( fBmc ) 
-    {
-clk = clock();
-        Counter = Fra_ClausBmcClauses( p );
-        p->nClauses -= Counter;
-if ( fVerbose )
-{
-        printf( "BMC disproved %d clauses.\n", Counter );
-PRT( "Cla-bmc", clock() - clk );
-}
-    }
+        // check clauses using BMC
+        if ( fBmc ) 
+        {
+            clk = clock();
+            Counter = Fra_ClausBmcClauses( p );
+            p->nClauses -= Counter;
+            if ( fVerbose )
+            {
+                printf( "BMC disproved %d clauses.\n", Counter );
+                PRT( "Cla-bmc", clock() - clk );
+            }
+        }
 
 
-    // prove clauses inductively
-clk = clock();
-    Counter = 1;
-    for ( Iter = 0; Counter > 0; Iter++ )
-    {
-        if ( fVerbose )
-        printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
-        Counter = Fra_ClausInductiveClauses( p );
-        if ( Counter > 0 )
-           p->nClauses -= Counter;
-        if ( fVerbose )
+        // prove clauses inductively
+        clk = clock();
+        Counter = 1;
+        for ( Iter = 0; Counter > 0; Iter++ )
         {
-        printf( "End = %5d. Exs = %5d.  ", p->nClauses, p->nCexes );
-//        printf( "\n" );
-        PRT( "Time", clock() - clk );
+            if ( fVerbose )
+            printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
+            Counter = Fra_ClausInductiveClauses( p );
+            if ( Counter > 0 )
+               p->nClauses -= Counter;
+            if ( fVerbose )
+            {
+            printf( "End = %5d. Exs = %5d.  ", p->nClauses, p->nCexes );
+    //        printf( "\n" );
+            PRT( "Time", clock() - clk );
+            }
+            clk = clock();
         }
-        clk = clock();
+        if ( Counter == -1 )
+            printf( "Fra_Claus(): Internal error.  " );
+        else if ( p->fFail )
+            printf( "Property FAILS during refinement.  " );
+        else
+            printf( "Property HOLDS inductively after strengthening.  " );
+        PRT( "Time  ", clock() - clkTotal );
+
+        if ( !p->fFail )
+            break;
+
+        // add proved clauses to storage
+        Fra_ClausAddToStorage( p );
     }
-    if ( Counter == -1 )
-        printf( "Fra_Claus(): Internal error.  " );
-    else if ( Counter == -2 )
-        printf( "Property FAILS during refinement.  " );
-    else
-        printf( "Property HOLDS inductively after strengthening.  " );
-    PRT( "Time  ", clock() - clkTotal );
 
     // clean the manager
     Fra_ClausFree( p );

src/base/abc/1.txt

+Comparing files abcDfs.c and C:\_PROJECTS\AARON\FRETIME\SRC\BASE\ABC\ABCDFS.C
+***** abcDfs.c
+        return pNode->Level;
+    assert( Abc_ObjIsNode( pNode ) );
+    // if this node is already visited, return
+***** C:\_PROJECTS\AARON\FRETIME\SRC\BASE\ABC\ABCDFS.C
+        return pNode->Level;
+    assert( Abc_ObjIsNode( pNode ) || pNode->Type == ABC_OBJ_CONST1);
+    // if this node is already visited, return
+*****
+
+***** abcDfs.c
+        return pNode->Level;
+    assert( Abc_ObjIsNode( pNode ) );
+    // if this node is already visited, return
+***** C:\_PROJECTS\AARON\FRETIME\SRC\BASE\ABC\ABCDFS.C
+        return pNode->Level;
+    assert( Abc_ObjIsNode( pNode ) || pNode->Type == ABC_OBJ_CONST1);
+    // if this node is already visited, return
+*****
+

src/base/abc/abcDfs.c

@@ -908,7 +908,7 @@ int Abc_NtkLevel_rec( Abc_Obj_t * pNode )
     // skip the PI
     if ( Abc_ObjIsCi(pNode) )
         return pNode->Level;
-    assert( Abc_ObjIsNode( pNode ) );
+    assert( Abc_ObjIsNode( pNode ) || pNode->Type == ABC_OBJ_CONST1);
     // if this node is already visited, return
     if ( Abc_NodeIsTravIdCurrent( pNode ) )
         return pNode->Level;
@@ -946,7 +946,7 @@ int Abc_NtkLevelReverse_rec( Abc_Obj_t * pNode )
     // skip the PI
     if ( Abc_ObjIsCo(pNode) )
         return pNode->Level;
-    assert( Abc_ObjIsNode( pNode ) );
+    assert( Abc_ObjIsNode( pNode ) || pNode->Type == ABC_OBJ_CONST1);
     // if this node is already visited, return
     if ( Abc_NodeIsTravIdCurrent( pNode ) )
         return pNode->Level;

src/base/abci/abc.c

@@ -6392,8 +6392,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
-//    printf( "This command is temporarily disabled.\n" );
-//    return 0;
+    printf( "This command is temporarily disabled.\n" );
+    return 0;
 
     // set defaults
     fVeryVerbose = 0;
@@ -13402,27 +13402,37 @@ int Abc_CommandIndcut( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nFrames;
     int nPref;
     int nClauses;
+    int nLutSize;
+    int nLevels;
+    int nCutsMax;
+    int nBatches;
+    int fStepUp;
     int fBmc;
     int fRegs;
     int fVerbose;
     int fVeryVerbose;
     int c;
-    extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int fBmc, int fRegs, int fVerbose, int fVeryVerbose );
+    extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRegs, int fVerbose, int fVeryVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFrames      = 1;
-    nPref        = 0;
+    nFrames      =    1;
+    nPref        =    0;
     nClauses     = 5000;
-    fBmc         = 1;
-    fRegs        = 1;
-    fVerbose     = 0;
-    fVeryVerbose = 0;
+    nLutSize     =    4;
+    nLevels      =    8;
+    nCutsMax     =   16;
+    nBatches     =    1;
+    fStepUp      =    0;
+    fBmc         =    1;
+    fRegs        =    1;
+    fVerbose     =    0;
+    fVeryVerbose =    0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FPCbrvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FPCMLNBsbrvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -13459,6 +13469,53 @@ int Abc_CommandIndcut( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nClauses < 0 ) 
                 goto usage;
             break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutSize < 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLevels = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLevels < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCutsMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCutsMax < 0 ) 
+                goto usage;
+            break;
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBatches = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBatches < 0 ) 
+                goto usage;
+            break;
+        case 's':
+            fStepUp ^= 1;
+            break;
         case 'b':
             fBmc ^= 1;
             break;
@@ -13492,14 +13549,24 @@ int Abc_CommandIndcut( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
         return 0;
     }
-    Abc_NtkDarClau( pNtk, nFrames, nPref, nClauses, fBmc, fRegs, fVerbose, fVeryVerbose );
+    if ( nLutSize > 12 )
+    {
+        fprintf( stdout, "The cut size should be not exceed 12.\n" );
+        return 0;
+    }
+    Abc_NtkDarClau( pNtk, nFrames, nPref, nClauses, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fBmc, fRegs, fVerbose, fVeryVerbose );
     return 0;
 usage:
-    fprintf( pErr, "usage: indcut [-F num] [-P num] [-C num] [-bvh]\n" );
+    fprintf( pErr, "usage: indcut [-FPCMLNB num] [-bvh]\n" );
     fprintf( pErr, "\t         K-step induction strengthened with cut properties\n" );
     fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFrames );
     fprintf( pErr, "\t-P num : number of time frames in the prefix (0=no prefix) [default = %d]\n", nPref );
     fprintf( pErr, "\t-C num : the max number of clauses to use for strengthening [default = %d]\n", nClauses );
+    fprintf( pErr, "\t-M num : the cut size (2 <= M <= 12) [default = %d]\n", nLutSize );
+    fprintf( pErr, "\t-L num : the max number of levels for cut computation [default = %d]\n", nLevels );
+    fprintf( pErr, "\t-N num : the max number of cuts to compute at a node [default = %d]\n", nCutsMax );
+    fprintf( pErr, "\t-B num : the max number of invariant batches to try [default = %d]\n", nBatches );
+    fprintf( pErr, "\t-s     : toggle increment cut size in each batch [default = %s]\n", fStepUp? "yes": "no" );
     fprintf( pErr, "\t-b     : toggle enabling BMC check [default = %s]\n", fBmc? "yes": "no" );
     fprintf( pErr, "\t-r     : toggle enabling register clauses [default = %s]\n", fRegs? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );

src/base/abci/abcDar.c

@@ -1433,10 +1433,10 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
+int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
 {
     extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose );
-    extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClauses, int fBmc, int fRefs, int fVerbose, int fVeryVerbose );
+    extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fVerbose, int fVeryVerbose );
     Aig_Man_t * pMan;
     if ( Abc_NtkPoNum(pNtk) != 1 )
     {
@@ -1452,7 +1452,7 @@ int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int
     pMan->vFlopNums = NULL;
 
 //    Fra_Clau( pMan, nStepsMax, fVerbose, fVeryVerbose );
-    Fra_Claus( pMan, nFrames, nPref, nClauses, fBmc, fRefs, fVerbose, fVeryVerbose );
+    Fra_Claus( pMan, nFrames, nPref, nClauses, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fBmc, fRefs, fVerbose, fVeryVerbose );
     Aig_ManStop( pMan );
     return 1;
 }

src/opt/fret/fretFlow.c

@@ -59,31 +59,32 @@ void dfsfast_preorder( Abc_Ntk_t *pNtk ) {
 
   // create reverse timing edges for backward traversal
 #if !defined(IGNORE_TIMING)
-  if (maxDelayCon)
+  if (pManMR->maxDelay) {
     Abc_NtkForEachObj( pNtk, pObj, i ) {
       Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, j ) {
-        vTimeIn = FDATA(pNext)->vTimeInEdges;
+        vTimeIn = FDATA(pNext)->vNodes;
         if (!vTimeIn) {
-          vTimeIn = FDATA(pNext)->vTimeInEdges = Vec_PtrAlloc(2);
+          vTimeIn = FDATA(pNext)->vNodes = Vec_PtrAlloc(2);
         }
         Vec_PtrPush(vTimeIn, pObj);
       }
     }
+  }
 #endif
 
   // clear histogram
-  memset(Vec_IntArray(vSinkDistHist), 0, sizeof(int)*Vec_IntSize(vSinkDistHist));
+  memset(Vec_IntArray(pManMR->vSinkDistHist), 0, sizeof(int)*Vec_IntSize(pManMR->vSinkDistHist));
 
   // seed queue : latches, PIOs, and blocks
   Abc_NtkForEachObj( pNtk, pObj, i )
     if (Abc_ObjIsPo(pObj) ||
         Abc_ObjIsLatch(pObj) || 
-        (fIsForward && FTEST(pObj, BLOCK))) {
+        (pManMR->fIsForward && FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask)) {
       Vec_PtrPush(qn, pObj);
       Vec_IntPush(qe, 'r');
       FDATA(pObj)->r_dist = 1;
     } else if (Abc_ObjIsPi(pObj) || 
-               (!fIsForward && FTEST(pObj, BLOCK))) {
+               (!pManMR->fIsForward && FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask)) {
       Vec_PtrPush(qn, pObj);
       Vec_IntPush(qe, 'e');
       FDATA(pObj)->e_dist = 1;
@@ -100,7 +101,7 @@ void dfsfast_preorder( Abc_Ntk_t *pNtk ) {
       d = FDATA(pObj)->r_dist;
 
       // 1. structural edges
-      if (fIsForward) {
+      if (pManMR->fIsForward) {
         Abc_ObjForEachFanin( pObj, pNext, i )
           if (!FDATA(pNext)->e_dist) {
             FDATA(pNext)->e_dist = d+1;
@@ -118,26 +119,26 @@ void dfsfast_preorder( Abc_Ntk_t *pNtk ) {
       if (d == 1) continue;
 
       // 2. reverse edges (forward retiming only)
-      if (fIsForward) {
+      if (pManMR->fIsForward) {
         Abc_ObjForEachFanout( pObj, pNext, i )
           if (!FDATA(pNext)->r_dist && !Abc_ObjIsLatch(pNext)) {
             FDATA(pNext)->r_dist = d+1;
             Vec_PtrPush(qn, pNext);
             Vec_IntPush(qe, 'r');
           }          
-      }
 
-      // 3. timimg edges (reverse)
+      // 3. timimg edges (forward retiming only)
 #if !defined(IGNORE_TIMING)
-      if (maxDelayCon && FDATA(pObj)->vTimeInEdges)
-        Vec_PtrForEachEntry( FDATA(pObj)->vTimeInEdges, pNext, i ) {
-          if (!FDATA(pNext)->r_dist) {
-            FDATA(pNext)->r_dist = d+1;
-            Vec_PtrPush(qn, pNext);
-            Vec_IntPush(qe, 'r');
+        if (pManMR->maxDelay && FDATA(pObj)->vNodes)
+          Vec_PtrForEachEntry( FDATA(pObj)->vNodes, pNext, i ) {
+            if (!FDATA(pNext)->r_dist) {
+              FDATA(pNext)->r_dist = d+1;
+              Vec_PtrPush(qn, pNext);
+              Vec_IntPush(qe, 'r');
+            }
           }
-        }
 #endif
+      }
       
     } else { // if 'e'
       if (Abc_ObjIsLatch(pObj)) continue;
@@ -152,39 +153,52 @@ void dfsfast_preorder( Abc_Ntk_t *pNtk ) {
       }
 
       // 2. reverse edges (backward retiming only)
-      if (!fIsForward) {
+      if (!pManMR->fIsForward) {
         Abc_ObjForEachFanin( pObj, pNext, i )
           if (!FDATA(pNext)->e_dist && !Abc_ObjIsLatch(pNext)) {
             FDATA(pNext)->e_dist = d+1;
             Vec_PtrPush(qn, pNext);
             Vec_IntPush(qe, 'e');
           }  
+
+      // 3. timimg edges (backward retiming only)
+#if !defined(IGNORE_TIMING)
+        if (pManMR->maxDelay && FDATA(pObj)->vNodes)
+          Vec_PtrForEachEntry( FDATA(pObj)->vNodes, pNext, i ) {
+            if (!FDATA(pNext)->e_dist) {
+              FDATA(pNext)->e_dist = d+1;
+              Vec_PtrPush(qn, pNext);
+              Vec_IntPush(qe, 'e');
+            }
+          }
+#endif
       }
     }
   }
  
-  // create reverse timing edges for backward traversal
+  // free time edges
 #if !defined(IGNORE_TIMING)
-  if (maxDelayCon)
+  if (pManMR->maxDelay) {
     Abc_NtkForEachObj( pNtk, pObj, i ) {
-      vTimeIn = FDATA(pObj)->vTimeInEdges;
+      vTimeIn = FDATA(pObj)->vNodes;
       if (vTimeIn) {
         Vec_PtrFree(vTimeIn);
-        FDATA(pObj)->vTimeInEdges = 0;
+        FDATA(pObj)->vNodes = 0;
       }
     }
+  }
 #endif
 
   Abc_NtkForEachObj( pNtk, pObj, i ) {
-    Vec_IntAddToEntry(vSinkDistHist, FDATA(pObj)->r_dist, 1);
-    Vec_IntAddToEntry(vSinkDistHist, FDATA(pObj)->e_dist, 1);
+    Vec_IntAddToEntry(pManMR->vSinkDistHist, FDATA(pObj)->r_dist, 1);
+    Vec_IntAddToEntry(pManMR->vSinkDistHist, FDATA(pObj)->e_dist, 1);
 
 #ifdef DEBUG_PREORDER
     printf("node %d\t: r=%d\te=%d\n", Abc_ObjId(pObj), FDATA(pObj)->r_dist, FDATA(pObj)->e_dist);
 #endif
   }
 
-  printf("\t\tpre-ordered (max depth=%d)\n", d+1);
+  // printf("\t\tpre-ordered (max depth=%d)\n", d+1);
 
   // deallocate
   Vec_PtrFree( qn );
@@ -195,11 +209,13 @@ int dfsfast_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   int i;
   Abc_Obj_t *pNext;
   
-  if (fSinkDistTerminate) return 0;
+  if (pManMR->fSinkDistTerminate) return 0;
 
-  if(FTEST(pObj, BLOCK) ||
+  // have we reached the sink?
+  if(FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask ||
      Abc_ObjIsPi(pObj)) {
-    assert(!fIsForward);
+    assert(pPred);
+    assert(!pManMR->fIsForward);
     return 1;
   }
 
@@ -210,7 +226,7 @@ int dfsfast_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
 #endif  
 
   // 1. structural edges
-  if (fIsForward)
+  if (pManMR->fIsForward)
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       if (!FTEST(pNext, VISITED_R) &&
           FDIST(pObj, e, pNext, r) &&
@@ -237,7 +253,7 @@ int dfsfast_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
     goto not_found;
 
   // 2. reverse edges (backward retiming only)
-  if (!fIsForward) { 
+  if (!pManMR->fIsForward) { 
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       if (!FTEST(pNext, VISITED_E) &&
           FDIST(pObj, e, pNext, e) &&
@@ -248,6 +264,21 @@ int dfsfast_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
         goto found;
       }
     }
+
+  // 3. timing edges (backward retiming only)
+#if !defined(IGNORE_TIMING)
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
+        if (!FTEST(pNext, VISITED_E) &&
+            FDIST(pObj, e, pNext, e) &&
+            dfsfast_e(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+          printf("o");
+#endif
+          goto found;
+        }
+      }
+#endif
   }
   
   // unwind
@@ -281,7 +312,7 @@ int dfsfast_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   int i;
   Abc_Obj_t *pNext, *pOldPred;
 
-  if (fSinkDistTerminate) return 0;
+  if (pManMR->fSinkDistTerminate) return 0;
 
 #ifdef DEBUG_VISITED
   printf("(%dr=%d) ", Abc_ObjId(pObj), FDATA(pObj)->r_dist);
@@ -289,8 +320,8 @@ int dfsfast_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
 
   // have we reached the sink?
   if (Abc_ObjIsLatch(pObj) ||
-      Abc_ObjIsPo(pObj) || 
-      (fIsForward && FTEST(pObj, BLOCK))) {
+      (pManMR->fIsForward && Abc_ObjIsPo(pObj)) || 
+      (pManMR->fIsForward && FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask)) {
     assert(pPred);
     return 1;
   }
@@ -330,7 +361,7 @@ int dfsfast_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   }
  
   // 2. reverse edges (forward retiming only)
-  if (fIsForward) {
+  if (pManMR->fIsForward) {
     Abc_ObjForEachFanin( pObj, pNext, i ) {
       if (!FTEST(pNext, VISITED_R) &&
           FDIST(pObj, r, pNext, r) &&
@@ -342,22 +373,22 @@ int dfsfast_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
         goto found;
       }
     }
-  }
   
-  // 3. timing edges
+  // 3. timing edges (forward retiming only)
 #if !defined(IGNORE_TIMING)
-  if (maxDelayCon) 
-    Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
-      if (!FTEST(pNext, VISITED_R) &&
-          FDIST(pObj, r, pNext, r) &&
-          dfsfast_r(pNext, pPred)) {
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
+        if (!FTEST(pNext, VISITED_R) &&
+            FDIST(pObj, r, pNext, r) &&
+            dfsfast_r(pNext, pPred)) {
 #ifdef DEBUG_PRINT_FLOWS
-        printf("o");
+          printf("o");
 #endif
-        goto found;
+          goto found;
+        }
       }
-    }
 #endif
+  }
   
   FUNSET(pObj, VISITED_R);
   dfsfast_r_retreat(pObj);
@@ -379,7 +410,7 @@ dfsfast_e_retreat(Abc_Obj_t *pObj) {
   int adj_dist, min_dist = MAX_DIST;
   
   // 1. structural edges
-  if (fIsForward)
+  if (pManMR->fIsForward)
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       adj_dist = FDATA(pNext)->r_dist;
       if (adj_dist) min_dist = MIN(min_dist, adj_dist);
@@ -399,11 +430,20 @@ dfsfast_e_retreat(Abc_Obj_t *pObj) {
   }
 
   // 3. reverse edges (backward retiming only)
-  if (!fIsForward) {
+  if (!pManMR->fIsForward) {
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       adj_dist = FDATA(pNext)->e_dist;
       if (adj_dist) min_dist = MIN(min_dist, adj_dist);
     }
+
+  // 4. timing edges (backward retiming only)
+#if !defined(IGNORE_TIMING)
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
+        adj_dist = FDATA(pNext)->e_dist;
+        if (adj_dist) min_dist = MIN(min_dist, adj_dist);
+      }
+#endif
   }
 
  update:
@@ -412,12 +452,12 @@ dfsfast_e_retreat(Abc_Obj_t *pObj) {
   // printf("[%de=%d->%d] ", Abc_ObjId(pObj), old_dist, min_dist+1);
   FDATA(pObj)->e_dist = min_dist;
 
-  assert(min_dist < Vec_IntSize(vSinkDistHist));
-  h = Vec_IntArray(vSinkDistHist);
+  assert(min_dist < Vec_IntSize(pManMR->vSinkDistHist));
+  h = Vec_IntArray(pManMR->vSinkDistHist);
   h[old_dist]--;
   h[min_dist]++;
   if (!h[old_dist]) {
-    fSinkDistTerminate = 1;
+    pManMR->fSinkDistTerminate = 1;
   }
 }
 
@@ -440,34 +480,34 @@ dfsfast_r_retreat(Abc_Obj_t *pObj) {
   }
 
   // 2. reverse edges (forward retiming only)
-  if (fIsForward) {
+  if (pManMR->fIsForward) {
     Abc_ObjForEachFanin( pObj, pNext, i )
       if (!Abc_ObjIsLatch(pNext)) {
         adj_dist = FDATA(pNext)->r_dist;
         if (adj_dist) min_dist = MIN(min_dist, adj_dist);
       }
-  }
 
-  // 3. timing edges
+  // 3. timing edges (forward retiming only)
 #if !defined(IGNORE_TIMING)
-  if (maxDelayCon) 
-    Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
-      adj_dist = FDATA(pNext)->r_dist;
-      if (adj_dist) min_dist = MIN(min_dist, adj_dist);
-    }
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
+        adj_dist = FDATA(pNext)->r_dist;
+        if (adj_dist) min_dist = MIN(min_dist, adj_dist);
+      }
 #endif
+  }
 
   ++min_dist;
   if (min_dist >= MAX_DIST) min_dist = 0;
   //printf("[%dr=%d->%d] ", Abc_ObjId(pObj), old_dist, min_dist+1);
   FDATA(pObj)->r_dist = min_dist;
 
-  assert(min_dist < Vec_IntSize(vSinkDistHist));
-  h = Vec_IntArray(vSinkDistHist);
+  assert(min_dist < Vec_IntSize(pManMR->vSinkDistHist));
+  h = Vec_IntArray(pManMR->vSinkDistHist);
   h[old_dist]--;
   h[min_dist]++;
   if (!h[old_dist]) {
-    fSinkDistTerminate = 1;
+    pManMR->fSinkDistTerminate = 1;
   }
 }
 
@@ -487,8 +527,10 @@ int dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   int i;
   Abc_Obj_t *pNext;
   
-  if (FTEST(pObj, BLOCK) || Abc_ObjIsPi(pObj)) {
-    assert(!fIsForward);
+  if (FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask || 
+      Abc_ObjIsPi(pObj)) {
+    assert(pPred);
+    assert(!pManMR->fIsForward);
     return 1;
   }
 
@@ -497,7 +539,7 @@ int dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   // printf(" %de\n", Abc_ObjId(pObj));
   
   // 1. structural edges
-  if (fIsForward)
+  if (pManMR->fIsForward)
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       if (!FTEST(pNext, VISITED_R) &&
           dfsplain_r(pNext, pPred)) {
@@ -521,8 +563,8 @@ int dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   if (Abc_ObjIsLatch(pObj))
     return 0;
 
-  // 2. follow reverse edges
-  if (!fIsForward) { // reverse retiming only
+  // 2. reverse edges (backward retiming only)
+  if (!pManMR->fIsForward) {
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       if (!FTEST(pNext, VISITED_E) &&
           dfsplain_e(pNext, pPred)) {
@@ -532,6 +574,20 @@ int dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
         goto found;
       }
     }
+
+  // 3. timing edges (backward retiming only)
+#if !defined(IGNORE_TIMING)
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
+        if (!FTEST(pNext, VISITED_E) &&
+            dfsplain_e(pNext, pPred)) {
+#ifdef DEBUG_PRINT_FLOWS
+          printf("o");
+#endif
+          goto found;
+        }
+      }
+#endif
   }
   
   // unwind
@@ -562,8 +618,8 @@ int dfsplain_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
 
   // have we reached the sink?
   if (Abc_ObjIsLatch(pObj) || 
-      Abc_ObjIsPo(pObj) || 
-      (fIsForward && FTEST(pObj, BLOCK))) {
+      (pManMR->fIsForward && Abc_ObjIsPo(pObj)) || 
+      (pManMR->fIsForward && FTEST(pObj, BLOCK_OR_CONS) & pManMR->constraintMask)) {
     assert(pPred);
     return 1;
   }
@@ -603,7 +659,7 @@ int dfsplain_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
   }
  
   // 2. follow reverse edges
-  if (fIsForward) { // forward retiming only
+  if (pManMR->fIsForward) { // forward retiming only
     Abc_ObjForEachFanin( pObj, pNext, i ) {
       if (!FTEST(pNext, VISITED_R) &&
           !Abc_ObjIsLatch(pNext) &&
@@ -614,21 +670,21 @@ int dfsplain_r( Abc_Obj_t *pObj, Abc_Obj_t *pPred ) {
         goto found;
       }
     }
-  }
   
-  // 3. follow timing constraints
+  // 3. timing edges (forward only)
 #if !defined(IGNORE_TIMING)
-  if (maxDelayCon) 
-    Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
-      if (!FTEST(pNext, VISITED_R) &&
-          dfsplain_r(pNext, pPred)) {
+    if (pManMR->maxDelay) 
+      Vec_PtrForEachEntry( FTIMEEDGES(pObj), pNext, i) {
+        if (!FTEST(pNext, VISITED_R) &&
+            dfsplain_r(pNext, pPred)) {
 #ifdef DEBUG_PRINT_FLOWS
-        printf("o");
+          printf("o");
 #endif
-        goto found;
+          goto found;
+        }
       }
-    }
 #endif
+  }
   
   return 0;
 

src/opt/fret/fretInit.c

@@ -22,6 +22,7 @@
 #include "vec.h"
 #include "io.h"
 #include "fretime.h"
+#include "mio.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION PROTOTYPES                          ///
@@ -36,9 +37,6 @@ static Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj,
 static void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj );
 static void Abc_FlowRetime_SimulateSop( Abc_Obj_t * pObj, char *pSop );
 
-Abc_Ntk_t *pInitNtk;
-int        fSolutionIsDc;
-
 extern void * Abc_FrameReadLibGen();                    
 extern Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup );
 
@@ -62,9 +60,9 @@ extern Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup );
 void
 Abc_FlowRetime_InitState( Abc_Ntk_t * pNtk ) {
 
-  if (!fComputeInitState) return;
+  if (!pManMR->fComputeInitState) return;
 
-  if (fIsForward)
+  if (pManMR->fIsForward)
     Abc_FlowRetime_UpdateForwardInit( pNtk );
   else {
     Abc_FlowRetime_UpdateBackwardInit( pNtk );
@@ -118,7 +116,7 @@ void Abc_FlowRetime_UpdateForwardInit( Abc_Ntk_t * pNtk ) {
   Abc_Obj_t *pObj, *pFanin;
   int i;
 
-  printf("\t\tupdating init state\n");
+  vprintf("\t\tupdating init state\n");
 
   Abc_NtkIncrementTravId( pNtk );
 
@@ -195,7 +193,7 @@ static inline void Abc_FlowRetime_SetInitValue( Abc_Obj_t * pObj,
 void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
   Abc_Ntk_t *pNtk = Abc_ObjNtk(pObj);
   Abc_Obj_t * pFanin;
-  int i, j, rAnd, rOr, rVar, dcAnd, dcOr, dcVar, v;
+  int i, rAnd, rVar, dcAnd, dcVar;
   DdManager * dd = pNtk->pManFunc;
   DdNode *pBdd = pObj->pData, *pVar;
   
@@ -206,7 +204,7 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
     Abc_FlowRetime_SetInitValue(pObj, 1, 0);
     return;
   }
-  if (!Abc_NtkIsStrash( pNtk ))
+  if (!Abc_NtkIsStrash( pNtk ) && Abc_ObjIsNode(pObj)) {
     if (Abc_NodeIsConst0(pObj)) {
       Abc_FlowRetime_SetInitValue(pObj, 0, 0);
       return;
@@ -214,6 +212,7 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
       Abc_FlowRetime_SetInitValue(pObj, 1, 0);
       return;
     }
+  }
   
   // (ii) terminal nodes
   if (!Abc_ObjIsNode(pObj)) {
@@ -229,7 +228,7 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
 
   // ------ SOP network
   if ( Abc_NtkHasSop( pNtk )) {
-    Abc_FlowRetime_SimulateSop( pObj, Abc_ObjData(pObj) );
+    Abc_FlowRetime_SimulateSop( pObj, (char *)Abc_ObjData(pObj) );
     return;
   }
 
@@ -242,12 +241,12 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
     // do nothing for X values
     Abc_ObjForEachFanin(pObj, pFanin, i) {
       pVar = Cudd_bddIthVar( dd, i );
-      if (FTEST(pFanin, INIT_CARE))
-        if (FTEST(pFanin, INIT_0)) {
+      if (FTEST(pFanin, INIT_CARE)) {
+        if (FTEST(pFanin, INIT_0))
           pBdd = Cudd_Cofactor( dd, pBdd, Cudd_Not(pVar) ); 
-        } else {
+        else
           pBdd = Cudd_Cofactor( dd, pBdd, pVar ); 
-        }
+      }
     }
 
     // if function has not been reduced to 
@@ -285,7 +284,7 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
 
   // ------ MAPPED network
   else if ( Abc_NtkHasMapping( pNtk )) {
-    Abc_FlowRetime_SimulateSop( pObj, Mio_GateReadSop(pObj->pData) );
+    Abc_FlowRetime_SimulateSop( pObj, (char *)Mio_GateReadSop(pObj->pData) );
     return;
   }
 
@@ -307,7 +306,7 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
 void Abc_FlowRetime_SimulateSop( Abc_Obj_t * pObj, char *pSop ) {
   Abc_Obj_t * pFanin;
   char *pCube;
-  int i, j, rAnd, rOr, rVar, dcAnd, dcOr, dcVar, v;
+  int i, j, rAnd, rOr, rVar, dcAnd, dcOr, v;
 
   assert( pSop && !Abc_SopIsExorType(pSop) );
       
@@ -363,14 +362,14 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
 
   // create the network used for the initial state computation
   if (Abc_NtkHasMapping(pNtk))
-    pInitNtk = Abc_NtkAlloc( pNtk->ntkType, ABC_FUNC_SOP, 1 );
+    pManMR->pInitNtk = Abc_NtkAlloc( pNtk->ntkType, ABC_FUNC_SOP, 1 );
   else
-    pInitNtk = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+    pManMR->pInitNtk = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
 
   // mitre inputs
   Abc_NtkForEachLatch( pNtk, pLatch, i ) {
     // map latch to initial state network
-    pPi = Abc_NtkCreatePi( pInitNtk );
+    pPi = Abc_NtkCreatePi( pManMR->pInitNtk );
 
     // has initial state requirement?
     if (Abc_LatchIsInit0(pLatch)) {
@@ -378,7 +377,7 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
       if (Abc_NtkHasAig(pNtk))
         pObj = Abc_ObjNot( pPi );
       else
-        pObj = Abc_NtkCreateNodeInv( pInitNtk, pPi );
+        pObj = Abc_NtkCreateNodeInv( pManMR->pInitNtk, pPi );
 
       Vec_PtrPush(vObj, pObj);
     }
@@ -392,22 +391,24 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
 
   // are there any nodes not DC?
   if (!Vec_PtrSize(vObj)) {
-    fSolutionIsDc = 1;
+    pManMR->fSolutionIsDc = 1;
     return;
   } else 
-    fSolutionIsDc = 0;
+    pManMR->fSolutionIsDc = 0;
 
   // mitre output
   if (Abc_NtkHasAig(pNtk)) {
     // create AND-by-AND
     pObj = Vec_PtrPop( vObj );
     while( Vec_PtrSize(vObj) )
-      pObj = Abc_AigAnd( pInitNtk->pManFunc, pObj, Vec_PtrPop( vObj ) ); 
+      pObj = Abc_AigAnd( pManMR->pInitNtk->pManFunc, pObj, Vec_PtrPop( vObj ) ); 
   } else
     // create n-input AND gate
-    pObj = Abc_NtkCreateNodeAnd( pInitNtk, vObj );
+    pObj = Abc_NtkCreateNodeAnd( pManMR->pInitNtk, vObj );
+
+  Abc_ObjAddFanin( Abc_NtkCreatePo( pManMR->pInitNtk ), pObj );
 
-  Abc_ObjAddFanin( Abc_NtkCreatePo( pInitNtk ), pObj );
+  Vec_PtrFree( vObj );
 }
 
 
@@ -422,27 +423,26 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
+int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   int i;
   Abc_Obj_t *pObj, *pInitObj;
-  Abc_Ntk_t *pRestrNtk;
   Vec_Ptr_t *vDelete = Vec_PtrAlloc(0);
   int result;
 
-  assert(pInitNtk);
+  assert(pManMR->pInitNtk);
 
   // is the solution entirely DC's?
-  if (fSolutionIsDc) {
-    Abc_NtkDelete(pInitNtk);
+  if (pManMR->fSolutionIsDc) {
+    Abc_NtkDelete(pManMR->pInitNtk);
     Vec_PtrFree(vDelete);
     Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj );
-    printf("\tno init state computation: all-don't-care solution\n");
-    return;
+    vprintf("\tno init state computation: all-don't-care solution\n");
+    return 1;
   }
 
   // check that network is combinational
   // mark superfluous BI nodes for deletion
-  Abc_NtkForEachObj( pInitNtk, pObj, i ) {
+  Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i ) {
     assert(!Abc_ObjIsLatch(pObj));
     assert(!Abc_ObjIsBo(pObj));
     
@@ -460,34 +460,36 @@ void Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   Vec_PtrFree(vDelete);
 
   // do some final cleanup on the network
-  Abc_NtkAddDummyPoNames(pInitNtk);
-  Abc_NtkAddDummyPiNames(pInitNtk);
-  if (Abc_NtkIsLogic(pInitNtk))
-    Abc_NtkCleanup(pInitNtk, 0);
-  else if (Abc_NtkIsStrash(pInitNtk)) {  
-    Abc_NtkReassignIds(pInitNtk);
+  Abc_NtkAddDummyPoNames(pManMR->pInitNtk);
+  Abc_NtkAddDummyPiNames(pManMR->pInitNtk);
+  if (Abc_NtkIsLogic(pManMR->pInitNtk))
+    Abc_NtkCleanup(pManMR->pInitNtk, 0);
+  else if (Abc_NtkIsStrash(pManMR->pInitNtk)) {  
+    Abc_NtkReassignIds(pManMR->pInitNtk);
   }
   
-  printf("\tsolving for init state (%d nodes)... ", Abc_NtkObjNum(pInitNtk));
+  vprintf("\tsolving for init state (%d nodes)... ", Abc_NtkObjNum(pManMR->pInitNtk));
   fflush(stdout);
 
   // convert SOPs to BDD
-  if (Abc_NtkHasSop(pInitNtk))
-    Abc_NtkSopToBdd( pInitNtk );
+  if (Abc_NtkHasSop(pManMR->pInitNtk))
+    Abc_NtkSopToBdd( pManMR->pInitNtk );
   
   // solve
-  result = Abc_NtkMiterSat( pInitNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
+  result = Abc_NtkMiterSat( pManMR->pInitNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
 
-  if (!result) printf("SUCCESS\n");
-  else  {
-    printf("FAILURE\n");  
-    printf("\tsetting all initial states to don't-care\n");
+  if (!result) { 
+    vprintf("SUCCESS\n");
+  } else  {    
+    vprintf("FAILURE\n");
+    printf("WARNING: no equivalent init state. setting all initial states to don't-cares\n");
     Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj );
-    return;
+    Abc_NtkDelete(pManMR->pInitNtk);
+    return 0;
   }
 
   // clear initial values, associate PIs to latches
-  Abc_NtkForEachPi( pInitNtk, pInitObj, i ) Abc_ObjSetCopy( pInitObj, NULL );
+  Abc_NtkForEachPi( pManMR->pInitNtk, pInitObj, i ) Abc_ObjSetCopy( pInitObj, NULL );
   Abc_NtkForEachLatch( pNtk, pObj, i ) {
     pInitObj = Abc_ObjData( pObj );
     assert( Abc_ObjIsPi( pInitObj ));
@@ -496,10 +498,10 @@ void Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   }
 
   // copy solution from PIs to latches
-  assert(pInitNtk->pModel);
-  Abc_NtkForEachPi( pInitNtk, pInitObj, i ) {
+  assert(pManMR->pInitNtk->pModel);
+  Abc_NtkForEachPi( pManMR->pInitNtk, pInitObj, i ) {
     if ((pObj = Abc_ObjCopy( pInitObj ))) {
-      if ( pInitNtk->pModel[i] )
+      if ( pManMR->pInitNtk->pModel[i] )
         Abc_LatchSetInit1( pObj );
       else
         Abc_LatchSetInit0( pObj );
@@ -512,7 +514,9 @@ void Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
 #endif
 
   // deallocate
-  Abc_NtkDelete( pInitNtk );
+  Abc_NtkDelete( pManMR->pInitNtk );
+
+  return 1;
 }
 
 
@@ -528,11 +532,10 @@ void Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
 
 ***********************************************************************/
 void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) {
-  Abc_Obj_t *pOrigObj,  *pOrigFanin, *pInitObj, *pInitFanin;
+  Abc_Obj_t *pOrigObj,  *pInitObj;
   Vec_Ptr_t *vBo = Vec_PtrAlloc(100);
   Vec_Ptr_t *vOldPis = Vec_PtrAlloc(100);
-  void *pData;
-  int i, j;
+  int i;
 
   // remove PIs from network (from BOs)
   Abc_NtkForEachObj( pNtk, pOrigObj, i )
@@ -624,20 +627,20 @@ Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj,
       if (!pOrigObj->pData) {
         // assume terminal...
         assert(Abc_ObjFaninNum(pOrigObj) == 1);
-        pInitObj = Abc_NtkCreateNodeBuf( pInitNtk, NULL );
+        pInitObj = Abc_NtkCreateNodeBuf( pManMR->pInitNtk, NULL );
       } else {
-        pInitObj = Abc_NtkCreateObj( pInitNtk, Abc_ObjType(pOrigObj) );
+        pInitObj = Abc_NtkCreateObj( pManMR->pInitNtk, Abc_ObjType(pOrigObj) );
         pData = Mio_GateReadSop(pOrigObj->pData);
         assert( Abc_SopGetVarNum(pData) == Abc_ObjFaninNum(pOrigObj) );
 
-        pInitObj->pData = Abc_SopRegister( pInitNtk->pManFunc, pData );
+        pInitObj->pData = Abc_SopRegister( pManMR->pInitNtk->pManFunc, pData );
       }
     } else {
       pData = Abc_ObjCopy( pOrigObj );   // save ptr to flow data    
       if (Abc_NtkIsStrash( pNtk ) && Abc_AigNodeIsConst( pOrigObj ))
-        pInitObj = Abc_AigConst1( pInitNtk );
+        pInitObj = Abc_AigConst1( pManMR->pInitNtk );
       else
-        pInitObj = Abc_NtkDupObj( pInitNtk, pOrigObj, 0 );
+        pInitObj = Abc_NtkDupObj( pManMR->pInitNtk, pOrigObj, 0 );
       Abc_ObjSetCopy( pOrigObj, pData ); // restore ptr to flow data
 
       // copy complementation
@@ -695,7 +698,7 @@ void Abc_FlowRetime_VerifyBackwardInit( Abc_Ntk_t * pNtk ) {
   Abc_Obj_t *pObj, *pFanin;
   int i;
 
-  printf("\t\tupdating init state\n");
+  vprintf("\t\tupdating init state\n");
 
   Abc_NtkIncrementTravId( pNtk );
 
@@ -741,3 +744,19 @@ void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj ) {
   
   Abc_FlowRetime_SimulateNode( pObj );
 }
+
+
+/**Function*************************************************************
+
+  Synopsis    [Constrains backward retiming for initializability.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_ConstrainInit( ) {
+  // unimplemented
+}

src/opt/fret/fretMain.c

@@ -28,9 +28,10 @@
 
 static void Abc_FlowRetime_AddDummyFanin( Abc_Obj_t * pObj );
 
+static void Abc_FlowRetime_MainLoop( );
+
 static void Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk );
 static void Abc_FlowRetime_MarkReachable_rec( Abc_Obj_t * pObj, char end );
-static int  Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk );
 static int  Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk );
 static void  Abc_FlowRetime_RemoveLatchBubbles( Abc_Obj_t * pLatch );
 
@@ -40,12 +41,12 @@ static int  Abc_FlowRetime_VerifyPathLatencies_rec( Abc_Obj_t * pObj, int markD
 extern void Abc_NtkMarkCone_rec( Abc_Obj_t * pObj, int fForward );
 extern Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup );
 
-int         fIsForward, fComputeInitState;
-int         fSinkDistTerminate;
-Vec_Int_t  *vSinkDistHist;
-int         maxDelayCon;
+void
+print_node3(Abc_Obj_t *pObj);
+
+MinRegMan_t *pManMR;
 
-int         fPathError = 0;
+int          fPathError = 0;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -63,53 +64,64 @@ int         fPathError = 0;
 
 ***********************************************************************/
 Abc_Ntk_t *
-Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState_,
+Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
                        int fForwardOnly, int fBackwardOnly, int nMaxIters,
-                       int maxDelay ) {
+                       int maxDelay, int fFastButConservative ) {
 
-  int i, j, nNodes, nLatches, flow, last, cut;
-  int iteration = 0;
-  Flow_Data_t *pDataArray;
+  int i;
   Abc_Obj_t   *pObj, *pNext;
 
-  fComputeInitState = fComputeInitState_;
+  // create manager
+  pManMR = ALLOC( MinRegMan_t, 1 );
+
+  pManMR->pNtk = pNtk;
+  pManMR->fVerbose = fVerbose;
+  pManMR->fComputeInitState = fComputeInitState;
+  pManMR->fGuaranteeInitState = 0;
+  pManMR->fForwardOnly = fForwardOnly;
+  pManMR->fBackwardOnly = fBackwardOnly;
+  pManMR->nMaxIters = nMaxIters;
+  pManMR->maxDelay = maxDelay;
+  pManMR->fComputeInitState = fComputeInitState;
+  pManMR->fConservTimingOnly = fFastButConservative;
+  pManMR->vNodes = Vec_PtrAlloc(100);
 
-  printf("Flow-based minimum-register retiming...\n");  
+  vprintf("Flow-based minimum-register retiming...\n");  
 
   if (!Abc_NtkHasOnlyLatchBoxes(pNtk)) {
     printf("\tERROR: Can not retime with black/white boxes\n");
     return pNtk;
   }
 
-  maxDelayCon = maxDelay;
-  if (maxDelayCon) {
-    printf("\tmax delay constraint = %d\n", maxDelayCon);
-    if (maxDelayCon < (i = Abc_NtkLevel(pNtk))) {
+  if (maxDelay) {
+    vprintf("\tmax delay constraint = %d\n", maxDelay);
+    if (maxDelay < (i = Abc_NtkLevel(pNtk))) {
       printf("ERROR: max delay constraint must be > current max delay (%d)\n", i);
       return pNtk;
     }
   }
 
   // print info about type of network
-  printf("\tnetlist type = ");
-  if (Abc_NtkIsNetlist( pNtk )) printf("netlist/");
-  else if (Abc_NtkIsLogic( pNtk )) printf("logic/");
-  else if (Abc_NtkIsStrash( pNtk )) printf("strash/");
-  else printf("***unknown***/");
-  if (Abc_NtkHasSop( pNtk )) printf("sop\n");
-  else if (Abc_NtkHasBdd( pNtk )) printf("bdd\n");
-  else if (Abc_NtkHasAig( pNtk )) printf("aig\n");
-  else if (Abc_NtkHasMapping( pNtk )) printf("mapped\n");
-  else printf("***unknown***\n");
-
-  printf("\tinitial reg count = %d\n", Abc_NtkLatchNum(pNtk));
+  vprintf("\tnetlist type = ");
+  if (Abc_NtkIsNetlist( pNtk )) { vprintf("netlist/"); }
+  else if (Abc_NtkIsLogic( pNtk )) { vprintf("logic/"); }
+  else if (Abc_NtkIsStrash( pNtk )) { vprintf("strash/"); }
+  else { vprintf("***unknown***/"); }
+  if (Abc_NtkHasSop( pNtk )) { vprintf("sop\n"); }
+  else if (Abc_NtkHasBdd( pNtk )) { vprintf("bdd\n"); }
+  else if (Abc_NtkHasAig( pNtk )) { vprintf("aig\n"); }
+  else if (Abc_NtkHasMapping( pNtk )) { vprintf("mapped\n"); }
+  else { vprintf("***unknown***\n"); }
+
+  vprintf("\tinitial reg count = %d\n", Abc_NtkLatchNum(pNtk));
+  vprintf("\tinitial levels = %d\n", Abc_NtkLevel(pNtk));
 
   // remove bubbles from latch boxes
-  Abc_FlowRetime_PrintInitStateInfo(pNtk);
-  printf("\tpushing bubbles out of latch boxes\n");
+  if (pManMR->fVerbose) Abc_FlowRetime_PrintInitStateInfo(pNtk);
+  vprintf("\tpushing bubbles out of latch boxes\n");
   Abc_NtkForEachLatch( pNtk, pObj, i )
     Abc_FlowRetime_RemoveLatchBubbles(pObj);
-  Abc_FlowRetime_PrintInitStateInfo(pNtk);
+  if (pManMR->fVerbose) Abc_FlowRetime_PrintInitStateInfo(pNtk);
 
   // check for box inputs/outputs
   Abc_NtkForEachLatch( pNtk, pObj, i ) {
@@ -129,100 +141,200 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState_,
     assert(!Abc_ObjFaninC0(pNext));
   }
 
-  nLatches = Abc_NtkLatchNum( pNtk );
-  nNodes = Abc_NtkObjNumMax( pNtk )+1;
+  pManMR->nLatches = Abc_NtkLatchNum( pNtk );
+  pManMR->nNodes = Abc_NtkObjNumMax( pNtk )+1;
    
   // build histogram
-  vSinkDistHist = Vec_IntStart( nNodes*2+10 );
+  pManMR->vSinkDistHist = Vec_IntStart( pManMR->nNodes*2+10 );
+
+  // initialize timing
+  if (maxDelay)
+    Abc_FlowRetime_InitTiming( pNtk );
 
   // create Flow_Data structure
-  pDataArray = (Flow_Data_t *)malloc(sizeof(Flow_Data_t)*nNodes);
-  memset(pDataArray, 0, sizeof(Flow_Data_t)*nNodes);
+  pManMR->pDataArray = ALLOC( Flow_Data_t, pManMR->nNodes );
+  Abc_FlowRetime_ClearFlows( 1 );
   Abc_NtkForEachObj( pNtk, pObj, i )
-    Abc_ObjSetCopy( pObj, (void *)(&pDataArray[i]) );
+    Abc_ObjSetCopy( pObj, (void *)(&pManMR->pDataArray[i]) );
+
+  // main loop!
+  Abc_FlowRetime_MainLoop();
+
+  // clear pCopy field
+  Abc_NtkForEachObj( pNtk, pObj, i ) {
+    Abc_ObjSetCopy( pObj, NULL );
+
+    // if not computing init state, set all latches to DC
+    if (!fComputeInitState && Abc_ObjIsLatch(pObj))
+      Abc_LatchSetInitDc(pObj);
+  }
+
+  // deallocate space
+  FREE( pManMR->pDataArray );
+  if (pManMR->vNodes) Vec_PtrFree(pManMR->vNodes);
+  if (pManMR->vSinkDistHist) Vec_IntFree(pManMR->vSinkDistHist);
+  if (pManMR->maxDelay) Abc_FlowRetime_FreeTiming( pNtk );
+
+  // restrash if necessary
+  if (Abc_NtkIsStrash(pNtk)) {
+    Abc_NtkReassignIds( pNtk );
+    pNtk = Abc_NtkRestrash( pNtk, 1 );
+  }
+  
+  vprintf("\tfinal reg count = %d\n", Abc_NtkLatchNum(pNtk));
+  vprintf("\tfinal levels = %d\n", Abc_NtkLevel(pNtk));
+
+#if defined(DEBUG_CHECK)
+  Abc_NtkDoCheck( pNtk );
+#endif
+
+  // free manager
+  FREE( pManMR );
+
+  return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Main loop.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_MainLoop( ) {
+  Abc_Ntk_t *pNtk = pManMR->pNtk;
+  // Abc_Obj_t *pObj; int i;
+  int last, flow = 0, cut;
 
   // (i) forward retiming loop
-  fIsForward = 1;
+  pManMR->fIsForward = 1;
+  pManMR->iteration = 0;
 
-  if (!fBackwardOnly) do {
-    if (iteration == nMaxIters) break;
+  if (!pManMR->fBackwardOnly) do {
+    if (pManMR->iteration == pManMR->nMaxIters) break;
+    pManMR->subIteration = 0;
 
-    printf("\tforward iteration %d\n", iteration);
+    vprintf("\tforward iteration %d\n", pManMR->iteration);
     last = Abc_NtkLatchNum( pNtk );
 
     Abc_FlowRetime_MarkBlocks( pNtk );
-    flow = Abc_FlowRetime_PushFlows( pNtk );
+
+    if (pManMR->maxDelay) {
+      // timing-constrained loop
+      Abc_FlowRetime_ConstrainConserv( pNtk );
+      while(Abc_FlowRetime_RefineConstraints( )) {
+        pManMR->subIteration++;
+        Abc_FlowRetime_ClearFlows( 0 );
+      }
+    } else {
+      flow = Abc_FlowRetime_PushFlows( pNtk, 1 );
+    }
+
     cut = Abc_FlowRetime_ImplementCut( pNtk );
 
-    // clear all
-    memset(pDataArray, 0, sizeof(Flow_Data_t)*nNodes);    
-    iteration++;
-  } while( flow != last );
+    vprintf("\t\tlevels = %d\n", Abc_NtkLevel(pNtk));
+
+#if 0
+    Abc_NtkForEachObj( pNtk, pObj, i ) pObj->Level = 0;
+
+    Abc_NtkLevel(pNtk);
+    Abc_NtkForEachObj( pNtk, pObj, i )
+      if (pObj->Level > pManMR->maxDelay) {
+        print_node( pObj );
+        Vec_PtrForEachEntry( FTIMEEDGES(pObj), p2,j ) {
+          printf(":%d ", p2->Id);
+        }
+      }
+    Abc_NtkLevelReverse(pNtk);
+    Abc_NtkForEachObj( pNtk, pObj, i )
+      if (pObj->Level > pManMR->maxDelay) {
+        print_node( pObj );
+      }
+#endif
+
+    Abc_FlowRetime_ClearFlows( 1 );
+
+    pManMR->iteration++;
+  } while( cut != last );
 
   // print info about initial states
-  if (fComputeInitState)
+  if (pManMR->fComputeInitState && pManMR->fVerbose)
     Abc_FlowRetime_PrintInitStateInfo( pNtk );
 
   // (ii) backward retiming loop
-  fIsForward = 0;
-  iteration = 0;
+  pManMR->fIsForward = 0;
+  pManMR->iteration = 0;
+
+  if (!pManMR->fForwardOnly) do {
+    // initializability loop
 
-  if (!fForwardOnly) {
-    if (fComputeInitState) {
+    if (pManMR->fComputeInitState) {
       Abc_FlowRetime_SetupBackwardInit( pNtk );
     }
 
     do {
-      if (iteration == nMaxIters) break;
+      if (pManMR->iteration == pManMR->nMaxIters) break;
+      pManMR->subIteration = 0;
 
-      printf("\tbackward iteration %d\n", iteration);
+      vprintf("\tbackward iteration %d\n", pManMR->iteration);
       last = Abc_NtkLatchNum( pNtk );
-      
+
       Abc_FlowRetime_MarkBlocks( pNtk );
-      flow = Abc_FlowRetime_PushFlows( pNtk );
-      cut = Abc_FlowRetime_ImplementCut( pNtk );
       
-      // clear all
-      memset(pDataArray, 0, sizeof(Flow_Data_t)*nNodes);    
-      iteration++;
-
-    } while( flow != last );
-    
-    // compute initial states
-    if (fComputeInitState) {
-      Abc_FlowRetime_SolveBackwardInit( pNtk );
-      Abc_FlowRetime_PrintInitStateInfo( pNtk );
-    }
-  }
-
-  // clear pCopy field
-  Abc_NtkForEachObj( pNtk, pObj, i ) {
-    Abc_ObjSetCopy( pObj, NULL );
+      if (pManMR->maxDelay) {
+        // timing-constrained loop
+        Abc_FlowRetime_ConstrainConserv( pNtk );
+        while(Abc_FlowRetime_RefineConstraints( )) {
+          pManMR->subIteration++;
+          Abc_FlowRetime_ClearFlows( 0 );
+        }
+      } else {
+        flow = Abc_FlowRetime_PushFlows( pNtk, 1 );
+      }
+      
+      cut = Abc_FlowRetime_ImplementCut( pNtk );
 
-    // if not computing init state, set all latches to DC
-    if (!fComputeInitState && Abc_ObjIsLatch(pObj))
-      Abc_LatchSetInitDc(pObj);
-  }
+      vprintf("\t\tlevels = %d\n", Abc_NtkLevelReverse(pNtk));
+      
+#if 0
+    Abc_NtkForEachObj( pNtk, pObj, i ) pObj->Level = 0;
 
-  // restrash if necessary
-  if (Abc_NtkIsStrash(pNtk)) {
-    Abc_NtkReassignIds( pNtk );
-    pNtk = Abc_NtkRestrash( pNtk, 1 );
-  }
-  
-#if defined(DEBUG_CHECK)
-  Abc_NtkDoCheck( pNtk );
+    Abc_NtkLevel(pNtk);
+    Abc_NtkForEachObj( pNtk, pObj, i )
+      if (pObj->Level > pManMR->maxDelay) {
+        print_node( pObj );
+      }
+    Abc_NtkLevelReverse(pNtk);
+    Abc_NtkForEachObj( pNtk, pObj, i )
+      if (pObj->Level > pManMR->maxDelay) {
+        print_node( pObj );
+      }
 #endif
 
-  // deallocate space
-  free(pDataArray);
-  if (vSinkDistHist) Vec_IntFree(vSinkDistHist);
-
-  printf("\tfinal reg count = %d\n", Abc_NtkLatchNum(pNtk));
+      Abc_FlowRetime_ClearFlows( 1 );
 
-  return pNtk;
+      pManMR->iteration++;
+    } while( cut != last );
+    
+    // compute initial states
+    if (!pManMR->fComputeInitState) break;
+
+    if (Abc_FlowRetime_SolveBackwardInit( pNtk )) {
+      if (pManMR->fVerbose) Abc_FlowRetime_PrintInitStateInfo( pNtk );
+      break;
+    } else {
+      if (!pManMR->fGuaranteeInitState) break;
+      Abc_FlowRetime_ConstrainInit( );
+    }
+  } while(1);
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Pushes latch bubbles outside of box.]
@@ -237,8 +349,8 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState_,
 ***********************************************************************/
 void
 Abc_FlowRetime_RemoveLatchBubbles( Abc_Obj_t * pLatch ) {
-  int i, j, k, bubble = 0;
-  Abc_Ntk_t *pNtk = Abc_ObjNtk( pLatch );
+  int bubble = 0;
+  Abc_Ntk_t *pNtk = pManMR->pNtk;
   Abc_Obj_t *pBi, *pBo, *pInv;
       
   pBi = Abc_ObjFanin0(pLatch);
@@ -284,7 +396,7 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) {
   int i;
   Abc_Obj_t *pObj;
 
-  if (fIsForward){
+  if (pManMR->fIsForward){
     // mark the frontier
     Abc_NtkForEachPo( pNtk, pObj, i )
       pObj->fMarkA = 1;
@@ -294,7 +406,7 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) {
       }
     // mark the nodes reachable from the PIs
     Abc_NtkForEachPi( pNtk, pObj, i )
-      Abc_NtkMarkCone_rec( pObj, fIsForward );
+      Abc_NtkMarkCone_rec( pObj, pManMR->fIsForward );
   } else {
     // mark the frontier
     Abc_NtkForEachPi( pNtk, pObj, i )
@@ -305,15 +417,14 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) {
       }
     // mark the nodes reachable from the POs
     Abc_NtkForEachPo( pNtk, pObj, i )
-      Abc_NtkMarkCone_rec( pObj, fIsForward );
+      Abc_NtkMarkCone_rec( pObj, pManMR->fIsForward );
   }
 
   // copy marks
   Abc_NtkForEachObj( pNtk, pObj, i ) {
     if (pObj->fMarkA) {
       pObj->fMarkA = 0;
-      if (!Abc_ObjIsLatch(pObj) && 
-          !Abc_ObjIsPi(pObj))
+      if (!Abc_ObjIsLatch(pObj) /* && !Abc_ObjIsPi(pObj) */ )
         FSET(pObj, BLOCK);
     }
   }
@@ -332,15 +443,17 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) {
 
 ***********************************************************************/
 int
-Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk ) {
+Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk, bool fVerbose ) {
   int i, j, flow = 0, last, srcDist = 0;
   Abc_Obj_t   *pObj, *pObj2;
 
-  fSinkDistTerminate = 0;
+  pManMR->constraintMask |= BLOCK;
+
+  pManMR->fSinkDistTerminate = 0;
   dfsfast_preorder( pNtk );
 
   // (i) fast max-flow computation
-  while(!fSinkDistTerminate && srcDist < MAX_DIST) {
+  while(!pManMR->fSinkDistTerminate && srcDist < MAX_DIST) {
     srcDist = MAX_DIST;
     Abc_NtkForEachLatch( pNtk, pObj, i )
       if (FDATA(pObj)->e_dist)    
@@ -357,7 +470,7 @@ Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk ) {
     }
   }
 
-  printf("\t\tmax-flow1 = %d \t", flow);
+  if (fVerbose) vprintf("\t\tmax-flow1 = %d \t", flow);
 
   // (ii) complete max-flow computation
   // also, marks source-reachable nodes
@@ -375,7 +488,7 @@ Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk ) {
     }
   } while (flow > last);
   
-  printf("max-flow2 = %d\n", flow);
+  if (fVerbose) vprintf("max-flow2 = %d\n", flow);
 
   return flow;
 }
@@ -396,10 +509,9 @@ Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk ) {
 void
 Abc_FlowRetime_FixLatchBoxes( Abc_Ntk_t *pNtk, Vec_Ptr_t *vBoxIns ) {
   int i;
-  Abc_Obj_t *pObj, *pNext, *pBo = NULL, *pBi = NULL;
+  Abc_Obj_t *pObj, *pBo = NULL, *pBi = NULL;
   Vec_Ptr_t *vFreeBi = Vec_PtrAlloc( 100 );
   Vec_Ptr_t *vFreeBo = Vec_PtrAlloc( 100 );
-  Vec_Ptr_t *vNodes;
 
   // 1. remove empty bi/bo pairs
   while(Vec_PtrSize( vBoxIns )) {
@@ -424,10 +536,10 @@ Abc_FlowRetime_FixLatchBoxes( Abc_Ntk_t *pNtk, Vec_Ptr_t *vBoxIns ) {
       Vec_PtrPush( vFreeBo, pBo );
 
       // free names
-      // if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pBi)))
-      //  Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pBi));
-      //if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pBo)))
-      //  Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pBo));
+      if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pBi)))
+        Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pBi));
+      if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pBo)))
+        Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pBo));
 
       // check for complete detachment
       assert(Abc_ObjFaninNum(pBi) == 0);
@@ -512,12 +624,12 @@ Abc_FlowRetime_VerifyPathLatencies( Abc_Ntk_t * pNtk ) {
   Abc_Obj_t *pObj;
   fPathError = 0;
 
-  printf("\t\tVerifying latency along all paths...");
+  vprintf("\t\tVerifying latency along all paths...");
 
   Abc_NtkForEachObj( pNtk, pObj, i ) {
     if (Abc_ObjIsBo(pObj)) {
       Abc_FlowRetime_VerifyPathLatencies_rec( pObj, 0 );
-    } else if (!fIsForward && Abc_ObjIsPi(pObj)) {
+    } else if (!pManMR->fIsForward && Abc_ObjIsPi(pObj)) {
       Abc_FlowRetime_VerifyPathLatencies_rec( pObj, 0 );
     }
 
@@ -531,7 +643,7 @@ Abc_FlowRetime_VerifyPathLatencies( Abc_Ntk_t * pNtk ) {
     }
   }
 
-  printf(" ok\n");
+  vprintf(" ok\n");
 
   Abc_NtkForEachObj( pNtk, pObj, i ) {
     pObj->fMarkA = 0;
@@ -554,20 +666,20 @@ Abc_FlowRetime_VerifyPathLatencies_rec( Abc_Obj_t * pObj, int markD ) {
     if (Abc_ObjIsLatch(pObj))
       markC = 1;      // latch in output
     
-    if (!fIsForward && !Abc_ObjIsPo(pObj) && !Abc_ObjFanoutNum(pObj))
+    if (!pManMR->fIsForward && !Abc_ObjIsPo(pObj) && !Abc_ObjFanoutNum(pObj))
       return -1; // dangling non-PO outputs : don't care what happens
     
     Abc_ObjForEachFanout( pObj, pNext, i ) {
       // reached end of cycle?
       if ( Abc_ObjIsBo(pNext) ||
-           (fIsForward && Abc_ObjIsPo(pNext)) ) {
+           (pManMR->fIsForward && Abc_ObjIsPo(pNext)) ) {
         if (!markD && !Abc_ObjIsLatch(pObj)) {
           printf("\nERROR: no-latch path (end)\n");
           print_node(pNext);
           printf("\n");
           fPathError = 1;
         }
-      } else if (!fIsForward && Abc_ObjIsPo(pNext)) {
+      } else if (!pManMR->fIsForward && Abc_ObjIsPo(pNext)) {
         if (markD || Abc_ObjIsLatch(pObj)) {
           printf("\nERROR: extra-latch path to outputs\n");
           print_node(pNext);
@@ -625,7 +737,7 @@ void
 Abc_FlowRetime_CopyInitState( Abc_Obj_t * pSrc, Abc_Obj_t * pDest ) {
   Abc_Obj_t *pObj;
 
-  if (!fComputeInitState) return;
+  if (!pManMR->fComputeInitState) return;
 
   assert(Abc_ObjIsLatch(pSrc));
   assert(Abc_ObjFanin0(pDest) == pSrc);
@@ -638,7 +750,7 @@ Abc_FlowRetime_CopyInitState( Abc_Obj_t * pSrc, Abc_Obj_t * pDest ) {
     FSET(pDest, INIT_1);  
   }
   
-  if (!fIsForward) {
+  if (!pManMR->fIsForward) {
     pObj = Abc_ObjData(pSrc);
     assert(Abc_ObjIsPi(pObj));
     FDATA(pDest)->pInitObj = pObj;
@@ -684,8 +796,8 @@ Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) {
     Abc_ObjRemoveFanins( pObj );
 
     // free name
-    // if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pObj)))
-    //  Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pObj));
+    if (Nm_ManFindNameById(pNtk->pManName, Abc_ObjId(pObj)))
+      Nm_ManDeleteIdName( pNtk->pManName, Abc_ObjId(pObj));
   }
 
   // insert latches into netlist
@@ -693,33 +805,25 @@ Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) {
     if (Abc_ObjIsLatch( pObj )) continue;
     
     // a latch is required on every node that lies across the min-cit
-    assert(!fIsForward || !FTEST(pObj, VISITED_E) || FTEST(pObj, VISITED_R));
+    assert(!pManMR->fIsForward || !FTEST(pObj, VISITED_E) || FTEST(pObj, VISITED_R));
     if (FTEST(pObj, VISITED_R) && !FTEST(pObj, VISITED_E)) {
       assert(FTEST(pObj, FLOW));
 
       // count size of cut
       cut++;
-      if ((fIsForward && Abc_ObjIsBo(pObj)) || 
-          (!fIsForward && Abc_ObjIsBi(pObj)))
+      if ((pManMR->fIsForward && Abc_ObjIsBo(pObj)) || 
+          (!pManMR->fIsForward && Abc_ObjIsBi(pObj)))
         unmoved++;
       
       // only insert latch between fanouts that lie across min-cut
       // some fanout paths may be cut at deeper points
       Abc_ObjForEachFanout( pObj, pNext, j )
-        if (fIsForward) {
-          if (!FTEST(pNext, VISITED_R) || 
-              FTEST(pNext, BLOCK) || 
-              FTEST(pNext, CROSS_BOUNDARY) || 
-              Abc_ObjIsLatch(pNext))
-            Vec_PtrPush(vMove, pNext);
-        } else {
-          if (FTEST(pNext, VISITED_E) ||
-              FTEST(pNext, CROSS_BOUNDARY))
-            Vec_PtrPush(vMove, pNext);
-        }
+        if (Abc_FlowRetime_IsAcrossCut( pObj, pNext ))
+          Vec_PtrPush(vMove, pNext);
+
+      // check that move-set is non-zero
       if (Vec_PtrSize(vMove) == 0)
         print_node(pObj);
-
       assert(Vec_PtrSize(vMove) > 0);
       
       // insert one of re-useable registers
@@ -757,10 +861,11 @@ Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) {
   Vec_PtrFree( vMove );
   Vec_PtrFree( vBoxIns );
 
-  printf("\t\tmin-cut = %d (unmoved = %d)\n", cut, unmoved);
+  vprintf("\t\tmin-cut = %d (unmoved = %d)\n", cut, unmoved);
   return cut;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Adds dummy fanin.]
@@ -808,13 +913,14 @@ print_node(Abc_Obj_t *pObj) {
   if (pObj->fMarkC)
     strcat(m, "C");
 
-  printf("node %d type=%d (%x%s) fanouts {", Abc_ObjId(pObj), Abc_ObjType(pObj), FDATA(pObj)->mark, m);
+  printf("node %d type=%d lev=%d tedge=%d (%x%s) fanouts {", Abc_ObjId(pObj), Abc_ObjType(pObj),
+         pObj->Level, Vec_PtrSize(FTIMEEDGES(pObj)), FDATA(pObj)->mark, m);
   Abc_ObjForEachFanout( pObj, pNext, i )
-    printf("%d (%d),", Abc_ObjId(pNext), FDATA(pNext)->mark);
+    printf("%d[%d](%d),", Abc_ObjId(pNext), Abc_ObjType(pNext), FDATA(pNext)->mark);
   printf("} fanins {");
   Abc_ObjForEachFanin( pObj, pNext, i )
-    printf("%d (%d),", Abc_ObjId(pNext), FDATA(pNext)->mark);
-  printf("} ");
+    printf("%d[%d](%d),", Abc_ObjId(pNext), Abc_ObjType(pNext), FDATA(pNext)->mark);
+  printf("}\n");
 }
 
 void
@@ -831,7 +937,7 @@ print_node2(Abc_Obj_t *pObj) {
   if (pObj->fMarkC)
     strcat(m, "C");
 
-  printf("node %d type=%d fanouts {", Abc_ObjId(pObj), Abc_ObjType(pObj), m);
+  printf("node %d type=%d %s fanouts {", Abc_ObjId(pObj), Abc_ObjType(pObj), m);
   Abc_ObjForEachFanout( pObj, pNext, i )
     printf("%d ,", Abc_ObjId(pNext));
   printf("} fanins {");
@@ -840,6 +946,33 @@ print_node2(Abc_Obj_t *pObj) {
   printf("} ");
 }
 
+void
+print_node3(Abc_Obj_t *pObj) {
+  int i;
+  Abc_Obj_t * pNext;
+  char m[6];
+
+  m[0] = 0;
+  if (pObj->fMarkA)
+    strcat(m, "A");
+  if (pObj->fMarkB)
+    strcat(m, "B");
+  if (pObj->fMarkC)
+    strcat(m, "C");
+
+  printf("\nnode %d type=%d mark=%d %s\n", Abc_ObjId(pObj), Abc_ObjType(pObj), FDATA(pObj)->mark, m);
+  printf("fanouts\n");
+  Abc_ObjForEachFanout( pObj, pNext, i ) {
+    print_node(pNext);
+    printf("\n");
+  }
+  printf("fanins\n");
+  Abc_ObjForEachFanin( pObj, pNext, i ) {
+    print_node(pNext);
+    printf("\n");
+  }
+}
+
 
 /**Function*************************************************************
 
@@ -862,3 +995,65 @@ Abc_ObjBetterTransferFanout( Abc_Obj_t * pFrom, Abc_Obj_t * pTo, int compl ) {
     Abc_ObjPatchFanin( pNext, pFrom, Abc_ObjNotCond(pTo, compl) );
   }
 }
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns true is a connection spans the min-cut.]
+
+  Description [pNext is a direct fanout of pObj.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool
+Abc_FlowRetime_IsAcrossCut( Abc_Obj_t *pObj, Abc_Obj_t *pNext ) {
+
+  if (FTEST(pObj, VISITED_R) && !FTEST(pObj, VISITED_E)) {
+    if (pManMR->fIsForward) {
+      if (!FTEST(pNext, VISITED_R) || 
+          (FTEST(pNext, BLOCK_OR_CONS) & pManMR->constraintMask)|| 
+          FTEST(pNext, CROSS_BOUNDARY) || 
+          Abc_ObjIsLatch(pNext))
+        return 1;
+    } else {
+      if (FTEST(pNext, VISITED_E) ||
+          FTEST(pNext, CROSS_BOUNDARY))
+        return 1;
+    }
+  }
+  
+  return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Resets flow problem]
+
+  Description [If fClearAll is true, all marks will be cleared; this is
+               typically appropriate after the circuit structure has
+               been modified.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_ClearFlows( bool fClearAll ) {
+  int i;
+
+  if (fClearAll)
+    memset(pManMR->pDataArray, 0, sizeof(Flow_Data_t)*pManMR->nNodes);
+  else {
+    // clear only data related to flow problem
+    for(i=0; i<pManMR->nNodes; i++) {
+      pManMR->pDataArray[i].mark &= ~(VISITED | FLOW );
+      pManMR->pDataArray[i].e_dist = 0;
+      pManMR->pDataArray[i].r_dist = 0;
+      pManMR->pDataArray[i].pred = NULL;
+    }
+  }
+}

src/opt/fret/fretTime.c

+/**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);
+}
+
+

src/opt/fret/fretime.h

@@ -23,7 +23,7 @@
 
 #include "abc.h"
 
-#define IGNORE_TIMING
+// #define IGNORE_TIMING
 // #define DEBUG_PRINT_FLOWS
 // #define DEBUG_VISITED
 // #define DEBUG_PREORDER
@@ -45,49 +45,29 @@
 #define INIT_0          0x20
 #define INIT_1          0x40
 #define INIT_CARE (INIT_0 | INIT_1)
+#define CONSERVATIVE    0x80
+#define BLOCK_OR_CONS (BLOCK | CONSERVATIVE)
 
-typedef struct Untimed_Flow_Data_t_ {
-  unsigned int mark : 8;
+typedef struct Flow_Data_t_ {
+  unsigned int mark : 16;
 
   union {
     Abc_Obj_t   *pred;
     /* unsigned int var; */
     Abc_Obj_t   *pInitObj;
+    Vec_Ptr_t   *vNodes;
   };
 
   unsigned int e_dist : 16;
   unsigned int r_dist : 16;
-} Untimed_Flow_Data_t;
-
-typedef struct Timed_Flow_Data_t_ {
-  unsigned int mark : 8;
-
-  union {
-    Abc_Obj_t   *pred;
-    Vec_Ptr_t   *vTimeInEdges;
-    /* unsigned int var; */
-    Abc_Obj_t   *pInitObj;
-  };
-
-  unsigned int e_dist : 16;
-  unsigned int r_dist : 16;
-
-  Vec_Ptr_t    vTimeEdges;
-
-} Timed_Flow_Data_t;
-
-#if defined(IGNORE_TIMING)
-typedef Untimed_Flow_Data_t Flow_Data_t;
-#else
-typedef Timed_Flow_Data_t Flow_Data_t;
-#endif
+} Flow_Data_t;
 
 // useful macros for manipulating Flow_Data structure...
 #define FDATA( x )     ((Flow_Data_t *)Abc_ObjCopy(x))
 #define FSET( x, y )   ((Flow_Data_t *)Abc_ObjCopy(x))->mark |= y
 #define FUNSET( x, y ) ((Flow_Data_t *)Abc_ObjCopy(x))->mark &= ~y
 #define FTEST( x, y )  (((Flow_Data_t *)Abc_ObjCopy(x))->mark & y)
-#define FTIMEEDGES( x )  &(((Timed_Flow_Data_t *)Abc_ObjCopy(x))->vTimeEdges)
+#define FTIMEEDGES( x )  &(pManMR->vTimeEdges[Abc_ObjId( x )])
 
 static inline void FSETPRED(Abc_Obj_t *pObj, Abc_Obj_t *pPred) {
   assert(!Abc_ObjIsLatch(pObj)); // must preserve field to maintain init state linkage
@@ -97,21 +77,56 @@ static inline Abc_Obj_t * FGETPRED(Abc_Obj_t *pObj) {
   return FDATA(pObj)->pred;
 }
 
+
+typedef struct MinRegMan_t_ {
+ 
+  // problem description:
+  int         maxDelay;
+  bool        fComputeInitState, fGuaranteeInitState;
+  int         nNodes, nLatches;
+  bool        fForwardOnly, fBackwardOnly;
+  bool        fConservTimingOnly;
+  int         nMaxIters;
+  bool        fVerbose;
+  Abc_Ntk_t  *pNtk;
+
+  int         nPreRefine;
+
+  // problem state
+  bool        fIsForward;
+  bool        fSinkDistTerminate;
+  int         nExactConstraints, nConservConstraints;
+  int         fSolutionIsDc;
+  int         constraintMask;
+  int         iteration, subIteration;
+  
+  // problem data
+  Vec_Int_t   *vSinkDistHist;
+  Flow_Data_t *pDataArray;
+  Vec_Ptr_t   *vTimeEdges;
+  Vec_Ptr_t   *vExactNodes;
+  Abc_Ntk_t   *pInitNtk;
+  Vec_Ptr_t   *vNodes; // re-useable struct
+
+} MinRegMan_t ;
+
+#define vprintf if (pManMR->fVerbose) printf 
+
 /*=== fretMain.c ==========================================================*/
+ 
+extern MinRegMan_t *pManMR;
 
 Abc_Ntk_t *    Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
                                       int fForward, int fBackward, int nMaxIters,
-                                      int maxDelay);
+                                      int maxDelay, int fFastButConservative);
 
 void print_node(Abc_Obj_t *pObj);
 
 void Abc_ObjBetterTransferFanout( Abc_Obj_t * pFrom, Abc_Obj_t * pTo, int compl );
 
-extern int         fIsForward;
-extern int         fSinkDistTerminate;
-extern Vec_Int_t  *vSinkDistHist;
-extern int         maxDelayCon;
-extern int         fComputeInitState;
+int  Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk, bool fVerbose );
+bool Abc_FlowRetime_IsAcrossCut( Abc_Obj_t *pCur, Abc_Obj_t *pNext );
+void Abc_FlowRetime_ClearFlows( bool fClearAll );
 
 /*=== fretFlow.c ==========================================================*/
 
@@ -132,9 +147,19 @@ void Abc_FlowRetime_UpdateForwardInit( Abc_Ntk_t * pNtk );
 void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk );
 
 void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk );
-void Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk );
+int  Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk );
+
+void Abc_FlowRetime_ConstrainInit(  );
+
+/*=== fretTime.c ==========================================================*/
+
+void Abc_FlowRetime_InitTiming( Abc_Ntk_t *pNtk );
+void Abc_FlowRetime_FreeTiming( Abc_Ntk_t *pNtk );
+
+bool Abc_FlowRetime_RefineConstraints( );
 
-extern Abc_Ntk_t *pInitNtk;
-extern int        fSolutionIsDc;
+void Abc_FlowRetime_ConstrainConserv( Abc_Ntk_t * pNtk );
+void Abc_FlowRetime_ConstrainExact( Abc_Obj_t * pObj );
+void Abc_FlowRetime_ConstrainExactAll( Abc_Ntk_t * pNtk );
 
 #endif

src/opt/fret/module.make

 SRC +=    src/opt/fret/fretMain.c \
     src/opt/fret/fretFlow.c \
-        src/opt/fret/fretInit.c
+        src/opt/fret/fretInit.c \
+    src/opt/fret/fretTime.c