Skip to content

A
abc
Commit 91effd81 by Alan Mishchenko
Options

Version abc80922

parent 23c428ea
Showing with 510 additions and 26 deletions
abc.dsp
...@@ -3438,6 +3438,10 @@ SOURCE=.\src\aig\ssw\sswAig.c ...@@ -3438,6 +3438,10 @@ SOURCE=.\src\aig\ssw\sswAig.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\aig\ssw\sswBmc.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswClass.c SOURCE=.\src\aig\ssw\sswClass.c
# End Source File # End Source File
# Begin Source File # Begin Source File
......
src/aig/ssw/module.make
SRC += src/aig/ssw/sswAig.c \ SRC += src/aig/ssw/sswAig.c \
src/aig/ssw/sswBmc.c \
src/aig/ssw/sswClass.c \ src/aig/ssw/sswClass.c \
src/aig/ssw/sswCnf.c \ src/aig/ssw/sswCnf.c \
src/aig/ssw/sswCore.c \ src/aig/ssw/sswCore.c \
......
src/aig/ssw/ssw.h
...@@ -52,11 +52,12 @@ struct Ssw_Pars_t_ ...@@ -52,11 +52,12 @@ struct Ssw_Pars_t_
int fPolarFlip; // uses polarity adjustment int fPolarFlip; // uses polarity adjustment
int fSkipCheck; // do not run equivalence check for unaffected cones int fSkipCheck; // do not run equivalence check for unaffected cones
int fLatchCorr; // perform register correspondence int fLatchCorr; // perform register correspondence
int fSemiFormal; // enable semiformal filtering
int fVerbose; // verbose stats
// optimized latch correspondence // optimized latch correspondence
int fLatchCorrOpt; // perform register correspondence (optimized) int fLatchCorrOpt; // perform register correspondence (optimized)
int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only) 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 nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only)
int fVerbose; // verbose stats
// internal parameters // internal parameters
int nIters; // the number of iterations performed int nIters; // the number of iterations performed
}; };
......
src/aig/ssw/sswAig.c
...@@ -39,9 +39,9 @@ ...@@ -39,9 +39,9 @@
SeeAlso [] 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 // skip nodes without representative
pObjRepr = Aig_ObjRepr(pAig, pObj); pObjRepr = Aig_ObjRepr(pAig, pObj);
if ( pObjRepr == NULL ) if ( pObjRepr == NULL )
...@@ -71,8 +71,16 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, ...@@ -71,8 +71,16 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
// set the new node // set the new node
Ssw_ObjSetFrame( p, pObj, iFrame, pObjNew2 ); Ssw_ObjSetFrame( p, pObj, iFrame, pObjNew2 );
// add the constraint // add the constraint
if ( fTwoPos )
{
Aig_ObjCreatePo( pFrames, pObjNew2 ); Aig_ObjCreatePo( pFrames, pObjNew2 );
Aig_ObjCreatePo( pFrames, pObjNew ); Aig_ObjCreatePo( pFrames, pObjNew );
}
else
{
pMiter = Aig_Exor( pFrames, pObjNew, pObjNew2 );
Aig_ObjCreatePo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
}
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -94,6 +102,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) ...@@ -94,6 +102,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
assert( p->pFrames == NULL ); assert( p->pFrames == NULL );
assert( Aig_ManRegNum(p->pAig) > 0 ); assert( Aig_ManRegNum(p->pAig) > 0 );
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
p->nConstrTotal = p->nConstrReduced = 0;
// start the fraig package // start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames ); pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
...@@ -101,22 +110,21 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) ...@@ -101,22 +110,21 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
Saig_ManForEachLo( p->pAig, pObj, i ) Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) ); Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
// add timeframes // add timeframes
p->nConstrTotal = p->nConstrReduced = 0;
for ( f = 0; f < p->pPars->nFramesK; f++ ) for ( f = 0; f < p->pPars->nFramesK; f++ )
{ {
// map constants and PIs // map constants and PIs
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) ); 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) ); Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(pFrames) );
// set the constraints on the latch outputs // set the constraints on the latch outputs
Aig_ManForEachLoSeq( p->pAig, pObj, i ) Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f ); Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
// add internal nodes of this frame // add internal nodes of this frame
Aig_ManForEachNode( p->pAig, pObj, i ) Aig_ManForEachNode( p->pAig, pObj, i )
{ {
pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew ); 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 // transfer latch input to the latch outputs
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
...@@ -134,6 +142,59 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) ...@@ -134,6 +142,59 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
return pFrames; 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 /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/ssw/sswClass.c
...@@ -195,6 +195,22 @@ void Ssw_ClassesStop( Ssw_Cla_t * p ) ...@@ -195,6 +195,22 @@ void Ssw_ClassesStop( Ssw_Cla_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Stop representation of equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ssw_ClassesReadAig( Ssw_Cla_t * p )
{
return p->pAig;
}
/**Function*************************************************************
Synopsis [] Synopsis []
Description [] Description []
...@@ -643,6 +659,37 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax ...@@ -643,6 +659,37 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
/**Function************************************************************* /**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.] Synopsis [Creates classes from the temporary representation.]
Description [] Description []
......
src/aig/ssw/sswCore.c
...@@ -52,6 +52,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) ...@@ -52,6 +52,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->fPolarFlip = 0; // uses polarity adjustment p->fPolarFlip = 0; // uses polarity adjustment
p->fSkipCheck = 0; // do not run equivalence check for unaffected cones p->fSkipCheck = 0; // do not run equivalence check for unaffected cones
p->fLatchCorr = 0; // performs register correspondence p->fLatchCorr = 0; // performs register correspondence
p->fSemiFormal = 0; // enable semiformal filtering
p->fVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats
// latch correspondence // latch correspondence
p->fLatchCorrOpt = 0; // performs optimized register correspondence p->fLatchCorrOpt = 0; // performs optimized register correspondence
...@@ -116,6 +117,16 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) ...@@ -116,6 +117,16 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
printf( "After BMC: " ); printf( "After BMC: " );
Ssw_ClassesPrint( p->ppClasses, 0 ); 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 // refine classes using induction
nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0; nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0;
for ( nIter = 0; ; nIter++ ) for ( nIter = 0; ; nIter++ )
...@@ -154,6 +165,18 @@ clk = clock(); ...@@ -154,6 +165,18 @@ clk = clock();
Ssw_ManCleanup( p ); Ssw_ManCleanup( p );
if ( !RetValue ) if ( !RetValue )
break; 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->pPars->nIters = nIter + 1;
p->timeTotal = clock() - clkTotal; p->timeTotal = clock() - clkTotal;
...@@ -220,6 +243,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) ...@@ -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 // 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_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 ); p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
} }
......
src/aig/ssw/sswInt.h
...@@ -62,7 +62,7 @@ struct Ssw_Man_t_ ...@@ -62,7 +62,7 @@ struct Ssw_Man_t_
// SAT solving // SAT solving
sat_solver * pSat; // recyclable SAT solver sat_solver * pSat; // recyclable SAT solver
int nSatVars; // the counter of SAT variables 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 int nSatVarsTotal; // the total number of SAT vars created
Vec_Ptr_t * vFanins; // fanins of the CNF node Vec_Ptr_t * vFanins; // fanins of the CNF node
// SAT solving (latch corr only) // SAT solving (latch corr only)
...@@ -118,8 +118,8 @@ struct Ssw_Man_t_ ...@@ -118,8 +118,8 @@ struct Ssw_Man_t_
/// MACRO DEFINITIONS /// /// MACRO DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
static inline int Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; } 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 ) { p->pSatVars[pObj->Id] = Num; } 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 ) 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 ...@@ -143,6 +143,9 @@ static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int
/*=== sswAig.c ===================================================*/ /*=== sswAig.c ===================================================*/
extern Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_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 =================================================*/ /*=== sswClass.c =================================================*/
extern Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig ); extern Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig );
extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData, extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
...@@ -150,6 +153,7 @@ 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 (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ); int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
extern void Ssw_ClassesStop( Ssw_Cla_t * p ); 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 Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p );
extern void Ssw_ClassesClearRefined( Ssw_Cla_t * p ); extern void Ssw_ClassesClearRefined( Ssw_Cla_t * p );
extern int Ssw_ClassesCand1Num( 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 ); ...@@ -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 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_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_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 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_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, 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 ...@@ -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_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 ); extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
/*=== sswSweep.c ===================================================*/ /*=== 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_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p );
......
src/aig/ssw/sswMan.c
...@@ -54,7 +54,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) ...@@ -54,7 +54,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
p->nFrames = pPars->nFramesK + 1; p->nFrames = pPars->nFramesK + 1;
p->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); p->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
// SAT solving // 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 ); p->vFanins = Vec_PtrAlloc( 100 );
// SAT solving (latch corr only) // SAT solving (latch corr only)
p->vUsedNodes = Vec_PtrAlloc( 1000 ); p->vUsedNodes = Vec_PtrAlloc( 1000 );
...@@ -147,11 +147,14 @@ void Ssw_ManCleanup( Ssw_Man_t * p ) ...@@ -147,11 +147,14 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
} }
if ( p->pSat ) if ( p->pSat )
{ {
int i;
// printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size ); // printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size );
p->nSatVarsTotal += p->pSat->size; p->nSatVarsTotal += p->pSat->size;
sat_solver_delete( p->pSat ); sat_solver_delete( p->pSat );
p->pSat = NULL; 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 ) if ( p->vSimInfo )
{ {
...@@ -186,8 +189,8 @@ void Ssw_ManStop( Ssw_Man_t * p ) ...@@ -186,8 +189,8 @@ void Ssw_ManStop( Ssw_Man_t * p )
Vec_PtrFree( p->vFanins ); Vec_PtrFree( p->vFanins );
Vec_PtrFree( p->vUsedNodes ); Vec_PtrFree( p->vUsedNodes );
Vec_PtrFree( p->vUsedPis ); Vec_PtrFree( p->vUsedPis );
Vec_IntFree( p->vSatVars );
FREE( p->pNodeToFrames ); FREE( p->pNodeToFrames );
FREE( p->pSatVars );
FREE( p->pPatWords ); FREE( p->pPatWords );
free( p ); free( p );
} }
......
src/aig/ssw/sswSweep.c
...@@ -156,14 +156,14 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f ) ...@@ -156,14 +156,14 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
SeeAlso [] 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; Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue; int RetValue;
// get representative of this class // get representative of this class
pObjRepr = Aig_ObjRepr( p->pAig, pObj ); pObjRepr = Aig_ObjRepr( p->pAig, pObj );
if ( pObjRepr == NULL ) if ( pObjRepr == NULL )
return; return 0;
// get the fraiged node // get the fraiged node
pObjFraig = Ssw_ObjFrame( p, pObj, f ); pObjFraig = Ssw_ObjFrame( p, pObj, f );
// get the fraiged representative // get the fraiged representative
...@@ -179,7 +179,7 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) ...@@ -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 the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
return; return 0;
// count the number of skipped calls // count the number of skipped calls
if ( !pObj->fMarkA && !pObjRepr->fMarkA ) if ( !pObj->fMarkA && !pObjRepr->fMarkA )
p->nRefSkip++; p->nRefSkip++;
...@@ -196,13 +196,12 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) ...@@ -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 ); pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 ); Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
return; return 0;
} }
if ( RetValue == -1 ) // timed out if ( RetValue == -1 ) // timed out
{ {
Ssw_ClassesRemoveNode( p->ppClasses, pObj ); Ssw_ClassesRemoveNode( p->ppClasses, pObj );
p->fRefined = 1; return 1;
return;
} }
// check if skipping calls works correctly // check if skipping calls works correctly
if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA ) 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 ) ...@@ -218,7 +217,7 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
else else
Ssw_ManResimulateBit( p, pObj, pObjRepr ); Ssw_ManResimulateBit( p, pObj, pObjRepr );
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
p->fRefined = 1; return 1;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -262,7 +261,7 @@ clk = clock(); ...@@ -262,7 +261,7 @@ clk = clock();
Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL ); 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) ); pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew ); 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 // quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 ) if ( f == p->pPars->nFramesK - 1 )
...@@ -351,13 +350,13 @@ p->timeMarkCones += clock() - clk; ...@@ -351,13 +350,13 @@ p->timeMarkCones += clock() - clk;
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL ); Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) ) 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) ) else if ( Aig_ObjIsNode(pObj) )
{ {
pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA; 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) ); pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew ); Ssw_ObjSetFrame( p, pObj, f, pObjNew );
Ssw_ManSweepNode( p, pObj, f, 0 ); p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
} }
} }
p->nSatFailsTotal += p->nSatFailsReal; p->nSatFailsTotal += p->nSatFailsReal;
......
src/base/abci/abc.c
...@@ -13535,7 +13535,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -13535,7 +13535,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults // set defaults
Ssw_ManSetDefaultParams( pPars ); Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsfvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -13625,6 +13625,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -13625,6 +13625,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's': case 's':
pPars->fSkipCheck ^= 1; pPars->fSkipCheck ^= 1;
break; break;
case 'f':
pPars->fSemiFormal ^= 1;
break;
case 'v': case 'v':
pPars->fVerbose ^= 1; pPars->fVerbose ^= 1;
break; break;
...@@ -13677,7 +13680,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -13677,7 +13680,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsvh]\n" ); fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsfvh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
...@@ -13689,6 +13692,7 @@ usage: ...@@ -13689,6 +13692,7 @@ usage:
fprintf( pErr, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" ); fprintf( pErr, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" ); fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
fprintf( pErr, "\t-s : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "yes": "no" ); fprintf( pErr, "\t-s : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "yes": "no" );
fprintf( pErr, "\t-f : toggle filtering using interative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-h : print the command usage\n");
return 1; return 1;
......
src/misc/vec/vecInt.h
...@@ -424,6 +424,25 @@ static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry ) ...@@ -424,6 +424,25 @@ static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void Vec_IntWriteEntryFill( Vec_Int_t * p, int i, int Entry )
{
assert( i >= 0 );
if ( i >= p->nSize )
Vec_IntFillExtra( p, 2 * i, 0 );
Vec_IntWriteEntry( p, i, Entry );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntShrink( Vec_Int_t * p, int nSizeNew ) static inline void Vec_IntShrink( Vec_Int_t * p, int nSizeNew )
{ {
assert( p->nSize >= nSizeNew ); assert( p->nSize >= nSizeNew );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment