summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2009-04-24 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2009-04-24 08:01:00 -0700
commitd7a048d738381651b53340684e26f06b78b8a78c (patch)
tree82f7bea9d0750a388494e6fffceb61cfeff969b7 /src/aig/ssw
parent77fab468ad32d15de5c065c211f6f74371670940 (diff)
downloadabc-d7a048d738381651b53340684e26f06b78b8a78c.tar.gz
abc-d7a048d738381651b53340684e26f06b78b8a78c.tar.bz2
abc-d7a048d738381651b53340684e26f06b78b8a78c.zip
Version abc90424
Diffstat (limited to 'src/aig/ssw')
-rw-r--r--src/aig/ssw/ssw.h2
-rw-r--r--src/aig/ssw/sswCore.c7
2 files changed, 9 insertions, 0 deletions
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index adb98401..c2a33ee4 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -61,6 +61,8 @@ struct Ssw_Pars_t_
int fLocalSim; // enable local simulation simulation
int fPartSigCorr; // uses partial signal correspondence
int nIsleDist; // extends islands by the given distance
+ int fScorrGia; // new signal correspondence implementation
+ int fUseCSat; // new SAT solver using when fScorrGia is selected
int fVerbose; // verbose stats
int fFlopVerbose; // verbose printout of redundant flops
// optimized latch correspondence
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 56b37fbe..41123ca4 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -277,6 +277,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
|| (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
return Ssw_SignalCorrespondencePart( pAig, pPars );
}
+
+ if ( pPars->fScorrGia )
+ {
+ extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
+ return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
+ }
+
// start the induction manager
p = Ssw_ManCreate( pAig, pPars );
// compute candidate equivalence classes