mirror of https://github.com/YosysHQ/abc.git
228 lines
9.3 KiB
C
228 lines
9.3 KiB
C
/**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"
|
|
#include "misc/vec/vecHsh.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[ABC_LUT_LIBS]; // 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 * pAbcRtl;
|
|
void * pAbcBac;
|
|
void * pAbcCba;
|
|
void * pAbcPla;
|
|
Abc_Nam_t * pJsonStrs;
|
|
Vec_Wec_t * vJsonObjs;
|
|
Hsh_VecMan_t * pHash;
|
|
#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;
|
|
Vec_Int_t * vMiniLutObjs;
|
|
Vec_Int_t * vObjDelays;
|
|
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 );
|
|
extern ABC_DLL void Abc_FrameStoreStart( Abc_Frame_t * pAbc );
|
|
extern ABC_DLL void Abc_FrameStoreStop( Abc_Frame_t * pAbc );
|
|
extern ABC_DLL void Abc_FrameStoreAdd( Abc_Frame_t * pAbc, Gia_Man_t * p );
|
|
extern ABC_DLL void Abc_FrameStorePrint( Abc_Frame_t * pAbc );
|
|
|
|
|
|
ABC_NAMESPACE_HEADER_END
|
|
|
|
#endif
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|