From 6537f941887b06e588d3acfc97b5fdf48875cc4e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 26 Jan 2008 08:01:00 -0800 Subject: Version abc80126 --- Makefile | 4 +- abc.dsp | 8 + src/aig/aig/aig.h | 54 ++++ src/aig/aig/aigCuts.c | 669 +++++++++++++++++++++++++++++++++++++++++ src/aig/cnf/cnfCore.c | 2 +- src/aig/dar/dar.h | 2 +- src/aig/dar/darCore.c | 49 ++- src/aig/dar/darCut.c | 41 +++ src/aig/dar/darInt.h | 1 + src/aig/fra/fraClaus.c | 498 ++++++++++++++++++++++++++----- src/base/abc/1.txt | 21 ++ src/base/abc/abcDfs.c | 4 +- src/base/abci/abc.c | 91 +++++- src/base/abci/abcDar.c | 6 +- src/opt/fret/fretFlow.c | 210 ++++++++----- src/opt/fret/fretInit.c | 141 +++++---- src/opt/fret/fretMain.c | 475 ++++++++++++++++++++--------- src/opt/fret/fretTime.c | 763 +++++++++++++++++++++++++++++++++++++++++++++++ src/opt/fret/fretime.h | 99 +++--- src/opt/fret/module.make | 3 +- 20 files changed, 2735 insertions(+), 406 deletions(-) create mode 100644 src/aig/aig/aigCuts.c create mode 100644 src/base/abc/1.txt create mode 100644 src/opt/fret/fretTime.c 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<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 @@ -193,6 +193,34 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; return 1; } +/**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 [] @@ -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 @@ -28,6 +28,47 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**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.] 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 ]++; } @@ -332,6 +383,26 @@ void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost Vec_IntPush( p->vCosts, 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<vClauses, Vec_IntSize(p->vLits) ); + Vec_IntPush( p->vCosts, Cost ); +} + /**Function************************************************************* Synopsis [Returns 1 if simulation info is composed of all zeros.] @@ -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 ); @@ -588,6 +662,174 @@ PRT( "Infocmb", clock() - clk ); return 1; } +/**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<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.] @@ -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; inNodes; 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 -- cgit v1.2.3