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

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

vis2.3
File size: 8.8 KB
RevLine 
[14]1/**CHeaderFile*****************************************************************
2
3  FileName    [imc.h]
4
5  PackageName [imc]
6
7  Synopsis    [Model Check using over(under)-approximation with automatic
8  iterative refinement.]
9
10  Description []
11
12
13  Author      [Jae-Young Jang]
14
15  Copyright [This file was created at the University of Colorado at Boulder.
16  The University of Colorado at Boulder makes no warranty about the suitability
17  of this software for any purpose.  It is presented on an AS IS basis.]
18
19  Revision    [$Id:]
20
21******************************************************************************/
22
23#ifndef _IMC
24#define _IMC
25
26#include "part.h"
27#include "mc.h"
28
29/*---------------------------------------------------------------------------*/
30/* Constant declarations                                                     */
31/*---------------------------------------------------------------------------*/
32
33
34/*---------------------------------------------------------------------------*/
35/* Structure declarations                                                    */
36/*---------------------------------------------------------------------------*/
37
38/**Enum************************************************************************
39
40  Synopsis    [Verbosity Levels.]
41
42******************************************************************************/
43typedef enum {
44  Imc_VerbosityNone_c,
45  Imc_VerbosityMin_c,
46  Imc_VerbosityMax_c
47} Imc_VerbosityLevel;
48
49/**Enum************************************************************************
50
51  Synopsis    [Refinement method.]
52
53******************************************************************************/
54typedef enum {
55  Imc_RefineSort_c,
56  Imc_RefineLatchRelation_c
57} Imc_RefineMethod;
58
59/**Enum************************************************************************
60
61  Synopsis    [Extent to which don't cares are used in Imc functions.]
62
63******************************************************************************/
64
65typedef enum {
66  Imc_DcLevelNone_c,
67  Imc_DcLevelRch_c,
68  Imc_DcLevelMax_c,
69  Imc_DcLevelArdc_c
70} Imc_DcLevel;
71
72/**Enum************************************************************************
73
74  Synopsis    [Type of a verification result.]
75
76******************************************************************************/
77typedef enum {
78  Imc_VerificationTrue_c,
79  Imc_VerificationFalse_c,
80  Imc_VerificationInconclusive_c,
81  Imc_VerificationRefine_c,
82  Imc_VerificationError_c
83} Imc_VerificationResult;
84
85/**Enum************************************************************************
86
87  Synopsis    [Type of an operational graph.]
88
89******************************************************************************/
90typedef enum {
91  Imc_GraphNDOG_c,
92  Imc_GraphPDOG_c,
93  Imc_GraphMOG_c
94} Imc_GraphType;
95
96/**Enum************************************************************************
97
98  Synopsis    [Type of a polarity in a graph.]
99
100******************************************************************************/
101typedef enum {
102  Imc_PolarityNeg_c,
103  Imc_PolarityPos_c,
104  Imc_PolarityBoth_c
105} Imc_Polarity;
106
107/**Enum************************************************************************
108
109  Synopsis    [Upper bound approximation computation method.]
110
111******************************************************************************/
112typedef enum {
113  Imc_UpperExistentialQuantification_c
114} Imc_UpperMethod;
115
116/**Enum************************************************************************
117
118  Synopsis    [Lower bound approximation computation method.]
119
120******************************************************************************/
121typedef enum {
122  Imc_LowerSubsetTR_c,
123  Imc_LowerUniversalQuantification_c
124} Imc_LowerMethod;
125
126/**Enum************************************************************************
127
128  Synopsis    [Partition Method.]
129
130******************************************************************************/
131typedef enum {
132  Imc_PartAll_c,
133  Imc_PartDepend_c,
134  Imc_PartInc_c
135} Imc_PartMethod;
136
137/*---------------------------------------------------------------------------*/
138/* Type declarations                                                         */
139/*---------------------------------------------------------------------------*/
140typedef struct ImcInfoStruct Imc_Info_t;
141typedef struct ImcUpperSystemInfo Imc_UpperSystemInfo_t;
142typedef struct ImcLowerSystemInfo Imc_LowerSystemInfo_t;
143typedef struct ImcSystemInfo Imc_SystemInfo_t;
144typedef struct ImcNodeInfo Imc_NodeInfo_t;
145
146/*---------------------------------------------------------------------------*/
147/* Variable declarations                                                     */
148/*---------------------------------------------------------------------------*/
149
150
151/*---------------------------------------------------------------------------*/
152/* Macro declarations                                                        */
153/*---------------------------------------------------------------------------*/
154
155
156/**AutomaticStart*************************************************************/
157
158/*---------------------------------------------------------------------------*/
159/* Function prototypes                                                       */
160/*---------------------------------------------------------------------------*/
161
162EXTERN void Imc_Init(void);
163EXTERN void Imc_End(void);
164EXTERN Imc_VerificationResult Imc_ImcEvaluateFormulaLinearRefine(Ntk_Network_t *network, Ctlp_Formula_t *orgFormula, Ctlp_Formula_t *formula, Ctlp_FormulaClass formulaClass, int incrementalSize, Imc_VerbosityLevel verbosity, Imc_RefineMethod refine, mdd_t *careStates, Fsm_Fsm_t *exactFsm, Imc_DcLevel dcLevel, Imc_GraphType graphType, Imc_LowerMethod lowerMethod, Imc_UpperMethod upperMethod, boolean computeExact, boolean needLower, boolean needUpper, Imc_PartMethod partMethod, Hrc_Node_t *currentNode, char *modelName);
165EXTERN Imc_VerificationResult Imc_ImcVerifyFormula(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula);
166EXTERN Imc_VerificationResult Imc_SatCheck(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula);
167EXTERN Imc_Info_t * Imc_ImcInfoInitialize(Ntk_Network_t *network, Ctlp_Formula_t *formula, Ctlp_FormulaClass formulaClass, Imc_VerbosityLevel verbosity, Imc_RefineMethod refine, mdd_t *careStates, Imc_DcLevel dcLevel, int incrementalSize, Imc_GraphType graphType, Fsm_Fsm_t *exactFsm, Imc_LowerMethod lowerMethod, Imc_UpperMethod upperMethod, boolean computeExact, boolean needLower, boolean needUpper, Imc_PartMethod partMethod, Hrc_Node_t *currentNode, char *modelName);
168EXTERN void Imc_ImcInfoFree(Imc_Info_t *imcInfo);
169EXTERN void Imc_SystemInfoInitialize(Imc_Info_t *imcInfo, st_table *globalLatchNameTable, st_table *initialLatchNameTable);
170EXTERN void Imc_SystemInfoFree(Imc_SystemInfo_t *systemInfo);
171EXTERN void Imc_ImcSystemInfoUpdate(Imc_Info_t *imcInfo, st_table *newLatchNameTable);
172EXTERN void Imc_UpperSystemInfoInitialize(Imc_Info_t *imcInfo, st_table *latchNameTable);
173EXTERN void Imc_UpperSystemMinimize(Imc_Info_t *imcInfo, mdd_t *careStates);
174EXTERN void Imc_UpperSystemInfoFree(Imc_UpperSystemInfo_t *upperSystem);
175EXTERN void Imc_LowerSystemInfoInitialize(Imc_Info_t *imcInfo, st_table *latchNameTable);
176EXTERN void Imc_LowerSystemMinimize(Imc_Info_t *imcInfo, mdd_t *careStates);
177EXTERN void Imc_LowerSystemInfoFree(Imc_LowerSystemInfo_t *lowerSystem);
178EXTERN Imc_NodeInfo_t * Imc_NodeInfoInitialize(Imc_Polarity polarity);
179EXTERN void Imc_NodeInfoReset(Imc_Info_t *imcInfo);
180EXTERN void Imc_NodeInfoFree(Imc_NodeInfo_t *nodeInfo);
181EXTERN void Imc_ImcPrintSystemSize(Imc_Info_t *imcInfo);
182EXTERN void Imc_ImcPrintApproxSystemSize(Imc_Info_t *imcInfo);
183EXTERN mdd_t * Imc_GetUpperSat(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula);
184EXTERN mdd_t * Imc_GetLowerSat(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula);
185EXTERN int Imc_ImcEvaluateCTLFormula(Imc_Info_t *imcInfo, Ctlp_Formula_t *ctlFormula, Imc_Polarity polarity);
186EXTERN int Imc_ImcEvaluateEXApprox(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper, boolean isRecomputation);
187EXTERN int Imc_ImcEvaluateEUApprox(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper, boolean isRecomputation);
188EXTERN int Imc_ImcEvaluateEGApprox(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper, boolean isRecomputation);
189EXTERN mdd_t * Imc_ComputeUpperPreimage(Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact);
190EXTERN mdd_t * Imc_ComputeApproxPreimageByQuantification(Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact, boolean computeLower);
191EXTERN mdd_t * Imc_ComputeLowerPreimage(Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact);
192EXTERN mdd_t * Imc_ComputeLowerPreimageBySubsetTR(Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact);
193EXTERN mdd_t * Imc_ProductAbstract(mdd_manager *mddMgr, array_t *relationArray, array_t *smoothVarsMddIdArray, mdd_t *toStates);
194
195/**AutomaticEnd***************************************************************/
196
197#endif /* _IMC */
Note: See TracBrowser for help on using the repository browser.