From 91effd8148493c3837513c9256eefdf488dd9b97 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 22 Sep 2008 08:01:00 -0700 Subject: Version abc80922 --- src/aig/ssw/module.make | 1 + src/aig/ssw/ssw.h | 3 +- src/aig/ssw/sswAig.c | 79 ++++++++++-- src/aig/ssw/sswBmc.c | 315 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/ssw/sswClass.c | 47 ++++++++ src/aig/ssw/sswCore.c | 24 ++++ src/aig/ssw/sswInt.h | 12 +- src/aig/ssw/sswMan.c | 9 +- src/aig/ssw/sswSweep.c | 19 ++- 9 files changed, 483 insertions(+), 26 deletions(-) create mode 100644 src/aig/ssw/sswBmc.c (limited to 'src/aig/ssw') diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make index c5668d6d..6b748598 100644 --- a/src/aig/ssw/module.make +++ b/src/aig/ssw/module.make @@ -1,4 +1,5 @@ SRC += src/aig/ssw/sswAig.c \ + src/aig/ssw/sswBmc.c \ src/aig/ssw/sswClass.c \ src/aig/ssw/sswCnf.c \ src/aig/ssw/sswCore.c \ diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 8d74f16b..98e8c9d7 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -52,11 +52,12 @@ struct Ssw_Pars_t_ 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 fVerbose; // verbose stats // optimized latch correspondence int fLatchCorrOpt; // perform register correspondence (optimized) int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only) int nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only) - int fVerbose; // verbose stats // internal parameters int nIters; // the number of iterations performed }; diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c index 5a47ba5f..0d0fdbee 100644 --- a/src/aig/ssw/sswAig.c +++ b/src/aig/ssw/sswAig.c @@ -39,9 +39,9 @@ SeeAlso [] ***********************************************************************/ -static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, Aig_Man_t * pAig, Aig_Obj_t * pObj, int iFrame ) +static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, Aig_Man_t * pAig, Aig_Obj_t * pObj, int iFrame, int fTwoPos ) { - Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew; + Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter; // skip nodes without representative pObjRepr = Aig_ObjRepr(pAig, pObj); if ( pObjRepr == NULL ) @@ -71,8 +71,16 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, // set the new node Ssw_ObjSetFrame( p, pObj, iFrame, pObjNew2 ); // add the constraint - Aig_ObjCreatePo( pFrames, pObjNew2 ); - Aig_ObjCreatePo( pFrames, pObjNew ); + if ( fTwoPos ) + { + Aig_ObjCreatePo( pFrames, pObjNew2 ); + Aig_ObjCreatePo( pFrames, pObjNew ); + } + else + { + pMiter = Aig_Exor( pFrames, pObjNew, pObjNew2 ); + Aig_ObjCreatePo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) ); + } } /**Function************************************************************* @@ -94,6 +102,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) assert( p->pFrames == NULL ); 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 ); @@ -101,22 +110,21 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) Saig_ManForEachLo( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) ); // add timeframes - p->nConstrTotal = p->nConstrReduced = 0; for ( f = 0; f < p->pPars->nFramesK; f++ ) { // map constants and PIs Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) ); - Aig_ManForEachPiSeq( p->pAig, pObj, i ) + Saig_ManForEachPi( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(pFrames) ); // set the constraints on the latch outputs - Aig_ManForEachLoSeq( p->pAig, pObj, i ) - Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f ); + Saig_ManForEachLo( p->pAig, pObj, i ) + Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 ); // add internal nodes of this frame Aig_ManForEachNode( p->pAig, pObj, i ) { pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); - Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f ); + Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 ); } // transfer latch input to the latch outputs Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) @@ -134,6 +142,59 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) return pFrames; } + + +/**Function************************************************************* + + Synopsis [Prepares the inductive case with speculative reduction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjNew; + int i; + assert( p->pFrames == NULL ); + 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 + Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(pFrames) ); + Saig_ManForEachPi( p->pAig, pObj, i ) + Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) ); + // create latches for the first frame + Saig_ManForEachLo( p->pAig, pObj, i ) + Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) ); + // set the constraints on the latch outputs + Saig_ManForEachLo( p->pAig, pObj, i ) + Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 ); + // add internal nodes of this frame + Aig_ManForEachNode( p->pAig, pObj, i ) + { + pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) ); + Ssw_ObjSetFrame( p, pObj, 0, pObjNew ); + Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 ); + } + // add the POs for the latch outputs of the last frame + Saig_ManForEachLi( p->pAig, pObj, i ) + Aig_ObjCreatePo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) ); + // 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 ); + return pFrames; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswBmc.c b/src/aig/ssw/sswBmc.c new file mode 100644 index 00000000..e2d47440 --- /dev/null +++ b/src/aig/ssw/sswBmc.c @@ -0,0 +1,315 @@ +/**CFile**************************************************************** + + FileName [sswBmc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Bounded model checker for equivalence clases.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswBmc.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// 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 [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Bmc_t * Ssw_BmcManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose ) +{ + 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 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_BmcCheckTargets( Ssw_Bmc_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_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.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManFilterBmc( Ssw_Bmc_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 + Ssw_ManStartSolver( p ); + 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->pSat->stats.conflicts >= pBmc->nConfMax ) + { + 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; + } + if ( p->nPatterns >= p->nPatternsAlloc ) + 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; + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index db593311..cfbb138c 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -193,6 +193,22 @@ void Ssw_ClassesStop( Ssw_Cla_t * p ) free( p ); } +/**Function************************************************************* + + Synopsis [Stop representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ssw_ClassesReadAig( Ssw_Cla_t * p ) +{ + return p->pAig; +} + /**Function************************************************************* Synopsis [] @@ -641,6 +657,37 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax return p; } +/**Function************************************************************* + + Synopsis [Creates initial simulation classes.] + + Description [Assumes that simulation info is assigned.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig ) +{ + Ssw_Cla_t * p; + Aig_Obj_t * pObj; + int i; + // start the classes + p = Ssw_ClassesStart( pAig ); + // go through the nodes + p->nCands1 = 0; + Saig_ManForEachPo( pAig, pObj, i ) + { + Ssw_ObjSetConst1Cand( pAig, Aig_ObjFanin0(pObj) ); + p->nCands1++; + } + // allocate room for classes + p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 ); +// Ssw_ClassesPrint( p, 0 ); + return p; +} + /**Function************************************************************* Synopsis [Creates classes from the temporary representation.] diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index fc9f5672..424e3531 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -52,6 +52,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) 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->fVerbose = 0; // verbose stats // latch correspondence p->fLatchCorrOpt = 0; // performs optimized register correspondence @@ -116,6 +117,16 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) printf( "After BMC: " ); 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 ); + 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++ ) @@ -154,6 +165,18 @@ clk = clock(); Ssw_ManCleanup( p ); if ( !RetValue ) break; + + { + 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 ); + } + } + } p->pPars->nIters = nIter + 1; p->timeTotal = clock() - clkTotal; @@ -220,6 +243,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) { // perform one round of seq simulation and generate candidate equivalence classes p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose ); +// p->ppClasses = Ssw_ClassesPrepareTargets( pAig ); p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); } diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index faa3a87d..5daffc75 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -62,7 +62,7 @@ struct Ssw_Man_t_ // SAT solving sat_solver * pSat; // recyclable SAT solver int nSatVars; // the counter of SAT variables - int * pSatVars; // mapping of each node into its SAT var + 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 (latch corr only) @@ -118,8 +118,8 @@ struct Ssw_Man_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; } -static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; } +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_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) { @@ -143,6 +143,9 @@ static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int /*=== sswAig.c ===================================================*/ 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, @@ -150,6 +153,7 @@ extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData, int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ); extern void Ssw_ClassesStop( Ssw_Cla_t * p ); +extern Aig_Man_t * Ssw_ClassesReadAig( Ssw_Cla_t * p ); extern Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p ); extern void Ssw_ClassesClearRefined( Ssw_Cla_t * p ); extern int Ssw_ClassesCand1Num( Ssw_Cla_t * p ); @@ -162,6 +166,7 @@ extern void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose ); extern void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ); extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose ); extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); +extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig ); extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses ); extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive ); extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive ); @@ -200,6 +205,7 @@ extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrame extern void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ); extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ); /*=== sswSweep.c ===================================================*/ +extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ); extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p ); diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index 8d2c8c24..ba19d46e 100644 --- a/src/aig/ssw/sswMan.c +++ b/src/aig/ssw/sswMan.c @@ -54,7 +54,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) p->nFrames = pPars->nFramesK + 1; p->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); // SAT solving - p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) ); + 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 ); @@ -147,11 +147,14 @@ void Ssw_ManCleanup( Ssw_Man_t * p ) } 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) ); +// 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 ) { @@ -186,8 +189,8 @@ void Ssw_ManStop( Ssw_Man_t * p ) Vec_PtrFree( p->vFanins ); Vec_PtrFree( p->vUsedNodes ); Vec_PtrFree( p->vUsedPis ); + Vec_IntFree( p->vSatVars ); FREE( p->pNodeToFrames ); - FREE( p->pSatVars ); FREE( p->pPatWords ); free( p ); } diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c index 9330dafa..add00a88 100644 --- a/src/aig/ssw/sswSweep.c +++ b/src/aig/ssw/sswSweep.c @@ -156,14 +156,14 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f ) SeeAlso [] ***********************************************************************/ -void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) +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; + return 0; // get the fraiged node pObjFraig = Ssw_ObjFrame( p, pObj, f ); // get the fraiged representative @@ -179,7 +179,7 @@ void 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; + return 0; // count the number of skipped calls if ( !pObj->fMarkA && !pObjRepr->fMarkA ) p->nRefSkip++; @@ -196,13 +196,12 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) { pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 ); - return; + return 0; } if ( RetValue == -1 ) // timed out { Ssw_ClassesRemoveNode( p->ppClasses, pObj ); - p->fRefined = 1; - return; + return 1; } // check if skipping calls works correctly if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA ) @@ -218,7 +217,7 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) else Ssw_ManResimulateBit( p, pObj, pObjRepr ); assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); - p->fRefined = 1; + return 1; } /**Function************************************************************* @@ -262,7 +261,7 @@ clk = clock(); 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 ); - Ssw_ManSweepNode( p, pObj, f, 1 ); + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1 ); } // quit if this is the last timeframe if ( f == p->pPars->nFramesK - 1 ) @@ -351,13 +350,13 @@ p->timeMarkCones += clock() - clk; if ( p->pPars->fVerbose ) Bar_ProgressUpdate( pProgress, i, NULL ); if ( Saig_ObjIsLo(p->pAig, pObj) ) - Ssw_ManSweepNode( p, pObj, f, 0 ); + 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 ); - Ssw_ManSweepNode( p, pObj, f, 0 ); + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 ); } } p->nSatFailsTotal += p->nSatFailsReal; -- cgit v1.2.3