source: vis_dev/vis-2.3/src/fsm/fsmArdc.c @ 33

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

vis2.3
File size: 141.3 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [fsmArdc.c]
4
5  PackageName [fsm]
6
7  Synopsis    [Routines to perform overapproximate reachability on the FSM
8  structure.]
9
10  Description [The basic algorithms are almost same as the one in
11  Hyunwoo Cho's paper in TCAD96, except as noted below. To read the
12  functions in this file, it is strongly recommended to read that
13  paper first and In-Ho Moon's paper in ICCAD98.
14
15  0. Cho's algorithm uses transition function for image computation,
16     whereas we use transition relation.
17  1. constrainTarget
18     In Cho's papers, there are two versions of algorithms: one is constraining
19     transition relation, the other is initial states, so this function
20     includes these two as well as the case of both.
21     0) Fsm_Ardc_Constrain_Tr_c      : constrain transition relation (default).
22     1) Fsm_Ardc_Constrain_Initial_c : constrain initial state.
23     2) Fsm_Ardc_Constrain_Both_c    : constrain both.
24  2. decomposeFlag
25     To do above constraining operation, we can make the constraint
26     either conjoined (as single bdd) or decomposed (as array of bdds) from
27     the reachable states of fanin submachines of the current submachine.
28     To have same interface for these two, array of constraints is used.
29  3. dynamic variable reordering
30     In Cho's algorithm, dynamic variable ordering is not allowed, but
31     it is allowed here. Also, refer to 5. restore-containment.
32  4. abstractPseudoInput
33     To make  convergence faster, we can abstract pseudo primary input
34     variables early, but refer to 5. restore-containment.
35     0) Fsm_Ardc_Abst_Ppi_No_c           : do not abstract pseudo input
36                                           variables.
37     1) Fsm_Ardc_Abst_Ppi_Before_Image_c : abstract before image computation
38                                           (default).
39     2) Fsm_Ardc_Abst_Ppi_After_Image_c  : abstract after image computation.
40     3) Fsm_Ardc_Abst_Ppi_At_End_c       : abstract at the end of approximate
41                                           traversal.
42  5. restore-constainment
43     Due to 3 (dynamic variable reordering) and 4 (abstractPseudoInput),
44     current reachable states may not be subset of previous reachable
45     states. In this case, we correct current reachable states to the
46     intersection of current and previous reachable states in MBM. However,
47     in FBF, we need to take union of the two.
48  6. projectedInitialFlag
49     When we do reachability analysis of submachines, initial states of
50     a submachine can be one of the followings. In Cho's paper, projected
51     initial states was used.
52     0) FALSE : use original initial states for submachine
53     1) TRUE  : use projected initial states for submachine (default)
54  ]
55
56  Author      [In-Ho Moon]
57
58  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado.
59  All rights reserved.
60
61  Permission is hereby granted, without written agreement and without license
62  or royalty fees, to use, copy, modify, and distribute this software and its
63  documentation for any purpose, provided that the above copyright notice and
64  the following two paragraphs appear in all copies of this software.
65
66  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
67  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
68  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
69  COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
70
71  THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
72  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
73  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
74  "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE
75  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
76
77******************************************************************************/
78
79#include "fsmInt.h"
80#include "ntm.h"
81
82static char rcsid[] UNUSED = "$Id: fsmArdc.c,v 1.86 2009/04/12 00:44:04 fabio Exp $";
83
84/*---------------------------------------------------------------------------*/
85/* Constant declarations                                                     */
86/*---------------------------------------------------------------------------*/
87
88#define ARDC_MAX_LINE_LEN       4096
89
90/*---------------------------------------------------------------------------*/
91/* Structure declarations                                                    */
92/*---------------------------------------------------------------------------*/
93
94
95/*---------------------------------------------------------------------------*/
96/* Type declarations                                                         */
97/*---------------------------------------------------------------------------*/
98
99
100/**AutomaticStart*************************************************************/
101
102/*---------------------------------------------------------------------------*/
103/* Static function prototypes                                                */
104/*---------------------------------------------------------------------------*/
105
106static void SortSubFsmsForApproximateTraversal(array_t **subFsmArray, array_t **fanInsIndexArray, array_t **fanOutsIndexArray, int verbosityLevel);
107static array_t * ArdcMbmTraversal(Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, array_t *fanOutsIndexArray, mdd_t ***subReached, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options, boolean lfpFlag);
108static array_t * ArdcRfbfTraversal(Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options);
109static array_t * ArdcTfbfTraversal(Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, mdd_t ***subReached, mdd_t ***subTo, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options);
110static array_t * ArdcTmbmTraversal(Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, array_t *fanOutsIndexArray, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options, boolean lfpFlag);
111static array_t * ArdcSimpleTraversal(Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options, int setFlag);
112static void ComputeFaninConstrainArray(array_t *faninConstrainArray, mdd_t **constraint, int current, array_t *fans, int decomposeFlag, int faninConstrainMode);
113static void MinimizeTransitionRelationWithFaninConstraint(Img_ImageInfo_t *imageInfo, array_t *faninConstrainArray, Img_MinimizeType constrainMethod, boolean reorderPtrFlag, boolean duplicate);
114static void ComputeConstrainedInitialStates(Fsm_Fsm_t *subFsm, array_t *faninConstrainArray, Img_MinimizeType constrainMethod);
115static void ComputeApproximateReachableStatesArray(mdd_manager *mddManager, array_t *reachedArray, mdd_t **reached, mdd_t ***subReached, int nSubFsms, int decomposeFlag);
116static array_t * ArdcCopyOverApproxReachableStatesFromExact(Fsm_Fsm_t *fsm);
117static void PrintCurrentReachedStates(mdd_manager *mddManager, Fsm_Fsm_t **subFsm, mdd_t **reached, Fsm_Ardc_TraversalType_t method, int nSubFsms, int iteration, int nvars, int ardcVerbosity, boolean supportCheckFlag);
118static void PrintBddWithName(Fsm_Fsm_t *fsm, array_t *mddIdArr, mdd_t *node);
119static void ArdcReadGroup(Ntk_Network_t *network, FILE *groupFile, array_t *latchNameArray, array_t *groupIndexArray);
120static void ArdcWriteOneGroup(Part_Subsystem_t *partitionSubsystem, FILE *groupFile, int i);
121static void ArdcPrintOneGroup(Part_Subsystem_t *partitionSubsystem, int i, int nLatches, array_t *fanIns, array_t *fanOuts);
122static int GetArdcSetIntValue(char *string, int l, int u, int defaultValue);
123static void ArdcEpdCountOnsetOfOverApproximateReachableStates(Fsm_Fsm_t *fsm, EpDouble *epd);
124static mdd_t * QuantifyVariables(mdd_t *state, array_t *smoothArray, mdd_t *smoothCube);
125static void UpdateMbmEventSchedule(Fsm_Fsm_t **subFsm, array_t *fanOutIndices, int *traverse, int lfpFlag);
126static void PrintTfmStatistics(array_t *subFsmArray);
127
128/**AutomaticEnd***************************************************************/
129
130
131/*---------------------------------------------------------------------------*/
132/* Definition of exported functions                                          */
133/*---------------------------------------------------------------------------*/
134
135/**Function********************************************************************
136
137  Synopsis    [Minimize transition relation of a submachine with ARDC.]
138
139  Description [Minimize transition relation of a submachine with
140  ARDC. Direction of traversal is specified by forward(1) or
141  backward(2) or both(3).
142
143  <p>This function is internal to the ardc sub-package.
144 
145  <p>Perhaps you should use Fsm_MinimizeTransitionRelationWithReachabilityInfo.
146  That function will minimize wrt exact RDCs if available.
147   ]
148
149
150  SideEffects []
151
152******************************************************************************/
153void
154Fsm_ArdcMinimizeTransitionRelation(Fsm_Fsm_t *fsm, Img_DirectionType fwdbwd)
155{
156  char                  *flagValue;
157  int                   value = 0;
158  int                   fwd = 0;
159  int                   bwd = 0;
160  Img_ImageInfo_t       *imageInfo;
161  int                   saveStatus;
162  boolean               reorderPtrFlag = FALSE;
163
164  switch (fwdbwd) {
165  case Img_Forward_c:
166    fwd = 1;
167    break;
168  case Img_Backward_c:
169    bwd = 1;
170    break;
171  case Img_Both_c:
172    fwd = 1;
173    bwd= 1;
174    break;
175  }
176
177  imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, bwd, fwd);
178
179  saveStatus = 0;
180  flagValue = Cmd_FlagReadByName("ardc_verbosity");
181  if (flagValue != NIL(char)) {
182    sscanf(flagValue, "%d", &value);
183    if (value > 1) {
184      saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
185      Img_SetPrintMinimizeStatus(imageInfo, 1);
186    }
187  }
188
189  reorderPtrFlag = FsmGetArdcSetBooleanValue("ardc_reorder_ptr",
190                                                reorderPtrFlag);
191  Img_MinimizeTransitionRelation(
192    imageInfo,
193    Fsm_FsmReadCurrentOverApproximateReachableStates(fsm),
194    Img_DefaultMinimizeMethod_c, fwdbwd, reorderPtrFlag);
195
196  if (value > 1)
197    Img_SetPrintMinimizeStatus(fsm->imageInfo, saveStatus);
198  return;
199}
200
201
202/**Function********************************************************************
203
204  Synopsis [Computes the image of current reachable states of an FSM.]
205
206  Description [Computes the image of current reachable states of an FSM.
207  It calls Fsm_FsmComputeReachableStates by setting depthValue to 1.]
208
209  SideEffects []
210
211  SeeAlso []
212
213******************************************************************************/
214mdd_t *
215Fsm_ArdcComputeImage(Fsm_Fsm_t *fsm,
216                     mdd_t *fromLowerBound,
217                     mdd_t *fromUpperBound,
218                     array_t *toCareSetArray)
219{
220  Img_ImageInfo_t       *imageInfo = NIL(Img_ImageInfo_t);
221  mdd_t                 *image;
222
223  /* Create an imageInfo for image computations, if not already created. */
224  imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, 0, 1);
225
226  /* Compute the image */
227  image = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
228                fromLowerBound, fromUpperBound, toCareSetArray);
229
230  return(image);
231}
232
233
234/**Function********************************************************************
235
236  Synopsis    [Computes overapproximate reachable states.]
237
238  Description [Computes overapproximate reachable states. This function is a
239  wrapper around Fsm_ArdcComputeOverApproximateReachableStates.]
240
241  SideEffects []
242
243  SeeAlso [Fsm_ArdcComputeOverApproximateReachableStates]
244
245******************************************************************************/
246array_t *
247Fsm_FsmComputeOverApproximateReachableStates(Fsm_Fsm_t *fsm,
248  int incrementalFlag, int verbosityLevel, int printStep, int depthValue,
249  int shellFlag, int reorderFlag, int reorderThreshold, int recompute)
250{
251  array_t               *apprReachableStates;
252  Fsm_ArdcOptions_t     options;
253
254  Fsm_ArdcGetDefaultOptions(&options);
255
256  if (printStep && options.verbosity < 2)
257    printStep = 0;
258
259  apprReachableStates = Fsm_ArdcComputeOverApproximateReachableStates(fsm,
260    incrementalFlag, verbosityLevel, printStep, depthValue, shellFlag,
261    reorderFlag, reorderThreshold, recompute, &options);
262
263  return(apprReachableStates);
264}
265
266
267/**Function********************************************************************
268
269  Synopsis [Computes the set of approximate reachable states of an FSM.]
270
271  Description [Computes the set of approximate reachable states of an FSM.
272  If this set has already been computed, then just returns the result of
273  the previous computation. The computations starts by creating
274  partitions (based on either hierarchy or state space
275  decomposition [TCAD96]). The submachines are created for each of these
276  partitions. Then approximate traversal is performed by one of the
277  supported methods (MBM, RFBF, TFBF, TMBM, LMBM, and TLMBM). The approximate
278  reachable set is returned in a conjunctive decomposed form in an array.]
279
280  SideEffects []
281
282  SeeAlso [Fsm_FsmComputeInitialStates Fsm_FsmComputeReachableStates]
283
284******************************************************************************/
285array_t *
286Fsm_ArdcComputeOverApproximateReachableStates(Fsm_Fsm_t *fsm,
287                                              int incrementalFlag,
288                                              int verbosityLevel,
289                                              int printStep,
290                                              int depthValue, int shellFlag,
291                                              int reorderFlag,
292                                              int reorderThreshold,
293                                              int recompute,
294                                              Fsm_ArdcOptions_t *options)
295{
296  array_t               *reachableStatesArray = NIL(array_t);
297  mdd_t                 *reachableStates = NIL(mdd_t);
298  mdd_t                 *initialStates;
299  Ntk_Network_t         *network = Fsm_FsmReadNetwork(fsm);
300  Part_Subsystem_t      *partitionSubsystem;
301  array_t               *partitionArray;
302  int                   i;
303  graph_t               *partition = Part_NetworkReadPartition(network);
304  st_table              *vertexTable;
305  Fsm_Fsm_t             *subFsm;
306  array_t               *subFsmArray;
307  array_t               *fanIns, *fanOuts;
308  array_t               *fanInsIndexArray, *fanOutsIndexArray;
309  array_t               *fans;
310  array_t               *psVars;
311  mdd_manager           *mddManager = Fsm_FsmReadMddManager(fsm);
312  char                  *flagValue;
313  Fsm_RchType_t         approxFlag;
314  int                   nvars; /* the number of binary variables of the fsm */
315  FILE                  *groupFile = NIL(FILE);
316  Img_MethodType        imageMethod = Img_Default_c;
317  Img_MethodType        saveImageMethod = Img_Default_c;
318  char                  *imageMethodString;
319  Fsm_Ardc_AbstPpiType_t saveAbstractPseudoInput;
320
321  if (recompute)
322    FsmResetReachabilityFields(fsm, Fsm_Rch_Oa_c);
323
324  /* If exact is already computed, copy exact to overapproximate. */
325  if (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t)) {
326    if (Fsm_FsmReadCurrentOverApproximateReachableStates(fsm) != NIL(array_t)) {
327      /* If the overapproximation is already the exact set, return it,
328       * otherwise discard it. */
329      if (FsmReadReachabilityOverApproxComputationStatus(fsm) ==
330          Fsm_Ardc_Exact_c) {
331        return(Fsm_FsmReadOverApproximateReachableStates(fsm));
332      } else {
333        fprintf(vis_stdout,
334                "** ardc warning : ignoring previous computation.\n");
335        Fsm_FsmFreeOverApproximateReachableStates(fsm);
336      }
337    }
338    if (verbosityLevel > 0 || options->verbosity > 0) {
339      fprintf(vis_stdout,
340              "** ardc info : exact reached states are already computed.\n");
341    }
342    /* Either we had no overapproximation, or it was not the exact set, and
343     * hence it was discarded.  Copy from exact to overapproximate. */
344    reachableStatesArray = ArdcCopyOverApproxReachableStatesFromExact(fsm);
345    return(reachableStatesArray);
346  }
347
348  /* If already computed, just return the array. */
349  if (Fsm_FsmReadCurrentOverApproximateReachableStates(fsm) != NIL(array_t)) {
350    if (FsmReadReachabilityOverApproxComputationStatus(fsm) >=
351        Fsm_Ardc_Converged_c) {
352      return(Fsm_FsmReadOverApproximateReachableStates(fsm));
353    } else {
354      /* Here, at this time, we just throw away current approximate
355       * reachable states which is not converged yet, then restart.
356       */
357      fprintf(vis_stdout,
358              "** ardc warning : ignoring previous computation.\n");
359      Fsm_FsmFreeOverApproximateReachableStates(fsm);
360    }
361  }
362
363  /* Perform state space decomposition. */
364  partitionArray = Fsm_ArdcDecomposeStateSpace(network,
365                                               fsm->fsmData.presentStateVars,
366                                               fsm->fsmData.nextStateFunctions,
367                                               options);
368
369  /* If there is only one group, call exact reachability analysis. */
370  if (array_n(partitionArray) == 1) {
371    if (options->verbosity > 0) {
372      fprintf(vis_stdout,
373              "** ardc info : changing to exact reachability analysis.\n");
374    }
375    arrayForEachItem(Part_Subsystem_t *, partitionArray, i,
376                     partitionSubsystem) {
377      Part_PartitionSubsystemFree(partitionSubsystem);
378    }
379    array_free(partitionArray);
380
381    if (options->useHighDensity)
382      approxFlag = Fsm_Rch_Hd_c;
383    else
384      approxFlag = Fsm_Rch_Bfs_c;
385    reachableStates = Fsm_FsmComputeReachableStates(fsm,
386                0, verbosityLevel, printStep, 0,
387                0, reorderFlag, reorderThreshold,
388                approxFlag, 0, 0, NIL(array_t), (verbosityLevel > 1),
389                                                    NIL(array_t));
390    mdd_free(reachableStates);
391    reachableStatesArray = ArdcCopyOverApproxReachableStatesFromExact(fsm);
392    return(reachableStatesArray);
393  }
394
395  /* Read the image_method flag, and save its value in imageMethodString. */
396  flagValue = Cmd_FlagReadByName("image_method");
397  if (flagValue != NIL(char)) {
398    if (strcmp(flagValue, "iwls95") == 0 || strcmp(flagValue, "default") == 0)
399      imageMethod = Img_Iwls95_c;
400    else if (strcmp(flagValue, "monolithic") == 0)
401      imageMethod = Img_Monolithic_c;
402    else if (strcmp(flagValue, "tfm") == 0)
403      imageMethod = Img_Tfm_c;
404    else if (strcmp(flagValue, "hybrid") == 0)
405      imageMethod = Img_Hybrid_c;
406    else if (strcmp(flagValue, "mlp") == 0)
407      imageMethod = Img_Mlp_c;
408    else {
409      fprintf(vis_stderr, "** ardc error: invalid image method %s.\n",
410              flagValue);
411    }
412  }
413  imageMethodString = flagValue;
414  /* Update the image_method flag to the method specified for approximate
415   * reachability. */
416  if (options->ardcImageMethod != Img_Default_c &&
417      options->ardcImageMethod != imageMethod) {
418    saveImageMethod = imageMethod;
419    if (options->ardcImageMethod == Img_Monolithic_c) {
420      Cmd_FlagUpdateValue("image_method", "monolithic");
421      imageMethod = Img_Monolithic_c;
422    } else if (options->ardcImageMethod == Img_Iwls95_c) {
423      Cmd_FlagUpdateValue("image_method", "iwls95");
424      imageMethod = Img_Iwls95_c;
425    } else if (options->ardcImageMethod == Img_Tfm_c) {
426      Cmd_FlagUpdateValue("image_method", "tfm");
427      imageMethod = Img_Tfm_c;
428    } else if (options->ardcImageMethod == Img_Hybrid_c) {
429      Cmd_FlagUpdateValue("image_method", "hybrid");
430      imageMethod = Img_Hybrid_c;
431    } else if (options->ardcImageMethod == Img_Mlp_c) {
432      Cmd_FlagUpdateValue("image_method", "mlp");
433      imageMethod = Img_Mlp_c;
434    }
435  }
436
437  /* Open the file where to save the result of partitioning is so requested. */
438  if (options->writeGroupFile) {
439    groupFile = Cmd_FileOpen(options->writeGroupFile, "w", NIL(char *), 0);
440    if (groupFile == NIL(FILE)) {
441      fprintf(vis_stderr, "** ardc error : can't open file [%s] to write.\n",
442              options->writeGroupFile);
443    }
444  }
445
446  /* Compute the set of initial states, if not already computed. */
447  initialStates = Fsm_FsmComputeInitialStates(fsm);
448
449  subFsmArray = array_alloc(Fsm_Fsm_t *, 0);
450  fanInsIndexArray = array_alloc(array_t *, 0);
451  fanOutsIndexArray = array_alloc(array_t *, 0);
452
453  /* For each partitioned submachines build an FSM. */
454  arrayForEachItem(Part_Subsystem_t *, partitionArray, i, partitionSubsystem) {
455    vertexTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
456    fanIns = Part_PartitionSubsystemReadFanIn(partitionSubsystem);
457    fanOuts = Part_PartitionSubsystemReadFanOut(partitionSubsystem);
458    subFsm = Fsm_FsmCreateSubsystemFromNetwork(network, partition,
459                                                vertexTable, TRUE,
460                                                options->createPseudoVarMode);
461    /* Depending on the options, the initial states of each submachine
462     * are either the states of the entire system or their projection
463     * on the subspace of the submachine. */
464    if (!options->projectedInitialFlag &&
465        options->abstractPseudoInput != Fsm_Ardc_Abst_Ppi_Before_Image_c) {
466      subFsm->reachabilityInfo.initialStates = mdd_dup(initialStates);
467    } else {
468      mdd_t     *dummy;
469
470      dummy = Fsm_FsmComputeInitialStates(subFsm);
471      mdd_free(dummy);
472    }
473    array_insert_last(Fsm_Fsm_t *, subFsmArray, subFsm);
474    array_insert_last(array_t *, fanInsIndexArray, fanIns);
475    array_insert_last(array_t *, fanOutsIndexArray, fanOuts);
476
477    if (options->verbosity > 1) {
478      int       nLatches;
479      nLatches = mdd_get_number_of_bdd_vars(mddManager,
480                                            subFsm->fsmData.presentStateVars);
481      ArdcPrintOneGroup(partitionSubsystem, i, nLatches, fanIns, fanOuts);
482    }
483    if (groupFile)
484      ArdcWriteOneGroup(partitionSubsystem, groupFile, i);
485
486    st_free_table(vertexTable);
487  } /* end of arrayForEachItem(partitionArray) */
488  mdd_free(initialStates);
489
490  if (groupFile)
491    fclose(groupFile);
492
493  /* Sort submachines to find the order in which to traverse them. */
494  SortSubFsmsForApproximateTraversal(&subFsmArray, &fanInsIndexArray,
495                                     &fanOutsIndexArray, options->verbosity);
496
497  /* Optimize pseudo-input variables to contain only the variables of fanin
498   * submachines. If createPseudoVarMode is 0, the set of pseudo-input
499   * variables is just the collection of the variables of all other
500   * submachines.
501   * If createPseudoVarMode is 1, the set is the collection of the variables
502   * of only its fanin submachines. If createPseudoVarMode is 2, the set is
503   * the collection of the support variables that appear in other submachines.
504   */
505  if (options->createPseudoVarMode == 0) {
506    arrayForEachItem(Fsm_Fsm_t *, subFsmArray, i, subFsm) {
507      Fsm_Fsm_t *faninSubfsm;
508      int       j, fanin;
509
510      subFsm->fsmData.primaryInputVars = array_dup(subFsm->fsmData.inputVars);
511      subFsm->fsmData.pseudoInputVars = array_alloc(int, 0);
512      fanIns = array_fetch(array_t *, fanInsIndexArray, i);
513      arrayForEachItem(int, fanIns, j, fanin) {
514        if (fanin == i)
515          continue;
516        faninSubfsm = array_fetch(Fsm_Fsm_t *, subFsmArray, fanin);
517        array_append(subFsm->fsmData.pseudoInputVars,
518                  faninSubfsm->fsmData.presentStateVars);
519      }
520      subFsm->fsmData.globalPsVars = array_dup(
521        subFsm->fsmData.presentStateVars);
522      array_append(subFsm->fsmData.globalPsVars,
523        subFsm->fsmData.pseudoInputVars);
524      array_append(subFsm->fsmData.inputVars, subFsm->fsmData.pseudoInputVars);
525
526      subFsm->fsmData.pseudoInputBddVars = mdd_id_array_to_bdd_array(mddManager,
527        subFsm->fsmData.pseudoInputVars);
528
529      if (subFsm->fsmData.createVarCubesFlag) {
530        subFsm->fsmData.pseudoInputCube = mdd_id_array_to_bdd_cube(mddManager,
531          subFsm->fsmData.pseudoInputVars);
532        subFsm->fsmData.primaryInputCube = subFsm->fsmData.inputCube;
533        subFsm->fsmData.inputCube = mdd_id_array_to_bdd_cube(mddManager,
534          subFsm->fsmData.inputVars);
535        subFsm->fsmData.globalPsCube = mdd_id_array_to_bdd_cube(mddManager,
536          subFsm->fsmData.globalPsVars);
537      }
538    }
539  }
540
541  if (options->useHighDensity)
542    approxFlag = Fsm_Rch_Hd_c;
543  else
544    approxFlag = Fsm_Rch_Bfs_c;
545
546  /* In case of transition function method, since quantification doesn't
547   * make any sense, we turn it off.  We turn quantification off also for the
548   * hybrid method, because it starts with tfm.
549   */
550  saveAbstractPseudoInput = options->abstractPseudoInput;
551  if (imageMethod == Img_Tfm_c || imageMethod == Img_Hybrid_c)
552    options->abstractPseudoInput = Fsm_Ardc_Abst_Ppi_No_c;
553
554  nvars = mdd_get_number_of_bdd_vars(mddManager, fsm->fsmData.presentStateVars);
555  if (options->traversalMethod == Fsm_Ardc_Traversal_Mbm_c) {
556    reachableStatesArray = ArdcMbmTraversal(fsm, nvars, subFsmArray,
557                fanInsIndexArray, fanOutsIndexArray, NULL,
558                incrementalFlag, verbosityLevel, printStep,
559                depthValue, shellFlag, reorderFlag,
560                reorderThreshold, approxFlag, options, FALSE);
561  } else if (options->traversalMethod == Fsm_Ardc_Traversal_Rfbf_c) {
562    if (approxFlag == Fsm_Rch_Hd_c) {
563      fprintf(vis_stderr,
564        "** ardc error : High Density Traversal is not allowed in FBF.\n");
565    }
566    reachableStatesArray = ArdcRfbfTraversal(fsm, nvars, subFsmArray,
567                fanInsIndexArray,
568                incrementalFlag, verbosityLevel, printStep,
569                depthValue, shellFlag, reorderFlag, reorderThreshold,
570                approxFlag, options);
571  } else if (options->traversalMethod == Fsm_Ardc_Traversal_Tfbf_c) {
572    if (approxFlag == Fsm_Rch_Hd_c) {
573      fprintf(vis_stderr,
574        "** ardc error : High Density Traversal is not allowed in FBF.\n");
575    }
576    reachableStatesArray = ArdcTfbfTraversal(fsm, nvars, subFsmArray,
577                fanInsIndexArray, NULL, NULL,
578                incrementalFlag, verbosityLevel, printStep,
579                depthValue, shellFlag, reorderFlag, reorderThreshold,
580                approxFlag, options);
581  } else if (options->traversalMethod == Fsm_Ardc_Traversal_Tmbm_c) {
582    reachableStatesArray = ArdcTmbmTraversal(fsm, nvars, subFsmArray,
583                fanInsIndexArray, fanOutsIndexArray,
584                incrementalFlag, verbosityLevel, printStep,
585                depthValue, shellFlag, reorderFlag, reorderThreshold,
586                approxFlag, options, FALSE);
587  } else if (options->traversalMethod == Fsm_Ardc_Traversal_Lmbm_c) {
588    reachableStatesArray = ArdcMbmTraversal(fsm, nvars, subFsmArray,
589                fanInsIndexArray, fanOutsIndexArray, NULL,
590                incrementalFlag, verbosityLevel, printStep,
591                depthValue, shellFlag, reorderFlag,
592                reorderThreshold, approxFlag, options, TRUE);
593  } else if (options->traversalMethod == Fsm_Ardc_Traversal_Tlmbm_c) {
594    reachableStatesArray = ArdcTmbmTraversal(fsm, nvars, subFsmArray,
595                fanInsIndexArray, fanOutsIndexArray,
596                incrementalFlag, verbosityLevel, printStep,
597                depthValue, shellFlag, reorderFlag, reorderThreshold,
598                approxFlag, options, TRUE);
599  } else {
600    reachableStatesArray = ArdcSimpleTraversal(fsm, nvars, subFsmArray,
601                incrementalFlag, verbosityLevel, printStep,
602                depthValue, shellFlag, reorderFlag, reorderThreshold,
603                approxFlag, options, TRUE);
604  }
605  options->abstractPseudoInput = saveAbstractPseudoInput;
606
607  if (options->verbosity &&
608      (options->ardcImageMethod == Img_Tfm_c ||
609       options->ardcImageMethod == Img_Hybrid_c)) {
610    PrintTfmStatistics(subFsmArray);
611  }
612
613  fsm->reachabilityInfo.subPsVars = array_alloc(array_t *, 0);
614  if (options->decomposeFlag) {
615    for (i = 0; i < array_n(subFsmArray); i++) {
616      subFsm = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
617      psVars = array_dup(subFsm->fsmData.presentStateVars);
618      array_insert_last(array_t *, fsm->reachabilityInfo.subPsVars, psVars);
619    }
620  } else {
621    psVars = array_dup(fsm->fsmData.presentStateVars);
622    array_insert_last(array_t *, fsm->reachabilityInfo.subPsVars, psVars);
623  }
624
625  arrayForEachItem(array_t *, fanInsIndexArray, i, fans) {
626    array_free(fans);
627  }
628  array_free(fanInsIndexArray);
629  arrayForEachItem(array_t *, fanOutsIndexArray, i, fans) {
630    array_free(fans);
631  }
632  array_free(fanOutsIndexArray);
633  arrayForEachItem(Part_Subsystem_t *, partitionArray, i, partitionSubsystem) {
634    FREE(partitionSubsystem);
635  }
636  array_free(partitionArray);
637
638  arrayForEachItem(Fsm_Fsm_t *, subFsmArray, i, subFsm) {
639    Fsm_FsmSubsystemFree(subFsm);
640  }
641  array_free(subFsmArray);
642
643  /* Restore value of image_method flag. */
644  if (options->ardcImageMethod != Img_Default_c &&
645      options->ardcImageMethod != saveImageMethod) {
646    if (imageMethodString) {
647      if (saveImageMethod == Img_Monolithic_c)
648        Cmd_FlagUpdateValue("image_method", "monolithic");
649      else if (saveImageMethod == Img_Iwls95_c)
650        Cmd_FlagUpdateValue("image_method", "iwls95");
651      else if (saveImageMethod == Img_Tfm_c)
652        Cmd_FlagUpdateValue("image_method", "tfm");
653      else if (saveImageMethod == Img_Hybrid_c)
654        Cmd_FlagUpdateValue("image_method", "hybrid");
655      else if (saveImageMethod == Img_Mlp_c)
656        Cmd_FlagUpdateValue("image_method", "mlp");
657    } else
658      Cmd_FlagDeleteByName("image_method");
659  }
660
661  fsm->reachabilityInfo.apprReachableStates = reachableStatesArray;
662  return(reachableStatesArray);
663}
664
665
666/**Function********************************************************************
667
668  Synopsis    [Performs state space decomposition.]
669
670  Description [Performs state space decomposition.]
671
672  SideEffects []
673
674  SeeAlso []
675
676******************************************************************************/
677array_t *
678Fsm_ArdcDecomposeStateSpace(Ntk_Network_t *network, array_t *presentStateVars,
679                        array_t *nextStateFunctions, Fsm_ArdcOptions_t *options)
680{
681  array_t               *latchNameArray;
682  array_t               *groupIndexArray;
683  char                  *name;
684  Ntk_Node_t            *latch;
685  int                   i, mddId;
686  Part_SubsystemInfo_t  *subsystemInfo;
687  array_t               *partitionArray;
688  FILE                  *groupFile = NIL(FILE);
689  long                  initialTime = 0, finalTime;
690  int                   verbosity = 0;
691  float                 affinityFactor = 0.5;
692  int                   groupSize = 8;
693
694  if (options) {
695    verbosity = options->verbosity;
696    affinityFactor = options->affinityFactor;
697    groupSize = options->groupSize;
698  } else {
699    char        *flagValue;
700
701    flagValue = Cmd_FlagReadByName("ardc_group_size");
702    if (flagValue != NIL(char)) {
703      sscanf(flagValue, "%d", &groupSize);
704      if (groupSize <= 0) {
705        fprintf(vis_stderr,
706                "** ardc error: invalid value %s for ardc_group_size[>0]. **\n",
707                flagValue);
708        groupSize = 8;
709      }
710    }
711    flagValue = Cmd_FlagReadByName("ardc_verbosity");
712    if (flagValue != NIL(char))
713      sscanf(flagValue, "%d", &verbosity);
714    flagValue = Cmd_FlagReadByName("ardc_affinity_factor");
715    if (flagValue != NIL(char)) {
716      sscanf(flagValue, "%f", &affinityFactor);
717      if (affinityFactor < 0.0 || affinityFactor > 1.0) {
718        fprintf(vis_stderr,
719      "** ardc error :invalid value %s for ardc_affinity_factor[0.0-1.0]. **\n",
720                flagValue);
721        affinityFactor = 0.5;
722      }
723    }
724  }
725
726  if (verbosity > 0)
727    initialTime = util_cpu_time();
728
729  if (options && options->readGroupFile) {
730    groupFile = Cmd_FileOpen(options->readGroupFile, "r", NIL(char *), 1);
731    if (groupFile == NIL(FILE)) {
732      fprintf(vis_stderr, "** ardc error : can't open file [%s] to read.\n",
733              options->readGroupFile);
734    }
735  }
736
737  if (groupFile) {
738    latchNameArray = array_alloc(char *, 0);
739    groupIndexArray = array_alloc(int, 0);
740    ArdcReadGroup(network, groupFile, latchNameArray, groupIndexArray);
741    subsystemInfo = Part_PartitionSubsystemInfoInit(network);
742    partitionArray = Part_PartCreateSubsystems(subsystemInfo,
743                        latchNameArray, groupIndexArray);
744    Part_PartitionSubsystemInfoFree(subsystemInfo);
745    arrayForEachItem(char *, latchNameArray, i, name) {
746      FREE(name);
747    }
748    array_free(latchNameArray);
749    array_free(groupIndexArray);
750    fclose(groupFile);
751    groupFile = NIL(FILE);
752  } else if (groupSize > 0) {
753    subsystemInfo = Part_PartitionSubsystemInfoInit(network);
754    /*
755    Part_PartitionSubsystemInfoSetVerbosity(subsystemInfo, verbosity);
756    */
757    Part_PartitionSubsystemInfoSetBound(subsystemInfo, groupSize);
758    Part_PartitionSubsystemInfoSetAffinityFactor(subsystemInfo, affinityFactor);
759    latchNameArray = array_alloc(char *, 0);
760    arrayForEachItem(int, presentStateVars, i, mddId) {
761      latch = Ntk_NetworkFindNodeByMddId(network, mddId);
762      name = Ntk_NodeReadName(latch);
763      array_insert_last(char *, latchNameArray, name);
764    }
765    partitionArray = Part_PartCreateSubsystems(subsystemInfo,
766                       latchNameArray, NIL(array_t));
767    array_free(latchNameArray);
768    Part_PartitionSubsystemInfoFree(subsystemInfo);
769  } else {
770    partitionArray = Part_PartGroupVeriticesBasedOnHierarchy(network,
771      nextStateFunctions);
772  }
773  if (verbosity > 0) {
774    finalTime = util_cpu_time();
775    fprintf(vis_stdout, "grouping(state space decomposition) time = %g\n",
776      (double)(finalTime - initialTime) / 1000.0);
777  }
778
779  return(partitionArray);
780}
781
782
783/**Function********************************************************************
784
785  Synopsis    [Allocates an ARDC option structure.]
786
787  Description [Allocates an ARDC option structure.]
788
789  SideEffects []
790
791  SeeAlso []
792
793******************************************************************************/
794Fsm_ArdcOptions_t *
795Fsm_ArdcAllocOptionsStruct(void)
796{
797  Fsm_ArdcOptions_t *options;
798
799  options = ALLOC(Fsm_ArdcOptions_t, 1);
800  (void)memset((void *)options, 0, sizeof(Fsm_ArdcOptions_t));
801
802  return(options);
803}
804
805
806/**Function********************************************************************
807
808  Synopsis    [Gets default values for ARDC computatiion.]
809
810  Description [Gets default values for ARDC computatiion.
811  Options are as follows.
812
813  set ardc_traversal_method <m>
814      m = 0 : MBM (machine by machine, default)
815      m = 1 : RFBF(reached frame by frame)
816      m = 2 : TFBF(to frame by frame)
817      m = 3 : TMBM(TFBF + MBM)
818      m = 4 : LMBM(least fixpoint MBM)
819  set ardc_group_size <n>
820      n (default = 8)
821  set ardc_affinity_factor <f>
822      f = 0.0 - 1.0 (default = 0.5)
823  set ardc_max_iteration <n>
824      n (default = 0(infinity))
825  set ardc_constrain_target <m>
826      m = 0 : constrain transition relation (default)
827      m = 1 : constrain initial states
828      m = 2 : constrain both
829  set ardc_constrain_method <m>
830      m = 0 : restrict (default)
831      m = 1 : constrain
832      m = 2 : compact (currently supported by only CUDD)
833      m = 3 : squeeze (currently supported by only CUDD)
834  set ardc_constrain_reorder <m>
835      m = yes : allow variable reorderings during consecutive
836                image constraining operations (default)
837      m = no  : don't allow variable reorderings during consecutive
838                image constraining operations
839  set ardc_abstract_pseudo_input <m>
840      m = 0 : do not abstract pseudo input variables
841      m = 1 : abstract pseudo inputs before image computation (default)
842      m = 2 : abstract pseudo inputs at every end of image computation
843      m = 3 : abstract pseudo inputs at the end of approximate traversal
844  set ardc_decompose_flag <m>
845      m = yes : keep decomposed reachable stateses (default)
846      m = no  : make a conjunction of reachable states of all submachines
847  set ardc_projected_initial_flag <m>
848      m = yes : use projected initial states for submachine (default)
849      m = no  : use original initial states for submachine
850  set ardc_image_method <m>
851      m = monolithic : use monolithic image computation for submachines
852      m = iwls95     : use iwls95 image computation for submachines (default)
853      m = tfm        : use tfm image computation for submachines
854      m = hybrid     : use hybrid image computation for submachines
855  set ardc_use_high_density <m>
856      m = yes : use High Density for reachable states of submachines
857      m = no  : use BFS for reachable states of submachines (default)
858  set ardc_create_pseudo_var_mode <m>
859      m = 0 : makes pseudo input variables with exact support (default)
860      m = 1 : makes pseudo input variables from all state variables of
861              the other machines
862      m = 2 : makes pseudo input variables from all state variables of
863              fanin machines
864  set ardc_reorder_ptr <m>
865      m = yes : whenever partitioned transition relation changes,
866                reorders partitioned transition relation
867      m = no  : no reordering of partitioned transition relation (default)
868  set ardc_fanin_constrain_mode <m>
869      m = 0 : constrains w.r.t. the reachable states of fanin machines (default)
870      m = 1 : constrains w.r.t. the reachable states of both fanin machines
871              and itself
872  set ardc_lmbm_initial_mode <m>
873      m = 0 : use given initial states all the time
874      m = 1 : use current reached states as initial states (default)
875      m = 2 : use current frontier as initial states
876  set ardc_mbm_reuse_tr <m>
877      m = yes : use constrained transition relation for next iteration
878      m = no  : use original transition relation for next iteration (default)
879  set ardc_read_group <filename>
880      <filename> file containing grouping information
881  set ardc_write_group <filename>
882      <filename> file to write grouping information
883  set ardc_verbosity <n>
884      n = 0 - 3 (default = 0)
885  ]
886
887  SideEffects []
888
889  SeeAlso []
890
891******************************************************************************/
892void
893Fsm_ArdcGetDefaultOptions(Fsm_ArdcOptions_t *options)
894{
895  int                   groupSize = 8;
896  float                 affinityFactor = 0.5;
897  Fsm_Ardc_TraversalType_t traversalMethod = Fsm_Ardc_Traversal_Lmbm_c;
898  int                   maxIteration = 0;
899  Fsm_Ardc_ConstrainTargetType_t constrainTarget = Fsm_Ardc_Constrain_Tr_c;
900  Img_MinimizeType      constrainMethod = Img_Restrict_c;
901  boolean               decomposeFlag = TRUE;
902  Fsm_Ardc_AbstPpiType_t abstractPseudoInput = Fsm_Ardc_Abst_Ppi_Before_Image_c;
903  boolean               projectedInitialFlag = TRUE;
904  boolean               constrainReorderFlag = TRUE;
905  Img_MethodType        ardcImageMethod = Img_Default_c;
906  boolean               useHighDensity = FALSE;
907  int                   createPseudoVarMode = 0;
908  int                   verbosity = 0;
909  char                  *flagValue;
910  int                   value;
911  float                 affinity;
912  boolean               reorderPtrFlag = FALSE;
913  int                   faninConstrainMode = 0;
914  int                   lmbmInitialStatesMode = 1;
915  int                   mbmReuseTrFlag = 0;
916
917  flagValue = Cmd_FlagReadByName("ardc_traversal_method");
918  if (flagValue != NIL(char)) {
919    sscanf(flagValue, "%d", &value);
920    switch (value) {
921    case 0 :
922      traversalMethod = Fsm_Ardc_Traversal_Mbm_c;
923      break;
924    case 1 :
925      traversalMethod = Fsm_Ardc_Traversal_Rfbf_c;
926      break;
927    case 2 :
928      traversalMethod = Fsm_Ardc_Traversal_Tfbf_c;
929      break;
930    case 3 :
931      traversalMethod = Fsm_Ardc_Traversal_Tmbm_c;
932      break;
933    case 4 :
934      traversalMethod = Fsm_Ardc_Traversal_Lmbm_c;
935      break;
936    case 5 :
937      traversalMethod = Fsm_Ardc_Traversal_Tlmbm_c;
938      break;
939    case 6 : /* hidden option */
940      traversalMethod = Fsm_Ardc_Traversal_Simple_c;
941      break;
942    default :
943      fprintf(vis_stderr, "** ardc error : invalid value %s", flagValue);
944      fprintf(vis_stderr, " for ardc_traversal_method[0-5]. **\n");
945      break;
946    }
947  }
948  options->traversalMethod = traversalMethod;
949
950  flagValue = Cmd_FlagReadByName("ardc_group_size");
951  if (flagValue != NIL(char)) {
952    sscanf(flagValue, "%d", &value);
953    if (value > 0)
954      groupSize = value;
955    else {
956      fprintf(vis_stderr,
957              "** ardc error : invalid value %s for ardc_group_size[>0]. **\n",
958              flagValue);
959    }
960  }
961  options->groupSize = groupSize;
962
963  flagValue = Cmd_FlagReadByName("ardc_affinity_factor");
964  if (flagValue != NIL(char)) {
965    sscanf(flagValue, "%f", &affinity);
966    if (affinity >= 0.0 && affinity <= 1.0)
967      affinityFactor = affinity;
968    else {
969      fprintf(vis_stderr,
970     "** ardc error : invalid value %s for ardc_affinity_factor[0.0-1.0]. **\n",
971              flagValue);
972    }
973  }
974  options->affinityFactor = affinityFactor;
975
976  flagValue = Cmd_FlagReadByName("ardc_constrain_method");
977  if (flagValue != NIL(char)) {
978    sscanf(flagValue, "%d", &value);
979    switch (value) {
980    case 0 :
981      constrainMethod = Img_Restrict_c;
982      break;
983    case 1 :
984      constrainMethod = Img_Constrain_c;
985      break;
986    case 2 :
987      if (bdd_get_package_name() != CUDD) {
988        fprintf(vis_stderr, "** ardc error : Compact in ardc_constrain_method");
989        fprintf(vis_stderr, " is currently supported by only CUDD. **\n");
990        break;
991      }
992      constrainMethod = Img_Compact_c;
993      break;
994    case 3 :
995      if (bdd_get_package_name() != CUDD) {
996        fprintf(vis_stderr, "** ardc error : Squeeze in ardc_constrain_method");
997        fprintf(vis_stderr, " is currently supported by only CUDD. **\n");
998        break;
999      }
1000      constrainMethod = Img_Squeeze_c;
1001      break;
1002    case 4 :
1003      constrainMethod = Img_And_c;
1004      break;
1005    default :
1006      fprintf(vis_stderr,
1007      "** ardc error : invalid value %s for ardc_constrain_method[0-4]. **\n",
1008              flagValue);
1009      break;
1010    }
1011  }
1012  options->constrainMethod = constrainMethod;
1013
1014  flagValue = Cmd_FlagReadByName("ardc_constran_to");
1015  if (flagValue != NIL(char)) {
1016    sscanf(flagValue, "%d", &value);
1017    switch (value) {
1018    case 0 :
1019      constrainTarget = Fsm_Ardc_Constrain_Tr_c;
1020      break;
1021    case 1 :
1022      constrainTarget = Fsm_Ardc_Constrain_Initial_c;
1023      break;
1024    case 2 :
1025      constrainTarget = Fsm_Ardc_Constrain_Both_c;
1026      break;
1027    default :
1028      fprintf(vis_stderr,
1029        "** ardc error : invalid value %s for ardc_constrain_target[0-2]. **\n",
1030            flagValue);
1031      break;
1032    }
1033  }
1034  options->constrainTarget = constrainTarget;
1035
1036  flagValue = Cmd_FlagReadByName("ardc_max_iteration");
1037  if (flagValue != NIL(char)) {
1038    sscanf(flagValue, "%d", &value);
1039    if (value >= 0)
1040      maxIteration = value;
1041    else {
1042      fprintf(vis_stderr,
1043        "** ardc error : invalid value %s for ardc_max_iteration[>=0]. **\n",
1044        flagValue);
1045    }
1046  }
1047  options->maxIteration = maxIteration;
1048
1049  flagValue = Cmd_FlagReadByName("ardc_abstract_pseudo_input");
1050  if (flagValue != NIL(char)) {
1051    sscanf(flagValue, "%d", &value);
1052    switch (value) {
1053    case 0 :
1054      abstractPseudoInput = Fsm_Ardc_Abst_Ppi_No_c;
1055      break;
1056    case 1 :
1057      abstractPseudoInput = Fsm_Ardc_Abst_Ppi_Before_Image_c;
1058      break;
1059    case 2 :
1060      abstractPseudoInput = Fsm_Ardc_Abst_Ppi_After_Image_c;
1061      break;
1062    case 3 :
1063      abstractPseudoInput = Fsm_Ardc_Abst_Ppi_At_End_c;
1064      break;
1065    default :
1066      fprintf(vis_stderr, "** ardc error : invalid value %s", flagValue);
1067      fprintf(vis_stderr, " for ardc_abstract_pseudo_input[0-3]. **\n");
1068      break;
1069    }
1070  }
1071  options->abstractPseudoInput = abstractPseudoInput;
1072
1073  decomposeFlag = FsmGetArdcSetBooleanValue("ardc_decompose_flag",
1074                                                decomposeFlag);
1075  options->decomposeFlag = decomposeFlag;
1076
1077  projectedInitialFlag =
1078                        FsmGetArdcSetBooleanValue("ardc_projected_initial_flag",
1079                                                projectedInitialFlag);
1080  options->projectedInitialFlag = projectedInitialFlag;
1081
1082  constrainReorderFlag = FsmGetArdcSetBooleanValue("ardc_constrain_reorder",
1083                                                constrainReorderFlag);
1084  options->constrainReorderFlag = constrainReorderFlag;
1085
1086  flagValue = Cmd_FlagReadByName("ardc_image_method");
1087  if (flagValue != NIL(char)) {
1088    if (strcmp(flagValue, "monolithic") == 0)
1089      ardcImageMethod = Img_Monolithic_c;
1090    else if (strcmp(flagValue, "iwls95") == 0)
1091      ardcImageMethod = Img_Iwls95_c;
1092    else if (strcmp(flagValue, "mlp") == 0)
1093      ardcImageMethod = Img_Mlp_c;
1094    else if (strcmp(flagValue, "tfm") == 0)
1095      ardcImageMethod = Img_Tfm_c;
1096    else if (strcmp(flagValue, "hybrid") == 0)
1097      ardcImageMethod = Img_Hybrid_c;
1098    else
1099      fprintf(vis_stderr, "** ardc error : invalid value %s\n", flagValue);
1100  }
1101  options->ardcImageMethod = ardcImageMethod;
1102
1103  useHighDensity = FsmGetArdcSetBooleanValue("ardc_use_high_density",
1104                                          useHighDensity);
1105  options->useHighDensity = useHighDensity;
1106
1107  createPseudoVarMode = GetArdcSetIntValue("ardc_create_pseudo_var_mode", 0, 2,
1108                                           createPseudoVarMode);
1109  options->createPseudoVarMode = createPseudoVarMode;
1110
1111  reorderPtrFlag = FsmGetArdcSetBooleanValue("ardc_reorder_ptr",
1112                                                reorderPtrFlag);
1113  options->reorderPtrFlag = reorderPtrFlag;
1114
1115  faninConstrainMode = GetArdcSetIntValue("ardc_fanin_constrain_mode", 0, 1,
1116                                           faninConstrainMode);
1117  options->faninConstrainMode = faninConstrainMode;
1118
1119  flagValue = Cmd_FlagReadByName("ardc_read_group");
1120  if (flagValue)
1121    options->readGroupFile = flagValue;
1122  else
1123    options->readGroupFile = NIL(char);
1124
1125  flagValue = Cmd_FlagReadByName("ardc_write_group");
1126  if (flagValue)
1127    options->writeGroupFile = flagValue;
1128  else
1129    options->writeGroupFile = NIL(char);
1130
1131  lmbmInitialStatesMode = GetArdcSetIntValue("ardc_lmbm_initial_mode", 0, 2,
1132                                                lmbmInitialStatesMode);
1133  options->lmbmInitialStatesMode = lmbmInitialStatesMode;
1134
1135  mbmReuseTrFlag = FsmGetArdcSetBooleanValue("ardc_mbm_reuse_tr",
1136                                                mbmReuseTrFlag);
1137  options->mbmReuseTrFlag = mbmReuseTrFlag;
1138
1139  verbosity = GetArdcSetIntValue("ardc_verbosity", 0, 3, verbosity);
1140  options->verbosity = verbosity;
1141}
1142
1143
1144/**Function********************************************************************
1145
1146  Synopsis    [Reads traversal method option.]
1147
1148  Description [Reads traversal method option.]
1149
1150  SideEffects []
1151
1152  SeeAlso     []
1153
1154******************************************************************************/
1155Fsm_Ardc_TraversalType_t
1156Fsm_ArdcOptionsReadTraversalMethod(Fsm_ArdcOptions_t *options)
1157{
1158  return(options->traversalMethod);
1159}
1160
1161
1162/**Function********************************************************************
1163
1164  Synopsis    [Reads group size option.]
1165
1166  Description [Reads group size option.]
1167
1168  SideEffects []
1169
1170  SeeAlso     []
1171
1172******************************************************************************/
1173int
1174Fsm_ArdcOptionsReadGroupSize(Fsm_ArdcOptions_t *options)
1175{
1176  return(options->groupSize);
1177}
1178
1179
1180/**Function********************************************************************
1181
1182  Synopsis    [Reads affinity factor option.]
1183
1184  Description [Reads affinity factor option.]
1185
1186  SideEffects []
1187
1188  SeeAlso     []
1189
1190******************************************************************************/
1191float
1192Fsm_ArdcOptionsReadAffinityFactor(Fsm_ArdcOptions_t *options)
1193{
1194  return(options->affinityFactor);
1195}
1196
1197
1198/**Function********************************************************************
1199
1200  Synopsis    [Reads constrain method option.]
1201
1202  Description [Reads constrain method option.]
1203
1204  SideEffects []
1205
1206  SeeAlso     []
1207
1208******************************************************************************/
1209Img_MinimizeType
1210Fsm_ArdcOptionsReadConstrainMethod(Fsm_ArdcOptions_t *options)
1211{
1212  return(options->constrainMethod);
1213}
1214
1215
1216/**Function********************************************************************
1217
1218  Synopsis    [Reads constrain option.]
1219
1220  Description [Reads constrain option.]
1221
1222  SideEffects []
1223
1224  SeeAlso     []
1225
1226******************************************************************************/
1227Fsm_Ardc_ConstrainTargetType_t
1228Fsm_ArdcOptionsReadConstrainTarget(Fsm_ArdcOptions_t *options)
1229{
1230  return(options->constrainTarget);
1231}
1232
1233
1234/**Function********************************************************************
1235
1236  Synopsis    [Reads max iteration option.]
1237
1238  Description [Reads max iteration option.]
1239
1240  SideEffects []
1241
1242  SeeAlso     []
1243
1244******************************************************************************/
1245int
1246Fsm_ArdcOptionsReadMaxIteration(Fsm_ArdcOptions_t *options)
1247{
1248  return(options->maxIteration);
1249}
1250
1251
1252/**Function********************************************************************
1253
1254  Synopsis    [Reads abstract pseudo input option.]
1255
1256  Description [Reads abstract pseudo input option.]
1257
1258  SideEffects []
1259
1260  SeeAlso     []
1261
1262******************************************************************************/
1263Fsm_Ardc_AbstPpiType_t
1264Fsm_ArdcOptionsReadAbstractPseudoInput(Fsm_ArdcOptions_t *options)
1265{
1266  return(options->abstractPseudoInput);
1267}
1268
1269
1270/**Function********************************************************************
1271
1272  Synopsis    [Reads decomposed constraint option.]
1273
1274  Description [Reads decomposed constraint option.]
1275
1276  SideEffects []
1277
1278  SeeAlso     []
1279
1280******************************************************************************/
1281boolean
1282Fsm_ArdcOptionsReadDecomposeFlag(Fsm_ArdcOptions_t *options)
1283{
1284  return(options->decomposeFlag);
1285}
1286
1287
1288/**Function********************************************************************
1289
1290  Synopsis    [Reads initial states mode option.]
1291
1292  Description [Reads initial states mode option.]
1293
1294  SideEffects []
1295
1296  SeeAlso     []
1297
1298******************************************************************************/
1299boolean
1300Fsm_ArdcOptionsReadProjectedInitialFlag(Fsm_ArdcOptions_t *options)
1301{
1302  return(options->projectedInitialFlag);
1303}
1304
1305
1306/**Function********************************************************************
1307
1308  Synopsis    [Reads constrain reorder flag option.]
1309
1310  Description [Reads constrain reorder flag option.]
1311
1312  SideEffects []
1313
1314  SeeAlso     []
1315
1316******************************************************************************/
1317boolean
1318Fsm_ArdcOptionsReadConstrainReorderFlag(Fsm_ArdcOptions_t *options)
1319{
1320  return(options->constrainReorderFlag);
1321}
1322
1323
1324/**Function********************************************************************
1325
1326  Synopsis    [Reads image method for ARDC computation.]
1327
1328  Description [Reads image method for ARDC computation.]
1329
1330  SideEffects []
1331
1332  SeeAlso     []
1333
1334******************************************************************************/
1335Img_MethodType
1336Fsm_ArdcOptionsReadImageMethod(Fsm_ArdcOptions_t *options)
1337{
1338  return(options->ardcImageMethod);
1339}
1340
1341
1342/**Function********************************************************************
1343
1344  Synopsis    [Reads use high density option.]
1345
1346  Description [Reads use high density option.]
1347
1348  SideEffects []
1349
1350  SeeAlso     []
1351
1352******************************************************************************/
1353boolean
1354Fsm_ArdcOptionsReadUseHighDensity(Fsm_ArdcOptions_t *options)
1355{
1356  return(options->useHighDensity);
1357}
1358
1359
1360/**Function********************************************************************
1361
1362  Synopsis    [Reads verbosity option.]
1363
1364  Description [Reads verbosity option.]
1365
1366  SideEffects []
1367
1368  SeeAlso     []
1369
1370******************************************************************************/
1371int
1372Fsm_ArdcOptionsReadVerbosity(Fsm_ArdcOptions_t *options)
1373{
1374  return(options->verbosity);
1375}
1376
1377
1378/**Function********************************************************************
1379
1380  Synopsis    [Sets traversal method option.]
1381
1382  Description [Sets traversal method option.]
1383
1384  SideEffects []
1385
1386  SeeAlso     []
1387
1388******************************************************************************/
1389void
1390Fsm_ArdcOptionsSetTraversalMethod(Fsm_ArdcOptions_t *options,
1391                                  Fsm_Ardc_TraversalType_t traversalMethod)
1392{
1393  options->traversalMethod = traversalMethod;
1394}
1395
1396
1397/**Function********************************************************************
1398
1399  Synopsis    [Sets group size option.]
1400
1401  Description [Sets group size option.]
1402
1403  SideEffects []
1404
1405  SeeAlso     []
1406
1407******************************************************************************/
1408void
1409Fsm_ArdcOptionsSetGroupSize(Fsm_ArdcOptions_t *options, int groupSize)
1410{
1411  options->groupSize = groupSize;
1412}
1413
1414
1415/**Function********************************************************************
1416
1417  Synopsis    [Sets affinity factor option.]
1418
1419  Description [Sets affinity factor option.]
1420
1421  SideEffects []
1422
1423  SeeAlso     []
1424
1425******************************************************************************/
1426void
1427Fsm_ArdcOptionsSetAffinityFactor(Fsm_ArdcOptions_t *options,
1428                                 float affinityFactor)
1429{
1430  options->affinityFactor = affinityFactor;
1431}
1432
1433
1434/**Function********************************************************************
1435
1436  Synopsis    [Sets constrain method option.]
1437
1438  Description [Sets constrain method option.]
1439
1440  SideEffects []
1441
1442  SeeAlso     []
1443
1444******************************************************************************/
1445void
1446Fsm_ArdcOptionsSetConstrainMethod(Fsm_ArdcOptions_t *options,
1447                                  Img_MinimizeType constrainMethod)
1448{
1449  options->constrainMethod = constrainMethod;
1450}
1451
1452
1453/**Function********************************************************************
1454
1455  Synopsis    [Sets constrain option.]
1456
1457  Description [Sets constrain option.]
1458
1459  SideEffects []
1460
1461  SeeAlso     []
1462
1463******************************************************************************/
1464void
1465Fsm_ArdcOptionsSetConstrainTarget(Fsm_ArdcOptions_t *options,
1466                                Fsm_Ardc_ConstrainTargetType_t constrainTarget)
1467{
1468  options->constrainTarget = constrainTarget;
1469}
1470
1471
1472/**Function********************************************************************
1473
1474  Synopsis    [Sets max iteration option.]
1475
1476  Description [Sets max iteration option.]
1477
1478  SideEffects []
1479
1480  SeeAlso     []
1481
1482******************************************************************************/
1483void
1484Fsm_ArdcOptionsSetMaxIteration(Fsm_ArdcOptions_t *options, int maxIteration)
1485{
1486  options->maxIteration = maxIteration;
1487}
1488
1489
1490/**Function********************************************************************
1491
1492  Synopsis    [Sets abstract pseudo input option.]
1493
1494  Description [Sets abstract pseudo input option.]
1495
1496  SideEffects []
1497
1498  SeeAlso     []
1499
1500******************************************************************************/
1501void
1502Fsm_ArdcOptionsSetAbstractPseudoInput(Fsm_ArdcOptions_t *options,
1503                              Fsm_Ardc_AbstPpiType_t abstractPseudoInput)
1504{
1505  options->abstractPseudoInput = abstractPseudoInput;
1506}
1507
1508
1509/**Function********************************************************************
1510
1511  Synopsis    [Sets decomposed constraint option.]
1512
1513  Description [Sets decomposed constraint option.]
1514
1515  SideEffects []
1516
1517  SeeAlso     []
1518
1519******************************************************************************/
1520void
1521Fsm_ArdcOptionsSetDecomposeFlag(Fsm_ArdcOptions_t *options,
1522                                boolean decomposeFlag)
1523{
1524  options->decomposeFlag = decomposeFlag;
1525}
1526
1527
1528/**Function********************************************************************
1529
1530  Synopsis    [Sets initial states mode option.]
1531
1532  Description [Sets initial states mode option.]
1533
1534  SideEffects []
1535
1536  SeeAlso     []
1537
1538******************************************************************************/
1539void
1540Fsm_ArdcOptionsSetProjectedInitialFlag(Fsm_ArdcOptions_t *options,
1541                                       boolean projectedInitialFlag)
1542{
1543  options->projectedInitialFlag = projectedInitialFlag;
1544}
1545
1546
1547/**Function********************************************************************
1548
1549  Synopsis    [Sets constrain reorder flag option.]
1550
1551  Description [Sets constrain reorder flag option.]
1552
1553  SideEffects []
1554
1555  SeeAlso     []
1556
1557******************************************************************************/
1558void
1559Fsm_ArdcOptionsSetConstrainReorderFlag(Fsm_ArdcOptions_t *options,
1560                                       int constrainReorderFlag)
1561{
1562  options->constrainReorderFlag = constrainReorderFlag;
1563}
1564
1565
1566/**Function********************************************************************
1567
1568  Synopsis    [Sets image method for ARDC computation.]
1569
1570  Description [Sets image method for ARDC computation.]
1571
1572  SideEffects []
1573
1574  SeeAlso     []
1575
1576******************************************************************************/
1577void
1578Fsm_ArdcOptionsSetImageMethod(Fsm_ArdcOptions_t *options,
1579                                Img_MethodType ardcImageMethod)
1580{
1581  options->ardcImageMethod = ardcImageMethod;
1582}
1583
1584
1585/**Function********************************************************************
1586
1587  Synopsis    [Sets use high density option.]
1588
1589  Description [Sets use high density option.]
1590
1591  SideEffects []
1592
1593  SeeAlso     []
1594
1595******************************************************************************/
1596void
1597Fsm_ArdcOptionsSetUseHighDensity(Fsm_ArdcOptions_t *options,
1598                                 boolean useHighDensity)
1599{
1600  options->useHighDensity = useHighDensity;
1601}
1602
1603
1604/**Function********************************************************************
1605
1606  Synopsis    [Sets verbosity option.]
1607
1608  Description [Sets verbosity option.]
1609
1610  SideEffects []
1611
1612  SeeAlso     []
1613
1614******************************************************************************/
1615void
1616Fsm_ArdcOptionsSetVerbosity(Fsm_ArdcOptions_t *options, int verbosity)
1617{
1618  options->verbosity = verbosity;
1619}
1620
1621
1622/**Function********************************************************************
1623
1624  Synopsis    [Returns the number of approximate reachable states of an FSM.]
1625
1626  Description [Returns the number of approximate reachable states of an FSM.]
1627
1628  SideEffects []
1629
1630  SeeAlso     []
1631
1632******************************************************************************/
1633double
1634Fsm_ArdcCountOnsetOfOverApproximateReachableStates(Fsm_Fsm_t *fsm)
1635{
1636  mdd_t *reached;
1637  array_t *psVars, *reachedArray;
1638  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
1639  double numReached = 1.0, tmpReached;
1640  int i;
1641
1642  if (!Fsm_FsmReadCurrentOverApproximateReachableStates(fsm))
1643    return(0.0);
1644
1645  reachedArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm);
1646  arrayForEachItem(mdd_t *, reachedArray, i, reached) {
1647    psVars = array_fetch(array_t *, fsm->reachabilityInfo.subPsVars, i);
1648    tmpReached = mdd_count_onset(mddManager, reached, psVars);
1649    numReached *= tmpReached;
1650  }
1651
1652  return(numReached);
1653}
1654
1655/**Function********************************************************************
1656
1657  Synopsis    [Returns the bdd size of the set of approximate reachable
1658  states of an FSM.]
1659
1660  Description [Returns the bdd size of the set of approximate reachable
1661  states of an FSM.]
1662
1663  SideEffects []
1664
1665  SeeAlso     []
1666
1667******************************************************************************/
1668int
1669Fsm_ArdcBddSizeOfOverApproximateReachableStates(Fsm_Fsm_t *fsm)
1670{
1671  mdd_t *reached;
1672  array_t *reachedArray;
1673  int i, size = 0;
1674
1675  if (!Fsm_FsmReadCurrentOverApproximateReachableStates(fsm))
1676    return(0);
1677
1678  reachedArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm);
1679  arrayForEachItem(mdd_t *, reachedArray, i, reached) {
1680    size += mdd_size(reached);
1681  }
1682
1683  return(size);
1684}
1685
1686/**Function********************************************************************
1687
1688  Synopsis    [Returns the conjunction of approximate reachable states of
1689  an FSM.]
1690
1691  Description [Returns the conjunction of approximate reachable states of
1692  an FSM.]
1693
1694  SideEffects []
1695
1696  SeeAlso     []
1697
1698******************************************************************************/
1699mdd_t *
1700Fsm_ArdcGetMddOfOverApproximateReachableStates(Fsm_Fsm_t *fsm)
1701{
1702  mdd_t         *reached, *reachedSet, *tmp;
1703  mdd_manager   *mddManager = Fsm_FsmReadMddManager(fsm);
1704  array_t       *reachedArray;
1705  int           i;
1706
1707  if (!Fsm_FsmReadCurrentOverApproximateReachableStates(fsm))
1708    return(NIL(mdd_t));
1709
1710  reachedSet = mdd_one(mddManager);
1711  reachedArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm);
1712  arrayForEachItem(mdd_t *, reachedArray, i, reached) {
1713    tmp = reachedSet;
1714    reachedSet = mdd_and(reachedSet, reached, 1, 1);
1715    mdd_free(tmp);
1716  }
1717
1718  return(reachedSet);
1719}
1720
1721/**Function********************************************************************
1722
1723  Synopsis    [Prints info about overapproximate reachable states.]
1724
1725  Description [Prints info about overapproximate reachable states.]
1726
1727  SideEffects []
1728
1729  SeeAlso []
1730
1731******************************************************************************/
1732void
1733Fsm_ArdcPrintReachabilityResults(Fsm_Fsm_t *fsm, long elapseTime)
1734{
1735  array_t *psVars = Fsm_FsmReadPresentStateVars(fsm);
1736  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
1737  int nvars = mdd_get_number_of_bdd_vars(mddMgr, psVars);
1738  char apprStr[24], ardcStr[24];
1739
1740  if (nvars <= EPD_MAX_BIN) {
1741    double mintermAppr, mintermArdc;
1742
1743    mintermAppr = Fsm_ArdcCountOnsetOfOverApproximateReachableStates(fsm);
1744    sprintf(apprStr, "%10g", mintermAppr);
1745    mintermArdc = pow((double)2.0, (double)nvars) - mintermAppr;
1746    sprintf(ardcStr, "%10g", mintermArdc);
1747  } else {
1748    EpDouble apprEpd, ardcEpd;
1749
1750    ArdcEpdCountOnsetOfOverApproximateReachableStates(fsm, &apprEpd);
1751    EpdPow2(nvars, &ardcEpd);
1752    EpdSubtract2(&ardcEpd, &apprEpd);
1753    EpdGetString(&apprEpd, apprStr);
1754    EpdGetString(&ardcEpd, ardcStr);
1755  }
1756
1757  (void)fprintf(vis_stdout,"***********************************************\n");
1758  (void)fprintf(vis_stdout,"Over-approximate Reachability analysis results:\n");
1759  (void)fprintf(vis_stdout, "%-30s%s\n", "reachable states = ", apprStr);
1760  (void)fprintf(vis_stdout, "%-30s%s\n", "unreachable states(ARDCs) = ",
1761                ardcStr);
1762  (void)fprintf(vis_stdout, "%-30s%10d\n", "BDD size = ",
1763                Fsm_ArdcBddSizeOfOverApproximateReachableStates(fsm));
1764  (void)fprintf(vis_stdout, "%-30s%10g\n", "analysis time = ",
1765                (double)elapseTime / 1000.0);
1766  switch (FsmReadReachabilityOverApproxComputationStatus(fsm)) {
1767  case Fsm_Ardc_NotConverged_c :
1768    (void) fprintf(vis_stdout, "%-30s%10s\n", "reachability status = ",
1769                   "not converged(invalid)");
1770    break;
1771  case Fsm_Ardc_Valid_c :
1772    (void) fprintf(vis_stdout, "%-30s%10s\n", "reachability status = ",
1773                   "not converged(valid)");
1774    break;
1775  case Fsm_Ardc_Converged_c :
1776    (void) fprintf(vis_stdout, "%-30s%10s\n", "reachability status = ",
1777                   "converged");
1778    break;
1779  case Fsm_Ardc_Exact_c :
1780    (void) fprintf(vis_stdout, "%-30s%10s\n", "reachability status = ",
1781                   "exact");
1782    break;
1783  default :
1784    break;
1785  }
1786}
1787
1788/**Function********************************************************************
1789
1790  Synopsis    [Reads ARDC verbosity option.]
1791
1792  Description [Reads ARDC verbosity option.]
1793
1794  SideEffects []
1795
1796  SeeAlso     []
1797
1798******************************************************************************/
1799int
1800Fsm_ArdcReadVerbosity(void)
1801{
1802  char *flagValue;
1803  int verbosity = 0;
1804
1805  flagValue = Cmd_FlagReadByName("ardc_verbosity");
1806  if (flagValue != NIL(char))
1807    sscanf(flagValue, "%d", &verbosity);
1808  return(verbosity);
1809}
1810
1811
1812/*---------------------------------------------------------------------------*/
1813/* Definition of internal functions                                          */
1814/*---------------------------------------------------------------------------*/
1815
1816/**Function********************************************************************
1817
1818  Synopsis    [Check if each conjunct is contained in the invariant.]
1819
1820  Description [Check if each conjunct is contained in the invariant.]
1821
1822  SideEffects []
1823
1824  SeeAlso []
1825
1826******************************************************************************/
1827int
1828FsmArdcCheckInvariant(Fsm_Fsm_t *fsm, array_t *invarStates)
1829{
1830  array_t *overApproxArray;
1831  mdd_t *conjunct;
1832  int i, j;
1833  mdd_t *invariant;
1834
1835  overApproxArray = Fsm_ArdcComputeOverApproximateReachableStates(fsm,
1836    0, 0, 0, 0, 0, 0, 0, 0, NIL(Fsm_ArdcOptions_t));
1837
1838  /* for each invariant check if the over approx holds */
1839  arrayForEachItem(mdd_t *, invarStates, i, invariant) {
1840    arrayForEachItem(mdd_t *, overApproxArray, j, conjunct) {
1841      if (conjunct == NIL(mdd_t))
1842        continue;
1843      if (!mdd_lequal(conjunct, invariant, 1, 1))
1844        return 0;
1845    }
1846  }
1847  return 1;
1848}
1849
1850
1851/**Function********************************************************************
1852
1853  Synopsis    [Prints ARDC options currently in use.]
1854
1855  Description [Prints ARDC options currently in use.]
1856
1857  SideEffects []
1858
1859  SeeAlso []
1860
1861******************************************************************************/
1862void
1863FsmArdcPrintOptions(void)
1864{
1865  Fsm_ArdcOptions_t     options;
1866  char                  dummy[31];
1867
1868  Fsm_ArdcGetDefaultOptions(&options);
1869
1870  switch (options.traversalMethod) {
1871  case Fsm_Ardc_Traversal_Mbm_c :
1872    sprintf(dummy, "MBM");
1873    break;
1874  case Fsm_Ardc_Traversal_Rfbf_c :
1875    sprintf(dummy, "RFBF");
1876    break;
1877  case Fsm_Ardc_Traversal_Tfbf_c :
1878    sprintf(dummy, "TFBF");
1879    break;
1880  case Fsm_Ardc_Traversal_Tmbm_c :
1881    sprintf(dummy, "TMBM");
1882    break;
1883  case Fsm_Ardc_Traversal_Lmbm_c :
1884    sprintf(dummy, "LMBM");
1885    break;
1886  case Fsm_Ardc_Traversal_Tlmbm_c :
1887    sprintf(dummy, "TLMBM");
1888    break;
1889  case Fsm_Ardc_Traversal_Simple_c :
1890    sprintf(dummy, "SIMPLE");
1891    break;
1892  default :
1893    sprintf(dummy, "invalid");
1894    break;
1895  }
1896  fprintf(vis_stdout, "ARDC: ardc_traversal_method = %d (%s)\n",
1897          options.traversalMethod, dummy);
1898  fprintf(vis_stdout, "ARDC: ardc_group_size = %d\n", options.groupSize);
1899  fprintf(vis_stdout, "ARDC: ardc_affinity_factor = %f\n",
1900          options.affinityFactor);
1901  fprintf(vis_stdout, "ARDC: ardc_max_iteration = %d\n", options.maxIteration);
1902  switch (options.constrainTarget) {
1903  case Fsm_Ardc_Constrain_Tr_c :
1904    sprintf(dummy, "transition relation");
1905    break;
1906  case Fsm_Ardc_Constrain_Initial_c :
1907    sprintf(dummy, "initial");
1908    break;
1909  case Fsm_Ardc_Constrain_Both_c :
1910    sprintf(dummy, "both");
1911    break;
1912  default :
1913    sprintf(dummy, "invalid");
1914    break;
1915  }
1916  fprintf(vis_stdout, "ARDC: ardc_constrain_target = %d (%s)\n",
1917          options.constrainTarget, dummy);
1918  switch (options.constrainMethod) {
1919  case Img_Restrict_c :
1920    sprintf(dummy, "restrict");
1921    break;
1922  case Img_Constrain_c :
1923    sprintf(dummy, "constrain");
1924    break;
1925  case Img_Compact_c :
1926    sprintf(dummy, "compact");
1927    break;
1928  case Img_Squeeze_c :
1929    sprintf(dummy, "squeeze");
1930    break;
1931  case Img_And_c :
1932    sprintf(dummy, "and");
1933    break;
1934  case Img_DefaultMinimizeMethod_c :
1935    sprintf(dummy, "restrict");
1936    break;
1937  default :
1938    sprintf(dummy, "invalid");
1939    break;
1940  }
1941  fprintf(vis_stdout, "ARDC: ardc_constrain_method = %d (%s)\n",
1942          options.constrainMethod, dummy);
1943  if (options.constrainReorderFlag)
1944    sprintf(dummy, "yes");
1945  else
1946    sprintf(dummy, "no");
1947  fprintf(vis_stdout, "ARDC: ardc_constrain_reorder = %s\n", dummy);
1948  if (options.decomposeFlag)
1949    sprintf(dummy, "yes");
1950  else
1951    sprintf(dummy, "no");
1952  fprintf(vis_stdout, "ARDC: ardc_decompose_flag = %s\n", dummy);
1953  switch (options.abstractPseudoInput) {
1954  case Fsm_Ardc_Abst_Ppi_No_c :
1955    sprintf(dummy, "no");
1956    break;
1957  case Fsm_Ardc_Abst_Ppi_Before_Image_c :
1958    sprintf(dummy, "before image");
1959    break;
1960  case Fsm_Ardc_Abst_Ppi_After_Image_c :
1961    sprintf(dummy, "after image");
1962    break;
1963  case Fsm_Ardc_Abst_Ppi_At_End_c :
1964    sprintf(dummy, "at end");
1965    break;
1966  default :
1967    sprintf(dummy, "invalid");
1968    break;
1969  }
1970  fprintf(vis_stdout, "ARDC: ardc_abstract_pseudo_input = %d (%s)\n",
1971          options.abstractPseudoInput, dummy);
1972  if (options.projectedInitialFlag)
1973    sprintf(dummy, "yes");
1974  else
1975    sprintf(dummy, "no");
1976  fprintf(vis_stdout, "ARDC: ardc_projected_initial_flag = %s\n", dummy);
1977  if (options.ardcImageMethod == Img_Monolithic_c)
1978    sprintf(dummy, "monolithic");
1979  else if (options.ardcImageMethod == Img_Tfm_c)
1980    sprintf(dummy, "tfm");
1981  else if (options.ardcImageMethod == Img_Hybrid_c)
1982    sprintf(dummy, "hybrid");
1983  else if (options.ardcImageMethod == Img_Mlp_c)
1984    sprintf(dummy, "mlp");
1985  else
1986    sprintf(dummy, "iwls95");
1987  fprintf(vis_stdout, "ARDC: ardc_image_method = %s\n", dummy);
1988  if (options.useHighDensity)
1989    sprintf(dummy, "yes");
1990  else
1991    sprintf(dummy, "no");
1992  fprintf(vis_stdout, "ARDC: ardc_use_high_density = %s\n", dummy);
1993  if (options.reorderPtrFlag)
1994    sprintf(dummy, "yes");
1995  else
1996    sprintf(dummy, "no");
1997  fprintf(vis_stdout, "ARDC: ardc_reorder_ptr = %s\n", dummy);
1998  if (options.faninConstrainMode == 0)
1999    sprintf(dummy, "only fanin");
2000  else
2001    sprintf(dummy, "fanin + itself");
2002  fprintf(vis_stdout, "ARDC: ardc_fanin_constrain_mode = %d (%s)\n",
2003          options.faninConstrainMode, dummy);
2004  if (options.createPseudoVarMode == 0)
2005    sprintf(dummy, "with exact support");
2006  else if (options.createPseudoVarMode == 1)
2007    sprintf(dummy, "all the other submachines");
2008  else
2009    sprintf(dummy, "only fanin submachines");
2010  fprintf(vis_stdout, "ARDC: ardc_create_pseudo_var_mode = %d (%s)\n",
2011          options.createPseudoVarMode, dummy);
2012  if (options.lmbmInitialStatesMode == 0)
2013    sprintf(dummy, "given initial");
2014  else if (options.lmbmInitialStatesMode == 1)
2015    sprintf(dummy, "reached set");
2016  else
2017    sprintf(dummy, "frontier set");
2018  fprintf(vis_stdout, "ARDC: ardc_lmbm_initial_mode = %d (%s)\n",
2019          options.lmbmInitialStatesMode, dummy);
2020  if (options.mbmReuseTrFlag)
2021    sprintf(dummy, "yes");
2022  else
2023    sprintf(dummy, "no");
2024  fprintf(vis_stdout, "ARDC: ardc_mbm_reuse_tr = %s\n", dummy);
2025  if (options.readGroupFile)
2026    fprintf(vis_stdout, "ARDC: ardc_read_group = %s\n", options.readGroupFile);
2027  else
2028    fprintf(vis_stdout, "ARDC: ardc_read_group = nil\n");
2029  if (options.writeGroupFile) {
2030    fprintf(vis_stdout, "ARDC: ardc_write_group = %s\n",
2031            options.writeGroupFile);
2032  } else
2033    fprintf(vis_stdout, "ARDC: ardc_write_group = nil\n");
2034  fprintf(vis_stdout, "ARDC: ardc_verbosity = %d\n", options.verbosity);
2035  fprintf(vis_stdout,
2036          "See help page on print_ardc_options for setting these options\n");
2037}
2038
2039
2040
2041/**Function********************************************************************
2042
2043  Synopsis    [Prints BDDS of approximate reachable states of an FSM.]
2044
2045  Description [Prints BDDS of approximate reachable states of an FSM.]
2046
2047  SideEffects []
2048
2049  SeeAlso []
2050
2051******************************************************************************/
2052void
2053FsmArdcPrintOverApproximateReachableStates(Fsm_Fsm_t *fsm)
2054{
2055  mdd_t *appr;
2056  array_t       *mddIdArr;
2057
2058  if (!Fsm_FsmTestIsOverApproximateReachabilityDone(fsm)) {
2059  fprintf(vis_stdout, "** ardc warning : no approximate reachable states **\n");
2060    return;
2061  }
2062  appr = Fsm_ArdcGetMddOfOverApproximateReachableStates(fsm);
2063  mddIdArr = Fsm_FsmReadPresentStateVars(fsm);
2064  PrintBddWithName(fsm, mddIdArr, appr);
2065}
2066
2067/**Function********************************************************************
2068
2069  Synopsis    [Prints BDDS of exact reachable states of an FSM.]
2070
2071  Description [Prints BDDS of exact reachable states of an FSM.]
2072
2073  SideEffects []
2074
2075  SeeAlso []
2076
2077******************************************************************************/
2078void
2079FsmArdcPrintExactReachableStates(Fsm_Fsm_t *fsm)
2080{
2081  mdd_t *reachableStates;
2082  array_t       *mddIdArr;
2083
2084  if (!Fsm_FsmTestIsReachabilityDone(fsm)) {
2085    fprintf(vis_stdout, "** ardc warning : no reachable states **\n");
2086    return;
2087  }
2088  reachableStates = Fsm_FsmReadReachableStates(fsm);
2089  mddIdArr = Fsm_FsmReadPresentStateVars(fsm);
2090  PrintBddWithName(fsm, mddIdArr, reachableStates);
2091}
2092
2093
2094/**Function********************************************************************
2095
2096  Synopsis    [Prints BDDs of a node.]
2097
2098  Description [Prints BDDs of a node.]
2099
2100  SideEffects []
2101
2102  SeeAlso []
2103
2104******************************************************************************/
2105void
2106FsmArdcPrintBddOfNode(Fsm_Fsm_t *fsm, mdd_t *node)
2107{
2108  PrintBddWithName(fsm, NIL(array_t), node);
2109}
2110
2111
2112/**Function********************************************************************
2113
2114  Synopsis    [Prints array of array of integer.]
2115
2116  Description [Prints array of array of integer.]
2117
2118  SideEffects []
2119
2120  SeeAlso     []
2121
2122******************************************************************************/
2123void
2124FsmArdcPrintArrayOfArrayInt(array_t *arrayOfArray)
2125{
2126  int           i, j, n;
2127  array_t       *array;
2128
2129  for (i = 0; i < array_n(arrayOfArray); i++) {
2130    array = array_fetch(array_t *, arrayOfArray, i);
2131    fprintf(vis_stdout, "array[%d] =", i);
2132    for (j = 0; j < array_n(array); j++) {
2133      n = array_fetch(int, array, j);
2134      fprintf(vis_stdout, " %d", n);
2135    }
2136    fprintf(vis_stdout, "\n");
2137  }
2138}
2139
2140/**Function********************************************************************
2141
2142  Synopsis    [Returns a set Boolean value related ARDC computation.]
2143
2144  Description [Returns a set Boolean value related ARDC computation.]
2145
2146  SideEffects []
2147
2148  SeeAlso     []
2149
2150******************************************************************************/
2151boolean
2152FsmGetArdcSetBooleanValue(char *string, boolean defaultValue)
2153{
2154  char          *flagValue;
2155  boolean       value = defaultValue;
2156
2157  flagValue = Cmd_FlagReadByName(string);
2158  if (flagValue != NIL(char)) {
2159    if (strcmp(flagValue, "yes") == 0)
2160      value = TRUE;
2161    else if (strcmp(flagValue, "no") == 0)
2162      value = FALSE;
2163    else {
2164      fprintf(vis_stderr,
2165              "** ardc error : invalid value %s for %s[yes/no]. **\n",
2166              flagValue, string);
2167    }
2168  }
2169
2170  return(value);
2171}
2172
2173
2174
2175/*---------------------------------------------------------------------------*/
2176/* Definition of static functions                                            */
2177/*---------------------------------------------------------------------------*/
2178
2179
2180/**Function********************************************************************
2181
2182  Synopsis    [Sorts subfsms so that a subfsm with smaller fanins comes first.]
2183
2184  Description [Sorts subfsms so that a subfsm with smaller fanins comes first.]
2185
2186  SideEffects []
2187
2188  SeeAlso []
2189
2190******************************************************************************/
2191static void
2192SortSubFsmsForApproximateTraversal(array_t **subFsmArray,
2193                                   array_t **fanInsIndexArray,
2194                                   array_t **fanOutsIndexArray,
2195                                   int verbosityLevel)
2196{
2197  int           n = array_n(*subFsmArray);
2198  array_t       *newSubFsmArray;
2199  array_t       *newFanInsIndexArray;
2200  array_t       *newFanOutsIndexArray;
2201  int           i, j, smallest;
2202  Fsm_Fsm_t     *subFsm;
2203  array_t       *fanIns, *fanOuts;
2204  Fsm_Fsm_t     *smallestSubFsm = NIL(Fsm_Fsm_t);
2205  array_t       *smallestFanIns = NIL(array_t);
2206  array_t       *smallestFanOuts = NIL(array_t);
2207  int           *flag;
2208  int           *nFanIns, *nFanOuts;
2209  int           fanIn, fanOut;
2210  int           *order = NIL(int);
2211  int           *target;
2212
2213  newSubFsmArray = array_alloc(Fsm_Fsm_t *, 0);
2214  newFanInsIndexArray = array_alloc(array_t *, 0);
2215  newFanOutsIndexArray = array_alloc(array_t *, 0);
2216
2217  flag = ALLOC(int, n);
2218  (void)memset((void *)flag, 0, sizeof(int) * n);
2219
2220  if (verbosityLevel > 1)
2221    order = ALLOC(int, n);
2222  target = ALLOC(int, n);
2223  nFanIns = ALLOC(int, n);
2224  nFanOuts = ALLOC(int, n);
2225  for (i = 0; i < n; i++) {
2226    fanIns = array_fetch(array_t *, *fanInsIndexArray, i);
2227    nFanIns[i] = array_n(fanIns);
2228    fanOuts = array_fetch(array_t *, *fanOutsIndexArray, i);
2229    nFanOuts[i] = array_n(fanOuts);
2230  }
2231
2232  for (i = 0; i < n; i++) {
2233    /*
2234    ** finds a submachine which has the smallest number of fanins
2235    ** if tie, use number of fanouts
2236    */
2237    smallest = -1;
2238    for (j = 0; j < n; j++) {
2239      if (flag[j])
2240        continue;
2241      subFsm = array_fetch(Fsm_Fsm_t *, *subFsmArray, j);
2242      fanIns = array_fetch(array_t *, *fanInsIndexArray, j);
2243      fanOuts = array_fetch(array_t *, *fanOutsIndexArray, j);
2244      if (smallest == -1 || nFanIns[j] < nFanIns[smallest] ||
2245          (nFanIns[j] == nFanIns[smallest] &&
2246           nFanOuts[j] < nFanOuts[smallest])) {
2247        smallest = j;
2248        smallestSubFsm = subFsm;
2249        smallestFanIns = fanIns;
2250        smallestFanOuts = fanOuts;
2251      }
2252    }
2253    target[smallest] = i;
2254    if (verbosityLevel > 1)
2255      order[i] = smallest;
2256    flag[smallest] = 1;
2257    array_insert_last(Fsm_Fsm_t *, newSubFsmArray, smallestSubFsm);
2258    array_insert_last(array_t *, newFanInsIndexArray, smallestFanIns);
2259    array_insert_last(array_t *, newFanOutsIndexArray, smallestFanOuts);
2260    /*
2261    ** decrease number of fanouts by 1 from each submachine
2262    ** which is not chosen yet
2263    */
2264    for (j = 0; j < array_n(smallestFanIns); j++) {
2265      fanIn = array_fetch(int, smallestFanIns, j);
2266      if (flag[fanIn])
2267        continue;
2268      nFanOuts[fanIn]--;
2269    }
2270    /*
2271    ** decrease number of fanins by 1 from each submachine
2272    ** which is not chosen yet
2273    */
2274    for (j = 0; j < array_n(smallestFanOuts); j++) {
2275      fanOut = array_fetch(int, smallestFanOuts, j);
2276      if (flag[fanOut])
2277        continue;
2278      nFanIns[fanOut]--;
2279    }
2280  }
2281
2282  /* make new fanins & fanouts  index array according to new order */
2283  for (i = 0; i < n; i++) {
2284    fanIns = array_fetch(array_t *, newFanInsIndexArray, i);
2285    for (j = 0; j < array_n(fanIns); j++) {
2286      fanIn = array_fetch(int, fanIns, j);
2287      array_insert(int, fanIns, j, target[fanIn]);
2288    }
2289    fanOuts = array_fetch(array_t *, newFanOutsIndexArray, i);
2290    for (j = 0; j < array_n(fanOuts); j++) {
2291      fanOut = array_fetch(int, fanOuts, j);
2292      array_insert(int, fanOuts, j, target[fanOut]);
2293    }
2294  }
2295
2296  if (verbosityLevel > 1) {
2297    int k;
2298
2299    fprintf(vis_stdout, "=== sorted sub-fsm order ===\n");
2300    for (i = 0; i < n; i++)
2301      fprintf(vis_stdout, " %d", order[i]);
2302    fprintf(vis_stdout, "\n");
2303
2304    for (i = 0; i < n; i++) {
2305      fprintf(vis_stdout, "SUB-FSM [%d]\n", i);
2306      fanIns = array_fetch(array_t *, newFanInsIndexArray, i);
2307      fanOuts = array_fetch(array_t *, newFanOutsIndexArray, i);
2308      fprintf(vis_stdout, "== fanins(%d) :", array_n(fanIns));
2309      for (j = 0; j < array_n(fanIns); j++) {
2310        k = array_fetch(int, fanIns, j);
2311        fprintf(vis_stdout, " %d", k);
2312      }
2313      fprintf(vis_stdout, "\n");
2314      fprintf(vis_stdout, "== fanouts(%d) :", array_n(fanOuts));
2315      for (j = 0; j < array_n(fanOuts); j++) {
2316        k = array_fetch(int, fanOuts, j);
2317        fprintf(vis_stdout, " %d", k);
2318      }
2319      fprintf(vis_stdout, "\n");
2320    }
2321  }
2322
2323  FREE(flag);
2324  FREE(nFanIns);
2325  FREE(nFanOuts);
2326  if (verbosityLevel > 1)
2327    FREE(order);
2328  FREE(target);
2329  array_free(*subFsmArray);
2330  array_free(*fanInsIndexArray);
2331  array_free(*fanOutsIndexArray);
2332  *subFsmArray = newSubFsmArray;
2333  *fanInsIndexArray = newFanInsIndexArray;
2334  *fanOutsIndexArray = newFanOutsIndexArray;
2335}
2336
2337
2338/**Function********************************************************************
2339
2340  Synopsis    [Computes an upper bound to the reachable states of an FSM
2341  by MBM.]
2342
2343  Description [Computes an upper bound to the reachable states of an
2344  FSM by MBM or LMBM. This computation proceeds in an event-driven
2345  manner. First it computes the reachable states of all submachines,
2346  then only for those submachines such that any of their fanin
2347  submachine's reachable states have changed. It recomputes reachable
2348  states by constraining the transition relation with respect to the
2349  reached states of all fanin submachines. This is iterated until it
2350  converges. The basic algorithm for MBM is almost same as the one in Hyunwoo
2351  Cho's paper in TCAD96, except as noted below.
2352  0. Cho's algorithm uses transition function for image computation,
2353     whereas we use either the transition function or the transition relation
2354     depending on the image computation method.
2355  1. constrainTarget
2356     In Cho's papers, there are two versions of algorithms: one is constraining
2357     transition relation, the other is initial states, so this function
2358     includes these two as well as the case of both.
2359     0) Fsm_Ardc_Constrain_Tr_c      : constrain transition relation (default).
2360     1) Fsm_Ardc_Constrain_Initial_c : constrain initial state.
2361     2) Fsm_Ardc_Constrain_Both_c    : constrain both.
2362  2. decomposeFlag
2363     To perform the above constraining operation, we can make the constraint
2364     either conjoined (as single bdd) or decomposed (as array of bdds) from
2365     the reachable states of fanin submachines of the current submachine.
2366     To have same interface for these two, array of constraints is used.
2367  3. dynamic variable reordering
2368     In Cho's algorithm, dynamic variable ordering is not allowed, but
2369     it is here. Also, refer to 5. (restore-containment).
2370  4. abstractPseudoInput
2371     To make faster convergence, we can abstract pseudo primary input
2372     variables early, but refer to 5. (restore-containment).
2373     0) Fsm_Ardc_Abst_Ppi_No_c           : do not abstract pseudo-input
2374                                           variables.
2375     1) Fsm_Ardc_Abst_Ppi_Before_Image_c : abstract before image computation
2376                                           (default).
2377     2) Fsm_Ardc_Abst_Ppi_After_Image_c  : abstract after image computation.
2378     3) Fsm_Ardc_Abst_Ppi_At_End_c       : abstract at the end of approximate
2379                                           traversal.
2380  5. restore-constainment
2381     Due to 3 (dynamic variable reordering) and 4 (abstractPseudoInput),
2382     current reachable states may not be a subset of previous reachable
2383     states. In this case, we correct current reachable state to the
2384     intersection of current and previous reachable states. But, in FBF,
2385     we need to take the union of the two.
2386  6. projectedInitialFlag
2387     When we do reachability analysis of submachines, initial states of
2388     a submachine can be one of the following. In Cho's paper, projected
2389     initial states was used.
2390     0) FALSE : use original initial states for submachine
2391     1) TRUE  : use projected initial states for submachine (default)
2392  ]
2393
2394  SideEffects []
2395
2396  SeeAlso [ArdcRfbfTraversal ArdcTfbfTraversal ArdcTmbmTraversal
2397  ArdcSimpleTraversal]
2398
2399******************************************************************************/
2400static array_t *
2401ArdcMbmTraversal(
2402  Fsm_Fsm_t *fsm,
2403  int nvars,
2404  array_t *subFsmArray,
2405  array_t *fanInsIndexArray,
2406  array_t *fanOutsIndexArray,
2407  mdd_t ***subReached /* sub-result for TMBM, pointer of bdd array */,
2408  /* The following arguments up to approxFlag are passed for exact
2409   * reachability. */
2410  int incrementalFlag,
2411  int verbosityLevel,
2412  int printStep,
2413  int depthValue,
2414  int shellFlag,
2415  int reorderFlag,
2416  int reorderThreshold,
2417  Fsm_RchType_t approxFlag,
2418  Fsm_ArdcOptions_t *options,
2419  boolean lfpFlag /* If TRUE, performs LMBM */
2420  )
2421{
2422  mdd_manager           *mddManager;
2423  int                   i, n = array_n(subFsmArray);
2424  int                   *traverse;
2425  mdd_t                 **reached, **constraint;
2426  mdd_t                 **oldReached;
2427  mdd_t                 **frontier;
2428  int                   converged = 0;
2429  Fsm_Fsm_t             **subFsm;
2430  array_t               *fans;
2431  mdd_t                 *tmp;
2432  int                   iteration = 0;
2433  mdd_t                 **initial = NIL(mdd_t *);
2434  array_t               *reachedArray = array_alloc(mdd_t *, 0);
2435  array_t               *faninConstrainArray;
2436  Img_ImageInfo_t       *imageInfo = NIL(Img_ImageInfo_t);
2437  int                   dynStatus;
2438  bdd_reorder_type_t    dynMethod;
2439  boolean               restoreContainmentFlag;
2440  boolean               reuseTrFlag = FALSE;
2441                        /* If set, just update the transition relation
2442                           without copying the original transition relation */
2443  boolean               reused = FALSE;
2444  boolean               duplicate;
2445  boolean               tmpReorderPtrFlag;
2446  int                   nConstrainOps = 0;
2447  long                  tImgComps = 0;
2448  long                  tConstrainOps = 0;
2449  long                  tRestoreContainment = 0;
2450  long                  tAbstractVars = 0;
2451  long                  tBuildTr = 0;
2452  long                  initialTime = 0, finalTime;
2453  int                   maxIteration = options->maxIteration;
2454  int                   constrainTarget = options->constrainTarget;
2455  boolean               decomposeFlag = options->decomposeFlag;
2456  int                   abstractPseudoInput = options->abstractPseudoInput;
2457  Img_MinimizeType      constrainMethod = options->constrainMethod;
2458  boolean               projectedInitialFlag = options->projectedInitialFlag;
2459  int                   ardcVerbosity = options->verbosity;
2460  boolean               constrainReorderFlag = options->constrainReorderFlag;
2461  boolean               reorderPtrFlag = options->reorderPtrFlag;
2462  int                   faninConstrainMode = options->faninConstrainMode;
2463  int                   lmbmInitialStatesMode = options->lmbmInitialStatesMode;
2464
2465  reuseTrFlag = FsmGetArdcSetBooleanValue("ardc_mbm_reuse_tr", reuseTrFlag);
2466  if (reuseTrFlag && lfpFlag) {
2467    /* This is to use the i-th constrained transition relation in
2468     * the (i+1)-th iteration, instead of the original transition relation.
2469     * Therefore, the i-th constraint should be a superset of the (i+1)-th. */
2470    fprintf(vis_stderr,
2471            "** ardc error : can't reuse transition relation in LMBM. **\n");
2472    reuseTrFlag = FALSE;
2473  }
2474
2475  Img_ResetNumberOfImageComputation(Img_Forward_c);
2476
2477  reached = ALLOC(mdd_t *, n);
2478  constraint = ALLOC(mdd_t *, n);
2479  traverse = ALLOC(int, n);     /* array used for scheduling */
2480  subFsm = ALLOC(Fsm_Fsm_t *, n);
2481  oldReached = ALLOC(mdd_t *, n);
2482
2483  mddManager = Fsm_FsmReadMddManager(fsm);
2484  for (i = 0; i < n; i++) {
2485    subFsm[i] = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
2486    oldReached[i] = NIL(mdd_t);
2487  }
2488
2489  /* Set up. */
2490  if (lfpFlag) {                /* LMBM */
2491    initial = ALLOC(mdd_t *, n);
2492    for (i = 0; i < n; i++)
2493      initial[i] = Fsm_FsmComputeInitialStates(subFsm[i]);
2494    if (lmbmInitialStatesMode >= 1)     /* restart from frontier states */
2495      frontier = ALLOC(mdd_t *, n);
2496    else
2497      frontier = NIL(mdd_t *);
2498
2499    for (i = 0; i < n; i++) {
2500      reached[i] = mdd_dup(initial[i]);
2501      constraint[i] = mdd_dup(initial[i]);
2502      traverse[i] = 1;
2503      if (frontier)
2504        frontier[i] = NIL(mdd_t);
2505    }
2506  } else {                      /* MBM */
2507    for (i = 0; i < n; i++) {
2508      reached[i] = mdd_one(mddManager);
2509      constraint[i] = mdd_one(mddManager);
2510      traverse[i] = 1;
2511    }
2512
2513    if (constrainTarget == Fsm_Ardc_Constrain_Initial_c ||
2514        constrainTarget == Fsm_Ardc_Constrain_Both_c) {
2515      initial = ALLOC(mdd_t *, n);
2516      for (i = 0; i < n; i++)
2517        initial[i] = Fsm_FsmComputeInitialStates(subFsm[i]);
2518    }
2519
2520    frontier = NIL(mdd_t *);
2521  }
2522
2523  /* Set the flag for containment restoration according to the options. */
2524  if (constrainMethod == Img_Constrain_c &&
2525      constrainReorderFlag == FALSE &&
2526      abstractPseudoInput == Fsm_Ardc_Abst_Ppi_No_c) {
2527    restoreContainmentFlag = FALSE;
2528  } else
2529    restoreContainmentFlag = TRUE;
2530
2531  /* Compute fixpoint. */
2532  do {
2533    converged = 1;
2534    for (i = 0; i < n; i++) {
2535      if (!traverse[i])
2536        continue;
2537      if (ardcVerbosity > 1)
2538        fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i);
2539      if (oldReached[i])
2540        mdd_free(oldReached[i]);
2541      oldReached[i] = reached[i];
2542      /* Build constraint array. */
2543      faninConstrainArray = array_alloc(mdd_t *, 0);
2544      fans = array_fetch(array_t *, fanInsIndexArray, i);
2545      ComputeFaninConstrainArray(faninConstrainArray, constraint,
2546                                 i, fans, decomposeFlag, faninConstrainMode);
2547      /* Build constrained transition relation. */
2548      dynStatus = bdd_reordering_status(mddManager, &dynMethod);
2549      if (dynStatus != 0 && constrainReorderFlag == 0)
2550        bdd_dynamic_reordering_disable(mddManager);
2551      if (ardcVerbosity > 0)
2552        initialTime = util_cpu_time();
2553      imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm[i], 0, 1); /* forward */
2554      if (ardcVerbosity > 0) {
2555        finalTime = util_cpu_time();
2556        tBuildTr += finalTime - initialTime;
2557      }
2558      /* Minimize the transition relation of the current submachine w.r.t.
2559       * the reached set of its fanin submachines.
2560       */
2561      if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) {
2562        int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
2563        if (ardcVerbosity > 2)
2564          Img_SetPrintMinimizeStatus(imageInfo, 2);
2565        else if (ardcVerbosity > 0)
2566          Img_SetPrintMinimizeStatus(imageInfo, 1);
2567        else
2568          Img_SetPrintMinimizeStatus(imageInfo, 0);
2569        if (reuseTrFlag) {
2570          if (reused)
2571            duplicate = FALSE;
2572          else
2573            duplicate = TRUE;
2574        } else
2575          duplicate = TRUE;
2576        if (reorderPtrFlag &&
2577            abstractPseudoInput != Fsm_Ardc_Abst_Ppi_Before_Image_c) {
2578          tmpReorderPtrFlag = 1;
2579        } else
2580          tmpReorderPtrFlag = 0;
2581        if (ardcVerbosity > 0)
2582          initialTime = util_cpu_time();
2583        MinimizeTransitionRelationWithFaninConstraint(imageInfo,
2584                faninConstrainArray, constrainMethod, tmpReorderPtrFlag,
2585                duplicate);
2586        if (ardcVerbosity > 0) {
2587          finalTime = util_cpu_time();
2588          tConstrainOps += finalTime - initialTime;
2589        }
2590        Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
2591      }
2592      if (constrainTarget != Fsm_Ardc_Constrain_Tr_c) {
2593        ComputeConstrainedInitialStates(subFsm[i], faninConstrainArray,
2594                                        constrainMethod);
2595      }
2596      nConstrainOps++;
2597      mdd_array_free(faninConstrainArray);
2598      /* Restore dynamic reordering options if they had been changed. */
2599      if (dynStatus != 0 && constrainReorderFlag == 0) {
2600        bdd_dynamic_reordering(mddManager, dynMethod,
2601                               BDD_REORDER_VERBOSITY_DEFAULT);
2602      }
2603      /* Quantify pseudo-input variables from the transition relation. */
2604      if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
2605        int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
2606        if (ardcVerbosity > 2)
2607          Img_SetPrintMinimizeStatus(imageInfo, 2);
2608        else if (ardcVerbosity > 0)
2609          Img_SetPrintMinimizeStatus(imageInfo, 1);
2610        else
2611          Img_SetPrintMinimizeStatus(imageInfo, 0);
2612        if (ardcVerbosity > 0)
2613          initialTime = util_cpu_time();
2614        Img_AbstractTransitionRelation(imageInfo,
2615          subFsm[i]->fsmData.pseudoInputBddVars,
2616          subFsm[i]->fsmData.pseudoInputCube, Img_Forward_c);
2617        if (reorderPtrFlag)
2618          Img_ReorderPartitionedTransitionRelation(imageInfo, Img_Forward_c);
2619        if (ardcVerbosity > 0) {
2620          finalTime = util_cpu_time();
2621          tAbstractVars += finalTime - initialTime;
2622        }
2623        Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
2624      }
2625      if (lfpFlag && lmbmInitialStatesMode > 0 && iteration > 0) {
2626        /* Update the initial states to either reached or frontier. */
2627        FsmSetReachabilityApproxComputationStatus(subFsm[i], Fsm_Rch_Under_c);
2628        mdd_free(subFsm[i]->reachabilityInfo.initialStates);
2629        if (lmbmInitialStatesMode == 1)
2630          subFsm[i]->reachabilityInfo.initialStates = mdd_dup(reached[i]);
2631        else
2632          subFsm[i]->reachabilityInfo.initialStates = mdd_dup(frontier[i]);
2633      } else {
2634        /* Reset the reachable states for a new reachability. */
2635        if (subFsm[i]->reachabilityInfo.reachableStates) {
2636          mdd_free(subFsm[i]->reachabilityInfo.reachableStates);
2637          subFsm[i]->reachabilityInfo.reachableStates = NIL(mdd_t);
2638        }
2639        subFsm[i]->reachabilityInfo.depth = 0;
2640      }
2641      /* Traverse this submachine. */
2642      if (ardcVerbosity > 0)
2643        initialTime = util_cpu_time();
2644      reached[i] = Fsm_FsmComputeReachableStates(subFsm[i],
2645                incrementalFlag, verbosityLevel, printStep, depthValue,
2646                shellFlag, reorderFlag, reorderThreshold,
2647                approxFlag, 0, 0, NIL(array_t), FALSE, NIL(array_t));
2648      if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
2649          Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
2650        Img_TfmFlushCache(imageInfo, FALSE);
2651      }
2652      if (ardcVerbosity > 0) {
2653        finalTime = util_cpu_time();
2654        tImgComps += finalTime - initialTime;
2655      }
2656      /* Compute the frontier for LMBM. */
2657      if (lfpFlag && lmbmInitialStatesMode > 0) {
2658        if (lmbmInitialStatesMode >= 1) {
2659          if (iteration == 0)
2660            frontier[i] = mdd_dup(reached[i]);
2661          else {
2662            mdd_t       *fromLowerBound;
2663
2664            fromLowerBound = mdd_and(reached[i], oldReached[i], 1, 0);
2665            tmp = reached[i];
2666            reached[i] = mdd_or(oldReached[i], tmp, 1, 1);
2667            mdd_free(tmp);
2668            mdd_free(frontier[i]);
2669            if (lmbmInitialStatesMode == 2) {
2670              frontier[i] = bdd_between(fromLowerBound, reached[i]);
2671              mdd_free(fromLowerBound);
2672            } else
2673              frontier[i] = fromLowerBound;
2674          }
2675        }
2676        if (iteration > 0) {
2677          mdd_free(subFsm[i]->reachabilityInfo.initialStates);
2678          subFsm[i]->reachabilityInfo.initialStates = mdd_dup(initial[i]);
2679        }
2680      }
2681      /* Restore the original transition relation. */
2682      if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) {
2683        if (!reuseTrFlag)
2684          Img_RestoreTransitionRelation(imageInfo, Img_Forward_c);
2685      }
2686      /* Quantify the pseudo-input variables from reached. */
2687      if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_After_Image_c) {
2688        if (ardcVerbosity > 0)
2689          initialTime = util_cpu_time();
2690        if (n > 1) {
2691          tmp = reached[i];
2692          reached[i] = QuantifyVariables(reached[i],
2693                                subFsm[i]->fsmData.pseudoInputBddVars,
2694                                subFsm[i]->fsmData.pseudoInputCube);
2695          mdd_free(tmp);
2696        }
2697        if (ardcVerbosity > 0) {
2698          finalTime = util_cpu_time();
2699          tAbstractVars += finalTime - initialTime;
2700        }
2701      }
2702
2703      mdd_free(constraint[i]);
2704      constraint[i] = mdd_dup(reached[i]);
2705      /* Update traversal schedule and possibly restore containment. */
2706      traverse[i] = 0;
2707      if (!mdd_equal(oldReached[i], reached[i])) {
2708        if (ardcVerbosity > 2) {
2709          double        r1, r2;
2710
2711          r1 = mdd_count_onset(mddManager, reached[i],
2712                               subFsm[i]->fsmData.presentStateVars);
2713          r2 = mdd_count_onset(mddManager, oldReached[i],
2714                               subFsm[i]->fsmData.presentStateVars);
2715          fprintf(vis_stdout, "oldReached = %g, reached = %g\n", r2, r1);
2716        }
2717
2718        /* Restore-containment operation. */
2719        if (restoreContainmentFlag) {
2720          if (ardcVerbosity > 0)
2721            initialTime = util_cpu_time();
2722          if (lfpFlag) {        /* LMBM */
2723            if (mdd_lequal(oldReached[i], reached[i], 1, 1)) {
2724              /* Containment OK. */
2725              fans = array_fetch(array_t *, fanOutsIndexArray, i);
2726              UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag);
2727            } else {
2728              /* Restoration needed. */
2729              if (ardcVerbosity > 1) {
2730                fprintf(vis_stdout,
2731    "** ardc info: reached is not superset of oldReached in subFsm[%d] **\n",
2732                        i);
2733              }
2734              mdd_free(reached[i]);
2735              reached[i] = mdd_or(oldReached[i],
2736                        subFsm[i]->reachabilityInfo.reachableStates, 1, 1);
2737              mdd_free(subFsm[i]->reachabilityInfo.reachableStates);
2738              subFsm[i]->reachabilityInfo.reachableStates = mdd_dup(reached[i]);
2739              mdd_free(constraint[i]);
2740              constraint[i] = mdd_dup(reached[i]);
2741              if (!mdd_equal(oldReached[i], reached[i])) {
2742                fans = array_fetch(array_t *, fanOutsIndexArray, i);
2743                UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag);
2744              }
2745            }
2746          } else {              /* MBM */
2747            if (!mdd_lequal(reached[i], oldReached[i], 1, 1)) {
2748              /* Restoration needed. */
2749              if (ardcVerbosity > 1) {
2750                fprintf(vis_stdout,
2751    "** ardc info: reached is not subset of oldReached in subFsm[%d] **\n", i);
2752              }
2753              mdd_free(reached[i]);
2754              reached[i] = mdd_and(oldReached[i],
2755                        subFsm[i]->reachabilityInfo.reachableStates, 1, 1);
2756              mdd_free(subFsm[i]->reachabilityInfo.reachableStates);
2757              subFsm[i]->reachabilityInfo.reachableStates = mdd_dup(reached[i]);
2758              mdd_free(constraint[i]);
2759              constraint[i] = mdd_dup(reached[i]);
2760              if (!mdd_equal(oldReached[i], reached[i])) {
2761                fans = array_fetch(array_t *, fanOutsIndexArray, i);
2762                UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag);
2763              }
2764            } else {
2765              /* Containment OK. */
2766              fans = array_fetch(array_t *, fanOutsIndexArray, i);
2767              UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag);
2768            }
2769          }
2770          if (ardcVerbosity > 0) {
2771            finalTime = util_cpu_time();
2772            tRestoreContainment += finalTime - initialTime;
2773          }
2774        } else {                /* no containment restoration needed */
2775          fans = array_fetch(array_t *, fanOutsIndexArray, i);
2776          UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag);
2777        }
2778      }
2779    }
2780    /* Check for convergence. */
2781    for (i = 0; i < n; i++) {
2782      if (traverse[i]) {
2783        converged = 0;
2784        break;
2785      }
2786    }
2787    iteration++;
2788    if (ardcVerbosity > 0) {
2789      boolean   supportCheckFlag = FALSE;
2790
2791      /* Print the current reached states and check the supports. */
2792      if (projectedInitialFlag ||
2793          abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
2794        supportCheckFlag = TRUE;
2795      }
2796      if (lfpFlag) {
2797        PrintCurrentReachedStates(mddManager, subFsm, reached,
2798                                  Fsm_Ardc_Traversal_Lmbm_c,
2799                                  n, iteration, nvars, ardcVerbosity,
2800                                  supportCheckFlag);
2801      } else {
2802        PrintCurrentReachedStates(mddManager, subFsm, reached,
2803                                  Fsm_Ardc_Traversal_Mbm_c,
2804                                  n, iteration, nvars, ardcVerbosity,
2805                                  supportCheckFlag);
2806      }
2807    }
2808
2809    if (iteration == maxIteration)
2810      break;
2811  } while (!converged);
2812
2813  /* Restore the original transtion relation. */
2814  if (reuseTrFlag) {
2815    if (constrainTarget != Fsm_Ardc_Constrain_Initial_c)
2816      Img_RestoreTransitionRelation(imageInfo, Img_Forward_c);
2817  }
2818
2819  if (ardcVerbosity > 0) {
2820    if (lfpFlag)
2821      fprintf(vis_stdout, "LMBM : total iterations %d\n", iteration);
2822    else
2823      fprintf(vis_stdout, "MBM : total iterations %d\n", iteration);
2824  }
2825
2826  /* Reset the initial states to the original. */
2827  if (constrainTarget == Fsm_Ardc_Constrain_Initial_c ||
2828      constrainTarget == Fsm_Ardc_Constrain_Both_c || lfpFlag) {
2829    for (i = 0; i < n; i++) {
2830      mdd_free(subFsm[i]->reachabilityInfo.initialStates);
2831      subFsm[i]->reachabilityInfo.initialStates = initial[i];
2832    }
2833    FREE(initial);
2834  }
2835
2836  /* Quantify the pseudo-input variables from reached. */
2837  if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_At_End_c) {
2838    if (ardcVerbosity > 0)
2839      initialTime = util_cpu_time();
2840    for (i = 0; i < n; i++) {
2841      tmp = reached[i];
2842      reached[i] = QuantifyVariables(reached[i],
2843                                subFsm[i]->fsmData.pseudoInputBddVars,
2844                                subFsm[i]->fsmData.pseudoInputCube);
2845      mdd_free(tmp);
2846    }
2847    if (ardcVerbosity > 0) {
2848      finalTime = util_cpu_time();
2849      tAbstractVars += finalTime - initialTime;
2850    }
2851  }
2852
2853  /* Set the status of current overapproximate reached states. */
2854  if (converged)
2855    FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Converged_c);
2856  else if (lfpFlag)
2857    FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_NotConverged_c);
2858  else
2859    FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Valid_c);
2860
2861  ComputeApproximateReachableStatesArray(mddManager, reachedArray,
2862                                         reached, subReached, n,
2863                                         decomposeFlag);
2864  /* Clean up. */
2865  if (decomposeFlag) {
2866    for (i = 0; i < n; i++) {
2867      mdd_free(oldReached[i]);
2868      mdd_free(constraint[i]);
2869    }
2870  } else {
2871    for (i = 0; i < n; i++) {
2872      mdd_free(oldReached[i]);
2873      if (subReached == NULL)
2874        mdd_free(reached[i]);
2875      mdd_free(constraint[i]);
2876    }
2877  }
2878
2879  if (subReached)
2880    *subReached = reached;
2881  else
2882    FREE(reached);
2883  FREE(traverse);
2884  FREE(constraint);
2885  FREE(subFsm);
2886  FREE(oldReached);
2887  if (lfpFlag && lmbmInitialStatesMode >= 1) {/*consistent:from >1 to >=1 C.W*/
2888    for (i = 0; i < n; i++) {
2889      if (frontier[i])
2890        mdd_free(frontier[i]);
2891    }
2892    FREE(frontier);
2893  }
2894
2895  /* Print final stats. */
2896  if (ardcVerbosity > 0) {
2897    fprintf(vis_stdout, "%d image computations, %d constrain operations\n",
2898        Img_GetNumberOfImageComputation(Img_Forward_c), nConstrainOps);
2899    fprintf(vis_stdout,
2900        "image computation time = %g, constrain operation time = %g\n",
2901        (double)tImgComps / 1000.0, (double)tConstrainOps / 1000.0);
2902    fprintf(vis_stdout, "restore-containment time = %g\n",
2903        (double)tRestoreContainment / 1000.0);
2904    fprintf(vis_stdout, "abstract variables time = %g\n",
2905        (double)tAbstractVars / 1000.0);
2906    fprintf(vis_stdout, "build TR time = %g\n",
2907        (double)tBuildTr / 1000.0);
2908  }
2909
2910  return(reachedArray);
2911}
2912
2913
2914/**Function********************************************************************
2915
2916  Synopsis    [Computes an upperbound of an FSM by RFBF.]
2917
2918  Description [Computes an upperbound of an FSM by RFBF. It first
2919  sets all constraints to initial states, then does one image
2920  computation, then updates constraints with reached states. This is
2921  iteratively done until it gets converged. Refer the description of
2922  ArdcMbmTraversal(MBM).]
2923
2924  SideEffects []
2925
2926  SeeAlso [ArdcMbmTraversal ArdcTfbfTraversal ArdcTmbmTraversal
2927  ArdcSimpleTraversal]
2928
2929******************************************************************************/
2930static array_t *
2931ArdcRfbfTraversal(Fsm_Fsm_t *fsm, int nvars,
2932                  array_t *subFsmArray, array_t *fanInsIndexArray,
2933                  int incrementalFlag, int verbosityLevel,
2934                  int printStep, int depthValue, int shellFlag,
2935                  int reorderFlag, int reorderThreshold,
2936                  Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options)
2937{
2938  mdd_manager           *mddManager;
2939  int                   i, n = array_n(subFsmArray);
2940  mdd_t                 **reached, **constraint, **newConstraint;
2941  mdd_t                 **newReached, *to;
2942  int                   converged = 0;
2943  Fsm_Fsm_t             **subFsm;
2944  array_t               *fans;
2945  mdd_t                 *tmp;
2946  mdd_t                 *initialStates;
2947  int                   iteration = 0;
2948  mdd_t                 **initial = NIL(mdd_t *);
2949  array_t               *reachedArray = array_alloc(mdd_t *, 0);
2950  array_t               *faninConstrainArray;
2951  Img_ImageInfo_t       *imageInfo = NIL(Img_ImageInfo_t);
2952  int                   dynStatus;
2953  bdd_reorder_type_t    dynMethod;
2954  boolean               restoreContainmentFlag;
2955  mdd_t                 *toCareSet;
2956  array_t               *toCareSetArray = array_alloc(mdd_t *, 0);
2957  int                   depth = 0;
2958  boolean               tmpReorderPtrFlag;
2959  long                  tImgComps = 0;
2960  long                  tConstrainOps = 0;
2961  long                  initialTime = 0, finalTime;
2962  int                   maxIteration = options->maxIteration;
2963  int                   constrainTarget = options->constrainTarget;
2964  boolean               decomposeFlag = options->decomposeFlag;
2965  int                   abstractPseudoInput = options->abstractPseudoInput;
2966  Img_MinimizeType      constrainMethod = options->constrainMethod;
2967  boolean               projectedInitialFlag = options->projectedInitialFlag;
2968  int                   ardcVerbosity = options->verbosity;
2969  boolean               constrainReorderFlag = options->constrainReorderFlag;
2970  boolean               reorderPtrFlag = options->reorderPtrFlag;
2971  int                   faninConstrainMode = options->faninConstrainMode;
2972
2973  Img_ResetNumberOfImageComputation(Img_Forward_c);
2974
2975  reached = ALLOC(mdd_t *, n);
2976  constraint = ALLOC(mdd_t *, n);
2977  newConstraint = ALLOC(mdd_t *, n);
2978  subFsm = ALLOC(Fsm_Fsm_t *, n);
2979  newReached = ALLOC(mdd_t *, n);
2980
2981  mddManager = Fsm_FsmReadMddManager(fsm);
2982  for (i = 0; i < n; i++) {
2983    subFsm[i] = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
2984    initialStates = Fsm_FsmComputeInitialStates(subFsm[i]);
2985    reached[i] = initialStates;
2986    constraint[i] = mdd_dup(initialStates);
2987
2988    if (printStep && ((depth % printStep) == 0)) {
2989      if (ardcVerbosity > 1)
2990        fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i);
2991      (void)fprintf(vis_stdout,
2992                    "BFS step = %d\t|states| = %8g\tBdd size = %8ld\n", depth,
2993                    mdd_count_onset(mddManager, reached[i],
2994                                    subFsm[i]->fsmData.presentStateVars),
2995                    (long)mdd_size(reached[i]));
2996    }
2997  }
2998
2999  if (constrainTarget == Fsm_Ardc_Constrain_Initial_c ||
3000      constrainTarget == Fsm_Ardc_Constrain_Both_c) {
3001    initial = ALLOC(mdd_t *, n);
3002    for (i = 0; i < n; i++)
3003      initial[i] = mdd_dup(reached[i]);
3004  }
3005
3006  if (constrainMethod != Img_Constrain_c ||
3007      constrainReorderFlag == TRUE ||
3008      abstractPseudoInput != Fsm_Ardc_Abst_Ppi_No_c) {
3009    restoreContainmentFlag = TRUE;
3010  } else
3011    restoreContainmentFlag = FALSE;
3012
3013  converged = 0;
3014  do {
3015    depth++;
3016    for (i = 0; i < n; i++) {
3017      if (ardcVerbosity > 1)
3018        fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i);
3019      faninConstrainArray = array_alloc(mdd_t *, 0);
3020      fans = array_fetch(array_t *, fanInsIndexArray, i);
3021      ComputeFaninConstrainArray(faninConstrainArray, constraint,
3022                                 i, fans, decomposeFlag, faninConstrainMode);
3023      dynStatus = bdd_reordering_status(mddManager, &dynMethod);
3024      if (dynStatus != 0 && constrainReorderFlag == 0)
3025        bdd_dynamic_reordering_disable(mddManager);
3026      imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm[i], 0, 1);
3027      if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) {
3028        int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
3029        if (ardcVerbosity > 2)
3030          Img_SetPrintMinimizeStatus(imageInfo, 2);
3031        else if (ardcVerbosity > 0)
3032          Img_SetPrintMinimizeStatus(imageInfo, 1);
3033        else
3034          Img_SetPrintMinimizeStatus(imageInfo, 0);
3035        if (reorderPtrFlag &&
3036            abstractPseudoInput != Fsm_Ardc_Abst_Ppi_Before_Image_c) {
3037          tmpReorderPtrFlag = 1;
3038        } else
3039          tmpReorderPtrFlag = 0;
3040        if (ardcVerbosity > 0)
3041          initialTime = util_cpu_time();
3042        MinimizeTransitionRelationWithFaninConstraint(imageInfo,
3043                faninConstrainArray, constrainMethod, tmpReorderPtrFlag,
3044                TRUE);
3045        if (ardcVerbosity > 0) {
3046          finalTime = util_cpu_time();
3047          tConstrainOps += finalTime - initialTime;
3048        }
3049        Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
3050      }
3051      if (constrainTarget != Fsm_Ardc_Constrain_Tr_c) {
3052        ComputeConstrainedInitialStates(subFsm[i], faninConstrainArray,
3053                                        constrainMethod);
3054      }
3055      mdd_array_free(faninConstrainArray);
3056      if (dynStatus != 0 && constrainReorderFlag == 0) {
3057        bdd_dynamic_reordering(mddManager, dynMethod,
3058                               BDD_REORDER_VERBOSITY_DEFAULT);
3059      }
3060      if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
3061        int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
3062        if (ardcVerbosity > 2)
3063          Img_SetPrintMinimizeStatus(imageInfo, 2);
3064        else if (ardcVerbosity > 0)
3065          Img_SetPrintMinimizeStatus(imageInfo, 1);
3066        else
3067          Img_SetPrintMinimizeStatus(imageInfo, 0);
3068        Img_AbstractTransitionRelation(imageInfo,
3069          subFsm[i]->fsmData.pseudoInputBddVars,
3070          subFsm[i]->fsmData.pseudoInputCube, Img_Forward_c);
3071        if (reorderPtrFlag)
3072          Img_ReorderPartitionedTransitionRelation(imageInfo, Img_Forward_c);
3073        Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
3074      }
3075      toCareSet = mdd_not(reached[i]);
3076      array_insert(mdd_t *, toCareSetArray, 0, toCareSet);
3077      if (ardcVerbosity > 0)
3078        initialTime = util_cpu_time();
3079      to = Fsm_ArdcComputeImage(subFsm[i], reached[i], reached[i],
3080                                toCareSetArray);
3081      if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
3082          Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
3083        Img_TfmFlushCache(imageInfo, FALSE);
3084      }
3085      if (ardcVerbosity > 0) {
3086        finalTime = util_cpu_time();
3087        tImgComps += finalTime - initialTime;
3088      }
3089      mdd_free(toCareSet);
3090
3091      newReached[i] = mdd_or(reached[i], to, 1, 1);
3092      mdd_free(to);
3093      if (constrainTarget != Fsm_Ardc_Constrain_Initial_c)
3094        Img_RestoreTransitionRelation(imageInfo, Img_Forward_c);
3095      if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_After_Image_c) {
3096        tmp = newReached[i];
3097        newReached[i] = QuantifyVariables(newReached[i],
3098                                        subFsm[i]->fsmData.pseudoInputBddVars,
3099                                        subFsm[i]->fsmData.pseudoInputCube);
3100        mdd_free(tmp);
3101      }
3102
3103      /* restore-containment operation */
3104      if (restoreContainmentFlag) {
3105        if (!mdd_lequal(reached[i], newReached[i], 1, 1)) {
3106          if (ardcVerbosity > 2) {
3107            double      r1, r2;
3108
3109            fprintf(vis_stdout,
3110   "** ardc warning : newReached is not superset of reached in subFsm[%d] **\n",
3111                    i);
3112            r1 = mdd_count_onset(mddManager, reached[i],
3113                                 subFsm[i]->fsmData.presentStateVars);
3114            r2 = mdd_count_onset(mddManager, newReached[i],
3115                                 subFsm[i]->fsmData.presentStateVars);
3116            fprintf(vis_stdout, "reached = %g, newReached = %g\n", r1, r2);
3117          }
3118          tmp = newReached[i];
3119          newReached[i] = mdd_or(newReached[i], reached[i], 1, 1);
3120          mdd_free(tmp);
3121        }
3122      }
3123
3124      newConstraint[i] = mdd_dup(newReached[i]);
3125
3126      if (printStep && ((depth % printStep) == 0)) {
3127        (void)fprintf(vis_stdout,
3128                      "BFS step = %d\t|states| = %8g\tBdd size = %8ld\n",
3129                      depth, mdd_count_onset(mddManager, newReached[i],
3130                                     subFsm[i]->fsmData.presentStateVars),
3131                      (long)mdd_size(newReached[i]));
3132      }
3133    }
3134    converged = 1;
3135    for (i = 0; i < n; i++) {
3136      if (mdd_equal(reached[i], newReached[i]))
3137        mdd_free(newReached[i]);
3138      else {
3139        converged = 0;
3140        mdd_free(reached[i]);
3141        reached[i] = newReached[i];
3142      }
3143    }
3144    iteration++;
3145    if (ardcVerbosity > 0) {
3146      boolean   supportCheckFlag = FALSE;
3147
3148      if (projectedInitialFlag ||
3149          abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
3150        supportCheckFlag = TRUE;
3151      }
3152      PrintCurrentReachedStates(mddManager, subFsm, reached,
3153                                Fsm_Ardc_Traversal_Rfbf_c,
3154                                n, iteration, nvars, ardcVerbosity,
3155                                supportCheckFlag);
3156    }
3157
3158    /* update constraints */
3159    for (i = 0; i < n; i++) {
3160      mdd_free(constraint[i]);
3161      constraint[i] = newConstraint[i];
3162      newConstraint[i] = NIL(mdd_t);
3163    }
3164
3165    if (iteration == maxIteration)
3166      break;
3167  } while (!converged);
3168  if (ardcVerbosity > 0) {
3169    fprintf(vis_stdout, "RFBF : total iteration %d\n", iteration);
3170    fprintf(vis_stdout, "%d image computations, %d constrain operations\n",
3171        Img_GetNumberOfImageComputation(Img_Forward_c), n * iteration);
3172    fprintf(vis_stdout,
3173        "image computation time = %g, constrain operation time = %g\n",
3174        (double)tImgComps / 1000.0, (double)tConstrainOps / 1000.0);
3175  }
3176
3177  if (constrainTarget == Fsm_Ardc_Constrain_Initial_c ||
3178      constrainTarget == Fsm_Ardc_Constrain_Both_c) {
3179    for (i = 0; i < n; i++) {
3180      mdd_free(subFsm[i]->reachabilityInfo.initialStates);
3181      subFsm[i]->reachabilityInfo.initialStates = initial[i];
3182    }
3183    FREE(initial);
3184  }
3185
3186  if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_At_End_c) {
3187    for (i = 0; i < n; i++) {
3188      tmp = reached[i];
3189      reached[i] = QuantifyVariables(reached[i],
3190                                subFsm[i]->fsmData.pseudoInputBddVars,
3191                                subFsm[i]->fsmData.pseudoInputCube);
3192      mdd_free(tmp);
3193    }
3194  }
3195
3196  /* sets the status of current overapproximate reached states */
3197  if (converged)
3198    FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Converged_c);
3199  else
3200    FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_NotConverged_c);
3201
3202  ComputeApproximateReachableStatesArray(mddManager, reachedArray,
3203                                         reached, NULL, n, decomposeFlag);
3204  if (decomposeFlag) {
3205    for (i = 0; i < n; i++) {
3206      mdd_free(constraint[i]);
3207    }
3208  } else {
3209    for (i = 0; i < n; i++) {
3210      mdd_free(reached[i]);
3211      mdd_free(constraint[i]);
3212    }
3213  }
3214
3215  FREE(reached);
3216  FREE(constraint);
3217  FREE(newConstraint);
3218  FREE(subFsm);
3219  FREE(newReached);
3220  array_free(toCareSetArray);
3221
3222  return(reachedArray);
3223}
3224
3225
3226/**Function********************************************************************
3227
3228  Synopsis    [Computes an upperbound of an FSM by TFBF.]
3229
3230  Description [Computes an upperbound of an FSM by TFBF. It first
3231  sets all constraints to initial states, then does one image
3232  computation, then updates constraints with the results of image
3233  computations. This is iteratively done until it gets converged.
3234  Refer the description of ArdcMbmTraversal(MBM).]
3235
3236  SideEffects []
3237
3238  SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTmbmTraversal
3239  ArdcSimpleTraversal]
3240
3241******************************************************************************/
3242static array_t *
3243ArdcTfbfTraversal(Fsm_Fsm_t *fsm, int nvars,
3244                  array_t *subFsmArray, array_t *fanInsIndexArray,
3245                  mdd_t ***subReached, mdd_t ***subTo,
3246                  int incrementalFlag, int verbosityLevel,
3247                  int printStep, int depthValue, int shellFlag,
3248                  int reorderFlag, int reorderThreshold,
3249                  Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options)
3250{
3251  mdd_manager           *mddManager = NIL(mdd_manager);
3252  int                   i, j, n = array_n(subFsmArray);
3253  mdd_t                 **reached, **constraint, **newConstraint;
3254  mdd_t                 **to, **old_to;
3255  int                   converged = 0;
3256  Fsm_Fsm_t             **subFsm;
3257  array_t               *pi_to;
3258  mdd_t                 *tmp;
3259  array_t               *fans;
3260  mdd_t                 *initialStates;
3261  int                   iteration = 0;
3262  mdd_t                 **initial = NIL(mdd_t *);
3263  array_t               *reachedArray = array_alloc(mdd_t *, 0);
3264  array_t               *faninConstrainArray;
3265  Img_ImageInfo_t       *imageInfo = NIL(Img_ImageInfo_t);
3266  int                   dynStatus;
3267  bdd_reorder_type_t    dynMethod;
3268  mdd_t                 *toCareSet;
3269  array_t               *toCareSetArray = array_alloc(mdd_t *, 0);
3270  int                   depth = 0;
3271  boolean               tmpReorderPtrFlag;
3272  long                  tImgComps = 0;
3273  long                  tConstrainOps = 0;
3274  long                  initialTime = 0, finalTime;
3275  int                   maxIteration = options->maxIteration;
3276  int                   constrainTarget = options->constrainTarget;
3277  boolean               decomposeFlag = options->decomposeFlag;
3278  int                   abstractPseudoInput = options->abstractPseudoInput;
3279  Img_MinimizeType      constrainMethod = options->constrainMethod;
3280  boolean               projectedInitialFlag = options->projectedInitialFlag;
3281  int                   ardcVerbosity = options->verbosity;
3282  boolean               constrainReorderFlag = options->constrainReorderFlag;
3283  boolean               reorderPtrFlag = options->reorderPtrFlag;
3284  int                   faninConstrainMode = options->faninConstrainMode;
3285
3286  Img_ResetNumberOfImageComputation(Img_Forward_c);
3287
3288  reached = ALLOC(mdd_t *, n);
3289  constraint = ALLOC(mdd_t *, n);
3290  newConstraint = ALLOC(mdd_t *, n);
3291  subFsm = ALLOC(Fsm_Fsm_t *, n);
3292  pi_to = array_alloc(mdd_t *, 0);
3293  to = ALLOC(mdd_t *, n);
3294  array_insert_last(mdd_t **, pi_to, to);
3295
3296  mddManager = Fsm_FsmReadMddManager(fsm);
3297  for (i = 0; i < n; i++) {
3298    subFsm[i] = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
3299    initialStates = Fsm_FsmComputeInitialStates(subFsm[i]);
3300    reached[i] = initialStates;
3301    constraint[i] = mdd_dup(initialStates);
3302    to[i] = mdd_zero(mddManager);
3303
3304    if (printStep && ((depth % printStep) == 0)) {
3305      if (ardcVerbosity > 1)
3306        fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i);
3307      (void)fprintf(vis_stdout,
3308                    "BFS step = %d\t|states| = %8g\tBdd size = %8ld\n", depth,
3309                    mdd_count_onset(mddManager, reached[i],
3310                                    subFsm[i]->fsmData.presentStateVars),
3311                    (long)mdd_size(reached[i]));
3312    }
3313  }
3314
3315  if (constrainTarget == Fsm_Ardc_Constrain_Initial_c ||
3316      constrainTarget == Fsm_Ardc_Constrain_Both_c) {
3317    initial = ALLOC(mdd_t *, n);
3318    for (i = 0; i < n; i++)
3319      initial[i] = Fsm_FsmComputeInitialStates(subFsm[i]);
3320  }
3321
3322  converged = 0;
3323  do {
3324    depth++;
3325    to = ALLOC(mdd_t *, n);
3326    for (i = 0; i < n; i++) {
3327      if (ardcVerbosity > 1)
3328        fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i);
3329      faninConstrainArray = array_alloc(mdd_t *, 0);
3330      fans = array_fetch(array_t *, fanInsIndexArray, i);
3331      ComputeFaninConstrainArray(faninConstrainArray, constraint,
3332                                 i, fans, decomposeFlag, faninConstrainMode);
3333      dynStatus = bdd_reordering_status(mddManager, &dynMethod);
3334      if (dynStatus != 0 && constrainReorderFlag == 0)
3335        bdd_dynamic_reordering_disable(mddManager);
3336      imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm[i], 0, 1);
3337      if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) {
3338        int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
3339        if (ardcVerbosity > 2)
3340          Img_SetPrintMinimizeStatus(imageInfo, 2);
3341        else if (ardcVerbosity > 0)
3342          Img_SetPrintMinimizeStatus(imageInfo, 1);
3343        else
3344          Img_SetPrintMinimizeStatus(imageInfo, 0);
3345        if (reorderPtrFlag &&
3346            abstractPseudoInput != Fsm_Ardc_Abst_Ppi_Before_Image_c) {
3347          tmpReorderPtrFlag = 1;
3348        } else
3349          tmpReorderPtrFlag = 0;
3350        if (ardcVerbosity > 0)
3351          initialTime = util_cpu_time();
3352        MinimizeTransitionRelationWithFaninConstraint(imageInfo,
3353                faninConstrainArray, constrainMethod, tmpReorderPtrFlag,
3354                TRUE);
3355        if (ardcVerbosity > 0) {
3356          finalTime = util_cpu_time();
3357          tConstrainOps += finalTime - initialTime;
3358        }
3359        Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
3360      }
3361      if (constrainTarget != Fsm_Ardc_Constrain_Tr_c) {
3362        ComputeConstrainedInitialStates(subFsm[i], faninConstrainArray,
3363                                        constrainMethod);
3364      }
3365      mdd_array_free(faninConstrainArray);
3366      if (dynStatus != 0 && constrainReorderFlag == 0) {
3367        bdd_dynamic_reordering(mddManager, dynMethod,
3368                               BDD_REORDER_VERBOSITY_DEFAULT);
3369      }
3370      if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
3371        int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
3372        if (ardcVerbosity > 2)
3373          Img_SetPrintMinimizeStatus(imageInfo, 2);
3374        else if (ardcVerbosity > 0)
3375          Img_SetPrintMinimizeStatus(imageInfo, 1);
3376        else
3377          Img_SetPrintMinimizeStatus(imageInfo, 0);
3378        Img_AbstractTransitionRelation(imageInfo,
3379                       subFsm[i]->fsmData.pseudoInputBddVars,
3380                       subFsm[i]->fsmData.pseudoInputCube, Img_Forward_c);
3381        if (reorderPtrFlag)
3382          Img_ReorderPartitionedTransitionRelation(imageInfo, Img_Forward_c);
3383        Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
3384      }
3385      toCareSet = mdd_not(reached[i]);
3386      array_insert(mdd_t *, toCareSetArray, 0, toCareSet);
3387      if (ardcVerbosity > 0)
3388        initialTime = util_cpu_time();
3389      to[i] = Fsm_ArdcComputeImage(subFsm[i], constraint[i],
3390                                   constraint[i], toCareSetArray);
3391      if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
3392          Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
3393        Img_TfmFlushCache(imageInfo, FALSE);
3394      }
3395      if (ardcVerbosity > 0) {
3396        finalTime = util_cpu_time();
3397        tImgComps += finalTime - initialTime;
3398      }
3399      mdd_free(toCareSet);
3400      if (constrainTarget != Fsm_Ardc_Constrain_Initial_c)
3401        Img_RestoreTransitionRelation(imageInfo, Img_Forward_c);
3402
3403      tmp = reached[i];
3404      reached[i] = mdd_or(reached[i], to[i], 1, 1);
3405      mdd_free(tmp);
3406      if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_After_Image_c) {
3407        tmp = reached[i];
3408        reached[i] = QuantifyVariables(reached[i],
3409                                subFsm[i]->fsmData.pseudoInputBddVars,
3410                                subFsm[i]->fsmData.pseudoInputCube);
3411        mdd_free(tmp);
3412      }
3413      newConstraint[i] = mdd_dup(to[i]);
3414
3415      if (printStep && ((depth % printStep) == 0)) {
3416        (void)fprintf(vis_stdout,
3417                      "BFS step = %d\t|states| = %8g\tBdd size = %8ld\n",
3418                      depth, mdd_count_onset(mddManager, reached[i],
3419                                     subFsm[i]->fsmData.presentStateVars),
3420                      (long)mdd_size(reached[i]));
3421      }
3422    }
3423    for (i = 0; i < array_n(pi_to); i++) {
3424      old_to = array_fetch(mdd_t **, pi_to, i);
3425      for (j = 0; j < n; j++) {
3426        if (!mdd_equal(old_to[j], to[j]))
3427          break;
3428      }
3429      if (j == n)
3430        break;
3431    }
3432    if (i == array_n(pi_to))
3433      converged = 0;
3434    else {
3435      converged = 1;
3436      if (ardcVerbosity > 0) {
3437        fprintf(vis_stdout,
3438                "** ardc info : TFBF converged at iteration %d(=%d).\n",
3439                iteration + 1, i);
3440      }
3441    }
3442    iteration++;
3443    if (ardcVerbosity > 0) {
3444      boolean   supportCheckFlag = FALSE;
3445
3446      if (projectedInitialFlag ||
3447          abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
3448        supportCheckFlag = TRUE;
3449      }
3450      PrintCurrentReachedStates(mddManager, subFsm, reached,
3451                                Fsm_Ardc_Traversal_Tfbf_c,
3452                                n, iteration, nvars, ardcVerbosity,
3453                                supportCheckFlag);
3454    }
3455
3456    /* update constraints */
3457    for (i = 0; i < n; i++) {
3458      mdd_free(constraint[i]);
3459      constraint[i] = newConstraint[i];
3460      newConstraint[i] = NIL(mdd_t);
3461    }
3462
3463    if (converged || iteration == maxIteration) {
3464      if (subTo)
3465        *subTo = to;
3466      else {
3467        for (i = 0; i < n; i++)
3468          mdd_free(to[i]);
3469        FREE(to);
3470      }
3471      break;
3472    }
3473    array_insert_last(mdd_t **, pi_to, to);
3474  } while (!converged);
3475  if (ardcVerbosity > 0) {
3476    fprintf(vis_stdout, "TFBF : total iteration %d\n", iteration);
3477    fprintf(vis_stdout, "%d image computations, %d constrain operations\n",
3478        Img_GetNumberOfImageComputation(Img_Forward_c), n * iteration);
3479    fprintf(vis_stdout,
3480        "image computation time = %g, constrain operation time = %g\n",
3481        (double)tImgComps / 1000.0, (double)tConstrainOps / 1000.0);
3482  }
3483
3484  if (constrainTarget == Fsm_Ardc_Constrain_Initial_c ||
3485      constrainTarget == Fsm_Ardc_Constrain_Both_c) {
3486    for (i = 0; i < n; i++) {
3487      mdd_free(subFsm[i]->reachabilityInfo.initialStates);
3488      subFsm[i]->reachabilityInfo.initialStates = initial[i];
3489    }
3490    FREE(initial);
3491  }
3492
3493  if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_At_End_c) {
3494    for (i = 0; i < n; i++) {
3495      tmp = reached[i];
3496      reached[i] = QuantifyVariables(reached[i],
3497                                subFsm[i]->fsmData.pseudoInputBddVars,
3498                                subFsm[i]->fsmData.pseudoInputCube);
3499      mdd_free(tmp);
3500    }
3501  }
3502
3503  /* sets the status of current overapproximate reached states */
3504  if (converged)
3505    FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Converged_c);
3506  else
3507    FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_NotConverged_c);
3508
3509  ComputeApproximateReachableStatesArray(mddManager, reachedArray,
3510                                         reached, subReached, n, decomposeFlag);
3511  if (decomposeFlag) {
3512    for (i = 0; i < n; i++) {
3513      mdd_free(constraint[i]);
3514    }
3515  } else {
3516    for (i = 0; i < n; i++) {
3517      if (subReached == NULL)
3518        mdd_free(reached[i]);
3519      mdd_free(constraint[i]);
3520    }
3521  }
3522
3523  if (subReached)
3524    *subReached = reached;
3525  else
3526    FREE(reached);
3527  FREE(constraint);
3528  FREE(newConstraint);
3529  FREE(subFsm);
3530  for (i = 0; i < array_n(pi_to); i++) {
3531    to = array_fetch(mdd_t **, pi_to, i);
3532    for (j = 0; j < n; j++)
3533      mdd_free(to[j]);
3534    FREE(to);
3535  }
3536  array_free(pi_to);
3537  array_free(toCareSetArray);
3538
3539  return(reachedArray);
3540}
3541
3542
3543/**Function********************************************************************
3544
3545  Synopsis    [Computes an upperbound of an FSM by TMBM.]
3546
3547  Description [Computes an upperbound of an FSM by TMBM. TMBM is a
3548  combination of TFBF and MBM. It first calls TFBF with max iteration
3549  number(given by ardc_max_iteration set option). Then if the reached
3550  states are not converged yet, it calls MBM by using current reached
3551  states as initial states.]
3552
3553  SideEffects []
3554
3555  SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal
3556  ArdcSimpleTraversal]
3557
3558******************************************************************************/
3559static array_t *
3560ArdcTmbmTraversal(
3561  Fsm_Fsm_t *fsm,
3562  int nvars,
3563  array_t *subFsmArray,
3564  array_t *fanInsIndexArray,
3565  array_t *fanOutsIndexArray,
3566  int incrementalFlag,
3567  int verbosityLevel,
3568  int printStep,
3569  int depthValue,
3570  int shellFlag,
3571  int reorderFlag,
3572  int reorderThreshold,
3573  Fsm_RchType_t approxFlag,
3574  Fsm_ArdcOptions_t *options,
3575  boolean lfpFlag)
3576{
3577  mdd_manager   *mddManager;
3578  int           i, n = array_n(subFsmArray);
3579  mdd_t         **reached, **tfbf_reached;
3580  mdd_t         **to, **initial;
3581  Fsm_Fsm_t     *subFsm = NIL(Fsm_Fsm_t);
3582  mdd_t         *tmp;
3583  array_t       *reachedArray;
3584  int           saveMaxIteration;
3585
3586  saveMaxIteration = options->maxIteration;
3587  if (options->maxIteration == 0)
3588    options->maxIteration = 10; /* default */
3589
3590  /* Try TFBF for the presecribed number of steps. */
3591  reachedArray = ArdcTfbfTraversal(fsm, nvars, subFsmArray, fanInsIndexArray,
3592                                   &tfbf_reached, &to,
3593                                   incrementalFlag, verbosityLevel, printStep,
3594                                   depthValue, shellFlag, reorderFlag,
3595                                   reorderThreshold, approxFlag, options);
3596
3597  /* If TFBF converged in the allotted number of iterations, clean up and
3598   * return. */
3599  if (FsmReadReachabilityOverApproxComputationStatus(fsm) >=
3600      Fsm_Ardc_Converged_c) {
3601    for (i = 0; i < n; i++) {
3602      mdd_free(tfbf_reached[i]);
3603      mdd_free(to[i]);
3604    }
3605    FREE(tfbf_reached);
3606    FREE(to);
3607    return(reachedArray);
3608  }
3609
3610  mdd_array_free(reachedArray);
3611
3612  /* Save the initial states of each submachine in "initial"; thenset it
3613   * to the "to" states returned by TFBF. */
3614  initial = ALLOC(mdd_t *, n);
3615  for (i = 0; i < n; i++) {
3616    subFsm = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
3617    initial[i] = subFsm->reachabilityInfo.initialStates;
3618    subFsm->reachabilityInfo.initialStates = mdd_dup(to[i]);
3619  }
3620
3621  /* Apply either MBM or LMBM starting from the "to" states returned by
3622   * TFBF. */
3623  options->maxIteration = 0;
3624  reachedArray = ArdcMbmTraversal(fsm, nvars, subFsmArray,
3625                          fanInsIndexArray, fanOutsIndexArray, &reached,
3626                          incrementalFlag, verbosityLevel, printStep,
3627                          depthValue, shellFlag, reorderFlag, reorderThreshold,
3628                          approxFlag, options, lfpFlag);
3629  options->maxIteration = saveMaxIteration;
3630
3631  mdd_array_free(reachedArray);
3632
3633  /* Combine the reachability results of TFBF and (L)MBM and restore
3634   * the initial states of the submachines. */
3635  for (i = 0; i < n; i++) {
3636    tmp = reached[i];
3637    reached[i] = mdd_or(tfbf_reached[i], reached[i], 1, 1);
3638    mdd_free(tmp);
3639    subFsm = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
3640    mdd_free(subFsm->reachabilityInfo.initialStates);
3641    subFsm->reachabilityInfo.initialStates = initial[i];
3642  }
3643
3644  /* Build the array of reachable states in either monolithic or decomposed
3645   * form depending on the value of decomposeFlag. */
3646  reachedArray = array_alloc(mdd_t *, 0);
3647  mddManager = Fsm_FsmReadMddManager(subFsm);
3648  ComputeApproximateReachableStatesArray(mddManager, reachedArray,
3649                                         reached, NULL, n,
3650                                         options->decomposeFlag);
3651  if (!options->decomposeFlag) {
3652    for (i = 0; i < n; i++)
3653      mdd_free(reached[i]);
3654  }
3655
3656  /* Clean up. */
3657  for (i = 0; i < n; i++) {
3658    mdd_free(tfbf_reached[i]);
3659    mdd_free(to[i]);
3660  }
3661
3662  FREE(reached);
3663  FREE(tfbf_reached);
3664  FREE(to);
3665  FREE(initial);
3666
3667  return(reachedArray);
3668}
3669
3670
3671/**Function********************************************************************
3672
3673  Synopsis    [Computes a very rough upperbound in short time.]
3674
3675  Description [Computes a very rough upperbound in short time. It is very
3676  simplified version of MBM, no iteration and no constrain operation.]
3677
3678  SideEffects []
3679
3680  SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal
3681  ArdcTmbmTraversal]
3682
3683******************************************************************************/
3684static array_t *
3685ArdcSimpleTraversal(Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray,
3686                    int incrementalFlag, int verbosityLevel,
3687                    int printStep, int depthValue, int shellFlag,
3688                    int reorderFlag, int reorderThreshold,
3689                    Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options,
3690                    int setFlag)
3691{
3692  mdd_manager           *mddManager;
3693  int                   i, n = array_n(subFsmArray);
3694  mdd_t                 **reached;
3695  Fsm_Fsm_t             **subFsm;
3696  mdd_t                 *tmp;
3697  array_t               *reachedArray = array_alloc(mdd_t *, 0);
3698  Img_ImageInfo_t       *imageInfo = NIL(Img_ImageInfo_t);
3699  boolean               decomposeFlag = options->decomposeFlag;
3700  int                   abstractPseudoInput = options->abstractPseudoInput;
3701  boolean               projectedInitialFlag = options->projectedInitialFlag;
3702  int                   ardcVerbosity = options->verbosity;
3703
3704  reached = ALLOC(mdd_t *, n);
3705  subFsm = ALLOC(Fsm_Fsm_t *, n);
3706
3707  for (i = 0; i < n; i++)
3708    subFsm[i] = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
3709
3710  mddManager = Fsm_FsmReadMddManager(subFsm[0]);
3711  for (i = 0; i < n; i++) {
3712    if (printStep && ardcVerbosity > 1)
3713      fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i);
3714    if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
3715      int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
3716      if (ardcVerbosity > 2)
3717        Img_SetPrintMinimizeStatus(imageInfo, 2);
3718      else if (ardcVerbosity > 0)
3719        Img_SetPrintMinimizeStatus(imageInfo, 1);
3720      else
3721        Img_SetPrintMinimizeStatus(imageInfo, 0);
3722      imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm[i], 0, 1);
3723      Img_AbstractTransitionRelation(imageInfo,
3724                                     subFsm[i]->fsmData.pseudoInputBddVars,
3725                                     subFsm[i]->fsmData.pseudoInputCube,
3726                                     Img_Forward_c);
3727      Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
3728    }
3729    reached[i] = Fsm_FsmComputeReachableStates(subFsm[i],
3730                       incrementalFlag, verbosityLevel, printStep, depthValue,
3731                       shellFlag, reorderFlag, reorderThreshold,
3732                       approxFlag, 0, 0, NIL(array_t), FALSE, NIL(array_t));
3733    if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
3734        Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
3735      Img_TfmFlushCache(imageInfo, FALSE);
3736    }
3737    if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_After_Image_c) {
3738      if (n > 1) {
3739        tmp = reached[i];
3740        reached[i] = QuantifyVariables(reached[i],
3741                                subFsm[i]->fsmData.pseudoInputBddVars,
3742                                subFsm[i]->fsmData.pseudoInputCube);
3743        mdd_free(tmp);
3744      }
3745    }
3746  }
3747
3748  if (ardcVerbosity > 0) {
3749    boolean     supportCheckFlag = FALSE;
3750
3751    if (projectedInitialFlag ||
3752        abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
3753      supportCheckFlag = TRUE;
3754    }
3755    PrintCurrentReachedStates(mddManager, subFsm, reached,
3756                                Fsm_Ardc_Traversal_Simple_c,
3757                                n, 0, nvars, ardcVerbosity,
3758                                supportCheckFlag);
3759  }
3760
3761  if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_At_End_c) {
3762    for (i = 0; i < n; i++) {
3763      tmp = reached[i];
3764      reached[i] = QuantifyVariables(reached[i],
3765                                subFsm[i]->fsmData.pseudoInputBddVars,
3766                                subFsm[i]->fsmData.pseudoInputCube);
3767      mdd_free(tmp);
3768    }
3769  }
3770
3771  /* sets the status of current overapproximate reached states */
3772  if (setFlag)
3773    FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Converged_c);
3774
3775  ComputeApproximateReachableStatesArray(mddManager, reachedArray,
3776                                         reached, NULL, n, decomposeFlag);
3777
3778  FREE(reached);
3779  FREE(subFsm);
3780
3781  return(reachedArray);
3782}
3783
3784
3785/**Function********************************************************************
3786
3787  Synopsis    [Computes fanin constraint with the reached states of
3788  fanin submachines.]
3789
3790  Description [Computes fanin constraint with the reached states of
3791  fanin submachines.]
3792
3793  SideEffects []
3794
3795  SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal]
3796
3797******************************************************************************/
3798static void
3799ComputeFaninConstrainArray(array_t *faninConstrainArray, mdd_t **constraint,
3800                           int current, array_t *fans,
3801                           int decomposeFlag, int faninConstrainMode)
3802{
3803  mdd_t *faninConstrain, *tmp;
3804  int   i, fanin;
3805
3806  if (decomposeFlag) {
3807    if (faninConstrainMode == 1) {
3808      array_insert_last(mdd_t *, faninConstrainArray,
3809                        mdd_dup(constraint[current]));
3810    }
3811    arrayForEachItem(int, fans, i, fanin) {
3812      array_insert_last(mdd_t *, faninConstrainArray,
3813                          mdd_dup(constraint[fanin]));
3814    }
3815  } else {
3816    if (faninConstrainMode == 1)
3817      faninConstrain = mdd_dup(constraint[current]);
3818    else
3819      faninConstrain = NIL(mdd_t);
3820    arrayForEachItem(int, fans, i, fanin) {
3821      if (faninConstrain) {
3822        tmp = faninConstrain;
3823        faninConstrain = mdd_and(faninConstrain, constraint[fanin], 1, 1);
3824        mdd_free(tmp);
3825      } else
3826        faninConstrain = mdd_dup(constraint[fanin]);
3827    }
3828    array_insert_last(mdd_t *, faninConstrainArray, faninConstrain);
3829  }
3830}
3831
3832
3833/**Function********************************************************************
3834
3835  Synopsis    [Minimizes transition relation with fanin constraint.]
3836
3837  Description [Minimizes transition relation with fanin constraint.]
3838
3839  SideEffects []
3840
3841  SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal]
3842
3843******************************************************************************/
3844static void
3845MinimizeTransitionRelationWithFaninConstraint(Img_ImageInfo_t *imageInfo,
3846                                              array_t *faninConstrainArray,
3847                                              Img_MinimizeType constrainMethod,
3848                                              boolean reorderPtrFlag,
3849                                              boolean duplicate)
3850{
3851  if (duplicate) {
3852    Img_DupTransitionRelation(imageInfo, Img_Forward_c);
3853    Img_ResetTrMinimizedFlag(imageInfo, Img_Forward_c);
3854  }
3855  Img_MinimizeTransitionRelation(imageInfo, faninConstrainArray,
3856                                 constrainMethod, Img_Forward_c,
3857                                 reorderPtrFlag);
3858}
3859
3860
3861/**Function********************************************************************
3862
3863  Synopsis    [Computes constrained initial states.]
3864
3865  Description [Computes constrained initial states.]
3866
3867  SideEffects [This function just update a new constrained initial
3868  states, so caller should take care of this.]
3869
3870  SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal]
3871
3872******************************************************************************/
3873static void
3874ComputeConstrainedInitialStates(Fsm_Fsm_t *subFsm,
3875                                array_t *faninConstrainArray,
3876                                Img_MinimizeType constrainMethod)
3877{
3878  int   i;
3879  mdd_t *faninConstrain, *tmp, *constrainedInitial;
3880
3881  constrainedInitial = subFsm->reachabilityInfo.initialStates;
3882  for (i = 0; i < array_n(faninConstrainArray); i++) {
3883    faninConstrain = array_fetch(mdd_t *, faninConstrainArray, i);
3884    tmp = constrainedInitial;
3885    constrainedInitial = Img_MinimizeImage(constrainedInitial,
3886                                           faninConstrain, constrainMethod,
3887                                           TRUE);
3888    mdd_free(tmp);
3889  }
3890  subFsm->reachabilityInfo.initialStates = constrainedInitial;
3891}
3892
3893
3894/**Function********************************************************************
3895
3896  Synopsis    [Makes an array of approximate reachable states.]
3897
3898  Description [Makes an array of approximate reachable states.]
3899
3900  SideEffects []
3901
3902  SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal]
3903
3904******************************************************************************/
3905static void
3906ComputeApproximateReachableStatesArray(mdd_manager *mddManager,
3907                                       array_t *reachedArray,
3908                                       mdd_t **reached,
3909                                       mdd_t ***subReached,
3910                                       int nSubFsms,
3911                                       int decomposeFlag)
3912{
3913  int i;
3914
3915  if (decomposeFlag) {
3916    for (i = 0; i < nSubFsms; i++) {
3917      if (subReached)
3918        array_insert_last(mdd_t *, reachedArray, mdd_dup(reached[i]));
3919      else
3920        array_insert_last(mdd_t *, reachedArray, reached[i]);
3921    }
3922  } else {
3923    mdd_t *reachedSet = mdd_one(mddManager);
3924    for (i = 0; i < nSubFsms; i++) {
3925      mdd_t *tmp = reachedSet;
3926      reachedSet = mdd_and(reachedSet, reached[i], 1, 1);
3927      mdd_free(tmp);
3928    }
3929    array_insert_last(mdd_t *, reachedArray, reachedSet);
3930  }
3931}
3932
3933
3934/**Function********************************************************************
3935
3936  Synopsis    [Copy exact reached states to overapproximate.]
3937
3938  Description [Copy exact reached states to overapproximate.]
3939
3940  SideEffects []
3941
3942  SeeAlso []
3943
3944******************************************************************************/
3945static array_t *
3946ArdcCopyOverApproxReachableStatesFromExact(Fsm_Fsm_t *fsm)
3947{
3948  array_t       *reachableStatesArray;
3949
3950  if (Fsm_FsmReadReachableStates(fsm) == NIL(mdd_t))
3951    return(NIL(array_t));
3952
3953  reachableStatesArray = array_alloc(mdd_t *, 0);
3954  array_insert_last(mdd_t *, reachableStatesArray,
3955                    mdd_dup(Fsm_FsmReadReachableStates(fsm)));
3956  FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Exact_c);
3957  fsm->reachabilityInfo.apprReachableStates = reachableStatesArray;
3958  fsm->reachabilityInfo.subPsVars = array_alloc(array_t *, 0);
3959  array_insert_last(array_t *, fsm->reachabilityInfo.subPsVars,
3960                    array_dup(fsm->fsmData.presentStateVars));
3961  return(reachableStatesArray);
3962}
3963
3964
3965/**Function********************************************************************
3966
3967  Synopsis    [Prints current approximate reached states.]
3968
3969  Description [Prints current approximate reached states.]
3970
3971  SideEffects []
3972
3973  SeeAlso []
3974
3975******************************************************************************/
3976static void
3977PrintCurrentReachedStates(mdd_manager *mddManager, Fsm_Fsm_t **subFsm,
3978                          mdd_t **reached, Fsm_Ardc_TraversalType_t method,
3979                          int nSubFsms, int iteration, int nvars,
3980                          int ardcVerbosity, boolean supportCheckFlag)
3981{
3982  int           i;
3983  char          string[24];
3984  double        tmpReached;
3985
3986  if (nvars <= EPD_MAX_BIN) {
3987    double      numReached = 1.0, tmpReached;
3988
3989    for (i = 0; i < nSubFsms; i++) {
3990      tmpReached = mdd_count_onset(mddManager, reached[i],
3991                                   subFsm[i]->fsmData.presentStateVars);
3992      if (ardcVerbosity > 1) {
3993        if (ardcVerbosity > 2 && supportCheckFlag) {
3994          assert(mdd_check_support(mddManager, reached[i],
3995                                   subFsm[i]->fsmData.presentStateVars));
3996        }
3997        fprintf(vis_stdout, "# of reached for subFsm[%d] = %g\n",
3998                i, tmpReached);
3999      }
4000      numReached *= tmpReached;
4001    }
4002    sprintf(string, "%g", numReached);
4003  } else {
4004    EpDouble    epd;
4005
4006    EpdConvert((double)1.0, &epd);
4007
4008    for (i = 0; i < nSubFsms; i++) {
4009      tmpReached = mdd_count_onset(mddManager, reached[i],
4010                                   subFsm[i]->fsmData.presentStateVars);
4011      if (ardcVerbosity > 1) {
4012        if (ardcVerbosity > 2 && supportCheckFlag) {
4013          assert(mdd_check_support(mddManager, reached[i],
4014                                   subFsm[i]->fsmData.presentStateVars));
4015        }
4016        fprintf(vis_stdout, "# of reached for subFsm[%d] = %g\n",
4017                i, tmpReached);
4018      }
4019      EpdMultiply(&epd, tmpReached);
4020    }
4021    EpdGetString(&epd, string);
4022  }
4023
4024  switch (method) {
4025  case Fsm_Ardc_Traversal_Mbm_c :
4026    fprintf(vis_stdout, "MBM : iteration %d, # of reached = %s\n",
4027            iteration, string);
4028    break;
4029  case Fsm_Ardc_Traversal_Rfbf_c :
4030    fprintf(vis_stdout, "RFBF : iteration %d, # of reached = %s\n",
4031            iteration, string);
4032    break;
4033  case Fsm_Ardc_Traversal_Tfbf_c :
4034    fprintf(vis_stdout, "TFBF : iteration %d, # of reached = %s\n",
4035            iteration, string);
4036    break;
4037  case Fsm_Ardc_Traversal_Tmbm_c :
4038    fprintf(vis_stdout, "TMBM : iteration %d, # of reached = %s\n",
4039            iteration, string);
4040    break;
4041  case Fsm_Ardc_Traversal_Lmbm_c :
4042    fprintf(vis_stdout, "LMBM : iteration %d, # of reached = %s\n",
4043            iteration, string);
4044    break;
4045  case Fsm_Ardc_Traversal_Tlmbm_c :
4046    fprintf(vis_stdout, "TLMBM : iteration %d, # of reached = %s\n",
4047            iteration, string);
4048    break;
4049  case Fsm_Ardc_Traversal_Simple_c :
4050    fprintf(vis_stdout, "SIMPLE : # of reached = %s\n", string);
4051    break;
4052  default :
4053    break;
4054  }
4055}
4056
4057
4058/**Function********************************************************************
4059
4060  Synopsis    [Prints bdd variable names and levels of mddIdArr, and minterms.]
4061
4062  Description [Prints bdd variable names and levels of mddIdArr, and minterms.]
4063
4064  SideEffects []
4065
4066  SeeAlso []
4067
4068******************************************************************************/
4069static void
4070PrintBddWithName(Fsm_Fsm_t *fsm, array_t *mddIdArr, mdd_t *node)
4071{
4072  int           i, j, size;
4073  mdd_manager   *mddManager;
4074  array_t       *mvarArray;
4075  mvar_type     mv;
4076  int           bddId, mddId, varLevel;
4077  bdd_t         *varBdd;
4078
4079  if (!node)
4080    return;
4081
4082  mddManager = Fsm_FsmReadMddManager(fsm);
4083  if (!mddIdArr)
4084    mddIdArr = mdd_get_support(mddManager, node);
4085  mvarArray = mdd_ret_mvar_list(mddManager);
4086
4087  size = array_n(mddIdArr);
4088  for (i = 0; i < size; i++) {
4089    mddId = array_fetch(int, mddIdArr, i);
4090    mv = array_fetch(mvar_type, mvarArray, mddId);
4091    for (j = 0; j < mv.encode_length; j++) {
4092      bddId = mdd_ret_bvar_id(&mv, j);
4093      varBdd = bdd_get_variable(mddManager, bddId);
4094      varLevel = bdd_top_var_level(mddManager, varBdd);
4095      if (mv.encode_length == 1)
4096        fprintf(vis_stdout, "%s %d\n", mv.name, varLevel);
4097      else
4098        fprintf(vis_stdout, "%s[%d] %d\n", mv.name, j, varLevel);
4099      bdd_free(varBdd);
4100    }
4101  }
4102  bdd_print_minterm(node);
4103}
4104
4105
4106/**Function********************************************************************
4107
4108  Synopsis    [Reads grouping information.]
4109
4110  Description [Reads grouping information.]
4111
4112  SideEffects []
4113
4114  SeeAlso     []
4115
4116******************************************************************************/
4117static void
4118ArdcReadGroup(Ntk_Network_t *network, FILE *groupFile,
4119        array_t *latchNameArray, array_t *groupIndexArray)
4120{
4121  char          line[ARDC_MAX_LINE_LEN];
4122  char          *latchName, *name, *group;
4123  int           groupIndex = 0;
4124
4125  while (fgets(line, ARDC_MAX_LINE_LEN, groupFile)) {
4126    if (strlen(line) == 0)
4127      continue;
4128    if (line[0] == '#')
4129      continue;
4130    if (line[strlen(line) - 1] == '\n')
4131      line[strlen(line) - 1] = '\0';
4132    group = strtok(line, " ");
4133    if (strncmp(group, "GROUP[", 6) == 0)
4134      sscanf(group, "GROUP[%d]:", &groupIndex);
4135    else {
4136      latchName = util_strsav(group);
4137      array_insert_last(char *, latchNameArray, latchName);
4138      array_insert_last(int, groupIndexArray, groupIndex);
4139    }
4140    while ((name = strtok(NIL(char), " \t")) != NIL(char)) {
4141      latchName = util_strsav(name);
4142      array_insert_last(char *, latchNameArray, latchName);
4143      array_insert_last(int, groupIndexArray, groupIndex);
4144    }
4145  }
4146}
4147
4148
4149/**Function********************************************************************
4150
4151  Synopsis    [Writes one grouping information.]
4152
4153  Description [Writes one grouping information.]
4154
4155  SideEffects []
4156
4157  SeeAlso     []
4158
4159******************************************************************************/
4160static void
4161ArdcWriteOneGroup(Part_Subsystem_t *partitionSubsystem, FILE *groupFile, int i)
4162{
4163  st_generator  *stGen;
4164  st_table      *vertexNameTable;
4165  char          *latchName;
4166
4167  fprintf(groupFile, "GROUP[%d]:", i);
4168  vertexNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
4169  st_foreach_item(vertexNameTable, stGen, &latchName, NIL(char *)) {
4170    fprintf(groupFile, " %s", latchName);
4171  }
4172  fprintf(groupFile, "\n");
4173}
4174
4175
4176/**Function********************************************************************
4177
4178  Synopsis    [Prints one grouping information.]
4179
4180  Description [Prints one grouping information.]
4181
4182  SideEffects []
4183
4184  SeeAlso     []
4185
4186******************************************************************************/
4187static void
4188ArdcPrintOneGroup(Part_Subsystem_t *partitionSubsystem, int i, int nLatches,
4189                  array_t *fanIns, array_t *fanOuts)
4190{
4191  int           j, k;
4192  st_generator  *stGen;
4193  st_table      *vertexNameTable;
4194  char          *latchName;
4195
4196  fprintf(vis_stdout, "SUB-FSM [%d]\n", i);
4197  fprintf(vis_stdout, "== latches(%d) :", nLatches);
4198  vertexNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
4199  st_foreach_item(vertexNameTable, stGen, &latchName, NIL(char *)) {
4200    fprintf(vis_stdout, " %s", latchName);
4201  }
4202  fprintf(vis_stdout, "\n");
4203  fprintf(vis_stdout, "== fanins(%d) :", array_n(fanIns));
4204  for (j = 0; j < array_n(fanIns); j++) {
4205    k = array_fetch(int, fanIns, j);
4206    fprintf(vis_stdout, " %d", k);
4207  }
4208  fprintf(vis_stdout, "\n");
4209  fprintf(vis_stdout, "== fanouts(%d) :", array_n(fanOuts));
4210  for (j = 0; j < array_n(fanOuts); j++) {
4211    k = array_fetch(int, fanOuts, j);
4212    fprintf(vis_stdout, " %d", k);
4213  }
4214  fprintf(vis_stdout, "\n");
4215}
4216
4217
4218/**Function********************************************************************
4219
4220  Synopsis    [Returns a set integer value related ARDC computation.]
4221
4222  Description [Returns a set integer value related ARDC computation.]
4223
4224  SideEffects []
4225
4226  SeeAlso     []
4227
4228******************************************************************************/
4229static int
4230GetArdcSetIntValue(char *string, int l, int u, int defaultValue)
4231{
4232  char  *flagValue;
4233  int   tmp;
4234  int   value = defaultValue;
4235
4236  flagValue = Cmd_FlagReadByName(string);
4237  if (flagValue != NIL(char)) {
4238    sscanf(flagValue, "%d", &tmp);
4239    if (tmp >= l && (tmp <= u || u == 0))
4240      value = tmp;
4241    else {
4242      fprintf(vis_stderr,
4243        "** ardc error : invalid value %d for %s[%d-%d]. **\n", tmp, string,
4244              l, u);
4245    }
4246  }
4247
4248  return(value);
4249}
4250
4251
4252/**Function********************************************************************
4253
4254  Synopsis    [Returns the number of approximate reachable states of an FSM.]
4255
4256  Description [Returns the number of approximate reachable states of an FSM.]
4257
4258  SideEffects []
4259
4260  SeeAlso     []
4261
4262******************************************************************************/
4263static void
4264ArdcEpdCountOnsetOfOverApproximateReachableStates(Fsm_Fsm_t *fsm, EpDouble *epd)
4265{
4266  mdd_t *reached;
4267  array_t *psVars, *reachedArray;
4268  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
4269  double tmpReached;
4270  int i;
4271
4272  EpdMakeZero(epd, 0);
4273
4274  if (!Fsm_FsmReadCurrentOverApproximateReachableStates(fsm))
4275    return;
4276
4277  EpdConvert((double)1.0, epd);
4278  reachedArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm);
4279  arrayForEachItem(mdd_t *, reachedArray, i, reached) {
4280    psVars = array_fetch(array_t *, fsm->reachabilityInfo.subPsVars, i);
4281    tmpReached = mdd_count_onset(mddManager, reached, psVars);
4282    EpdMultiply(epd, tmpReached);
4283  }
4284}
4285
4286
4287/**Function********************************************************************
4288
4289  Synopsis    [Quantifies out smoothing variables.]
4290
4291  Description [Quantifies out smoothing variables. If the bdd package is CUDD,
4292  it performs with a cube for better efficiency. Otherwise, it uses
4293  conventional  mdd id array. smoothArray should be an array of bdd variables.]
4294
4295  SideEffects []
4296
4297  SeeAlso     []
4298
4299******************************************************************************/
4300static mdd_t *
4301QuantifyVariables(mdd_t *state, array_t *smoothArray, mdd_t *smoothCube)
4302{
4303  if (smoothCube)
4304    return(bdd_smooth_with_cube(state, smoothCube));
4305  else
4306    return(bdd_smooth(state, smoothArray));
4307}
4308
4309
4310/**Function********************************************************************
4311
4312  Synopsis    [Updates event scheduling of submachines for traversal.]
4313
4314  Description [Updates event scheduling of submachines for traversal.]
4315
4316  SideEffects []
4317
4318  SeeAlso     []
4319
4320******************************************************************************/
4321static void
4322UpdateMbmEventSchedule(Fsm_Fsm_t **subFsm, array_t *fanOutIndices,
4323                        int *traverse, int lfpFlag)
4324{
4325  int   i, fanout;
4326
4327  arrayForEachItem(int, fanOutIndices, i, fanout) {
4328    if (lfpFlag) {
4329      if (!subFsm[fanout]->reachabilityInfo.reachableStates ||
4330          !bdd_is_tautology(subFsm[fanout]->reachabilityInfo.reachableStates,
4331                            1)) {
4332        traverse[fanout] = 1;
4333      }
4334    } else
4335      traverse[fanout] = 1;
4336  }
4337}
4338
4339
4340/**Function********************************************************************
4341
4342  Synopsis    [Prints statistics of transition function method.]
4343
4344  Description [Prints statistics of transition function method.]
4345
4346  SideEffects []
4347
4348  SeeAlso     []
4349
4350******************************************************************************/
4351static void
4352PrintTfmStatistics(array_t *subFsmArray)
4353{
4354  int                   i;
4355  Img_ImageInfo_t       *imageInfo;
4356  Fsm_Fsm_t             *subFsm;
4357  double                tInserts, tLookups, tHits, tEntries;
4358  double                inserts, lookups, hits, entries;
4359  int                   nSlots, tSlots, maxChainLength;
4360  float                 avgDepth, tAvgDepth, avgDecomp, tAvgDecomp;
4361  int                   tRecurs, tLeaves, tTurns, tDecomps, minDecomp;
4362  int                   nRecurs, nLeaves, nTurns;
4363  int                   nDecomps, topDecomp, maxDecomp, tMaxDecomp;
4364  int                   maxDepth, tMaxDepth;
4365  int                   flag, globalCache;
4366
4367  tInserts = tLookups = tHits = tEntries = 0.0;
4368  tSlots = 0;
4369  tRecurs = tLeaves = tTurns = tDecomps = 0;
4370  tAvgDepth = tAvgDecomp = 0.0;
4371  tMaxDecomp = tMaxDepth = 0;
4372  minDecomp = 10000000; /* arbitrarily large number */
4373
4374  globalCache = Img_TfmCheckGlobalCache(0);
4375  if (globalCache) {
4376    flag = Img_TfmGetCacheStatistics(NIL(Img_ImageInfo_t), 0, &inserts,
4377                                     &lookups, &hits, &entries, &nSlots,
4378                                     &maxChainLength);
4379    tInserts = inserts;
4380    tLookups = lookups;
4381    tHits = hits;
4382    tEntries = entries;
4383    tSlots = nSlots;
4384  }
4385
4386  for (i = 0; i < array_n(subFsmArray); i++) {
4387    subFsm = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
4388    imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm, 0, 1);
4389
4390    if (!globalCache) {
4391      flag = Img_TfmGetCacheStatistics(imageInfo, 0, &inserts, &lookups, &hits,
4392                                       &entries, &nSlots, &maxChainLength);
4393      if (flag) {
4394        tInserts += inserts;
4395        tLookups += lookups;
4396        tHits += hits;
4397        tEntries += entries;
4398        tSlots += nSlots;
4399      }
4400    }
4401
4402    flag = Img_TfmGetRecursionStatistics(imageInfo, 0, &nRecurs, &nLeaves,
4403                                 &nTurns, &avgDepth, &maxDepth, &nDecomps,
4404                                 &topDecomp, &maxDecomp, &avgDecomp);
4405    if (flag) {
4406      tAvgDepth = (tAvgDepth * (float)tLeaves + avgDepth * (float)nLeaves) /
4407                  (float)(tLeaves + nLeaves);
4408      tRecurs += nRecurs;
4409      tLeaves += nLeaves;
4410      tTurns += nTurns;
4411      tAvgDecomp = (tAvgDecomp * (float)tDecomps +
4412                    avgDecomp * (float)nDecomps) / (float)(tDecomps + nDecomps);
4413      tDecomps += nDecomps;
4414      if (topDecomp < minDecomp)
4415        minDecomp = topDecomp;
4416      if (maxDecomp > tMaxDecomp)
4417        tMaxDecomp = maxDecomp;
4418      if (maxDepth > tMaxDepth)
4419        tMaxDepth = maxDepth;
4420    }
4421  }
4422
4423  if (tInserts != 0.0) {
4424    if (globalCache) {
4425      fprintf(vis_stdout,
4426        "** global cache statistics of transition function **\n");
4427    } else
4428      fprintf(vis_stdout, "** cache statistics of transition function **\n");
4429    fprintf(vis_stdout, "# insertions = %g\n", tInserts);
4430    fprintf(vis_stdout, "# lookups = %g\n", tLookups);
4431    fprintf(vis_stdout, "# hits = %g (%.2f%%)\n", tHits,
4432      tHits / tLookups * 100.0);
4433    fprintf(vis_stdout, "# misses = %g (%.2f%%)\n", tLookups - tHits,
4434      (tLookups - tHits) / tLookups * 100.0);
4435    fprintf(vis_stdout, "# entries = %g\n", tEntries);
4436    if (tSlots > 0) {
4437      fprintf(vis_stdout, "# slots = %d\n", tSlots);
4438      fprintf(vis_stdout, "maxChainLength = %d\n", maxChainLength);
4439    }
4440  }
4441
4442  if (tRecurs != 0) {
4443    fprintf(vis_stdout, "** recursion statistics of transition function **\n");
4444    fprintf(vis_stdout, "# recursions = %d\n", tRecurs);
4445    fprintf(vis_stdout, "# leaves = %d\n", tLeaves);
4446    fprintf(vis_stdout, "# turns = %d\n", tTurns);
4447    fprintf(vis_stdout, "# average recursion depth = %g (max = %d)\n",
4448            tAvgDepth, tMaxDepth);
4449    fprintf(vis_stdout,
4450            "# decompositions = %d (top = %d, max = %d, average = %g)\n",
4451            tDecomps, minDecomp, tMaxDecomp, tAvgDecomp);
4452  }
4453}
Note: See TracBrowser for help on using the repository browser.