1 /**CFile**************************************************************** 2 3 FileName [llb.h] 4 5 SystemName [ABC: Logic synthesis and verification system.] 6 7 PackageName [BDD-based reachability.] 8 9 Synopsis [External declarations.] 10 11 Author [Alan Mishchenko] 12 13 Affiliation [UC Berkeley] 14 15 Date [Ver. 1.0. Started - May 8, 2010.] 16 17 Revision [$Id: llb.h,v 1.00 2010/05/08 00:00:00 alanmi Exp $] 18 19 ***********************************************************************/ 20 21 #ifndef ABC__aig__llb__llb_h 22 #define ABC__aig__llb__llb_h 23 24 25 //////////////////////////////////////////////////////////////////////// 26 /// INCLUDES /// 27 //////////////////////////////////////////////////////////////////////// 28 29 //////////////////////////////////////////////////////////////////////// 30 /// PARAMETERS /// 31 //////////////////////////////////////////////////////////////////////// 32 33 34 ABC_NAMESPACE_HEADER_START 35 36 37 //////////////////////////////////////////////////////////////////////// 38 /// BASIC TYPES /// 39 //////////////////////////////////////////////////////////////////////// 40 41 typedef struct Gia_ParLlb_t_ Gia_ParLlb_t; 42 struct Gia_ParLlb_t_ 43 { 44 int nBddMax; // maximum BDD size 45 int nIterMax; // maximum iteration count 46 int nClusterMax; // maximum cluster size 47 int nHintDepth; // the number of times to cofactor 48 int HintFirst; // the number of first hint to use 49 int fUseFlow; // use flow computation 50 int nVolumeMax; // the largest volume 51 int nVolumeMin; // the smallest volume 52 int nPartValue; // partitioning value 53 int fBackward; // enable backward reachability 54 int fReorder; // enable dynamic variable reordering 55 int fIndConstr; // extract inductive constraints 56 int fUsePivots; // use internal pivot variables 57 int fCluster; // use partition clustering 58 int fSchedule; // use cluster scheduling 59 int fDumpReached; // dump reached states into a file 60 int fVerbose; // print verbose information 61 int fVeryVerbose; // print dependency matrices 62 int fSilent; // do not print any infomation 63 int fSkipReach; // skip reachability (preparation phase only) 64 int fSkipOutCheck; // does not check the property output 65 int TimeLimit; // time limit for one reachability run 66 int TimeLimitGlo; // time limit for all reachability runs 67 // internal parameters 68 abctime TimeTarget; // the time to stop 69 int iFrame; // explored up to this frame 70 }; 71 72 //////////////////////////////////////////////////////////////////////// 73 /// MACRO DEFINITIONS /// 74 //////////////////////////////////////////////////////////////////////// 75 76 //////////////////////////////////////////////////////////////////////// 77 /// FUNCTION DECLARATIONS /// 78 //////////////////////////////////////////////////////////////////////// 79 80 /*=== llbCore.c ==========================================================*/ 81 extern void Llb_ManSetDefaultParams( Gia_ParLlb_t * pPars ); 82 /*=== llb4Nonlin.c ==========================================================*/ 83 extern int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ); 84 85 86 87 ABC_NAMESPACE_HEADER_END 88 89 90 91 #endif 92 93 //////////////////////////////////////////////////////////////////////// 94 /// END OF FILE /// 95 //////////////////////////////////////////////////////////////////////// 96 97