1 /**CFile****************************************************************
2 
3   FileName    [mainInt.h]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [The main package.]
8 
9   Synopsis    [Internal declarations of the main package.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 20, 2005.]
16 
17   Revision    [$Id: mainInt.h,v 1.1 2008/05/14 22:13:13 wudenni Exp $]
18 
19 ***********************************************************************/
20 
21 #ifndef ABC__base__main__mainInt_h
22 #define ABC__base__main__mainInt_h
23 
24 
25 ////////////////////////////////////////////////////////////////////////
26 ///                          INCLUDES                                ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 #include "main.h"
30 #include "misc/tim/tim.h"
31 #include "map/if/if.h"
32 #include "aig/aig/aig.h"
33 #include "aig/gia/gia.h"
34 #include "proof/ssw/ssw.h"
35 #include "proof/fra/fra.h"
36 
37 #ifdef ABC_USE_CUDD
38 #include "bdd/extrab/extraBdd.h"
39 #endif
40 
41 ABC_NAMESPACE_HEADER_START
42 
43 ////////////////////////////////////////////////////////////////////////
44 ///                         PARAMETERS                               ///
45 ////////////////////////////////////////////////////////////////////////
46 
47 // the current version
48 #define ABC_VERSION "UC Berkeley, ABC 1.01"
49 
50 // the maximum length of an input line
51 #define ABC_MAX_STR     (1<<15)
52 
53 ////////////////////////////////////////////////////////////////////////
54 ///                    STRUCTURE DEFINITIONS                         ///
55 ////////////////////////////////////////////////////////////////////////
56 
57 typedef void (*Abc_Frame_Callback_BmcFrameDone_Func)(int frame, int po, int status);
58 
59 struct Abc_Frame_t_
60 {
61     // general info
62     char *          sVersion;      // the name of the current version
63     char *          sBinary;       // the name of the binary running
64     // commands, aliases, etc
65     st__table *      tCommands;     // the command table
66     st__table *      tAliases;      // the alias table
67     st__table *      tFlags;        // the flag table
68     Vec_Ptr_t *     aHistory;      // the command history
69     // the functionality
70     Abc_Ntk_t *     pNtkCur;       // the current network
71     Abc_Ntk_t *     pNtkBestDelay; // the current network
72     Abc_Ntk_t *     pNtkBestArea;  // the current network
73     Abc_Ntk_t *     pNtkBackup;    // the current network
74     int             nSteps;        // the counter of different network processed
75     int             fSource;       // marks the source mode
76     int             fAutoexac;     // marks the autoexec mode
77     int             fBatchMode;    // batch mode flag
78     int             fBridgeMode;   // bridge mode flag
79     // save/load
80     Abc_Ntk_t *     pNtkBest;        // the current network
81     float           nBestNtkArea;   // best area
82     float           nBestNtkDelay;  // best delay
83     int             nBestNtkNodes;  // best nodes
84     int             nBestNtkLevels; // best levels
85 
86     // output streams
87     FILE *          Out;
88     FILE *          Err;
89     FILE *          Hst;
90     // used for runtime measurement
91     double          TimeCommand;   // the runtime of the last command
92     double          TimeTotal;     // the total runtime of all commands
93     // temporary storage for structural choices
94     Vec_Ptr_t *     vStore;        // networks to be used by choice
95     // decomposition package
96     void *          pManDec;       // decomposition manager
97     void *          pManDsd;       // decomposition manager
98     void *          pManDsd2;      // decomposition manager
99     // libraries for mapping
100     void *          pLibLut;       // the current LUT library
101     void *          pLibBox;       // the current box library
102     void *          pLibGen;       // the current genlib
103     void *          pLibGen2;      // the current genlib
104     void *          pLibSuper;     // the current supergate library
105     void *          pLibScl;       // the current Liberty library
106     void *          pAbcCon;       // constraint manager
107     // timing constraints
108     char *          pDrivingCell;  // name of the driving cell
109     float           MaxLoad;       // maximum output load
110     // inductive don't-cares
111     Vec_Int_t *     vIndFlops;
112     int             nIndFrames;
113 
114     // new code
115     Gia_Man_t *     pGia;          // alternative current network as a light-weight AIG
116     Gia_Man_t *     pGia2;         // copy of the above
117     Gia_Man_t *     pGiaBest;      // copy of the above
118     Gia_Man_t *     pGiaBest2;     // copy of the above
119     Gia_Man_t *     pGiaSaved;     // copy of the above
120     int             nBestLuts;     // best LUT count
121     int             nBestEdges;    // best edge count
122     int             nBestLevels;   // best level count
123     int             nBestLuts2;     // best LUT count
124     int             nBestEdges2;    // best edge count
125     int             nBestLevels2;   // best level count
126     Abc_Cex_t *     pCex;          // a counter-example to fail the current network
127     Abc_Cex_t *     pCex2;         // copy of the above
128     Vec_Ptr_t *     vCexVec;       // a vector of counter-examples if more than one PO fails
129     Vec_Ptr_t *     vPoEquivs;     // equivalence classes of isomorphic primary outputs
130     Vec_Int_t *     vStatuses;     // problem status for each output
131     Vec_Int_t *     vAbcObjIds;    // object IDs
132     int             Status;                // the status of verification problem (proved=1, disproved=0, undecided=-1)
133     int             nFrames;               // the number of time frames completed by BMC
134     Vec_Ptr_t *     vPlugInComBinPairs;    // pairs of command and its binary name
135     Vec_Ptr_t *     vLTLProperties_global; // related to LTL
136     void *          pSave1;
137     void *          pSave2;
138     void *          pSave3;
139     void *          pSave4;
140     void *          pAbc85Ntl;
141     void *          pAbc85Ntl2;
142     void *          pAbc85Best;
143     void *          pAbc85Delay;
144     void *          pAbcWlc;
145     Vec_Int_t *     pAbcWlcInv;
146     void *          pAbcBac;
147     void *          pAbcCba;
148     void *          pAbcPla;
149     Abc_Nam_t *     pJsonStrs;
150     Vec_Wec_t *     vJsonObjs;
151 #ifdef ABC_USE_CUDD
152     DdManager *     dd;            // temporary BDD package
153 #endif
154     Gia_Man_t *     pGiaMiniAig;
155     Gia_Man_t *     pGiaMiniLut;
156     Vec_Int_t *     vCopyMiniAig;
157     Vec_Int_t *     vCopyMiniLut;
158     int *           pArray;
159     int *           pBoxes;
160     void *          pNdr;
161     int *           pNdrArray;
162 
163     Abc_Frame_Callback_BmcFrameDone_Func pFuncOnFrameDone;
164 };
165 
166 typedef void (*Abc_Frame_Initialization_Func)( Abc_Frame_t * pAbc );
167 
168 struct Abc_FrameInitializer_t_;
169 typedef struct Abc_FrameInitializer_t_ Abc_FrameInitializer_t;
170 
171 struct Abc_FrameInitializer_t_
172 {
173     Abc_Frame_Initialization_Func init;
174     Abc_Frame_Initialization_Func destroy;
175 
176     Abc_FrameInitializer_t* next;
177     Abc_FrameInitializer_t* prev;
178 };
179 
180 ////////////////////////////////////////////////////////////////////////
181 ///                       GLOBAL VARIABLES                           ///
182 ////////////////////////////////////////////////////////////////////////
183 
184 ////////////////////////////////////////////////////////////////////////
185 ///                       MACRO DEFINITIONS                          ///
186 ////////////////////////////////////////////////////////////////////////
187 
188 
189 ////////////////////////////////////////////////////////////////////////
190 ///                     FUNCTION DEFINITIONS                         ///
191 ////////////////////////////////////////////////////////////////////////
192 
193 /*=== mvMain.c ===========================================================*/
194 extern ABC_DLL int             main( int argc, char * argv[] );
195 /*=== mvInit.c ===================================================*/
196 extern ABC_DLL void            Abc_FrameInit( Abc_Frame_t * pAbc );
197 extern ABC_DLL void            Abc_FrameEnd( Abc_Frame_t * pAbc );
198 extern ABC_DLL void            Abc_FrameAddInitializer( Abc_FrameInitializer_t* p );
199 /*=== mvFrame.c =====================================================*/
200 extern ABC_DLL Abc_Frame_t *   Abc_FrameAllocate();
201 extern ABC_DLL void            Abc_FrameDeallocate( Abc_Frame_t * p );
202 /*=== mvUtils.c =====================================================*/
203 extern ABC_DLL char *          Abc_UtilsGetVersion( Abc_Frame_t * pAbc );
204 extern ABC_DLL char *          Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc );
205 extern ABC_DLL void            Abc_UtilsPrintHello( Abc_Frame_t * pAbc );
206 extern ABC_DLL void            Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName );
207 extern ABC_DLL void            Abc_UtilsSource( Abc_Frame_t * pAbc );
208 
209 
210 
211 ABC_NAMESPACE_HEADER_END
212 
213 #endif
214 
215 ////////////////////////////////////////////////////////////////////////
216 ///                       END OF FILE                                ///
217 ////////////////////////////////////////////////////////////////////////
218