source: vis_dev/vis-2.3/src/imc/imcInt.h @ 101

Last change on this file since 101 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 8.6 KB
RevLine 
[14]1/**CHeaderFile*****************************************************************
2
3  FileName    [imcInt.h]
4
5  PackageName [imc]
6
7  Synopsis    [Internal data type definitions and macros to handle the
8  structures of the imc package.]
9
10  Author      [Jae-Young Jang <jjang@vlsi.colorado.edu>]
11
12  Copyright [This file was created at the University of Colorado at Boulder.
13  The University of Colorado at Boulder makes no warranty about the suitability
14  of this software for any purpose.  It is presented on an AS IS basis.]
15
16  Revision    [$Id:]
17
18******************************************************************************/
19
20#ifndef _IMCINT
21#define _IMCINT
22
23/*---------------------------------------------------------------------------*/
24/* Nested includes                                                           */
25/*---------------------------------------------------------------------------*/
26
27#include "imc.h"
28#include "fsm.h"
29#include <string.h>
30
31/*---------------------------------------------------------------------------*/
32/* Constant declarations                                                     */
33/*---------------------------------------------------------------------------*/
34
35/*---------------------------------------------------------------------------*/
36/* Type declarations                                                         */
37/*---------------------------------------------------------------------------*/
38
39/*---------------------------------------------------------------------------*/
40/* Structure declarations                                                    */
41/*---------------------------------------------------------------------------*/
42
43/**Struct**********************************************************************
44
45  Synopsis    [Information for a total system.]
46
47  Description [Information for a total system.]
48
49  SeeAlso     [ImcInfoStruct]
50
51******************************************************************************/
52struct ImcSystemInfo{
53  st_table      *latchNameTable;      /* Names of latches in a system */
54  array_t       *latchNameArray;
55  array_t       *latchNodeArray;
56  array_t       *nsMddIdArray;
57  array_t       *psMddIdArray;
58  array_t       *inputMddIdArray;
59  array_t       *TRArray;
60  array_t       *lowerTRArray;
61  array_t       *mvfArray;
62  array_t       *latchSizeArray;
63  st_table      *nsMddIdToIndex;
64  st_table      *psMddIdToIndex;
65  array_t       *includedPsMddId; 
66  array_t       *includedNsMddId;
67  array_t       *includedLatchIndex;
68  array_t       *excludedPsMddId;
69  array_t       *excludedNsMddId;
70  array_t       *excludedLatchIndex;
71  st_table      *excludedPsMddIdTable;
72};
73
74 
75/**Struct**********************************************************************
76
77  Synopsis    [Information for an upper-bound approximate system.]
78
79  Description [Information for an upper-bound approximate system.]
80
81  SeeAlso     [ImcInfoStruct]
82
83******************************************************************************/
84struct ImcUpperSystemInfo{
85  Imc_SystemInfo_t *systemInfo;
86  mdd_t *careStates;
87  array_t *fwdRealationArray;
88  array_t *fwdSmoothVarsArray;
89  array_t *bwdRealationArray;
90  array_t *bwdMinimizedRealationArray;
91  array_t *bwdSmoothVarsArray;
92
93};
94
95/**Struct**********************************************************************
96
97  Synopsis    [Information for an upper-bound approximate system.]
98
99  Description [Information for an upper-bound approximate system.]
100
101  SeeAlso     [ImcInfoStruct]
102
103******************************************************************************/
104struct ImcLowerSystemInfo{
105  Imc_SystemInfo_t *systemInfo;
106  mdd_t *careStates;
107  array_t *bwdRealationArray;
108  array_t *bwdMinimizedRealationArray;
109  array_t *bwdSmoothVarsArray;
110};
111
112/**Struct**********************************************************************
113
114  Synopsis    [Information for nodes in opeerational graph.]
115
116  Description [Information for nodes in opeerational graph.]
117
118  SeeAlso     [ImcInfoStruct]
119
120******************************************************************************/
121struct ImcNodeInfo{
122  boolean                polarity;
123  boolean                isExact;
124  mdd_t                  *upperSat;   /* upper satisfying set */
125  mdd_t                  *lowerSat;   /* lower satisfying set */
126  boolean                upperDone;
127  boolean                lowerDone;
128  mdd_t                  *propagatedGoalSet;
129  mdd_t                  *propagatedGoalSetTrue;
130  mdd_t                  *goalSet;
131  mdd_t                  *goalSetTrue;
132  mdd_t                  *pseudoEdges;
133  Imc_VerificationResult answer; 
134};
135
136/**Struct**********************************************************************
137
138  Synopsis    [Information regarding the imc package.]
139
140  Description [This is a higher level of information related to the imc
141  verification.]
142
143  SeeAlso     [ImcSubsystemInfo]
144
145******************************************************************************/
146struct ImcInfoStruct{
147  /* General Info */
148  Ntk_Network_t          *network;         /* Corresponding network */
149  Fsm_Fsm_t              *globalFsm;       /* Global FSM */
150  boolean                useLocalFsm;
151  Imc_DcLevel            dcLevel;          /* Don't care level */
152  mdd_t                  *initialStates;   /* Initial states */
153  Ctlp_FormulaClass      formulaClass;     /* ECTL, ACTL, MIXED, QuantifierFree */
154  mdd_t                  *modelCareStates; /* Global care states */
155  Imc_VerbosityLevel     verbosity;        /* Verbosity */
156  Imc_RefineMethod       refine;           /* Refinement method */
157  Imc_VerificationResult result;           /* Verification Result */
158  mdd_manager            *mddMgr;          /* MDD Manager */
159  Imc_PartMethod         partMethod;
160  char                   *modelName;
161  Hrc_Node_t             *currentNode;
162
163  /* Image, Preimage computation Info */
164  array_t                *supportMddIdArray; /* don't free */
165  array_t                *preQMddIdArray;    /* don't free */
166  array_t                *imgQMddIdArray;    /* don't free */
167
168  /* Operational graph Info */
169  Imc_GraphType          graphType;        /* pDOG, nDOG, MOG */
170  st_table               *nodeInfoTable;   /* node info table */
171  boolean                needLower;
172  boolean                needUpper;
173
174  /* Incremental Verification dependent info */
175  Imc_SystemInfo_t       *systemInfo;      /* System info of total system */
176  int                    incrementalSize;  /* Number of transition sub-relations
177                                              to be refined at each refinement */ 
178
179  /* approximation and Dynamic Refinement dependent Info */
180  Imc_LowerMethod        lowerMethod;      /* Lower-bound approximation method */
181  Imc_UpperMethod        upperMethod;      /* Upper-bound approximation method */
182  Imc_UpperSystemInfo_t  *upperSystemInfo; /* Upper-bound approximate system */
183  Imc_LowerSystemInfo_t  *lowerSystemInfo; /* Lower-bound approximate system */
184  mdd_t                  *edges;           /* for edge traversal refinement */
185
186  /* approximation and Static Refinement dependent Info */
187  Part_CMethod           correlationMethod;
188  array_t                *staticRefineSchedule; /* Static refinement schedule */
189};
190
191/*---------------------------------------------------------------------------*/
192/* Variable declarations                                                     */
193/*---------------------------------------------------------------------------*/
194
195
196/*---------------------------------------------------------------------------*/
197/* Macro declarations                                                        */
198/*---------------------------------------------------------------------------*/
199
200
201/**AutomaticStart*************************************************************/
202
203/*---------------------------------------------------------------------------*/
204/* Function prototypes                                                       */
205/*---------------------------------------------------------------------------*/
206
207EXTERN array_t  * ImcCreateScheduleArray(Ntk_Network_t *network, Ctlp_Formula_t *formula, boolean dynamicIncrease, Imc_RefineMethod refine, int verbosity, int incrementalSize, Part_CMethod correlationMethod);
208EXTERN int ImcModelCheckAtomicFormula(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula);
209EXTERN int ImcModelCheckTrueFalseFormula(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isTrue);
210EXTERN int ImcModelCheckNotFormula(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper);
211EXTERN int ImcModelCheckAndFormula(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper);
212EXTERN void ImcPrintLatchInApproxSystem(Imc_Info_t *imcInfo);
213EXTERN void ImcNodeInfoTableFree(st_table *nodeInfoTable);
214
215/**AutomaticEnd***************************************************************/
216
217#endif /* _IMCINT */
218
219
220
221
222
223
224
225
226
227
228
229
Note: See TracBrowser for help on using the repository browser.