blob: c008fc8be4577c226b5eaf72067244a751586bdd (
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
|
/**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 __MAIN_INT_H__
#define __MAIN_INT_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "main.h"
#include "tim.h"
#include "if.h"
#include "aig.h"
#include "gia.h"
#include "ssw.h"
#include "fra.h"
#include "nwkMerge.h"
#include "ntlnwk.h"
#include "ext.h"
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
// the current version
#define ABC_VERSION "UC Berkeley, ABC 1.01"
// the maximum length of an input line
#define MAX_STR 32768
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
struct Abc_Frame_t_
{
// general info
char * sVersion; // the name of the current version
// 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
int nSteps; // the counter of different network processed
int fAutoexac; // marks the autoexec mode
int fBatchMode; // are we invoked in batch mode?
// 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
DdManager * dd; // temporary BDD package
// libraries for mapping
void * pLibLut; // the current LUT library
void * pLibGen; // the current genlib
void * pLibGen2; // the current genlib
void * pLibSuper; // the current supergate library
void * pLibVer; // the current Verilog library
// new code
Ntl_Man_t * pAbc8Ntl; // the current design
Nwk_Man_t * pAbc8Nwk; // the current mapped network
Aig_Man_t * pAbc8Aig; // the current AIG
If_Lib_t * pAbc8Lib; // the current LUT library
If_Lib_t * pAbc85Lib; // the current LUT library
Gia_Man_t * pGia;
Gia_Man_t * pGia2;
Abc_Cex_t * pCex;
Vec_Ptr_t * vCexVec;
void * pSave1;
void * pSave2;
void * pSave3;
void * pSave4;
// related to LTL
Vec_Ptr_t * vLTLProperties_global;
// the addition to keep the best Ntl that can be used to restore
void * pAbc8NtlBestDelay; // the best delay, Ntl
void * pAbc8NtlBestArea; // the best area
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
EXT_ABC_FRAME // plugin for external functionality
};
////////////////////////////////////////////////////////////////////////
/// 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 );
/*=== 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 ///
////////////////////////////////////////////////////////////////////////
|
