diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-21 04:30:10 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-21 04:30:10 -0800 |
commit | 8014f25f6db719fa62336f997963532a14c568f6 (patch) | |
tree | c691ee91a3a2d452a2bd24ac89a8c717beaa7af7 /src/proof/ssw/sswDyn.c | |
parent | c44cc5de9429e6b4f1c05045fcf43c9cb96437b5 (diff) | |
download | abc-8014f25f6db719fa62336f997963532a14c568f6.tar.gz abc-8014f25f6db719fa62336f997963532a14c568f6.tar.bz2 abc-8014f25f6db719fa62336f997963532a14c568f6.zip |
Major restructuring of the code.
Diffstat (limited to 'src/proof/ssw/sswDyn.c')
-rw-r--r-- | src/proof/ssw/sswDyn.c | 489 |
1 files changed, 489 insertions, 0 deletions
diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c new file mode 100644 index 00000000..d9a16e22 --- /dev/null +++ b/src/proof/ssw/sswDyn.c @@ -0,0 +1,489 @@ +/**CFile**************************************************************** + + FileName [sswDyn.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Dynamic loading of constraints.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswDyn.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" +#include "src/misc/bar/bar.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Label PIs nodes of the frames corresponding to PIs of AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManLabelPiNodes( Ssw_Man_t * p ) +{ + Aig_Obj_t * pObj, * pObjFrames; + int f, i; + Aig_ManConst1( p->pFrames )->fMarkA = 1; + Aig_ManConst1( p->pFrames )->fMarkB = 1; + for ( f = 0; f < p->nFrames; f++ ) + { + Saig_ManForEachPi( p->pAig, pObj, i ) + { + pObjFrames = Ssw_ObjFrame( p, pObj, f ); + assert( Aig_ObjIsPi(pObjFrames) ); + assert( pObjFrames->fMarkB == 0 ); + pObjFrames->fMarkA = 1; + pObjFrames->fMarkB = 1; + } + } +} + +/**Function************************************************************* + + Synopsis [Collects new POs in p->vNewPos.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( pObj->fMarkA ) + return; + pObj->fMarkA = 1; + if ( Aig_ObjIsPi(pObj) ) + { + Vec_PtrPush( vNewPis, pObj ); + return; + } + assert( Aig_ObjIsNode(pObj) ); + Ssw_ManCollectPis_rec( Aig_ObjFanin0(pObj), vNewPis ); + Ssw_ManCollectPis_rec( Aig_ObjFanin1(pObj), vNewPis ); +} + +/**Function************************************************************* + + Synopsis [Collects new POs in p->vNewPos.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos ) +{ + Aig_Obj_t * pFanout; + int iFanout = -1, i; + assert( !Aig_IsComplement(pObj) ); + if ( pObj->fMarkB ) + return; + pObj->fMarkB = 1; + if ( pObj->Id > p->nSRMiterMaxId ) + return; + if ( Aig_ObjIsPo(pObj) ) + { + // skip if it is a register input PO + if ( Aig_ObjPioNum(pObj) >= Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig) ) + return; + // add the number of this constraint + Vec_IntPush( vNewPos, Aig_ObjPioNum(pObj)/2 ); + return; + } + // visit the fanouts + assert( p->pFrames->pFanData != NULL ); + Aig_ObjForEachFanout( p->pFrames, pObj, pFanout, iFanout, i ) + Ssw_ManCollectPos_rec( p, pFanout, vNewPos ); +} + +/**Function************************************************************* + + Synopsis [Loads logic cones and relevant constraints.] + + Description [Both pRepr and pObj are objects of the AIG. + The result is the current SAT solver loaded with the logic cones + for pRepr and pObj corresponding to them in the frames, + as well as all the relevant constraints.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pObjFrames, * pReprFrames; + Aig_Obj_t * pTemp, * pObj0, * pObj1; + int i, iConstr, RetValue; + + assert( pRepr != pObj ); + // get the corresponding frames nodes + pReprFrames = Aig_Regular( Ssw_ObjFrame( p, pRepr, p->pPars->nFramesK ) ); + pObjFrames = Aig_Regular( Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) ); + assert( pReprFrames != pObjFrames ); + /* + // compute the AIG support + Vec_PtrClear( p->vNewLos ); + Ssw_ManCollectPis_rec( pRepr, p->vNewLos ); + Ssw_ManCollectPis_rec( pObj, p->vNewLos ); + // add logic cones for register outputs + Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i ) + { + pObj0 = Aig_Regular( Ssw_ObjFrame( p, pTemp, p->pPars->nFramesK ) ); + Ssw_CnfNodeAddToSolver( p->pMSat, pObj0 ); + } +*/ + // add cones for the nodes + Ssw_CnfNodeAddToSolver( p->pMSat, pReprFrames ); + Ssw_CnfNodeAddToSolver( p->pMSat, pObjFrames ); + + // compute the frames support + Vec_PtrClear( p->vNewLos ); + Ssw_ManCollectPis_rec( pReprFrames, p->vNewLos ); + Ssw_ManCollectPis_rec( pObjFrames, p->vNewLos ); + // these nodes include both nodes corresponding to PIs and LOs + // (the nodes corresponding to PIs should be labeled with fMarkB!) + + // collect the related constraint POs + Vec_IntClear( p->vNewPos ); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i ) + Ssw_ManCollectPos_rec( p, pTemp, p->vNewPos ); + // check if the corresponding pairs are added + Vec_IntForEachEntry( p->vNewPos, iConstr, i ) + { + pObj0 = Aig_ManPo( p->pFrames, 2*iConstr ); + pObj1 = Aig_ManPo( p->pFrames, 2*iConstr+1 ); +// if ( pObj0->fMarkB && pObj1->fMarkB ) + if ( pObj0->fMarkB || pObj1->fMarkB ) + { + pObj0->fMarkB = 1; + pObj1->fMarkB = 1; + Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj0), Aig_ObjChild0(pObj1) ); + } + } + if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead ) + { + RetValue = sat_solver_simplify(p->pMSat->pSat); + assert( RetValue != 0 ); + } +} + +/**Function************************************************************* + + Synopsis [Tranfers simulation information from FRAIG to AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManSweepTransferDyn( Ssw_Man_t * p ) +{ + Aig_Obj_t * pObj, * pObjFraig; + unsigned * pInfo; + int i, f, nFrames; + + // transfer simulation information + Aig_ManForEachPi( p->pAig, pObj, i ) + { + pObjFraig = Ssw_ObjFrame( p, pObj, 0 ); + if ( pObjFraig == Aig_ManConst0(p->pFrames) ) + { + Ssw_SmlObjAssignConst( p->pSml, pObj, 0, 0 ); + continue; + } + assert( !Aig_IsComplement(pObjFraig) ); + assert( Aig_ObjIsPi(pObjFraig) ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); + Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 ); + } + // set random simulation info for the second frame + for ( f = 1; f < p->nFrames; f++ ) + { + Saig_ManForEachPi( p->pAig, pObj, i ) + { + pObjFraig = Ssw_ObjFrame( p, pObj, f ); + assert( !Aig_IsComplement(pObjFraig) ); + assert( Aig_ObjIsPi(pObjFraig) ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); + Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f ); + } + } + // create random info + nFrames = Ssw_SmlNumFrames( p->pSml ); + for ( ; f < nFrames; f++ ) + { + Saig_ManForEachPi( p->pAig, pObj, i ) + Ssw_SmlAssignRandomFrame( p->pSml, pObj, f ); + } +} + +/**Function************************************************************* + + Synopsis [Performs one round of simulation with counter-examples.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f ) +{ + int RetValue1, RetValue2, clk = clock(); + // transfer PI simulation information from storage +// Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords ); + Ssw_ManSweepTransferDyn( p ); + // simulate internal nodes +// Ssw_SmlSimulateOneFrame( p->pSml ); + Ssw_SmlSimulateOne( p->pSml ); + // check equivalence classes + RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 ); + RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 ); + // prepare simulation info for the next round + Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 ); + p->nPatterns = 0; + p->nSimRounds++; +p->timeSimSat += clock() - clk; + return RetValue1 > 0 || RetValue2 > 0; +} + +/**Function************************************************************* + + Synopsis [Performs one round of simulation with counter-examples.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f ) +{ + Aig_Obj_t * pObj, * pRepr, ** ppClass; + int i, k, nSize, RetValue1, RetValue2, clk = clock(); + p->nSimRounds++; + // transfer PI simulation information from storage +// Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords ); + Ssw_ManSweepTransferDyn( p ); + // determine const1 cands and classes to be simulated + Vec_PtrClear( p->vResimConsts ); + Vec_PtrClear( p->vResimClasses ); + Aig_ManIncrementTravId( p->pAig ); + for ( i = p->iNodeStart; i < p->iNodeLast + p->pPars->nResimDelta; i++ ) + { + if ( i >= Aig_ManObjNumMax( p->pAig ) ) + break; + pObj = Aig_ManObj( p->pAig, i ); + if ( pObj == NULL ) + continue; + if ( Ssw_ObjIsConst1Cand(p->pAig, pObj) ) + { + Vec_PtrPush( p->vResimConsts, pObj ); + continue; + } + pRepr = Aig_ObjRepr(p->pAig, pObj); + if ( pRepr == NULL ) + continue; + if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) ) + continue; + Aig_ObjSetTravIdCurrent(p->pAig, pRepr); + Vec_PtrPush( p->vResimClasses, pRepr ); + } + // simulate internal nodes +// Ssw_SmlSimulateOneFrame( p->pSml ); +// Ssw_SmlSimulateOne( p->pSml ); + // resimulate dynamically +// Aig_ManIncrementTravId( p->pAig ); +// Aig_ObjIsTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) ); + p->nVisCounter++; + Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimConsts, pObj, i ) + Ssw_SmlSimulateOneDyn_rec( p->pSml, pObj, p->nFrames-1, p->pVisited, p->nVisCounter ); + // resimulate the cone of influence of the cand classes + Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i ) + { + ppClass = Ssw_ClassesReadClass( p->ppClasses, pRepr, &nSize ); + for ( k = 0; k < nSize; k++ ) + Ssw_SmlSimulateOneDyn_rec( p->pSml, ppClass[k], p->nFrames-1, p->pVisited, p->nVisCounter ); + } + + // check equivalence classes +// RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 ); +// RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 ); + // refine these nodes + RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vResimConsts, 1 ); + RetValue2 = 0; + Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i ) + RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRepr, 1 ); + + // prepare simulation info for the next round + Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 ); + p->nPatterns = 0; + p->nSimRounds++; +p->timeSimSat += clock() - clk; + return RetValue1 > 0 || RetValue2 > 0; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweepDyn( Ssw_Man_t * p ) +{ + Bar_Progress_t * pProgress = NULL; + Aig_Obj_t * pObj, * pObjNew; + int clk, i, f; + + // perform speculative reduction +clk = clock(); + // create timeframes + p->pFrames = Ssw_FramesWithClasses( p ); + Aig_ManFanoutStart( p->pFrames ); + p->nSRMiterMaxId = Aig_ManObjNumMax( p->pFrames ); + + // map constants and PIs of the last frame + f = p->pPars->nFramesK; + Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); + Saig_ManForEachPi( p->pAig, pObj, i ) + Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); + Aig_ManSetPioNumbers( p->pFrames ); + // label nodes corresponding to primary inputs + Ssw_ManLabelPiNodes( p ); +p->timeReduce += clock() - clk; + + // prepare simulation info + assert( p->vSimInfo == NULL ); + p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 ); + Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 ); + + // sweep internal nodes + p->fRefined = 0; + Ssw_ClassesClearRefined( p->ppClasses ); + if ( p->pPars->fVerbose ) + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) ); + p->iNodeStart = 0; + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( p->iNodeStart == 0 ) + p->iNodeStart = i; + if ( p->pPars->fVerbose ) + Bar_ProgressUpdate( pProgress, i, NULL ); + if ( Saig_ObjIsLo(p->pAig, pObj) ) + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL ); + else if ( Aig_ObjIsNode(pObj) ) + { + pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL ); + } + // check if it is time to recycle the solver + if ( p->pMSat->pSat == NULL || + (p->pPars->nSatVarMax2 && + p->pMSat->nSatVars > p->pPars->nSatVarMax2 && + p->nRecycleCalls > p->pPars->nRecycleCalls2) ) + { + // resimulate + if ( p->nPatterns > 0 ) + { + p->iNodeLast = i; + if ( p->pPars->fLocalSim ) + Ssw_ManSweepResimulateDynLocal( p, f ); + else + Ssw_ManSweepResimulateDyn( p, f ); + p->iNodeStart = i+1; + } +// printf( "Recycling SAT solver with %d vars and %d calls.\n", +// p->pMSat->nSatVars, p->nRecycleCalls ); +// Aig_ManCleanMarkAB( p->pAig ); + Aig_ManCleanMarkAB( p->pFrames ); + // label nodes corresponding to primary inputs + Ssw_ManLabelPiNodes( p ); + // replace the solver + if ( p->pMSat ) + { + p->nVarsMax = Abc_MaxInt( p->nVarsMax, p->pMSat->nSatVars ); + p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls ); + Ssw_SatStop( p->pMSat ); + p->nRecycles++; + p->nRecyclesTotal++; + p->nRecycleCalls = 0; + } + p->pMSat = Ssw_SatStart( 0 ); + assert( p->nPatterns == 0 ); + } + // resimulate + if ( p->nPatterns == 32 ) + { + p->iNodeLast = i; + if ( p->pPars->fLocalSim ) + Ssw_ManSweepResimulateDynLocal( p, f ); + else + Ssw_ManSweepResimulateDyn( p, f ); + p->iNodeStart = i+1; + } + } + // resimulate + if ( p->nPatterns > 0 ) + { + p->iNodeLast = i; + if ( p->pPars->fLocalSim ) + Ssw_ManSweepResimulateDynLocal( p, f ); + else + Ssw_ManSweepResimulateDyn( p, f ); + } + // collect stats + if ( p->pPars->fVerbose ) + Bar_ProgressStop( pProgress ); + + // cleanup +// Ssw_ClassesCheck( p->ppClasses ); + return p->fRefined; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |