summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-09-05 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2008-09-05 08:01:00 -0700
commit092c7be0ffb89d869e8eaeb04de12779ce96e8b9 (patch)
treefe4ae0c41d0481c1c3f9eec7689f49cba58cd4e8
parent73c8aa7c400bab320cea56529241e1d396f1e0f5 (diff)
downloadabc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.tar.gz
abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.tar.bz2
abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.zip
Version abc80905
-rw-r--r--src/aig/dch/dchMan.c9
-rw-r--r--src/aig/dch/dchSimSat.c7
-rw-r--r--src/aig/fra/fraClass.c2
-rw-r--r--src/aig/fra/fraInd.c6
-rw-r--r--src/aig/ivy/ivyFraig.c7
-rw-r--r--src/aig/ssw/sswAig.c38
-rw-r--r--src/aig/ssw/sswClass.c59
-rw-r--r--src/aig/ssw/sswCore.c23
-rw-r--r--src/aig/ssw/sswInt.h4
-rw-r--r--src/aig/ssw/sswMan.c31
-rw-r--r--src/aig/ssw/sswSat.c80
-rw-r--r--src/aig/ssw/sswSimSat.c66
-rw-r--r--src/aig/ssw/sswSweep.c88
-rw-r--r--src/base/abci/abc.c8
14 files changed, 307 insertions, 121 deletions
diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c
index 6c005fbf..a5faa2a6 100644
--- a/src/aig/dch/dchMan.c
+++ b/src/aig/dch/dchMan.c
@@ -170,16 +170,21 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p )
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is not used
// var 1 is reserved for const1 node - add the clause
- Lit = toLit( 1 );
+ 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 );
- p->nSatVars = 2;
+ Dch_ObjSetSatNum( p, Aig_ManConst1(p->pAigFraig), p->nSatVars++ );
+
p->nRecycles++;
p->nCallsSince = 0;
}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c
index 1fefa6eb..7a6865bd 100644
--- a/src/aig/dch/dchSimSat.c
+++ b/src/aig/dch/dchSimSat.c
@@ -108,8 +108,11 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
if ( Aig_ObjIsPi(pObj) )
{
- Aig_Obj_t * pObjFraig = Dch_ObjFraig( pObj );
- int nVarNum = Dch_ObjSatNum( p, pObjFraig );
+ Aig_Obj_t * pObjFraig;
+ int nVarNum;
+ pObjFraig = Dch_ObjFraig( pObj );
+ assert( !Aig_IsComplement(pObjFraig) );
+ nVarNum = Dch_ObjSatNum( p, pObjFraig );
// get the value from the SAT solver
// (account for the fact that some vars may be minimized away)
pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 498ea758..442cf80e 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -296,7 +296,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue;
// skip the node with more that the given number of levels
- if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
+ if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
continue;
}
// hash the node by its simulation info
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 668c20cb..76c7abad 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -505,6 +505,7 @@ PRT( "Time", clock() - clk );
int nLitsOld = Fra_ClassesCountLits(p->pCla);
int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
+ int clk3 = clock();
if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
{
@@ -571,7 +572,7 @@ p->timeTrav += clock() - clk2;
// report the intermediate results
if ( pPars->fVerbose )
{
- printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. ",
+ printf( "%3d : Const = %6d. Cl = %6d. L = %6d. LR = %6d. ",
nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
if ( p->pCla->vImps )
@@ -579,7 +580,8 @@ p->timeTrav += clock() - clk2;
if ( p->pPars->fUse1Hot )
printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) );
printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
- printf( "\n" );
+ PRT( "T", clock() - clk3 );
+// printf( "\n" );
}
// perform sweeping
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index c306c394..25f7a3ef 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2226,7 +2226,7 @@ p->timeSatFail += clock() - clk;
int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
{
int pLits[2], RetValue1, clk;
-// int RetValue;
+ int RetValue;
// make sure the nodes are not complemented
assert( !Ivy_IsComplement(pNew) );
@@ -2261,8 +2261,8 @@ p->timeSat += clock() - clk;
{
p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
-// RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
-// assert( RetValue );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+ assert( RetValue );
// continue solving the other implication
p->nSatCallsUnsat++;
}
@@ -2533,6 +2533,7 @@ void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t *
Ivy_ObjSetFaninVec( pNode, vFanins );
}
Vec_PtrFree( vFrontier );
+ sat_solver_simplify( p->pSat );
}
/**Function*************************************************************
diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c
index 47f15e55..9304edc7 100644
--- a/src/aig/ssw/sswAig.c
+++ b/src/aig/ssw/sswAig.c
@@ -44,7 +44,8 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
{
Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;
// skip nodes without representative
- if ( (pObjRepr = Aig_ObjRepr(pAig, pObj)) == NULL )
+ pObjRepr = Aig_ObjRepr(pAig, pObj);
+ if ( pObjRepr == NULL )
return;
p->nConstrTotal++;
assert( pObjRepr->Id < pObj->Id );
@@ -53,16 +54,26 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
// get the new node of the representative
pObjReprNew = Ssw_ObjFraig( p, pObjRepr, iFrame );
// if this is the same node, no need to add constraints
- if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
- return;
+ if ( pObj->fPhase == pObjRepr->fPhase )
+ {
+ assert( pObjNew != Aig_Not(pObjReprNew) );
+ if ( pObjNew == pObjReprNew )
+ return;
+ }
+ else
+ {
+ assert( pObjNew != pObjReprNew );
+ if ( pObjNew == Aig_Not(pObjReprNew) )
+ return;
+ }
p->nConstrReduced++;
// these are different nodes - perform speculative reduction
pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
// set the new node
Ssw_ObjSetFraig( p, pObj, iFrame, pObjNew2 );
// add the constraint
- Aig_ObjCreatePo( pFrames, Aig_Regular(pObjNew) );
- Aig_ObjCreatePo( pFrames, Aig_Regular(pObjReprNew) );
+ Aig_ObjCreatePo( pFrames, pObjNew2 );
+ Aig_ObjCreatePo( pFrames, pObjNew );
}
/**Function*************************************************************
@@ -80,7 +91,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
- int i, k, f;
+ int i, f;
assert( p->pFrames == NULL );
assert( Aig_ManRegNum(p->pAig) > 0 );
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
@@ -90,18 +101,14 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
// create latches for the first frame
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
- // create PI nodes for the frames
- for ( f = 0; f < p->pPars->nFramesK; f++ )
- Aig_ManForEachPiSeq( p->pAig, pObj, i )
- Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) );
- // map constant nodes
- for ( f = 0; f < p->pPars->nFramesK; f++ )
- Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
-
// add timeframes
p->nConstrTotal = p->nConstrReduced = 0;
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
+ // map constants and PIs
+ Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
+ Aig_ManForEachPiSeq( p->pAig, pObj, i )
+ Ssw_ObjSetFraig( 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 );
@@ -113,7 +120,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
}
// transfer latch input to the latch outputs
- Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, k )
+ Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
}
// add the POs for the latch outputs of the last frame
@@ -124,6 +131,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
Aig_ManCleanup( pFrames );
// make sure the satisfying assignment is node assigned
assert( pFrames->pData == NULL );
+//Aig_ManShow( pFrames, 0, NULL );
return pFrames;
}
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index bf4883e3..c84a5d3d 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -425,15 +425,15 @@ void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs )
{
if ( fLatchCorr )
{
- if ( !Aig_ObjIsPi(pObj) )
+ if ( !Saig_ObjIsPi(p->pAig, pObj) )
continue;
}
else
{
- if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+ if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsPi(p->pAig, pObj) )
continue;
// skip the node with more that the given number of levels
- if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
+ if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
continue;
}
// check if the node belongs to the class of constant 1
@@ -556,7 +556,7 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
p = Ssw_ClassesStart( pAig );
// go through the nodes
p->nCands1 = 0;
- Aig_ManForEachObj( p->pAig, pObj, i )
+ Aig_ManForEachObj( pAig, pObj, i )
{
if ( fLatchCorr )
{
@@ -568,10 +568,10 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsLo(pAig, pObj) )
continue;
// skip the node with more that the given number of levels
- if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
+ if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
continue;
}
- Ssw_ObjSetConst1Cand( p->pAig, pObj );
+ Ssw_ObjSetConst1Cand( pAig, pObj );
p->nCands1++;
}
// allocate room for classes
@@ -708,6 +708,53 @@ int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Refine the group of constant 1 nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
+{
+ Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
+ int i;
+ // collect the nodes to be refined
+ Vec_PtrClear( p->vClassNew );
+ for ( i = 0; i < Vec_PtrSize(p->pAig->vObjs); i++ )
+ if ( p->pAig->pReprs[i] == Aig_ManConst1(p->pAig) )
+ {
+ pObj = Aig_ManObj( p->pAig, i );
+ if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
+ Vec_PtrPush( p->vClassNew, pObj );
+ }
+ // check if there is a new class
+ if ( Vec_PtrSize(p->vClassNew) == 0 )
+ return 0;
+ p->nCands1 -= Vec_PtrSize(p->vClassNew);
+ pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
+ Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
+ if ( Vec_PtrSize(p->vClassNew) == 1 )
+ return 1;
+ // create a new class composed of these nodes
+ ppClassNew = p->pMemClassesFree;
+ p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
+ Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+ {
+ ppClassNew[i] = pObj;
+ Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
+ }
+ Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
+ // refine them recursively
+ if ( fRecursive )
+ return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 1e314b78..6c19ab70 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -48,7 +48,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->nConstrs = 0; // treat the last nConstrs POs as seq constraints
p->nBTLimit = 1000; // conflict limit at a node
p->fPolarFlip = 0; // uses polarity adjustment
- p->fLatchCorr = 0; // performs register correspondence
+ p->fLatchCorr = 1; // performs register correspondence
p->fVerbose = 1; // verbose stats
p->nIters = 0; // the number of iterations performed
}
@@ -66,6 +66,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
+ Aig_Man_t * pAigNew;
Ssw_Man_t * p;
int RetValue, nIter, clk, clkTotal = clock();
// reset random numbers
@@ -75,27 +76,33 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// compute candidate equivalence classes
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
// refine classes using BMC
- Ssw_ClassesPrint( p->ppClasses, 0 );
+ if ( pPars->fVerbose )
+ Ssw_ClassesPrint( p->ppClasses, 0 );
Ssw_ManSweepBmc( p );
- Ssw_ClassesPrint( p->ppClasses, 0 );
+ Ssw_ManCleanup( p );
+ if ( pPars->fVerbose )
+ Ssw_ClassesPrint( p->ppClasses, 0 );
// refine classes using induction
for ( nIter = 0; ; nIter++ )
{
clk = clock();
- RetValue = Ssw_ManSweep(p);
+ RetValue = Ssw_ManSweep( p );
if ( pPars->fVerbose )
{
- printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. NR = %6d. ",
+ printf( "%3d : Const = %6d. Cl = %6d. L = %6d. LR = %6d. NR = %6d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
- p->nConstrTotal, p->nConstrReduced, p->nFrameNodes );
+ p->nConstrTotal, p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
PRT( "T", clock() - clk );
}
+ Ssw_ManCleanup( p );
if ( !RetValue )
break;
- }
+ }
p->timeTotal = clock() - clkTotal;
Ssw_ManStop( p );
- return Aig_ManDupRepr( pAig, 0 );
+ pAigNew = Aig_ManDupRepr( pAig, 0 );
+ Aig_ManSeqCleanup( pAigNew );
+ return pAigNew;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 0e54af32..21621c0d 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -55,7 +55,6 @@ struct Ssw_Man_t_
Aig_Man_t * pAig; // user-given AIG
Aig_Man_t * pFrames; // final AIG
Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes
- int nFrameNodes; // the number of nodes in the timeframes
// equivalence classes
Ssw_Cla_t * ppClasses; // equivalence classes of nodes
// Aig_Obj_t ** pReprsProved; // equivalences proved
@@ -70,6 +69,7 @@ struct Ssw_Man_t_
// constraints
int nConstrTotal; // the number of total constraints
int nConstrReduced; // the number of reduced constraints
+ int nStragers;
// SAT calls statistics
int nSatCalls; // the number of SAT calls
int nSatProof; // the number of proofs
@@ -136,6 +136,7 @@ extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr,
extern int Ssw_ClassesRefine( Ssw_Cla_t * p );
extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
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 );
/*=== sswMan.c ===================================================*/
@@ -148,6 +149,7 @@ extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj
extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== sswSimSat.c ===================================================*/
extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
+extern void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
/*=== sswSweep.c ===================================================*/
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 86144ebb..0b935daa 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -42,22 +42,25 @@
Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
Ssw_Man_t * p;
+ // prepare the sequential AIG
+ assert( Saig_ManRegNum(pAig) > 0 );
+ Aig_ManFanoutStart( pAig );
+ Aig_ManSetPioNumbers( pAig );
// create interpolation manager
p = ALLOC( Ssw_Man_t, 1 );
memset( p, 0, sizeof(Ssw_Man_t) );
p->pPars = pPars;
p->pAig = pAig;
p->nFrames = pPars->nFramesK + 1;
- Aig_ManFanoutStart( pAig );
+ p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
// SAT solving
p->nSatVars = 1;
- p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) );
+ p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * p->nFrames );
p->vFanins = Vec_PtrAlloc( 100 );
p->vSimRoots = Vec_PtrAlloc( 1000 );
p->vSimClasses = Vec_PtrAlloc( 1000 );
// equivalences proved
// p->pReprsProved = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
- p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
return p;
}
@@ -97,21 +100,19 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
{
printf( "Parameters: Frames = %d. Conf limit = %d. Constrs = %d.\n",
p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs );
- printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d.\n",
- Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig) );
- printf( "SAT solver: Vars = %d.\n", p->nSatVars );
- printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n",
+ printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. SAT vars = %d.\n",
+ Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), p->nSatVars );
+ printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d. Equivs = %d. Str = %d.\n",
p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal,
- p->nSatCallsSat, p->nSatFailsReal );
- printf( "Equivs : All = %6d.\n", Ssw_ManCountEquivs(p) );
+ p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p), p->nStragers );
printf( "Runtime statistics:\n" );
p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeSimSat-p->timeSat;
PRTP( "BMC ", p->timeBmc, p->timeTotal );
PRTP( "Spec reduce", p->timeReduce, p->timeTotal );
PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal );
PRTP( "SAT solving", p->timeSat, p->timeTotal );
- PRTP( " sat ", p->timeSatSat, p->timeTotal );
PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
+ PRTP( " sat ", p->timeSatSat, p->timeTotal );
PRTP( " undecided", p->timeSatUndec, p->timeTotal );
PRTP( "Other ", p->timeOther, p->timeTotal );
PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
@@ -135,14 +136,15 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
{
Aig_ManStop( p->pFrames );
p->pFrames = NULL;
+ memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
}
if ( p->pSat )
{
sat_solver_delete( p->pSat );
p->pSat = NULL;
- p->nSatVars = 0;
+// p->nSatVars = 0;
+ memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
}
- memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
p->nConstrTotal = 0;
p->nConstrReduced = 0;
}
@@ -192,11 +194,12 @@ void Ssw_ManStartSolver( Ssw_Man_t * p )
sat_solver_setnvars( p->pSat, 10000 );
// var 0 is not used
// var 1 is reserved for const1 node - add the clause
- Lit = toLit( 1 );
+ p->nSatVars = 1;
+ Lit = toLit( p->nSatVars );
if ( p->pPars->fPolarFlip )
Lit = lit_neg( Lit );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
- p->nSatVars = 2;
+ Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c
index 06abd2c9..90752baa 100644
--- a/src/aig/ssw/sswSat.c
+++ b/src/aig/ssw/sswSat.c
@@ -32,7 +32,7 @@
Synopsis [Runs equivalence test for the two nodes.]
- Description []
+ Description [Both nodes should be regular and different from each other.]
SideEffects []
@@ -42,13 +42,13 @@
int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
int nBTLimit = p->pPars->nBTLimit;
- int pLits[2], RetValue, RetValue1, status, clk;
+ int pLits[2], RetValue, RetValue1, clk;//, status;
p->nSatCalls++;
// sanity checks
- assert( !Aig_IsComplement(pNew) );
assert( !Aig_IsComplement(pOld) );
- assert( pNew != pOld );
+ assert( !Aig_IsComplement(pNew) );
+ assert( pOld != pNew );
if ( p->pSat == NULL )
Ssw_ManStartSolver( p );
@@ -57,14 +57,6 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
Ssw_CnfNodeAddToSolver( p, pOld );
Ssw_CnfNodeAddToSolver( p, pNew );
- // propagate unit clauses
- if ( p->pSat->qtail != p->pSat->qhead )
- {
- status = sat_solver_simplify(p->pSat);
- assert( status != 0 );
- assert( p->pSat->qtail == p->pSat->qhead );
- }
-
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
@@ -75,6 +67,10 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
}
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+
+ RetValue = sat_solver_simplify(p->pSat);
+ assert( RetValue != 0 );
+
clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
@@ -117,6 +113,10 @@ p->timeSatUndec += clock() - clk;
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
}
+
+ RetValue = sat_solver_simplify(p->pSat);
+ assert( RetValue != 0 );
+
clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
@@ -160,23 +160,45 @@ p->timeSatUndec += clock() - clk;
***********************************************************************/
int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
- int pLits[2], RetValue;
+ int pLits[2], RetValue, fComplNew;
+ Aig_Obj_t * pTemp;
// sanity checks
- assert( !Aig_IsComplement(pNew) );
- assert( !Aig_IsComplement(pOld) );
- assert( pNew != pOld );
+ assert( Aig_Regular(pOld) != Aig_Regular(pNew) );
+ // move constant to the old node
+ if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) )
+ {
+ assert( Aig_Regular(pOld) != Aig_ManConst1(p->pFrames) );
+ pTemp = pOld;
+ pOld = pNew;
+ pNew = pTemp;
+ }
+
+ // move complement to the new node
+ if ( Aig_IsComplement(pOld) )
+ {
+ pOld = Aig_Regular(pOld);
+ pNew = Aig_Not(pNew);
+ }
+
+ // start the solver
if ( p->pSat == NULL )
Ssw_ManStartSolver( p );
// if the nodes do not have SAT variables, allocate them
Ssw_CnfNodeAddToSolver( p, pOld );
- Ssw_CnfNodeAddToSolver( p, pNew );
+ Ssw_CnfNodeAddToSolver( p, Aig_Regular(pNew) );
+
+ // transform the new node
+ fComplNew = Aig_IsComplement( pNew );
+ pNew = Aig_Regular( pNew );
+ // consider the constant 1 case
if ( pOld == Aig_ManConst1(p->pFrames) )
{
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), !pNew->fPhase );
+ // add constaint A = 1 ----> A
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew );
if ( p->pPars->fPolarFlip )
{
if ( pNew->fPhase ) pLits[0] = lit_neg( pLits[0] );
@@ -186,10 +208,11 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
}
else
{
- // solve under assumptions
- // A = 1; B = 0 OR A = 1; B = 1
+ // 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), pOld->fPhase == pNew->fPhase );
+ pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), !fComplNew );
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
@@ -200,10 +223,9 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
- // solve under assumptions
- // A = 0; B = 1 OR A = 0; B = 0
+ // (!A v B)
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
- pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
+ pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew);
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
@@ -214,16 +236,6 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
}
-/*
- // propagate unit clauses
- if ( p->pSat->qtail != p->pSat->qhead )
- {
- int status;
- status = sat_solver_simplify(p->pSat);
- assert( status != 0 );
- assert( p->pSat->qtail == p->pSat->qhead );
- }
-*/
return 1;
}
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
index 5986c27a..868a016b 100644
--- a/src/aig/ssw/sswSimSat.c
+++ b/src/aig/ssw/sswSimSat.c
@@ -92,6 +92,32 @@ void Ssw_ManCollectTfoCands( Ssw_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2
/**Function*************************************************************
+ Synopsis [Retrives value of the PI in the original AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+{
+ Aig_Obj_t * pObjFraig;
+ int nVarNum, Value;
+ assert( Aig_ObjIsPi(pObj) );
+ pObjFraig = Ssw_ObjFraig( p, pObj, f );
+ nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
+ Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( Aig_Regular(pObjFraig)->fPhase ) Value ^= 1;
+ }
+ return Value;
+}
+
+/**Function*************************************************************
+
Synopsis [Resimulates the cone of influence of the solved nodes.]
Description []
@@ -108,11 +134,7 @@ void Ssw_ManResimulateSolved_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
Aig_ObjSetTravIdCurrent(p->pAig, pObj);
if ( Aig_ObjIsPi(pObj) )
{
- Aig_Obj_t * pObjFraig = Ssw_ObjFraig( p, pObj, f );
- int nVarNum = Ssw_ObjSatNum( p, pObjFraig );
- // get the value from the SAT solver
- // (account for the fact that some vars may be minimized away)
- pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
+ pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
return;
}
Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj), f );
@@ -194,6 +216,40 @@ void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, i
p->timeSimSat += clock() - clk;
}
+/**Function*************************************************************
+
+ Synopsis [Handle the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
+{
+ Aig_Obj_t * pObj;
+ int i, RetValue1, RetValue2, clk = clock();
+ // set the PI simulation information
+ Aig_ManConst1(p->pAig)->fMarkB = 1;
+ Aig_ManForEachPi( p->pAig, pObj, i )
+ pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
+ // simulate internal nodes
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+ & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+ // check equivalence classes
+ RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
+ RetValue2 = Ssw_ClassesRefine( p->ppClasses );
+ // make sure refinement happened
+ if ( Aig_ObjIsConst1(pRepr) )
+ assert( RetValue1 );
+ else
+ assert( RetValue2 );
+p->timeSimSat += clock() - clk;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 18796b20..0630de56 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -50,12 +50,33 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
return;
// get the fraiged node
pObjFraig = Ssw_ObjFraig( p, pObj, f );
- if ( pObjFraig == NULL )
- return;
+ assert( pObjFraig != NULL );
// get the fraiged representative
pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f );
- if ( pObjReprFraig == NULL )
+ assert( pObjReprFraig != NULL );
+ // check if constant 0 pattern distinquishes these nodes
+ if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
+ {
+ Aig_Obj_t * pObj;
+ int i;
+ if ( p->pSat->model.cap < p->pSat->size )
+ {
+ veci_resize(&p->pSat->model, 0);
+ for ( i = 0; i < p->pSat->size; i++ )
+ veci_push( &p->pSat->model, (int)l_False );
+ }
+ // set the values of SAT vars to be equal to the phase of the nodes
+ Aig_ManForEachObj( p->pFrames, pObj, i )
+ if ( Ssw_ObjSatNum( p, pObj ) )
+ {
+ int iVar = Ssw_ObjSatNum( p, pObj );
+ assert( iVar < p->pSat->size );
+ p->pSat->model.ptr[iVar] = (int)(p->pPars->fPolarFlip? 0 : (pObj->fPhase? l_True : l_False));
+ p->pSat->model.size = p->pSat->size;
+ }
+ p->nStragers++;
return;
+ }
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
{
@@ -63,10 +84,15 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
// p->pReprsProved[ pObj->Id ] = pObjRepr;
return;
}
- assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) );
- RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
+// assert( 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) );
+
if ( RetValue == -1 ) // timed out
{
+ assert( 0 );
Ssw_ClassesRemoveNode( p->ppClasses, pObj );
p->fRefined = 1;
return;
@@ -80,7 +106,8 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
return;
}
// disproved the equivalence
- Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
+// Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
+ Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
p->fRefined = 1;
}
@@ -110,7 +137,8 @@ clk = clock();
// sweep internal nodes
p->fRefined = 0;
- pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
+ if ( p->pPars->fVerbose )
+ pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// map constants and PIs
@@ -120,17 +148,18 @@ clk = clock();
// sweep internal nodes
Aig_ManForEachNode( p->pAig, pObj, i )
{
- Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
+ if ( p->pPars->fVerbose )
+ Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFraig( p, pObj, f, pObjNew );
Ssw_ManSweepNode( p, pObj, f );
}
}
- Bar_ProgressStop( pProgress );
+ if ( p->pPars->fVerbose )
+ Bar_ProgressStop( pProgress );
// cleanup
- Ssw_ClassesCheck( p->ppClasses );
- Ssw_ManCleanup( p );
+// Ssw_ClassesCheck( p->ppClasses );
p->timeBmc += clock() - clk;
return p->fRefined;
}
@@ -150,21 +179,21 @@ int Ssw_ManSweep( Ssw_Man_t * p )
{
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
- int nConstrPairs, clk, i, f = p->pPars->nFramesK;
+ int nConstrPairs, clk, i, f;
// perform speculative reduction
clk = clock();
// create timeframes
p->pFrames = Ssw_FramesWithClasses( p );
- p->nFrameNodes = Aig_ManNodeNum( p->pFrames );
// add constraints
+ Ssw_ManStartSolver( p );
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 );
- Ssw_NodesAreConstrained( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) );
+ Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
}
// build logic cones for register inputs
for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
@@ -175,25 +204,36 @@ clk = clock();
sat_solver_simplify( p->pSat );
p->timeReduce += clock() - clk;
- // map constants and PIs
+ // map constants and PIs of the last frame
+ f = p->pPars->nFramesK;
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+ // make sure LOs are assigned
+ Saig_ManForEachLo( p->pAig, pObj, i )
+ assert( Ssw_ObjFraig( p, pObj, f ) != NULL );
// sweep internal nodes
p->fRefined = 0;
- pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
- Aig_ManForEachNode( p->pAig, pObj, i )
+ if ( p->pPars->fVerbose )
+ pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
+ Aig_ManForEachObj( p->pAig, pObj, i )
{
- Bar_ProgressUpdate( pProgress, i, NULL );
- pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
- Ssw_ObjSetFraig( p, pObj, f, pObjNew );
- Ssw_ManSweepNode( p, pObj, f );
+ if ( p->pPars->fVerbose )
+ Bar_ProgressUpdate( pProgress, i, NULL );
+ if ( Saig_ObjIsLo(p->pAig, pObj) )
+ Ssw_ManSweepNode( p, pObj, f );
+ else if ( Aig_ObjIsNode(pObj) )
+ {
+ pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
+ Ssw_ObjSetFraig( p, pObj, f, pObjNew );
+ Ssw_ManSweepNode( p, pObj, f );
+ }
}
- Bar_ProgressStop( pProgress );
+ if ( p->pPars->fVerbose )
+ Bar_ProgressStop( pProgress );
// cleanup
- Ssw_ClassesCheck( p->ppClasses );
- Ssw_ManCleanup( p );
+// Ssw_ClassesCheck( p->ppClasses );
return p->fRefined;
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 90ee04b2..8df6f066 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -453,8 +453,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "fretime", Abc_CommandFlowRetime, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 );
- Cmd_CommandAdd( pAbc, "Sequential", "ssw", Abc_CommandSeqSweep, 1 );
- Cmd_CommandAdd( pAbc, "Sequential", "ssw2", Abc_CommandSeqSweep2, 1 );
+ Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 );
+ Cmd_CommandAdd( pAbc, "Sequential", "scorr", Abc_CommandSeqSweep2, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "testssw", Abc_CommandSeqSweepTest, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "lcorr", Abc_CommandLcorr, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 );
@@ -13482,7 +13482,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: ssw [-PQNFL num] [-lrfetvh]\n" );
+ fprintf( pErr, "usage: ssweep [-PQNFL num] [-lrfetvh]\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-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
@@ -13655,7 +13655,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: ssw2 [-PQFCLN num] [-plvh]\n" );
+ fprintf( pErr, "usage: scorr [-PQFCLN num] [-plvh]\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-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );