mainInt.h 8.9 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
/**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.]

Alan Mishchenko committed
17
  Revision    [$Id: mainInt.h,v 1.1 2008/05/14 22:13:13 wudenni Exp $]
Alan Mishchenko committed
18 19 20

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

21 22
#ifndef ABC__base__main__mainInt_h
#define ABC__base__main__mainInt_h
23

Alan Mishchenko committed
24
 
Alan Mishchenko committed
25 26 27 28 29
////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

#include "main.h"
30 31 32 33 34 35
#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"
36 37

#ifdef ABC_USE_CUDD
38
#include "bdd/extrab/extraBdd.h"
39
#endif
40 41

ABC_NAMESPACE_HEADER_START
Alan Mishchenko committed
42 43 44 45 46 47

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

// the current version
Alan Mishchenko committed
48
#define ABC_VERSION "UC Berkeley, ABC 1.01"
Alan Mishchenko committed
49 50

// the maximum length of an input line 
51
#define ABC_MAX_STR     (1<<15)
Alan Mishchenko committed
52 53 54 55 56

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

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

Alan Mishchenko committed
59 60 61
struct Abc_Frame_t_
{
    // general info
Alan Mishchenko committed
62
    char *          sVersion;      // the name of the current version
63
    char *          sBinary;       // the name of the binary running
Alan Mishchenko committed
64
    // commands, aliases, etc
65 66 67
    st__table *      tCommands;     // the command table
    st__table *      tAliases;      // the alias table
    st__table *      tFlags;        // the flag table
Alan Mishchenko committed
68
    Vec_Ptr_t *     aHistory;      // the command history
Alan Mishchenko committed
69
    // the functionality
Alan Mishchenko committed
70 71 72
    Abc_Ntk_t *     pNtkCur;       // the current network
    Abc_Ntk_t *     pNtkBestDelay; // the current network
    Abc_Ntk_t *     pNtkBestArea;  // the current network
73
    Abc_Ntk_t *     pNtkBackup;    // the current network
Alan Mishchenko committed
74
    int             nSteps;        // the counter of different network processed
75
    int             fSource;       // marks the source mode
Alan Mishchenko committed
76
    int             fAutoexac;     // marks the autoexec mode
77
    int             fBatchMode;    // batch mode flag
78
    int             fBridgeMode;   // bridge mode flag
79 80 81 82 83 84 85
    // 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

Alan Mishchenko committed
86 87 88 89 90
    // output streams
    FILE *          Out;
    FILE *          Err;
    FILE *          Hst;
    // used for runtime measurement
Alan Mishchenko committed
91 92
    double          TimeCommand;   // the runtime of the last command
    double          TimeTotal;     // the total runtime of all commands
Alan Mishchenko committed
93
    // temporary storage for structural choices
Alan Mishchenko committed
94
    Vec_Ptr_t *     vStore;        // networks to be used by choice
95
    // decomposition package    
Alan Mishchenko committed
96
    void *          pManDec;       // decomposition manager
97
    void *          pManDsd;       // decomposition manager
98
    void *          pManDsd2;      // decomposition manager
Alan Mishchenko committed
99
    // libraries for mapping
Alan Mishchenko committed
100
    void *          pLibLut;       // the current LUT library
Alan Mishchenko committed
101
    void *          pLibBox;       // the current box library
Alan Mishchenko committed
102 103 104
    void *          pLibGen;       // the current genlib
    void *          pLibGen2;      // the current genlib
    void *          pLibSuper;     // the current supergate library
105
    void *          pLibScl;       // the current Liberty library
106
    void *          pAbcCon;       // constraint manager
107 108 109
    // timing constraints
    char *          pDrivingCell;  // name of the driving cell
    float           MaxLoad;       // maximum output load
110 111 112
    // inductive don't-cares
    Vec_Int_t *     vIndFlops;
    int             nIndFrames;
Alan Mishchenko committed
113 114

    // new code
Alan Mishchenko committed
115 116
    Gia_Man_t *     pGia;          // alternative current network as a light-weight AIG
    Gia_Man_t *     pGia2;         // copy of the above
117
    Gia_Man_t *     pGiaBest;      // copy of the above
118 119
    Gia_Man_t *     pGiaBest2;     // copy of the above
    Gia_Man_t *     pGiaSaved;     // copy of the above
120 121 122
    int             nBestLuts;     // best LUT count
    int             nBestEdges;    // best edge count
    int             nBestLevels;   // best level count
123 124 125
    int             nBestLuts2;     // best LUT count
    int             nBestEdges2;    // best edge count
    int             nBestLevels2;   // best level count
Alan Mishchenko committed
126
    Abc_Cex_t *     pCex;          // a counter-example to fail the current network
127
    Abc_Cex_t *     pCex2;         // copy of the above
Alan Mishchenko committed
128 129
    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
130
    Vec_Int_t *     vStatuses;     // problem status for each output
131
    Vec_Int_t *     vAbcObjIds;    // object IDs
Alan Mishchenko committed
132 133 134 135
    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
136
    Vec_Ptr_t *     vSignalNames;  // temporary storage for signal names
137
    char *          pSpecName;
Alan Mishchenko committed
138 139 140 141
    void *          pSave1; 
    void *          pSave2; 
    void *          pSave3; 
    void *          pSave4; 
Alan Mishchenko committed
142 143 144 145
    void *          pAbc85Ntl;
    void *          pAbc85Ntl2;
    void *          pAbc85Best;
    void *          pAbc85Delay;
146
    void *          pAbcWlc;
Alan Mishchenko committed
147
    Vec_Int_t *     pAbcWlcInv;
148
    void *          pAbcRtl;
149
    void *          pAbcBac;
150
    void *          pAbcCba;
151
    void *          pAbcPla;
152 153
    Abc_Nam_t *     pJsonStrs;
    Vec_Wec_t *     vJsonObjs;
154 155 156
#ifdef ABC_USE_CUDD
    DdManager *     dd;            // temporary BDD package
#endif
157 158 159 160
    Gia_Man_t *     pGiaMiniAig; 
    Gia_Man_t *     pGiaMiniLut; 
    Vec_Int_t *     vCopyMiniAig;
    Vec_Int_t *     vCopyMiniLut;
161
    int *           pArray;
162
    int *           pBoxes;
163 164
    void *          pNdr;
    int *           pNdrArray;
165 166

    Abc_Frame_Callback_BmcFrameDone_Func pFuncOnFrameDone;
Alan Mishchenko committed
167 168
};

169 170 171 172 173 174 175 176 177 178 179 180 181 182
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;
};

Alan Mishchenko committed
183 184 185 186 187
////////////////////////////////////////////////////////////////////////
///                       GLOBAL VARIABLES                           ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
Alan Mishchenko committed
188
///                       MACRO DEFINITIONS                          ///
Alan Mishchenko committed
189 190 191 192
////////////////////////////////////////////////////////////////////////


////////////////////////////////////////////////////////////////////////
Alan Mishchenko committed
193
///                     FUNCTION DEFINITIONS                         ///
Alan Mishchenko committed
194
////////////////////////////////////////////////////////////////////////
Alan Mishchenko committed
195

Alan Mishchenko committed
196
/*=== mvMain.c ===========================================================*/
Alan Mishchenko committed
197
extern ABC_DLL int             main( int argc, char * argv[] );
Alan Mishchenko committed
198
/*=== mvInit.c ===================================================*/
Alan Mishchenko committed
199 200
extern ABC_DLL void            Abc_FrameInit( Abc_Frame_t * pAbc );
extern ABC_DLL void            Abc_FrameEnd( Abc_Frame_t * pAbc );
201
extern ABC_DLL void            Abc_FrameAddInitializer( Abc_FrameInitializer_t* p );
Alan Mishchenko committed
202
/*=== mvFrame.c =====================================================*/
Alan Mishchenko committed
203 204
extern ABC_DLL Abc_Frame_t *   Abc_FrameAllocate();
extern ABC_DLL void            Abc_FrameDeallocate( Abc_Frame_t * p );
Alan Mishchenko committed
205
/*=== mvUtils.c =====================================================*/
Alan Mishchenko committed
206 207 208 209 210
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 );
Alan Mishchenko committed
211

212 213 214 215


ABC_NAMESPACE_HEADER_END

Alan Mishchenko committed
216 217
#endif

Alan Mishchenko committed
218 219 220
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////