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/saig/saigRetMin.c | 517 ++++++++++++++++++++++++++++++++-------------- 1 file changed, 364 insertions(+), 153 deletions(-) (limited to 'src/aig/saig/saigRetMin.c') 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