diff options
Diffstat (limited to 'src/proof/cec/cecSweep.c')
| -rw-r--r-- | src/proof/cec/cecSweep.c | 299 |
1 files changed, 299 insertions, 0 deletions
diff --git a/src/proof/cec/cecSweep.c b/src/proof/cec/cecSweep.c new file mode 100644 index 00000000..4523810e --- /dev/null +++ b/src/proof/cec/cecSweep.c @@ -0,0 +1,299 @@ +/**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 ); + 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_ObjLevel(p->pAig, pObj) > p->pPars->nLevelMax || + Gia_ObjLevel(p->pAig, pRepr) > 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, clk; +clk = clock(); + vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), pSim->nWords ); +p->timePat += clock() - clk; +clk = clock(); + if ( vInfo != NULL ) + { + Gia_ManSetRefs( 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 += 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 + |