summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw')
-rw-r--r--src/aig/ssw/ssw.h1
-rw-r--r--src/aig/ssw/sswClass.c18
-rw-r--r--src/aig/ssw/sswCore.c3
-rw-r--r--src/aig/ssw/sswInt.h2
-rw-r--r--src/aig/ssw/sswIslands.c2
5 files changed, 19 insertions, 7 deletions
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 437e6ec8..e4a2619e 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -57,6 +57,7 @@ struct Ssw_Pars_t_
int TimeLimit; // time out in seconds
int fPolarFlip; // uses polarity adjustment
int fLatchCorr; // perform register correspondence
+ int fConstCorr; // perform constant correspondence
int fOutputCorr; // perform 'PO correspondence'
int fSemiFormal; // enable semiformal filtering
// int fUniqueness; // enable uniqueness constraints
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 7fd2a21b..a0e64cc0 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -39,6 +39,7 @@ struct Ssw_Cla_t_
Aig_Man_t * pAig; // original AIG manager
Aig_Obj_t *** pId2Class; // non-const classes by ID of repr node
int * pClassSizes; // sizes of each equivalence class
+ int fConstCorr;
// statistics
int nClasses; // the total number of non-const classes
int nCands1; // the total number of const candidates
@@ -496,7 +497,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
+int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr )
{
Aig_Man_t * pAig = p->pAig;
Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
@@ -522,6 +523,8 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
p->nCands1++;
continue;
}
+ if ( fConstCorr )
+ continue;
// hash the node by its simulation info
iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
// add the node to the class
@@ -590,7 +593,7 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
SeeAlso []
***********************************************************************/
-Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fOutputCorr, int nMaxLevs, int fVerbose )
+Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose )
{
// int nFrames = 4;
// int nWords = 1;
@@ -611,6 +614,7 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr,
// start the classes
p = Ssw_ClassesStart( pAig );
+ p->fConstCorr = fConstCorr;
// perform sequential simulation
clk = clock();
@@ -668,7 +672,7 @@ clk = clock();
p->pMemClassesFree = p->pMemClasses;
// now it is time to refine the classes
- Ssw_ClassesPrepareRehash( p, vCands );
+ Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
if ( fVerbose )
{
printf( "Collecting candidate equivalence classes. " );
@@ -688,7 +692,7 @@ clk = clock();
// perform new round of simulation
Ssw_SmlResimulateSeq( pSml );
// check equivalence classes
- RetValue = Ssw_ClassesPrepareRehash( p, vCands );
+ RetValue = Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
if ( RetValue == 0 )
break;
}
@@ -1110,6 +1114,12 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
// check if there is a new class
if ( Vec_PtrSize(p->vClassNew) == 0 )
return 0;
+ if ( p->fConstCorr )
+ {
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
+ Aig_ObjSetRepr( p->pAig, pObj, NULL );
+ return 1;
+ }
p->nCands1 -= Vec_PtrSize(p->vClassNew);
pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 76cc34fa..1f4d44d2 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -59,6 +59,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->nStepsMax = -1; // (scorr only) the max number of induction steps
p->fPolarFlip = 0; // uses polarity adjustment
p->fLatchCorr = 0; // performs register correspondence
+ p->fConstCorr = 0; // performs constant correspondence
p->fOutputCorr = 0; // perform 'PO correspondence'
p->fSemiFormal = 0; // enable semiformal filtering
p->fDynamic = 0; // dynamic partitioning
@@ -465,7 +466,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
else
{
// perform one round of seq simulation and generate candidate equivalence classes
- p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
+ p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
// p->ppClasses = Ssw_ClassesPrepareTargets( pAig );
if ( pPars->fLatchCorrOpt )
p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 );
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 189494bc..32959e85 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -219,7 +219,7 @@ extern void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr,
extern void Ssw_ClassesCheck( Ssw_Cla_t * p );
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 nFramesK, int fLatchCorr, int fOutputCorr, int nMaxLevs, int fVerbose );
+extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose );
extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
extern Ssw_Cla_t * Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig );
extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
diff --git a/src/aig/ssw/sswIslands.c b/src/aig/ssw/sswIslands.c
index d1ebe4bc..0802aca5 100644
--- a/src/aig/ssw/sswIslands.c
+++ b/src/aig/ssw/sswIslands.c
@@ -438,7 +438,7 @@ Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_
if ( p->pPars->fPartSigCorr )
p->ppClasses = Ssw_ClassesPreparePairsSimple( pMiter, vPairsMiter );
else
- p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
+ p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
if ( p->pPars->fDumpSRInit )
{
if ( p->pPars->fPartSigCorr )
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-02 14:19:44 +0000