summaryrefslogtreecommitdiffstats
path: root/src/base/main/mainInt.h
blob: e860878ec9a56a861f672f3786246fa715c46452 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
/**CFile****************************************************************

  FileName    [mainInt.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [The main package.]

  Synopsis    [Internal declarations of the main package.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: mainInt.h,v 1.1 2008/05/14 22:13:13 wudenni Exp $]

***********************************************************************/

#ifndef ABC__base__main__mainInt_h
#define ABC__base__main__mainInt_h

 
////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

#include "main.h"
#include "misc/tim/tim.h"
#include "map/if/if.h"
#include "aig/aig/aig.h"
#include "aig/gia/gia.h"
#include "proof/ssw/ssw.h"
#include "proof/fra/fra.h"

#ifdef ABC_USE_CUDD
#include "bdd/extrab/extraBdd.h"
#endif

ABC_NAMESPACE_HEADER_START

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////

// the current version
#define ABC_VERSION "UC Berkeley, ABC 1.01"

// the maximum length of an input line 
#define ABC_MAX_STR     (1<<15)

////////////////////////////////////////////////////////////////////////
///                    STRUCTURE DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

typedef void (*Abc_Frame_Callback_BmcFrameDone_Func)(int frame, int po, int status);

struct Abc_Frame_t_
{
    // general info
    char *          sVersion;      // the name of the current version
    char *          sBinary;       // the name of the binary running
    // commands, aliases, etc
    st__table *      tCommands;     // the command table
    st__table *      tAliases;      // the alias table
    st__table *      tFlags;        // the flag table
    Vec_Ptr_t *     aHistory;      // the command history
    // the functionality
    Abc_Ntk_t *     pNtkCur;       // the current network
    Abc_Ntk_t *     pNtkBestDelay; // the current network
    Abc_Ntk_t *     pNtkBestArea;  // the current network
    Abc_Ntk_t *     pNtkBackup;    // the current network
    int             nSteps;        // the counter of different network processed
    int             fSource;       // marks the source mode
    int             fAutoexac;     // marks the autoexec mode
    int             fBatchMode;    // batch mode flag
    int             fBridgeMode;   // bridge mode flag
    // save/load
    Abc_Ntk_t *     pNtkBest;        // the current network
    float           nBestNtkArea;   // best area
    float           nBestNtkDelay;  // best delay
    int             nBestNtkNodes;  // best nodes
    int             nBestNtkLevels; // best levels

    // output streams
    FILE *          Out;
    FILE *          Err;
    FILE *          Hst;
    // used for runtime measurement
    double          TimeCommand;   // the runtime of the last command
    double          TimeTotal;     // the total runtime of all commands
    // temporary storage for structural choices
    Vec_Ptr_t *     vStore;        // networks to be used by choice
    // decomposition package    
    void *          pManDec;       // decomposition manager
    void *          pManDsd;       // decomposition manager
    void *          pManDsd2;      // decomposition manager
    // libraries for mapping
    void *          pLibLut;       // the current LUT library
    void *          pLibBox;       // the current box library
    void *          pLibGen;       // the current genlib
    void *          pLibGen2;      // the current genlib
    void *          pLibSuper;     // the current supergate library
    void *          pLibScl;       // the current Liberty library
    void *          pAbcCon;       // constraint manager
    // timing constraints
    char *          pDrivingCell;  // name of the driving cell
    float           MaxLoad;       // maximum output load
    // inductive don't-cares
    Vec_Int_t *     vIndFlops;
    int             nIndFrames;

    // new code
    Gia_Man_t *     pGia;          // alternative current network as a light-weight AIG
    Gia_Man_t *     pGia2;         // copy of the above
    Gia_Man_t *     pGiaBest;      // copy of the above
    Gia_Man_t *     pGiaBest2;     // copy of the above
    Gia_Man_t *     pGiaSaved;     // copy of the above
    int             nBestLuts;     // best LUT count
    int             nBestEdges;    // best edge count
    int             nBestLevels;   // best level count
    int             nBestLuts2;     // best LUT count
    int             nBestEdges2;    // best edge count
    int             nBestLevels2;   // best level count
    Abc_Cex_t *     pCex;          // a counter-example to fail the current network
    Abc_Cex_t *     pCex2;         // copy of the above
    Vec_Ptr_t *     vCexVec;       // a vector of counter-examples if more than one PO fails
    Vec_Ptr_t *     vPoEquivs;     // equivalence classes of isomorphic primary outputs
    Vec_Int_t *     vStatuses;     // problem status for each output
    Vec_Int_t *     vAbcObjIds;    // object IDs
    int             Status;                // the status of verification problem (proved=1, disproved=0, undecided=-1)
    int             nFrames;               // the number of time frames completed by BMC
    Vec_Ptr_t *     vPlugInComBinPairs;    // pairs of command and its binary name
    Vec_Ptr_t *     vLTLProperties_global; // related to LTL
    Vec_Ptr_t *     vSignalNames;  // temporary storage for signal names
    char *          pSpecName;
    void *          pSave1; 
    void *          pSave2; 
    void *          pSave3; 
    void *          pSave4; 
    void *          pAbc85Ntl;
    void *          pAbc85Ntl2;
    void *          pAbc85Best;
    void *          pAbc85Delay;
    void *          pAbcWlc;
    Vec_Int_t *     pAbcWlcInv;
    void *          pAbcBac;
    void *          pAbcCba;
    void *          pAbcPla;
    Abc_Nam_t *     pJsonStrs;
    Vec_Wec_t *     vJsonObjs;
#ifdef ABC_USE_CUDD
    DdManager *     dd;            // temporary BDD package
#endif
    Gia_Man_t *     pGiaMiniAig; 
    Gia_Man_t *     pGiaMiniLut; 
    Vec_Int_t *     vCopyMiniAig;
    Vec_Int_t *     vCopyMiniLut;
    int *           pArray;
    int *           pBoxes;
    void *          pNdr;
    int *           pNdrArray;

    Abc_Frame_Callback_BmcFrameDone_Func pFuncOnFrameDone;
};

typedef void (*Abc_Frame_Initialization_Func)( Abc_Frame_t * pAbc );

struct Abc_FrameInitializer_t_;
typedef struct Abc_FrameInitializer_t_ Abc_FrameInitializer_t;

struct Abc_FrameInitializer_t_
{
    Abc_Frame_Initialization_Func init;
    Abc_Frame_Initialization_Func destroy;

    Abc_FrameInitializer_t* next;
    Abc_FrameInitializer_t* prev;
};

////////////////////////////////////////////////////////////////////////
///                       GLOBAL VARIABLES                           ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                       MACRO DEFINITIONS                          ///
////////////////////////////////////////////////////////////////////////


////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/*=== mvMain.c ===========================================================*/
extern ABC_DLL int             main( int argc, char * argv[] );
/*=== mvInit.c ===================================================*/
extern ABC_DLL void            Abc_FrameInit( Abc_Frame_t * pAbc );
extern ABC_DLL void            Abc_FrameEnd( Abc_Frame_t * pAbc );
extern ABC_DLL void            Abc_FrameAddInitializer( Abc_FrameInitializer_t* p );
/*=== mvFrame.c =====================================================*/
extern ABC_DLL Abc_Frame_t *   Abc_FrameAllocate();
extern ABC_DLL void            Abc_FrameDeallocate( Abc_Frame_t * p );
/*=== mvUtils.c =====================================================*/
extern ABC_DLL char *          Abc_UtilsGetVersion( Abc_Frame_t * pAbc );
extern ABC_DLL char *          Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc );
extern ABC_DLL void            Abc_UtilsPrintHello( Abc_Frame_t * pAbc );
extern ABC_DLL void            Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName );
extern ABC_DLL void            Abc_UtilsSource( Abc_Frame_t * pAbc );



ABC_NAMESPACE_HEADER_END

#endif

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////