diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-10-13 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-10-13 08:01:00 -0700 |
commit | e917dda1d363cf56274d0595c97cecf3c59eca75 (patch) | |
tree | 597e60685df29a7ae91574140900f97b4ba0d4cc /src/aig/ssw | |
parent | a2535d49a0dac5bad8d27567ad674adc78edf74b (diff) | |
download | abc-e917dda1d363cf56274d0595c97cecf3c59eca75.tar.gz abc-e917dda1d363cf56274d0595c97cecf3c59eca75.tar.bz2 abc-e917dda1d363cf56274d0595c97cecf3c59eca75.zip |
Version abc81013
Diffstat (limited to 'src/aig/ssw')
-rw-r--r-- | src/aig/ssw/module.make | 1 | ||||
-rw-r--r-- | src/aig/ssw/ssw.h | 6 | ||||
-rw-r--r-- | src/aig/ssw/sswAig.c | 50 | ||||
-rw-r--r-- | src/aig/ssw/sswBmc.c | 350 | ||||
-rw-r--r-- | src/aig/ssw/sswCnf.c | 124 | ||||
-rw-r--r-- | src/aig/ssw/sswCore.c | 58 | ||||
-rw-r--r-- | src/aig/ssw/sswInt.h | 62 | ||||
-rw-r--r-- | src/aig/ssw/sswLcorr.c | 57 | ||||
-rw-r--r-- | src/aig/ssw/sswMan.c | 59 | ||||
-rw-r--r-- | src/aig/ssw/sswSat.c | 74 | ||||
-rw-r--r-- | src/aig/ssw/sswSemi.c | 318 | ||||
-rw-r--r-- | src/aig/ssw/sswSim.c | 39 | ||||
-rw-r--r-- | src/aig/ssw/sswSweep.c | 183 | ||||
-rw-r--r-- | src/aig/ssw/sswUnique.c | 155 |
14 files changed, 891 insertions, 645 deletions
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make index 625d72d1..915f7dd0 100644 --- a/src/aig/ssw/module.make +++ b/src/aig/ssw/module.make @@ -8,6 +8,7 @@ SRC += src/aig/ssw/sswAig.c \ src/aig/ssw/sswPart.c \ src/aig/ssw/sswPairs.c \ src/aig/ssw/sswSat.c \ + src/aig/ssw/sswSemi.c \ src/aig/ssw/sswSim.c \ src/aig/ssw/sswSimSat.c \ src/aig/ssw/sswSweep.c \ diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 2785bca6..2d067a17 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -50,8 +50,8 @@ struct Ssw_Pars_t_ int nBTLimit; // conflict limit at a node int nBTLimitGlobal;// conflict limit for multiple runs int nMinDomSize; // min clock domain considered for optimization + int nItersStop; // stop after the given number of iterations int fPolarFlip; // uses polarity adjustment - int fSkipCheck; // do not run equivalence check for unaffected cones int fLatchCorr; // perform register correspondence int fSemiFormal; // enable semiformal filtering int fUniqueness; // enable uniqueness constraints @@ -88,13 +88,13 @@ struct Ssw_Cex_t_ /*=== sswAbs.c ==========================================================*/ extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose ); +/*=== sswBmc.c ==========================================================*/ +extern int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame ); /*=== sswCore.c ==========================================================*/ extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ); extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p ); extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); -/*=== sswLoc.c ==========================================================*/ -extern int Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose ); /*=== sswMiter.c ===================================================*/ extern int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose ); /*=== sswPart.c ==========================================================*/ diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c index 0d0fdbee..fda05941 100644 --- a/src/aig/ssw/sswAig.c +++ b/src/aig/ssw/sswAig.c @@ -30,6 +30,50 @@ /**Function************************************************************* + Synopsis [Starts the SAT manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig ) +{ + Ssw_Frm_t * p; + p = ALLOC( Ssw_Frm_t, 1 ); + memset( p, 0, sizeof(Ssw_Frm_t) ); + p->pAig = pAig; + p->nObjs = Aig_ManObjNumMax( pAig ); + p->nFrames = 0; + p->pFrames = NULL; + p->vAig2Frm = Vec_PtrAlloc( 0 ); + Vec_PtrFill( p->vAig2Frm, 2 * p->nObjs, NULL ); + return p; +} + +/**Function************************************************************* + + Synopsis [Starts the SAT manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_FrmStop( Ssw_Frm_t * p ) +{ + if ( p->pFrames ) + Aig_ManStop( p->pFrames ); + Vec_PtrFree( p->vAig2Frm ); + free( p ); +} + +/**Function************************************************************* + Synopsis [Performs speculative reduction for one node.] Description [] @@ -164,7 +208,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ) assert( Aig_ManRegNum(p->pAig) > 0 ); assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); p->nConstrTotal = p->nConstrReduced = 0; - + // start the fraig package pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames ); // map constants and PIs @@ -190,8 +234,8 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ) // remove dangling nodes Aig_ManCleanup( pFrames ); Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) ); - printf( "SpecRed: Total constraints = %d. Reduced constraints = %d.\n", - p->nConstrTotal, p->nConstrReduced ); +// printf( "SpecRed: Total constraints = %d. Reduced constraints = %d.\n", +// p->nConstrTotal, p->nConstrReduced ); return pFrames; } diff --git a/src/aig/ssw/sswBmc.c b/src/aig/ssw/sswBmc.c index e2d47440..93859c01 100644 --- a/src/aig/ssw/sswBmc.c +++ b/src/aig/ssw/sswBmc.c @@ -6,7 +6,7 @@ PackageName [Inductive prover with constraints.] - Synopsis [Bounded model checker for equivalence clases.] + Synopsis [Bounded model checker using dynamic unrolling.] Author [Alan Mishchenko] @@ -24,32 +24,13 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -typedef struct Ssw_Bmc_t_ Ssw_Bmc_t; // BMC manager - -struct Ssw_Bmc_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 [] + Synopsis [Incrementally unroll the timeframes.] Description [] @@ -58,60 +39,43 @@ struct Ssw_Bmc_t_ SeeAlso [] ***********************************************************************/ -Ssw_Bmc_t * Ssw_BmcManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose ) +Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f ) { - Ssw_Bmc_t * p; - Aig_Obj_t * pObj; - int i; - // create interpolation manager - p = ALLOC( Ssw_Bmc_t, 1 ); - memset( p, 0, sizeof(Ssw_Bmc_t) ); - p->nConfMaxStart = nConfMax; - p->nConfMax = nConfMax; - p->nFramesSweep = AIG_MAX( (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), Aig_BitWordNum(p->nPatternsAlloc) ); - Vec_PtrCleanSimInfo( p->vPatterns, 0, Aig_BitWordNum(p->nPatternsAlloc) ); - p->vHistory = Vec_IntAlloc( 100 ); - Vec_IntPush( p->vHistory, 0 ); - // update arrays of the manager - free( p->pMan->pNodeToFrames ); - Vec_IntFree( p->pMan->vSatVars ); - p->pMan->pNodeToFrames = 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_BmcManStop( Ssw_Bmc_t * p ) -{ - Vec_PtrFree( p->vTargets ); - Vec_PtrFree( p->vPatterns ); - Vec_IntFree( p->vHistory ); - free( p ); + Aig_Obj_t * pRes, * pRes0, * pRes1; + if ( (pRes = Ssw_ObjFrame_(pFrm, pObj, f)) ) + return pRes; + if ( Aig_ObjIsConst1(pObj) ) + pRes = Aig_ManConst1( pFrm->pFrames ); + else if ( Saig_ObjIsPi(pFrm->pAig, pObj) ) + pRes = Aig_ObjCreatePi( pFrm->pFrames ); + else if ( Aig_ObjIsPo(pObj) ) + { + Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f ); + pRes = Ssw_ObjChild0Fra_( pFrm, pObj, f ); + } + else if ( Saig_ObjIsLo(pFrm->pAig, pObj) ) + { + if ( f == 0 ) + pRes = Aig_ManConst0( pFrm->pFrames ); + else + pRes = Ssw_BmcUnroll_rec( pFrm, Saig_ObjLoToLi(pFrm->pAig, pObj), f-1 ); + } + else + { + assert( Aig_ObjIsNode(pObj) ); + Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f ); + Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin1(pObj), f ); + pRes0 = Ssw_ObjChild0Fra_( pFrm, pObj, f ); + pRes1 = Ssw_ObjChild1Fra_( pFrm, pObj, f ); + pRes = Aig_And( pFrm->pFrames, pRes0, pRes1 ); + } + Ssw_ObjSetFrame_( pFrm, pObj, f, pRes ); + return pRes; } /**Function************************************************************* - Synopsis [] + Synopsis [Derives counter-example.] Description [] @@ -120,46 +84,34 @@ void Ssw_BmcManStop( Ssw_Bmc_t * p ) SeeAlso [] ***********************************************************************/ -int Ssw_BmcCheckTargets( Ssw_Bmc_t * p ) +Ssw_Cex_t * Ssw_BmcGetCounterExample( Ssw_Frm_t * pFrm, Ssw_Sat_t * pSat, int iPo, int iFrame ) { - Aig_Obj_t * pObj; - int i; - Vec_PtrForEachEntry( p->vTargets, pObj, i ) - if ( !Ssw_ObjIsConst1Cand(p->pMan->pAig, pObj) ) - return 1; - return 0; + Ssw_Cex_t * pCex; + Aig_Obj_t * pObj, * pObjFrames; + int f, i, nShift; + assert( Saig_ManRegNum(pFrm->pAig) > 0 ); + // allocate the counter example + pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pFrm->pAig), Saig_ManPiNum(pFrm->pAig), iFrame + 1 ); + pCex->iPo = iPo; + pCex->iFrame = iFrame; + // create data-bits + nShift = Saig_ManRegNum(pFrm->pAig); + for ( f = 0; f <= iFrame; f++, nShift += Saig_ManPiNum(pFrm->pAig) ) + Saig_ManForEachPi( pFrm->pAig, pObj, i ) + { + pObjFrames = Ssw_ObjFrame_(pFrm, pObj, f); + if ( pObjFrames == NULL ) + continue; + if ( Ssw_CnfGetNodeValue( pSat, pObjFrames ) ) + Aig_InfoSetBit( pCex->pData, nShift + i ); + } + return pCex; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_ManFilterBmcSavePattern( Ssw_Bmc_t * p ) -{ - unsigned * pInfo; - Aig_Obj_t * pObj; - int i; - if ( p->nPatterns >= p->nPatternsAlloc ) - return; - Saig_ManForEachLo( p->pMan->pAig, pObj, i ) - { - pInfo = Vec_PtrEntry( p->vPatterns, i ); - if ( Aig_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) ) - Aig_InfoSetBit( pInfo, p->nPatterns ); - } - p->nPatterns++; -} /**Function************************************************************* - Synopsis [Performs fraiging for the internal nodes.] + Synopsis [Performs BMC for the given AIG.] Description [] @@ -168,143 +120,95 @@ void Ssw_ManFilterBmcSavePattern( Ssw_Bmc_t * p ) SeeAlso [] ***********************************************************************/ -int Ssw_ManFilterBmc( Ssw_Bmc_t * pBmc, int iPat, int fCheckTargets ) +int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame ) { - Ssw_Man_t * p = pBmc->pMan; - Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo; - unsigned * pInfo; - int i, f, clk, RetValue, fFirst = 0; -clk = clock(); - - // start initialized timeframes - p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 ); - Saig_ManForEachLo( p->pAig, pObj, i ) + Ssw_Frm_t * pFrm; + Ssw_Sat_t * pSat; + Aig_Obj_t * pObj, * pObjFrame; + int status, clkPart, Lit, i, f, RetValue; + + // start managers + assert( Saig_ManRegNum(pAig) > 0 ); + Aig_ManSetPioNumbers( pAig ); + pSat = Ssw_SatStart( 0 ); + pFrm = Ssw_FrmStart( pAig ); + pFrm->pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * 3 ); + // report statistics + if ( fVerbose ) { - pInfo = Vec_PtrEntry( pBmc->vPatterns, i ); - pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Aig_InfoHasBit(pInfo, iPat) ); - Ssw_ObjSetFrame( p, pObj, 0, pObjNew ); + printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", + Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), + Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); + fflush( stdout ); } - - // sweep internal nodes - Ssw_ManStartSolver( p ); - RetValue = pBmc->nFramesSweep; - for ( f = 0; f < pBmc->nFramesSweep; f++ ) + // perform dynamic unrolling + RetValue = -1; + for ( f = 0; f < nFramesMax; 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_ObjCreatePi(p->pFrames) ); - // sweep internal nodes - Aig_ManForEachNode( p->pAig, pObj, i ) + clkPart = clock(); + Saig_ManForEachPo( 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 ) ) + // unroll the circuit for this output + Ssw_BmcUnroll_rec( pFrm, pObj, f ); + pObjFrame = Ssw_ObjFrame_( pFrm, pObj, f ); + Ssw_CnfNodeAddToSolver( pSat, Aig_Regular(pObjFrame) ); + status = sat_solver_simplify(pSat->pSat); + assert( status ); + // solve + Lit = toLitCond( Ssw_ObjSatNum(pSat,pObjFrame), Aig_IsComplement(pObjFrame) ); + if ( fVerbose ) + { + printf( "Solving output %2d of frame %3d ... \r", + i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); + } + status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( status == l_False ) { - Ssw_ManFilterBmcSavePattern( pBmc ); - if ( fFirst == 0 ) +/* + Lit = lit_neg( Lit ); + RetValue = sat_solver_addclause( pSat->pSat, &Lit, &Lit + 1 ); + assert( RetValue ); + if ( pSat->pSat->qtail != pSat->pSat->qhead ) { - fFirst = 1; - pBmc->nConfMax *= 10; - } + RetValue = sat_solver_simplify(pSat->pSat); + assert( RetValue ); + } +*/ + RetValue = 1; + continue; } - if ( f > 0 && p->pSat->stats.conflicts >= pBmc->nConfMax ) + else if ( status == l_True ) { + pAig->pSeqModel = Ssw_BmcGetCounterExample( pFrm, pSat, i, f ); + if ( piFrame ) + *piFrame = f; + RetValue = 0; + break; + } + else + { + if ( piFrame ) + *piFrame = f; RetValue = -1; break; } } - // quit if this is the last timeframe - if ( p->pSat->stats.conflicts >= pBmc->nConfMax ) - { - RetValue += f + 1; - break; - } - if ( fCheckTargets && Ssw_BmcCheckTargets( 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, Aig_Regular(pObjNew) ); - } -//printf( "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts ); - } - if ( fFirst ) - pBmc->nConfMax /= 10; - - // cleanup - Ssw_ClassesCheck( p->ppClasses ); -p->timeBmc += clock() - clk; - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if one of the targets has failed.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_FilterUsingBmc( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose ) -{ - Ssw_Bmc_t * p; - int RetValue, Frames, Iter, clk = clock(); - p = Ssw_BmcManStart( pMan, nConfMax, fVerbose ); - if ( fCheckTargets && Ssw_BmcCheckTargets( p ) ) - { - assert( 0 ); - Ssw_BmcManStop( p ); - return 1; - } - if ( fVerbose ) - { - printf( "AIG : Const = %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 = clock(); - Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets ); if ( fVerbose ) { - printf( "%3d : Const = %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->pSat->stats.conflicts, p->nPatterns, - p->pMan->nSatFailsReal? "f" : " " ); - PRT( "T", clock() - clk ); - } - Ssw_ManCleanup( p->pMan ); - if ( fCheckTargets && Ssw_BmcCheckTargets( p ) ) - { - printf( "Target is hit!!!\n" ); - RetValue = 1; + printf( "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), f ); + printf( "Conf =%8.0f. Var =%8d. AIG=%9d. ", + (double)pSat->pSat->stats.conflicts, + pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) ); + PRT( "T", clock() - clkPart ); + clkPart = clock(); + fflush( stdout ); } - if ( p->nPatterns >= p->nPatternsAlloc ) + if ( RetValue != 1 ) break; } - Ssw_BmcManStop( p ); - - pMan->nStrangers = 0; - pMan->nSatCalls = 0; - pMan->nSatProof = 0; - pMan->nSatFailsReal = 0; - pMan->nSatFailsTotal = 0; - pMan->nSatCallsUnsat = 0; - pMan->nSatCallsSat = 0; - pMan->timeSimSat = 0; - pMan->timeSat = 0; - pMan->timeSatSat = 0; - pMan->timeSatUnsat = 0; - pMan->timeSatUndec = 0; + + Ssw_SatStop( pSat ); + Ssw_FrmStop( pFrm ); return RetValue; } diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c index e4b8f9f6..d068bb78 100644 --- a/src/aig/ssw/sswCnf.c +++ b/src/aig/ssw/sswCnf.c @@ -30,6 +30,63 @@ /**Function************************************************************* + Synopsis [Starts the SAT manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Sat_t * Ssw_SatStart( int fPolarFlip ) +{ + Ssw_Sat_t * p; + int Lit; + p = ALLOC( Ssw_Sat_t, 1 ); + memset( p, 0, sizeof(Ssw_Sat_t) ); + p->pAig = NULL; + p->fPolarFlip = fPolarFlip; + p->vSatVars = Vec_IntStart( 10000 ); + p->vFanins = Vec_PtrAlloc( 100 ); + p->vUsedPis = Vec_PtrAlloc( 100 ); + p->pSat = sat_solver_new(); + sat_solver_setnvars( p->pSat, 1000 ); + // var 0 is not used + // var 1 is reserved for const1 node - add the clause + p->nSatVars = 1; + Lit = toLit( p->nSatVars ); + if ( fPolarFlip ) + Lit = lit_neg( Lit ); + sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); +// Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ ); + Vec_IntWriteEntry( p->vSatVars, 0, p->nSatVars++ ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stop the SAT manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SatStop( Ssw_Sat_t * p ) +{ + if ( p->pSat ) + sat_solver_delete( p->pSat ); + Vec_IntFree( p->vSatVars ); + Vec_PtrFree( p->vFanins ); + Vec_PtrFree( p->vUsedPis ); + free( p ); +} + +/**Function************************************************************* + Synopsis [Addes clauses to the solver.] Description [] @@ -39,7 +96,7 @@ SeeAlso [] ***********************************************************************/ -void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) +void Ssw_AddClausesMux( Ssw_Sat_t * p, Aig_Obj_t * pNode ) { Aig_Obj_t * pNodeI, * pNodeT, * pNodeE; int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; @@ -68,7 +125,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) pLits[0] = toLitCond(VarI, 1); pLits[1] = toLitCond(VarT, 1^fCompT); pLits[2] = toLitCond(VarF, 0); - if ( p->pPars->fPolarFlip ) + if ( p->fPolarFlip ) { if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); @@ -79,7 +136,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) pLits[0] = toLitCond(VarI, 1); pLits[1] = toLitCond(VarT, 0^fCompT); pLits[2] = toLitCond(VarF, 1); - if ( p->pPars->fPolarFlip ) + if ( p->fPolarFlip ) { if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); @@ -90,7 +147,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) pLits[0] = toLitCond(VarI, 0); pLits[1] = toLitCond(VarE, 1^fCompE); pLits[2] = toLitCond(VarF, 0); - if ( p->pPars->fPolarFlip ) + if ( p->fPolarFlip ) { if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); @@ -101,7 +158,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) pLits[0] = toLitCond(VarI, 0); pLits[1] = toLitCond(VarE, 0^fCompE); pLits[2] = toLitCond(VarF, 1); - if ( p->pPars->fPolarFlip ) + if ( p->fPolarFlip ) { if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); @@ -126,7 +183,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) pLits[0] = toLitCond(VarT, 0^fCompT); pLits[1] = toLitCond(VarE, 0^fCompE); pLits[2] = toLitCond(VarF, 1); - if ( p->pPars->fPolarFlip ) + if ( p->fPolarFlip ) { if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); @@ -137,7 +194,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) pLits[0] = toLitCond(VarT, 1^fCompT); pLits[1] = toLitCond(VarE, 1^fCompE); pLits[2] = toLitCond(VarF, 0); - if ( p->pPars->fPolarFlip ) + if ( p->fPolarFlip ) { if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); @@ -158,7 +215,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) +void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) { Aig_Obj_t * pFanin; int * pLits, nLits, RetValue, i; @@ -173,7 +230,7 @@ void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) { pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin)); pLits[1] = toLitCond(Ssw_ObjSatNum(p,pNode), 1); - if ( p->pPars->fPolarFlip ) + if ( p->fPolarFlip ) { if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] ); @@ -185,13 +242,13 @@ void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) Vec_PtrForEachEntry( vSuper, pFanin, i ) { pLits[i] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin)); - if ( p->pPars->fPolarFlip ) + if ( p->fPolarFlip ) { if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] ); } } pLits[nLits-1] = toLitCond(Ssw_ObjSatNum(p,pNode), 0); - if ( p->pPars->fPolarFlip ) + if ( p->fPolarFlip ) { if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] ); } @@ -221,6 +278,7 @@ void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int Vec_PtrPushUnique( vSuper, pObj ); return; } +// pObj->fMarkA = 1; // go through the branches Ssw_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes ); Ssw_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes ); @@ -256,7 +314,7 @@ void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) SeeAlso [] ***********************************************************************/ -void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier ) +void Ssw_ObjAddToFrontier( Ssw_Sat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier ) { assert( !Aig_IsComplement(pObj) ); if ( Ssw_ObjSatNum(p,pObj) ) @@ -264,12 +322,10 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie assert( Ssw_ObjSatNum(p,pObj) == 0 ); if ( Aig_ObjIsConst1(pObj) ) return; - if ( p->pPars->fLatchCorrOpt ) - { - Vec_PtrPush( p->vUsedNodes, pObj ); - if ( Aig_ObjIsPi(pObj) ) - Vec_PtrPush( p->vUsedPis, pObj ); - } +// pObj->fMarkA = 1; + // save PIs (used by register correspondence) + if ( Aig_ObjIsPi(pObj) ) + Vec_PtrPush( p->vUsedPis, pObj ); Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ ); sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) ); if ( Aig_ObjIsNode(pObj) ) @@ -287,7 +343,7 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie SeeAlso [] ***********************************************************************/ -void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ) +void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj ) { Vec_Ptr_t * vFrontier; Aig_Obj_t * pNode, * pFanin; @@ -327,6 +383,36 @@ void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ) } +/**Function************************************************************* + + Synopsis [Copy pattern from the solver into the internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj ) +{ + int Value0, Value1, nVarNum; + assert( !Aig_IsComplement(pObj) ); + nVarNum = Ssw_ObjSatNum( p, pObj ); + if ( nVarNum > 0 ) + return sat_solver_var_value( p->pSat, nVarNum ); +// if ( pObj->fMarkA == 1 ) +// return 0; + if ( Aig_ObjIsPi(pObj) ) + return 0; + assert( Aig_ObjIsNode(pObj) ); + Value0 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin0(pObj) ); + Value0 ^= Aig_ObjFaninC0(pObj); + Value1 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin1(pObj) ); + Value1 ^= Aig_ObjFaninC1(pObj); + return Value0 & Value1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 2af9e900..39f4c736 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -45,13 +45,13 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) p->nPartSize = 0; // size of the partition p->nOverSize = 0; // size of the overlap between partitions p->nFramesK = 1; // the induction depth - p->nFramesAddSim = 0; // additional frames to simulate + p->nFramesAddSim = 2; // additional frames to simulate p->nConstrs = 0; // treat the last nConstrs POs as seq constraints p->nBTLimit = 1000; // conflict limit at a node p->nBTLimitGlobal = 5000000; // conflict limit for all runs p->nMinDomSize = 100; // min clock domain considered for optimization + p->nItersStop = 0; // stop after the given number of iterations p->fPolarFlip = 0; // uses polarity adjustment - p->fSkipCheck = 0; // do not run equivalence check for unaffected cones p->fLatchCorr = 0; // performs register correspondence p->fSemiFormal = 0; // enable semiformal filtering p->fUniqueness = 0; // enable uniqueness constraints @@ -111,7 +111,12 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) } if ( !p->pPars->fLatchCorr ) { + p->pMSat = Ssw_SatStart( 0 ); Ssw_ManSweepBmc( p ); + if ( p->pPars->nFramesK > 1 && p->pPars->fUniqueness ) + Ssw_UniqueRegisterPairInfo( p ); + Ssw_SatStop( p->pMSat ); + p->pMSat = NULL; Ssw_ManCleanup( p ); } if ( p->pPars->fVerbose ) @@ -120,20 +125,23 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) Ssw_ClassesPrint( p->ppClasses, 0 ); } // apply semi-formal filtering +/* if ( p->pPars->fSemiFormal ) { Aig_Man_t * pSRed; - Ssw_FilterUsingBmc( p, 0, 2000, p->pPars->fVerbose ); -// Ssw_FilterUsingBmc( p, 1, 100000, p->pPars->fVerbose ); + Ssw_FilterUsingSemi( p, 0, 2000, p->pPars->fVerbose ); +// Ssw_FilterUsingSemi( p, 1, 100000, p->pPars->fVerbose ); pSRed = Ssw_SpeculativeReduction( p ); Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL ); Aig_ManStop( pSRed ); } +*/ // refine classes using induction nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0; for ( nIter = 0; ; nIter++ ) { clk = clock(); + p->pMSat = Ssw_SatStart( 0 ); if ( p->pPars->fLatchCorrOpt ) { RetValue = Ssw_ManSweepLatch( p ); @@ -153,34 +161,32 @@ clk = clock(); else { RetValue = Ssw_ManSweep( p ); - p->pPars->nConflicts += p->pSat->stats.conflicts; + p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts; if ( p->pPars->fVerbose ) { printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. U = %3d. F = %2d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nUniques, p->nSatFailsReal ); - if ( p->pPars->fSkipCheck ) - printf( "Use = %5d. Skip = %5d. ", - p->nRefUse, p->nRefSkip ); PRT( "T", clock() - clk ); } } + Ssw_SatStop( p->pMSat ); + p->pMSat = NULL; Ssw_ManCleanup( p ); - if ( !RetValue ) + if ( !RetValue ) break; -/* + + if ( p->pPars->nItersStop && p->pPars->nItersStop == nIter ) { - static int Flag = 0; - if ( Flag++ == 4 && nIter == 4 ) - { - Aig_Man_t * pSRed; - pSRed = Ssw_SpeculativeReduction( p ); - Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL ); - Aig_ManStop( pSRed ); - } + Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p ); + Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL ); + Aig_ManStop( pSRed ); + printf( "Iterative refinement is stopped after iteration %d.\n", nIter ); + printf( "The network is reduced using candidate equivalences.\n" ); + printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" ); + printf( "If the miter is SAT, the reduced result is incorrect.\n" ); + break; } -*/ - } p->pPars->nIters = nIter + 1; p->timeTotal = clock() - clkTotal; @@ -224,6 +230,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) return Aig_ManDupOrdered(pAig); } // check and update parameters + if ( pPars->fUniqueness ) + { + pPars->nFramesAddSim = 0; + if ( pPars->nFramesK != 2 ) + printf( "Setting K = 2 for uniqueness constaints to work.\n" ); + pPars->nFramesK = 2; + } if ( pPars->fLatchCorrOpt ) { pPars->fLatchCorr = 1; @@ -232,8 +245,6 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) else { assert( pPars->nFramesK > 0 ); - if ( pPars->nFramesK > 1 ) - pPars->fSkipCheck = 0; // perform partitioning if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig)) || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) ) @@ -259,6 +270,9 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) } // perform refinement of classes pAigNew = Ssw_SignalCorrespondenceRefine( p ); + if ( pPars->fUniqueness ) + printf( "Uniqueness constaint = %3d. Prevented counter-examples = %3d.\n", + p->nUniquesAdded, p->nUniquesUseful ); // cleanup Ssw_ManStop( p ); return pAigNew; diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 636bd139..0a3f7e21 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -42,6 +42,8 @@ extern "C" { //////////////////////////////////////////////////////////////////////// typedef struct Ssw_Man_t_ Ssw_Man_t; // signal correspondence manager +typedef struct Ssw_Frm_t_ Ssw_Frm_t; // unrolled frames manager +typedef struct Ssw_Sat_t_ Ssw_Sat_t; // SAT solver manager typedef struct Ssw_Cla_t_ Ssw_Cla_t; // equivalence classe manager typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager @@ -57,17 +59,10 @@ struct Ssw_Man_t_ // equivalence classes Ssw_Cla_t * ppClasses; // equivalence classes of nodes int fRefined; // is set to 1 when refinement happens - int nRefUse; // the number of equivalences used - int nRefSkip; // the number of equivalences skipped - // SAT solving - sat_solver * pSat; // recyclable SAT solver - int nSatVars; // the counter of SAT variables - Vec_Int_t * vSatVars; // mapping of each node into its SAT var - int nSatVarsTotal; // the total number of SAT vars created - Vec_Ptr_t * vFanins; // fanins of the CNF node + // SAT solving + Ssw_Sat_t * pMSatBmc; // SAT manager for base case + Ssw_Sat_t * pMSat; // SAT manager for inductive case // SAT solving (latch corr only) - Vec_Ptr_t * vUsedNodes; // the nodes with SAT variables - Vec_Ptr_t * vUsedPis; // the PIs with SAT variables Vec_Ptr_t * vSimInfo; // simulation information for the framed PIs int nPatterns; // the number of patterns saved int nSimRounds; // the number of simulation rounds performed @@ -81,7 +76,10 @@ struct Ssw_Man_t_ // uniqueness Vec_Ptr_t * vCommon; // the set of common variables in the logic cones int iOutputLit; // the output literal of the uniqueness constaint + Vec_Int_t * vDiffPairs; // is set to 1 if reg pair can be diff int nUniques; // the number of uniqueness constaints used + int nUniquesAdded; // useful uniqueness constraints + int nUniquesUseful; // useful uniqueness constraints // sequential simulator Ssw_Sml_t * pSml; // counter example storage @@ -118,12 +116,35 @@ struct Ssw_Man_t_ int timeTotal; // total runtime }; +// internal SAT manager +struct Ssw_Sat_t_ +{ + Aig_Man_t * pAig; // the AIG manager + int fPolarFlip; // flips polarity + sat_solver * pSat; // recyclable SAT solver + int nSatVars; // the counter of SAT variables + Vec_Int_t * vSatVars; // mapping of each node into its SAT var + int nSatVarsTotal; // the total number of SAT vars created + Vec_Ptr_t * vFanins; // fanins of the CNF node + Vec_Ptr_t * vUsedPis; // the PIs with SAT variables +}; + +// internal frames manager +struct Ssw_Frm_t_ +{ + Aig_Man_t * pAig; // user-given AIG + int nObjs; // offset in terms of AIG nodes + int nFrames; // the number of frames in current unrolling + Aig_Man_t * pFrames; // unrolled AIG + Vec_Ptr_t * vAig2Frm; // mapping of AIG nodes into frame nodes +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj ) { return Vec_IntEntry( p->vSatVars, pObj->Id ); } -static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntWriteEntryFill( p->vSatVars, pObj->Id, Num ); } +static inline int Ssw_ObjSatNum( Ssw_Sat_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vSatVars, pObj->Id ); } +static inline void Ssw_ObjSetSatNum( Ssw_Sat_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vSatVars, pObj->Id, Num); } static inline int Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) { @@ -141,15 +162,22 @@ static inline void Ssw_ObjSetFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; } static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; } +static inline Aig_Obj_t * Ssw_ObjFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { return Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id ); } +static inline void Ssw_ObjSetFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode ); } + +static inline Aig_Obj_t * Ssw_ObjChild0Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Ssw_ObjChild1Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// /*=== sswAig.c ===================================================*/ +extern Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig ); +extern void Ssw_FrmStop( Ssw_Frm_t * p ); extern Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ); extern Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ); /*=== sswBmc.c ===================================================*/ -extern int Ssw_FilterUsingBmc( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose ); /*=== sswClass.c =================================================*/ extern Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig ); extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData, @@ -177,7 +205,10 @@ extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive ); extern int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive ); /*=== sswCnf.c ===================================================*/ -extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ); +extern Ssw_Sat_t * Ssw_SatStart( int fPolarFlip ); +extern void Ssw_SatStop( Ssw_Sat_t * p ); +extern void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj ); +extern int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObjFraig ); /*=== sswCore.c ===================================================*/ extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ); /*=== sswLcorr.c ==========================================================*/ @@ -190,6 +221,8 @@ extern void Ssw_ManStartSolver( Ssw_Man_t * p ); /*=== sswSat.c ===================================================*/ extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); +/*=== sswSemi.c ===================================================*/ +extern int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose ); /*=== sswSim.c ===================================================*/ extern unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj ); extern int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj ); @@ -214,6 +247,7 @@ extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, i extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p ); /*=== sswUnique.c ===================================================*/ +extern void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p ); extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ); extern int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 ); diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c index cde9b0c9..d374c5f6 100644 --- a/src/aig/ssw/sswLcorr.c +++ b/src/aig/ssw/sswLcorr.c @@ -31,48 +31,6 @@ /**Function************************************************************* - Synopsis [Recycles the SAT solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_ManSatSolverRecycle( Ssw_Man_t * p ) -{ - int Lit; - if ( p->pSat ) - { - Aig_Obj_t * pObj; - int i; - Vec_PtrForEachEntry( p->vUsedNodes, pObj, i ) - Ssw_ObjSetSatNum( p, pObj, 0 ); - Vec_PtrClear( p->vUsedNodes ); - Vec_PtrClear( p->vUsedPis ); -// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) ); - sat_solver_delete( p->pSat ); - } - p->pSat = sat_solver_new(); - sat_solver_setnvars( p->pSat, 1000 ); - // var 0 is not used - // var 1 is reserved for const1 node - add the clause - p->nSatVars = 1; -// p->nSatVars = 0; - Lit = toLit( p->nSatVars ); - if ( p->pPars->fPolarFlip ) - Lit = lit_neg( Lit ); - sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); - Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pFrames), p->nSatVars++ ); - - p->nRecycles++; - p->nRecycleCalls = 0; -} - - -/**Function************************************************************* - Synopsis [Tranfers simulation information from FRAIG to AIG.] Description [] @@ -148,11 +106,11 @@ void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand ) Aig_Obj_t * pObj; unsigned * pInfo; int i, nVarNum, Value; - Vec_PtrForEachEntry( p->vUsedPis, pObj, i ) + Vec_PtrForEachEntry( p->pMSat->vUsedPis, pObj, i ) { - nVarNum = Ssw_ObjSatNum( p, pObj ); + nVarNum = Ssw_ObjSatNum( p->pMSat, pObj ); assert( nVarNum > 0 ); - Value = sat_solver_var_value( p->pSat, nVarNum ); + Value = sat_solver_var_value( p->pMSat->pSat, nVarNum ); if ( Value == 0 ) continue; pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) ); @@ -339,9 +297,14 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) Ssw_ManSweepResimulate( p ); // attempt recycling the SAT solver if ( p->pPars->nSatVarMax && - p->nSatVars > p->pPars->nSatVarMax && + p->pMSat->nSatVars > p->pPars->nSatVarMax && p->nRecycleCalls > p->pPars->nRecycleCalls ) - Ssw_ManSatSolverRecycle( p ); + { + Ssw_SatStop( p->pMSat ); + p->pMSat = Ssw_SatStart( 0 ); + p->nRecycles++; + p->nRecycleCalls = 0; + } } // resimulate if ( p->nPatterns > 0 ) diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index d4a26f64..1b29037c 100644 --- a/src/aig/ssw/sswMan.c +++ b/src/aig/ssw/sswMan.c @@ -53,12 +53,6 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) p->pAig = pAig; p->nFrames = pPars->nFramesK + 1; p->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); - // SAT solving - p->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) ); - p->vFanins = Vec_PtrAlloc( 100 ); - // SAT solving (latch corr only) - p->vUsedNodes = Vec_PtrAlloc( 1000 ); - p->vUsedPis = Vec_PtrAlloc( 1000 ); p->vCommon = Vec_PtrAlloc( 100 ); p->iOutputLit = -1; // allocate storage for sim pattern @@ -106,11 +100,11 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory ); printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n", Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), - p->nSatVarsTotal/p->pPars->nIters ); + 0/p->pPars->nIters ); printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Equivs = %d. Str = %d.\n", p->nSatProof, p->nSatCallsSat, p->nSatFailsTotal, Ssw_ManCountEquivs(p), p->nStrangers ); printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d. Rounds = %d.\n", - p->nSatVars, p->nConeMax, p->nRecycles, p->nSimRounds ); + 0, p->nConeMax, p->nRecycles, p->nSimRounds ); printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) ); @@ -141,23 +135,14 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) ***********************************************************************/ void Ssw_ManCleanup( Ssw_Man_t * p ) { + assert( p->pMSat == NULL ); if ( p->pFrames ) { + Aig_ManCleanMarkA( p->pFrames ); Aig_ManStop( p->pFrames ); p->pFrames = NULL; memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames ); } - if ( p->pSat ) - { - int i; -// printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size ); - p->nSatVarsTotal += p->pSat->size; - sat_solver_delete( p->pSat ); - p->pSat = NULL; -// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) ); - for ( i = 0; i < Vec_IntSize(p->vSatVars); i++ ) - p->vSatVars->pArray[i] = 0; - } if ( p->vSimInfo ) { Vec_PtrFree( p->vSimInfo ); @@ -188,46 +173,14 @@ void Ssw_ManStop( Ssw_Man_t * p ) Ssw_ClassesStop( p->ppClasses ); if ( p->pSml ) Ssw_SmlStop( p->pSml ); - Vec_PtrFree( p->vFanins ); - Vec_PtrFree( p->vUsedNodes ); - Vec_PtrFree( p->vUsedPis ); - Vec_IntFree( p->vSatVars ); + if ( p->vDiffPairs ) + Vec_IntFree( p->vDiffPairs ); Vec_PtrFree( p->vCommon ); FREE( p->pNodeToFrames ); FREE( p->pPatWords ); free( p ); } -/**Function************************************************************* - - Synopsis [Starts the SAT solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_ManStartSolver( Ssw_Man_t * p ) -{ - int Lit; - assert( p->pSat == NULL ); - p->pSat = sat_solver_new(); - sat_solver_setnvars( p->pSat, 1000 ); - // var 0 is not used - // var 1 is reserved for const1 node - add the clause - p->nSatVars = 1; - Lit = toLit( p->nSatVars ); - if ( p->pPars->fPolarFlip ) - Lit = lit_neg( Lit ); - sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); - Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ ); - - Vec_PtrClear( p->vUsedNodes ); - Vec_PtrClear( p->vUsedPis ); -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c index af3bf80e..fc902560 100644 --- a/src/aig/ssw/sswSat.c +++ b/src/aig/ssw/sswSat.c @@ -50,18 +50,19 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) assert( !Aig_IsComplement(pNew) ); assert( pOld != pNew ); - if ( p->pSat == NULL ) - Ssw_ManStartSolver( p ); +// if ( p->pSat == NULL ) +// Ssw_ManStartSolver( p ); + assert( p->pMSat != NULL ); // if the nodes do not have SAT variables, allocate them - Ssw_CnfNodeAddToSolver( p, pOld ); - Ssw_CnfNodeAddToSolver( p, pNew ); + Ssw_CnfNodeAddToSolver( p->pMSat, pOld ); + Ssw_CnfNodeAddToSolver( p->pMSat, pNew ); // solve under assumptions // A = 1; B = 0 OR A = 1; B = 1 nLits = 2; - pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 ); - pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase ); + pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 ); + pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase == pNew->fPhase ); if ( p->iOutputLit > -1 ) pLits[nLits++] = p->iOutputLit; if ( p->pPars->fPolarFlip ) @@ -71,14 +72,14 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) } //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); - if ( p->pSat->qtail != p->pSat->qhead ) + if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead ) { - RetValue = sat_solver_simplify(p->pSat); + RetValue = sat_solver_simplify(p->pMSat->pSat); assert( RetValue != 0 ); } clk = clock(); - RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits, + RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); p->timeSat += clock() - clk; if ( RetValue1 == l_False ) @@ -88,8 +89,15 @@ p->timeSatUnsat += clock() - clk; { pLits[0] = lit_neg( pLits[0] ); pLits[1] = lit_neg( pLits[1] ); - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 ); assert( RetValue ); +/* + if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead ) + { + RetValue = sat_solver_simplify(p->pMSat->pSat); + assert( RetValue != 0 ); + } +*/ } p->nSatCallsUnsat++; } @@ -116,8 +124,8 @@ p->timeSatUndec += clock() - clk; // solve under assumptions // A = 0; B = 1 OR A = 0; B = 0 nLits = 2; - pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 ); - pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase ); + pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 ); + pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase ^ pNew->fPhase ); if ( p->iOutputLit > -1 ) pLits[nLits++] = p->iOutputLit; if ( p->pPars->fPolarFlip ) @@ -126,14 +134,14 @@ p->timeSatUndec += clock() - clk; if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); } - if ( p->pSat->qtail != p->pSat->qhead ) + if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead ) { - RetValue = sat_solver_simplify(p->pSat); + RetValue = sat_solver_simplify(p->pMSat->pSat); assert( RetValue != 0 ); } clk = clock(); - RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits, + RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); p->timeSat += clock() - clk; if ( RetValue1 == l_False ) @@ -143,8 +151,15 @@ p->timeSatUnsat += clock() - clk; { pLits[0] = lit_neg( pLits[0] ); pLits[1] = lit_neg( pLits[1] ); - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 ); assert( RetValue ); +/* + if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead ) + { + RetValue = sat_solver_simplify(p->pMSat->pSat); + assert( RetValue != 0 ); + } +*/ } p->nSatCallsUnsat++; } @@ -183,6 +198,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) // sanity checks assert( Aig_Regular(pOld) != Aig_Regular(pNew) ); + assert( Aig_ObjPhaseReal(pOld) == Aig_ObjPhaseReal(pNew) ); // move constant to the old node if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) ) @@ -200,13 +216,13 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) pNew = Aig_Not(pNew); } - // start the solver - if ( p->pSat == NULL ) - Ssw_ManStartSolver( p ); +// if ( p->pSat == NULL ) +// Ssw_ManStartSolver( p ); + assert( p->pMSat != NULL ); // if the nodes do not have SAT variables, allocate them - Ssw_CnfNodeAddToSolver( p, pOld ); - Ssw_CnfNodeAddToSolver( p, Aig_Regular(pNew) ); + Ssw_CnfNodeAddToSolver( p->pMSat, pOld ); + Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pNew) ); // transform the new node fComplNew = Aig_IsComplement( pNew ); @@ -216,12 +232,12 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) if ( pOld == Aig_ManConst1(p->pFrames) ) { // add constaint A = 1 ----> A - pLits[0] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew ); + pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew ); if ( p->pPars->fPolarFlip ) { if ( pNew->fPhase ) pLits[0] = lit_neg( pLits[0] ); } - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); + RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 1 ); assert( RetValue ); } else @@ -229,8 +245,8 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) // add constaint A = B ----> (A v !B)(!A v B) // (A v !B) - pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 ); - pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), !fComplNew ); + pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 ); + pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), !fComplNew ); if ( p->pPars->fPolarFlip ) { if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); @@ -238,12 +254,12 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) } pLits[0] = lit_neg( pLits[0] ); pLits[1] = lit_neg( pLits[1] ); - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 ); assert( RetValue ); // (!A v B) - pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 ); - pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew); + pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 ); + pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew); if ( p->pPars->fPolarFlip ) { if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); @@ -251,7 +267,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) } pLits[0] = lit_neg( pLits[0] ); pLits[1] = lit_neg( pLits[1] ); - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 ); assert( RetValue ); } return 1; diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c new file mode 100644 index 00000000..b445c2c4 --- /dev/null +++ b/src/aig/ssw/sswSemi.c @@ -0,0 +1,318 @@ +/**CFile**************************************************************** + + FileName [sswSemi.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Semiformal for equivalence clases.] + + 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" + +//////////////////////////////////////////////////////////////////////// +/// 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 = ALLOC( Ssw_Sem_t, 1 ); + memset( p, 0, sizeof(Ssw_Sem_t) ); + p->nConfMaxStart = nConfMax; + p->nConfMax = nConfMax; + p->nFramesSweep = AIG_MAX( (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), Aig_BitWordNum(p->nPatternsAlloc) ); + Vec_PtrCleanSimInfo( p->vPatterns, 0, Aig_BitWordNum(p->nPatternsAlloc) ); + p->vHistory = Vec_IntAlloc( 100 ); + Vec_IntPush( p->vHistory, 0 ); + // update arrays of the manager + assert( 0 ); +/* + free( p->pMan->pNodeToFrames ); + Vec_IntFree( p->pMan->vSatVars ); + p->pMan->pNodeToFrames = 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 ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SemCheckTargets( Ssw_Sem_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Vec_PtrForEachEntry( 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 = Vec_PtrEntry( p->vPatterns, i ); + if ( Aig_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) ) + Aig_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, clk, RetValue, fFirst = 0; +clk = clock(); + + // start initialized timeframes + p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 ); + Saig_ManForEachLo( p->pAig, pObj, i ) + { + pInfo = Vec_PtrEntry( pBmc->vPatterns, i ); + pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Aig_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_ObjCreatePi(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 ) ) + { + 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) ); + } +//printf( "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts ); + } + if ( fFirst ) + pBmc->nConfMax /= 10; + + // cleanup + Ssw_ClassesCheck( p->ppClasses ); +p->timeBmc += 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, clk = clock(); + p = Ssw_SemManStart( pMan, nConfMax, fVerbose ); + if ( fCheckTargets && Ssw_SemCheckTargets( p ) ) + { + assert( 0 ); + Ssw_SemManStop( p ); + return 1; + } + if ( fVerbose ) + { + printf( "AIG : Const = %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 = clock(); + pMan->pMSat = Ssw_SatStart( 0 ); + Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets ); + if ( fVerbose ) + { + printf( "%3d : Const = %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" : " " ); + PRT( "T", clock() - clk ); + } + Ssw_ManCleanup( p->pMan ); + if ( fCheckTargets && Ssw_SemCheckTargets( p ) ) + { + printf( "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->nSatFailsTotal = 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 /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index ba8ad247..b80c3710 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -271,45 +271,6 @@ void Ssw_SmlSavePattern1( Ssw_Man_t * p, int fInit ) Aig_InfoXorBit( p->pPatWords, nTruePis * p->nFrames + k++ ); } -/**Function************************************************************* - - Synopsis [Copy pattern from the solver into the internal storage.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_SmlSavePattern( Ssw_Man_t * p ) -{ - Aig_Obj_t * pObj; - int i; - memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); - Aig_ManForEachPi( p->pFrames, pObj, i ) - if ( p->pSat->model.ptr[Ssw_ObjSatNum(p, pObj)] == l_True ) - Aig_InfoSetBit( p->pPatWords, i ); -/* - if ( p->vCex ) - { - Vec_IntClear( p->vCex ); - for ( i = 0; i < Saig_ManPiNum(p->pAig); i++ ) - Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) ); - for ( i = Saig_ManPiNum(p->pFrames); i < Aig_ManPiNum(p->pFrames); i++ ) - Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) ); - } -*/ - -/* - printf( "Pattern: " ); - Aig_ManForEachPi( p->pFrames, pObj, i ) - printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) ); - printf( "\n" ); -*/ -} - - /**Function************************************************************* diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c index b971a13a..36e8bab3 100644 --- a/src/aig/ssw/sswSweep.c +++ b/src/aig/ssw/sswSweep.c @@ -31,53 +31,6 @@ /**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 [] @@ -89,12 +42,22 @@ void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p ) ***********************************************************************/ int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) { + int fUseNoBoundary = 0; Aig_Obj_t * pObjFraig; - int nVarNum, Value; + int Value; // assert( Aig_ObjIsPi(pObj) ); pObjFraig = Ssw_ObjFrame( p, pObj, f ); - nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) ); - Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum )); + if ( fUseNoBoundary ) + { + Value = Ssw_CnfGetNodeValue( p->pMSat, Aig_Regular(pObjFraig) ); + Value ^= Aig_IsComplement(pObjFraig); + } + else + { + int nVarNum = Ssw_ObjSatNum( p->pMSat, Aig_Regular(pObjFraig) ); + Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pMSat->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 ) @@ -181,15 +144,8 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) // 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) ) + 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) ); @@ -204,18 +160,13 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) 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 RetValue; @@ -224,12 +175,39 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) p->iOutputLit = -1; return RetValue; } +*/ + if ( Ssw_ManUniqueAddConstraint( p, p->vCommon, 0, 1 ) ) + { + int RetValue2 = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); + p->iOutputLit = -1; + p->nUniques++; + p->nUniquesAdded++; + if ( RetValue2 == 0 ) + { + int x; +// printf( "Second time:\n" ); + x = Ssw_ManUniqueOne( p, pObjRepr, pObj ); + 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; + } + else + p->nUniquesUseful++; +// printf( "Counter-example prevented!!!\n" ); + return 0; + } } 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(): Failed to refine representative.\n" ); + } return 1; } @@ -260,7 +238,7 @@ clk = clock(); p->fRefined = 0; if ( p->pPars->fVerbose ) pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); - Ssw_ManStartSolver( p ); +// Ssw_ManStartSolver( p ); for ( f = 0; f < p->pPars->nFramesK; f++ ) { // map constants and PIs @@ -285,7 +263,7 @@ clk = clock(); { pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f); Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew ); - Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) ); + Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );// } } if ( p->pPars->fVerbose ) @@ -308,19 +286,63 @@ p->timeBmc += clock() - clk; SeeAlso [] ***********************************************************************/ -int Ssw_ManSweep( Ssw_Man_t * p ) +void Ssw_CheckConstaints( Ssw_Man_t * p ) { + Aig_Obj_t * pObj, * pObj2; + int nConstrPairs, i; + int Counter = 0; + nConstrPairs = Aig_ManPoNum(p->pFrames)-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 ); + if ( Ssw_NodesAreEquiv( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) ) != 1 ) + { + Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) ); + Counter++; + } + } + printf( "Total constraints = %d. Added constraints = %d.\n", nConstrPairs/2, Counter ); + } + +/**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; +// int v; // perform speculative reduction clk = clock(); // create timeframes p->pFrames = Ssw_FramesWithClasses( p ); // add constraints - Ssw_ManStartSolver( p ); +// p->pMSat = Ssw_SatStart( 0 ); +// Ssw_ManStartSolver( p ); +/* + { + int clk2 = clock(); + Ssw_CheckConstaints( p ); + PRT( "Time", clock() - clk2 ); + } + + Ssw_ManCleanup( p ); + p->pFrames = Ssw_FramesWithClasses( p ); + p->pMSat = Ssw_SatStart( 0 ); +// Ssw_ManStartSolver( p ); +*/ nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig); assert( (nConstrPairs & 1) == 0 ); for ( i = 0; i < nConstrPairs; i += 2 ) @@ -333,17 +355,11 @@ clk = clock(); for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) { pObj = Aig_ManPo( p->pFrames, nConstrPairs + i ); - Ssw_CnfNodeAddToSolver( p, Aig_ObjFanin0(pObj) ); + Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );// } - sat_solver_simplify( p->pSat ); + sat_solver_simplify( p->pMSat->pSat ); 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 @@ -354,17 +370,26 @@ p->timeMarkCones += clock() - clk; // make sure LOs are assigned Saig_ManForEachLo( p->pAig, pObj, i ) assert( Ssw_ObjFrame( p, pObj, f ) != NULL ); +/* + // mark the PI/LO of the last frame + Aig_ManForEachPi( p->pAig, pObj, i ) + { + pObjNew = Ssw_ObjFrame( p, pObj, f ); + Aig_Regular(pObjNew)->fMarkA = 1; + } +*/ //// +/* // bring up the previous frames if ( p->pPars->fUniqueness ) for ( v = 0; v < f; v++ ) Saig_ManForEachLo( p->pAig, pObj, i ) - Ssw_CnfNodeAddToSolver( p, Aig_Regular(Ssw_ObjFrame(p, pObj, v)) ); + Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(Ssw_ObjFrame(p, pObj, v)) ); +*/ //// // 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 ) diff --git a/src/aig/ssw/sswUnique.c b/src/aig/ssw/sswUnique.c index 888ed3da..0d9b016f 100644 --- a/src/aig/ssw/sswUnique.c +++ b/src/aig/ssw/sswUnique.c @@ -30,83 +30,39 @@ /**Function************************************************************* - Synopsis [Returns the result of merging the two vectors.] + Synopsis [Performs computation of signal correspondence with constraints.] - Description [Assumes that the vectors are sorted in the increasing order.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -static inline void Vec_PtrTwoMerge( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr ) +void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p ) { - Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray; - Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray; - Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray; - Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize; - Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize; - Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) ); - pBeg = (Aig_Obj_t **)vArr->pArray; - while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + Aig_Obj_t * pObjLo, * pObj0, * pObj1; + int i; + if ( p->vDiffPairs == NULL ) + p->vDiffPairs = Vec_IntAlloc( Saig_ManRegNum(p->pAig) ); + Vec_IntClear( p->vDiffPairs ); + Saig_ManForEachLo( p->pAig, pObjLo, i ) { - if ( (*pBeg1)->Id == (*pBeg2)->Id ) - *pBeg++ = *pBeg1++, pBeg2++; - else if ( (*pBeg1)->Id < (*pBeg2)->Id ) - *pBeg++ = *pBeg1++; + pObj0 = Ssw_ObjFrame( p, pObjLo, 0 ); + pObj1 = Ssw_ObjFrame( p, pObjLo, 1 ); + if ( pObj0 == pObj1 ) + Vec_IntPush( p->vDiffPairs, 0 ); + else if ( pObj0 == Aig_Not(pObj1) ) + Vec_IntPush( p->vDiffPairs, 1 ); else - *pBeg++ = *pBeg2++; + { + // assume that if the nodes are structurally different + // they can also be functionally different + Vec_IntPush( p->vDiffPairs, 1 ); + } } - while ( pBeg1 < pEnd1 ) - *pBeg++ = *pBeg1++; - while ( pBeg2 < pEnd2 ) - *pBeg++ = *pBeg2++; - vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray; - assert( vArr->nSize <= vArr->nCap ); - assert( vArr->nSize >= vArr1->nSize ); - assert( vArr->nSize >= vArr2->nSize ); } -/**Function************************************************************* - - Synopsis [Returns the result of merging the two vectors.] - - Description [Assumes that the vectors are sorted in the increasing order.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Vec_PtrTwoCommon( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr ) -{ - Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray; - Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray; - Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray; - Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize; - Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize; - Vec_PtrGrow( vArr, AIG_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) ); - pBeg = (Aig_Obj_t **)vArr->pArray; - while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) - { - if ( (*pBeg1)->Id == (*pBeg2)->Id ) - *pBeg++ = *pBeg1++, pBeg2++; - else if ( (*pBeg1)->Id < (*pBeg2)->Id ) -// *pBeg++ = *pBeg1++; - pBeg1++; - else -// *pBeg++ = *pBeg2++; - pBeg2++; - } -// while ( pBeg1 < pEnd1 ) -// *pBeg++ = *pBeg1++; -// while ( pBeg2 < pEnd2 ) -// *pBeg++ = *pBeg2++; - vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray; - assert( vArr->nSize <= vArr->nCap ); - assert( vArr->nSize <= vArr1->nSize ); - assert( vArr->nSize <= vArr2->nSize ); -} /**Function************************************************************* @@ -123,56 +79,32 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ) { int fVerbose = 0; Aig_Obj_t * ppObjs[2], * pTemp; - Vec_Ptr_t * vSupp, * vSupp2; - int i, k, Value0, Value1, RetValue; - assert( p->pPars->nFramesK > 1 ); + int i, k, Value0, Value1, RetValue, fFeasible; - vSupp = Vec_PtrAlloc( 100 ); - vSupp2 = Vec_PtrAlloc( 100 ); - Vec_PtrClear( p->vCommon ); + assert( p->pPars->nFramesK > 1 ); + assert( p->vDiffPairs && Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) ); // compute the first support in terms of LOs ppObjs[0] = pRepr; ppObjs[1] = pObj; - Aig_SupportNodes( p->pAig, ppObjs, 2, vSupp ); - // modify support to be in terms of LIs + Aig_SupportNodes( p->pAig, ppObjs, 2, p->vCommon ); + // keep only LOs + RetValue = Vec_PtrSize( p->vCommon ); + fFeasible = 0; k = 0; - Vec_PtrForEachEntry( vSupp, pTemp, i ) + Vec_PtrForEachEntry( p->vCommon, pTemp, i ) if ( Saig_ObjIsLo(p->pAig, pTemp) ) - Vec_PtrWriteEntry( vSupp, k++, Saig_ObjLoToLi(p->pAig, pTemp) ); - Vec_PtrShrink( vSupp, k ); - // compute the support of support - Aig_SupportNodes( p->pAig, (Aig_Obj_t **)Vec_PtrArray(vSupp), Vec_PtrSize(vSupp), vSupp2 ); - // return support to LO - Vec_PtrForEachEntry( vSupp, pTemp, i ) - Vec_PtrWriteEntry( vSupp, i, Saig_ObjLiToLo(p->pAig, pTemp) ); - // find the number of common vars - Vec_PtrSort( vSupp, Aig_ObjCompareIdIncrease ); - Vec_PtrSort( vSupp2, Aig_ObjCompareIdIncrease ); - Vec_PtrTwoCommon( vSupp, vSupp2, p->vCommon ); -/* - { - Vec_Ptr_t * vNew = Vec_PtrDup(vSupp); - Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease ); - if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp) ) - printf( "Not unique!\n" ); - } - { - Vec_Ptr_t * vNew = Vec_PtrDup(vSupp2); - Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease ); - if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp2) ) - printf( "Not unique!\n" ); - } - { - Vec_Ptr_t * vNew = Vec_PtrDup(p->vCommon); - Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease ); - if ( Vec_PtrSize(vNew) != Vec_PtrSize(p->vCommon) ) - printf( "Not unique!\n" ); - } -*/ + { + Vec_PtrWriteEntry( p->vCommon, k++, pTemp ); + if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjPioNum(pTemp) - Saig_ManPiNum(p->pAig)) ) + fFeasible = 1; + } + Vec_PtrShrink( p->vCommon, k ); + if ( fVerbose ) - printf( "Node = %5d : One = %3d. Two = %3d. Common = %3d. ", - Aig_ObjId(pObj), Vec_PtrSize(vSupp), Vec_PtrSize(vSupp2), Vec_PtrSize(p->vCommon) ); + printf( "Node = %5d : Supp = %3d. Regs = %3d. Feasible = %s. ", + Aig_ObjId(pObj), RetValue, Vec_PtrSize(p->vCommon), + fFeasible? "yes": "no " ); // check the current values RetValue = 1; @@ -185,14 +117,10 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ) if ( fVerbose ) printf( "%d", Value0 ^ Value1 ); } - if ( Vec_PtrSize(p->vCommon) == 0 ) - RetValue = 0; if ( fVerbose ) printf( "\n" ); - Vec_PtrFree( vSupp ); - Vec_PtrFree( vSupp2 ); - return RetValue; + return RetValue && fFeasible; } /**Function************************************************************* @@ -227,11 +155,10 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int // printf( "Skipped\n" ); return 0; } - p->nUniques++; // create CNF - Ssw_CnfNodeAddToSolver( p, Aig_Regular(pTotal) ); + Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pTotal) ); // add output constraint - pLits[0] = toLitCond( Ssw_ObjSatNum(p,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) ); + pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) ); /* RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); assert( RetValue ); |