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