| /**CFile**************************************************************** |
| |
| FileName [cecSweep.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Combinational equivalence checking.] |
| |
| Synopsis [SAT sweeping manager.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: cecSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "cecInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs limited speculative reduction.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ) |
| { |
| Gia_Man_t * pNew, * pTemp; |
| Gia_Obj_t * pObj, * pRepr = NULL; |
| int iRes0, iRes1, iRepr, iNode, iMiter; |
| int i, fCompl, * piCopies, * pDepths; |
| Gia_ManSetPhase( p->pAig ); |
| Vec_IntClear( p->vXorNodes ); |
| if ( p->pPars->nLevelMax ) |
| Gia_ManLevelNum( p->pAig ); |
| pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) ); |
| pNew->pName = Abc_UtilStrsav( p->pAig->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pAig->pName ); |
| Gia_ManHashAlloc( pNew ); |
| piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) ); |
| pDepths = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) ); |
| piCopies[0] = 0; |
| Gia_ManForEachObj1( p->pAig, pObj, i ) |
| { |
| if ( Gia_ObjIsCi(pObj) ) |
| { |
| piCopies[i] = Gia_ManAppendCi( pNew ); |
| continue; |
| } |
| if ( Gia_ObjIsCo(pObj) ) |
| continue; |
| if ( piCopies[Gia_ObjFaninId0(pObj,i)] == -1 || |
| piCopies[Gia_ObjFaninId1(pObj,i)] == -1 ) |
| continue; |
| iRes0 = Abc_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) ); |
| iRes1 = Abc_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) ); |
| iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 ); |
| pDepths[i] = Abc_MaxInt( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] ); |
| if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID || Gia_ObjFailed(p->pAig, i) ) |
| continue; |
| assert( Gia_ObjRepr(p->pAig, i) < i ); |
| iRepr = piCopies[Gia_ObjRepr(p->pAig, i)]; |
| if ( iRepr == -1 ) |
| continue; |
| if ( Abc_LitRegular(iNode) == Abc_LitRegular(iRepr) ) |
| continue; |
| if ( p->pPars->nLevelMax && |
| (Gia_ObjLevelId(p->pAig, i) > p->pPars->nLevelMax || |
| Gia_ObjLevelId(p->pAig, Abc_Lit2Var(iRepr)) > p->pPars->nLevelMax) ) |
| continue; |
| if ( p->pPars->fDualOut ) |
| { |
| // if ( i % 1000 == 0 && Gia_ObjRepr(p->pAig, i) ) |
| // Gia_ManEquivPrintOne( p->pAig, Gia_ObjRepr(p->pAig, i), 0 ); |
| if ( p->pPars->fColorDiff ) |
| { |
| if ( !Gia_ObjDiffColors( p->pAig, Gia_ObjRepr(p->pAig, i), i ) ) |
| continue; |
| } |
| else |
| { |
| if ( !Gia_ObjDiffColors2( p->pAig, Gia_ObjRepr(p->pAig, i), i ) ) |
| continue; |
| } |
| } |
| pRepr = Gia_ManObj( p->pAig, Gia_ObjRepr(p->pAig, i) ); |
| fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr); |
| piCopies[i] = Abc_LitNotCond( iRepr, fCompl ); |
| if ( Gia_ObjProved(p->pAig, i) ) |
| continue; |
| // produce speculative miter |
| iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] ); |
| Gia_ManAppendCo( pNew, iMiter ); |
| Vec_IntPush( p->vXorNodes, Gia_ObjRepr(p->pAig, i) ); |
| Vec_IntPush( p->vXorNodes, i ); |
| // add to the depth of this node |
| pDepths[i] = 1 + Abc_MaxInt( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] ); |
| if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax ) |
| piCopies[i] = -1; |
| } |
| ABC_FREE( piCopies ); |
| ABC_FREE( pDepths ); |
| Gia_ManHashStop( pNew ); |
| Gia_ManSetRegNum( pNew, 0 ); |
| pNew = Gia_ManCleanup( pTemp = pNew ); |
| Gia_ManStop( pTemp ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Cec_ManFraClassesUpdate_rec( Gia_Obj_t * pObj ) |
| { |
| int Result; |
| if ( pObj->fMark0 ) |
| return 1; |
| if ( Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj) ) |
| return 0; |
| Result = (Cec_ManFraClassesUpdate_rec( Gia_ObjFanin0(pObj) ) | |
| Cec_ManFraClassesUpdate_rec( Gia_ObjFanin1(pObj) )); |
| return pObj->fMark0 = Result; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates simulation info for this round.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Cec_ManFraCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vCiInfo, Vec_Ptr_t * vInfo, int nSeries ) |
| { |
| unsigned * pRes0, * pRes1; |
| int i, w; |
| for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) |
| { |
| pRes0 = (unsigned *)Vec_PtrEntry( vCiInfo, i ); |
| pRes1 = (unsigned *)Vec_PtrEntry( vInfo, i ); |
| pRes1 += p->nWords * nSeries; |
| for ( w = 0; w < p->nWords; w++ ) |
| pRes0[w] = pRes1[w]; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Updates equivalence classes using the patterns.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew ) |
| { |
| Vec_Ptr_t * vInfo; |
| Gia_Obj_t * pObj, * pObjOld, * pReprOld; |
| int i, k, iRepr, iNode; |
| abctime clk; |
| clk = Abc_Clock(); |
| vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), pSim->nWords ); |
| p->timePat += Abc_Clock() - clk; |
| clk = Abc_Clock(); |
| if ( vInfo != NULL ) |
| { |
| Gia_ManCreateValueRefs( p->pAig ); |
| for ( i = 0; i < pPat->nSeries; i++ ) |
| { |
| Cec_ManFraCreateInfo( pSim, pSim->vCiSimInfo, vInfo, i ); |
| if ( Cec_ManSimSimulateRound( pSim, pSim->vCiSimInfo, pSim->vCoSimInfo ) ) |
| { |
| Vec_PtrFree( vInfo ); |
| return 1; |
| } |
| } |
| Vec_PtrFree( vInfo ); |
| } |
| p->timeSim += Abc_Clock() - clk; |
| assert( Vec_IntSize(p->vXorNodes) == 2*Gia_ManCoNum(pNew) ); |
| // mark the transitive fanout of failed nodes |
| if ( p->pPars->nDepthMax != 1 ) |
| { |
| Gia_ManCleanMark0( p->pAig ); |
| Gia_ManCleanMark1( p->pAig ); |
| Gia_ManForEachCo( pNew, pObj, k ) |
| { |
| iRepr = Vec_IntEntry( p->vXorNodes, 2*k ); |
| iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 ); |
| if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved |
| continue; |
| // Gia_ManObj(p->pAig, iRepr)->fMark0 = 1; |
| Gia_ManObj(p->pAig, iNode)->fMark0 = 1; |
| } |
| // mark the nodes reachable through the failed nodes |
| Gia_ManForEachAnd( p->pAig, pObjOld, k ) |
| pObjOld->fMark0 |= (Gia_ObjFanin0(pObjOld)->fMark0 | Gia_ObjFanin1(pObjOld)->fMark0); |
| // unmark the disproved nodes |
| Gia_ManForEachCo( pNew, pObj, k ) |
| { |
| iRepr = Vec_IntEntry( p->vXorNodes, 2*k ); |
| iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 ); |
| if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved |
| continue; |
| pObjOld = Gia_ManObj(p->pAig, iNode); |
| assert( pObjOld->fMark0 == 1 ); |
| if ( Gia_ObjFanin0(pObjOld)->fMark0 == 0 && Gia_ObjFanin1(pObjOld)->fMark0 == 0 ) |
| pObjOld->fMark1 = 1; |
| } |
| // clean marks |
| Gia_ManForEachAnd( p->pAig, pObjOld, k ) |
| if ( pObjOld->fMark1 ) |
| { |
| pObjOld->fMark0 = 0; |
| pObjOld->fMark1 = 0; |
| } |
| } |
| // set the results |
| p->nAllProved = p->nAllDisproved = p->nAllFailed = 0; |
| Gia_ManForEachCo( pNew, pObj, k ) |
| { |
| iRepr = Vec_IntEntry( p->vXorNodes, 2*k ); |
| iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 ); |
| pReprOld = Gia_ManObj(p->pAig, iRepr); |
| pObjOld = Gia_ManObj(p->pAig, iNode); |
| if ( pObj->fMark1 ) |
| { // proved |
| assert( pObj->fMark0 == 0 ); |
| assert( !Gia_ObjProved(p->pAig, iNode) ); |
| if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 ) |
| // if ( pObjOld->fMark0 == 0 ) |
| { |
| assert( iRepr == Gia_ObjRepr(p->pAig, iNode) ); |
| Gia_ObjSetProved( p->pAig, iNode ); |
| p->nAllProved++; |
| } |
| } |
| else if ( pObj->fMark0 ) |
| { // disproved |
| assert( pObj->fMark1 == 0 ); |
| if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 ) |
| // if ( pObjOld->fMark0 == 0 ) |
| { |
| if ( iRepr == Gia_ObjRepr(p->pAig, iNode) ) |
| Abc_Print( 1, "Cec_ManFraClassesUpdate(): Error! Node is not refined!\n" ); |
| p->nAllDisproved++; |
| } |
| } |
| else |
| { // failed |
| assert( pObj->fMark0 == 0 ); |
| assert( pObj->fMark1 == 0 ); |
| assert( !Gia_ObjFailed(p->pAig, iNode) ); |
| assert( !Gia_ObjProved(p->pAig, iNode) ); |
| Gia_ObjSetFailed( p->pAig, iNode ); |
| p->nAllFailed++; |
| } |
| } |
| return 0; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
