diff options
32 files changed, 3189 insertions, 169 deletions
@@ -2558,6 +2558,10 @@ SOURCE=.\src\aig\fra\fra.h # End Source File # Begin Source File +SOURCE=.\src\aig\fra\fraCec.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\fra\fraClass.c # End Source File # Begin Source File @@ -2570,6 +2574,10 @@ SOURCE=.\src\aig\fra\fraCore.c # End Source File # Begin Source File +SOURCE=.\src\aig\fra\fraImp.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\fra\fraInd.c # End Source File # Begin Source File @@ -2578,10 +2586,18 @@ SOURCE=.\src\aig\fra\fraMan.c # End Source File # Begin Source File +SOURCE=.\src\aig\fra\fraPart.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\fra\fraSat.c # End Source File # Begin Source File +SOURCE=.\src\aig\fra\fraSec.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\fra\fraSim.c # End Source File # End Group @@ -2770,6 +2786,10 @@ SOURCE=.\src\aig\aig\aigRepr.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigRet.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigSeq.c # End Source File # Begin Source File diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index d6a97257..a1abd2b7 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -126,6 +126,7 @@ struct Aig_Man_t_ void * pData; // the temporary data int nTravIds; // the current traversal ID int fCatchExor; // enables EXOR nodes + int fAddStrash; // performs additional strashing // timing statistics int time1; int time2; @@ -149,7 +150,16 @@ static inline int Aig_TruthWordNum( int nVars ) { return nVars static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } +static inline unsigned Aig_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); } static inline unsigned Aig_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } +static inline int Aig_WordCountOnes( unsigned uWord ) +{ + uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555); + uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333); + uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F); + uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF); + return (uWord & 0x0000FFFF) + (uWord>>16); +} static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)((unsigned long)(p) & ~01); } static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)((unsigned long)(p) ^ 01); } @@ -328,6 +338,10 @@ static inline int Aig_ObjFanoutNext( Aig_Man_t * p, int iFan ) { assert(iF // iterator over the latch inputs #define Aig_ManForEachLiSeq( p, pObj, i ) \ Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) ) +// iterator over the latch input and outputs +#define Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, k ) \ + for ( k = 0; (k < Aig_ManRegNum(p)) && (((pObjLi) = Aig_ManLi(p, k)), 1) \ + && (((pObjLo)=Aig_ManLo(p, k)), 1); k++ ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// @@ -358,10 +372,14 @@ extern void Aig_ManFanoutStop( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManStart( int nNodesMax ); extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ); +extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ); extern Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 ); extern void Aig_ManStop( Aig_Man_t * p ); extern int Aig_ManCleanup( Aig_Man_t * p ); +extern int Aig_ManCountMergeRegs( Aig_Man_t * p ); +extern int Aig_ManSeqCleanup( Aig_Man_t * p ); extern void Aig_ManPrintStats( Aig_Man_t * p ); +extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose ); /*=== aigMem.c ==========================================================*/ extern void Aig_ManStartMemory( Aig_Man_t * p ); extern void Aig_ManStopMemory( Aig_Man_t * p ); @@ -414,8 +432,11 @@ extern void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p ); extern void Aig_ManCreateChoices( Aig_Man_t * p ); +/*=== aigRet.c ========================================================*/ +extern Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose ); /*=== aigSeq.c ========================================================*/ extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits ); +extern Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose ); /*=== aigShow.c ========================================================*/ extern void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ); /*=== aigTable.c ========================================================*/ diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 818b75fe..d09bf41b 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -172,6 +172,54 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) /**Function************************************************************* + Synopsis [Remaps the manager.] + + Description [Map in the array specifies for each CI nodes the node that + should be used after remapping.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjMapped; + int i; + // create the new manager + pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + pNew->nRegs = p->nRegs; + pNew->nAsserts = p->nAsserts; + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi(pNew); + // implement the mapping + Aig_ManForEachPi( p, pObj, i ) + { + pObjMapped = Vec_PtrEntry( vMap, i ); + pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) ); + } + // duplicate internal nodes + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjIsBuf(pObj) ) + pObj->pData = Aig_ObjChild0Copy(pObj); + else if ( Aig_ObjIsNode(pObj) ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // add the POs + Aig_ManForEachPo( p, pObj, i ) + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) ); + // check the resulting network + if ( !Aig_ManCheck(pNew) ) + printf( "Aig_ManDup(): The check has failed.\n" ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Extracts the miter composed of XOR of the two nodes.] Description [] @@ -257,6 +305,110 @@ void Aig_ManStop( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ +void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + // collect latch input corresponding to unmarked PI (latch output) + if ( Aig_ObjIsPi(pObj) ) + { + Vec_PtrPush( vNodes, pObj->pNext ); + return; + } + if ( Aig_ObjIsPo(pObj) ) + { + Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes ); + return; + } + assert( Aig_ObjIsNode(pObj) ); + Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes ); + Aig_ManSeqCleanup_rec( p, Aig_ObjFanin1(pObj), vNodes ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManSeqCleanup( Aig_Man_t * p ) +{ + Vec_Ptr_t * vNodes, * vCis, * vCos; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, nTruePis, nTruePos; + assert( Aig_ManBufNum(p) == 0 ); + + // mark the PIs + Aig_ManIncrementTravId( p ); + Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); + Aig_ManForEachPiSeq( p, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + + // prepare to collect nodes reachable from POs + vNodes = Vec_PtrAlloc( 100 ); + Aig_ManForEachPoSeq( p, pObj, i ) + Vec_PtrPush( vNodes, pObj ); + + // remember latch inputs in latch outputs + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + pObjLo->pNext = pObjLi; + // mark the nodes reachable from these nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + Aig_ManSeqCleanup_rec( p, pObj, vNodes ); + assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) ); + // clean latch output pointers + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + pObjLo->pNext = NULL; + + // if some latches are removed, update PIs/POs + if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) ) + { + // collect new CIs/COs + vCis = Vec_PtrAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPi( p, pObj, i ) + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + Vec_PtrPush( vCis, pObj ); + vCos = Vec_PtrAlloc( Aig_ManPoNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + Vec_PtrPush( vCos, pObj ); + else + Aig_ObjDisconnect( p, pObj ); + // remember the number of true PIs/POs + nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p); + nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p); + // set the new number of registers + p->nRegs -= Aig_ManPoNum(p) - Vec_PtrSize(vNodes); + // create new PIs/POs + assert( Vec_PtrSize(vCis) == nTruePis + p->nRegs ); + assert( Vec_PtrSize(vCos) == nTruePos + p->nRegs ); + Vec_PtrFree( p->vPis ); p->vPis = vCis; + Vec_PtrFree( p->vPos ); p->vPos = vCos; + p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis ); + p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos ); + } + Vec_PtrFree( vNodes ); + // remove dangling nodes + return Aig_ManCleanup( p ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Aig_ManCleanup( Aig_Man_t * p ) { Vec_Ptr_t * vObjs; @@ -277,6 +429,42 @@ int Aig_ManCleanup( Aig_Man_t * p ) /**Function************************************************************* + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManCountMergeRegs( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pFanin; + int i, Counter = 0, Const0 = 0, Const1 = 0; + Aig_ManIncrementTravId( p ); + Aig_ManForEachLiSeq( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + if ( Aig_ObjIsConst1(pFanin) ) + { + if ( Aig_ObjFaninC0(pObj) ) + Const0++; + else + Const1++; + } + if ( Aig_ObjIsTravIdCurrent(p, pFanin) ) + continue; + Aig_ObjSetTravIdCurrent(p, pFanin); + Counter++; + } + printf( "Regs = %d. Fanins = %d. Const0 = %d. Const1 = %d.\n", + Aig_ManRegNum(p), Counter, Const0, Const1 ); + return 0; +} + +/**Function************************************************************* + Synopsis [Stops the AIG manager.] Description [] @@ -302,6 +490,148 @@ void Aig_ManPrintStats( Aig_Man_t * p ) printf( "\n" ); } +/**Function************************************************************* + + Synopsis [Checks how many latches can be reduced.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManReduceLachesCount( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pFanin; + int i, Counter = 0; + assert( Aig_ManRegNum(p) > 0 ); + Aig_ManForEachObj( p, pObj, i ) + assert( !pObj->fMarkA && !pObj->fMarkB ); + Aig_ManForEachLiSeq( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + if ( Aig_ObjFaninC0(pObj) ) + { + if ( pFanin->fMarkB ) + Counter++; + else + pFanin->fMarkB = 1; + } + else + { + if ( pFanin->fMarkA ) + Counter++; + else + pFanin->fMarkA = 1; + } + } + Aig_ManForEachLiSeq( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + pFanin->fMarkA = pFanin->fMarkB = 0; + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Reduces the latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p ) +{ + Vec_Ptr_t * vMap; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pFanin; + int * pMapping, i; + // start mapping by adding the true PIs + vMap = Vec_PtrAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPiSeq( p, pObj, i ) + Vec_PtrPush( vMap, pObj ); + // create mapping of fanin nodes into the corresponding latch outputs + pMapping = ALLOC( int, 2 * (Aig_ManObjIdMax(p) + 1) ); + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + { + pFanin = Aig_ObjFanin0(pObjLi); + if ( Aig_ObjFaninC0(pObjLi) ) + { + if ( pFanin->fMarkB ) + { + Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id + 1]) ); + } + else + { + pFanin->fMarkB = 1; + pMapping[2*pFanin->Id + 1] = i; + Vec_PtrPush( vMap, pObjLo ); + } + } + else + { + if ( pFanin->fMarkA ) + { + Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id]) ); + } + else + { + pFanin->fMarkA = 1; + pMapping[2*pFanin->Id] = i; + Vec_PtrPush( vMap, pObjLo ); + } + } + } + free( pMapping ); + Aig_ManForEachLiSeq( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + pFanin->fMarkA = pFanin->fMarkB = 0; + } + return vMap; +} + +/**Function************************************************************* + + Synopsis [Reduces the latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose ) +{ + Aig_Man_t * pTemp; + Vec_Ptr_t * vMap; + int nSaved, nCur; + for ( nSaved = 0; nCur = Aig_ManReduceLachesCount(p); nSaved += nCur ) + { + if ( fVerbose ) + { + printf( "Saved = %5d. ", nCur ); + printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); + } + vMap = Aig_ManReduceLachesOnce( p ); + p = Aig_ManRemap( pTemp = p, vMap ); + Aig_ManStop( pTemp ); + Vec_PtrFree( vMap ); + Aig_ManSeqCleanup( p ); + if ( fVerbose ) + { + printf( "REnd = %5d. NEnd = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); + printf( "\n" ); + } + } + return p; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/aig/aigOper.c b/src/aig/aig/aigOper.c index d13d4bed..68216ee0 100644 --- a/src/aig/aig/aigOper.c +++ b/src/aig/aig/aigOper.c @@ -148,6 +148,89 @@ Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ) return p0 == p->pConst1 ? p1 : Aig_Not(p->pConst1); if ( Aig_Regular(p1) == p->pConst1 ) return p1 == p->pConst1 ? p0 : Aig_Not(p->pConst1); + // check not so trivial cases + if ( p->fAddStrash && (Aig_ObjIsNode(Aig_Regular(p0)) || Aig_ObjIsNode(Aig_Regular(p1))) ) + { // http://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf + Aig_Obj_t * pFanA, * pFanB, * pFanC, * pFanD; + pFanA = Aig_ObjChild0(Aig_Regular(p0)); + pFanB = Aig_ObjChild1(Aig_Regular(p0)); + pFanC = Aig_ObjChild0(Aig_Regular(p1)); + pFanD = Aig_ObjChild1(Aig_Regular(p1)); + if ( Aig_IsComplement(p0) ) + { + if ( pFanA == Aig_Not(p1) || pFanB == Aig_Not(p1) ) + return p1; + if ( pFanB == p1 ) + return Aig_And( p, Aig_Not(pFanA), pFanB ); + if ( pFanA == p1 ) + return Aig_And( p, Aig_Not(pFanB), pFanA ); + } + else + { + if ( pFanA == Aig_Not(p1) || pFanB == Aig_Not(p1) ) + return Aig_Not(p->pConst1); + if ( pFanA == p1 || pFanB == p1 ) + return p0; + } + if ( Aig_IsComplement(p1) ) + { + if ( pFanC == Aig_Not(p0) || pFanD == Aig_Not(p0) ) + return p0; + if ( pFanD == p0 ) + return Aig_And( p, Aig_Not(pFanC), pFanD ); + if ( pFanC == p0 ) + return Aig_And( p, Aig_Not(pFanD), pFanC ); + } + else + { + if ( pFanC == Aig_Not(p0) || pFanD == Aig_Not(p0) ) + return Aig_Not(p->pConst1); + if ( pFanC == p0 || pFanD == p0 ) + return p1; + } + if ( !Aig_IsComplement(p0) && !Aig_IsComplement(p1) ) + { + if ( pFanA == Aig_Not(pFanC) || pFanA == Aig_Not(pFanD) || pFanB == Aig_Not(pFanC) || pFanB == Aig_Not(pFanD) ) + return Aig_Not(p->pConst1); + if ( pFanA == pFanC || pFanB == pFanC ) + return Aig_And( p, p0, pFanD ); + if ( pFanB == pFanC || pFanB == pFanD ) + return Aig_And( p, pFanA, p1 ); + if ( pFanA == pFanD || pFanB == pFanD ) + return Aig_And( p, p0, pFanC ); + if ( pFanA == pFanC || pFanA == pFanD ) + return Aig_And( p, pFanB, p1 ); + } + else if ( Aig_IsComplement(p0) && !Aig_IsComplement(p1) ) + { + if ( pFanA == Aig_Not(pFanC) || pFanA == Aig_Not(pFanD) || pFanB == Aig_Not(pFanC) || pFanB == Aig_Not(pFanD) ) + return p1; + if ( pFanB == pFanC || pFanB == pFanD ) + return Aig_And( p, Aig_Not(pFanA), p1 ); + if ( pFanA == pFanC || pFanA == pFanD ) + return Aig_And( p, Aig_Not(pFanB), p1 ); + } + else if ( !Aig_IsComplement(p0) && Aig_IsComplement(p1) ) + { + if ( pFanC == Aig_Not(pFanA) || pFanC == Aig_Not(pFanB) || pFanD == Aig_Not(pFanA) || pFanD == Aig_Not(pFanB) ) + return p0; + if ( pFanD == pFanA || pFanD == pFanB ) + return Aig_And( p, Aig_Not(pFanC), p0 ); + if ( pFanC == pFanA || pFanC == pFanB ) + return Aig_And( p, Aig_Not(pFanD), p0 ); + } + else // if ( Aig_IsComplement(p0) && Aig_IsComplement(p1) ) + { + if ( pFanA == pFanD && pFanB == Aig_Not(pFanC) ) + return Aig_Not(pFanA); + if ( pFanB == pFanC && pFanA == Aig_Not(pFanD) ) + return Aig_Not(pFanB); + if ( pFanA == pFanC && pFanB == Aig_Not(pFanD) ) + return Aig_Not(pFanA); + if ( pFanB == pFanD && pFanA == Aig_Not(pFanC) ) + return Aig_Not(pFanB); + } + } // check if it can be an EXOR gate // if ( Aig_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) ) // return Aig_Exor( p, pFan0, pFan1 ); diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c new file mode 100644 index 00000000..eacf756b --- /dev/null +++ b/src/aig/aig/aigRet.c @@ -0,0 +1,552 @@ +/**CFile**************************************************************** + + FileName [aigRet.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Retiming of AIGs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigRet.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// init values +typedef enum { + RTM_VAL_NONE, // 0: non-existent value + RTM_VAL_ZERO, // 1: initial value 0 + RTM_VAL_ONE, // 2: initial value 1 + RTM_VAL_VOID // 3: unused value +} Rtm_Init_t; + +typedef struct Rtm_Man_t_ Rtm_Man_t; +struct Rtm_Man_t_ +{ + // network representation + Vec_Ptr_t * vObjs; // retiming objects + Vec_Ptr_t * vPis; // PIs only + Vec_Ptr_t * vPos; // POs only + Aig_MmFlex_t * pMem; // the memory manager + // storage for overflow latches + unsigned * pExtra; + unsigned * pExtraFree; +}; + +typedef struct Rtm_Edg_t_ Rtm_Edg_t; +struct Rtm_Edg_t_ +{ + unsigned long nLats : 12; // the number of latches + unsigned long LData : 20; // the latches themselves +}; + +typedef struct Rtm_Obj_t_ Rtm_Obj_t; +struct Rtm_Obj_t_ +{ + void * pCopy; // the copy of this object + unsigned long Type : 3; // object type + unsigned long fMark : 1; // multipurpose mark + unsigned long fCompl0 : 1; // complemented attribute of the first edge + unsigned long fCompl1 : 1; // complemented attribute of the second edge + unsigned long nFanins : 8; // the number of fanins + unsigned Num : 18; // the retiming number of this node + int Id; // ID of this object + int Temp; // temporary usage + int nFanouts; // the number of fanouts + void * pFanio[0]; // fanins and their edges (followed by fanouts and pointers to their edges) +}; + +static Rtm_Init_t Rtm_InitNot( Rtm_Init_t Val ) { if ( Val == RTM_VAL_ZERO ) return RTM_VAL_ONE; if ( Val == RTM_VAL_ONE ) return RTM_VAL_ZERO; assert( 0 ); return -1; } +static Rtm_Init_t Rtm_InitNotCond( Rtm_Init_t Val, int c ) { return c ? Rtm_InitNot(Val) : Val; } +static Rtm_Init_t Rtm_InitAnd(Rtm_Init_t ValA, Rtm_Init_t ValB) { if ( ValA == RTM_VAL_ONE && ValB == RTM_VAL_ONE ) return RTM_VAL_ONE; if ( ValA == RTM_VAL_ZERO || ValB == RTM_VAL_ZERO ) return RTM_VAL_ZERO; assert( 0 ); return -1; } + +static Rtm_Obj_t * Rtm_ObjFanin( Rtm_Obj_t * pObj, int i ) { return (Rtm_Obj_t *)pObj->pFanio[2*i]; } +static Rtm_Obj_t * Rtm_ObjFanout( Rtm_Obj_t * pObj, int i ) { return (Rtm_Obj_t *)pObj->pFanio[2*(pObj->nFanins+i)]; } +static Rtm_Edg_t * Rtm_ObjEdge( Rtm_Obj_t * pObj, int i ) { return (Rtm_Edg_t *)(pObj->pFanio + 2*i + 1); } +static Rtm_Edg_t * Rtm_ObjFanoutEdge( Rtm_Obj_t * pObj, int i ) { return (Rtm_Edg_t *)pObj->pFanio[2*(pObj->nFanins+i) + 1]; } + +static Rtm_Init_t Rtm_ObjGetFirst( Rtm_Edg_t * pEdge ) { return pEdge->LData & 3; } +static Rtm_Init_t Rtm_ObjGetLast( Rtm_Edg_t * pEdge ) { return (pEdge->LData >> (2 *(pEdge->nLats-1))) & 3; } +static Rtm_Init_t Rtm_ObjGetOne( Rtm_Edg_t * pEdge, int i ) { assert( i < (int)pEdge->nLats ); return (pEdge->LData >> (2 * i)) & 3; } +static Rtm_Init_t Rtm_ObjRemFirst( Rtm_Edg_t * pEdge ) { int Val = pEdge->LData & 3; pEdge->LData >>= 2; assert(pEdge->nLats > 0); pEdge->nLats--; return Val; } +static Rtm_Init_t Rtm_ObjRemLast( Rtm_Edg_t * pEdge ) { int Val = (pEdge->LData >> (2 *(pEdge->nLats-1))) & 3; pEdge->LData ^= Val << (2 *(pEdge->nLats-1)); assert(pEdge->nLats > 0); pEdge->nLats--; return Val; } +static void Rtm_ObjAddFirst( Rtm_Edg_t * pEdge, Rtm_Init_t Lat ) { assert( Lat < 4 ); pEdge->LData = (pEdge->LData << 2) | Lat; pEdge->nLats++; } +static void Rtm_ObjAddLast( Rtm_Edg_t * pEdge, Rtm_Init_t Lat ) { assert( Lat < 4 ); pEdge->LData |= Lat << (2*pEdge->nLats); pEdge->nLats++; } + +// iterator over the primary inputs +#define Rtm_ManForEachPi( p, pObj, i ) \ + Vec_PtrForEachEntry( p->vPis, pObj, i ) +// iterator over the primary outputs +#define Rtm_ManForEachPo( p, pObj, i ) \ + Vec_PtrForEachEntry( p->vPos, pObj, i ) +// iterator over all objects, including those currently not used +#define Rtm_ManForEachObj( p, pObj, i ) \ + Vec_PtrForEachEntry( p->vObjs, pObj, i ) +// iterate through the fanins +#define Rtm_ObjForEachFanin( pObj, pFanin, i ) \ + for ( i = 0; i < (int)(pObj)->nFanins && ((pFanin = Rtm_ObjFanin(pObj, i)), 1); i++ ) +// iterate through the fanouts +#define Rtm_ObjForEachFanout( pObj, pFanout, i ) \ + for ( i = 0; i < (int)(pObj)->nFanouts && ((pFanout = Rtm_ObjFanout(pObj, i)), 1); i++ ) +// iterate through the fanin edges +#define Rtm_ObjForEachFaninEdge( pObj, pEdge, i ) \ + for ( i = 0; i < (int)(pObj)->nFanins && ((pEdge = Rtm_ObjEdge(pObj, i)), 1); i++ ) +// iterate through the fanout edges +#define Rtm_ObjForEachFanoutEdge( pObj, pEdge, i ) \ + for ( i = 0; i < (int)(pObj)->nFanouts && ((pEdge = Rtm_ObjFanoutEdge(pObj, i)), 1); i++ ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates the retiming manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Rtm_Man_t * Rtm_ManAlloc( Aig_Man_t * p ) +{ + Rtm_Man_t * pRtm; + // start the manager + pRtm = ALLOC( Rtm_Man_t, 1 ); + memset( pRtm, 0, sizeof(Rtm_Man_t) ); + // perform initializations + pRtm->vObjs = Vec_PtrAlloc( Aig_ManObjNum(p) ); + pRtm->vPis = Vec_PtrAlloc( Aig_ManPiNum(p) ); + pRtm->vPos = Vec_PtrAlloc( Aig_ManPoNum(p) ); + pRtm->pMem = Aig_MmFlexStart(); + return pRtm; +} + +/**Function************************************************************* + + Synopsis [Allocates the retiming manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rtm_ManFree( Rtm_Man_t * p ) +{ + Vec_PtrFree( p->vObjs ); + Vec_PtrFree( p->vPis ); + Vec_PtrFree( p->vPos ); + Aig_MmFlexStop( p->pMem, 0 ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Counts the maximum number of latches on an edge.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rtm_ManLatchMax( Rtm_Man_t * p ) +{ + Rtm_Obj_t * pObj; + Rtm_Edg_t * pEdge; + int nLatchMax = 0, i, k; + Rtm_ManForEachObj( p, pObj, i ) + Rtm_ObjForEachFaninEdge( pObj, pEdge, k ) + nLatchMax = AIG_MAX( nLatchMax, (int)pEdge->nLats ); + return nLatchMax; +} + +/**Function************************************************************* + + Synopsis [Allocates the retiming object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Rtm_Obj_t * Rtm_ObjAlloc( Rtm_Man_t * pRtm, int nFanins, int nFanouts ) +{ + Rtm_Obj_t * pObj; + int Size = sizeof(Rtm_Obj_t) + sizeof(Rtm_Obj_t *) * (nFanins + nFanouts) * 2; + pObj = (Rtm_Obj_t *)Aig_MmFlexEntryFetch( pRtm->pMem, Size ); + memset( pObj, 0, sizeof(Rtm_Obj_t) ); + pObj->Type = (int)(nFanins == 1 && nFanouts == 0); // mark PO + pObj->Num = nFanins; // temporary + pObj->Temp = nFanouts; + pObj->Id = Vec_PtrSize(pRtm->vObjs); + Vec_PtrPush( pRtm->vObjs, pObj ); + return pObj; +} + +/**Function************************************************************* + + Synopsis [Allocates the retiming object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rtm_ObjAddFanin( Rtm_Obj_t * pObj, Rtm_Obj_t * pFanin, int fCompl ) +{ + pObj->pFanio[ 2*pObj->nFanins ] = pFanin; + pObj->pFanio[ 2*pObj->nFanins + 1 ] = NULL; + pFanin->pFanio[ 2*(pFanin->Num + pFanin->nFanouts) ] = pObj; + pFanin->pFanio[ 2*(pFanin->Num + pFanin->nFanouts) + 1 ] = pObj->pFanio + 2*pObj->nFanins + 1; + if ( pObj->nFanins == 0 ) + pObj->fCompl0 = fCompl; + else if ( pObj->nFanins == 1 ) + pObj->fCompl1 = fCompl; + else + assert( 0 ); + pObj->nFanins++; + pFanin->nFanouts++; + assert( pObj->nFanins <= pObj->Num ); + assert( pFanin->nFanouts <= pFanin->Temp ); +} + +/**Function************************************************************* + + Synopsis [Check the possibility of forward retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rtm_ObjCheckRetimeFwd( Rtm_Obj_t * pObj ) +{ + Rtm_Edg_t * pEdge; + int i; + Rtm_ObjForEachFaninEdge( pObj, pEdge, i ) + if ( pEdge->nLats == 0 ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Check the possibility of forward retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj ) +{ + Rtm_Obj_t * pFanin; + int i, Degree = 0; + Rtm_ObjForEachFanin( pObj, pFanin, i ) + Degree = AIG_MAX( Degree, (int)pFanin->Num ); + return Degree + 1; +} + +/**Function************************************************************* + + Synopsis [Performs forward retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rtm_ObjRetimeFwd( Rtm_Obj_t * pObj ) +{ + Rtm_Init_t ValTotal, ValCur; + Rtm_Edg_t * pEdge; + int i; + assert( Rtm_ObjCheckRetimeFwd(pObj) ); + // extract values and compute the result + ValTotal = RTM_VAL_ONE; + Rtm_ObjForEachFaninEdge( pObj, pEdge, i ) + { + ValCur = Rtm_ObjRemFirst( pEdge ); + ValCur = Rtm_InitNotCond( ValCur, i? pObj->fCompl1 : pObj->fCompl0 ); + ValTotal = Rtm_InitAnd( ValTotal, ValCur ); + } + // insert the result in the fanout values + Rtm_ObjForEachFanoutEdge( pObj, pEdge, i ) + { + if ( pEdge->nLats >= 10 ) + printf( "Rtm_ObjRetimeFwd(); More than 10 latches on the edge!\n" ); + Rtm_ObjAddLast( pEdge, ValTotal ); + } +} + +/**Function************************************************************* + + Synopsis [Derive retiming manager from the given AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Rtm_Man_t * Rtm_ManFromAig( Aig_Man_t * p ) +{ + Rtm_Man_t * pRtm; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i; + assert( Aig_ManRegNum(p) > 0 ); + assert( Aig_ManBufNum(p) == 0 ); + // allocate the manager + pRtm = Rtm_ManAlloc( p ); + // allocate objects + pObj = Aig_ManConst1(p); + pObj->pData = Rtm_ObjAlloc( pRtm, 0, pObj->nRefs ); + Aig_ManForEachPiSeq( p, pObj, i ) + { + pObj->pData = Rtm_ObjAlloc( pRtm, 0, pObj->nRefs ); + Vec_PtrPush( pRtm->vPis, pObj->pData ); + } + Aig_ManForEachPoSeq( p, pObj, i ) + { + pObj->pData = Rtm_ObjAlloc( pRtm, 1, 0 ); + Vec_PtrPush( pRtm->vPos, pObj->pData ); + } + Aig_ManForEachLoSeq( p, pObj, i ) + pObj->pData = Rtm_ObjAlloc( pRtm, 1, pObj->nRefs ); + Aig_ManForEachLiSeq( p, pObj, i ) + pObj->pData = Rtm_ObjAlloc( pRtm, 1, 1 ); + Aig_ManForEachNode( p, pObj, i ) + pObj->pData = Rtm_ObjAlloc( pRtm, 2, pObj->nRefs ); + // connect objects + Aig_ManForEachPoSeq( p, pObj, i ) + Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + Aig_ManForEachLiSeq( p, pObj, i ) + Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + Rtm_ObjAddFanin( pObjLo->pData, pObjLi->pData, 0 ); + Aig_ManForEachNode( p, pObj, i ) + { + Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); + } + // set registers + Aig_ManForEachLoSeq( p, pObj, i ) + Rtm_ObjAddFirst( Rtm_ObjEdge(pObj->pData, 0), RTM_VAL_ZERO ); + return pRtm; +} + +/**Function************************************************************* + + Synopsis [Derive AIG manager after retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Obj_t * pObjRtm, int * pLatches ) +{ + Rtm_Edg_t * pEdge; + Aig_Obj_t * pRes, * pFanin; + int k, Val; + if ( pObjRtm->pCopy ) + return pObjRtm->pCopy; + // get the inputs + pRes = Aig_ManConst1( pNew ); + Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k ) + { + if ( pEdge->nLats == 0 ) + pFanin = Rtm_ManToAig_rec( pNew, Rtm_ObjFanin(pObjRtm, k), pLatches ); + else + { + Val = Rtm_ObjGetFirst( pEdge ); + pFanin = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + pEdge->nLats - 1 ); + pFanin = Aig_NotCond( pFanin, Val == RTM_VAL_ONE ); + } + pFanin = Aig_NotCond( pFanin, k ? pObjRtm->fCompl1 : pObjRtm->fCompl0 ); + pRes = Aig_And( pNew, pRes, pFanin ); + } + return pObjRtm->pCopy = pRes; +} + +/**Function************************************************************* + + Synopsis [Derive AIG manager after retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObjNew; + Rtm_Obj_t * pObjRtm; + Rtm_Edg_t * pEdge; + int i, k, m, Val, nLatches, * pLatches; + // count latches and mark the first latch on each edge + pLatches = ALLOC( int, 2 * Vec_PtrSize(pRtm->vObjs) ); + nLatches = 0; + Rtm_ManForEachObj( pRtm, pObjRtm, i ) + Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k ) + { + pLatches[2*pObjRtm->Id + k] = Vec_PtrSize(pRtm->vPis) + nLatches; + nLatches += pEdge->nLats; + } + // create the new manager + pNew = Aig_ManStart( Vec_PtrSize(pRtm->vObjs) + nLatches ); + // create PIs/POs and latches + pObjRtm = Vec_PtrEntry( pRtm->vObjs, 0 ); + pObjRtm->pCopy = Aig_ManConst1(pNew); + Rtm_ManForEachPi( pRtm, pObjRtm, i ) + pObjRtm->pCopy = Aig_ObjCreatePi(pNew); + for ( i = 0; i < nLatches; i++ ) + Aig_ObjCreatePi(pNew); + // create internal nodes + Rtm_ManForEachObj( pRtm, pObjRtm, i ) + Rtm_ManToAig_rec( pNew, pObjRtm, pLatches ); + // create POs + Rtm_ManForEachPo( pRtm, pObjRtm, i ) + Aig_ObjCreatePo( pNew, pObjRtm->pCopy ); + // connect latches + Rtm_ManForEachObj( pRtm, pObjRtm, i ) + Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k ) + { + if ( pEdge->nLats == 0 ) + continue; + pObjNew = Rtm_ObjFanin( pObjRtm, k )->pCopy; + for ( m = 0; m < (int)pEdge->nLats; m++ ) + { + Val = Rtm_ObjGetOne( pEdge, pEdge->nLats - 1 - m ); + pObjNew = Aig_NotCond( pObjNew, Val == RTM_VAL_ONE ); + Aig_ObjCreatePo( pNew, pObjNew ); + pObjNew = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + m ); + pObjNew = Aig_NotCond( pObjNew, Val == RTM_VAL_ONE ); + } + assert( Aig_Regular(pObjNew)->nRefs > 0 ); + } + free( pLatches ); + pNew->nRegs = nLatches; + // remove useless nodes + Aig_ManCleanup( pNew ); + if ( !Aig_ManCheck( pNew ) ) + printf( "Rtm_ManToAig: The network check has failed.\n" ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Performs forward retiming with the given limit on depth.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose ) +{ + Vec_Ptr_t * vQueue; + Aig_Man_t * pNew; + Rtm_Man_t * pRtm; + Rtm_Obj_t * pObj, * pFanout; + Aig_Obj_t * pObjAig; + int i, k, Degree, DegreeMax = 0; + // create the retiming manager + pRtm = Rtm_ManFromAig( p ); + // set the current retiming number + Rtm_ManForEachObj( pRtm, pObj, i ) + { + assert( pObj->nFanins == pObj->Num ); + assert( pObj->nFanouts == pObj->Temp ); + pObj->Num = 0; + } + + // put the LOs on the queue + vQueue = Vec_PtrAlloc( 1000 ); + Aig_ManForEachLoSeq( p, pObjAig, i ) + { + pObj = pObjAig->pData; + pObj->fMark = 1; + Vec_PtrPush( vQueue, pObj ); + } + // perform retiming + DegreeMax = 0; + Vec_PtrForEachEntry( vQueue, pObj, i ) + { + pObj->fMark = 0; + // retime the node + Rtm_ObjRetimeFwd( pObj ); + // check if its fanouts should be retimed + Rtm_ObjForEachFanout( pObj, pFanout, k ) + { + if ( pFanout->fMark ) // skip aleady scheduled + continue; + if ( pFanout->Type ) // skip POs + continue; + if ( !Rtm_ObjCheckRetimeFwd( pFanout ) ) // skip non-retimable + continue; + Degree = Rtm_ObjGetDegreeFwd( pFanout ); + DegreeMax = AIG_MAX( DegreeMax, Degree ); + if ( Degree > nStepsMax ) // skip nodes with high degree + continue; + pFanout->fMark = 1; + pFanout->Num = Degree; + Vec_PtrPush( vQueue, pFanout ); + } + } + + if ( fVerbose ) + printf( "Performed %d fwd latch moves of max depth %d and max latch count %d.\n", + Vec_PtrSize(vQueue), DegreeMax, Rtm_ManLatchMax(pRtm) ); + Vec_PtrFree( vQueue ); + + // get the new manager + pNew = Rtm_ManToAig( pRtm ); + Rtm_ManFree( pRtm ); + // group the registers + pNew = Aig_ManReduceLaches( pNew, fVerbose ); + return pNew; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/aigSeq.c b/src/aig/aig/aigSeq.c index 19466996..5bd5aaa5 100644 --- a/src/aig/aig/aigSeq.c +++ b/src/aig/aig/aigSeq.c @@ -24,6 +24,70 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define AIG_XVS0 1 +#define AIG_XVS1 2 +#define AIG_XVSX 3 + +static inline void Aig_ObjSetXsim( Aig_Obj_t * pObj, int Value ) { pObj->nCuts = Value; } +static inline int Aig_ObjGetXsim( Aig_Obj_t * pObj ) { return pObj->nCuts; } +static inline int Aig_XsimInv( int Value ) +{ + if ( Value == AIG_XVS0 ) + return AIG_XVS1; + if ( Value == AIG_XVS1 ) + return AIG_XVS0; + assert( Value == AIG_XVSX ); + return AIG_XVSX; +} +static inline int Aig_XsimAnd( int Value0, int Value1 ) +{ + if ( Value0 == AIG_XVS0 || Value1 == AIG_XVS0 ) + return AIG_XVS0; + if ( Value0 == AIG_XVSX || Value1 == AIG_XVSX ) + return AIG_XVSX; + assert( Value0 == AIG_XVS1 && Value1 == AIG_XVS1 ); + return AIG_XVS1; +} +static inline int Aig_XsimRand2() +{ + return (rand() & 1) ? AIG_XVS1 : AIG_XVS0; +} +static inline int Aig_XsimRand3() +{ + int RetValue; + do { + RetValue = rand() & 3; + } while ( RetValue == 0 ); + return RetValue; +} +static inline int Aig_ObjGetXsimFanin0( Aig_Obj_t * pObj ) +{ + int RetValue; + RetValue = Aig_ObjGetXsim(Aig_ObjFanin0(pObj)); + return Aig_ObjFaninC0(pObj)? Aig_XsimInv(RetValue) : RetValue; +} +static inline int Aig_ObjGetXsimFanin1( Aig_Obj_t * pObj ) +{ + int RetValue; + RetValue = Aig_ObjGetXsim(Aig_ObjFanin1(pObj)); + return Aig_ObjFaninC1(pObj)? Aig_XsimInv(RetValue) : RetValue; +} +static inline void Aig_XsimPrint( FILE * pFile, int Value ) +{ + if ( Value == AIG_XVS0 ) + { + fprintf( pFile, "0" ); + return; + } + if ( Value == AIG_XVS1 ) + { + fprintf( pFile, "1" ); + return; + } + assert( Value == AIG_XVSX ); + fprintf( pFile, "x" ); +} + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -493,6 +557,163 @@ int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits ) } + + +/**Function************************************************************* + + Synopsis [Cycles the circuit to create a new initial state.] + + Description [Simulates the circuit with random input for the given + number of timeframes to get a better initial state.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose ) +{ + int nRounds = 1000; // limit on the number of ternary simulation rounds + Vec_Ptr_t * vMap; + Vec_Ptr_t * vStates; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + unsigned * pState, * pPrev; + int i, k, f, fConstants, Value, nWords, nCounter; + // allocate storage for states + nWords = Aig_BitWordNum( 2*Aig_ManRegNum(p) ); + vStates = Vec_PtrAllocSimInfo( nRounds, nWords ); + // initialize the values + Aig_ObjSetXsim( Aig_ManConst1(p), AIG_XVS1 ); + Aig_ManForEachPiSeq( p, pObj, i ) + Aig_ObjSetXsim( pObj, AIG_XVSX ); + Aig_ManForEachLoSeq( p, pObj, i ) + Aig_ObjSetXsim( pObj, AIG_XVS0 ); + // simulate for the given number of timeframes + for ( f = 0; f < nRounds; f++ ) + { + // collect this state + pState = Vec_PtrEntry( vStates, f ); + memset( pState, 0, sizeof(unsigned) * nWords ); + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + { + Value = Aig_ObjGetXsim(pObjLo); + if ( Value & 1 ) + Aig_InfoSetBit( pState, 2 * i ); + if ( Value & 2 ) + Aig_InfoSetBit( pState, 2 * i + 1 ); +// Aig_XsimPrint( stdout, Value ); + } +// printf( "\n" ); + // check if this state exists + for ( i = f - 1; i >= 0; i-- ) + { + pPrev = Vec_PtrEntry( vStates, i ); + if ( !memcmp( pPrev, pState, sizeof(unsigned) * nWords ) ) + break; + } + if ( i >= 0 ) + break; + // simulate internal nodes + Aig_ManForEachNode( p, pObj, i ) + Aig_ObjSetXsim( pObj, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) ); + // transfer the latch values + Aig_ManForEachLiSeq( p, pObj, i ) + Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) ); + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) ); + } + if ( f == nRounds ) + { + printf( "Aig_ManTernarySimulate(): Did not reach a fixed point.\n" ); + Vec_PtrFree( vStates ); + return NULL; + } + // OR all the states + pState = Vec_PtrEntry( vStates, 0 ); + for ( i = 1; i <= f; i++ ) + { + pPrev = Vec_PtrEntry( vStates, i ); + for ( k = 0; k < nWords; k++ ) + pState[k] |= pPrev[k]; + } + // check if there are constants + fConstants = 0; + if ( 2*Aig_ManRegNum(p) == 32*nWords ) + { + for ( i = 0; i < nWords; i++ ) + if ( pState[i] != ~0 ) + fConstants = 1; + } + else + { + for ( i = 0; i < nWords - 1; i++ ) + if ( pState[i] != ~0 ) + fConstants = 1; + if ( pState[i] != Aig_InfoMask( 2*Aig_ManRegNum(p) - 32*(nWords-1) ) ) + fConstants = 1; + } + if ( fConstants == 0 ) + { + Vec_PtrFree( vStates ); + return NULL; + } + + // start mapping by adding the true PIs + vMap = Vec_PtrAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPiSeq( p, pObj, i ) + Vec_PtrPush( vMap, pObj ); + // find constant registers + nCounter = 0; + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + { + Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + nCounter += (Value == 1 || Value == 2); + if ( Value == 1 ) + Vec_PtrPush( vMap, Aig_ManConst0(p) ); + else if ( Value == 2 ) + Vec_PtrPush( vMap, Aig_ManConst1(p) ); + else if ( Value == 3 ) + Vec_PtrPush( vMap, pObjLo ); + else + assert( 0 ); +// Aig_XsimPrint( stdout, Value ); + } +// printf( "\n" ); + Vec_PtrFree( vStates ); + if ( fVerbose ) + printf( "Detected %d constants after %d iterations.\n", nCounter, f ); + return vMap; +} + +/**Function************************************************************* + + Synopsis [Reduces the circuit using ternary simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose ) +{ + Aig_Man_t * pTemp; + Vec_Ptr_t * vMap; + while ( vMap = Aig_ManTernarySimulate( p, fVerbose ) ) + { + if ( fVerbose ) + printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); + p = Aig_ManRemap( pTemp = p, vMap ); + Aig_ManStop( pTemp ); + Vec_PtrFree( vMap ); + Aig_ManSeqCleanup( p ); + if ( fVerbose ) + printf( "REnd = %5d. NEnd = %6d. \n", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); + } + return p; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make index d4737278..93b25e4a 100644 --- a/src/aig/aig/module.make +++ b/src/aig/aig/module.make @@ -13,5 +13,5 @@ SRC += src/aig/aig/aigCheck.c \ src/aig/aig/aigTable.c \ src/aig/aig/aigTiming.c \ src/aig/aig/aigTruth.c \ - src/aig/aig/aigUtil.c \ - src/aig/aig/aigWin.c + src/aig/aig/aigUtil.c \ + src/aig/aig/aigWin.c
\ No newline at end of file diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h index 65ab9d27..9649f870 100644 --- a/src/aig/bdc/bdcInt.h +++ b/src/aig/bdc/bdcInt.h @@ -76,7 +76,6 @@ struct Bdc_Isf_t_ unsigned * puOff; // off-set }; -typedef struct Bdc_Man_t_ Bdc_Man_t; struct Bdc_Man_t_ { // external parameters diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 5d357290..1051aa30 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -71,6 +71,7 @@ struct Fra_Par_t_ int nBTLimitMiter; // conflict limit at an output int nFramesK; // the number of timeframes to unroll int fRewrite; // use rewriting for constraint reduction + int fLatchCorr; // computes latch correspondence only }; // FRAIG equivalence classes @@ -101,6 +102,7 @@ struct Fra_Man_t_ int nFramesAll; // the number of timeframes used Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes // simulation info + void * pSim; // the simulation manager unsigned * pSimWords; // memory for simulation information int nSimWords; // the number of simulation words // counter example storage @@ -187,21 +189,23 @@ extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ); extern void Fra_ClassesStop( Fra_Cla_t * p ); extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ); extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ); -extern void Fra_ClassesPrepare( Fra_Cla_t * p ); +extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr ); extern int Fra_ClassesRefine( Fra_Cla_t * p ); extern int Fra_ClassesRefine1( Fra_Cla_t * p ); extern int Fra_ClassesCountLits( Fra_Cla_t * p ); extern int Fra_ClassesCountPairs( Fra_Cla_t * p ); extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 ); +extern void Fra_ClassesLatchCorr( Fra_Man_t * p ); /*=== fraCnf.c ========================================================*/ extern void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); /*=== fraCore.c ========================================================*/ extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars ); extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig ); extern void Fra_FraigSweep( Fra_Man_t * pManAig ); +extern int Fra_FraigMiterStatus( Aig_Man_t * p ); /*=== fraDfs.c ========================================================*/ /*=== fraInd.c ========================================================*/ -extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fVerbose ); +extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); @@ -214,6 +218,8 @@ extern void Fra_ManPrint( Fra_Man_t * p ); /*=== fraSat.c ========================================================*/ extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); +/*=== fraSec.c ========================================================*/ +extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbose, int fVeryVerbose ); /*=== fraSim.c ========================================================*/ extern int Fra_NodeHasZeroSim( Aig_Obj_t * pObj ); extern int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c new file mode 100644 index 00000000..e705f4fc --- /dev/null +++ b/src/aig/fra/fraCec.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [fraCec.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [New FRAIG package.] + + Synopsis [CEC engined based on fraiging.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraCec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 31d6270a..8923c7b0 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -250,7 +250,7 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ) SeeAlso [] ***********************************************************************/ -void Fra_ClassesPrepare( Fra_Cla_t * p ) +void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr ) { Aig_Obj_t ** ppTable, ** ppNexts; Aig_Obj_t * pObj, * pTemp; @@ -266,8 +266,16 @@ void Fra_ClassesPrepare( Fra_Cla_t * p ) Vec_PtrClear( p->vClasses1 ); Aig_ManForEachObj( p->pAig, pObj, i ) { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) - continue; + if ( fLatchCorr ) + { + if ( !Aig_ObjIsPi(pObj) ) + continue; + } + else + { + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + continue; + } //printf( "%3d : ", pObj->Id ); //Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 ); //printf( "\n" ); @@ -312,7 +320,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p ) // allocate room for classes p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) ); p->pMemClassesFree = p->pMemClasses + 2*nEntries; - + // copy the entries into storage in the topological order Vec_PtrClear( p->vClasses ); nEntries = 0; @@ -563,6 +571,32 @@ void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 ) Vec_PtrPush( p->vClasses, pClass ); } +/**Function************************************************************* + + Synopsis [Creates latch correspondence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesLatchCorr( Fra_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, nEntries = 0; + Vec_PtrClear( p->pCla->vClasses1 ); + Aig_ManForEachLoSeq( p->pManAig, pObj, i ) + { + Vec_PtrPush( p->pCla->vClasses1, pObj ); + Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) ); + } + // allocate room for classes + p->pCla->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) ); + p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 71e12a75..41d264bb 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -30,6 +30,63 @@ /**Function************************************************************* + Synopsis [Reports the status of the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_FraigMiterStatus( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pObjNew; + int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0; + if ( p->pData ) + return 0; + Aig_ManForEachPoSeq( p, pObj, i ) + { + pObjNew = Aig_ObjChild0(pObj); + // check if the output is constant 0 + if ( pObjNew == Aig_ManConst0(p) ) + { + CountConst0++; + continue; + } + // check if the output is constant 1 + if ( pObjNew == Aig_ManConst1(p) ) + { + CountNonConst0++; + continue; + } + // check if the output can be constant 0 + if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) ) + { + CountNonConst0++; + continue; + } + CountUndecided++; + } +/* + if ( p->pParams->fVerbose ) + { + printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) ); + printf( "Const0 = %d. ", CountConst0 ); + printf( "NonConst0 = %d. ", CountNonConst0 ); + printf( "Undecided = %d. ", CountUndecided ); + printf( "\n" ); + } +*/ + if ( CountNonConst0 ) + return 0; + if ( CountUndecided ) + return -1; + return 1; +} + +/**Function************************************************************* + Synopsis [Write speculative miter for one node.] Description [] @@ -121,9 +178,9 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) Vec_PtrPush( p->vTimeouts, pObj ); // simulate the counter-example and return the Fraig node Fra_Resimulate( p ); - assert( Fra_ClassObjRepr(pObj) != pObjRepr ); if ( Fra_ClassObjRepr(pObj) == pObjRepr ) printf( "Fra_FraigNode(): Error in class refinement!\n" ); + assert( Fra_ClassObjRepr(pObj) != pObjRepr ); } /**Function************************************************************* @@ -196,7 +253,7 @@ clk = clock(); Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 ); // collect initial states p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 ); - p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); + p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); p->nNodesBeg = Aig_ManNodeNum(pManAig); p->nRegsBeg = Aig_ManRegNum(pManAig); // perform fraig sweep @@ -228,7 +285,7 @@ p->timeTrav += clock() - clk2; } p->timeTotal = clock() - clk; // collect final stats - p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); + p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); p->nNodesEnd = Aig_ManNodeNum(pManAigNew); p->nRegsEnd = Aig_ManRegNum(pManAigNew); Fra_ManStop( p ); diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c new file mode 100644 index 00000000..9643b887 --- /dev/null +++ b/src/aig/fra/fraImp.c @@ -0,0 +1,826 @@ +/**CFile**************************************************************** + + FileName [fraImp.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [New FRAIG package.] + + Synopsis [Detecting and proving implications.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraImp.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// simulation manager +typedef struct Sml_Man_t_ Sml_Man_t; +struct Sml_Man_t_ +{ + Aig_Man_t * pAig; + int nFrames; + int nWordsFrame; + int nWordsTotal; + unsigned pData[0]; +}; + +static inline unsigned * Sml_ObjSim( Sml_Man_t * p, int Id ) { return p->pData + p->nWordsTotal * Id; } +static inline int Sml_ImpLeft( int Imp ) { return Imp & 0xFFFF; } +static inline int Sml_ImpRight( int Imp ) { return Imp >> 16; } +static inline int Sml_ImpCreate( int Left, int Right ) { return (Right << 16) | Left; } + +static int * s_ImpCost = NULL; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates simulation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sml_Man_t * Sml_ManStart( Aig_Man_t * pAig, int nFrames, int nWordsFrame ) +{ + Sml_Man_t * p; + assert( Aig_ManObjIdMax(pAig) + 1 < (1 << 16) ); + p = (Sml_Man_t *)malloc( sizeof(Sml_Man_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * nFrames * nWordsFrame ); + memset( p, 0, sizeof(Sml_Man_t) + sizeof(unsigned) * nFrames * nWordsFrame ); + p->nFrames = nFrames; + p->nWordsFrame = nWordsFrame; + p->nWordsTotal = nFrames * nWordsFrame; + return p; +} + +/**Function************************************************************* + + Synopsis [Deallocates simulation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sml_ManStop( Sml_Man_t * p ) +{ + free( p ); +} + + +/**Function************************************************************* + + Synopsis [Assigns random patterns to the PI node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sml_ManAssignRandom( Sml_Man_t * p, Aig_Obj_t * pObj ) +{ + unsigned * pSims; + int i; + assert( Aig_ObjIsPi(pObj) ); + pSims = Sml_ObjSim( p, pObj->Id ); + for ( i = 0; i < p->nWordsTotal; i++ ) + pSims[i] = Fra_ObjRandomSim(); +} + +/**Function************************************************************* + + Synopsis [Assigns constant patterns to the PI node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sml_ManAssignConst( Sml_Man_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame ) +{ + unsigned * pSims; + int i; + assert( Aig_ObjIsPi(pObj) ); + pSims = Sml_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = fConst1? ~(unsigned)0 : 0; +} + +/**Function************************************************************* + + Synopsis [Assings random simulation info for the PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sml_ManInitialize( Sml_Man_t * p, int fInit ) +{ + Aig_Obj_t * pObj; + int i; + if ( fInit ) + { + assert( Aig_ManRegNum(p->pAig) > 0 ); + assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); + // assign random info for primary inputs + Aig_ManForEachPiSeq( p->pAig, pObj, i ) + Sml_ManAssignRandom( p, pObj ); + // assign the initial state for the latches + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Sml_ManAssignConst( p, pObj, 0, 0 ); + } + else + { + Aig_ManForEachPi( p->pAig, pObj, i ) + Sml_ManAssignRandom( p, pObj ); + } +} + +/**Function************************************************************* + + Synopsis [Assings distance-1 simulation info for the PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sml_ManAssignDist1( Sml_Man_t * p, unsigned * pPat ) +{ + Aig_Obj_t * pObj; + int f, i, k, Limit, nTruePis; + assert( p->nFrames > 0 ); + if ( p->nFrames == 1 ) + { + // copy the PI info + Aig_ManForEachPi( p->pAig, pObj, i ) + Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 ); + // flip one bit + Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 ); + for ( i = 0; i < Limit; i++ ) + Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 ); + } + else + { + // copy the PI info for each frame + nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig); + for ( f = 0; f < p->nFrames; f++ ) + Aig_ManForEachPiSeq( p->pAig, pObj, i ) + Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f ); + // copy the latch info + k = 0; + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 ); +// assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) ); + + // flip one bit of the last frame + if ( p->nFrames == 2 ) + { + Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 ); + for ( i = 0; i < Limit; i++ ) + Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 ); +// Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig, nTruePis*(p->nFrames-2) + i)->Id ), i+1 ); + } + } +} + + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sml_NodeSimulate( Sml_Man_t * p, Aig_Obj_t * pObj, int iFrame ) +{ + unsigned * pSims, * pSims0, * pSims1; + int fCompl, fCompl0, fCompl1, i; + int nSimWords = p->nWordsFrame; + assert( !Aig_IsComplement(pObj) ); + assert( Aig_ObjIsNode(pObj) ); + assert( iFrame == 0 || nSimWords < p->nWordsTotal ); + // get hold of the simulation information + pSims = Fra_ObjSim(pObj) + nSimWords * iFrame; + pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame; + pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)) + nSimWords * iFrame; + // get complemented attributes of the children using their random info + fCompl = pObj->fPhase; + fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj)); + fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj)); + // simulate + if ( fCompl0 && fCompl1 ) + { + if ( fCompl ) + for ( i = 0; i < nSimWords; i++ ) + pSims[i] = (pSims0[i] | pSims1[i]); + else + for ( i = 0; i < nSimWords; i++ ) + pSims[i] = ~(pSims0[i] | pSims1[i]); + } + else if ( fCompl0 && !fCompl1 ) + { + if ( fCompl ) + for ( i = 0; i < nSimWords; i++ ) + pSims[i] = (pSims0[i] | ~pSims1[i]); + else + for ( i = 0; i < nSimWords; i++ ) + pSims[i] = (~pSims0[i] & pSims1[i]); + } + else if ( !fCompl0 && fCompl1 ) + { + if ( fCompl ) + for ( i = 0; i < nSimWords; i++ ) + pSims[i] = (~pSims0[i] | pSims1[i]); + else + for ( i = 0; i < nSimWords; i++ ) + pSims[i] = (pSims0[i] & ~pSims1[i]); + } + else // if ( !fCompl0 && !fCompl1 ) + { + if ( fCompl ) + for ( i = 0; i < nSimWords; i++ ) + pSims[i] = ~(pSims0[i] & pSims1[i]); + else + for ( i = 0; i < nSimWords; i++ ) + pSims[i] = (pSims0[i] & pSims1[i]); + } +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sml_NodeCopyFanin( Sml_Man_t * p, Aig_Obj_t * pObj, int iFrame ) +{ + unsigned * pSims, * pSims0; + int fCompl, fCompl0, i; + int nSimWords = p->nWordsFrame; + assert( !Aig_IsComplement(pObj) ); + assert( Aig_ObjIsPo(pObj) ); + assert( iFrame == 0 || nSimWords < p->nWordsTotal ); + // get hold of the simulation information + pSims = Sml_ObjSim(p, pObj->Id) + nSimWords * iFrame; + pSims0 = Sml_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + nSimWords * iFrame; + // get complemented attributes of the children using their random info + fCompl = pObj->fPhase; + fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj)); + // copy information as it is + if ( fCompl0 ) + for ( i = 0; i < nSimWords; i++ ) + pSims[i] = ~pSims0[i]; + else + for ( i = 0; i < nSimWords; i++ ) + pSims[i] = pSims0[i]; +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sml_NodeTransferNext( Sml_Man_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame ) +{ + unsigned * pSims0, * pSims1; + int i, nSimWords = p->nWordsFrame; + assert( !Aig_IsComplement(pOut) ); + assert( !Aig_IsComplement(pIn) ); + assert( Aig_ObjIsPo(pOut) ); + assert( Aig_ObjIsPi(pIn) ); + assert( iFrame == 0 || nSimWords < p->nWordsTotal ); + // get hold of the simulation information + pSims0 = Sml_ObjSim(p, pOut->Id) + nSimWords * iFrame; + pSims1 = Sml_ObjSim(p, pIn->Id) + nSimWords * (iFrame+1); + // copy information as it is + for ( i = 0; i < nSimWords; i++ ) + pSims1[i] = pSims0[i]; +} + + +/**Function************************************************************* + + Synopsis [Simulates AIG manager.] + + Description [Assumes that the PI simulation info is attached.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sml_SimulateOne( Sml_Man_t * p ) +{ + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int f, i, clk; +clk = clock(); + for ( f = 0; f < p->nFrames; f++ ) + { + // simulate the nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + Sml_NodeSimulate( p, pObj, f ); + if ( f == p->nFrames - 1 ) + break; + // copy simulation info into outputs + Aig_ManForEachLiSeq( p->pAig, pObj, i ) + Sml_NodeCopyFanin( p, pObj, f ); + // copy simulation info into the inputs +// for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) +// Sml_NodeTransferNext( p, Aig_ManLi(p->pAig, i), Aig_ManLo(p->pAig, i), f ); + Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i ) + Sml_NodeTransferNext( p, pObjLi, pObjLo, f ); + } +//p->timeSim += clock() - clk; +//p->nSimRounds++; +} + +/**Function************************************************************* + + Synopsis [Performs simulation of the uninitialized circuit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sml_Man_t * Sml_ManSimulateComb( Aig_Man_t * pAig, int nWords ) +{ + Sml_Man_t * p; + p = Sml_ManStart( pAig, 1, nWords ); + Sml_ManInitialize( p, 0 ); + Sml_SimulateOne( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [Performs simulation of the initialized circuit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sml_Man_t * Sml_ManSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords ) +{ + Sml_Man_t * p; + p = Sml_ManStart( pAig, nFrames, nWords ); + Sml_ManInitialize( p, 1 ); + Sml_SimulateOne( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [Counts the number of 1s in each siminfo of each node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Sml_ManCountOnes( Sml_Man_t * p ) +{ + Aig_Obj_t * pObj; + unsigned * pSim; + int i, k, * pnBits; + pnBits = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 ); + memset( pnBits, 0, sizeof(int) * Aig_ManObjIdMax(p->pAig) + 1 ); + Aig_ManForEachObj( p->pAig, pObj, i ) + { + pSim = Sml_ObjSim( p, i ); + for ( k = 0; k < p->nWordsTotal; k++ ) + pnBits[i] += Aig_WordCountOnes( pSim[k] ); + } + return pnBits; +} + +/**Function************************************************************* + + Synopsis [Counts the number of 1s in the reverse implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Sml_NodeNotImpCost( Sml_Man_t * p, int Left, int Right ) +{ + unsigned * pSimL, * pSimR; + int k, Counter = 0; + pSimL = Sml_ObjSim( p, Left ); + pSimR = Sml_ObjSim( p, Right ); + for ( k = 0; k < p->nWordsTotal; k++ ) + Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if implications holds.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Sml_NodeCheckImp( Sml_Man_t * p, int Left, int Right ) +{ + unsigned * pSimL, * pSimR; + int k; + pSimL = Sml_ObjSim( p, Left ); + pSimR = Sml_ObjSim( p, Right ); + for ( k = 0; k < p->nWordsTotal; k++ ) + if ( pSimL[k] & ~pSimR[k] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns the array of nodes sorted by the number of 1s.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Sml_ManSortUsingOnes( Sml_Man_t * p ) +{ + Aig_Obj_t * pObj; + Vec_Ptr_t * vNodes; + int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory; + // count 1s in each node's siminfo + pnBits = Sml_ManCountOnes( p ); + // count number of nodes having that many 1s + nBits = p->nWordsTotal * 32; + assert( nBits >= 32 ); + nNodes = 0; + pnNodes = ALLOC( int, nBits ); + memset( pnNodes, 0, sizeof(int) * nBits ); + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( i == 0 ) continue; + assert( pnBits[i] < nBits ); // "<" because of normalized info + pnNodes[pnBits[i]]++; + nNodes++; + } + // allocate memory for all the nodes + pMemory = ALLOC( int, nNodes + nBits ); + // markup the memory for each node + vNodes = Vec_PtrAlloc( nBits ); + Vec_PtrPush( vNodes, pMemory ); + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( i == 0 ) continue; + pMemory += pnBits[i-1] + 1; + Vec_PtrPush( vNodes, pMemory ); + } + // add the nodes + memset( pnNodes, 0, sizeof(int) * nBits ); + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( i == 0 ) continue; + pMemory = Vec_PtrEntry( vNodes, pnBits[i] ); + pMemory[ pnNodes[pnBits[i]]++ ] = i; + } + // add 0s in the end + nTotal = 0; + Vec_PtrForEachEntry( vNodes, pMemory, i ) + { + pMemory[ pnNodes[i]++ ] = 0; + nTotal += pnNodes[i]; + } + assert( nTotal == nNodes + nBits ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Compares two implications using their cost.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sml_CompareCost( int * pNum1, int * pNum2 ) +{ + int Cost1 = s_ImpCost[*pNum1]; + int Cost2 = s_ImpCost[*pNum2]; + if ( Cost1 > Cost2 ) + return -1; + if ( Cost1 < Cost2 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Compares two implications using their largest ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 ) +{ + int Max1 = AIG_MAX( pImp1[0], pImp1[1] ); + int Max2 = AIG_MAX( pImp2[0], pImp2[1] ); + if ( Max1 < Max2 ) + return -1; + if ( Max1 > Max2 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Derives implication candidates.] + + Description [Implication candidates have the property that + (1) they hold using sequential simulation information + (2) they do not hold using combinational simulation information + (3) they have as high expressive power as possible (heuristically) + - this means they are relatively far in terms of Humming distance + meaning their complement covers a larger Boolean space + - they are easy to disprove combinationally + meaning they cover relatively a larger sequential subspace.] + + SideEffects [The managers should have the first pattern (000...)] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Sml_ManImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit ) +{ + Sml_Man_t * pSeq, * pComb; + Vec_Int_t * vImps, * vTemp; + Vec_Ptr_t * vNodes; + int * pNodesI, * pNodesK, * pNumbers; + int i, k, Imp; + assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit ); + // normalize both managers + pComb = Sml_ManSimulateComb( p->pManAig, 32 ); + pSeq = Sml_ManSimulateSeq( p->pManAig, 32, 1 ); + // get the nodes sorted by the number of 1s + vNodes = Sml_ManSortUsingOnes( pSeq ); + // compute implications and their costs + s_ImpCost = ALLOC( int, nImpMaxLimit ); + vImps = Vec_IntAlloc( nImpMaxLimit ); + for ( k = pSeq->nWordsTotal * 32 - 1; k >= 0; k-- ) + for ( i = k - 1; i >= 0; i-- ) + { + for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ ) + for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ ) + { + if ( Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) && + !Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) ) + { + Imp = Sml_ImpCreate( *pNodesI, *pNodesK ); + s_ImpCost[ Vec_IntSize(vImps) ] = Sml_NodeNotImpCost(pComb, *pNodesI, *pNodesK); + Vec_IntPush( vImps, Imp ); + } + if ( Vec_IntSize(vImps) == nImpMaxLimit ) + goto finish; + } + } +finish: + Sml_ManStop( pComb ); + Sml_ManStop( pSeq ); + + // sort implications by their cost + pNumbers = ALLOC( int, Vec_IntSize(vImps) ); + for ( i = 0; i < Vec_IntSize(vImps); i++ ) + pNumbers[i] = i; + qsort( (void *)pNumbers, Vec_IntSize(vImps), sizeof(int), + (int (*)(const void *, const void *)) Sml_CompareCost ); + // reorder implications + vTemp = Vec_IntAlloc( nImpUseLimit ); + for ( i = 0; i < nImpUseLimit; i++ ) + Vec_IntPush( vTemp, Vec_IntEntry( vImps, pNumbers[i] ) ); + Vec_IntFree( vImps ); vImps = vTemp; + // dealloc + free( pNumbers ); + free( s_ImpCost ); s_ImpCost = NULL; + free( Vec_PtrEntry(vNodes, 0) ); + Vec_PtrFree( vNodes ); + // order implications by the max ID involved + qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int), + (int (*)(const void *, const void *)) Sml_CompareMaxId ); + return vImps; +} + +// the following three procedures are called to +// - add implications to the SAT solver +// - check implications using the SAT solver +// - refine implications using after a cex is generated + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps ) +{ + sat_solver * pSat = p->pSat; + Aig_Obj_t * pLeft, * pRight; + Aig_Obj_t * pLeftF, * pRightF; + int pLits[2], Imp, Left, Right, i, f, status; + Vec_IntForEachEntry( vImps, Imp, i ) + { + // get the corresponding nodes + pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) ); + pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) ); + // add constraints in each timeframe + for ( f = 0; f < p->pPars->nFramesK; f++ ) + { + // map these info fraig + pLeftF = Fra_ObjFraig( pLeft, f ); + pRightF = Fra_ObjFraig( pRight, f ); + // get the corresponding SAT numbers + Left = Fra_ObjSatNum( Aig_Regular(pLeftF) ); + Right = Fra_ObjSatNum( Aig_Regular(pRightF) ); + assert( Left > 0 && Left < p->nSatVars ); + assert( Right > 0 && Right < p->nSatVars ); + // get the constaint + // L => R L' v R L & R' + pLits[0] = 2 * Left + !Aig_ObjPhaseReal(pLeftF); + pLits[1] = 2 * Right + Aig_ObjPhaseReal(pRightF); + // add contraint to solver + if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) ) + { + sat_solver_delete( pSat ); + p->pSat = NULL; + return; + } + } + } + status = sat_solver_simplify(pSat); + if ( status == 0 ) + { + sat_solver_delete( pSat ); + p->pSat = NULL; + } +} + +/**Function************************************************************* + + Synopsis [Check implications for the node (if they are present).] + + Description [Returns the new position in the array.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos ) +{ + Aig_Obj_t * pLeft, * pRight; + int i, Imp, Left, Right, Max; + Vec_IntForEachEntryStart( vImps, Imp, i, Pos ) + { + Left = Sml_ImpLeft(Imp); + Right = Sml_ImpRight(Imp); + Max = AIG_MAX( Left, Right ); + assert( Max >= pNode->Id ); + if ( Max > pNode->Id ) + return i; + // get the corresponding nodes + pLeft = Aig_ManObj( p->pManAig, Left ); + pRight = Aig_ManObj( p->pManAig, Right ); + // check the implication + // - if true, a clause is added + // - if false, a cex is simulated +// Fra_NodesAreImp( p, pLeft, pRight ); + // make sure the implication is refined + assert( Vec_IntEntry(vImps, Pos) == 0 ); + } + return i; +} + +/**Function************************************************************* + + Synopsis [Removes those implications that no longer hold.] + + Description [Returns 1 if refinement has happened.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps ) +{ + Aig_Obj_t * pLeft, * pRight; + int Imp, i, RetValue = 0; + Vec_IntForEachEntry( vImps, Imp, i ) + { + if ( Imp == 0 ) + continue; + // get the corresponding nodes + pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) ); + pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) ); + // check if implication holds using this simulation info + if ( !Sml_NodeCheckImp(p->pSim, pLeft->Id, pRight->Id) ) + { + Vec_IntWriteEntry( vImps, i, 0 ); + RetValue = 1; + } + } + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Removes empty implications.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ImpCompactArray( Vec_Int_t * vImps ) +{ + int i, k, Imp; + k = 0; + Vec_IntForEachEntry( vImps, Imp, i ) + if ( Imp ) + Vec_IntWriteEntry( vImps, k++, Imp ); + Vec_IntShrink( vImps, k ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index bb4c4287..4a7d7b7e 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -198,7 +198,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fVerbose ) +Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter ) { Fra_Man_t * p; Fra_Par_t Pars, * pPars = &Pars; @@ -208,7 +208,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int nIter, i, clk = clock(), clk2; if ( Aig_ManNodeNum(pManAig) == 0 ) + { + if ( pnIter ) *pnIter = 0; return Aig_ManDup(pManAig, 1); + } assert( Aig_ManLatchNum(pManAig) == 0 ); assert( Aig_ManRegNum(pManAig) > 0 ); assert( nFramesK > 0 ); @@ -216,14 +219,18 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, // get parameters Fra_ParamsDefaultSeq( pPars ); - pPars->nFramesK = nFramesK; - pPars->fVerbose = fVerbose; - pPars->fRewrite = fRewrite; + pPars->nFramesK = nFramesK; + pPars->fVerbose = fVerbose; + pPars->fRewrite = fRewrite; + pPars->fLatchCorr = fLatchCorr; // start the fraig manager for this run p = Fra_ManStart( pManAig, pPars ); // derive and refine e-classes using K initialized frames - Fra_Simulate( p, 1 ); +// if ( fLatchCorr ) +// Fra_ClassesLatchCorr( p ); +// else + Fra_Simulate( p, 1 ); // refine e-classes using sequential simulation? p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 ); @@ -239,6 +246,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, p->pCla->fRefinement = 0; // derive non-init K-timeframes while implementing e-classes p->pManFraig = Fra_FramesWithClasses( p ); +//Aig_ManDumpBlif( p->pManFraig, "testaig.blif" ); + // perform AIG rewriting if ( p->pPars->fRewrite ) Fra_FraigInductionRewrite( p ); @@ -252,8 +261,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, } // convert the manager to SAT solver (the last nLatches outputs are inputs) - pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); -// pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); +// pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); + pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); p->pSat = Cnf_DataWriteIntoSolver( pCnf ); @@ -278,7 +287,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, Fra_ObjSetFaninVec( pObj, (void *)1 ); } Cnf_DataFree( pCnf ); -/* +/* Aig_ManForEachObj( p->pManFraig, pObj, i ) { Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); @@ -300,6 +309,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, clk2 = clock(); Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); pManAigNew = Aig_ManDupRepr( pManAig ); + Aig_ManSeqCleanup( pManAigNew ); +// Aig_ManCountMergeRegs( pManAigNew ); p->timeTrav += clock() - clk2; p->timeTotal = clock() - clk; // get the final stats @@ -309,9 +320,10 @@ p->timeTotal = clock() - clk; // free the manager Fra_ManStop( p ); // check the output - if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 ) - if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) ) - printf( "Proved output constant 0.\n" ); +// if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 ) +// if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) ) +// printf( "Proved output constant 0.\n" ); + if ( pnIter ) *pnIter = nIter; return pManAigNew; } diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index 95cf28d8..4dcc4988 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -86,6 +86,7 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) pPars->nFramesK = 1; // the number of timeframes to unroll pPars->fConeBias = 0; pPars->fRewrite = 0; + pPars->fLatchCorr = 0; } /**Function************************************************************* diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c new file mode 100644 index 00000000..d3fdbcfd --- /dev/null +++ b/src/aig/fra/fraPart.c @@ -0,0 +1,177 @@ +/**CFile**************************************************************** + + FileName [fraPart.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [New FRAIG package.] + + Synopsis [Partitioning for induction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraPart.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim ) +{ + ProgressBar * pProgress; + Vec_Vec_t * vSupps, * vSuppsIn; + Vec_Ptr_t * vSuppsNew; + Vec_Int_t * vSupNew, * vSup, * vSup2, * vTemp;//, * vSupIn; + Vec_Int_t * vOverNew, * vQuantNew; + Aig_Obj_t * pObj; + int i, k, nCommon, CountOver, CountQuant; + int nTotalSupp, nTotalSupp2, Entry, Largest;//, iVar; + double Ratio, R; + int clk; + + nTotalSupp = 0; + nTotalSupp2 = 0; + Ratio = 0.0; + + // compute supports +clk = clock(); + vSupps = Aig_ManSupports( p ); +PRT( "Supports", clock() - clk ); + // remove last entry + Aig_ManForEachPo( p, pObj, i ) + { + vSup = Vec_VecEntry( vSupps, i ); + Vec_IntPop( vSup ); + // remember support +// pObj->pNext = (Aig_Obj_t *)vSup; + } + + // create reverse supports +clk = clock(); + vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + { + vSup = Vec_VecEntry( vSupps, i ); + Vec_IntForEachEntry( vSup, Entry, k ) + Vec_VecPush( vSuppsIn, Entry, (void *)i ); + } +PRT( "Inverse ", clock() - clk ); + +clk = clock(); + // compute extended supports + Largest = 0; + vSuppsNew = Vec_PtrAlloc( Aig_ManPoNum(p) ); + vOverNew = Vec_IntAlloc( Aig_ManPoNum(p) ); + vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) ); + pProgress = Extra_ProgressBarStart( stdout, Aig_ManPoNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // get old supports + vSup = Vec_VecEntry( vSupps, i ); + if ( Vec_IntSize(vSup) < 2 ) + continue; + // compute new supports + CountOver = CountQuant = 0; + vSupNew = Vec_IntDup( vSup ); + // go through the nodes where the first var appears + Aig_ManForEachPo( p, pObj, k ) +// iVar = Vec_IntEntry( vSup, 0 ); +// vSupIn = Vec_VecEntry( vSuppsIn, iVar ); +// Vec_IntForEachEntry( vSupIn, Entry, k ) + { +// pObj = Aig_ManObj( p, Entry ); + // get support of this output +// vSup2 = (Vec_Int_t *)pObj->pNext; + vSup2 = Vec_VecEntry( vSupps, k ); + // count the number of common vars + nCommon = Vec_IntTwoCountCommon(vSup, vSup2); + if ( nCommon < 2 ) + continue; + if ( nCommon > nComLim ) + { + vSupNew = Vec_IntTwoMerge( vTemp = vSupNew, vSup2 ); + Vec_IntFree( vTemp ); + CountOver++; + } + else + CountQuant++; + } + // save the results + Vec_PtrPush( vSuppsNew, vSupNew ); + Vec_IntPush( vOverNew, CountOver ); + Vec_IntPush( vQuantNew, CountQuant ); + + if ( Largest < Vec_IntSize(vSupNew) ) + Largest = Vec_IntSize(vSupNew); + + nTotalSupp += Vec_IntSize(vSup); + nTotalSupp2 += Vec_IntSize(vSupNew); + if ( Vec_IntSize(vSup) ) + R = Vec_IntSize(vSupNew) / Vec_IntSize(vSup); + else + R = 0; + Ratio += R; + + if ( R < 5.0 ) + continue; + + printf( "%6d : ", i ); + printf( "S = %5d. ", Vec_IntSize(vSup) ); + printf( "SNew = %5d. ", Vec_IntSize(vSupNew) ); + printf( "R = %7.2f. ", R ); + printf( "Over = %5d. ", CountOver ); + printf( "Quant = %5d. ", CountQuant ); + printf( "\n" ); +/* + Vec_IntForEachEntry( vSupNew, Entry, k ) + printf( "%d ", Entry ); + printf( "\n" ); +*/ + } + Extra_ProgressBarStop( pProgress ); +PRT( "Scanning", clock() - clk ); + + // print cumulative statistics + printf( "PIs = %6d. POs = %6d. Lim = %3d. AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n", + Aig_ManPiNum(p), Aig_ManPoNum(p), nComLim, + nTotalSupp/Aig_ManPoNum(p), nTotalSupp2/Aig_ManPoNum(p), + Ratio/Aig_ManPoNum(p), Largest ); + + Vec_VecFree( vSupps ); + Vec_VecFree( vSuppsIn ); + Vec_VecFree( (Vec_Vec_t *)vSuppsNew ); + Vec_IntFree( vOverNew ); + Vec_IntFree( vQuantNew ); +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c new file mode 100644 index 00000000..6afa6f89 --- /dev/null +++ b/src/aig/fra/fraSec.c @@ -0,0 +1,95 @@ +/**CFile**************************************************************** + + FileName [fraSec.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [New FRAIG package.] + + Synopsis [Performs SEC based on seq sweeping.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraSec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose ) +{ + Aig_Man_t * pNew; + int nFrames, RetValue, nIter, clk, clkTotal = clock(); + if ( nFramesFix ) + { + nFrames = nFramesFix; + // perform seq sweeping for one frame number + pNew = Fra_FraigInduction( p, nFrames, 0, 0, fVeryVerbose, &nIter ); + } + else + { + // perform seq sweeping while increasing the number of frames + for ( nFrames = 1; ; nFrames++ ) + { +clk = clock(); + pNew = Fra_FraigInduction( p, nFrames, 0, 0, fVeryVerbose, &nIter ); + RetValue = Fra_FraigMiterStatus( pNew ); + if ( fVerbose ) + { + printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter ); + if ( RetValue == 1 ) + printf( "UNSAT " ); + else + printf( "UNDECIDED " ); +PRT( "Time", clock() - clk ); + } + if ( RetValue != -1 ) + break; + Aig_ManStop( pNew ); + } + } + + // get the miter status + RetValue = Fra_FraigMiterStatus( pNew ); + Aig_ManStop( pNew ); + + // report the miter + if ( RetValue == 1 ) + printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter ); + else if ( RetValue == 0 ) + printf( "Networks are NOT EQUIVALENT. " ); + else + printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter ); +PRT( "Time", clock() - clkTotal ); + return RetValue; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 4a6e0251..c17cea9f 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -537,7 +537,7 @@ int Fra_SelectBestPat( Fra_Man_t * p ) ***********************************************************************/ void Fra_SimulateOne( Fra_Man_t * p ) { - Aig_Obj_t * pObj; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; int f, i, clk; clk = clock(); for ( f = 0; f < p->nFramesAll; f++ ) @@ -551,9 +551,10 @@ clk = clock(); Aig_ManForEachLiSeq( p->pManAig, pObj, i ) Fra_NodeCopyFanin( p, pObj, f ); // copy simulation info into the inputs - for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ ) - Fra_NodeTransferNext( p, Aig_ManLi(p->pManAig, i), Aig_ManLo(p->pManAig, i), f ); - +// for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ ) +// Fra_NodeTransferNext( p, Aig_ManLi(p->pManAig, i), Aig_ManLo(p->pManAig, i), f ); + Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, i ) + Fra_NodeTransferNext( p, pObjLi, pObjLo, f ); } p->timeSim += clock() - clk; p->nSimRounds++; @@ -627,7 +628,7 @@ void Fra_Simulate( Fra_Man_t * p, int fInit ) // start the classes Fra_AssignRandom( p, fInit ); Fra_SimulateOne( p ); - Fra_ClassesPrepare( p->pCla ); + Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr ); // Fra_ClassesPrint( p->pCla, 0 ); //printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) ); diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make index 191427c9..f2a8b230 100644 --- a/src/aig/fra/module.make +++ b/src/aig/fra/module.make @@ -1,7 +1,10 @@ -SRC += src/aig/fra/fraClass.c \ +SRC += src/aig/fra/fraCec.c \ + src/aig/fra/fraClass.c \ src/aig/fra/fraCnf.c \ src/aig/fra/fraCore.c \ + src/aig/fra/fraImp.c \ src/aig/fra/fraInd.c \ src/aig/fra/fraMan.c \ src/aig/fra/fraSat.c \ + src/aig/fra/fraSec.c \ src/aig/fra/fraSim.c diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 7d8d0f0f..00d8911b 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -1086,6 +1086,89 @@ void Abc_NtkMakeComb( Abc_Ntk_t * pNtk ) } +/**Function************************************************************* + + Synopsis [Removes POs with suppsize less than 2 and PIs without fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkTrim( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int i, k, m; + + // filter POs + k = m = 0; + Abc_NtkForEachCo( pNtk, pObj, i ) + { + if ( Abc_ObjIsPo(pObj) ) + { + // remove constant nodes and PI pointers + if ( Abc_ObjFaninNum(Abc_ObjFanin0(pObj)) == 0 ) + { + Abc_ObjDeleteFanin( pObj, Abc_ObjFanin0(pObj) ); + if ( Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) == 0 && !Abc_ObjIsPi(Abc_ObjFanin0(pObj)) ) + Abc_NtkDeleteObj_rec( Abc_ObjFanin0(pObj), 1 ); + pNtk->vObjs->pArray[pObj->Id] = NULL; + pObj->Id = (1<<26)-1; + pNtk->nObjCounts[pObj->Type]--; + pNtk->nObjs--; + Abc_ObjRecycle( pObj ); + continue; + } + // remove buffers/inverters of PIs + if ( Abc_ObjFaninNum(Abc_ObjFanin0(pObj)) == 1 ) + { + if ( Abc_ObjIsPi(Abc_ObjFanin0(Abc_ObjFanin0(pObj))) ) + { + Abc_ObjDeleteFanin( pObj, Abc_ObjFanin0(pObj) ); + if ( Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) == 0 ) + Abc_NtkDeleteObj_rec( Abc_ObjFanin0(pObj), 1 ); + pNtk->vObjs->pArray[pObj->Id] = NULL; + pObj->Id = (1<<26)-1; + pNtk->nObjCounts[pObj->Type]--; + pNtk->nObjs--; + Abc_ObjRecycle( pObj ); + continue; + } + } + Vec_PtrWriteEntry( pNtk->vPos, m++, pObj ); + } + Vec_PtrWriteEntry( pNtk->vCos, k++, pObj ); + } + Vec_PtrShrink( pNtk->vPos, m ); + Vec_PtrShrink( pNtk->vCos, k ); + + // filter PIs + k = m = 0; + Abc_NtkForEachCi( pNtk, pObj, i ) + { + if ( Abc_ObjIsPi(pObj) ) + { + if ( Abc_ObjFanoutNum(pObj) == 0 ) + { + pNtk->vObjs->pArray[pObj->Id] = NULL; + pObj->Id = (1<<26)-1; + pNtk->nObjCounts[pObj->Type]--; + pNtk->nObjs--; + Abc_ObjRecycle( pObj ); + continue; + } + Vec_PtrWriteEntry( pNtk->vPis, m++, pObj ); + } + Vec_PtrWriteEntry( pNtk->vCis, k++, pObj ); + } + Vec_PtrShrink( pNtk->vPis, m ); + Vec_PtrShrink( pNtk->vCis, k ); + + return Abc_NtkDup( pNtk ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3a916fdc..1b5e2361 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -93,6 +93,7 @@ static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTrim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -171,6 +172,7 @@ static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -257,6 +259,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 ); Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 ); Cmd_CommandAdd( pAbc, "Various", "topmost", Abc_CommandTopmost, 1 ); + Cmd_CommandAdd( pAbc, "Various", "trim", Abc_CommandTrim, 1 ); Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 ); Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 ); @@ -335,6 +338,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "dsec", Abc_CommandDSec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); @@ -5134,6 +5138,84 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTrim( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c, nLevels; + extern Abc_Ntk_t * Abc_NtkTrim( Abc_Ntk_t * pNtk ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nLevels = 10; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF ) + { + switch ( c ) + { +/* + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nLevels = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLevels < 0 ) + goto usage; + break; +*/ + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for logic circuits.\n" ); + return 0; + } + + pNtkRes = Abc_NtkTrim( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "The command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: trim [-h]\n" ); + fprintf( pErr, "\t removes POs fed by PIs and constants, and PIs w/o fanout\n" ); +// fprintf( pErr, "\t-N num : max number of levels [default = %d]\n", nLevels ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* @@ -6085,6 +6167,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ); + extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk ); + extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -6200,10 +6284,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Network should be strashed. Command has failed.\n" ); return 1; } -// pNtkRes = Abc_NtkDar( pNtk ); - pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" ); */ - pNtkRes = NULL; + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); + return 0; + } + +// pNtkRes = Abc_NtkDar( pNtk ); + pNtkRes = Abc_NtkDarRetime( pNtk, 100, 1 ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -6211,7 +6301,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); - return 0; usage: fprintf( pErr, "usage: test [-h]\n" ); @@ -6627,6 +6716,11 @@ int Abc_CommandICut( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } Abc_NtkIvyCuts( pNtk, nInputs ); return 0; @@ -6690,6 +6784,11 @@ int Abc_CommandIRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkIvyRewrite( pNtk, fUpdateLevel, fUseZeroCost, fVerbose ); if ( pNtkRes == NULL ) @@ -6790,6 +6889,11 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkDRewrite( pNtk, pPars ); if ( pNtkRes == NULL ) { @@ -6904,6 +7008,11 @@ int Abc_CommandDRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } if ( pPars->nLeafMax < 4 || pPars->nLeafMax > 15 ) { fprintf( pErr, "This command only works for cut sizes 4 <= K <= 15.\n" ); @@ -6986,6 +7095,11 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkDCompress2( pNtk, fBalance, fUpdateLevel, fVerbose ); if ( pNtkRes == NULL ) { @@ -7054,6 +7168,11 @@ int Abc_CommandDrwsat( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkDrwsat( pNtk, fBalance, fVerbose ); if ( pNtkRes == NULL ) { @@ -7124,6 +7243,11 @@ int Abc_CommandIRewriteSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkIvyRewriteSeq( pNtk, fUseZeroCost, fVerbose ); if ( pNtkRes == NULL ) @@ -7192,6 +7316,11 @@ int Abc_CommandIResyn( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkIvyResyn( pNtk, fUpdateLevel, fVerbose ); if ( pNtkRes == NULL ) @@ -7273,6 +7402,11 @@ int Abc_CommandISat( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkIvySat( pNtk, nConfLimit, fVerbose ); if ( pNtkRes == NULL ) @@ -7359,6 +7493,11 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose ); if ( pNtkRes == NULL ) @@ -7453,6 +7592,11 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fChoicing, fVerbose ); if ( pNtkRes == NULL ) @@ -7557,6 +7701,11 @@ int Abc_CommandCSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "The number of leaves is infeasible.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkCSweep( pNtk, nCutsMax, nLeafMax, fVerbose ); if ( pNtkRes == NULL ) @@ -7728,6 +7877,11 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkIvyHaig( pNtk, nIters, fUseZeroCost, fVerbose ); if ( pNtkRes == NULL ) @@ -10417,9 +10571,10 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) int c, nMaxIters; int fForward; int fBackward; + int fOneStep; int fVerbose; int Mode; - extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fVerbose ); + extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fOneStep, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -10429,10 +10584,11 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) Mode = 5; fForward = 0; fBackward = 0; + fOneStep = 0; fVerbose = 0; nMaxIters = 15; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Mfbvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Mfbsvh" ) ) != EOF ) { switch ( c ) { @@ -10453,6 +10609,9 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'b': fBackward ^= 1; break; + case 's': + fOneStep ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -10497,7 +10656,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) // convert the network into an SOP network pNtkRes = Abc_NtkToLogic( pNtk ); // perform the retiming - Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fVerbose ); + Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fOneStep, fVerbose ); // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; @@ -10517,7 +10676,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) } // perform the retiming - Abc_NtkRetime( pNtk, Mode, fForward, fBackward, fVerbose ); + Abc_NtkRetime( pNtk, Mode, fForward, fBackward, fOneStep, fVerbose ); return 0; usage: @@ -10532,6 +10691,7 @@ usage: fprintf( pErr, "\t-M num : the retiming algorithm to use [default = %d]\n", Mode ); fprintf( pErr, "\t-f : enables forward-only retiming in modes 3,4,5 [default = %s]\n", fForward? "yes": "no" ); fprintf( pErr, "\t-b : enables backward-only retiming in modes 3,4,5 [default = %s]\n", fBackward? "yes": "no" ); + fprintf( pErr, "\t-s : enables retiming one step only in mode 4 [default = %s]\n", fOneStep? "yes": "no" ); fprintf( pErr, "\t-v : enables verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -10816,21 +10976,23 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) int fExdc; int fImp; int fRewrite; + int fLatchCorr; int fVerbose; - extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fLatchCorr, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nFramesK = 1; - fExdc = 1; - fImp = 0; - fRewrite = 0; - fVerbose = 0; + nFramesK = 1; + fExdc = 1; + fImp = 0; + fRewrite = 0; + fLatchCorr = 0; + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Feirvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Feirlvh" ) ) != EOF ) { switch ( c ) { @@ -10854,6 +11016,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fRewrite ^= 1; break; + case 'l': + fLatchCorr ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -10883,7 +11048,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fVerbose ); + pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fLatchCorr, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential sweeping has failed.\n" ); @@ -10894,11 +11059,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ssweep [-F num] [-rvh]\n" ); + fprintf( pErr, "usage: ssweep [-F num] [-lrvh]\n" ); fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK ); // fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" ); // fprintf( pErr, "\t-i : toggle computing implications [default = %s]\n", fImp? "yes": "no" ); + fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" ); fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -10919,11 +11085,12 @@ usage: int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk; + Abc_Ntk_t * pNtk, * pNtkRes, * pTemp; int c; int fLatchSweep; int fAutoSweep; int fVerbose; + extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -10964,14 +11131,31 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } // modify the current network - Abc_NtkCleanupSeq( pNtk, fLatchSweep, fAutoSweep, fVerbose ); + + // get the new network + pNtkRes = Abc_NtkDup( pNtk ); + Abc_NtkCleanupSeq( pNtkRes, 0, fAutoSweep, fVerbose ); + if ( fLatchSweep ) + { + pNtkRes = Abc_NtkStrash( pTemp = pNtkRes, 0, 0, 0 ); + Abc_NtkDelete( pTemp ); + pNtkRes = Abc_NtkDarLatchSweep( pTemp = pNtkRes, fVerbose ); + Abc_NtkDelete( pTemp ); + } + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Sequential cleanup has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: fprintf( pErr, "usage: scleanup [-lavh]\n" ); fprintf( pErr, "\t performs sequential cleanup\n" ); fprintf( pErr, "\t - removes nodes/latches that do not feed into POs\n" ); - fprintf( pErr, "\t - removes and shared latches driven by constants\n" ); + fprintf( pErr, "\t - removes stuck-at and identical latches (latch sweep)\n" ); fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" ); fprintf( pErr, "\t (the latter may change sequential behaviour)\n" ); fprintf( pErr, "\t-l : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" ); @@ -11402,17 +11586,17 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( Abc_NtkLatchNum(pNtk) == 0 ) - { - printf( "The network has no latches. Used combinational command \"cec\".\n" ); - return 0; - } - pArgvNew = argv + globalUtilOptind; nArgcNew = argc - globalUtilOptind; if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) return 1; + if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 ) + { + printf( "The network has no latches. Used combinational command \"cec\".\n" ); + return 0; + } + // perform equivalence checking if ( fRetime ) Abc_NtkSecRetime( pNtk1, pNtk2 ); @@ -11454,6 +11638,97 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtk1, * pNtk2; + int fDelete1, fDelete2; + char ** pArgvNew; + int nArgcNew; + int c; + int fVerbose; + int fVeryVerbose; + int nFrames; + + extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nFrames = 0; // if 0, iterates through frames + fVerbose = 1; + fVeryVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Fwvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames <= 0 ) + goto usage; + break; + case 'w': + fVeryVerbose ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + default: + goto usage; + } + } + + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) + return 1; + + if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 ) + { + printf( "The network has no latches. Used combinational command \"cec\".\n" ); + return 0; + } + + // perform verification + Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fVerbose, fVeryVerbose ); + + if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); + if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); + return 0; + +usage: + fprintf( pErr, "usage: dsec [-F num] [-wvh] <file1> <file2>\n" ); + fprintf( pErr, "\t performs inductive sequential equivalence checking\n" ); + fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames ); + fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); + fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\tfile1 : (optional) the file with the first network\n"); + fprintf( pErr, "\tfile2 : (optional) the file with the second network\n"); + fprintf( pErr, "\t if no files are given, uses the current network and its spec\n"); + fprintf( pErr, "\t if one file is given, uses the current network and the file\n"); + return 1; +} +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index ca80fec8..4013b98d 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -23,6 +23,7 @@ #include "dar.h" #include "cnf.h" #include "fra.h" +#include "fraig.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -79,11 +80,13 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) if ( Abc_LatchIsInit1(pObj) ) Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy); // perform the conversion of the internal nodes (assumes DFS ordering) +// pMan->fAddStrash = 1; Abc_NtkForEachNode( pNtk, pObj, i ) { pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) ); // printf( "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id ); } + pMan->fAddStrash = 0; // create the POs Abc_NtkForEachCo( pNtk, pObj, i ) Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) ); @@ -121,6 +124,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Abc_Ntk_t * pNtkNew; Aig_Obj_t * pObj; int i; + assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) ); // perform strashing pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); // transfer the pointers to the basic nodes @@ -147,6 +151,59 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Synopsis [Converts the network from the AIG manager into ABC.] + Description [This procedure should be called after seq sweeping, + which changes the number of registers.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObjNew; + Aig_Obj_t * pObj, * pObjLo, * pObjLi; + int i; +// assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) ); + // perform strashing + pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + Aig_ManForEachPiSeq( pMan, pObj, i ) + pObj->pData = Abc_NtkCi(pNtkNew, i); + // create as many latches as there are registers in the manager + Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i ) + { + pObjNew = Abc_NtkCreateLatch( pNtkNew ); + pObjLi->pData = Abc_NtkCreateBi( pNtkNew ); + pObjLo->pData = Abc_NtkCreateBo( pNtkNew ); + Abc_ObjAddFanin( pObjNew, pObjLi->pData ); + Abc_ObjAddFanin( pObjLo->pData, pObjNew ); + Abc_LatchSetInit0( pObjNew ); + } + Abc_NtkAddDummyBoxNames( pNtkNew ); + // rebuild the AIG + vNodes = Aig_ManDfs( pMan ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + if ( Aig_ObjIsBuf(pObj) ) + pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj); + else + pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) ); + Vec_PtrFree( vNodes ); + // connect the PO nodes + Aig_ManForEachPo( pMan, pObj, i ) + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + Description [] SideEffects [] @@ -367,55 +424,23 @@ void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) ***********************************************************************/ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) { - Abc_Ntk_t * pNtkAig; - Aig_Man_t * pMan;//, * pTemp; -// int * pArray; + Abc_Ntk_t * pNtkAig = NULL; + Aig_Man_t * pMan; + extern void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim ); assert( Abc_NtkIsStrash(pNtk) ); // convert to the AIG manager pMan = Abc_NtkToDar( pNtk, 0 ); if ( pMan == NULL ) return NULL; - if ( !Aig_ManCheck( pMan ) ) - { - printf( "Abc_NtkDar: AIG check has failed.\n" ); - Aig_ManStop( pMan ); - return NULL; - } - // perform balance - Aig_ManPrintStats( pMan ); -/* - pArray = Abc_NtkGetLatchValues(pNtk); - Aig_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray ); - free( pArray ); -*/ -// Aig_ManDumpBlif( pMan, "aig_temp.blif" ); -// pMan->pPars = Dar_ManDefaultRwrPars(); - Dar_ManRewrite( pMan, NULL ); - Aig_ManPrintStats( pMan ); -// Dar_ManComputeCuts( pMan ); - -/* -{ -extern Aig_Cnf_t * Aig_ManDeriveCnf( Aig_Man_t * p ); -extern void Aig_CnfFree( Aig_Cnf_t * pCnf ); -Aig_Cnf_t * pCnf; -pCnf = Aig_ManDeriveCnf( pMan ); -Aig_CnfFree( pCnf ); -} -*/ - - // convert from the AIG manager - if ( Aig_ManLatchNum(pMan) ) - pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan ); - else - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); - if ( pNtkAig == NULL ) - return NULL; + // perform computation +// Fra_ManPartitionTest( pMan, 4 ); + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); Aig_ManStop( pMan ); + // make sure everything is okay - if ( !Abc_NtkCheck( pNtkAig ) ) + if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) ) { printf( "Abc_NtkDar: The network check has failed.\n" ); Abc_NtkDelete( pNtkAig ); @@ -867,23 +892,146 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fVerbose ) +Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose ) { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; - pMan = Abc_NtkToDar( pNtk, 0 ); + pMan = Abc_NtkToDar( pNtk, 1 ); if ( pMan == NULL ) return NULL; - pMan->nRegs = Abc_NtkLatchNum(pNtk); +// pMan->nRegs = Abc_NtkLatchNum(pNtk); - pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fVerbose ); + pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fLatchCorr, fVerbose, NULL ); Aig_ManStop( pTemp ); - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + else + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose ) +{ + Fraig_Params_t Params; + Aig_Man_t * pMan; + Abc_Ntk_t * pMiter, * pTemp; + int RetValue; + + // get the miter of the two networks + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 ); + if ( pMiter == NULL ) + { + printf( "Miter computation has failed.\n" ); + return 0; + } + RetValue = Abc_NtkMiterIsConstant( pMiter ); + if ( RetValue == 0 ) + { + extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); + printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); + // report the error + pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames ); + Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames ); + FREE( pMiter->pModel ); + Abc_NtkDelete( pMiter ); + return 0; + } + if ( RetValue == 1 ) + { + Abc_NtkDelete( pMiter ); + printf( "Networks are equivalent after structural hashing.\n" ); + return 1; + } + + // preprocess the miter by fraiging it + // (note that for each functional class, fraiging leaves one representative; + // so fraiging does not reduce the number of functions represented by nodes + Fraig_ParamsSetDefault( &Params ); + pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 ); + Abc_NtkDelete( pTemp ); + + // derive the AIG manager + pMan = Abc_NtkToDar( pMiter, 1 ); + Abc_NtkDelete( pMiter ); + if ( pMan == NULL ) + { + printf( "Converting miter into AIG has failed.\n" ); + return -1; + } + assert( pMan->nRegs > 0 ); + + // perform verification + RetValue = Fra_FraigSec( pMan, nFrames, fVerbose, fVeryVerbose ); + Aig_ManStop( pMan ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan; + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return NULL; + pMan = Aig_ManReduceLaches( pMan, fVerbose ); + pMan = Aig_ManConstReduce( pMan, fVerbose ); + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); Aig_ManStop( pMan ); return pNtkAig; } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return NULL; + pMan = Rtm_ManRetimeFwd( pTemp = pMan, nStepsMax, fVerbose ); + Aig_ManStop( pTemp ); + +// pMan = Aig_ManReduceLaches( pMan, 1 ); +// pMan = Aig_ManConstReduce( pMan, 1 ); + + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index a33b9875..5dc63750 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -98,6 +98,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, in Abc_NtkMiterAddOne( pNtk1, pNtkMiter ); Abc_NtkMiterAddOne( pNtk2, pNtkMiter ); Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize ); + Abc_AigCleanup(pNtkMiter->pManFunc); // make sure that everything is okay if ( !Abc_NtkCheck( pNtkMiter ) ) diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index ad8eec6a..4c061637 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -322,7 +322,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ) fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n", Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] ); fprintf( pFile, "Const fanin = %3d. DC init = %3d. Matching init = %3d. ", Counter0, Counter1, Counter2 ); - fprintf( pFile, "Self-feed latches = %2d.\n", Abc_NtkCountSelfFeedLatches(pNtk) ); + fprintf( pFile, "Self-feed latches = %2d.\n", -1 ); //Abc_NtkCountSelfFeedLatches(pNtk) ); } /**Function************************************************************* diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 63ba4843..67ecaae0 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -27,7 +27,7 @@ //////////////////////////////////////////////////////////////////////// static void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel ); -static void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); +extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c index d17ab1dd..c05823da 100644 --- a/src/base/abci/abcXsim.c +++ b/src/base/abci/abcXsim.c @@ -139,7 +139,11 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) ); fprintf( stdout, " : " ); Abc_NtkForEachLatch( pNtk, pObj, i ) + { +// if ( Abc_ObjGetXsim(Abc_ObjFanout0(pObj)) != XVSX ) +// printf( " %s=", Abc_ObjName(pObj) ); Abc_XsimPrint( stdout, Abc_ObjGetXsim(Abc_ObjFanout0(pObj)) ); + } fprintf( stdout, " : " ); Abc_NtkForEachPo( pNtk, pObj, i ) Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) ); diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c index 23b5b350..be80dc82 100644 --- a/src/base/io/ioReadAiger.c +++ b/src/base/io/ioReadAiger.c @@ -121,8 +121,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) Abc_ObjAddFanin( pNode1, pObj ); Vec_PtrPush( vNodes, pNode1 ); // assign names to latch and its input - Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL ); - +// Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL ); // printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id ); } @@ -142,7 +141,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) uLit = ((i + 1 + nInputs + nLatches) << 1); uLit1 = uLit - Io_ReadAigerDecode( &pCur ); uLit0 = uLit1 - Io_ReadAigerDecode( &pCur ); - assert( uLit1 > uLit0 ); +// assert( uLit1 > uLit0 ); pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 ); pNode1 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 ); assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches ); @@ -171,66 +170,84 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); Abc_ObjAddFanin( pObj, pNode0 ); } - + // read the names if present pCur = pSymbols; - while ( pCur < pContents + nFileSize && *pCur != 'c' ) + if ( *pCur != 'c' ) { - // get the terminal type - pType = pCur; - if ( *pCur == 'i' ) - vTerms = pNtkNew->vPis; - else if ( *pCur == 'l' ) - vTerms = pNtkNew->vBoxes; - else if ( *pCur == 'o' ) - vTerms = pNtkNew->vPos; - else + int Counter = 0; + while ( pCur < pContents + nFileSize && *pCur != 'c' ) + { + // get the terminal type + pType = pCur; + if ( *pCur == 'i' ) + vTerms = pNtkNew->vPis; + else if ( *pCur == 'l' ) + vTerms = pNtkNew->vBoxes; + else if ( *pCur == 'o' ) + vTerms = pNtkNew->vPos; + else + { + fprintf( stdout, "Wrong terminal type.\n" ); + return NULL; + } + // get the terminal number + iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' ); + // get the node + if ( iTerm >= Vec_PtrSize(vTerms) ) + { + fprintf( stdout, "The number of terminal is out of bound.\n" ); + return NULL; + } + pObj = Vec_PtrEntry( vTerms, iTerm ); + if ( *pType == 'l' ) + pObj = Abc_ObjFanout0(pObj); + // assign the name + pName = pCur; while ( *pCur++ != '\n' ); + // assign this name + *(pCur-1) = 0; + Abc_ObjAssignName( pObj, pName, NULL ); + if ( *pType == 'l' ) + { + Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" ); + Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" ); + } + // mark the node as named + pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); + } + + // assign the remaining names + Abc_NtkForEachPi( pNtkNew, pObj, i ) { - fprintf( stdout, "Wrong terminal type.\n" ); - return NULL; + if ( pObj->pCopy ) continue; + Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); + Counter++; } - // get the terminal number - iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' ); - // get the node - if ( iTerm >= Vec_PtrSize(vTerms) ) + Abc_NtkForEachLatchOutput( pNtkNew, pObj, i ) { - fprintf( stdout, "The number of terminal is out of bound.\n" ); - return NULL; + if ( pObj->pCopy ) continue; + Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); + Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" ); + Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" ); + Counter++; } - pObj = Vec_PtrEntry( vTerms, iTerm ); - if ( *pType == 'l' ) - pObj = Abc_ObjFanout0(pObj); - // assign the name - pName = pCur; while ( *pCur++ != '\n' ); - // assign this name - *(pCur-1) = 0; - Abc_ObjAssignName( pObj, pName, NULL ); - if ( *pType == 'l' ) - Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "L" ); - // mark the node as named - pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); - } - // skipping the comments - free( pContents ); - Vec_PtrFree( vNodes ); - - // assign the remaining names - Abc_NtkForEachPi( pNtkNew, pObj, i ) - { - if ( pObj->pCopy ) continue; - Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); - } - Abc_NtkForEachLatchOutput( pNtkNew, pObj, i ) - { - if ( pObj->pCopy ) continue; - Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); - Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), NULL ); + Abc_NtkForEachPo( pNtkNew, pObj, i ) + { + if ( pObj->pCopy ) continue; + Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); + Counter++; + } + if ( Counter ) + printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter ); } - Abc_NtkForEachPo( pNtkNew, pObj, i ) + else { - if ( pObj->pCopy ) continue; - Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); +// printf( "Io_ReadAiger(): I/O/register names are not given. Generating short names.\n" ); + Abc_NtkShortNames( pNtkNew ); } + // skipping the comments + free( pContents ); + Vec_PtrFree( vNodes ); // remove the extra nodes Abc_AigCleanup( pNtkNew->pManFunc ); diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index 7c9da184..958e3d96 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -163,6 +163,12 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) fprintf( stdout, "Io_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName ); return; } + Abc_NtkForEachLatch( pNtk, pObj, i ) + if ( !Abc_LatchIsInit0(pObj) ) + { + fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" ); + return; + } // set the node numbers to be used in the output file nNodes = 0; diff --git a/src/opt/ret/retCore.c b/src/opt/ret/retCore.c index 551ec594..47b2cbbc 100644 --- a/src/opt/ret/retCore.c +++ b/src/opt/ret/retCore.c @@ -41,7 +41,7 @@ int timeRetime = 0; SeeAlso [] ***********************************************************************/ -int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fVerbose ) +int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fOneStep, int fVerbose ) { int nLatches = Abc_NtkLatchNum(pNtk); int nLevels = Abc_NtkLevel(pNtk); @@ -62,26 +62,26 @@ int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOn switch ( Mode ) { case 1: // forward - RetValue = Abc_NtkRetimeIncremental( pNtk, 1, 0, fVerbose ); + RetValue = Abc_NtkRetimeIncremental( pNtk, 1, 0, 0, fVerbose ); break; case 2: // backward - RetValue = Abc_NtkRetimeIncremental( pNtk, 0, 0, fVerbose ); + RetValue = Abc_NtkRetimeIncremental( pNtk, 0, 0, 0, fVerbose ); break; case 3: // min-area RetValue = Abc_NtkRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fVerbose ); break; case 4: // min-delay if ( !fBackwardOnly ) - RetValue += Abc_NtkRetimeIncremental( pNtk, 1, 1, fVerbose ); + RetValue += Abc_NtkRetimeIncremental( pNtk, 1, 1, fOneStep, fVerbose ); if ( !fForwardOnly ) - RetValue += Abc_NtkRetimeIncremental( pNtk, 0, 1, fVerbose ); + RetValue += Abc_NtkRetimeIncremental( pNtk, 0, 1, fOneStep, fVerbose ); break; case 5: // min-area + min-delay RetValue = Abc_NtkRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fVerbose ); if ( !fBackwardOnly ) - RetValue += Abc_NtkRetimeIncremental( pNtk, 1, 1, fVerbose ); + RetValue += Abc_NtkRetimeIncremental( pNtk, 1, 1, 0, fVerbose ); if ( !fForwardOnly ) - RetValue += Abc_NtkRetimeIncremental( pNtk, 0, 1, fVerbose ); + RetValue += Abc_NtkRetimeIncremental( pNtk, 0, 1, 0, fVerbose ); break; case 6: // Pan's algorithm RetValue = Abc_NtkRetimeLValue( pNtk, 500, fVerbose ); @@ -121,7 +121,7 @@ int Abc_NtkRetimeDebug( Abc_Ntk_t * pNtk ) // fprintf( stdout, "Abc_NtkRetimeDebug(): Network check has failed.\n" ); // Io_WriteBlifLogic( pNtk, "debug_temp.blif", 1 ); pNtkRet = Abc_NtkDup( pNtk ); - Abc_NtkRetime( pNtkRet, 3, 0, 1, 0 ); // debugging backward flow + Abc_NtkRetime( pNtkRet, 3, 0, 1, 0, 0 ); // debugging backward flow return !Abc_NtkSecFraig( pNtk, pNtkRet, 10000, 3, 0 ); } diff --git a/src/opt/ret/retDelay.c b/src/opt/ret/retDelay.c index 468d6187..bcfe3a2e 100644 --- a/src/opt/ret/retDelay.c +++ b/src/opt/ret/retDelay.c @@ -63,7 +63,7 @@ int Abc_NtkRetimeMinDelay( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkCopy, int nIterLimi Synopsis [Returns the best delay and the number of best iteration.] - Description [] + Description [] SideEffects [] @@ -145,7 +145,7 @@ if ( fVerbose && !fInitial ) if ( fVerbose && !fInitial ) printf( "%s : Starting delay = %3d. Final delay = %3d. IterBest = %2d (out of %2d).\n", fForward? "Forward " : "Backward", DelayStart, DelayBest, IterBest, nIterLimit ); - *pIterBest = IterBest; + *pIterBest = (nIterLimit == 1) ? 1 : IterBest; return DelayBest; } diff --git a/src/opt/ret/retIncrem.c b/src/opt/ret/retIncrem.c index 93305a8e..ba8104be 100644 --- a/src/opt/ret/retIncrem.c +++ b/src/opt/ret/retIncrem.c @@ -41,7 +41,7 @@ static int Abc_NtkRetimeOneWay( Abc_Ntk_t * pNtk, int fForward, int fVerbose ); SeeAlso [] ***********************************************************************/ -int Abc_NtkRetimeIncremental( Abc_Ntk_t * pNtk, int fForward, int fMinDelay, int fVerbose ) +int Abc_NtkRetimeIncremental( Abc_Ntk_t * pNtk, int fForward, int fMinDelay, int fOneStep, int fVerbose ) { Abc_Ntk_t * pNtkCopy = NULL; Vec_Ptr_t * vBoxes; @@ -55,7 +55,7 @@ int Abc_NtkRetimeIncremental( Abc_Ntk_t * pNtk, int fForward, int fMinDelay, int Abc_NtkOrderCisCos( pNtk ); if ( fMinDelay ) { - nIterLimit = 2 * Abc_NtkLevel(pNtk); + nIterLimit = fOneStep? 1 : 2 * Abc_NtkLevel(pNtk); pNtkCopy = Abc_NtkDup( pNtk ); tLatches = Abc_NtkRetimePrepareLatches( pNtkCopy ); st_free_table( tLatches ); diff --git a/src/opt/ret/retInt.h b/src/opt/ret/retInt.h index 28529cdc..51428bce 100644 --- a/src/opt/ret/retInt.h +++ b/src/opt/ret/retInt.h @@ -46,11 +46,11 @@ /*=== retArea.c ========================================================*/ extern int Abc_NtkRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fVerbose ); /*=== retCore.c ========================================================*/ -extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fVerbose ); +extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fOneStep, int fVerbose ); /*=== retDelay.c ========================================================*/ extern int Abc_NtkRetimeMinDelay( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkCopy, int nIterLimit, int fForward, int fVerbose ); /*=== retDirect.c ========================================================*/ -extern int Abc_NtkRetimeIncremental( Abc_Ntk_t * pNtk, int fForward, int fMinDelay, int fVerbose ); +extern int Abc_NtkRetimeIncremental( Abc_Ntk_t * pNtk, int fForward, int fMinDelay, int fOneStep, int fVerbose ); extern void Abc_NtkRetimeShareLatches( Abc_Ntk_t * pNtk, int fInitial ); extern int Abc_NtkRetimeNodeIsEnabled( Abc_Obj_t * pObj, int fForward ); extern void Abc_NtkRetimeNode( Abc_Obj_t * pObj, int fForward, int fInitial ); |