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