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