1 /**CFile**************************************************************** 2 3 FileName [cec.h] 4 5 SystemName [ABC: Logic synthesis and verification system.] 6 7 PackageName [Combinational equivalence checking.] 8 9 Synopsis [External declarations.] 10 11 Author [Alan Mishchenko] 12 13 Affiliation [UC Berkeley] 14 15 Date [Ver. 1.0. Started - June 20, 2005.] 16 17 Revision [$Id: cec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] 18 19 ***********************************************************************/ 20 21 #ifndef ABC__aig__cec__cec_h 22 #define ABC__aig__cec__cec_h 23 24 25 //////////////////////////////////////////////////////////////////////// 26 /// INCLUDES /// 27 //////////////////////////////////////////////////////////////////////// 28 29 //////////////////////////////////////////////////////////////////////// 30 /// PARAMETERS /// 31 //////////////////////////////////////////////////////////////////////// 32 33 34 35 ABC_NAMESPACE_HEADER_START 36 37 38 //////////////////////////////////////////////////////////////////////// 39 /// BASIC TYPES /// 40 //////////////////////////////////////////////////////////////////////// 41 42 // dynamic SAT parameters 43 typedef struct Cec_ParSat_t_ Cec_ParSat_t; 44 struct Cec_ParSat_t_ 45 { 46 int nBTLimit; // conflict limit at a node 47 int nSatVarMax; // the max number of SAT variables 48 int nCallsRecycle; // calls to perform before recycling SAT solver 49 int fNonChrono; // use non-chronological backtracling (for circuit SAT only) 50 int fPolarFlip; // flops polarity of variables 51 int fCheckMiter; // the circuit is the miter 52 // int fFirstStop; // stop on the first sat output 53 int fLearnCls; // perform clause learning 54 int fSaveCexes; // saves counter-examples 55 int fVerbose; // verbose stats 56 }; 57 58 // simulation parameters 59 typedef struct Cec_ParSim_t_ Cec_ParSim_t; 60 struct Cec_ParSim_t_ 61 { 62 int nWords; // the number of simulation words 63 int nFrames; // the number of simulation frames 64 int nRounds; // the number of simulation rounds 65 int nNonRefines; // the max number of rounds without refinement 66 int TimeLimit; // the runtime limit in seconds 67 int fDualOut; // miter with separate outputs 68 int fCheckMiter; // the circuit is the miter 69 // int fFirstStop; // stop on the first sat output 70 int fSeqSimulate; // performs sequential simulation 71 int fLatchCorr; // consider only latch outputs 72 int fConstCorr; // consider only constants 73 int fVeryVerbose; // verbose stats 74 int fVerbose; // verbose stats 75 }; 76 77 // semiformal parameters 78 typedef struct Cec_ParSmf_t_ Cec_ParSmf_t; 79 struct Cec_ParSmf_t_ 80 { 81 int nWords; // the number of simulation words 82 int nRounds; // the number of simulation rounds 83 int nFrames; // the max number of time frames 84 int nNonRefines; // the max number of rounds without refinement 85 int nMinOutputs; // the min outputs to accumulate 86 int nBTLimit; // conflict limit at a node 87 int TimeLimit; // the runtime limit in seconds 88 int fDualOut; // miter with separate outputs 89 int fCheckMiter; // the circuit is the miter 90 // int fFirstStop; // stop on the first sat output 91 int fVerbose; // verbose stats 92 }; 93 94 // combinational SAT sweeping parameters 95 typedef struct Cec_ParFra_t_ Cec_ParFra_t; 96 struct Cec_ParFra_t_ 97 { 98 int nWords; // the number of simulation words 99 int nRounds; // the number of simulation rounds 100 int nItersMax; // the maximum number of iterations of SAT sweeping 101 int nBTLimit; // conflict limit at a node 102 int TimeLimit; // the runtime limit in seconds 103 int nLevelMax; // restriction on the level nodes to be swept 104 int nDepthMax; // the depth in terms of steps of speculative reduction 105 int fRewriting; // enables AIG rewriting 106 int fCheckMiter; // the circuit is the miter 107 // int fFirstStop; // stop on the first sat output 108 int fDualOut; // miter with separate outputs 109 int fColorDiff; // miter with separate outputs 110 int fSatSweeping; // enable SAT sweeping 111 int fRunCSat; // enable another solver 112 int fUseCones; // use cones 113 int fUseOrigIds; // enable recording of original IDs 114 int fVeryVerbose; // verbose stats 115 int fVerbose; // verbose stats 116 int iOutFail; // the failed output 117 }; 118 119 // combinational equivalence checking parameters 120 typedef struct Cec_ParCec_t_ Cec_ParCec_t; 121 struct Cec_ParCec_t_ 122 { 123 int nBTLimit; // conflict limit at a node 124 int TimeLimit; // the runtime limit in seconds 125 // int fFirstStop; // stop on the first sat output 126 int fUseSmartCnf; // use smart CNF computation 127 int fRewriting; // enables AIG rewriting 128 int fNaive; // performs naive SAT-based checking 129 int fSilent; // print no messages 130 int fVeryVerbose; // verbose stats 131 int fVerbose; // verbose stats 132 int iOutFail; // the number of failed output 133 }; 134 135 // sequential register correspodence parameters 136 typedef struct Cec_ParCor_t_ Cec_ParCor_t; 137 struct Cec_ParCor_t_ 138 { 139 int nWords; // the number of simulation words 140 int nRounds; // the number of simulation rounds 141 int nFrames; // the number of time frames 142 int nPrefix; // the number of time frames in the prefix 143 int nBTLimit; // conflict limit at a node 144 int nLevelMax; // (scorr only) the max number of levels 145 int nStepsMax; // (scorr only) the max number of induction steps 146 int fLatchCorr; // consider only latch outputs 147 int fConstCorr; // consider only constants 148 int fUseRings; // use rings 149 int fMakeChoices; // use equilvaences as choices 150 int fUseCSat; // use circuit-based solver 151 // int fFirstStop; // stop on the first sat output 152 int fUseSmartCnf; // use smart CNF computation 153 int fStopWhenGone; // quit when PO is not a candidate constant 154 int fVerboseFlops; // verbose stats 155 int fVeryVerbose; // verbose stats 156 int fVerbose; // verbose stats 157 // callback 158 void * pData; 159 void * pFunc; 160 }; 161 162 // sequential register correspodence parameters 163 typedef struct Cec_ParChc_t_ Cec_ParChc_t; 164 struct Cec_ParChc_t_ 165 { 166 int nWords; // the number of simulation words 167 int nRounds; // the number of simulation rounds 168 int nBTLimit; // conflict limit at a node 169 int fUseRings; // use rings 170 int fUseCSat; // use circuit-based solver 171 int fVeryVerbose; // verbose stats 172 int fVerbose; // verbose stats 173 }; 174 175 // sequential synthesis parameters 176 typedef struct Cec_ParSeq_t_ Cec_ParSeq_t; 177 struct Cec_ParSeq_t_ 178 { 179 int fUseLcorr; // enables latch correspondence 180 int fUseScorr; // enables signal correspondence 181 int nBTLimit; // (scorr/lcorr) conflict limit at a node 182 int nFrames; // (scorr/lcorr) the number of timeframes 183 int nLevelMax; // (scorr only) the max number of levels 184 int fConsts; // (scl only) merging constants 185 int fEquivs; // (scl only) merging equivalences 186 int fUseMiniSat; // enables MiniSat in lcorr/scorr 187 int nMinDomSize; // the size of minimum clock domain 188 int fVeryVerbose; // verbose stats 189 int fVerbose; // verbose stats 190 }; 191 192 //////////////////////////////////////////////////////////////////////// 193 /// MACRO DEFINITIONS /// 194 //////////////////////////////////////////////////////////////////////// 195 196 //////////////////////////////////////////////////////////////////////// 197 /// FUNCTION DECLARATIONS /// 198 //////////////////////////////////////////////////////////////////////// 199 200 /*=== cecCec.c ==========================================================*/ 201 extern int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars ); 202 extern int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose ); 203 extern int Cec_ManVerifySimple( Gia_Man_t * p ); 204 /*=== cecChoice.c ==========================================================*/ 205 extern Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars ); 206 /*=== cecCorr.c ==========================================================*/ 207 extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ); 208 extern Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ); 209 /*=== cecCore.c ==========================================================*/ 210 extern void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ); 211 extern void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p ); 212 extern void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p ); 213 extern void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p ); 214 extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ); 215 extern void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p ); 216 extern void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p ); 217 extern Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSilent ); 218 extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ); 219 extern void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ); 220 /*=== cecSeq.c ==========================================================*/ 221 extern int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex ); 222 extern int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ); 223 extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig ); 224 /*=== cecSynth.c ==========================================================*/ 225 extern int Cec_SeqReadMinDomSize( Cec_ParSeq_t * p ); 226 extern int Cec_SeqReadVerbose( Cec_ParSeq_t * p ); 227 extern void Cec_SeqSynthesisSetDefaultParams( Cec_ParSeq_t * pPars ); 228 extern int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars ); 229 230 231 232 ABC_NAMESPACE_HEADER_END 233 234 235 236 #endif 237 238 //////////////////////////////////////////////////////////////////////// 239 /// END OF FILE /// 240 //////////////////////////////////////////////////////////////////////// 241 242