source: vis_dev/vis-2.3/src/img/img.h @ 17

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

vis2.3
File size: 17.5 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [img.h]
4
5  PackageName [img]
6
7  Synopsis    [Methods for performing image computations.]
8
9  Description [The image package is used to compute the image (forward or
10  backward) of a set under a vector of functions.  The functions are given by
11  a graph of multi-valued functions (MVFs). This graph is built using the
12  partition package. Each vertex in this graph has an MVF and an MDD id.  The
13  fanins of a vertex v give those vertices upon which the MVF at v depends.
14  The vector of functions to use for an image computation, the "roots", is
15  specified by an array of (names of) vertices of the graph.  The domain
16  variables are the variables over which "from" sets are defined for forward
17  images, and "to" sets are defined for backward images.  The range variables
18  are the variables over which "to" sets are defined for forward images, and
19  "from" sets are defined for backward images.  The quantify variables are
20  additional variables over which the functions are defined; this set is
21  disjoint from domain variables.  These variables are existentially
22  quantified from the results of backward image computation. <p>
23 
24  Computing images is fundamental to many symbolic analysis techniques, and
25  methods for computing images efficiently is an area of ongoing research.
26  For this reason, the image package has been designed with lots of
27  flexibility to easily allow new methods to be integrated (to add a new
28  method, see the instructions in imgInt.h).  Applications that use the image
29  package can switch among different image methods simply by specifying the
30  method type in the image initialization routine.  By using the returned
31  structure (Img_ImageInfo_t) from the initialization routine, all subsequent
32  (forward or backward) image computations will be done using the specified
33  method.<p>
34 
35  VIS users can control which image method is used by appropriately setting
36  the "image_method" flag.  Also, VIS users can set flags to control
37  parameters for different image computation methods.  Because the user has
38  the ability to change the values of these flags, Img_ImageInfo_t structs
39  should be freed and re-initialized whenever the VIS user changes the value
40  of these flags.<p>
41 
42  Following are descriptions of the methods implemented. In the descriptions,
43  x=x_1,...x_n is the set of domain variables, u=u_1,...,u_k is the set of
44  quantify variables, y=y_1,...,y_m is the set of range variables, and
45  f=f_1(x,u),...,f_m(x,u) is the set of functions under which we wish to
46  compute images.<p>
47 
48  <b>Monolithic:</b> This is the most naive approach possible.  A single
49  relation T(x,y) is constructed during the initialization phase, using the
50  computation (exists u (prod_i(y_i = f_i(x,u)))). To compute the forward
51  image, where fromUpperBound=U(x), fromLowerBound=L(x), and toCareSet=C(y),
52  we first compute a set A(x) between U(x) and L(x).  Then, T(x,y) is
53  simplified with respect to A(x) and C(y) to get T*.  Finally, x is
54  quantified from T* to produce the final answer.  Backward images are
55  computed analogously.  The monolithic method does not recognize any
56  user-settable flags for image computation.<p>
57
58  <b>IWLS95:</b> This technique is based on the early quantification heuristic.
59  The initialization process consists of following steps:   
60  <UL>
61  <LI> Create the relation of the roots at the bit level
62  in terms of the quantify and domain variables.
63  <LI> Order the bit level relations.
64  <LI> Group the relations of bits together, making a cluster
65  whenever the BDD size reaches a threshold.
66  <LI> For each cluster, quantify out the quantify variables which
67  are local to that particular cluster.
68  <LI> Order the clusters using the algorithm given in
69  "Efficient BDD Algorithms for FSM Synthesis and
70  Verification", by R. K. Ranjan et. al. in the proceedings of
71  IWLS'95{1}.
72  <LI> The orders of the clusters for forward and backward image are
73  calculated and stored. Also stored is the schedule of
74  variables for early quantification.
75  </UL>
76  For forward and backward image computation the corresponding
77  routines are called with appropriate ordering of clusters and
78  early quantification schedule. <p>]
79
80  Author      [Rajeev Ranjan, Tom Shiple, Abelardo Pardo, In-Ho Moon]
81
82  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
83  All rights reserved.
84
85  Permission is hereby granted, without written agreement and without license
86  or royalty fees, to use, copy, modify, and distribute this software and its
87  documentation for any purpose, provided that the above copyright notice and
88  the following two paragraphs appear in all copies of this software.
89
90  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
91  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
92  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
93  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
94
95  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
96  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
97  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
98  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
99  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
100
101  Revision    [$Id: img.h,v 1.50 2005/05/15 01:03:36 jinh Exp $]
102
103******************************************************************************/
104
105#ifndef _IMG
106#define _IMG
107
108#include "vm.h"
109#include "ntk.h"
110
111/*---------------------------------------------------------------------------*/
112/* Constant declarations                                                     */
113/*---------------------------------------------------------------------------*/
114
115/* This is a threshold for finding dependent variables. */
116#define IMG_MAX_DEP_SIZE        20
117
118/*---------------------------------------------------------------------------*/
119/* Structure declarations                                                     */
120/*---------------------------------------------------------------------------*/
121
122/*---------------------------------------------------------------------------*/
123/* Type declarations                                                         */
124/*---------------------------------------------------------------------------*/
125typedef struct ImgImageInfoStruct Img_ImageInfo_t;
126
127/**Enum************************************************************************
128
129  Synopsis    [Methods for image computation.  See the description in img.h.]
130
131******************************************************************************/
132typedef enum {
133  Img_Monolithic_c,
134  Img_Iwls95_c,
135  Img_Mlp_c,
136  Img_Tfm_c, /* transition function method */
137  Img_Hybrid_c, /* hybrid image comutation */
138  Img_Linear_c,
139  Img_Linear_Range_c,
140  Img_Default_c
141} Img_MethodType;
142
143
144/**Enum************************************************************************
145
146  Synopsis    [Type to indicate the direction of image computation.]
147
148  Description [Type to indicate the direction of image computation.  When an
149  imageInfo structure is initialized, the application must specify what
150  "directions" of image computation will be performed: forward, backward, or
151  both.]
152
153******************************************************************************/
154typedef enum {
155  Img_Forward_c,
156  Img_Backward_c,
157  Img_Both_c
158} Img_DirectionType;
159
160
161/**Enum************************************************************************
162
163  Synopsis    [Type to indicate image minimization method.]
164
165  Description [Type to indicate image minimization method.]
166
167******************************************************************************/
168typedef enum {
169  Img_Restrict_c, /* default */
170  Img_Constrain_c,
171  Img_Compact_c,
172  Img_Squeeze_c,
173  Img_And_c,
174  Img_OrNot_c,
175  Img_DefaultMinimizeMethod_c /* refer to img_minimize_method */
176} Img_MinimizeType;
177
178/**Enum************************************************************************
179
180  Synopsis    [Image substitute direction]
181
182******************************************************************************/
183typedef enum {
184  Img_D2R_c,    /* domain to range */
185  Img_R2D_c     /* range to domain */
186} Img_SubstituteDir;
187
188/**Enum************************************************************************
189
190  Synopsis    [State variables optimization direction]
191
192******************************************************************************/
193typedef enum {
194  Opt_None,
195  Opt_CS,
196  Opt_NS,
197  Opt_Both
198} Img_OptimizeType;
199
200/*---------------------------------------------------------------------------*/
201/* Variable declarations                                                     */
202/*---------------------------------------------------------------------------*/
203
204
205/*---------------------------------------------------------------------------*/
206/* Macro declarations                                                        */
207/*---------------------------------------------------------------------------*/
208
209/**AutomaticStart*************************************************************/
210
211/*---------------------------------------------------------------------------*/
212/* Function prototypes                                                       */
213/*---------------------------------------------------------------------------*/
214
215EXTERN int Img_ImageBuildFwdLFPRelation(Ntk_Network_t *network, Img_ImageInfo_t *imageInfo, mdd_t *constraint, int whichTime, int *maxTime, int *numBlocks);
216EXTERN void Img_PrintHybridOptions(void);
217EXTERN mdd_t* Img_MultiwayLinearAndSmooth(mdd_manager *mddManager, array_t *relationArray, array_t *smoothVarMddIdArray, array_t *introducedVarMddIdArray, Img_MethodType method, Img_DirectionType direction);
218EXTERN void Img_PrintPartitionedTransitionRelation(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
219EXTERN void Img_ReorderPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
220EXTERN void Img_UpdateQuantificationSchedule(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
221EXTERN void Img_ClusterRelationArray(mdd_manager *mddManager, Img_MethodType method, Img_DirectionType direction, array_t *relationArray, array_t *domainVarMddIdArray, array_t *rangeVarMddIdArray, array_t *quantifyVarMddIdArray, array_t **clusteredRelationArray, array_t **arraySmoothVarBddArray, array_t **smoothVarCubeArray, boolean freeRelationArray);
222EXTERN void Img_PrintMlpOptions(void);
223EXTERN int Img_TfmGetRecursionStatistics(Img_ImageInfo_t *imageInfo, int preFlag, int *nRecurs, int *nLeaves, int *nTurns, float *averageDepth, int *maxDepth, int *nDecomps, int *topDecomp, int *maxDecomp, float *averageDecomp);
224EXTERN void Img_TfmPrintStatistics(Img_ImageInfo_t *imageInfo, Img_DirectionType dir);
225EXTERN void Img_TfmPrintRecursionStatistics(Img_ImageInfo_t *imageInfo, int preFlag);
226EXTERN void Img_PrintTfmOptions(void);
227EXTERN int Img_TfmGetCacheStatistics(Img_ImageInfo_t *imageInfo, int preFlag, double *inserts, double *lookups, double *hits, double *entries, int *nSlots, int *maxChainLength);
228EXTERN int Img_TfmCheckGlobalCache(int preFlag);
229EXTERN void Img_TfmPrintCacheStatistics(Img_ImageInfo_t *imageInfo, int preFlag);
230EXTERN void Img_TfmFlushCache(Img_ImageInfo_t *imageInfo, int preFlag);
231EXTERN void Img_Init(void);
232EXTERN void Img_End(void);
233EXTERN Img_MethodType Img_UserSpecifiedMethod(void);
234EXTERN Img_ImageInfo_t * Img_ImageInfoInitialize(Img_ImageInfo_t *imageInfo, graph_t * mddNetwork, array_t * roots, array_t * domainVars, array_t * rangeVars, array_t * quantifyVars, mdd_t * domainCube, mdd_t * rangeCube, mdd_t * quantifyCube, Ntk_Network_t * network, Img_MethodType methodType, Img_DirectionType directionType, int FAFWFlag, mdd_t *winning);
235EXTERN void Img_ImageInfoUpdateVariables(Img_ImageInfo_t *imageInfo, graph_t * mddNetwork, array_t * domainVars, array_t * quantifyVars, mdd_t * domainCube, mdd_t * quantifyCube);
236EXTERN void Img_ImageAllowPartialImage(Img_ImageInfo_t *info, boolean value);
237EXTERN void Img_ImagePrintPartialImageOptions(void);
238EXTERN boolean Img_ImageWasPartial(Img_ImageInfo_t *info);
239EXTERN mdd_t * Img_ImageInfoComputeImageWithDomainVars(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray);
240EXTERN mdd_t * Img_ImageInfoComputeFwdWithDomainVars(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, mdd_t * toCareSet);
241EXTERN mdd_t * Img_ImageInfoComputeFwd(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray);
242EXTERN mdd_t * Img_ImageInfoComputePreImageWithDomainVars(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray);
243EXTERN mdd_t * Img_ImageInfoComputeEXWithDomainVars(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray);
244EXTERN mdd_t * Img_ImageInfoComputeBwdWithDomainVars(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, mdd_t * toCareSet);
245EXTERN mdd_t * Img_ImageInfoComputeBwd(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray);
246EXTERN void Img_ImageInfoFree(Img_ImageInfo_t * imageInfo);
247EXTERN char * Img_ImageInfoObtainMethodTypeAsString(Img_ImageInfo_t * imageInfo);
248EXTERN Img_MethodType Img_ImageInfoObtainMethodType(Img_ImageInfo_t * imageInfo);
249EXTERN void Img_ImageInfoPrintMethodParams(Img_ImageInfo_t *imageInfo, FILE *fp);
250EXTERN void Img_ResetTrMinimizedFlag(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
251EXTERN Img_MinimizeType Img_ReadMinimizeMethod(void);
252EXTERN void Img_MinimizeTransitionRelation(Img_ImageInfo_t *imageInfo, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, boolean reorderIwls95Clusters);
253EXTERN mdd_t * Img_MinimizeImage(mdd_t *image, mdd_t *constraint, Img_MinimizeType method, boolean underapprox);
254EXTERN mdd_t * Img_AddDontCareToImage(mdd_t *image, mdd_t *constraint, Img_MinimizeType method);
255EXTERN mdd_t * Img_MinimizeImageArray(mdd_t *image, array_t *constraintArray, Img_MinimizeType method, boolean underapprox);
256EXTERN void Img_SetPrintMinimizeStatus(Img_ImageInfo_t *imageInfo, int status);
257EXTERN int Img_ReadPrintMinimizeStatus(Img_ImageInfo_t *imageInfo);
258EXTERN void Img_AbstractTransitionRelation(Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, Img_DirectionType directionType);
259EXTERN void Img_DupTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
260EXTERN void Img_RestoreTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
261EXTERN int Img_ApproximateTransitionRelation(Img_ImageInfo_t *imageInfo, bdd_approx_dir_t approxDir, bdd_approx_type_t approxMethod, int approxThreshold, double approxQuality, double approxQualityBias, Img_DirectionType directionType, mdd_t *bias);
262EXTERN mdd_t * Img_ApproximateImage(mdd_manager *mgr, mdd_t *image, bdd_approx_dir_t approxDir, bdd_approx_type_t approxMethod, int approxThreshold, double approxQuality, double approxQualityBias, mdd_t *bias);
263EXTERN int Img_IsPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo);
264EXTERN void Img_ResetNumberOfImageComputation(Img_DirectionType imgDir);
265EXTERN int Img_GetNumberOfImageComputation(Img_DirectionType imgDir);
266EXTERN array_t * Img_GetPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
267EXTERN void Img_ReplaceIthPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, int i, mdd_t *relation, Img_DirectionType directionType);
268EXTERN void Img_ReplacePartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, array_t *relationArray, Img_DirectionType directionType);
269EXTERN mdd_t * Img_ComposeIntermediateNodes(graph_t *partition, mdd_t *node, array_t *psVars, array_t *nsVars, array_t *inputVars);
270EXTERN void Img_ImageConstrainAndClusterTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType direction, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus);
271EXTERN Img_MinimizeType Img_GuidedSearchReadUnderApproxMinimizeMethod(void);
272EXTERN Img_MinimizeType Img_GuidedSearchReadOverApproxMinimizeMethod(void);
273EXTERN mdd_t * Img_Substitute(Img_ImageInfo_t *imageInfo, mdd_t *f, Img_SubstituteDir dir);
274EXTERN mdd_t * Img_ImageGetUnreachableStates(Img_ImageInfo_t * imageInfo);
275EXTERN void Img_ImageInfoSetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo);
276EXTERN void Img_ImageInfoResetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo);
277EXTERN void Img_ImageInfoResetLinearComputeRange(Img_ImageInfo_t * imageInfo);
278EXTERN void Img_ImageInfoSetLinearComputeRange(Img_ImageInfo_t * imageInfo);
279EXTERN int Img_IsTransitionRelationOptimized(Img_ImageInfo_t * imageInfo);
280EXTERN void Img_ForwardImageInfoConjoinWithWinningStrategy( Img_ImageInfo_t * imageInfo, mdd_t *winningStrategy);
281EXTERN void Img_ForwardImageInfoRecoverFromWinningStrategy( Img_ImageInfo_t * imageInfo);
282EXTERN Img_OptimizeType Img_ImageInfoObtainOptimizeType(Img_ImageInfo_t * imageInfo);
283EXTERN int Img_IsQuantifyCubeSame( Img_ImageInfo_t *imageInfo, mdd_t *quantifyCube);
284EXTERN int Img_IsQuantifyArraySame( Img_ImageInfo_t *imageInfo, array_t *quantifyArray);
285EXTERN void Img_ImageInfoFreeFAFW(Img_ImageInfo_t * imageInfo);
286
287
288
289
290/**
291EXTERN void ImgLinearClusterRelationArray(mdd_manager *mgr, ImgFunctionData_t *functionData, array_t *relationArray, Img_DirectionType direction, array_t **clusteredRelationArrayPtr, array_t **arraySmoothVarBddArrayPtr, array_t **optClusteredRelationArrayPtr, array_t **optArraySmoothVarBddArrayPtr, ImgTrmOption_t *option);
292**/
293
294
295
296/**AutomaticEnd***************************************************************/
297
298#endif /* _IMG */
Note: See TracBrowser for help on using the repository browser.