From e2e9aed11dd841801dae3cdf47db06946e7ffb28 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 22 Apr 2008 08:01:00 -0700 Subject: Version abc80422 --- src/aig/aig/aig.h | 3 + src/aig/aig/aigMan.c | 22 ++ src/aig/aig/aigObj.c | 75 ++++++ src/aig/aig/aigUtil.c | 42 +++ src/aig/cnf/cnf.h | 1 + src/aig/cnf/cnfWrite.c | 102 ++++++++ src/aig/nwk/nwkFlow.c | 28 +- src/aig/nwk/nwkFlow_depth.c | 626 ++++++++++++++++++++++++++++++++++++++++++++ src/aig/saig/saigPhase.c | 62 ++++- src/aig/saig/saigRetMin.c | 517 +++++++++++++++++++++++++----------- 10 files changed, 1313 insertions(+), 165 deletions(-) create mode 100644 src/aig/nwk/nwkFlow_depth.c (limited to 'src/aig') diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 74e3de31..47696a41 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -273,6 +273,7 @@ static inline Aig_Obj_t * Aig_ManLi( Aig_Man_t * p, int i ) { return (Aig_ static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; } static inline Aig_Type_t Aig_ObjType( Aig_Obj_t * pObj ) { return (Aig_Type_t)pObj->Type; } +static inline int Aig_ObjId( Aig_Obj_t * pObj ) { return pObj->Id; } static inline int Aig_ObjIsNone( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_NONE; } static inline int Aig_ObjIsConst1( Aig_Obj_t * pObj ) { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_OBJ_CONST1; } static inline int Aig_ObjIsPi( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_PI; } @@ -493,6 +494,7 @@ extern void Aig_ManStop( Aig_Man_t * p ); extern int Aig_ManCleanup( Aig_Man_t * p ); extern int Aig_ManPiCleanup( Aig_Man_t * p ); extern void Aig_ManPrintStats( Aig_Man_t * p ); +extern void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew ); /*=== aigMem.c ==========================================================*/ extern void Aig_ManStartMemory( Aig_Man_t * p ); extern void Aig_ManStopMemory( Aig_Man_t * p ); @@ -513,6 +515,7 @@ extern void Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj ); extern void Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fFreeTop ); extern void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew ); extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel ); +extern void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj ); /*=== aigOper.c =========================================================*/ extern Aig_Obj_t * Aig_IthVar( Aig_Man_t * p, int i ); extern Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type ); diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index ee782423..41a62484 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -337,6 +337,28 @@ void Aig_ManPrintStats( Aig_Man_t * p ) fflush( stdout ); } +/**Function************************************************************* + + Synopsis [Reports the reduction of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew ) +{ + printf( "REGs: Beg = %d. End = %d. (R = %6.2f %%). ", + Aig_ManRegNum(p), Aig_ManRegNum(pNew), + Aig_ManRegNum(p)? 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pNew))/Aig_ManRegNum(p) : 0.0 ); + printf( "ANDs: Beg = %d. End = %d. (R = %6.2f %%).", + Aig_ManNodeNum(p), Aig_ManNodeNum(pNew), + Aig_ManNodeNum(p)? 100.0*(Aig_ManNodeNum(p)-Aig_ManNodeNum(pNew))/Aig_ManNodeNum(p) : 0.0 ); + printf( "\n" ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index a66eb2b8..9c7cf2c4 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -416,6 +416,81 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in pObjOld->pHaig = pHaig; } +/**Function************************************************************* + + Synopsis [Verbose printing of the AIG node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + int fHaig = 0; + int fShowFanouts = 0; + Aig_Obj_t * pTemp; + assert( !Aig_IsComplement(pObj) ); + printf( "Node %4d : ", Aig_ObjId(pObj) ); + if ( Aig_ObjIsConst1(pObj) ) + printf( "constant 1" ); + else if ( Aig_ObjIsPi(pObj) ) + printf( "PI" ); + else if ( Aig_ObjIsPo(pObj) ) + printf( "PO( %4d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") ); + else if ( Aig_ObjIsBuf(pObj) ) + printf( "BUF( %d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") ); + else + printf( "AND( %4d%s, %4d%s )", + Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " "), + Aig_ObjFanin1(pObj)->Id, (Aig_ObjFaninC1(pObj)? "\'" : " ") ); + printf( " (refs = %3d)", Aig_ObjRefs(pObj) ); + if ( fShowFanouts && p->pFanData ) + { + Aig_Obj_t * pFanout; + int i, iFan; + printf( "\nFanouts:\n" ); + Aig_ObjForEachFanout( p, pObj, pFanout, iFan, i ) + { + printf( " " ); + printf( "Node %4d : ", Aig_ObjId(pFanout) ); + if ( Aig_ObjIsPo(pFanout) ) + printf( "PO( %4d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") ); + else if ( Aig_ObjIsBuf(pFanout) ) + printf( "BUF( %d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") ); + else + printf( "AND( %4d%s, %4d%s )", + Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " "), + Aig_ObjFanin1(pFanout)->Id, (Aig_ObjFaninC1(pFanout)? "\'" : " ") ); + printf( "\n" ); + } + return; + } + if ( fHaig ) + { + if ( pObj->pHaig == NULL ) + printf( " HAIG node not given" ); + else + printf( " HAIG node = %d%s", Aig_Regular(pObj->pHaig)->Id, (Aig_IsComplement(pObj->pHaig)? "\'" : " ") ); + return; + } + // there are choices + if ( p->pEquivs && p->pEquivs[pObj->Id] ) + { + // print equivalence class + printf( " { %4d ", pObj->Id ); + for ( pTemp = p->pEquivs[pObj->Id]; pTemp; pTemp = p->pEquivs[pTemp->Id] ) + printf( " %4d%s", pTemp->Id, (pTemp->fPhase != pObj->fPhase)? "\'" : " " ); + printf( " }" ); + return; + } + // this is a secondary node + if ( p->pReprs && p->pReprs[pObj->Id] ) + printf( " class of %d", pObj->Id ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index 7dc0c6e3..00e0311d 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -947,6 +947,48 @@ int Aig_ManCountChoices( Aig_Man_t * p ) return Counter; } +/**Function************************************************************* + + Synopsis [Prints the fanouts of the control register.] + + Description [Useful only for Intel MC benchmarks.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPrintControlFanouts( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pFanin0, * pFanin1, * pCtrl; + int i, Counter = 0; + + pCtrl = Aig_ManPi( p, Aig_ManPiNum(p) - 1 ); + + printf( "Control signal:\n" ); + Aig_ObjPrint( p, pCtrl ); printf( "\n\n" ); + + Aig_ManForEachObj( p, pObj, i ) + { + if ( !Aig_ObjIsNode(pObj) ) + continue; + assert( pObj != pCtrl ); + pFanin0 = Aig_ObjFanin0(pObj); + pFanin1 = Aig_ObjFanin1(pObj); + if ( pFanin0 == pCtrl && Aig_ObjIsPi(pFanin1) ) + { + Aig_ObjPrint( p, pObj ); printf( "\n" ); + Aig_ObjPrint( p, pFanin1 ); printf( "\n" ); + printf( "\n" ); + } + if ( pFanin1 == pCtrl && Aig_ObjIsPi(pFanin0) ) + { + Aig_ObjPrint( p, pObj ); printf( "\n" ); + Aig_ObjPrint( p, pFanin0 ); printf( "\n" ); + printf( "\n" ); + } + } +} //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index ddb2dafe..cf763e67 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -152,6 +152,7 @@ extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPre extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover ); extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ); extern Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ); +extern Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p ); #ifdef __cplusplus } diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c index 5a96f23f..23b3e8f0 100644 --- a/src/aig/cnf/cnfWrite.c +++ b/src/aig/cnf/cnfWrite.c @@ -440,6 +440,108 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ) return pCnf; } +/**Function************************************************************* + + Synopsis [Derives a simple CNF for backward retiming computation.] + + Description [The last argument shows the number of last outputs + of the manager, which will not be converted into clauses. + New variables will be introduced for these outputs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + Cnf_Dat_t * pCnf; + int OutVar, PoVar, pVars[32], * pLits, ** pClas; + int i, nLiterals, nClauses, Number; + + // count the number of literals and clauses + nLiterals = 1 + 7 * Aig_ManNodeNum(p) + 5 * Aig_ManPoNum(p); + nClauses = 1 + 3 * Aig_ManNodeNum(p) + 3 * Aig_ManPoNum(p); + + // allocate CNF + pCnf = ALLOC( Cnf_Dat_t, 1 ); + memset( pCnf, 0, sizeof(Cnf_Dat_t) ); + pCnf->pMan = p; + pCnf->nLiterals = nLiterals; + pCnf->nClauses = nClauses; + pCnf->pClauses = ALLOC( int *, nClauses + 1 ); + pCnf->pClauses[0] = ALLOC( int, nLiterals ); + pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; + + // create room for variable numbers + pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p) ); + memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) ); + // assign variables to the last (nOutputs) POs + Number = 1; + Aig_ManForEachPo( p, pObj, i ) + pCnf->pVarNums[pObj->Id] = Number++; + // assign variables to the internal nodes + Aig_ManForEachNode( p, pObj, i ) + pCnf->pVarNums[pObj->Id] = Number++; + // assign variables to the PIs and constant node + Aig_ManForEachPi( p, pObj, i ) + pCnf->pVarNums[pObj->Id] = Number++; + pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++; + pCnf->nVars = Number; + // assign the clauses + pLits = pCnf->pClauses[0]; + pClas = pCnf->pClauses; + Aig_ManForEachNode( p, pObj, i ) + { + OutVar = pCnf->pVarNums[ pObj->Id ]; + pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; + pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ]; + + // positive phase + *pClas++ = pLits; + *pLits++ = 2 * OutVar; + *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); + *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); + // negative phase + *pClas++ = pLits; + *pLits++ = 2 * OutVar + 1; + *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); + *pClas++ = pLits; + *pLits++ = 2 * OutVar + 1; + *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); + } + + // write the constant literal + OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ]; + assert( OutVar <= Aig_ManObjNumMax(p) ); + *pClas++ = pLits; + *pLits++ = 2 * OutVar; + + // write the output literals + Aig_ManForEachPo( p, pObj, i ) + { + OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; + PoVar = pCnf->pVarNums[ pObj->Id ]; + // first clause + *pClas++ = pLits; + *pLits++ = 2 * PoVar; + *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); + // second clause + *pClas++ = pLits; + *pLits++ = 2 * PoVar + 1; + *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); + // final clause (init-state is always 0 -> set the output to 0) + *pClas++ = pLits; + *pLits++ = 2 * PoVar + 1; + } + + // verify that the correct number of literals and clauses was written + assert( pLits - pCnf->pClauses[0] == nLiterals ); + assert( pClas - pCnf->pClauses == nClauses ); + return pCnf; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/nwk/nwkFlow.c b/src/aig/nwk/nwkFlow.c index 3a7e6df6..48496158 100644 --- a/src/aig/nwk/nwkFlow.c +++ b/src/aig/nwk/nwkFlow.c @@ -20,6 +20,14 @@ #include "nwk.h" +/* + This code is based on the papers: + A. Hurst, A. Mishchenko, and R. Brayton, "Fast minimum-register retiming + via binary maximum-flow", Proc. FMCAD '07, pp. 181-187. + A. Hurst, A. Mishchenko, and R. Brayton, "Scalable min-area retiming + under simultaneous delay and initial state constraints". Proc. DAC'08. +*/ + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -368,7 +376,7 @@ int Nwk_ManVerifyCut_rec( Nwk_Obj_t * pObj ) return 0; return 1; } - + /**Function************************************************************* Synopsis [Verifies the forward cut.] @@ -453,7 +461,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos Counter++; } if ( fVerbose ) - printf( "Forward: Max-flow1 = %5d. ", Counter ); + printf( "Forward: Max-flow = %4d -> ", Counter ); // continue flow computation from each LO Nwk_ManIncrementTravIdFlow( pMan ); Nwk_ManForEachLoSeq( pMan, pObj, i ) @@ -464,7 +472,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos Counter2++; } if ( fVerbose ) - printf( "Max-flow2 = %5d. ", Counter+Counter2 ); + printf( "%4d. ", Counter+Counter2 ); // repeat flow computation from each LO if ( Counter2 > 0 ) { @@ -489,10 +497,10 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos } } Nwk_ManCleanMarks( pMan ); - assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) ); +// assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) ); if ( fVerbose ) { - printf( "Min-cut = %5d. Unmoved regs = %5d. ", Vec_PtrSize(vNodes), Counter ); + printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter ); PRT( "Time", clock() - clk ); } return vNodes; @@ -536,8 +544,8 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo Nwk_ManIncrementTravIdFlow( pMan ); Counter++; } - if ( fVerbose ) - printf( "Backward: Max-flow1 = %5d. ", Counter ); + if ( fVerbose ) + printf( "Backward: Max-flow = %4d -> ", Counter ); // continue flow computation from each LI driver Nwk_ManIncrementTravIdFlow( pMan ); Nwk_ManForEachLiSeq( pMan, pObj, i ) @@ -548,7 +556,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo Counter2++; } if ( fVerbose ) - printf( "Max-flow2 = %5d. ", Counter+Counter2 ); + printf( "%4d. ", Counter+Counter2 ); // repeat flow computation from each LI driver if ( Counter2 > 0 ) { @@ -576,10 +584,10 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo if ( Nwk_ObjVisitedBotOnly( Nwk_ObjFanin0(pObj) ) ) Counter++; Nwk_ManCleanMarks( pMan ); - assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) ); +// assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) ); if ( fVerbose ) { - printf( "Min-cut = %5d. Unmoved regs = %5d. ", Vec_PtrSize(vNodes), Counter ); + printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter ); PRT( "Time", clock() - clk ); } return vNodes; diff --git a/src/aig/nwk/nwkFlow_depth.c b/src/aig/nwk/nwkFlow_depth.c new file mode 100644 index 00000000..a457631c --- /dev/null +++ b/src/aig/nwk/nwkFlow_depth.c @@ -0,0 +1,626 @@ +/**CFile**************************************************************** + + FileName [nwkFlow.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [Max-flow/min-cut computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: nwkFlow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "nwk.h" + +/* + This code is based on the papers: + A. Hurst, A. Mishchenko, and R. Brayton, "Fast minimum-register retiming + via binary maximum-flow", Proc. FMCAD '07, pp. 181-187. + A. Hurst, A. Mishchenko, and R. Brayton, "Scalable min-area retiming + under simultaneous delay and initial state constraints". Proc. DAC'08. +*/ + +int DepthFwd, DepthBwd, DepthFwdMax, DepthBwdMax; + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// predecessors +static inline Nwk_Obj_t * Nwk_ObjPred( Nwk_Obj_t * pObj ) { return pObj->pCopy; } +static inline int Nwk_ObjSetPred( Nwk_Obj_t * pObj, Nwk_Obj_t * p ) { pObj->pCopy = p; return 1; } +// sink +static inline int Nwk_ObjIsSink( Nwk_Obj_t * pObj ) { return pObj->MarkA; } +static inline void Nwk_ObjSetSink( Nwk_Obj_t * pObj ) { pObj->MarkA = 1; } +// flow +static inline int Nwk_ObjHasFlow( Nwk_Obj_t * pObj ) { return pObj->MarkB; } +static inline void Nwk_ObjSetFlow( Nwk_Obj_t * pObj ) { pObj->MarkB = 1; } +static inline void Nwk_ObjClearFlow( Nwk_Obj_t * pObj ) { pObj->MarkB = 0; } + +// representation of visited nodes +// pObj->TravId < pNtk->nTravIds-2 --- not visited +// pObj->TravId == pNtk->nTravIds-2 --- visited bot only +// pObj->TravId == pNtk->nTravIds-1 --- visited top only +// pObj->TravId == pNtk->nTravIds --- visited bot and top +static inline int Nwk_ObjVisitedBotOnly( Nwk_Obj_t * pObj ) +{ + return pObj->TravId == pObj->pMan->nTravIds - 2; +} +static inline int Nwk_ObjVisitedBot( Nwk_Obj_t * pObj ) +{ + return pObj->TravId == pObj->pMan->nTravIds - 2 || pObj->TravId == pObj->pMan->nTravIds; +} +static inline int Nwk_ObjVisitedTop( Nwk_Obj_t * pObj ) +{ + return pObj->TravId == pObj->pMan->nTravIds - 1 || pObj->TravId == pObj->pMan->nTravIds; +} +static inline void Nwk_ObjSetVisitedBot( Nwk_Obj_t * pObj ) +{ + if ( pObj->TravId < pObj->pMan->nTravIds - 2 ) + pObj->TravId = pObj->pMan->nTravIds - 2; + else if ( pObj->TravId == pObj->pMan->nTravIds - 1 ) + pObj->TravId = pObj->pMan->nTravIds; + else + assert( 0 ); +} +static inline void Nwk_ObjSetVisitedTop( Nwk_Obj_t * pObj ) +{ + if ( pObj->TravId < pObj->pMan->nTravIds - 2 ) + pObj->TravId = pObj->pMan->nTravIds - 1; + else if ( pObj->TravId == pObj->pMan->nTravIds - 2 ) + pObj->TravId = pObj->pMan->nTravIds; + else + assert( 0 ); +} +static inline Nwk_ManIncrementTravIdFlow( Nwk_Man_t * pMan ) +{ + Nwk_ManIncrementTravId( pMan ); + Nwk_ManIncrementTravId( pMan ); + Nwk_ManIncrementTravId( pMan ); +} + +static int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred ); +static int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred ); + +static int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred ); +static int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Marks TFI of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManMarkTfiCone_rec( Nwk_Obj_t * pObj ) +{ + Nwk_Obj_t * pNext; + int i; + if ( pObj->MarkA ) + return; + pObj->MarkA = 1; + Nwk_ObjForEachFanin( pObj, pNext, i ) + Nwk_ManMarkTfiCone_rec( pNext ); +} + +/**Function************************************************************* + + Synopsis [Marks TFO of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManMarkTfoCone_rec( Nwk_Obj_t * pObj ) +{ + Nwk_Obj_t * pNext; + int i; + if ( pObj->MarkA ) + return; + pObj->MarkA = 1; + Nwk_ObjForEachFanout( pObj, pNext, i ) + Nwk_ManMarkTfoCone_rec( pNext ); +} + +/**Function************************************************************* + + Synopsis [Fast forward flow pushing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManPushForwardFast_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred ) +{ + Nwk_Obj_t * pNext; + int i; + if ( Nwk_ObjIsTravIdCurrent( pObj ) ) + return 0; + Nwk_ObjSetTravIdCurrent( pObj ); + if ( Nwk_ObjHasFlow(pObj) ) + return 0; + if ( Nwk_ObjIsSink(pObj) ) + { + Nwk_ObjSetFlow(pObj); + return Nwk_ObjSetPred( pObj, pPred ); + } + Nwk_ObjForEachFanout( pObj, pNext, i ) + if ( Nwk_ManPushForwardFast_rec( pNext, pObj ) ) + { + Nwk_ObjSetFlow(pObj); + return Nwk_ObjSetPred( pObj, pPred ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Fast backward flow pushing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManPushBackwardFast_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred ) +{ + Nwk_Obj_t * pNext; + int i; + if ( Nwk_ObjIsTravIdCurrent( pObj ) ) + return 0; + Nwk_ObjSetTravIdCurrent( pObj ); + if ( Nwk_ObjHasFlow(pObj) ) + return 0; + if ( Nwk_ObjIsSink(pObj) ) + { + Nwk_ObjSetFlow(pObj); + return Nwk_ObjSetPred( pObj, pPred ); + } + Nwk_ObjForEachFanin( pObj, pNext, i ) + if ( Nwk_ManPushBackwardFast_rec( pNext, pObj ) ) + { + Nwk_ObjSetFlow(pObj); + return Nwk_ObjSetPred( pObj, pPred ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Pushing the flow through the bottom part of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred ) +{ + Nwk_Obj_t * pNext; + int i; + if ( Nwk_ObjVisitedBot(pObj) ) + return 0; + Nwk_ObjSetVisitedBot(pObj); + DepthFwd++; + if ( DepthFwdMax < DepthFwd ) + DepthFwdMax = DepthFwd; + // propagate through the internal edge + if ( Nwk_ObjHasFlow(pObj) ) + { + if ( Nwk_ObjPred(pObj) ) + if ( Nwk_ManPushForwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) ) + { + DepthFwd--; + return Nwk_ObjSetPred( pObj, pPred ); + } + } + else if ( Nwk_ManPushForwardTop_rec(pObj, pObj) ) + { + DepthFwd--; + Nwk_ObjSetFlow( pObj ); + return Nwk_ObjSetPred( pObj, pPred ); + } + // try to push through the fanins + Nwk_ObjForEachFanin( pObj, pNext, i ) + if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) ) + { + DepthFwd--; + return 1; + } + DepthFwd--; + return 0; +} + +/**Function************************************************************* + + Synopsis [Pushing the flow through the top part of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred ) +{ + Nwk_Obj_t * pNext; + int i; + if ( Nwk_ObjVisitedTop(pObj) ) + return 0; + Nwk_ObjSetVisitedTop(pObj); + // check if this is the sink + if ( Nwk_ObjIsSink(pObj) ) + return 1; + DepthFwd++; + if ( DepthFwdMax < DepthFwd ) + DepthFwdMax = DepthFwd; + // try to push through the fanouts + Nwk_ObjForEachFanout( pObj, pNext, i ) + if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) ) + { + DepthFwd--; + return 1; + } + // redirect the flow + if ( Nwk_ObjHasFlow(pObj) && !Nwk_ObjIsCi(pObj) ) + if ( Nwk_ManPushForwardBot_rec( pObj, Nwk_ObjPred(pObj) ) ) + { + DepthFwd--; + Nwk_ObjClearFlow( pObj ); + return Nwk_ObjSetPred( pObj, NULL ); + } + DepthFwd--; + return 0; +} + +/**Function************************************************************* + + Synopsis [Pushing the flow through the bottom part of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred ) +{ + if ( Nwk_ObjVisitedBot(pObj) ) + return 0; + Nwk_ObjSetVisitedBot(pObj); + // propagate through the internal edge + if ( Nwk_ObjHasFlow(pObj) ) + { + if ( Nwk_ObjPred(pObj) ) + if ( Nwk_ManPushBackwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) ) + return Nwk_ObjSetPred( pObj, pPred ); + } + else if ( Nwk_ManPushBackwardTop_rec(pObj, pObj) ) + { + Nwk_ObjSetFlow( pObj ); + return Nwk_ObjSetPred( pObj, pPred ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Pushing the flow through the top part of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred ) +{ + Nwk_Obj_t * pNext; + int i; + if ( Nwk_ObjVisitedTop(pObj) ) + return 0; + Nwk_ObjSetVisitedTop(pObj); + // check if this is the sink + if ( Nwk_ObjIsSink(pObj) ) + return 1; + // try to push through the fanins + Nwk_ObjForEachFanin( pObj, pNext, i ) + if ( Nwk_ManPushBackwardBot_rec( pNext, pPred ) ) + return 1; + // try to push through the fanouts + Nwk_ObjForEachFanout( pObj, pNext, i ) + if ( !Nwk_ObjIsCo(pObj) && Nwk_ManPushBackwardTop_rec( pNext, pPred ) ) + return 1; + // redirect the flow + if ( Nwk_ObjHasFlow(pObj) ) + if ( Nwk_ObjPred(pObj) && Nwk_ManPushBackwardBot_rec( pObj, Nwk_ObjPred(pObj) ) ) + { + Nwk_ObjClearFlow( pObj ); + return Nwk_ObjSetPred( pObj, NULL ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Returns 0 if there is an unmarked path to a CI.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManVerifyCut_rec( Nwk_Obj_t * pObj ) +{ + Nwk_Obj_t * pNext; + int i; + if ( pObj->MarkA ) + return 1; + if ( Nwk_ObjIsLo(pObj) ) + return 0; + if ( Nwk_ObjIsTravIdCurrent( pObj ) ) + return 1; + Nwk_ObjSetTravIdCurrent( pObj ); + Nwk_ObjForEachFanin( pObj, pNext, i ) + if ( !Nwk_ManVerifyCut_rec( pNext ) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Verifies the forward cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManRetimeVerifyCutForward( Nwk_Man_t * pMan, Vec_Ptr_t * vNodes ) +{ + Nwk_Obj_t * pObj; + int i; + // mark the nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + assert( pObj->MarkA == 0 ); + pObj->MarkA = 1; + } + // traverse from the COs + Nwk_ManIncrementTravId( pMan ); + Nwk_ManForEachCo( pMan, pObj, i ) + if ( !Nwk_ManVerifyCut_rec( pObj ) ) + printf( "Nwk_ManRetimeVerifyCutForward(): Internal cut verification failed.\n" ); + // unmark the nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->MarkA = 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Verifies the forward cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManRetimeVerifyCutBackward( Nwk_Man_t * pMan, Vec_Ptr_t * vNodes ) +{ + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes minimum cut for forward retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose ) +{ + Vec_Ptr_t * vNodes; + Nwk_Obj_t * pObj; + int i, RetValue, Counter = 0, Counter2 = 0; + int clk = clock(); + // set the sequential parameters + pMan->nLatches = nLatches; + pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches; + pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches; + // mark the COs and the TFO of PIs + Nwk_ManForEachCo( pMan, pObj, i ) + pObj->MarkA = 1; + Nwk_ManForEachPiSeq( pMan, pObj, i ) + Nwk_ManMarkTfoCone_rec( pObj ); + // start flow computation from each LO + Nwk_ManIncrementTravIdFlow( pMan ); + Nwk_ManForEachLoSeq( pMan, pObj, i ) + { + if ( !Nwk_ManPushForwardFast_rec( pObj, NULL ) ) + continue; + Nwk_ManIncrementTravIdFlow( pMan ); + Counter++; + } + if ( fVerbose ) + printf( "Forward: Max-flow = %4d -> ", Counter ); + // continue flow computation from each LO + DepthFwdMax = DepthFwd = 0; + Nwk_ManIncrementTravIdFlow( pMan ); + Nwk_ManForEachLoSeq( pMan, pObj, i ) + { + printf( "%d ", DepthFwdMax ); + if ( !Nwk_ManPushForwardBot_rec( pObj, NULL ) ) + continue; + assert( DepthFwd == 0 ); + Nwk_ManIncrementTravIdFlow( pMan ); + Counter2++; + } + printf( "DepthMax = %d.\n", DepthFwdMax ); + if ( fVerbose ) + printf( "%4d. ", Counter+Counter2 ); + // repeat flow computation from each LO + if ( Counter2 > 0 ) + { + Nwk_ManIncrementTravIdFlow( pMan ); + Nwk_ManForEachLoSeq( pMan, pObj, i ) + { + RetValue = Nwk_ManPushForwardBot_rec( pObj, NULL ); + assert( !RetValue ); + } + } + // cut is a set of nodes whose bottom is visited but top is not visited + vNodes = Vec_PtrAlloc( Counter+Counter2 ); + Counter = 0; + Nwk_ManForEachObj( pMan, pObj, i ) + { + if ( Nwk_ObjVisitedBotOnly(pObj) ) + { + assert( Nwk_ObjHasFlow(pObj) ); + assert( !Nwk_ObjIsCo(pObj) ); + Vec_PtrPush( vNodes, pObj ); + Counter += Nwk_ObjIsCi(pObj); + } + } + Nwk_ManCleanMarks( pMan ); + assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) ); + if ( fVerbose ) + { + printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter ); + PRT( "Time", clock() - clk ); + } + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Computes minimum cut for backward retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose ) +{ + Vec_Ptr_t * vNodes; + Nwk_Obj_t * pObj; + int i, RetValue, Counter = 0, Counter2 = 0; + int clk = clock(); + // set the sequential parameters + pMan->nLatches = nLatches; + pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches; + pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches; + // mark the CIs, the TFI of POs, and the constant nodes + Nwk_ManForEachCi( pMan, pObj, i ) + pObj->MarkA = 1; + Nwk_ManForEachPoSeq( pMan, pObj, i ) + Nwk_ManMarkTfiCone_rec( pObj ); + Nwk_ManForEachNode( pMan, pObj, i ) + if ( Nwk_ObjFaninNum(pObj) == 0 ) + pObj->MarkA = 1; + // start flow computation from each LI driver + Nwk_ManIncrementTravIdFlow( pMan ); + Nwk_ManForEachLiSeq( pMan, pObj, i ) + { + if ( !Nwk_ManPushBackwardFast_rec( Nwk_ObjFanin0(pObj), NULL ) ) + continue; + Nwk_ManIncrementTravIdFlow( pMan ); + Counter++; + } + if ( fVerbose ) + printf( "Backward: Max-flow = %4d -> ", Counter ); + // continue flow computation from each LI driver + Nwk_ManIncrementTravIdFlow( pMan ); + Nwk_ManForEachLiSeq( pMan, pObj, i ) + { + if ( !Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL ) ) + continue; + Nwk_ManIncrementTravIdFlow( pMan ); + Counter2++; + } + if ( fVerbose ) + printf( "%4d. ", Counter+Counter2 ); + // repeat flow computation from each LI driver + if ( Counter2 > 0 ) + { + Nwk_ManIncrementTravIdFlow( pMan ); + Nwk_ManForEachLiSeq( pMan, pObj, i ) + { + RetValue = Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL ); + assert( !RetValue ); + } + } + // cut is a set of nodes whose bottom is visited but top is not visited + vNodes = Vec_PtrAlloc( Counter+Counter2 ); + Nwk_ManForEachObj( pMan, pObj, i ) + { + if ( Nwk_ObjVisitedBotOnly(pObj) ) + { + assert( Nwk_ObjHasFlow(pObj) ); + assert( !Nwk_ObjIsCo(pObj) ); + Vec_PtrPush( vNodes, pObj ); + } + } + // count CO drivers + Counter = 0; + Nwk_ManForEachLiSeq( pMan, pObj, i ) + if ( Nwk_ObjVisitedBotOnly( Nwk_ObjFanin0(pObj) ) ) + Counter++; + Nwk_ManCleanMarks( pMan ); + assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) ); + if ( fVerbose ) + { + printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter ); + PRT( "Time", clock() - clk ); + } + return vNodes; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c index f83666c4..fc00ce3c 100644 --- a/src/aig/saig/saigPhase.c +++ b/src/aig/saig/saigPhase.c @@ -272,7 +272,7 @@ void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix ) else continue; // print trace - printf( "%5d : %5d ", Counter, i ); + printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id ); Vec_PtrForEachEntryStop( p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 ) { Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); @@ -534,6 +534,60 @@ Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits ) return NULL; } +/**Function************************************************************* + + Synopsis [Analize initial value of the selected register.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManAnalizeControl( Aig_Man_t * p, int Reg ) +{ + Aig_Obj_t * pObj, * pReg, * pCtrl, * pAnd; + int i; + pReg = Saig_ManLo( p, Reg ); + pCtrl = Saig_ManLo( p, Saig_ManRegNum(p)-1 ); + assert( pReg->Id < pCtrl->Id ); + // find a node pointing to both + pAnd = NULL; + Aig_ManForEachNode( p, pObj, i ) + { + if ( Aig_ObjFanin0(pObj) == pReg && Aig_ObjFanin1(pObj) == pCtrl ) + { + pAnd = pObj; + break; + } + } + if ( pAnd == NULL ) + { + printf( "Register is not found.\n" ); + return; + } + printf( "Clock-like register: \n" ); + Aig_ObjPrint( p, pReg ); + printf( "\n" ); + printf( "Control register: \n" ); + Aig_ObjPrint( p, pCtrl ); + printf( "\n" ); + printf( "Their fanout: \n" ); + Aig_ObjPrint( p, pAnd ); + printf( "\n" ); + + // find the fanouts of pAnd + printf( "Fanouts of the fanout: \n" ); + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjFanin0(pObj) == pAnd || Aig_ObjFanin1(pObj) == pAnd ) + { + Aig_ObjPrint( p, pObj ); + printf( "\n" ); + } + printf( "\n" ); +} + /**Function************************************************************* Synopsis [Finds the registers to phase-abstract.] @@ -587,6 +641,9 @@ int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVe for ( k = 0; k < nFrames; k++ ) Saig_XsimPrint( stdout, Values[k] ); printf( "]\n" ); + + if ( fVerbose ) + Saig_ManAnalizeControl( pTsi->pAig, Reg ); } } Vec_IntShrink( pTsi->vNonXRegs, r ); @@ -595,6 +652,7 @@ int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVe return Vec_IntSize(pTsi->vNonXRegs); } + /**Function************************************************************* Synopsis [Mapping of AIG nodes into frames nodes.] @@ -662,7 +720,7 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe pState = Vec_PtrEntry( pTsi->vStates, f ); Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg ); assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 ); - pObjNew = Value? Aig_ManConst1(pFrames) : Aig_ManConst0(pFrames); + pObjNew = (Value == SAIG_XVS1)? Aig_ManConst1(pFrames) : Aig_ManConst0(pFrames); Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew ); } // add internal nodes of this frame diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c index 3adb76c6..c53d6d6b 100644 --- a/src/aig/saig/saigRetMin.c +++ b/src/aig/saig/saigRetMin.c @@ -19,8 +19,10 @@ ***********************************************************************/ #include "saig.h" -#include "satSolver.h" + #include "cnf.h" +#include "satSolver.h" +#include "satStore.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -34,7 +36,7 @@ extern Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fV /**Function************************************************************* - Synopsis [Marks the TFI cone with the current traversal ID.] + Synopsis [Derives the initial state after backward retiming.] Description [] @@ -43,66 +45,161 @@ extern Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fV SeeAlso [] ***********************************************************************/ -void Saig_ManMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +Vec_Int_t * Saig_ManRetimeInitState( Aig_Man_t * p ) { - if ( pObj == NULL ) - return; - if ( Aig_ObjIsTravIdCurrent( p, pObj ) ) - return; - Aig_ObjSetTravIdCurrent( p, pObj ); - Saig_ManMarkCone_rec( p, Aig_ObjFanin0(pObj) ); - Saig_ManMarkCone_rec( p, Aig_ObjFanin1(pObj) ); + int nConfLimit = 1000000; + Vec_Int_t * vCiIds, * vInit = NULL; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + Aig_Obj_t * pObj; + int i, RetValue, * pModel; + // solve the SAT problem + pCnf = Cnf_DeriveSimpleForRetiming( p ); + pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( pSat == NULL ) + { + Cnf_DataFree( pCnf ); + return NULL; + } + RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + assert( RetValue != l_Undef ); + // create counter-example + if ( RetValue == l_True ) + { + // accumulate SAT variables of the CIs + vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPi( p, pObj, i ) + Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] ); + // create the model + pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); + vInit = Vec_IntAllocArray( pModel, Aig_ManPiNum(p) ); + Vec_IntFree( vCiIds ); + } + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return vInit; } /**Function************************************************************* - Synopsis [Counts the number of nodes to get registers after retiming.] + Synopsis [Uses UNSAT core to find the part of AIG to be excluded.] - Description [] + Description [Returns the number of the PO that appears in the UNSAT core.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut ) +int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose ) { - Vec_Ptr_t * vNodes; - Aig_Obj_t * pObj, * pFanin; - int i, RetValue; - // mark the cones - Aig_ManIncrementTravId( p ); - Vec_PtrForEachEntry( vCut, pObj, i ) - Saig_ManMarkCone_rec( p, pObj ); - // collect the new cut - vNodes = Vec_PtrAlloc( 1000 ); - Aig_ManForEachObj( p, pObj, i ) + int fVeryVerbose = 0; + int nConfLimit = 1000000; + void * pSatCnf = NULL; + Intp_Man_t * pManProof; + Vec_Int_t * vCore = NULL; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + Aig_Obj_t * pObj; + int * pClause1, * pClause2, * pLit, * pVars; + int i, RetValue, iBadPo, iClause, nVars, nPos; + // create the SAT solver + pCnf = Cnf_DeriveSimpleForRetiming( p ); + pSat = sat_solver_new(); + sat_solver_store_alloc( pSat ); + sat_solver_setnvars( pSat, pCnf->nVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) { - if ( Aig_ObjIsTravIdCurrent(p, pObj) ) - continue; - pFanin = Aig_ObjFanin0( pObj ); - if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) ) + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) { - Vec_PtrPush( vNodes, pFanin ); - pFanin->fMarkA = 1; + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + return -1; } - pFanin = Aig_ObjFanin1( pObj ); - if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) ) + } + sat_solver_store_mark_roots( pSat ); + // solve the problem + RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + assert( RetValue != l_Undef ); + assert( RetValue == l_False ); + pSatCnf = sat_solver_store_release( pSat ); + sat_solver_delete( pSat ); + // derive the UNSAT core + pManProof = Intp_ManAlloc(); + vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVeryVerbose ); + Intp_ManFree( pManProof ); + Sto_ManFree( pSatCnf ); + // derive the set of variables on which the core depends + // collect the variable numbers + nVars = 0; + pVars = ALLOC( int, pCnf->nVars ); + memset( pVars, 0, sizeof(int) * pCnf->nVars ); + Vec_IntForEachEntry( vCore, iClause, i ) + { + pClause1 = pCnf->pClauses[iClause]; + pClause2 = pCnf->pClauses[iClause+1]; + for ( pLit = pClause1; pLit < pClause2; pLit++ ) { - Vec_PtrPush( vNodes, pFanin ); - pFanin->fMarkA = 1; + if ( pVars[ (*pLit) >> 1 ] == 0 ) + nVars++; + pVars[ (*pLit) >> 1 ] = 1; + if ( fVeryVerbose ) + printf( "%s%d ", ((*pLit) & 1)? "-" : "+", (*pLit) >> 1 ); } + if ( fVeryVerbose ) + printf( "\n" ); } - Vec_PtrForEachEntry( vNodes, pObj, i ) - pObj->fMarkA = 0; - RetValue = Vec_PtrSize( vNodes ); - Vec_PtrFree( vNodes ); - return RetValue; + // collect the nodes + if ( fVeryVerbose ) + Aig_ManForEachObj( p, pObj, i ) + if ( pCnf->pVarNums[pObj->Id] >= 0 && pVars[ pCnf->pVarNums[pObj->Id] ] == 1 ) + { + Aig_ObjPrint( p, pObj ); + printf( "\n" ); + } + // pick the first PO in the list + nPos = 0; + iBadPo = -1; + Aig_ManForEachPo( p, pObj, i ) + if ( pCnf->pVarNums[pObj->Id] >= 0 && pVars[ pCnf->pVarNums[pObj->Id] ] == 1 ) + { + if ( iBadPo == -1 ) + iBadPo = i; + nPos++; + } + if ( fVerbose ) + printf( "UNSAT core: %d clauses, %d variables, %d POs. ", Vec_IntSize(vCore), nVars, nPos ); + free( pVars ); + Vec_IntFree( vCore ); + Cnf_DataFree( pCnf ); + return iBadPo; +} + +/**Function************************************************************* + + Synopsis [Marks the TFI cone with the current traversal ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( pObj == NULL ) + return; + if ( Aig_ObjIsTravIdCurrent( p, pObj ) ) + return; + Aig_ObjSetTravIdCurrent( p, pObj ); + Saig_ManMarkCone_rec( p, Aig_ObjFanin0(pObj) ); + Saig_ManMarkCone_rec( p, Aig_ObjFanin1(pObj) ); } /**Function************************************************************* - Synopsis [Computes the new cut after excluding the nodes in the set.] + Synopsis [Counts the number of nodes to get registers after retiming.] Description [] @@ -111,17 +208,15 @@ int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Saig_ManRetimeExtendCut( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Ptr_t * vToExclude ) +int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut ) { Vec_Ptr_t * vNodes; Aig_Obj_t * pObj, * pFanin; - int i; + int i, RetValue; // mark the cones Aig_ManIncrementTravId( p ); Vec_PtrForEachEntry( vCut, pObj, i ) Saig_ManMarkCone_rec( p, pObj ); - Vec_PtrForEachEntry( vToExclude, pObj, i ) - Saig_ManMarkCone_rec( p, pObj ); // collect the new cut vNodes = Vec_PtrAlloc( 1000 ); Aig_ManForEachObj( p, pObj, i ) @@ -143,7 +238,9 @@ Vec_Ptr_t * Saig_ManRetimeExtendCut( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Ptr_t } Vec_PtrForEachEntry( vNodes, pObj, i ) pObj->fMarkA = 0; - return vNodes; + RetValue = Vec_PtrSize( vNodes ); + Vec_PtrFree( vNodes ); + return RetValue; } /**Function************************************************************* @@ -222,12 +319,13 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut ) Saig_ManRetimeDup_rec( pNew, pObj ); Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, pObj->fPhase) ); } + Aig_ManCleanup( pNew ); return pNew; } /**Function************************************************************* - Synopsis [Derives AIG for the initial state computation.] + Synopsis [Duplicates the AIG while retiming the registers to the cut.] Description [] @@ -236,33 +334,64 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManRetimeDupInitState( Aig_Man_t * p, Vec_Ptr_t * vCut ) +Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Int_t * vInit ) { Aig_Man_t * pNew; - Aig_Obj_t * pObj; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i; // mark the cones under the cut // assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) ); // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + pNew->nRegs = Vec_PtrSize(vCut); + pNew->nTruePis = p->nTruePis; + pNew->nTruePos = p->nTruePos; // create the true PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Saig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); // create the registers Vec_PtrForEachEntry( vCut, pObj, i ) - pObj->pData = Aig_ObjCreatePi(pNew); - // duplicate logic above the cut and create POs + pObj->pData = Aig_NotCond( Aig_ObjCreatePi(pNew), vInit?Vec_IntEntry(vInit,i):0 ); + // duplicate logic above the cut and remember values Saig_ManForEachLi( p, pObj, i ) + { + Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) ); + pObj->pData = Aig_ObjChild0Copy(pObj); + } + // transfer values from the LIs to the LOs + Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; + // erase the data values on the internal nodes of the cut + Vec_PtrForEachEntry( vCut, pObj, i ) + if ( Aig_ObjIsNode(pObj) ) + pObj->pData = NULL; + // replicate the data on the constant node and the PIs + pObj = Aig_ManConst1(p); + pObj->pData = Aig_ManConst1(pNew); + Saig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ManPi( pNew, i ); + // duplicate logic below the cut + Saig_ManForEachPo( p, pObj, i ) { Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) ); Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); } + Vec_PtrForEachEntry( vCut, pObj, i ) + { + Saig_ManRetimeDup_rec( pNew, pObj ); + Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, vInit?Vec_IntEntry(vInit,i):0) ); + } + Aig_ManCleanup( pNew ); return pNew; } /**Function************************************************************* - Synopsis [Derives the initial state after backward retiming.] + Synopsis [Derives AIG for the initial state computation.] Description [] @@ -271,36 +400,28 @@ Aig_Man_t * Saig_ManRetimeDupInitState( Aig_Man_t * p, Vec_Ptr_t * vCut ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManRetimeFindInitState( Aig_Man_t * p ) +Aig_Man_t * Saig_ManRetimeDupInitState( Aig_Man_t * p, Vec_Ptr_t * vCut ) { - int nConfLimit = 1000000; - Vec_Int_t * vCiIds, * vInit = NULL; - Cnf_Dat_t * pCnf; - sat_solver * pSat; + Aig_Man_t * pNew; Aig_Obj_t * pObj; - int i, RetValue, * pAssumps, * pModel; - // solve the SAT problem - pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) ); - pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - pAssumps = ALLOC( int, Aig_ManPoNum(p) ); - Aig_ManForEachPo( p, pObj, i ) - pAssumps[i] = toLitCond( pCnf->pVarNums[pObj->Id], 1 ); - RetValue = sat_solver_solve( pSat, pAssumps, pAssumps+Aig_ManPoNum(p), (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); - free( pAssumps ); - if ( RetValue == l_True ) + int i; + // mark the cones under the cut +// assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + // create the true PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + // create the registers + Vec_PtrForEachEntry( vCut, pObj, i ) + pObj->pData = Aig_ObjCreatePi(pNew); + // duplicate logic above the cut and create POs + Saig_ManForEachLi( p, pObj, i ) { - // accumulate SAT variables of the CIs - vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) ); - Aig_ManForEachPi( p, pObj, i ) - Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] ); - // create the model - pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); - vInit = Vec_IntAllocArray( pModel, Aig_ManPiNum(p) ); - Vec_IntFree( vCiIds ); + Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) ); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); } - sat_solver_delete( pSat ); - Cnf_DataFree( pCnf ); - return vInit; + return pNew; } /**Function************************************************************* @@ -316,7 +437,7 @@ Vec_Int_t * Saig_ManRetimeFindInitState( Aig_Man_t * p ) ***********************************************************************/ Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p ) { - Vec_Ptr_t * vNodes = NULL; + Vec_Ptr_t * vNodes; Aig_Obj_t * pObj, * pFanin; int i, Diffs; assert( Saig_ManRegNum(p) > 0 ); @@ -334,13 +455,20 @@ Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p ) pFanin = Aig_ObjFanin0(pObj); Diffs += pFanin->fMarkA && pFanin->fMarkB; } + vNodes = Vec_PtrAlloc( 100 ); if ( Diffs > 0 ) - vNodes = Vec_PtrAlloc( Diffs ); + { + Saig_ManForEachLi( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + if ( pFanin->fMarkA && pFanin->fMarkB ) + Vec_PtrPush( vNodes, pObj ); + } + assert( Vec_PtrSize(vNodes) == Diffs ); + } Saig_ManForEachLi( p, pObj, i ) { pFanin = Aig_ObjFanin0(pObj); - if ( vNodes && pFanin->fMarkA && pFanin->fMarkB ) - Vec_PtrPush( vNodes, pFanin ); pFanin->fMarkA = pFanin->fMarkB = 0; } return vNodes; @@ -348,7 +476,7 @@ Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p ) /**Function************************************************************* - Synopsis [Duplicates the AIG while retiming the registers to the cut.] + Synopsis [Hides the registers that cannot be backward retimed.] Description [] @@ -357,79 +485,125 @@ Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCutInit ) +int Saig_ManHideBadRegs( Aig_Man_t * p, Vec_Ptr_t * vBadRegs ) { - Vec_Ptr_t * vToExclude, * vCut; - Vec_Int_t * vInit = NULL; - Aig_Man_t * pNew, * pInit; - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int i; - // check if there are bad registers - vToExclude = Saig_ManGetRegistersToExclude( p ); - if ( vToExclude ) - { - vCut = Saig_ManRetimeExtendCut( p, vCutInit, vToExclude ); - printf( "Bad registers = %d. Extended cut from %d to %d nodes.\n", - Vec_PtrSize(vToExclude), Vec_PtrSize(vCutInit), Vec_PtrSize(vCut) ); - Vec_PtrFree( vToExclude ); - } - else - vCut = Vec_PtrDup( vCutInit ); - // mark the cones under the cut -// assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) ); - // count if there are registers to disable - // derive the initial state - pInit = Saig_ManRetimeDupInitState( p, vCut ); - vInit = Saig_ManRetimeFindInitState( pInit ); - if ( vInit == NULL ) - printf( "Initial state computation has failed.\n" ); - Aig_ManStop( pInit ); - // create the new manager - pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); - pNew->pSpec = Aig_UtilStrsav( p->pSpec ); - pNew->nRegs = Vec_PtrSize(vCut); - pNew->nTruePis = p->nTruePis; - pNew->nTruePos = p->nTruePos; - // create the true PIs - Aig_ManCleanData( p ); - Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); - Saig_ManForEachPi( p, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pNew ); - // create the registers - Vec_PtrForEachEntry( vCut, pObj, i ) - pObj->pData = Aig_NotCond( Aig_ObjCreatePi(pNew), vInit?Vec_IntEntry(vInit,i):0 ); - // duplicate logic above the cut and remember values - Saig_ManForEachLi( p, pObj, i ) + Vec_Ptr_t * vPisNew, * vPosNew; + Aig_Obj_t * pObjLi, * pObjLo; + int nTruePi, nTruePo, nBadRegs, i; + if ( Vec_PtrSize(vBadRegs) == 0 ) + return 0; + // attached LOs to LIs + Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) + pObjLi->pData = pObjLo; + // reorder them by putting bad registers first + vPisNew = Vec_PtrDup( p->vPis ); + vPosNew = Vec_PtrDup( p->vPos ); + nTruePi = Aig_ManPiNum(p) - Aig_ManRegNum(p); + nTruePo = Aig_ManPoNum(p) - Aig_ManRegNum(p); + assert( nTruePi == p->nTruePis ); + assert( nTruePo == p->nTruePos ); + Vec_PtrForEachEntry( vBadRegs, pObjLi, i ) { - Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) ); - pObj->pData = Aig_ObjChild0Copy(pObj); + Vec_PtrWriteEntry( vPisNew, nTruePi++, pObjLi->pData ); + Vec_PtrWriteEntry( vPosNew, nTruePo++, pObjLi ); + pObjLi->fMarkA = 1; } - // transfer values from the LIs to the LOs Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) - pObjLo->pData = pObjLi->pData; - // erase the data values on the internal nodes of the cut - Vec_PtrForEachEntry( vCut, pObj, i ) - if ( Aig_ObjIsNode(pObj) ) - pObj->pData = NULL; - // replicate the data on the primary inputs - Saig_ManForEachPi( p, pObj, i ) - pObj->pData = Aig_ManPi( pNew, i ); - // duplicate logic below the cut - Saig_ManForEachPo( p, pObj, i ) { - Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) ); - Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + if ( pObjLi->fMarkA ) + { + pObjLi->fMarkA = 0; + continue; + } + Vec_PtrWriteEntry( vPisNew, nTruePi++, pObjLo ); + Vec_PtrWriteEntry( vPosNew, nTruePo++, pObjLi ); } - Vec_PtrForEachEntry( vCut, pObj, i ) + // check the sizes + assert( nTruePi == Aig_ManPiNum(p) ); + assert( nTruePo == Aig_ManPoNum(p) ); + // transfer the arrays + Vec_PtrFree( p->vPis ); p->vPis = vPisNew; + Vec_PtrFree( p->vPos ); p->vPos = vPosNew; + // update the PIs + nBadRegs = Vec_PtrSize(vBadRegs); + p->nRegs -= nBadRegs; + p->nTruePis += nBadRegs; + p->nTruePos += nBadRegs; + return nBadRegs; +} + +/**Function************************************************************* + + Synopsis [Exposes bad registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManExposeBadRegs( Aig_Man_t * p, int nBadRegs ) +{ + p->nRegs += nBadRegs; + p->nTruePis -= nBadRegs; + p->nTruePos -= nBadRegs; +} + +/**Function************************************************************* + + Synopsis [Performs min-area retiming backward with initial state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManRetimeMinAreaBackward( Aig_Man_t * pNew, int fVerbose ) +{ + Aig_Man_t * pInit, * pFinal; + Vec_Ptr_t * vBadRegs, * vCut; + Vec_Int_t * vInit; + int iBadReg; + // transform the AIG to have no bad registers + vBadRegs = Saig_ManGetRegistersToExclude( pNew ); + if ( fVerbose && Vec_PtrSize(vBadRegs) ) + printf( "Excluding %d registers that cannot be backward retimed.\n", Vec_PtrSize(vBadRegs) ); + while ( 1 ) { - Saig_ManRetimeDup_rec( pNew, pObj ); - Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, vInit?Vec_IntEntry(vInit,i):0) ); + Saig_ManHideBadRegs( pNew, vBadRegs ); + Vec_PtrFree( vBadRegs ); + // compute cut + vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose ); + if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) ) + { + Vec_PtrFree( vCut ); + return NULL; + } + // derive the initial state + pInit = Saig_ManRetimeDupInitState( pNew, vCut ); + vInit = Saig_ManRetimeInitState( pInit ); + if ( vInit != NULL ) + { + pFinal = Saig_ManRetimeDupBackward( pNew, vCut, vInit ); + Vec_IntFree( vInit ); + Vec_PtrFree( vCut ); + Aig_ManStop( pInit ); + return pFinal; + } + Vec_PtrFree( vCut ); + // there is no initial state - find the offending output + iBadReg = Saig_ManRetimeUnsatCore( pInit, fVerbose ); + Aig_ManStop( pInit ); + if ( fVerbose ) + printf( "Excluding register %d.\n", iBadReg ); + // prepare to remove this output + vBadRegs = Vec_PtrAlloc( 1 ); + Vec_PtrPush( vBadRegs, Aig_ManPo( pNew, Saig_ManPoNum(pNew) + iBadReg ) ); } - if ( vInit ) - Vec_IntFree( vInit ); - Vec_PtrFree( vCut ); - return pNew; + return NULL; } /**Function************************************************************* @@ -443,36 +617,73 @@ Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCutInit ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fVerbose ) +Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ) { Vec_Ptr_t * vCut; - Aig_Man_t * pNew, * pTemp; + Aig_Man_t * pNew, * pTemp, * pCopy; + int fChanges; pNew = Aig_ManDup( p ); // perform several iterations of forward retiming + fChanges = 0; if ( !fBackwardOnly ) while ( 1 ) { vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose ); if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) ) { + if ( fVerbose && !fChanges ) + printf( "Forward retiming cannot reduce registers.\n" ); Vec_PtrFree( vCut ); break; } pNew = Saig_ManRetimeDupForward( pTemp = pNew, vCut ); Aig_ManStop( pTemp ); Vec_PtrFree( vCut ); + if ( fVerbose ) + Aig_ManReportImprovement( p, pNew ); + fChanges = 1; } - // perform one iteration of backward retiming - if ( !fForwardOnly ) + // perform several iterations of backward retiming + fChanges = 0; + if ( !fForwardOnly && !fInitial ) + while ( 1 ) { vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose ); - if ( Vec_PtrSize(vCut) < Aig_ManRegNum(pNew) ) + if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) ) { - pNew = Saig_ManRetimeDupBackward( pTemp = pNew, vCut ); - Aig_ManStop( pTemp ); + if ( fVerbose && !fChanges ) + printf( "Backward retiming cannot reduce registers.\n" ); + Vec_PtrFree( vCut ); + break; } + pNew = Saig_ManRetimeDupBackward( pTemp = pNew, vCut, NULL ); + Aig_ManStop( pTemp ); Vec_PtrFree( vCut ); + if ( fVerbose ) + Aig_ManReportImprovement( p, pNew ); + fChanges = 1; + } + else if ( !fForwardOnly && fInitial ) + while ( 1 ) + { + pCopy = Aig_ManDup( pNew ); + pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose ); + Aig_ManStop( pCopy ); + if ( pTemp == NULL ) + { + if ( fVerbose && !fChanges ) + printf( "Backward retiming cannot reduce registers.\n" ); + break; + } + Saig_ManExposeBadRegs( pTemp, Saig_ManPoNum(pTemp) - Saig_ManPoNum(pNew) ); + Aig_ManStop( pNew ); + pNew = pTemp; + if ( fVerbose ) + Aig_ManReportImprovement( p, pNew ); + fChanges = 1; } + if ( !fForwardOnly && !fInitial && fChanges ) + printf( "Assuming const-0 init-state after backward retiming. Result will not verify.\n" ); return pNew; } -- cgit v1.2.3