diff options
Diffstat (limited to 'src/aig/cec/cec.h')
| -rw-r--r-- | src/aig/cec/cec.h | 100 |
1 files changed, 100 insertions, 0 deletions
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h new file mode 100644 index 00000000..fb0bb830 --- /dev/null +++ b/src/aig/cec/cec.h @@ -0,0 +1,100 @@ +/**CFile**************************************************************** + + FileName [cec.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CEC_H__ +#define __CEC_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// dynamic SAT parameters +typedef struct Cec_ParSat_t_ Cec_ParSat_t; +struct Cec_ParSat_t_ +{ + int nBTLimit; // conflict limit at a node + int nSatVarMax; // the max number of SAT variables + int nCallsRecycle; // calls to perform before recycling SAT solver + int fFirstStop; // stop on the first sat output + int fPolarFlip; // uses polarity adjustment + int fVerbose; // verbose stats +}; + +// combinational SAT sweeping parameters +typedef struct Cec_ParCsw_t_ Cec_ParCsw_t; +struct Cec_ParCsw_t_ +{ + int nWords; // the number of simulation words + int nRounds; // the number of simulation rounds + int nBTlimit; // conflict limit at a node + int fRewriting; // enables AIG rewriting + int fVerbose; // verbose stats +}; + +// combinational equivalence checking parameters +typedef struct Cec_ParCec_t_ Cec_ParCec_t; +struct Cec_ParCec_t_ +{ + int nIters; // iterations of SAT solving/sweeping + int nBTLimitBeg; // starting backtrack limit + int nBTlimitMulti; // multiple of backtrack limit + int fUseSmartCnf; // use smart CNF computation + int fRewriting; // enables AIG rewriting + int fSatSweeping; // enables SAT sweeping + int fFirstStop; // stop on the first sat output + int fVerbose; // verbose stats +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== cecCore.c ==========================================================*/ +extern void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ); +extern void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p ); +extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ); +extern int Cec_Solve( Aig_Man_t * pAig0, Aig_Man_t * pAig1, Cec_ParCec_t * p ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + |