1 /**CFile**************************************************************** 2 3 FileName [pdr.h] 4 5 SystemName [ABC: Logic synthesis and verification system.] 6 7 PackageName [Property driven reachability.] 8 9 Synopsis [External declarations.] 10 11 Author [Alan Mishchenko] 12 13 Affiliation [UC Berkeley] 14 15 Date [Ver. 1.0. Started - November 20, 2010.] 16 17 Revision [$Id: pdr.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $] 18 19 ***********************************************************************/ 20 21 #ifndef ABC__sat__pdr__pdr_h 22 #define ABC__sat__pdr__pdr_h 23 24 25 ABC_NAMESPACE_HEADER_START 26 27 28 //////////////////////////////////////////////////////////////////////// 29 /// INCLUDES /// 30 //////////////////////////////////////////////////////////////////////// 31 32 //////////////////////////////////////////////////////////////////////// 33 /// PARAMETERS /// 34 //////////////////////////////////////////////////////////////////////// 35 36 //////////////////////////////////////////////////////////////////////// 37 /// BASIC TYPES /// 38 //////////////////////////////////////////////////////////////////////// 39 40 typedef struct Pdr_Par_t_ Pdr_Par_t; 41 struct Pdr_Par_t_ 42 { 43 // int iOutput; // zero-based number of primary output to solve 44 int nRecycle; // limit on vars for recycling 45 int nFrameMax; // limit on frame count 46 int nConfLimit; // limit on SAT solver conflicts 47 int nConfGenLimit; // limit on SAT solver conflicts during generalization 48 int nRestLimit; // limit on the number of proof-obligations 49 int nTimeOut; // timeout in seconds 50 int nTimeOutGap; // approximate timeout in seconds since the last change 51 int nTimeOutOne; // approximate timeout in seconds per one output 52 int nRandomSeed; // value to seed the SAT solver with 53 int fTwoRounds; // use two rounds for generalization 54 int fMonoCnf; // monolythic CNF 55 int fNewXSim; // updated X-valued simulation 56 int fFlopPrio; // use structural flop priorities 57 int fFlopOrder; // order flops for 'analyze_final' during generalization 58 int fDumpInv; // dump inductive invariant 59 int fUseSupp; // use support in the invariant 60 int fShortest; // forces bug traces to be shortest 61 int fShiftStart; // allows clause pushing to start from an intermediate frame 62 int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe 63 int fSimpleGeneral; // simplified generalization 64 int fSkipGeneral; // skips expensive generalization step 65 int fSkipDown; // skips the application of down 66 int fCtgs; // handle CTGs in down 67 int fUseAbs; // use abstraction 68 int fUseSimpleRef; // simplified CEX refinement 69 int fVerbose; // verbose output` 70 int fVeryVerbose; // very verbose output 71 int fNotVerbose; // not printing line by line progress 72 int fSilent; // totally silent execution 73 int fSolveAll; // do not stop when found a SAT output 74 int fStoreCex; // enable storing counter-examples in MO mode 75 int fUseBridge; // use bridge interface 76 int fUsePropOut; // use property output 77 int nFailOuts; // the number of failed outputs 78 int nDropOuts; // the number of timed out outputs 79 int nProveOuts; // the number of proved outputs 80 int iFrame; // explored up to this frame 81 int RunId; // PDR id in this run 82 int(*pFuncStop)(int); // callback to terminate 83 int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode 84 abctime timeLastSolved; // the time when the last output was solved 85 Vec_Int_t * vOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided) 86 char * pInvFileName; // invariable file name 87 }; 88 89 //////////////////////////////////////////////////////////////////////// 90 /// MACRO DEFINITIONS /// 91 //////////////////////////////////////////////////////////////////////// 92 93 //////////////////////////////////////////////////////////////////////// 94 /// FUNCTION DECLARATIONS /// 95 //////////////////////////////////////////////////////////////////////// 96 97 /*=== pdrCore.c ==========================================================*/ 98 extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ); 99 extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars ); 100 101 102 ABC_NAMESPACE_HEADER_END 103 104 105 #endif 106 107 //////////////////////////////////////////////////////////////////////// 108 /// END OF FILE /// 109 //////////////////////////////////////////////////////////////////////// 110 111