From f936cc0680c98ffe51b3a1716c996072d5dbf76c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 18 Jan 2009 08:01:00 -0800 Subject: Version abc90118 --- src/aig/cgt/cgt.h | 3 +- src/aig/cgt/cgtAig.c | 381 ++++++++++++++++++++++++++++++++++++++++++------ src/aig/cgt/cgtCore.c | 112 ++++++++++---- src/aig/cgt/cgtDecide.c | 220 ++++++++++++++++++++++++++-- src/aig/cgt/cgtInt.h | 21 ++- src/aig/cgt/cgtMan.c | 50 ++++--- 6 files changed, 673 insertions(+), 114 deletions(-) (limited to 'src/aig/cgt') diff --git a/src/aig/cgt/cgt.h b/src/aig/cgt/cgt.h index b9997d56..f8c1cc2e 100644 --- a/src/aig/cgt/cgt.h +++ b/src/aig/cgt/cgt.h @@ -52,8 +52,9 @@ struct Cgt_Par_t_ int nConfMax; // the max number of conflicts at a node int nVarsMin; // the min number of variables to recycle the SAT solver int nFlopsMin; // the min number of flops needed to recycle the SAT solver + int fAreaOnly; // derive clock gating to minimize area int fVerbose; // verbosity flag - + int fVeryVerbose; // verbosity flag }; //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cgt/cgtAig.c b/src/aig/cgt/cgtAig.c index b30d3f16..d411c25a 100644 --- a/src/aig/cgt/cgtAig.c +++ b/src/aig/cgt/cgtAig.c @@ -67,7 +67,7 @@ void Cgt_ManDetectCandidates_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevel void Cgt_ManDetectCandidates( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands ) { Vec_PtrClear( vCands ); - if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) ) + if ( !Aig_ObjIsNode(pObj) ) return; Aig_ManIncrementTravId( pAig ); Cgt_ManDetectCandidates_rec( pAig, pObj, nLevelMax, vCands ); @@ -134,6 +134,67 @@ void Cgt_ManDetectFanout( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_P assert( Vec_PtrSize(vFanout) > 0 ); } +/**Function************************************************************* + + Synopsis [Computes visited nodes in the topological order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_ManCollectVisited_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vVisited ) +{ + if ( Aig_ObjIsPi(pObj) ) + return; + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(pAig, pObj); + assert( Aig_ObjIsNode(pObj) ); + Cgt_ManCollectVisited_rec( pAig, Aig_ObjFanin0(pObj), vVisited ); + Cgt_ManCollectVisited_rec( pAig, Aig_ObjFanin1(pObj), vVisited ); + Vec_PtrPush( vVisited, pObj ); +} + +/**Function************************************************************* + + Synopsis [Computes visited nodes in the topological order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_ManCollectVisited( Aig_Man_t * pAig, Vec_Ptr_t * vFanout, Vec_Ptr_t * vVisited ) +{ + Aig_Obj_t * pObj; + int i; + Vec_PtrClear( vVisited ); + Aig_ManIncrementTravId( pAig ); + Vec_PtrForEachEntry( vFanout, pObj, i ) + Cgt_ManCollectVisited_rec( pAig, pObj, vVisited ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Aig_Obj_t * Aig_ObjChild0CopyVec( Vec_Ptr_t * vCopy, Aig_Obj_t * pObj ) +{ return Aig_NotCond((Aig_Obj_t *)Vec_PtrEntry(vCopy, Aig_ObjFaninId0(pObj)), Aig_ObjFaninC0(pObj)); } +static inline Aig_Obj_t * Aig_ObjChild1CopyVec( Vec_Ptr_t * vCopy, Aig_Obj_t * pObj ) +{ return Aig_NotCond((Aig_Obj_t *)Vec_PtrEntry(vCopy, Aig_ObjFaninId1(pObj)), Aig_ObjFaninC1(pObj)); } + /**Function************************************************************* Synopsis [Derives miter for clock-gating.] @@ -145,15 +206,46 @@ void Cgt_ManDetectFanout( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_P SeeAlso [] ***********************************************************************/ -Aig_Obj_t * Cgt_ManConstructMiter( Cgt_Man_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObjLo ) +Aig_Obj_t * Cgt_ManConstructCareCondition( Cgt_Man_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObjLo, Vec_Ptr_t * vCopy0, Vec_Ptr_t * vCopy1 ) { - Aig_Obj_t * pMiter, * pRoot; + Aig_Obj_t * pMiter, * pObj, * pTemp; int i; assert( Aig_ObjIsPi(pObjLo) ); - pMiter = Aig_ManConst0( pNew ); + // detect nodes and their cone Cgt_ManDetectFanout( p->pAig, pObjLo, p->pPars->nOdcMax, p->vFanout ); - Vec_PtrForEachEntry( p->vFanout, pRoot, i ) - pMiter = Aig_Or( pNew, pMiter, Aig_Exor(pNew, pRoot->pData, pRoot->pNext) ); + Cgt_ManCollectVisited( p->pAig, p->vFanout, p->vVisited ); + // add new variables if the observability condition depends on PI variables + Vec_PtrForEachEntry( p->vVisited, pObj, i ) + { + assert( Aig_ObjIsNode(pObj) ); + if ( Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObj)) && Vec_PtrEntry(vCopy0, Aig_ObjFaninId0(pObj)) == NULL ) + { + pTemp = Aig_ObjCreatePi( pNew ); + Vec_PtrWriteEntry( vCopy0, Aig_ObjFaninId0(pObj), pTemp ); + Vec_PtrWriteEntry( vCopy1, Aig_ObjFaninId0(pObj), pTemp ); + } + if ( Saig_ObjIsPi(p->pAig, Aig_ObjFanin1(pObj)) && Vec_PtrEntry(vCopy0, Aig_ObjFaninId1(pObj)) == NULL ) + { + pTemp = Aig_ObjCreatePi( pNew ); + Vec_PtrWriteEntry( vCopy0, Aig_ObjFaninId1(pObj), pTemp ); + Vec_PtrWriteEntry( vCopy1, Aig_ObjFaninId1(pObj), pTemp ); + } + } + // construct AIGs for the nodes + Vec_PtrForEachEntry( p->vVisited, pObj, i ) + { + pTemp = Aig_And( pNew, Aig_ObjChild0CopyVec(vCopy0, pObj), Aig_ObjChild1CopyVec(vCopy0, pObj) ); + Vec_PtrWriteEntry( vCopy0, Aig_ObjId(pObj), pTemp ); + pTemp = Aig_And( pNew, Aig_ObjChild0CopyVec(vCopy1, pObj), Aig_ObjChild1CopyVec(vCopy1, pObj) ); + Vec_PtrWriteEntry( vCopy1, Aig_ObjId(pObj), pTemp ); + } + // construct the care miter + pMiter = Aig_ManConst0( pNew ); + Vec_PtrForEachEntry( p->vFanout, pObj, i ) + { + pTemp = Aig_Exor( pNew, Vec_PtrEntry(vCopy0, Aig_ObjId(pObj)), Vec_PtrEntry(vCopy1, Aig_ObjId(pObj)) ); + pMiter = Aig_Or( pNew, pMiter, pTemp ); + } return pMiter; } @@ -171,11 +263,12 @@ Aig_Obj_t * Cgt_ManConstructMiter( Cgt_Man_t * p, Aig_Man_t * pNew, Aig_Obj_t * Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p ) { Aig_Man_t * pNew; - Aig_Obj_t * pObj, * pObjLi, * pObjLo; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pCare, * pMiter; + Vec_Ptr_t * vCopy0, * vCopy1; int i; assert( Aig_ManRegNum(p->pAig) ); - Aig_ManCleanNext( p->pAig ); pNew = Aig_ManStart( Aig_ManObjNumMax(p->pAig) ); + pNew->pName = Aig_UtilStrsav( "CG_miter" ); // build the first frame Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew); Aig_ManForEachPi( p->pAig, pObj, i ) @@ -184,24 +277,126 @@ Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p ) pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); // Saig_ManForEachPo( p->pAig, pObj, i ) // pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); - // build the second frame - Aig_ManConst1(p->pAig)->pNext = Aig_ManConst1(pNew); - Saig_ManForEachPi( p->pAig, pObj, i ) - pObj->pNext = Aig_ObjCreatePi( pNew ); - Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) - pObjLo->pNext = Aig_ObjChild0Copy(pObjLi); - Aig_ManForEachNode( p->pAig, pObj, i ) - if ( Aig_ObjLevel(pObj) <= p->pPars->nOdcMax ) - pObj->pNext = Aig_And( pNew, Aig_ObjChild0Next(pObj), Aig_ObjChild1Next(pObj) ); - // construct clock-gating miters for each register input - Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) - pObjLi->pData = Aig_ObjCreatePo( pNew, Cgt_ManConstructMiter(p, pNew, pObjLo) ); - Aig_ManCleanNext( p->pAig ); - Aig_ManSetPioNumbers( p->pAig ); + if ( p->pPars->nOdcMax > 0 ) + { + // create storage for observability conditions + vCopy0 = Vec_PtrStart( Aig_ManObjNumMax(p->pAig) ); + vCopy1 = Vec_PtrStart( Aig_ManObjNumMax(p->pAig) ); + // initialize register outputs + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + { + Vec_PtrWriteEntry( vCopy0, Aig_ObjId(pObjLo), Aig_ObjChild0Copy(pObjLi) ); + Vec_PtrWriteEntry( vCopy1, Aig_ObjId(pObjLo), Aig_ObjChild0Copy(pObjLi) ); + } + // compute observability condition for each latch output + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + { + // set the constants + Vec_PtrWriteEntry( vCopy0, Aig_ObjId(pObjLo), Aig_ManConst0(pNew) ); + Vec_PtrWriteEntry( vCopy1, Aig_ObjId(pObjLo), Aig_ManConst1(pNew) ); + // compute condition + pCare = Cgt_ManConstructCareCondition( p, pNew, pObjLo, vCopy0, vCopy1 ); + // restore the values + Vec_PtrWriteEntry( vCopy0, Aig_ObjId(pObjLo), Aig_ObjChild0Copy(pObjLi) ); + Vec_PtrWriteEntry( vCopy1, Aig_ObjId(pObjLo), Aig_ObjChild0Copy(pObjLi) ); + // compute the miter + pMiter = Aig_Exor( pNew, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) ); + pMiter = Aig_And( pNew, pMiter, pCare ); + pObjLi->pData = Aig_ObjCreatePo( pNew, pMiter ); + } + Vec_PtrFree( vCopy0 ); + Vec_PtrFree( vCopy1 ); + } + else + { + // construct clock-gating miters for each register input + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + { + pMiter = Aig_Exor( pNew, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) ); + pObjLi->pData = Aig_ObjCreatePo( pNew, pMiter ); + } + } Aig_ManCleanup( pNew ); + Aig_ManSetPioNumbers( pNew ); return pNew; } +/**Function************************************************************* + + Synopsis [Adds relevant constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Cgt_ManConstructCare_rec( Aig_Man_t * pCare, Aig_Obj_t * pObj, Aig_Man_t * pNew ) +{ + Aig_Obj_t * pObj0, * pObj1; + if ( Aig_ObjIsTravIdCurrent( pCare, pObj ) ) + return pObj->pData; + Aig_ObjSetTravIdCurrent( pCare, pObj ); + if ( Aig_ObjIsPi(pObj) ) + return pObj->pData = NULL; + pObj0 = Cgt_ManConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pNew ); + if ( pObj0 == NULL ) + return pObj->pData = NULL; + pObj1 = Cgt_ManConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pNew ); + if ( pObj1 == NULL ) + return pObj->pData = NULL; + pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) ); + pObj1 = Aig_NotCond( pObj1, Aig_ObjFaninC1(pObj) ); + return pObj->pData = Aig_And( pNew, pObj0, pObj1 ); +} + +/**Function************************************************************* + + Synopsis [Builds constraints belonging to the given partition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_ManConstructCare( Aig_Man_t * pNew, Aig_Man_t * pCare, Vec_Vec_t * vSuppsInv, Vec_Ptr_t * vLeaves ) +{ + Vec_Int_t * vOuts; + Aig_Obj_t * pLeaf, * pPi, * pPo, * pObjAig; + int i, k, iOut; + // go through the PIs of the partition + // label the corresponding PIs of the care set + Aig_ManIncrementTravId( pCare ); + Vec_PtrForEachEntry( vLeaves, pLeaf, i ) + { + pPi = Aig_ManPi( pCare, Aig_ObjPioNum(pLeaf) ); + Aig_ObjSetTravIdCurrent( pCare, pPi ); + pPi->pData = pLeaf->pData; + } + // construct the constraints + Vec_PtrForEachEntry( vLeaves, pLeaf, i ) + { + vOuts = Vec_VecEntry( vSuppsInv, Aig_ObjPioNum(pLeaf) ); + Vec_IntForEachEntry( vOuts, iOut, k ) + { + pPo = Aig_ManPo( pCare, iOut ); + if ( Aig_ObjIsTravIdCurrent( pCare, pPo ) ) + continue; + Aig_ObjSetTravIdCurrent( pCare, pPo ); + if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(pCare) ) + continue; + pObjAig = Cgt_ManConstructCare_rec( pCare, Aig_ObjFanin0(pPo), pNew ); + if ( pObjAig == NULL ) + continue; + pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) ); + Aig_ObjCreatePo( pNew, pObjAig ); + } + } +} + /**Function************************************************************* Synopsis [Duplicates the AIG recursively.] @@ -213,15 +408,19 @@ Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Obj_t * Cgt_ManDupPartition_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj_t * pObj ) +Aig_Obj_t * Cgt_ManDupPartition_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vLeaves ) { if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) return pObj->pData; Aig_ObjSetTravIdCurrent(pAig, pObj); if ( Aig_ObjIsPi(pObj) ) - return pObj->pData = Aig_ObjCreatePi( pNew ); - Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); - Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin1(pObj) ); + { + pObj->pData = Aig_ObjCreatePi( pNew ); + Vec_PtrPush( vLeaves, pObj ); + return pObj->pData; + } + Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj), vLeaves ); + Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin1(pObj), vLeaves ); return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); } @@ -236,32 +435,78 @@ Aig_Obj_t * Cgt_ManDupPartition_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj SeeAlso [] ***********************************************************************/ -Aig_Man_t * Cgt_ManDupPartition( Aig_Man_t * pAig, int nVarsMin, int nFlopsMin, int iStart ) +Aig_Man_t * Cgt_ManDupPartition( Aig_Man_t * pFrame, int nVarsMin, int nFlopsMin, int iStart, Aig_Man_t * pCare, Vec_Vec_t * vSuppsInv, int * pnOutputs ) { + Vec_Ptr_t * vRoots, * vLeaves, * vPos; Aig_Man_t * pNew; Aig_Obj_t * pObj; int i; - assert( Aig_ManRegNum(pAig) == 0 ); + assert( Aig_ManRegNum(pFrame) == 0 ); + vRoots = Vec_PtrAlloc( 100 ); + vLeaves = Vec_PtrAlloc( 100 ); + vPos = Vec_PtrAlloc( 100 ); pNew = Aig_ManStart( nVarsMin ); - Aig_ManIncrementTravId( pAig ); - Aig_ManConst1(pAig)->pData = Aig_ManConst1(pNew); - Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) ); - for ( i = iStart; i < iStart + nFlopsMin && i < Aig_ManPoNum(pAig); i++ ) + pNew->pName = Aig_UtilStrsav( "partition" ); + Aig_ManIncrementTravId( pFrame ); + Aig_ManConst1(pFrame)->pData = Aig_ManConst1(pNew); + Aig_ObjSetTravIdCurrent( pFrame, Aig_ManConst1(pFrame) ); + for ( i = iStart; i < iStart + nFlopsMin && i < Aig_ManPoNum(pFrame); i++ ) { - pObj = Aig_ManPo( pAig, i ); - Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); - pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + pObj = Aig_ManPo( pFrame, i ); + Cgt_ManDupPartition_rec( pNew, pFrame, Aig_ObjFanin0(pObj), vLeaves ); + Vec_PtrPush( vRoots, Aig_ObjChild0Copy(pObj) ); + Vec_PtrPush( vPos, pObj ); } - for ( ; Aig_ManObjNum(pNew) < nVarsMin && i < Aig_ManPoNum(pAig); i++ ) + for ( ; Aig_ManObjNum(pNew) < nVarsMin && i < Aig_ManPoNum(pFrame); i++ ) { - pObj = Aig_ManPo( pAig, i ); - Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); - pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + pObj = Aig_ManPo( pFrame, i ); + Cgt_ManDupPartition_rec( pNew, pFrame, Aig_ObjFanin0(pObj), vLeaves ); + Vec_PtrPush( vRoots, Aig_ObjChild0Copy(pObj) ); + Vec_PtrPush( vPos, pObj ); } - assert( nFlopsMin >= Aig_ManPoNum(pAig) || Aig_ManPoNum(pNew) >= nFlopsMin ); + assert( nFlopsMin >= Vec_PtrSize(vRoots) || Vec_PtrSize(vRoots) >= nFlopsMin ); + // create constaints + if ( pCare ) + Cgt_ManConstructCare( pNew, pCare, vSuppsInv, vLeaves ); + // create POs + Vec_PtrForEachEntry( vPos, pObj, i ) + pObj->pData = Aig_ObjCreatePo( pNew, Vec_PtrEntry(vRoots, i) ); + if ( pnOutputs != NULL ) + *pnOutputs = Vec_PtrSize( vPos ); + Vec_PtrFree( vRoots ); + Vec_PtrFree( vLeaves ); + Vec_PtrFree( vPos ); return pNew; } +/**Function************************************************************* + + Synopsis [Implements one clock-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Cgt_ManBuildClockGate( Aig_Man_t * pNew, Vec_Ptr_t * vGates ) +{ + Aig_Obj_t * pGate, * pTotal; + int i; + assert( Vec_PtrSize(vGates) > 0 ); + pTotal = Aig_ManConst0(pNew); + Vec_PtrForEachEntry( vGates, pGate, i ) + { + if ( Aig_Regular(pGate)->pNext ) + pGate = Aig_NotCond( Aig_Regular(pGate)->pNext, Aig_IsComplement(pGate) ); + else + pGate = Aig_NotCond( Aig_Regular(pGate)->pData, Aig_IsComplement(pGate) ); + pTotal = Aig_Or( pNew, pTotal, pGate ); + } + return pTotal; +} + /**Function************************************************************* Synopsis [Derives AIG after clock-gating.] @@ -273,34 +518,74 @@ Aig_Man_t * Cgt_ManDupPartition( Aig_Man_t * pAig, int nVarsMin, int nFlopsMin, SeeAlso [] ***********************************************************************/ -Aig_Man_t * Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Ptr_t * vGates ) +Aig_Man_t * Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Vec_t * vGates, int fReduce, int * pnUsedNodes ) { Aig_Man_t * pNew; - Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo, * pGate, * pGateNew; - int i; + Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo, * pGateNew; + Vec_Ptr_t * vOne; + int i, k; + Aig_ManCleanNext( pAig ); + // label nodes + Vec_VecForEachEntry( vGates, pObj, i, k ) + { + if ( Aig_IsComplement(pObj) ) + Aig_Regular(pObj)->fMarkB = 1; + else + Aig_Regular(pObj)->fMarkA = 1; + } + // construct AIG assert( Aig_ManRegNum(pAig) ); pNew = Aig_ManStart( Aig_ManObjNumMax(pAig) ); + pNew->pName = Aig_UtilStrsav( pAig->pName ); + pNew->pSpec = Aig_UtilStrsav( pAig->pSpec ); Aig_ManConst1(pAig)->pData = Aig_ManConst1(pNew); Aig_ManForEachPi( pAig, pObj, i ) pObj->pData = Aig_ObjCreatePi( pNew ); - Aig_ManForEachNode( pAig, pObj, i ) - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + if ( fReduce ) + { + Aig_ManForEachNode( pAig, pObj, i ) + { + assert( !(pObj->fMarkA && pObj->fMarkB) ); + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + if ( pObj->fMarkA ) + { + pObj->pNext = pObj->pData; + pObj->pData = Aig_ManConst0(pNew); + } + else if ( pObj->fMarkB ) + { + pObj->pNext = pObj->pData; + pObj->pData = Aig_ManConst1(pNew); + } + } + } + else + { + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + } + if ( pnUsedNodes != NULL ) + *pnUsedNodes = Aig_ManNodeNum(pNew); Saig_ManForEachPo( pAig, pObj, i ) pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) { - pGate = Vec_PtrEntry( vGates, i ); - if ( pGate == NULL ) + vOne = Vec_VecEntry( vGates, i ); + if ( Vec_PtrSize(vOne) == 0 ) pObjNew = Aig_ObjChild0Copy(pObjLi); else { - pGateNew = Aig_NotCond( Aig_Regular(pGate)->pData, Aig_IsComplement(pGate) ); +// pGateNew = Aig_NotCond( Aig_Regular(pGate)->pData, Aig_IsComplement(pGate) ); + pGateNew = Cgt_ManBuildClockGate( pNew, vOne ); pObjNew = Aig_Mux( pNew, pGateNew, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) ); } pObjLi->pData = Aig_ObjCreatePo( pNew, pObjNew ); } Aig_ManCleanup( pNew ); Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) ); + // unlabel nodes + Aig_ManCleanMarkAB( pAig ); + Aig_ManCleanNext( pAig ); return pNew; } diff --git a/src/aig/cgt/cgtCore.c b/src/aig/cgt/cgtCore.c index a06820b4..f49cd46f 100644 --- a/src/aig/cgt/cgtCore.c +++ b/src/aig/cgt/cgtCore.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "cgtInt.h" +#include "bar.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -42,13 +43,14 @@ void Cgt_SetDefaultParams( Cgt_Par_t * p ) { memset( p, 0, sizeof(Cgt_Par_t) ); - p->nLevelMax = 1000; // the max number of levels to look for clock-gates + p->nLevelMax = 25; // the max number of levels to look for clock-gates p->nCandMax = 1000; // the max number of candidates at each node p->nOdcMax = 0; // the max number of ODC levels to consider - p->nConfMax = 1000; // the max number of conflicts at a node - p->nVarsMin = 5000; // the min number of vars to recycle the SAT solver - p->nFlopsMin = 25; // the min number of flops to recycle the SAT solver - p->fVerbose = 0; // verbosity flag + p->nConfMax = 10; // the max number of conflicts at a node + p->nVarsMin = 1000; // the min number of vars to recycle the SAT solver + p->nFlopsMin = 5; // the min number of flops to recycle the SAT solver + p->fAreaOnly = 0; // derive clock-gating to minimize area + p->fVerbose = 1; // verbosity flag } /**Function************************************************************* @@ -62,14 +64,14 @@ void Cgt_SetDefaultParams( Cgt_Par_t * p ) SeeAlso [] ***********************************************************************/ -int Cgt_SimulationFilter( Cgt_Man_t * p, Aig_Obj_t * pCandFrame, Aig_Obj_t * pMiterFrame ) +int Cgt_SimulationFilter( Cgt_Man_t * p, Aig_Obj_t * pCandPart, Aig_Obj_t * pMiterPart ) { unsigned * pInfoCand, * pInfoMiter; int w, nWords = Aig_BitWordNum( p->nPatts ); - pInfoCand = Vec_PtrEntry( p->vPatts, Aig_ObjId(Aig_Regular(pCandFrame)) ); - pInfoMiter = Vec_PtrEntry( p->vPatts, Aig_ObjId(pMiterFrame) ); + pInfoCand = Vec_PtrEntry( p->vPatts, Aig_ObjId(Aig_Regular(pCandPart)) ); + pInfoMiter = Vec_PtrEntry( p->vPatts, Aig_ObjId(pMiterPart) ); // C => !M -- true is the same as C & M -- false - if ( !Aig_IsComplement(pCandFrame) ) + if ( !Aig_IsComplement(pCandPart) ) { for ( w = 0; w < nWords; w++ ) if ( pInfoCand[w] & pInfoMiter[w] ) @@ -106,6 +108,7 @@ void Cgt_SimulationRecord( Cgt_Man_t * p ) if ( p->nPatts == 32 * p->nPattWords ) { Vec_PtrReallocSimInfo( p->vPatts ); + Vec_PtrCleanSimInfo( p->vPatts, p->nPattWords, 2 * p->nPattWords ); p->nPattWords *= 2; } } @@ -121,15 +124,16 @@ void Cgt_SimulationRecord( Cgt_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart ) +void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart, int nOutputs ) { Vec_Ptr_t * vNodes = p->vFanout; Aig_Obj_t * pMiter, * pCand, * pMiterFrame, * pCandFrame, * pMiterPart, * pCandPart; - int i, k, RetValue; + int i, k, RetValue, nCalls; assert( Vec_VecSize(p->vGatesAll) == Aig_ManPoNum(p->pFrame) ); // go through all the registers inputs of this range - for ( i = iStart; i < iStart + Aig_ManPoNum(p->pPart); i++ ) + for ( i = iStart; i < iStart + nOutputs; i++ ) { + nCalls = p->nCalls; pMiter = Saig_ManLi( p->pAig, i ); Cgt_ManDetectCandidates( p->pAig, Aig_ObjFanin0(pMiter), p->pPars->nLevelMax, vNodes ); // go through the candidates of this PO @@ -153,6 +157,8 @@ void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart ) if ( RetValue == 0 ) Cgt_SimulationRecord( p ); } + else + p->nCallsFiltered++; // try reverse polarity if ( Cgt_SimulationFilter( p, Aig_Not(pCandPart), pMiterPart ) ) { @@ -165,9 +171,18 @@ void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart ) if ( RetValue == 0 ) Cgt_SimulationRecord( p ); } + else + p->nCallsFiltered++; } + + if ( p->pPars->fVerbose ) + { +// printf( "Flop %3d : Cand = %4d. Gate = %4d. SAT calls = %3d.\n", +// i, Vec_PtrSize(vNodes), Vec_PtrSize(Vec_VecEntry(p->vGatesAll, i)), p->nCalls-nCalls ); + } + } -} +} /**Function************************************************************* @@ -182,16 +197,33 @@ void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart ) ***********************************************************************/ int Cgt_ClockGatingRange( Cgt_Man_t * p, int iStart ) { - int iStop; - p->pPart = Cgt_ManDupPartition( p->pFrame, p->pPars->nVarsMin, p->pPars->nFlopsMin, iStart ); - p->pCnf = Cnf_DeriveSimple( p->pPart, Aig_ManPoNum(p->pPart) ); + int nOutputs, iStop, clk, clkTotal = clock(); + int nCallsUnsat = p->nCallsUnsat; + int nCallsSat = p->nCallsSat; + int nCallsUndec = p->nCallsUndec; + int nCallsFiltered = p->nCallsFiltered; +clk = clock(); + p->pPart = Cgt_ManDupPartition( p->pFrame, p->pPars->nVarsMin, p->pPars->nFlopsMin, iStart, p->pCare, p->vSuppsInv, &nOutputs ); + p->pCnf = Cnf_DeriveSimple( p->pPart, nOutputs ); p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 ); sat_solver_compress( p->pSat ); - p->vPatts = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pPart), 16 ); + p->vPatts = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pPart), p->nPattWords ); Vec_PtrCleanSimInfo( p->vPatts, 0, p->nPattWords ); - Cgt_ClockGatingRangeCheck( p, iStart ); - iStop = iStart + Aig_ManPoNum(p->pPart); +p->timePrepare += clock() - clk; + Cgt_ClockGatingRangeCheck( p, iStart, nOutputs ); + iStop = iStart + nOutputs; + if ( p->pPars->fVeryVerbose ) + { + printf( "%5d : D =%4d. C =%5d. Var =%6d. Pr =%5d. Cex =%5d. F =%4d. Saved =%6d. ", + iStart, iStop-iStart, Aig_ManPoNum(p->pPart)-nOutputs, p->pSat->size, + p->nCallsUnsat-nCallsUnsat, + p->nCallsSat -nCallsSat, + p->nCallsUndec-nCallsUndec, + p->nCallsFiltered-nCallsFiltered ); + PRT( "Time", clock() - clkTotal ); + } Cgt_ManClean( p ); + p->nRecycles++; return iStop; } @@ -208,18 +240,30 @@ int Cgt_ClockGatingRange( Cgt_Man_t * p, int iStart ) ***********************************************************************/ Vec_Vec_t * Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars ) { - Cgt_Par_t Pars; + Bar_Progress_t * pProgress = NULL; + Cgt_Par_t Pars; Cgt_Man_t * p; Vec_Vec_t * vGatesAll; - int iStart; + int iStart, clk = clock(), clkTotal = clock(); + // reset random numbers + Aig_ManRandom( 1 ); if ( pPars == NULL ) Cgt_SetDefaultParams( pPars = &Pars ); p = Cgt_ManCreate( pAig, pCare, pPars ); p->pFrame = Cgt_ManDeriveAigForGating( p ); +p->timeAig += clock() - clk; assert( Aig_ManPoNum(p->pFrame) == Saig_ManRegNum(p->pAig) ); + pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p->pFrame) ); for ( iStart = 0; iStart < Aig_ManPoNum(p->pFrame); ) + { + Bar_ProgressUpdate( pProgress, iStart, NULL ); iStart = Cgt_ClockGatingRange( p, iStart ); + } + Bar_ProgressStop( pProgress ); vGatesAll = p->vGatesAll; + p->vGatesAll = NULL; +p->timeTotal = clock() - clkTotal; + Cgt_ManStop( p ); return vGatesAll; } @@ -238,11 +282,29 @@ Aig_Man_t * Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pP { Aig_Man_t * pGated; Vec_Vec_t * vGatesAll; - Vec_Ptr_t * vGates; + Vec_Vec_t * vGates; + int nNodesUsed, clk = clock(); vGatesAll = Cgt_ClockGatingCandidates( pAig, pCare, pPars ); - vGates = Cgt_ManDecideSimple( pAig, vGatesAll ); - pGated = Cgt_ManDeriveGatedAig( pAig, vGates ); - Vec_PtrFree( vGates ); + if ( pPars->fAreaOnly ) + vGates = Cgt_ManDecideArea( pAig, vGatesAll, pPars->nOdcMax, pPars->fVerbose ); + else + vGates = Cgt_ManDecideSimple( pAig, vGatesAll, pPars->nOdcMax, pPars->fVerbose ); + if ( pPars->fVerbose ) + { +// printf( "Before CG: " ); +// Aig_ManPrintStats( pAig ); + } + pGated = Cgt_ManDeriveGatedAig( pAig, vGates, pPars->fAreaOnly, &nNodesUsed ); + if ( pPars->fVerbose ) + { +// printf( "After CG: " ); +// Aig_ManPrintStats( pGated ); + printf( "Nodes: Before CG = %6d. After CG = %6d. (%6.2f %%). Total after CG = %6d.\n", + Aig_ManNodeNum(pAig), nNodesUsed, + 100.0*nNodesUsed/Aig_ManNodeNum(pAig), + Aig_ManNodeNum(pGated) ); + } + Vec_VecFree( vGates ); Vec_VecFree( vGatesAll ); return pGated; } diff --git a/src/aig/cgt/cgtDecide.c b/src/aig/cgt/cgtDecide.c index 8f57bd4a..0fb2a681 100644 --- a/src/aig/cgt/cgtDecide.c +++ b/src/aig/cgt/cgtDecide.c @@ -25,8 +25,11 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand ); extern int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand ); +extern int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand ); +extern int Ssw_SmlCountEqual( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo ); +extern int Ssw_SmlNodeCountOnesReal( Ssw_Sml_t * p, Aig_Obj_t * pObj ); +extern int Ssw_SmlNodeCountOnesRealVec( Ssw_Sml_t * p, Vec_Ptr_t * vObjs ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -34,7 +37,7 @@ extern int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Ob /**Function************************************************************* - Synopsis [Chooses what clock-gate to use for each register.] + Synopsis [Collects POs in the transitive fanout.] Description [] @@ -43,11 +46,127 @@ extern int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Ob SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Cgt_ManDecide( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll ) +void Cgt_ManCollectFanoutPos_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vFanout ) +{ + Aig_Obj_t * pFanout; + int f, iFanout; + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(pAig, pObj); + if ( Aig_ObjIsPo(pObj) ) + { + Vec_PtrPush( vFanout, pObj ); + return; + } + Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, f ) + Cgt_ManCollectFanoutPos_rec( pAig, pFanout, vFanout ); +} + +/**Function************************************************************* + + Synopsis [Collects POs in the transitive fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_ManCollectFanoutPos( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vFanout ) +{ + Vec_PtrClear( vFanout ); + Aig_ManIncrementTravId( pAig ); + Cgt_ManCollectFanoutPos_rec( pAig, pObj, vFanout ); +} + +/**Function************************************************************* + + Synopsis [Checks if all PO fanouts can be gated by this node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cgt_ManCheckGateComplete( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, Aig_Obj_t * pGate, Vec_Ptr_t * vFanout ) { Vec_Ptr_t * vGates; - vGates = Vec_PtrStart( Saig_ManRegNum(pAig) ); - return vGates; + Aig_Obj_t * pObj; + int i; + Vec_PtrForEachEntry( vFanout, pObj, i ) + { + if ( Saig_ObjIsPo(pAig, pObj) ) + return 0; + vGates = Vec_VecEntry( vGatesAll, Aig_ObjPioNum(pObj) - Saig_ManPoNum(pAig) ); + if ( Vec_PtrFind( vGates, pGate ) == -1 ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes the set of complete clock gates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Cgt_ManCompleteGates( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdcMax, int fVerbose ) +{ + Vec_Ptr_t * vFanout, * vGatesFull; + Aig_Obj_t * pGate, * pGateR; + int i, k; + vFanout = Vec_PtrAlloc( 100 ); + vGatesFull = Vec_PtrAlloc( 100 ); + Vec_VecForEachEntry( vGatesAll, pGate, i, k ) + { + pGateR = Aig_Regular(pGate); + if ( pGateR->fMarkA ) + continue; + pGateR->fMarkA = 1; + Cgt_ManCollectFanoutPos( pAig, pGateR, vFanout ); + if ( Cgt_ManCheckGateComplete( pAig, vGatesAll, pGate, vFanout ) ) + Vec_PtrPush( vGatesFull, pGate ); + } + Vec_PtrFree( vFanout ); + Vec_VecForEachEntry( vGatesAll, pGate, i, k ) + Aig_Regular(pGate)->fMarkA = 0; + return vGatesFull; +} + +/**Function************************************************************* + + Synopsis [Calculates coverage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Cgt_ManComputeCoverage( Aig_Man_t * pAig, Vec_Vec_t * vGates ) +{ + int nFrames = 32; + int nWords = 1; + Ssw_Sml_t * pSml; + Vec_Ptr_t * vOne; + int i, nTransTotal = 0, nTransSaved = 0; + pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords ); + Vec_VecForEachLevel( vGates, vOne, i ) + { + nTransSaved += Ssw_SmlNodeCountOnesRealVec( pSml, vOne ); + nTransTotal += 32 * nFrames * nWords; + } + Ssw_SmlStop( pSml ); + return (float)100.0*nTransSaved/nTransTotal; } /**Function************************************************************* @@ -62,14 +181,18 @@ Vec_Ptr_t * Cgt_ManDecide( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll ) +Vec_Vec_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdcMax, int fVerbose ) { + int nFrames = 32; + int nWords = 1; Ssw_Sml_t * pSml; - Vec_Ptr_t * vGates, * vCands; + Vec_Vec_t * vGates; + Vec_Ptr_t * vCands; Aig_Obj_t * pObjLi, * pObjLo, * pCand, * pCandBest; - int i, k, nHitsCur, nHitsMax; - vGates = Vec_PtrStart( Saig_ManRegNum(pAig) ); - pSml = Ssw_SmlSimulateSeq( pAig, 0, 32, 1 ); + int i, k, nHitsCur, nHitsMax, Counter = 0, clk = clock(); + int nTransTotal = 0, nTransSaved = 0; + vGates = Vec_VecStart( Saig_ManRegNum(pAig) ); + pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords ); Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) { nHitsMax = 0; @@ -78,10 +201,10 @@ Vec_Ptr_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll ) Vec_PtrForEachEntry( vCands, pCand, k ) { // check if this is indeed a clock-gate - if ( !Ssw_SmlCheckXorImplication( pSml, pObjLi, pObjLo, pCand ) ) + if ( nOdcMax == 0 && !Ssw_SmlCheckXorImplication( pSml, pObjLi, pObjLo, pCand ) ) printf( "Clock gate candidate is invalid!\n" ); // find its characteristic number - nHitsCur = Ssw_SmlCountXorImplication( pSml, pObjLi, pObjLo, pCand ); + nHitsCur = Ssw_SmlNodeCountOnesReal( pSml, pCand ); if ( nHitsMax < nHitsCur ) { nHitsMax = nHitsCur; @@ -89,9 +212,80 @@ Vec_Ptr_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll ) } } if ( pCandBest != NULL ) - Vec_PtrWriteEntry( vGates, i, pCandBest ); + { + Vec_VecPush( vGates, i, pCandBest ); + Counter++; + nTransSaved += nHitsMax; + } + nTransTotal += 32 * nFrames * nWords; } Ssw_SmlStop( pSml ); + if ( fVerbose ) + { + printf( "Gating signals = %6d. Gated flops = %6d. (Total flops = %6d.)\n", + Vec_VecSizeSize(vGatesAll), Counter, Saig_ManRegNum(pAig) ); +// printf( "Gated transitions = %5.2f %%. (%5.2f %%.) ", +// 100.0*nTransSaved/nTransTotal, Cgt_ManComputeCoverage(pAig, vGates) ); + printf( "Gated transitions = %5.2f %%. ", Cgt_ManComputeCoverage(pAig, vGates) ); + PRT( "Time", clock() - clk ); + } +/* + { + Vec_Ptr_t * vCompletes; + vCompletes = Cgt_ManCompleteGates( pAig, vGatesAll, nOdcMax, fVerbose ); + printf( "Complete gates = %d. \n", Vec_PtrSize(vCompletes) ); + Vec_PtrFree( vCompletes ); + } +*/ + return vGates; +} + +/**Function************************************************************* + + Synopsis [Computes the set of complete clock gates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Cgt_ManDecideArea( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdcMax, int fVerbose ) +{ + Vec_Vec_t * vGates; + Vec_Ptr_t * vCompletes, * vOne; + Aig_Obj_t * pGate; + int i, k, Counter = 0, clk = clock(); + // derive and label complete gates + vCompletes = Cgt_ManCompleteGates( pAig, vGatesAll, nOdcMax, fVerbose ); + // label complete gates + Vec_PtrForEachEntry( vCompletes, pGate, i ) + Aig_Regular(pGate)->fMarkA = 1; + // select only complete gates + vGates = Vec_VecStart( Saig_ManRegNum(pAig) ); + Vec_VecForEachEntry( vGatesAll, pGate, i, k ) + if ( Aig_Regular(pGate)->fMarkA ) + Vec_VecPush( vGates, i, pGate ); + // unlabel complete gates + Vec_PtrForEachEntry( vCompletes, pGate, i ) + Aig_Regular(pGate)->fMarkA = 0; + // count the number of gated flops + Vec_VecForEachLevel( vGates, vOne, i ) + { + Counter += (int)(Vec_PtrSize(vOne) > 0); +// printf( "%d ", Vec_PtrSize(vOne) ); + } +// printf( "\n" ); + if ( fVerbose ) + { + printf( "Gating signals = %6d. Gated flops = %6d. (Total flops = %6d.)\n", + Vec_VecSizeSize(vGatesAll), Counter, Saig_ManRegNum(pAig) ); + printf( "Complete gates = %6d. Gated transitions = %5.2f %%. ", + Vec_PtrSize(vCompletes), Cgt_ManComputeCoverage(pAig, vGates) ); + PRT( "Time", clock() - clk ); + } + Vec_PtrFree( vCompletes ); return vGates; } diff --git a/src/aig/cgt/cgtInt.h b/src/aig/cgt/cgtInt.h index 7b4b6e63..23d851f3 100644 --- a/src/aig/cgt/cgtInt.h +++ b/src/aig/cgt/cgtInt.h @@ -48,12 +48,16 @@ struct Cgt_Man_t_ // user's data Cgt_Par_t * pPars; // user's parameters Aig_Man_t * pAig; // user's AIG manager - Aig_Man_t * pCare; // user's constraints + // user's constraints + Aig_Man_t * pCare; // constraint cones + Vec_Vec_t * vSuppsInv; // inverse support of the constraints + // result of clock-gating Vec_Vec_t * vGatesAll; // the computed clock-gates Vec_Ptr_t * vGates; // the selected clock-gates // internal data Aig_Man_t * pFrame; // clock gate AIG manager Vec_Ptr_t * vFanout; // temporary storage for fanouts + Vec_Ptr_t * vVisited; // temporary storage for visited nodes // SAT solving Aig_Man_t * pPart; // partition Cnf_Dat_t * pCnf; // CNF of the partition @@ -62,14 +66,21 @@ struct Cgt_Man_t_ int nPatts; // the number of patterns accumulated int nPattWords; // the number of pattern words // statistics + int nRecycles; // recycles int nCalls; // total calls int nCallsSat; // satisfiable calls int nCallsUnsat; // unsatisfiable calls int nCallsUndec; // undecided calls + int nCallsFiltered; // filtered out calls + int timeAig; // constructing AIG + int timePrepare; // partitioning and SAT solving int timeSat; // total runtime int timeSatSat; // satisfiable runtime int timeSatUnsat; // unsatisfiable runtime int timeSatUndec; // undecided runtime + int timeDecision; // making decision about what gates to use + int timeOther; // other runtime + int timeTotal; // total runtime }; //////////////////////////////////////////////////////////////////////// @@ -83,11 +94,11 @@ struct Cgt_Man_t_ /*=== cgtAig.c ==========================================================*/ extern void Cgt_ManDetectCandidates( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands ); extern Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p ); -extern Aig_Man_t * Cgt_ManDupPartition( Aig_Man_t * pAig, int nVarsMin, int nFlopsMin, int iStart ); -extern Aig_Man_t * Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Ptr_t * vGates ); +extern Aig_Man_t * Cgt_ManDupPartition( Aig_Man_t * pAig, int nVarsMin, int nFlopsMin, int iStart, Aig_Man_t * pCare, Vec_Vec_t * vSuppsInv, int * pnOutputs ); +extern Aig_Man_t * Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Vec_t * vGates, int fReduce, int * pnUsedNodes ); /*=== cgtDecide.c ==========================================================*/ -extern Vec_Ptr_t * Cgt_ManDecide( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll ); -extern Vec_Ptr_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll ); +extern Vec_Vec_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdcMax, int fVerbose ); +extern Vec_Vec_t * Cgt_ManDecideArea( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdcMax, int fVerbose ); /*=== cgtMan.c ==========================================================*/ extern Cgt_Man_t * Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars ); extern void Cgt_ManClean( Cgt_Man_t * p ); diff --git a/src/aig/cgt/cgtMan.c b/src/aig/cgt/cgtMan.c index 9615d2e6..a3385228 100644 --- a/src/aig/cgt/cgtMan.c +++ b/src/aig/cgt/cgtMan.c @@ -53,7 +53,19 @@ Cgt_Man_t * Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPar p->pAig = pAig; p->vGatesAll = Vec_VecStart( Saig_ManRegNum(pAig) ); p->vFanout = Vec_PtrAlloc( 1000 ); + p->vVisited = Vec_PtrAlloc( 1000 ); p->nPattWords = 16; + if ( pCare == NULL ) + return p; + // check out the constraints + if ( Aig_ManPiNum(pCare) != Aig_ManPiNum(pAig) ) + { + printf( "The PI count of care (%d) and AIG (%d) differ. Careset is not used.\n", + Aig_ManPiNum(pCare), Aig_ManPiNum(pAig) ); + return p; + } + p->pCare = pCare; + p->vSuppsInv = (Vec_Vec_t *)Aig_ManSupportsInverse( p->pCare ); return p; } @@ -106,27 +118,16 @@ void Cgt_ManClean( Cgt_Man_t * p ) ***********************************************************************/ void Cgt_ManPrintStats( Cgt_Man_t * p ) { + printf( "Params: LevMax = %d. CandMax = %d. OdcMax = %d. ConfMax = %d. VarMin = %d. FlopMin = %d.\n", + p->pPars->nLevelMax, p->pPars->nCandMax, p->pPars->nOdcMax, + p->pPars->nConfMax, p->pPars->nVarsMin, p->pPars->nFlopsMin ); + printf( "SAT : Calls = %d. Unsat = %d. Sat = %d. Fails = %d. Recycles = %d. ", + p->nCalls, p->nCallsUnsat, p->nCallsSat, p->nCallsUndec, p->nRecycles ); + PRT( "Time", p->timeTotal ); /* - double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20); - - printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f Mb.\n", - p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory ); - printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n", - Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), - 0/p->pPars->nIters ); - printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n", - p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Cgt_ManCountEquivs(p) ); - printf( "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n", - p->nVarsMax, p->nCallsMax, p->nRecyclesTotal, p->nSimRounds ); - printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", - p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), - p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) ); - - p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat; - PRTP( "BMC ", p->timeBmc, p->timeTotal ); - PRTP( "Spec reduce", p->timeReduce, p->timeTotal ); - PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal ); - PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal ); + p->timeOther = p->timeTotal-p->timeAig-p->timePrepare-p->timeSat-p->timeDecision; + PRTP( "AIG ", p->timeAig, p->timeTotal ); + PRTP( "Prepare ", p->timePrepare, p->timeTotal ); PRTP( "SAT solving", p->timeSat, p->timeTotal ); PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); PRTP( " sat ", p->timeSatSat, p->timeTotal ); @@ -155,8 +156,13 @@ void Cgt_ManStop( Cgt_Man_t * p ) Aig_ManStop( p->pFrame ); Cgt_ManClean( p ); Vec_PtrFree( p->vFanout ); - Vec_PtrFree( p->vGates ); - Vec_VecFree( p->vGatesAll ); + Vec_PtrFree( p->vVisited ); + if ( p->vGates ) + Vec_PtrFree( p->vGates ); + if ( p->vGatesAll ) + Vec_VecFree( p->vGatesAll ); + if ( p->vSuppsInv ) + Vec_VecFree( p->vSuppsInv ); free( p ); } -- cgit v1.2.3