diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-10-04 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-10-04 08:01:00 -0700 |
commit | eb75697fe00a8668f74b3c710dcbf5658e07d167 (patch) | |
tree | 05b78ce8fb95fcc37b013f5bfd9da0dd3544b42a /src/aig/ssw_old/sswSweep.c | |
parent | 689cbe904e3a28d7502feb9931b748764f947aaf (diff) | |
download | abc-eb75697fe00a8668f74b3c710dcbf5658e07d167.tar.gz abc-eb75697fe00a8668f74b3c710dcbf5658e07d167.tar.bz2 abc-eb75697fe00a8668f74b3c710dcbf5658e07d167.zip |
Version abc81004
Diffstat (limited to 'src/aig/ssw_old/sswSweep.c')
-rw-r--r-- | src/aig/ssw_old/sswSweep.c | 473 |
1 files changed, 473 insertions, 0 deletions
diff --git a/src/aig/ssw_old/sswSweep.c b/src/aig/ssw_old/sswSweep.c new file mode 100644 index 00000000..b9d4ad63 --- /dev/null +++ b/src/aig/ssw_old/sswSweep.c @@ -0,0 +1,473 @@ +/**CFile**************************************************************** + + FileName [sswSweep.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [One round of SAT sweeping.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswSweep.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" +#include "bar.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Mark nodes affected by sweep in the previous iteration.] + + Description [Assumes that affected nodes are in p->ppClasses->vRefined.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p ) +{ + Vec_Ptr_t * vRefined, * vSupp; + Aig_Obj_t * pObj, * pObjLo, * pObjLi; + int i, k; + vRefined = Ssw_ClassesGetRefined( p->ppClasses ); + if ( Vec_PtrSize(vRefined) == 0 ) + { + Aig_ManForEachObj( p->pAig, pObj, i ) + pObj->fMarkA = 1; + return; + } + // mark the nodes to be refined + Aig_ManCleanMarkA( p->pAig ); + Vec_PtrForEachEntry( vRefined, pObj, i ) + { + if ( Aig_ObjIsPi(pObj) ) + { + pObj->fMarkA = 1; + continue; + } + assert( Aig_ObjIsNode(pObj) ); + vSupp = Aig_Support( p->pAig, pObj ); + Vec_PtrForEachEntry( vSupp, pObjLo, k ) + pObjLo->fMarkA = 1; + Vec_PtrFree( vSupp ); + } + // mark refinement + Aig_ManForEachNode( p->pAig, pObj, i ) + pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA; + Saig_ManForEachLi( p->pAig, pObj, i ) + pObj->fMarkA |= Aig_ObjFanin0(pObj)->fMarkA; + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + pObjLo->fMarkA |= pObjLi->fMarkA; +} + +/**Function************************************************************* + + Synopsis [Retrives value of the PI in the original AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) +{ + Aig_Obj_t * pObjFraig; + int nVarNum, Value; +// assert( Aig_ObjIsPi(pObj) ); + pObjFraig = Ssw_ObjFrame( p, pObj, f ); + nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) ); + assert( nVarNum > 0 ); + if ( nVarNum == 0 ) + printf( "Variable is not assigned.\n" ); + Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum )); +// Value = (Aig_IsComplement(pObjFraig) ^ ((!nVarNum)? 0 : sat_solver_var_value( p->pSat, nVarNum ))); +// Value = (!nVarNum)? Aig_ManRandom(0) & 1 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum )); + if ( p->pPars->fPolarFlip ) + { + if ( Aig_Regular(pObjFraig)->fPhase ) Value ^= 1; + } + return Value; +} + +/**Function************************************************************* + + Synopsis [Copy pattern from the solver into the internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f ) +{ + Aig_Obj_t * pObj; + int i; + memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); + Aig_ManForEachPi( p->pAig, pObj, i ) + if ( Ssw_ManGetSatVarValue( p, pObj, f ) ) + Aig_InfoSetBit( p->pPatWords, i ); +} + +/**Function************************************************************* + + Synopsis [Copy pattern from the solver into the internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlSavePatternAig2( Ssw_Man_t * p, int f ) +{ + Aig_Obj_t * pObj; + int i; + memset( p->pPatWords2, 0, sizeof(unsigned) * p->nPatWords ); + Aig_ManForEachPi( p->pAig, pObj, i ) + if ( Ssw_ManGetSatVarValue( p, pObj, f ) ) + Aig_InfoSetBit( p->pPatWords2, i ); +} + +/**Function************************************************************* + + Synopsis [Copy pattern from the solver into the internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f ) +{ + Aig_Obj_t * pObj; + int i; + memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); + Aig_ManForEachPi( p->pAig, pObj, i ) + if ( Aig_ObjPhaseReal( Ssw_ObjFrame(p, pObj, f) ) ) + Aig_InfoSetBit( p->pPatWords, i ); +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) +{ + Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; + int RetValue; + // get representative of this class + pObjRepr = Aig_ObjRepr( p->pAig, pObj ); + if ( pObjRepr == NULL ) + return 0; + // get the fraiged node + pObjFraig = Ssw_ObjFrame( p, pObj, f ); + // get the fraiged representative + pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f ); + // check if constant 0 pattern distinquishes these nodes + assert( pObjFraig != NULL && pObjReprFraig != NULL ); + if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) ) + { + p->nStrangers++; + Ssw_SmlSavePatternAigPhase( p, f ); + } + else + { + // if the fraiged nodes are the same, return + if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) + return 0; + // count the number of skipped calls + if ( !pObj->fMarkA && !pObjRepr->fMarkA ) + p->nRefSkip++; + else + p->nRefUse++; + // call equivalence checking + if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA ) + RetValue = 1; + else if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) ) + RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); + else + RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) ); + if ( RetValue == 1 ) // proved equivalent + { + pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); + Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 ); + return 0; + } + if ( RetValue == -1 ) // timed out + { + Ssw_ClassesRemoveNode( p->ppClasses, pObj ); + return 1; + } + // check if skipping calls works correctly + if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA ) + { + assert( 0 ); + printf( "\nSsw_ManSweepNode(): Error!\n" ); + } + // disproved the equivalence + Ssw_SmlSavePatternAig( p, f ); + } + if ( !fBmc && p->pPars->fUniqueness && p->pPars->nFramesK > 1 && + Ssw_ManUniqueOne( p, pObjRepr, pObj ) && p->iOutputLit == -1 ) + { + if ( Ssw_ManUniqueAddConstraint( p, p->vCommon, 0, 1 ) ) + { + int RetValue2 = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); + p->iOutputLit = -1; + + { + int Flag = 0; + if ( Flag ) + { + Aig_Obj_t * pFan0 = Aig_ObjFanin0(pObj); + Aig_Obj_t * pFan1 = Aig_ObjFanin1(pObj); + Aig_Obj_t * pFan00 = Aig_ObjFanin0(pFan0); + Aig_Obj_t * pFan01 = Aig_ObjFanin1(pFan0); + Aig_Obj_t * pFan10 = Aig_ObjFanin0(pFan1); + Aig_Obj_t * pFan11 = Aig_ObjFanin1(pFan1); + } + } + + if ( RetValue2 == 0 ) + { + int x = Ssw_ManUniqueOne( p, pObjRepr, pObj ); +// Ssw_SmlSavePatternAig2( p, f ); +// Ssw_ManResimulateWord2( p, pObj, pObjRepr, f ); + Ssw_SmlSavePatternAig( p, f ); + Ssw_ManResimulateWord( p, pObj, pObjRepr, f ); + if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr ) + printf( "Ssw_ManSweepNode(): Refinement did not happen!!!!!!!!!!!!!!!!!!!!.\n" ); + return 1; + } + return 0; + + +/* + int RetValue; + assert( p->iOutputLit > -1 ); + RetValue = Ssw_ManSweepNode( p, pObj, f, 0 ); + p->iOutputLit = -1; + return RetValue; +*/ + } + } + if ( p->pPars->nConstrs == 0 ) + Ssw_ManResimulateWord( p, pObj, pObjRepr, f ); + else + Ssw_ManResimulateBit( p, pObj, pObjRepr ); + assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); + if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr ) + printf( "Ssw_ManSweepNode(): Refinement did not happen.\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweepBmc( Ssw_Man_t * p ) +{ + Bar_Progress_t * pProgress = NULL; + Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo; + int i, f, clk; +clk = clock(); + + // start initialized timeframes + p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); + Saig_ManForEachLo( p->pAig, pObj, i ) + Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) ); + + // sweep internal nodes + p->fRefined = 0; + if ( p->pPars->fVerbose ) + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); + Ssw_ManStartSolver( p ); + for ( f = 0; f < p->pPars->nFramesK; f++ ) + { + // map constants and PIs + Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); + Saig_ManForEachPi( p->pAig, pObj, i ) + { + pObjNew = Aig_ObjCreatePi(p->pFrames); + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); + Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) ); + } + // sweep internal nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + { + if ( p->pPars->fVerbose ) + Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL ); + 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, 1 ); + } + // quit if this is the last timeframe + if ( f == p->pPars->nFramesK - 1 ) + break; + // transfer latch input to the latch outputs + // build logic cones for register outputs + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + { + pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f); + Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew ); + Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) ); + } + } + if ( p->pPars->fVerbose ) + Bar_ProgressStop( pProgress ); + + // cleanup +// Ssw_ClassesCheck( p->ppClasses ); +p->timeBmc += clock() - clk; + return p->fRefined; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweep( Ssw_Man_t * p ) +{ + Bar_Progress_t * pProgress = NULL; + Aig_Obj_t * pObj, * pObj2, * pObjNew; + int nConstrPairs, clk, i, f; + int v; + + // perform speculative reduction +clk = clock(); + // create timeframes + p->pFrames = Ssw_FramesWithClasses( p ); + // add constraints + Ssw_ManStartSolver( p ); +// nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig); + nConstrPairs = Aig_ManPoNum(p->pFrames)-p->nFrames*Aig_ManRegNum(p->pAig); + assert( (nConstrPairs & 1) == 0 ); + for ( i = 0; i < nConstrPairs; i += 2 ) + { + pObj = Aig_ManPo( p->pFrames, i ); + pObj2 = Aig_ManPo( p->pFrames, i+1 ); + Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) ); + } +/* + // build logic cones for register inputs + for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) + { + pObj = Aig_ManPo( p->pFrames, nConstrPairs + i ); + Ssw_CnfNodeAddToSolver( p, Aig_ObjFanin0(pObj) ); + } +*/ +p->timeReduce += clock() - clk; + + // mark nodes that do not have to be refined +clk = clock(); + if ( p->pPars->fSkipCheck ) + Ssw_ManSweepMarkRefinement( p ); +p->timeMarkCones += clock() - clk; + +//Ssw_ManUnique( p ); + + // 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) ); +//// + // bring up the previous frames +// if ( p->pPars->fUniqueness ) + for ( v = 0; v <= f; v++ ) +// Saig_ManForEachLo( p->pAig, pObj, i ) + Aig_ManForEachPi( p->pAig, pObj, i ) + { +/* + if ( i == 53 && v == 1 ) + { + int x = 0; + } +*/ + Ssw_CnfNodeAddToSolver( p, Aig_Regular(Ssw_ObjFrame(p, pObj, v)) ); + } +//// + sat_solver_simplify( p->pSat ); + // make sure LOs are assigned + Saig_ManForEachLo( p->pAig, pObj, i ) + assert( Ssw_ObjFrame( p, pObj, f ) != NULL ); + // sweep internal nodes + p->fRefined = 0; + p->nSatFailsReal = 0; + p->nRefUse = p->nRefSkip = 0; + p->nUniques = 0; + Ssw_ClassesClearRefined( p->ppClasses ); + if ( p->pPars->fVerbose ) + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) ); + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( p->pPars->fVerbose ) + Bar_ProgressUpdate( pProgress, i, NULL ); + if ( Saig_ObjIsLo(p->pAig, pObj) ) + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 ); + else if ( Aig_ObjIsNode(pObj) ) + { + pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA; + 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 ); + } + } + p->nSatFailsTotal += p->nSatFailsReal; + if ( p->pPars->fVerbose ) + Bar_ProgressStop( pProgress ); + + // cleanup +// Ssw_ClassesCheck( p->ppClasses ); + return p->fRefined; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |