| /**CFile**************************************************************** |
| |
| FileName [sswSemi.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Inductive prover with constraints.] |
| |
| Synopsis [Semiformal for equivalence classes.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - September 1, 2008.] |
| |
| Revision [$Id: sswSemi.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "sswInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| typedef struct Ssw_Sem_t_ Ssw_Sem_t; // BMC manager |
| |
| struct Ssw_Sem_t_ |
| { |
| // parameters |
| int nConfMaxStart; // the starting conflict limit |
| int nConfMax; // the intermediate conflict limit |
| int nFramesSweep; // the number of frames to sweep |
| int fVerbose; // prints output statistics |
| // equivalences considered |
| Ssw_Man_t * pMan; // SAT sweeping manager |
| Vec_Ptr_t * vTargets; // the nodes that are watched |
| // storage for patterns |
| int nPatternsAlloc; // the max number of interesting states |
| int nPatterns; // the number of patterns |
| Vec_Ptr_t * vPatterns; // storage for the interesting states |
| Vec_Int_t * vHistory; // what state and how many steps |
| }; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose ) |
| { |
| Ssw_Sem_t * p; |
| Aig_Obj_t * pObj; |
| int i; |
| // create interpolation manager |
| p = ABC_ALLOC( Ssw_Sem_t, 1 ); |
| memset( p, 0, sizeof(Ssw_Sem_t) ); |
| p->nConfMaxStart = nConfMax; |
| p->nConfMax = nConfMax; |
| p->nFramesSweep = Abc_MaxInt( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames ); |
| p->fVerbose = fVerbose; |
| // equivalences considered |
| p->pMan = pMan; |
| p->vTargets = Vec_PtrAlloc( Saig_ManPoNum(p->pMan->pAig) ); |
| Saig_ManForEachPo( p->pMan->pAig, pObj, i ) |
| Vec_PtrPush( p->vTargets, Aig_ObjFanin0(pObj) ); |
| // storage for patterns |
| p->nPatternsAlloc = 512; |
| p->nPatterns = 1; |
| p->vPatterns = Vec_PtrAllocSimInfo( Aig_ManRegNum(p->pMan->pAig), Abc_BitWordNum(p->nPatternsAlloc) ); |
| Vec_PtrCleanSimInfo( p->vPatterns, 0, Abc_BitWordNum(p->nPatternsAlloc) ); |
| p->vHistory = Vec_IntAlloc( 100 ); |
| Vec_IntPush( p->vHistory, 0 ); |
| // update arrays of the manager |
| assert( 0 ); |
| /* |
| ABC_FREE( p->pMan->pNodeToFrames ); |
| Vec_IntFree( p->pMan->vSatVars ); |
| p->pMan->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep ); |
| p->pMan->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) ); |
| */ |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ssw_SemManStop( Ssw_Sem_t * p ) |
| { |
| Vec_PtrFree( p->vTargets ); |
| Vec_PtrFree( p->vPatterns ); |
| Vec_IntFree( p->vHistory ); |
| ABC_FREE( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ssw_SemCheckTargets( Ssw_Sem_t * p ) |
| { |
| Aig_Obj_t * pObj; |
| int i; |
| Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i ) |
| if ( !Ssw_ObjIsConst1Cand(p->pMan->pAig, pObj) ) |
| return 1; |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ssw_ManFilterBmcSavePattern( Ssw_Sem_t * p ) |
| { |
| unsigned * pInfo; |
| Aig_Obj_t * pObj; |
| int i; |
| if ( p->nPatterns >= p->nPatternsAlloc ) |
| return; |
| Saig_ManForEachLo( p->pMan->pAig, pObj, i ) |
| { |
| pInfo = (unsigned *)Vec_PtrEntry( p->vPatterns, i ); |
| if ( Abc_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) ) |
| Abc_InfoSetBit( pInfo, p->nPatterns ); |
| } |
| p->nPatterns++; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs fraiging for the internal nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ssw_ManFilterBmc( Ssw_Sem_t * pBmc, int iPat, int fCheckTargets ) |
| { |
| Ssw_Man_t * p = pBmc->pMan; |
| Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo; |
| unsigned * pInfo; |
| int i, f, RetValue, fFirst = 0; |
| abctime clk; |
| clk = Abc_Clock(); |
| |
| // start initialized timeframes |
| p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 ); |
| Saig_ManForEachLo( p->pAig, pObj, i ) |
| { |
| pInfo = (unsigned *)Vec_PtrEntry( pBmc->vPatterns, i ); |
| pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Abc_InfoHasBit(pInfo, iPat) ); |
| Ssw_ObjSetFrame( p, pObj, 0, pObjNew ); |
| } |
| |
| // sweep internal nodes |
| RetValue = pBmc->nFramesSweep; |
| for ( f = 0; f < pBmc->nFramesSweep; f++ ) |
| { |
| // map constants and PIs |
| Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); |
| Saig_ManForEachPi( p->pAig, pObj, i ) |
| Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) ); |
| // sweep internal nodes |
| Aig_ManForEachNode( p->pAig, pObj, i ) |
| { |
| pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); |
| Ssw_ObjSetFrame( p, pObj, f, pObjNew ); |
| if ( Ssw_ManSweepNode( p, pObj, f, 1, NULL ) ) |
| { |
| Ssw_ManFilterBmcSavePattern( pBmc ); |
| if ( fFirst == 0 ) |
| { |
| fFirst = 1; |
| pBmc->nConfMax *= 10; |
| } |
| } |
| if ( f > 0 && p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax ) |
| { |
| RetValue = -1; |
| break; |
| } |
| } |
| // quit if this is the last timeframe |
| if ( p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax ) |
| { |
| RetValue += f + 1; |
| break; |
| } |
| if ( fCheckTargets && Ssw_SemCheckTargets( pBmc ) ) |
| 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->pMSat, Aig_Regular(pObjNew) ); |
| } |
| //Abc_Print( 1, "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts ); |
| } |
| if ( fFirst ) |
| pBmc->nConfMax /= 10; |
| |
| // cleanup |
| Ssw_ClassesCheck( p->ppClasses ); |
| p->timeBmc += Abc_Clock() - clk; |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if one of the targets has failed.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose ) |
| { |
| Ssw_Sem_t * p; |
| int RetValue, Frames, Iter; |
| abctime clk = Abc_Clock(); |
| p = Ssw_SemManStart( pMan, nConfMax, fVerbose ); |
| if ( fCheckTargets && Ssw_SemCheckTargets( p ) ) |
| { |
| assert( 0 ); |
| Ssw_SemManStop( p ); |
| return 1; |
| } |
| if ( fVerbose ) |
| { |
| Abc_Print( 1, "AIG : C = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n", |
| Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), |
| Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep ); |
| } |
| RetValue = 0; |
| for ( Iter = 0; Iter < p->nPatterns; Iter++ ) |
| { |
| clk = Abc_Clock(); |
| pMan->pMSat = Ssw_SatStart( 0 ); |
| Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets ); |
| if ( fVerbose ) |
| { |
| Abc_Print( 1, "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ", |
| Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), |
| Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns, |
| p->pMan->nSatFailsReal? "f" : " " ); |
| ABC_PRT( "T", Abc_Clock() - clk ); |
| } |
| Ssw_ManCleanup( p->pMan ); |
| if ( fCheckTargets && Ssw_SemCheckTargets( p ) ) |
| { |
| Abc_Print( 1, "Target is hit!!!\n" ); |
| RetValue = 1; |
| } |
| if ( p->nPatterns >= p->nPatternsAlloc ) |
| break; |
| } |
| Ssw_SemManStop( p ); |
| |
| pMan->nStrangers = 0; |
| pMan->nSatCalls = 0; |
| pMan->nSatProof = 0; |
| pMan->nSatFailsReal = 0; |
| pMan->nSatCallsUnsat = 0; |
| pMan->nSatCallsSat = 0; |
| pMan->timeSimSat = 0; |
| pMan->timeSat = 0; |
| pMan->timeSatSat = 0; |
| pMan->timeSatUnsat = 0; |
| pMan->timeSatUndec = 0; |
| return RetValue; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
