source: vis_dev/vis-2.3/src/fsm/fsmReach.c@ 83

Last change on this file since 83 was 15, checked in by cecile, 15 years ago

Vis main file for expermeriments
File size: 80.8 KB
Line 
1/**CFile***********************************************************************
2
3 FileName [fsmReach.c]
4
5 PackageName [fsm]
6
7 Synopsis [Routines to perform reachability on the FSM structure.]
8
9 Author [Rajeev K. Ranjan, In-Ho Moon, Kavita Ravi]
10
11 Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California.
12 All rights reserved.
13
14 Permission is hereby granted, without written agreement and without license
15 or royalty fees, to use, copy, modify, and distribute this software and its
16 documentation for any purpose, provided that the above copyright notice and
17 the following two paragraphs appear in all copies of this software.
18
19 IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
20 DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
21 OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
22 CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23
24 THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
25 INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
26 FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN
27 "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
28 MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
29
30******************************************************************************/
31
32#include "fsmInt.h"
33#include "bdd.h"
34#include "ntm.h"
35#include "img.h"
36#include "sim.h"
37
38static char rcsid[] UNUSED = "$Id: fsmReach.c,v 1.102 2009/04/11 01:40:54 fabio Exp $";
39
40/*---------------------------------------------------------------------------*/
41/* Constant declarations */
42/*---------------------------------------------------------------------------*/
43/* HD constants */
44#define FSM_HD_NONGREEDY 0 /* flag to indicate non-greedy computation at
45 dead-ends */
46#define FSM_HD_GREEDY 1 /* flag to indicate greedy computation at dead-ends */
47#define FSM_HD_LARGE_SIZE 100000 /* size considered large for reached */
48#define FSM_HD_MID_SIZE 50000 /* size considered medium for reached*/
49#define FSM_HD_MINT_GROWTH 0.5 /* factor measuring minterm jump of reached*/
50#define FSM_HD_GROWTH_RATE 0.04 /* Growth rate for reached in measuring slow
51 * growth. */
52#define FSM_MDD_DONT_FREE 0 /* flag to indicate that bdd should not be freed. */
53#define FSM_MDD_FREE 1 /* flag to indicate that bdd should be freed.*/
54#define FSM_HD_NUM_SLOW_GROWTHS 5 /* number of iterations of allowed
55 * slow growth of reached. */
56/*---------------------------------------------------------------------------*/
57/* Structure declarations */
58/*---------------------------------------------------------------------------*/
59
60/**AutomaticStart*************************************************************/
61
62/*---------------------------------------------------------------------------*/
63/* Static function prototypes */
64/*---------------------------------------------------------------------------*/
65
66static int CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t *domainVarMddIdArray, array_t *quantifyVarMddIdArray);
67/*static*/ int ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, array_t *mddIdArray);
68static mdd_t * AddStates(mdd_t *a, mdd_t *b, int freeA, int freeB);
69static void RandomSimulation(int simNVec, Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag, mdd_t *initialStates, mdd_t **reachableStates, mdd_t **fromLowerBound, FsmHdStruct_t *hdInfo);
70static void PrintStatsPerIteration(Fsm_RchType_t approxFlag, int nvars, int depth, FsmHdStruct_t *hdInfo, mdd_manager *mddManager, mdd_t *reachableStates, mdd_t *fromLowerBound, array_t *mintermVarArray);
71static void HdInduceFullDeadEndIfNecessary(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, mdd_t **fromLowerBound, mdd_t **fromUpperBound, mdd_t **reachableStates, mdd_t **image, FsmHdStruct_t *hdInfo, int *depth, int shellFlag, array_t *onionRings, array_t *mintermVarArray, int oldSize, double oldMint, int verbosityLevel);
72static mdd_t * ComputeInitialStates(Fsm_Fsm_t *fsm, int shellFlag, boolean printWarning);
73static int CheckStatesContainedInInvariant(mdd_t *reachableStates, array_t *invarStates);
74static void HdComputeReachabilityParameters(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, mdd_t **reachableStates, mdd_t **fromUpperBound, mdd_t **fromLowerBound, mdd_t **image, FsmHdStruct_t *hdInfo, mdd_t *initialStates, array_t *mintermVarArray, int *depth, int printStep, int shellFlag, array_t *onionRings, int verbosityLevel);
75static int InitializeIncrementalParameters(Fsm_Fsm_t *fsm, Ntk_Network_t *network, array_t **arrayOfRoots, st_table **tableOfLeaves);
76static mdd_t * IncrementalImageCompute(Ntk_Network_t *network, Fsm_Fsm_t *fsm, mdd_manager *mddManager, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet, array_t *arrayOfRoots, st_table *tableOfLeaves, array_t *smoothVarArray, array_t *relationArray, int numLatch);
77static void PrintOnionRings(Fsm_Fsm_t *fsm, int printStep, Fsm_RchType_t approxFlag, int nvars);
78static array_t * GenerateGuidedSearchSequenceArray(array_t *guideArray);
79static void ComputeReachabilityParameters(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, Fsm_RchType_t approxFlag, mdd_t **reachableStates, mdd_t **fromUpperBound, mdd_t **fromLowerBound, mdd_t **image, FsmHdStruct_t *hdInfo, mdd_t *initialStates, array_t *mintermVarArray, int *depth, int printStep, int shellFlag, array_t *onionRings, int verbosityLevel, boolean guidedSearchMode, mdd_t *hint, int *hintDepth, boolean *notConverged);
80
81/**AutomaticEnd***************************************************************/
82
83
84/*---------------------------------------------------------------------------*/
85/* Definition of exported functions */
86/*---------------------------------------------------------------------------*/
87/**Function********************************************************************
88
89 Synopsis [Computes the set of reachable states of an FSM.]
90
91 Description [Computes the set of reachable states of an FSM. If
92 this set has already been computed, then just returns the result of
93 the previous computation. The recomputation is done anyway if onion
94 rings are required and have not been previously computed. The
95 calling application is responsible for freeing the returned MDD in
96 all cases. If verbosityLevel is greater than 1, then information is
97 printed after every k steps of reachability, where k is defined by
98 the -s option in the compute_reach command (the default for k is
99 1). If reorderFlag is set, then dynamic reordering is invoked once
100 when the size of the reachable state set reaches the threshold given
101 by reorderThreshold. This is independent of the
102 dynamic_variable_reordering command. The shell flag indicates that
103 the onion rings of frontier states should be stored. The default
104 does not store the onion rings. The default value for approxFlag is
105 Fsm_Rch_Default_c. See fsm.h for values.
106
107 The procedure offers the following variations of reachability
108 analysis: 1. Exact Reachability analysis by breadth-first search
109 (default). 2. Reachability Analysis (HD) . 3. Reachability Analysis
110 (upper bound by overapproximate FSM traversal). 4 ARDC-accelerated
111 Reachability Analysis. 5. Invariant checking with early termination.
112
113 A lower bound (specified by depthValue) on the reachable states may
114 be obtained by performing a specified number of iterations
115 (depthValue argument). It updates a field in the
116 fsm.reachabilityInfo signalling that the reachable states are an
117 under approximation. The default for the depthValue argument is 0
118 which indicates that reachability analysis computation should
119 proceed to a fixpoint. If a depthValue is specified after the
120 computation of reachable states, the reachable states is returned,
121 else depthValue number of computations are performed. Every non-zero
122 depthValue is interpreted as the number of iterations (image
123 computations) to be performed from the current state (not from the
124 initial state).
125
126 Reachability Analysis (HD) is requested as approxFlag = Fsm_Rch_Hd_c.
127 HD provides an exact set of reachable states with memory efficiency or
128 a lower bound if reachability analysis does not complete.
129 HD Principles: 1. compute image of small BDDs. 2. compute partial
130 image if necessary 3. When no new states are generated (dead-end),
131 compute new states from image of reached in a decomposed form. Allow
132 no partial image. 4. When there is a big jump in the size of
133 reached, compute its entire image. 5. store states that will
134 produce no new successors (interior states)
135
136 The algorithm is implemented as follows
137 from = init; reached = init;
138 while (reached != 1 && from != 0) {
139 Allow partial image;
140 image = Image(from);
141 Check if partial image;
142 from = image - reached;
143 if (!partial image) interior_states_candidate = from;
144 if (from == 0 || slow growth of Reached for 5 iterations) {
145 Dead-end computation(greedy): find new states from image of reached;
146 }
147 if (from != 0 and (reached+from) size has a big jump) {
148 Dead-end computation(non-greedy): find the entire image of reached;
149 }
150 if (from != 0) {
151 Compute dense subset of from with at least 1 new state;
152 if subset contains from (i.e., all new states)
153 interior states += interior states candidate;
154 reached = reached + from/subset;
155 }
156 }
157
158 Legend: fromLowerBound = from; initialStates = init;
159 reachableStates = reached
160 fromUpperBound = reachableStates (BFS)/fromLowerBound(HD)
161 interiorStates = states with no new successors
162 interiorStateCandidates = states that may be interior
163 states depending on whether all of them are added to
164 reachableStates.
165
166 Currently, this does not support the incrementalFlag = 1 option.
167
168 Reachability Analysis (upper bound by overapproximate FSM traversal)
169 gives an upper bound of exact reachable states by overapproximation.
170 It is requested as approxFlag = Fsm_Rch_Oa_c. To do this, first, it
171 groups latch variables by using SSD(State Space Decomposition in the
172 paper Cho et.al, TCAD96-DEC) algorithm, then computes the reachable
173 states of each submachines until convergence, then the product of
174 reachable states of all submachines is an overapproximate reachable
175 states. In this case, depthValue and shellFlag and incrementalFlag
176 are incompatible with this option.
177
178 ARDC-accelerated Reachability Analysis may allow faster and smaller
179 memory usage reachability analysis. First, it computes
180 overapproximated reachable states (if already computed, just use it).
181 Reachability Analysis is then performed (any value of approxFlag is
182 applicable) with a transition relation minimized with the complement
183 of overapproximate reachable states as don't cares (called
184 ARDC). This option is requested as ardc = 1.
185
186 invarStates is a set of invariant states that can be specified. The
187 reachable states must satisfy all invariants. The default value is
188 NULL. Any invalid invariant must also be set to NULL in the
189 invarStaes array. This option is used by the check_invariant
190 command. When an array of invariant states is provided, reachability
191 analysis is done until an invariant is violated or when reachability
192 finishes, whichever is earlier. If an approximation of the reachable
193 states exists, then each invariant is checked for violation. If none
194 are violated, the set of reachable states is returned. It is the
195 caller's resposibility to remove the violating invariant from the
196 invarStates array to continue checking the remaining
197 invariants. The presence of invarStates takes precedence over a
198 non-zero depthValue.
199
200 In general, the reachable states may not be consistent with the
201 onion rings i.e., sum of onion rings is always contained in the
202 reachable states. When the shell flag is specified and onion rings
203 exist, the initial states are set to the sum of the onion ring
204 states instead of the default initial states of the fsm or
205 previously computed reachable states.
206
207 Some random simulation of the reachable states can be done prior to
208 reachability analysis. This is turned on using the rch_simulate
209 flag. A number should be specifed in the command : set sim_reach
210 <number>, which specifies the number of vectors to be simulated.
211 The initial states are then set to the simulated set of states. If
212 HD is specified, a subset may be taken.
213
214 The recompute flag asks for an explicit recomputation. This means
215 that even reachable states have been computed, they will be
216 recomputed.
217
218 On consecutive calls, recomputation is avoided as much as
219 possible. The specific cases are when
220 Case a. No shell Flag: Recomputation is avoided when reachability is
221 done, when an underapproximation exists and it violates an
222 invariant, an overapproximation exists and all invariants pass.
223
224 Case b. With shell flag: Recomputation is avoided when onion rings
225 are up-to-date and reachability is done or when onion rings are
226 up-to-date, an underapproximation exists and an invariant fails.
227
228 Update of fsm.reachabiltiyInfo fields are also based on minimum
229 recomputation. The reachability field is updated only if the current
230 set of reachable states are larger than the previous set.
231
232 printWarning flag turns is used to turn on/off the warning message
233 printed when the previously computed reachable states are used to
234 proceed with computation. The default is TRUE. ]
235
236 SideEffects [The result of the reachable state computation is stored
237 with the FSM. i.e., depth, reachable set, underapprox flag. ]
238
239 SeeAlso [Fsm_FsmComputeInitialStates
240 Fsm_ArdcComputeOverApproximateReachableStates]
241
242******************************************************************************/
243mdd_t *
244Fsm_FsmComputeReachableStates(
245 Fsm_Fsm_t *fsm,
246 int incrementalFlag,
247 int verbosityLevel,
248 int printStep,
249 int depthValue,
250 int shellFlag,
251 int reorderFlag,
252 int reorderThreshold,
253 Fsm_RchType_t approxFlag,
254 int ardc,
255 int recompute,
256 array_t *invarStates,
257 boolean printWarning,
258 array_t *guideArray)
259{
260 /* BFS variables */
261 Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t); /* image info structure*/
262 Img_ImageInfo_t *oldImageInfo = NIL(Img_ImageInfo_t);
263 mdd_t *reachableStates;/* reachable states */
264 mdd_t *unreachableStates;
265 mdd_t *fromLowerBound; /* new states in each iteration */
266 mdd_t *fromUpperBound; /* set to reachable states */
267 mdd_t *image, *newImage;/* image computed at each iteration */
268 mdd_t *initialStates; /* initial states */
269 mdd_t *toCareSet; /* the complement of the reached set */
270 int depth = 0; /* depth upto which the computation is
271 * performed.
272 */
273 graph_t *partition, *oldPartition;
274 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); /* mdd manager */
275 Ntk_Network_t *network = fsm->network; /* network */
276 bdd_reorder_type_t currentMethod =
277 Ntk_NetworkReadDynamicVarOrderingMethod(network); /* current reordering
278 * method */
279 int firstTimeFlag = TRUE, firstReorderFlag = FALSE;
280 /* a flag to indicate the start of the computation */
281 Fsm_RchStatus_t rchStatus = Fsm_Rch_Under_c;
282 /* under approximation of the reached set computed */
283 int reachableStateSetSize; /* bdd size of the reached set */
284 array_t *mintermVarArray; /* array of present state variables */
285 array_t *onionRings = NIL(array_t);
286 /* onionringarray for shellFlag computation */
287
288 /* Incremental flag variables */
289 array_t *arrayOfRoots = NIL(array_t);
290 st_table *tableOfLeaves = NIL(st_table);
291 int numLatch = 0;
292 array_t *relationArray = NIL(array_t), *smoothVarArray = NIL(array_t);
293
294 boolean notConverged = FALSE; /* flag that says that the fixpoint procedure
295 did not converge. */
296 /* HD variables */
297 FsmHdStruct_t *hdInfo = NULL;
298 int nvars; /* number of present state variables */
299
300
301 /* Simulation variables */
302 int simNVec = 0; /* number of simulation vectors. */
303 char *simString = Cmd_FlagReadByName("rch_simulate");
304
305 /* Guided Search */
306 array_t *hintDepthArray = NIL(array_t);
307 int hintDepth = -1;
308 mdd_t *hint = NIL(mdd_t); /* iterates over guide array */
309 int hintnr; /* idem */
310 boolean guidedSearchMode = FALSE;
311 boolean guideArrayAllocated = FALSE;
312
313 boolean invariantFailed = FALSE;
314
315 /* initializations */
316 /* if fsm is a submachine, takes realPsVars to count minterm correctly. */
317 mintermVarArray = Fsm_FsmReadPresentStateVars(fsm);
318
319 /* compute number of present state variables */
320 nvars = ComputeNumberOfBinaryStateVariables(mddManager, mintermVarArray);
321 assert(nvars > 0);
322
323 /* initializations */
324 if (recompute) {
325 if (incrementalFlag &&
326 ((approxFlag == Fsm_Rch_Hd_c) || (approxFlag == Fsm_Rch_Oa_c))) {
327 fprintf(vis_stdout,
328 "** rch error: Incremental flag and HD computation are not compatible\n");
329 return NIL(mdd_t);
330 }
331 FsmResetReachabilityFields(fsm, approxFlag);
332 } else if ((!shellFlag) || Fsm_FsmTestReachabilityOnionRingsUpToDate(fsm)) {
333 /* If already computed and exact , just return a copy. */
334 reachableStates = Fsm_FsmReadReachableStates(fsm);
335 if (reachableStates != NIL(mdd_t)){
336 if (printWarning) {
337 fprintf(vis_stdout, "** rch info: Reachable states have been previously computed.\n");
338 fprintf(vis_stdout, "** rch info: Not recomputing reachable states.\n");
339 fprintf(vis_stdout, "** rch info: Use compute_reach -F to recompute if necessary.\n");
340 }
341 if (!shellFlag) {
342 if (printWarning) {
343 if (FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Bfs_c) {
344 fprintf(vis_stdout, "** rch info: All previous computations done using BFS (-A 0 option).\n");
345 } else {
346 fprintf(vis_stdout, "** rch info: Some previous computations done using BFS/DFS mode (-A 1 or -g option).\n");
347 }
348 }
349 return (mdd_dup(reachableStates));
350 } else if (Fsm_FsmReadReachabilityOnionRings(fsm)) {
351 /* if onion rings exist, since they are up-to-date, return the
352 * reachable states
353 */
354 if (printWarning) {
355 if (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Bfs_c) {
356 fprintf(vis_stdout, "** rch info: Onion rings have been computed using BFS (-A 0 option)\n");
357 } else {
358 fprintf(vis_stdout, "** rch info: Some onion rings have been computed using BFS/DFS (-A 1 or -g option)\n");
359 }
360 }
361 if (printStep)
362 PrintOnionRings(fsm, printStep, approxFlag, nvars);
363 return (mdd_dup(reachableStates));
364 }
365 }
366
367 /* if some computed states exist and they violate an invariant,
368 return the current set of reachable states */
369 reachableStates = Fsm_FsmReadCurrentReachableStates(fsm);
370 if (reachableStates != NIL(mdd_t)) {
371 if (!shellFlag) {
372 /* if an underApprox exists, check invariant, if any */
373 if (invarStates != NIL(array_t)) {
374 if (!CheckStatesContainedInInvariant(reachableStates, invarStates)) {
375 if (printWarning) {
376 fprintf(vis_stdout, "** rch info: Invariant violation using previously computed states\n");
377 }
378 /* return violating reachable states */
379 return (mdd_dup(reachableStates));
380 }
381 }
382 } else if (Fsm_FsmReadReachabilityOnionRings(fsm)) {
383 /* an invariant fails. */
384 if (invarStates != NIL(array_t)) {
385 if (!CheckStatesContainedInInvariant(reachableStates, invarStates)) {
386 if (printWarning) {
387 fprintf(vis_stdout, "** rch info: Invariant violation using previously computed states\n");
388 if (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Bfs_c) {
389 fprintf(vis_stdout, "** rch info: Previous onion rings computed in BFS (-A 0 option).\n");
390 } else {
391 fprintf(vis_stdout, "** rch info: Some set of onion rings have been computed using BFS/DFS (-A 1 or -g option)\n");
392 }
393 fprintf(vis_stdout, "** rch info: Use compute_reach -F to recompute if necessary.\n");
394 }
395 if (printStep) {
396 PrintOnionRings(fsm, printStep, approxFlag, nvars);
397 }
398 return (mdd_dup(reachableStates));
399 }
400 }
401 }
402 }
403 /* if an over approx exists, check invariant, if any */
404 if ((invarStates != NIL(array_t)) && (!shellFlag) && (!depthValue) &&
405 (Fsm_FsmReadOverApproximateReachableStates(fsm)
406 != NIL(array_t))) {
407 if (FsmArdcCheckInvariant(fsm, invarStates)) {
408 fprintf(vis_stdout, "** rch info: Over approximation exists, using over approximation for invariant checking.\n");
409 return(Fsm_ArdcGetMddOfOverApproximateReachableStates(fsm));
410 }
411 }
412
413 if (incrementalFlag &&
414 ((approxFlag == Fsm_Rch_Hd_c) || (approxFlag == Fsm_Rch_Oa_c))) {
415 fprintf(vis_stdout,
416 "** rch error: Incremental flag and HD computation are not compatible\n");
417
418 return NIL(mdd_t);
419 }
420 }
421 /* onion rings make no sense with Over approx */
422 if (shellFlag && (approxFlag == Fsm_Rch_Oa_c)) {
423 fprintf(vis_stdout, "** rch error: Can't generate onion rings with over approx\n");
424 return NIL(mdd_t);
425 }
426
427 /* depth value makes no sense with over approximation */
428 if (depthValue && (approxFlag == Fsm_Rch_Oa_c)) {
429 fprintf(vis_stdout, "** rch error: Can't generate over approx with depth Value\n");
430 return NIL(mdd_t);
431 }
432
433 /* guided search cannot be done with Over approximation */
434 if ((guideArray != NIL(array_t)) && (approxFlag == Fsm_Rch_Oa_c)) {
435 fprintf(vis_stdout, "Guided search is not implemented with Over approximations\n");
436 return NIL(mdd_t);
437 }
438
439 /* initializations */
440 reachableStateSetSize = 0;
441 if ((approxFlag == Fsm_Rch_Hd_c) || (guideArray != NIL(array_t))) {
442 /* this structure is needed for HD and guidedSearch */
443 hdInfo = FsmHdStructAlloc(nvars);
444 }
445
446 simNVec = 0;
447 if (simString != NIL(char)) {
448 simNVec = strtol(simString, NULL, 10);
449 if (simNVec <= 0) simNVec = 0;
450 }
451 /* initialize onion ring array */
452 if (shellFlag) {
453 if (Fsm_FsmReadReachabilityOnionRings(fsm) == NIL(array_t)) {
454 onionRings = array_alloc(mdd_t *, 0);
455 } else {
456 onionRings = Fsm_FsmReadReachabilityOnionRings(fsm);
457 }
458 }
459
460 /* Computes ARDCs, and overapproximation by SSD traversal, if required. */
461 if (approxFlag == Fsm_Rch_Oa_c || ardc) {
462 long initialTime = 0;
463 long finalTime;
464
465 assert(!incrementalFlag);
466
467 if (verbosityLevel > 0)
468 initialTime = util_cpu_time();
469
470 (void)Fsm_FsmComputeOverApproximateReachableStates(fsm, incrementalFlag,
471 verbosityLevel, printStep, depthValue, shellFlag, reorderFlag,
472 reorderThreshold, recompute);
473
474 if (approxFlag == Fsm_Rch_Oa_c) {
475 if (hdInfo != NIL(FsmHdStruct_t)) FsmHdStructFree(hdInfo);
476 return(Fsm_ArdcGetMddOfOverApproximateReachableStates(fsm));
477 }
478
479 if (verbosityLevel > 0) {
480 finalTime = util_cpu_time();
481 Fsm_ArdcPrintReachabilityResults(fsm, finalTime-initialTime);
482 }
483 }
484
485 if(Cmd_FlagReadByName("linear_compute_range")) {
486 partition = Part_NetworkCreatePartition(network, 0, "temp", (lsList)0,
487 (lsList)0, NIL(mdd_t), Part_Fine_c, 0, 0, 0, 0);
488 oldPartition = fsm->partition;
489 oldImageInfo = fsm->imageInfo;
490 fsm->imageInfo = 0;
491 imageInfo = Fsm_FsmReadOrCreateImageInfoForComputingRange(fsm, 0, 1);
492 unreachableStates = Img_ImageGetUnreachableStates(imageInfo);
493 fprintf(vis_stdout, "%-20s%10g\n", "reachable states =",
494 mdd_count_onset(mddManager, unreachableStates,
495 fsm->fsmData.presentStateVars));
496 fflush(vis_stdout);
497 /* get unreachable states */
498 Img_ImageInfoFree(imageInfo);
499 fsm->imageInfo = oldImageInfo;
500 fsm->partition = oldPartition;
501 Part_PartitionFree(partition);
502 exit(0);
503 }
504 /* Compute the set of initial states. Start with the
505 * underapproximation of Reached states if it exists or sum of
506 * onion rings if shell flag is specified or the initial states of
507 * the fsm.
508 */
509 initialStates = ComputeInitialStates(fsm, shellFlag, printWarning);
510 if (initialStates == NIL(mdd_t)) {
511 fprintf(vis_stdout, "** rch error: No initial states computed.");
512 fprintf(vis_stdout, " No reachability will be performed.\n");
513 if (hdInfo != NIL(FsmHdStruct_t)) FsmHdStructFree(hdInfo);
514 return NIL(mdd_t);
515 }
516
517 if (incrementalFlag){
518 /* Note: if incrementalflag is set, no imageinfo is created! */
519 numLatch = InitializeIncrementalParameters(fsm, network, &arrayOfRoots,
520 &tableOfLeaves);
521 smoothVarArray = array_join(fsm->fsmData.presentStateVars,
522 fsm->fsmData.inputVars);
523 relationArray = array_alloc(mdd_t *, numLatch+1);
524 } else {
525 /* Create an imageInfo for image computations, if not already created. */
526 imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, 0, 1);
527 if (ardc) {
528 Fsm_ArdcMinimizeTransitionRelation(fsm, Img_Forward_c);
529 }
530 }
531
532 /* Get approximate traversal options */
533 if ((!incrementalFlag) && (approxFlag == Fsm_Rch_Hd_c)) {
534 /* only partial image allowed. No approximation of frontier set */
535 hdInfo->onlyPartialImage = Fsm_FsmHdOptionReadOnlyPartialImage(hdInfo->options);
536 /* states which can produce no new successors. */
537 hdInfo->interiorStates = bdd_zero(mddManager);
538 }
539
540 /* pertaining to simulation */
541 if (simNVec > 0) {
542 RandomSimulation(simNVec, fsm, approxFlag, initialStates,
543 &reachableStates, &fromLowerBound, hdInfo);
544 } else {
545 /* start reached set with initial states */
546 reachableStates = mdd_dup(initialStates);
547 fromLowerBound = mdd_dup(reachableStates);
548 }
549
550 /* initialize variables to print */
551 if ((!incrementalFlag) && (approxFlag == Fsm_Rch_Hd_c)) {
552
553 FsmHdStatsComputeSizeAndMinterms(mddManager, reachableStates,
554 mintermVarArray, nvars,
555 Fsm_Hd_Reached, hdInfo->stats);
556 FsmHdStatsComputeSizeAndMinterms(mddManager, fromLowerBound,
557 mintermVarArray, nvars,
558 Fsm_Hd_From, hdInfo->stats);
559 FsmHdStatsSetMintermFromSubset(hdInfo->stats, FsmHdStatsReadMintermFrom(hdInfo->stats));
560 FsmHdStatsSetSizeFromSubset(hdInfo->stats, FsmHdStatsReadSizeFrom(hdInfo->stats));
561 }
562
563 if (printStep && ((depth % printStep) == 0) && (approxFlag == Fsm_Rch_Hd_c)){
564 fprintf(vis_stdout, "\nIndex: R = Reached; I = Image, F = Frontier, FA = Approximation of Frontier\n");
565 fprintf(vis_stdout, " f = Minterms in f; |f| = Bdd nodes in f\n\n");
566 }
567 /* initialize for the first iteration */
568 fromUpperBound = reachableStates;
569
570 /* hint array */
571 if (guideArray == NIL(array_t)) {
572 guideArray = array_alloc(mdd_t *, 0);
573 guideArrayAllocated = TRUE;
574 }
575 /* pad with 1 when no hints are provided */
576 if (array_n(guideArray) == 0) {
577 array_insert_last(mdd_t *, guideArray, bdd_one(mddManager));
578 }
579 /* depth sequence for hints. 1-to-1 correspondence with guidearray */
580 /* -1 implies apply hint to convergence. */
581 hintDepthArray = GenerateGuidedSearchSequenceArray(guideArray);
582
583 assert(array_n(hintDepthArray) == array_n(guideArray));
584
585 if (array_n(guideArray) == 0) hint = mdd_one(mddManager);
586
587 arrayForEachItem(mdd_t *, guideArray, hintnr, hint){
588
589 /* check the depth for which this hint is to be applied. */
590 hintDepth = array_fetch(int, hintDepthArray, hintnr);
591
592 if(hintnr == 0 && mdd_is_tautology(hint, 1) && array_n(guideArray) == 1){
593 assert(hintDepth == -1);
594 } else {
595 assert(!incrementalFlag);
596 guidedSearchMode = TRUE;
597 Fsm_InstantiateHint(fsm, hint, 1, 0, Ctlp_Underapprox_c,
598 verbosityLevel > 1);
599 if (hintnr < (array_n(guideArray)-1))
600 fprintf(vis_stdout, "**GS info: Instantiating hint number %d\n", hintnr+1);
601 else
602 fprintf(vis_stdout, "**GS info: Restoring original transition relation\n");
603
604 if (approxFlag == Fsm_Rch_Hd_c) {
605 /* clean up all the invalid state information */
606 if (hdInfo->interiorStates != NIL(mdd_t))
607 mdd_free(hdInfo->interiorStates);
608 hdInfo->interiorStates = NIL(mdd_t); /* for every new hint, this is invalid. */
609 if (hdInfo->interiorStateCandidate != NIL(mdd_t))
610 mdd_free(hdInfo->interiorStateCandidate);
611 hdInfo->interiorStateCandidate = NIL(mdd_t); /* for every new hint, this is invalid */
612 hdInfo->imageOfReachedComputed = FALSE; /* since it doesn't matter for every new hint */
613 if (hdInfo->deadEndResidue != NIL(mdd_t))
614 mdd_free(hdInfo->deadEndResidue);
615 hdInfo->deadEndResidue = NIL(mdd_t);
616 }
617 /* generate a frontier by doing a dead-end computation if the
618 frontier is empty. This is non-greedy for BFS and greedy for
619 HD. */
620 if (mdd_is_tautology(fromLowerBound, 0)) {
621 ComputeReachabilityParameters(mddManager, imageInfo, approxFlag,
622 &reachableStates, &fromUpperBound,
623 &fromLowerBound, &image, hdInfo,
624 initialStates,
625 mintermVarArray,
626 &depth, printStep,
627 shellFlag, onionRings,
628 verbosityLevel,
629 guidedSearchMode, hint, &hintDepth,
630 &notConverged);
631 }
632 }
633 /* initialize */
634 notConverged = FALSE;
635 if (!incrementalFlag)
636 Img_ImageInfoResetUseOptimizedRelationFlag(imageInfo);
637 /* Main loop of reachability computation. */
638 /* Iterate until fromLowerBound is empty or all states are reached. */
639 while (!mdd_is_tautology(fromLowerBound, 0)) {
640 if(depth > 0 && !incrementalFlag)
641 Img_ImageInfoSetUseOptimizedRelationFlag(imageInfo);
642 /* fromLowerBound is the "onion shell" of states just reached. */
643 if ((shellFlag && (approxFlag != Fsm_Rch_Hd_c) &&
644 (!firstTimeFlag ||
645 (Fsm_FsmReadReachabilityOnionRings(fsm) == NIL(array_t)))) ||
646 (shellFlag && (approxFlag == Fsm_Rch_Hd_c) &&
647 (Fsm_FsmReadReachabilityOnionRings(fsm) == NIL(array_t)) &&
648 firstTimeFlag)) {
649 array_insert_last(mdd_t*, onionRings, mdd_dup(fromLowerBound));
650 }
651
652 /* if it is the print step, print out the iteration and the */
653 if (printStep && ((depth % printStep) == 0)) {
654 int step;
655 /* for BFS, preserve earlier format of printing */
656 step = (shellFlag) ? array_n(onionRings) : Fsm_FsmGetReachableDepth(fsm)+depth;
657 PrintStatsPerIteration(approxFlag,
658 nvars,
659 step,
660 hdInfo,
661 mddManager,
662 reachableStates,
663 fromLowerBound,
664 mintermVarArray);
665 }
666
667 /* Check if invariant contains the new states. In case of HD
668 * computation, check the containment of the entire reached set.
669 */
670 if (invarStates != NIL(array_t)) {
671 mdd_t *temp;
672 temp = (approxFlag == Fsm_Rch_Hd_c) ? reachableStates : fromLowerBound;
673 if (!CheckStatesContainedInInvariant(temp, invarStates)) {
674 notConverged = TRUE;
675 invariantFailed = TRUE; /* flag used for early termination */
676 break;
677 }
678 }
679
680 if (mdd_is_tautology(reachableStates, 1)) {
681 break;
682 }
683
684 if ((depthValue && (depth == depthValue)) ||
685 /* limited depth hint is implemented this way */
686 (hintDepth == 0)) {
687 /* No more steps */
688 notConverged = TRUE;
689 break;
690 }
691
692 if (reorderFlag && !firstReorderFlag &&
693 (reachableStateSetSize >= reorderThreshold )){
694 firstReorderFlag = TRUE;
695 (void) fprintf(vis_stdout, "Dynamic variable ordering forced ");
696 (void) fprintf(vis_stdout, "with method sift\n");
697 Ntk_NetworkSetDynamicVarOrderingMethod(network,
698 BDD_REORDER_SIFT,
699 BDD_REORDER_VERBOSITY_DEFAULT);
700 bdd_reorder(Ntk_NetworkReadMddManager(network));
701 Ntk_NetworkSetDynamicVarOrderingMethod(network, currentMethod,
702 BDD_REORDER_VERBOSITY_DEFAULT);
703 }
704
705 firstTimeFlag = FALSE;
706 /* careSet for image computation is the set of all states not reached
707 * so far.
708 */
709 toCareSet = mdd_not(reachableStates);
710
711 /*
712 * Image of some set between lower and upper, where we care
713 * about the image only on unreached states.
714 */
715 if (incrementalFlag){
716 image = IncrementalImageCompute(network, fsm, mddManager,
717 fromLowerBound,
718 fromUpperBound, toCareSet,
719 arrayOfRoots, tableOfLeaves,
720 smoothVarArray, relationArray,
721 numLatch);
722 } else{
723 assert(!incrementalFlag);
724
725 if (approxFlag == Fsm_Rch_Hd_c) {
726 /* allow partial image computation */
727 Img_ImageAllowPartialImage(imageInfo, TRUE);
728 }
729
730 /* compute the image of this iteration */
731 image = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
732 fromLowerBound,
733 fromUpperBound,
734 toCareSet);
735
736
737
738 /* record if partial image or not */
739 if (approxFlag == Fsm_Rch_Hd_c) {
740 /* Check if partial image computation, disallow partial image
741 * computation.
742 */
743 hdInfo->partialImage = Img_ImageWasPartial(imageInfo);
744 /* record this to prevent dead-end computation. */
745 hdInfo->imageOfReachedComputed = (!hdInfo->partialImage) &&
746 mdd_equal(reachableStates, fromLowerBound);
747 /* potential candidates for interior states (only if not a
748 * partial image)
749 */
750 if (!hdInfo->partialImage) hdInfo->interiorStateCandidate = mdd_dup(fromLowerBound);
751 }
752 }
753
754 /* free the used bdds */
755 mdd_free(toCareSet);
756
757 /* New lower bound is the states just reached. */
758 mdd_free(fromLowerBound);
759 fromLowerBound = mdd_and(image, reachableStates, 1, 0);
760 depth++;
761 hintDepth--;
762
763
764 if ((!incrementalFlag) && (approxFlag == Fsm_Rch_Hd_c)) {
765 FsmHdStatsComputeSizeAndMinterms(mddManager, image,
766 mintermVarArray, nvars,
767 Fsm_Hd_To, hdInfo->stats);
768 }
769
770 /* need image only if HD and not dead-end */
771 if (approxFlag != Fsm_Rch_Hd_c) {
772 mdd_free(image);
773 image = NULL;
774 } else {
775 if (hdInfo->imageOfReachedComputed || hdInfo->onlyPartialImage ||
776 (hdInfo->slowGrowth >= FSM_HD_NUM_SLOW_GROWTHS) ||
777 mdd_is_tautology(fromLowerBound, 0)) {
778 mdd_free(image);
779 image = NULL;
780 }
781 }
782
783 /* computes reachable states, fromlowerBound and fromupperbound
784 * for BFS. For HD it computes the above as well as interior
785 * statess, dead-end residue, etc. All the other parameteres are
786 * updated. For guided search, this call does not perform a
787 * non-greedy dead-end computation, even if the frontier is 0. */
788 ComputeReachabilityParameters(mddManager, imageInfo, approxFlag,
789 &reachableStates,
790 &fromUpperBound,
791 &fromLowerBound,
792 &image,
793 hdInfo,
794 initialStates,
795 mintermVarArray,
796 &depth, printStep,
797 shellFlag, onionRings,
798 verbosityLevel, FALSE, hint,
799 &hintDepth,
800 &notConverged);
801
802
803 if (mdd_is_tautology(fromLowerBound, 0) &&
804 (approxFlag == Fsm_Rch_Bfs_c) &&
805 (!guidedSearchMode) && (!depthValue))
806 depth--;
807
808 } /* end of main while loop (while frontier != 0) */
809
810 /* stop iterating over hint if invariants are violated or all
811 states are reachable or limited depth value has been
812 reached. */
813 if (invariantFailed) break;
814 if (mdd_is_tautology(reachableStates, 1)) {
815 break;
816 }
817 if (depthValue && (depth == depthValue)) {
818 /* No more steps */
819 break;
820 }
821
822 }/* for each hint */
823
824
825 if(!incrementalFlag &&
826 Img_ImageInfoObtainMethodType(imageInfo) == Img_Linear_c &&
827 Img_ImageInfoObtainOptimizeType(imageInfo) == Opt_NS &&
828 Img_IsTransitionRelationOptimized(imageInfo)) {
829 Img_ImageInfoResetUseOptimizedRelationFlag(imageInfo);
830 fprintf(vis_stdout, "%-20s%10g\n", "reachable states =",
831 mdd_count_onset(mddManager, reachableStates,
832 fsm->fsmData.presentStateVars));
833 fromLowerBound = mdd_dup(reachableStates);
834 fromUpperBound = reachableStates;
835 while (1) {
836 toCareSet = mdd_dup(reachableStates);
837 image = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
838 fromLowerBound,
839 fromUpperBound,
840 toCareSet);
841 newImage = bdd_or(image, initialStates, 1, 1);
842 bdd_free(image);
843 image = newImage;
844 if(mdd_equal(fromLowerBound, image)) {
845 mdd_free(toCareSet);
846 mdd_free(fromLowerBound);
847 mdd_free(reachableStates);
848 fromLowerBound = image;
849 reachableStates = mdd_dup(fromLowerBound);
850 fromUpperBound = reachableStates;
851 fprintf(vis_stdout, "%-20s%10g\n", "reachable states =",
852 mdd_count_onset(mddManager, reachableStates,
853 fsm->fsmData.presentStateVars));
854 break;
855 }
856 mdd_free(toCareSet);
857 mdd_free(fromLowerBound);
858 mdd_free(reachableStates);
859 fromLowerBound = image;
860 reachableStates = mdd_dup(fromLowerBound);
861 fromUpperBound = reachableStates;
862
863 fprintf(vis_stdout, "%-20s%10g\n", "reachable states =",
864 mdd_count_onset(mddManager, reachableStates,
865 fsm->fsmData.presentStateVars));
866 }
867 }
868
869
870 /* clean up for Guided search mainly, only if needed */
871 /* we rely on the fact that the variable hint is set to the last hint from
872 * the previous loop.
873 */
874 if (guidedSearchMode && !mdd_is_tautology(hint, 1))
875 Fsm_CleanUpHints(fsm, 1, 0, printStep);
876 array_free(hintDepthArray);
877
878 /* If (1) all states are reachable, or (2) not limited depth computation
879 and not a converge with a hint, or (3) limited depth and not
880 guided search mode and BFS and frontier = 0, or (4) in guided
881 search, if limited depth and frontier = 0 then one full dead-end
882 should have occured */
883 if(mdd_is_tautology(reachableStates, 1) ||
884 ((notConverged == FALSE) && mdd_is_tautology(hint, 1)) ||
885 (!guidedSearchMode && (notConverged == TRUE) &&
886 mdd_is_tautology(fromLowerBound, 0) && (approxFlag == Fsm_Rch_Bfs_c)) ||
887 (guidedSearchMode && hdInfo->deadEndWithOriginalTR &&
888 mdd_is_tautology(fromLowerBound, 0) && (approxFlag == Fsm_Rch_Bfs_c))) {
889
890 rchStatus = Fsm_Rch_Exact_c;
891 if (mdd_is_tautology(reachableStates, 1) &&
892 !mdd_is_tautology(fromLowerBound, 0) &&
893 printStep && ((depth % printStep) == 0) ) {
894 int step;
895 /* for BFS, preserve earlier format of printing */
896 step = (shellFlag) ?
897 array_n(onionRings) :
898 Fsm_FsmGetReachableDepth(fsm)+depth;
899 PrintStatsPerIteration(approxFlag, nvars, step, hdInfo,
900 mddManager, reachableStates,
901 fromLowerBound, mintermVarArray);
902 }
903 }
904
905 /* clean up the hints if allocated here */
906 if (guideArrayAllocated) mdd_array_free(guideArray);
907
908 if (hdInfo != NIL(FsmHdStruct_t)) {
909 FsmHdStructFree(hdInfo);
910 }
911
912 mdd_free(fromLowerBound);
913 mdd_free(initialStates);
914
915 /* Update FSM reahcability fields */
916
917 /* indicate whether the shells are consistent with the reachable states */
918 if (!shellFlag) {
919 /* if any states were added from a previous computation, shells
920 are not up-to-date */
921 if (Fsm_FsmReadCurrentReachableStates(fsm) != NIL(mdd_t)) {
922 if (!mdd_lequal(reachableStates, Fsm_FsmReadCurrentReachableStates(fsm), 1, 1)) {
923 FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE);
924 } /* otherwise the previous iteration was computed with onion
925 rings, in which case it is still up-to-date or the previous
926 iteration was computed without onion rings and it was set to not
927 up-to-date in the previous iteration */
928 } else {
929 assert(Fsm_FsmReadReachabilityOnionRings(fsm) == NIL(array_t));
930 /* not up-to-date because no onion rings */
931 FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE);
932 }
933
934 } else {
935 /* shells are up to date only if current set adds upto previously
936 computed states or more */
937 if (Fsm_FsmReadCurrentReachableStates(fsm)) {
938 if (!mdd_lequal(Fsm_FsmReadCurrentReachableStates(fsm),
939 reachableStates, 1, 1)) {
940 FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE);
941 } else {
942 FsmSetReachabilityOnionRingsUpToDateFlag(fsm, TRUE);
943 }
944
945 } else FsmSetReachabilityOnionRingsUpToDateFlag(fsm, TRUE);
946
947 /* Onion rings are not BFS, i.e., HD or Guided search. */
948 if ((approxFlag == Fsm_Rch_Hd_c) ||
949 (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Hd_c) ||
950 guidedSearchMode)
951 FsmSetReachabilityOnionRingsMode(fsm, Fsm_Rch_Hd_c);
952
953 if (array_n(onionRings) == 0) {
954 array_free(onionRings);
955 onionRings = NIL(array_t);
956 }
957 FsmSetReachabilityOnionRings(fsm, onionRings);
958 }
959
960 /* update fsm structure */
961 /* record depth of traversal, depth is consistent with reachable
962 states, hence may not be consistent with the onion rings */
963 /* replace reachable states if only more states have been computed now */
964 if (Fsm_FsmReadCurrentReachableStates(fsm) != NIL(mdd_t)) {
965 if (!mdd_lequal(reachableStates, Fsm_FsmReadCurrentReachableStates(fsm), 1, 1)) {
966 Fsm_FsmFreeReachableStates(fsm);
967 fsm->reachabilityInfo.reachableStates = mdd_dup(reachableStates);
968 if (!shellFlag) fsm->reachabilityInfo.depth = Fsm_FsmGetReachableDepth(fsm) + depth;
969 else if (Fsm_FsmReadReachabilityOnionRings(fsm))
970 fsm->reachabilityInfo.depth = array_n(Fsm_FsmReadReachabilityOnionRings(fsm));
971 /* set computation mode as HD if HD or Guided search, basically to indicate not BFS */
972 if ((approxFlag == Fsm_Rch_Hd_c) ||
973 (FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Hd_c) ||
974 guidedSearchMode) {
975 FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Hd_c);
976 }
977 }
978 } else {
979 fsm->reachabilityInfo.reachableStates = mdd_dup(reachableStates);
980 if (!shellFlag) fsm->reachabilityInfo.depth = depth;
981 else if (Fsm_FsmReadReachabilityOnionRings(fsm))
982 fsm->reachabilityInfo.depth = array_n(Fsm_FsmReadReachabilityOnionRings(fsm));
983 /* set computation mode as HD if HD or Guided search, basically to indicate not BFS */
984 if ((approxFlag == Fsm_Rch_Hd_c) || guidedSearchMode) {
985 FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Hd_c);
986 } else {
987 FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Bfs_c);
988 }
989
990 }
991 /* indicate whether reachability analysis is completed or not */
992 FsmSetReachabilityApproxComputationStatus(fsm, rchStatus);
993
994 if (incrementalFlag){
995 array_free(relationArray);
996 array_free(arrayOfRoots);
997 st_free_table(tableOfLeaves);
998 array_free(smoothVarArray);
999 /* Need to put in next state function data for the partition */
1000 }
1001
1002 return reachableStates;
1003} /* end of Fsm_FsmComputeReachableStates */
1004
1005
1006
1007/**Function********************************************************************
1008
1009 Synopsis [Existentially quantifies variables from an implicit product.]
1010
1011 Description [Existentially quantifies the smoothing variables from the
1012 product of the MDDs in mddArray, and returns the result. SmoothingVars is an
1013 array of MDD ids. For now, uses the simplistic approach of conjunction all
1014 the MDDs, and then quantifying the smoothing variables.]
1015
1016 SideEffects []
1017
1018******************************************************************************/
1019mdd_t *
1020Fsm_MddMultiwayAndSmooth(mdd_manager *mddManager, array_t *mddArray,
1021 array_t *smoothingVars)
1022{
1023 int i;
1024 mdd_t *resultMdd;
1025 mdd_t *product = mdd_one(mddManager);
1026
1027 for (i = 0; i<array_n(mddArray); i++){
1028 mdd_t *mdd = array_fetch(mdd_t*, mddArray, i);
1029 mdd_t *tempProduct = mdd_and(product, mdd, 1, 1);
1030 mdd_free(product);
1031 product = tempProduct;
1032 }
1033
1034 if (array_n(smoothingVars) == 0) {
1035 resultMdd = mdd_dup(product);
1036 }
1037 else{
1038 resultMdd = mdd_smooth(mddManager, product, smoothingVars);
1039 }
1040
1041 mdd_free(product);
1042 return resultMdd;
1043}
1044
1045/**Function********************************************************************
1046
1047 Synopsis [Prints the results of reachability analysis.]
1048
1049 Description [Prints the results of reachability analysis.]
1050
1051 SideEffects []
1052
1053 SeeAlso []
1054
1055******************************************************************************/
1056void
1057Fsm_FsmReachabilityPrintResults(
1058 Fsm_Fsm_t *fsm,
1059 long elapseTime,
1060 int approxFlag)
1061{
1062 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
1063 mdd_t *reachableStates = fsm->reachabilityInfo.reachableStates;
1064 array_t *psVarsArray;
1065 int nvars;
1066
1067 if (!reachableStates)
1068 return;
1069
1070 psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
1071 /* compute number of present state variables */
1072 nvars = ComputeNumberOfBinaryStateVariables(mddManager, psVarsArray);
1073
1074 (void) fprintf(vis_stdout,"********************************\n");
1075 (void) fprintf(vis_stdout,"Reachability analysis results:\n");
1076 if ((FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Bfs_c) &&
1077 (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t))) {
1078 (void) fprintf(vis_stdout, "%-20s%10d\n", "FSM depth =",
1079 fsm->reachabilityInfo.depth);
1080 } else {
1081 (void) fprintf(vis_stdout, "%-20s%10d\n", "computation depth =",
1082 fsm->reachabilityInfo.depth);
1083 }
1084 if (nvars <= 1023) {
1085 (void) fprintf(vis_stdout, "%-20s%10g\n", "reachable states =",
1086 mdd_count_onset(mddManager, reachableStates,
1087 fsm->fsmData.presentStateVars));
1088 } else {
1089 /*
1090 (void) fprintf(vis_stdout, "%-20s", "reachable states = ");
1091 bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6);
1092 */
1093 EpDouble epd;
1094 char strValue[20];
1095
1096 mdd_epd_count_onset(mddManager, reachableStates,
1097 fsm->fsmData.presentStateVars, &epd);
1098 EpdGetString(&epd, strValue);
1099 (void) fprintf(vis_stdout, "%-20s%10s\n", "reachable states =", strValue);
1100 }
1101 (void) fprintf(vis_stdout, "%-20s%10d\n", "BDD size =",
1102 mdd_size(reachableStates));
1103 (void) fprintf(vis_stdout, "%-20s%10g\n", "analysis time =",
1104 (double)elapseTime/1000.0);
1105 if (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t)) {
1106 (void) fprintf(vis_stdout, "%-20s%10s\n", "reachability analysis = ", "complete");
1107 } else {
1108 (void) fprintf(vis_stdout, "%-20s%10s\n", "reachability analysis = ", "incomplete");
1109 }
1110}
1111
1112
1113/*---------------------------------------------------------------------------*/
1114/* Definition of static functions */
1115/*---------------------------------------------------------------------------*/
1116
1117/**Function********************************************************************
1118
1119 Synopsis [Checks the validity of image]
1120
1121 Description [In a properly formed image, there should not be any
1122 domain or quantify variables in its support. This function checks
1123 for that fact.]
1124
1125 SideEffects []
1126
1127******************************************************************************/
1128static int
1129CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t
1130 *domainVarMddIdArray, array_t *quantifyVarMddIdArray)
1131{
1132 int i;
1133 array_t *imageSupportArray = mdd_get_support(mddManager, image);
1134 st_table *imageSupportTable = st_init_table(st_numcmp, st_numhash);
1135 for (i=0; i<array_n(imageSupportArray); i++){
1136 int mddId = array_fetch(int, imageSupportArray, i);
1137 (void) st_insert(imageSupportTable, (char *) (long) mddId, NIL(char));
1138 }
1139 for (i=0; i<array_n(domainVarMddIdArray); i++){
1140 int domainVarId;
1141 domainVarId = array_fetch(int, domainVarMddIdArray, i);
1142 assert(st_is_member(imageSupportTable, (char *)(long)domainVarId) == 0);
1143 }
1144 for (i=0; i<array_n(quantifyVarMddIdArray); i++){
1145 int quantifyVarId;
1146 quantifyVarId = array_fetch(int, quantifyVarMddIdArray, i);
1147 assert(st_is_member(imageSupportTable, (char *)(long)quantifyVarId) == 0);
1148 }
1149 st_free_table(imageSupportTable);
1150 array_free(imageSupportArray);
1151 return 1;
1152}
1153
1154/**Function********************************************************************
1155
1156 Synopsis [Counts the number of Bdd variables for the given Mdd id array].
1157
1158 Description [Counts the number of Bdd variables for the given Mdd id array]
1159
1160
1161 SideEffects []
1162
1163******************************************************************************/
1164/*static*/ int
1165ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager,
1166 array_t *mddIdArray)
1167{
1168 int mddId, i;
1169 mvar_type mddVar;
1170 int numEncodingBits, count = 0;
1171 array_t *mvar_list = mdd_ret_mvar_list(mddManager);
1172
1173 arrayForEachItem(int, mddIdArray, i, mddId) {
1174 mddVar = array_fetch(mvar_type, mvar_list, mddId);
1175 numEncodingBits = mddVar.encode_length;
1176 count += numEncodingBits;
1177 }
1178 return count;
1179} /* end of ComputeNumberOfBinaryStateVariables */
1180
1181
1182/**Function********************************************************************
1183
1184 Synopsis [Add states.]
1185
1186 Description [Add States.]
1187
1188 SideEffects [ Free the original parts]
1189
1190******************************************************************************/
1191static mdd_t *
1192AddStates(mdd_t *a, mdd_t *b, int freeA, int freeB)
1193{
1194 mdd_t *result;
1195 if ((a != NULL) && (b != NULL)) {
1196 result = mdd_or(a, b, 1, 1);
1197 } else if ((a == NULL) && (b == NULL)) {
1198 result = a;
1199 } else if (a == NULL) {
1200 result = mdd_dup(b);
1201 } else {
1202 result = mdd_dup(a);
1203 }
1204 if ((freeA == FSM_MDD_FREE) && (a != NULL)) mdd_free(a);
1205 if ((freeB == FSM_MDD_FREE) && (b != NULL)) mdd_free(b);
1206 return result;
1207} /* end of AddStates */
1208
1209
1210/**Function********************************************************************
1211
1212 Synopsis [Simulates randomly specified number of states.]
1213
1214 Description [Simulates randomly specified number of states.]
1215
1216 SideEffects []
1217
1218******************************************************************************/
1219static void
1220RandomSimulation(int simNVec,
1221 Fsm_Fsm_t *fsm,
1222 Fsm_RchType_t approxFlag,
1223 mdd_t *initialStates,
1224 mdd_t **reachableStates,
1225 mdd_t **fromLowerBound,
1226 FsmHdStruct_t *hdInfo)
1227{
1228 Ntk_Network_t *network = fsm->network;
1229
1230 /* Compute specified number of simulated states. */
1231 *reachableStates = Sim_RandomSimulate(network, simNVec, 0);
1232 *reachableStates = AddStates(*reachableStates, initialStates, FSM_MDD_FREE, FSM_MDD_DONT_FREE);
1233 *fromLowerBound = mdd_dup(*reachableStates);
1234
1235 if (approxFlag == Fsm_Rch_Hd_c) {
1236 if (mdd_size(*fromLowerBound) >
1237 Fsm_FsmHdOptionReadFrontierApproxThreshold(hdInfo->options)) {
1238 /* Reset frontier if too large. */
1239 mdd_free(*fromLowerBound);
1240 *fromLowerBound = bdd_between(initialStates, *reachableStates);
1241 if (!mdd_equal(*fromLowerBound, *reachableStates)) {
1242 hdInfo->firstSubset = FALSE;
1243 hdInfo->deadEndResidue = mdd_and(*reachableStates,
1244 *fromLowerBound, 1, 0);
1245 }
1246 }
1247 }
1248 return;
1249} /* end of RandomSimulation */
1250
1251
1252/**Function********************************************************************
1253
1254 Synopsis [Prints stats per iteration]
1255
1256 Description [Prints stats per iteration]
1257
1258 SideEffects []
1259
1260******************************************************************************/
1261static void
1262PrintStatsPerIteration(Fsm_RchType_t approxFlag,
1263 int nvars,
1264 int depth,
1265 FsmHdStruct_t *hdInfo,
1266 mdd_manager *mddManager,
1267 mdd_t *reachableStates,
1268 mdd_t *fromLowerBound,
1269 array_t *mintermVarArray)
1270{
1271 if (approxFlag != Fsm_Rch_Hd_c) {
1272 int reachableStateSetSize = mdd_size(reachableStates);
1273 if (nvars <= 1023) {
1274 (void)fprintf(vis_stdout, "BFS step = %d\t|states| = %8g\tBdd size = %8ld\n",
1275 depth, mdd_count_onset(mddManager, reachableStates,
1276 mintermVarArray),
1277 (long)reachableStateSetSize);
1278 /* bdd_print_minterm(reachableStates); */
1279 } else {
1280 (void)fprintf(vis_stdout, "BFS step = %d\tBdd size = %8d\t|states| = ",
1281 depth, reachableStateSetSize);
1282 (void) bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6);
1283 }
1284
1285 } else { /* HD */
1286
1287 if (nvars <= 1023) {
1288 (void)fprintf(vis_stdout, "Step = %d, R = %8g, |R| = %8d, I = %8g, |I| = %8d\n",
1289 depth, FsmHdStatsReadMintermReached(hdInfo->stats),
1290 FsmHdStatsReadSizeReached(hdInfo->stats), FsmHdStatsReadMintermTo(hdInfo->stats) ,
1291 FsmHdStatsReadSizeTo(hdInfo->stats));
1292 (void)fprintf(vis_stdout, "Completed iteration %d at %g seconds\n",
1293 depth, (util_cpu_time()/1000.0));
1294
1295 (void)fprintf(vis_stdout, "Step = %d, F = %8g, |F| = %8d, FA = %8g, |FA| = %8d\n",
1296 depth+1, FsmHdStatsReadMintermFrom(hdInfo->stats),
1297 FsmHdStatsReadSizeFrom(hdInfo->stats),
1298 FsmHdStatsReadMintermFromSubset(hdInfo->stats),
1299 FsmHdStatsReadSizeFromSubset(hdInfo->stats));
1300 } else {
1301 int status;
1302 (void)fprintf(vis_stdout, "Step = %d, |R| = %8d, R = ",
1303 depth, FsmHdStatsReadSizeReached(hdInfo->stats));
1304 status = bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6);
1305 if (!status) {
1306 error_append("** rch error: Error in printing arbitrary precision minterm count of Reached");
1307 }
1308
1309 (void)fprintf(vis_stdout, "Completed iteration %d at %g seconds\n",
1310 depth, (util_cpu_time()/1000.0));
1311 (void)fprintf(vis_stdout, "Step = %d, |F| = %8d, F = %8g, |FA| = %8d, FA = ",
1312 depth, FsmHdStatsReadSizeFrom(hdInfo->stats), 0.0,
1313 FsmHdStatsReadSizeFromSubset(hdInfo->stats) );
1314 status = bdd_print_apa_minterm(vis_stdout, fromLowerBound, nvars, 6);
1315 if (!status) {
1316 error_append("** rch error: Error in printing arbitrary precision minterm count of From");
1317 }
1318 }
1319 }
1320 return;
1321} /* end of PrintStatsPerIteration */
1322
1323/**Function********************************************************************
1324
1325 Synopsis [Induce full dead-end if there is a big jump in Reached
1326 size]
1327
1328 Description [Induce full dead-end if there is a big jump in Reached
1329 size and not enough increase in minterms of Reached. So throw away
1330 the new large-sized Reached and compute its entire image. Use the
1331 dead-end computation for this and use the non-greedy flag. This is a
1332 recovery mechanism to combat fragmentation of the state space.]
1333
1334 SideEffects [Other quantities are adjusted accordingly. Now the Reached
1335 set before the dead-end computation will be added to the interior states.]
1336
1337******************************************************************************/
1338static void
1339HdInduceFullDeadEndIfNecessary(mdd_manager *mddManager,
1340 Img_ImageInfo_t *imageInfo,
1341 mdd_t **fromLowerBound,
1342 mdd_t **fromUpperBound,
1343 mdd_t **reachableStates,
1344 mdd_t **image,
1345 FsmHdStruct_t *hdInfo,
1346 int *depth,
1347 int shellFlag,
1348 array_t *onionRings,
1349 array_t *mintermVarArray,
1350 int oldSize,
1351 double oldMint,
1352 int verbosityLevel)
1353{
1354 int nvars = Fsm_FsmHdOptionReadNumVars(hdInfo->options);
1355 /*
1356 * Compute a full (non-greedy) dead-end when a dead-end computation
1357 * hasn't occurred, and the jump in minterms is lower than MINT_GROWTH and
1358 * either the old reached size is between MID_SIZE and LARGE_SIZE and the
1359 * jump is MID_SIZE or the new size is larger than LARGE_SIZE and the jump
1360 * is LARGE_SIZE.
1361 */
1362 if ((hdInfo->deadEndComputation == FALSE) &&
1363 ((FsmHdStatsReadMintermReached(hdInfo->stats) - oldMint)/oldMint < FSM_HD_MINT_GROWTH) &&
1364 (((FsmHdStatsReadSizeReached(hdInfo->stats) > FSM_HD_MID_SIZE) &&
1365 (FsmHdStatsReadSizeReached(hdInfo->stats) - oldSize > FSM_HD_MID_SIZE) &&
1366 (oldSize > FSM_HD_MID_SIZE) && (oldSize < FSM_HD_LARGE_SIZE)) ||
1367 ((FsmHdStatsReadSizeReached(hdInfo->stats) > FSM_HD_LARGE_SIZE) &&
1368 (FsmHdStatsReadSizeReached(hdInfo->stats) - oldSize > FSM_HD_LARGE_SIZE)))) {
1369 if (verbosityLevel >= 2) {
1370 fprintf(vis_stdout, "Full Dead End: New Reached = %d, Minterms = %g\n",
1371 FsmHdStatsReadSizeReached(hdInfo->stats), FsmHdStatsReadMintermReached(hdInfo->stats));
1372 }
1373
1374 if (*image != NULL) {
1375 mdd_free(*image);
1376 *image = NULL;
1377 }
1378 /* throw away the reached with the jump in size */
1379 mdd_free(*reachableStates);
1380 if (shellFlag && onionRings) {
1381 mdd_free(array_fetch(mdd_t *, onionRings, array_n(onionRings)-1));
1382 array_insert(mdd_t *, onionRings, array_n(onionRings)-1, NIL(mdd_t));
1383 }
1384
1385 *reachableStates = *fromUpperBound;
1386 /* throw away interior state candidates since we just threw away
1387 * the new states
1388 */
1389 if (hdInfo->interiorStateCandidate != NIL(mdd_t)) {
1390 mdd_free(hdInfo->interiorStateCandidate);
1391 hdInfo->interiorStateCandidate = NIL(mdd_t);
1392 }
1393
1394 if (verbosityLevel >= 2) {
1395 /* record number of dead ends */
1396 (hdInfo->numDeadEnds)++;
1397 fprintf(vis_stdout, "Dead-End %d at %g seconds - FULL\n",
1398 hdInfo->numDeadEnds, (util_cpu_time()/1000.0));
1399 }
1400
1401 /* perform a full non-greedy dead-end computation */
1402 *fromLowerBound = FsmHdDeadEnd(mddManager, imageInfo, *reachableStates,
1403 hdInfo,
1404 mintermVarArray,
1405 FSM_HD_NONGREEDY, verbosityLevel);
1406 (*depth)++;
1407 /* update reached since a new set of seeds have been found */
1408 assert (!mdd_is_tautology(*fromLowerBound, 0));
1409 if (shellFlag && onionRings) {
1410 mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0);
1411 if (!mdd_is_tautology(temp, 0))
1412 array_insert(mdd_t *, onionRings, array_n(onionRings)-1, temp);
1413 else
1414 mdd_free(temp);
1415 }
1416 *fromUpperBound = *reachableStates;
1417 *reachableStates = mdd_or(*fromLowerBound, *fromUpperBound, 1, 1);
1418 FsmHdStatsComputeSizeAndMinterms(mddManager, *reachableStates,
1419 mintermVarArray, nvars,
1420 Fsm_Hd_Reached, hdInfo->stats);
1421 } /* end of if jump in Reached */
1422} /* end of HdInduceFullDeadEndIfNecessary */
1423
1424
1425/**Function********************************************************************
1426
1427 Synopsis [Compute initial states.]
1428
1429 Description [Compute initial states. Return fsm initial states if no
1430 previously computed states are found. If shell flag, compute union
1431 of rings. If not shell flag, return previously computed states.]
1432
1433 SideEffects []
1434
1435******************************************************************************/
1436static mdd_t *
1437ComputeInitialStates(Fsm_Fsm_t *fsm, int shellFlag, boolean printWarning)
1438{
1439 mdd_t *initialStates = NIL(mdd_t);
1440 boolean rings = FALSE;
1441 array_t *mintermVarArray = Fsm_FsmReadPresentStateVars(fsm);
1442
1443 if (Fsm_FsmReadCurrentReachableStates(fsm) == NIL(mdd_t)) {
1444 initialStates = Fsm_FsmComputeInitialStates(fsm);
1445 return (initialStates);
1446 } else if (shellFlag) {
1447 (void) Fsm_FsmReachabilityOnionRingsStates(fsm, &initialStates);
1448 if (initialStates == NIL(mdd_t)) {
1449 initialStates = Fsm_FsmComputeInitialStates(fsm);
1450 return (initialStates);
1451 } else if (mdd_is_tautology(initialStates, 0)) {
1452 initialStates = Fsm_FsmComputeInitialStates(fsm);
1453 return (initialStates);
1454 }
1455 /* some states are found in the onion rings */
1456 rings = TRUE;
1457 } else {
1458 /* use previously computed states */
1459 initialStates = mdd_dup(Fsm_FsmReadCurrentReachableStates(fsm));
1460 }
1461 if (printWarning) {
1462 fprintf(vis_stdout, "** rch warning: Starting reachability analysis from previously computed states.\n");
1463 fprintf(vis_stdout, "** rch warning: Use compute_reach -F to recompute if necessary.\n");
1464 fprintf(vis_stdout, "** rch warning: Previously computed states = %g, Size = %d, computation depth = 0-%d\n", mdd_count_onset(Fsm_FsmReadMddManager(fsm), initialStates, mintermVarArray), mdd_size(initialStates), fsm->reachabilityInfo.depth);
1465 if (!rings) {
1466 if (FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Bfs_c) {
1467 fprintf(vis_stdout, "** rch warning: Previous computation done with BFS (-A 0 option)\n");
1468 } else if (FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Hd_c) {
1469 fprintf(vis_stdout, "** rch warning: Some previous computations done using BFS/DFS mode (-A 1 or -g option)\n");
1470 }
1471 } else {
1472 if (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Bfs_c) {
1473 fprintf(vis_stdout, "** rch warning: Previous onion rings computed with BFS (-A 0 option)\n");
1474 } else if (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Hd_c) {
1475 fprintf(vis_stdout, "** rch warning: Some set of onion rings have been computed using BFS/DFS (-A 1 or -g option)\n");
1476 }
1477 }
1478 }
1479 return (initialStates);
1480} /* end of ComputeInitialStates */
1481
1482
1483/**Function********************************************************************
1484
1485 Synopsis [Checks if the reachable states are contained in each
1486 element of an array of invariants.]
1487
1488 Description [Checks if the reachable states are contained in each
1489 element of an array of invariants. Returns 0 as soon as a violation
1490 is found.]
1491
1492 SideEffects []
1493
1494******************************************************************************/
1495static int
1496CheckStatesContainedInInvariant(mdd_t *reachableStates,
1497 array_t *invarStates)
1498{
1499 int i;
1500 mdd_t *invariant;
1501
1502 arrayForEachItem(mdd_t *, invarStates, i, invariant) {
1503 if (invariant == NIL(mdd_t)) continue;
1504 if (!mdd_lequal(reachableStates, invariant, 1, 1)) {
1505 return 0;
1506 }
1507 }
1508 return 1;
1509}
1510
1511/**Function********************************************************************
1512
1513 Synopsis [Computes the reachable states, fromLowerBound and
1514 fromUpperBound for HD Traversal.]
1515
1516 Description [Computes the reachable states, fromLowerBound and
1517 fromUpperBound for HD Traversal. Updates all other arguments such as
1518 interiorStates, deadEndResidue . There are 3 major operations in
1519 this procedure. 1. Induce (if slow growth in reached) and compute a
1520 dead-end if necessary. 2. Compute the image of Reached if there is a
1521 big jump in its size. 3. Compute a dense subset of states to be used
1522 as a frontier in the next iteration.
1523
1524 1. A dead-end is the situation where no new states have been
1525 produced (fromLowerBound = 0), It is induced if the rate of growth
1526 of Reached is slow. If the image of the Entire Reached set has been
1527 computed in the previous iteration, then pretend this is a dead-end.
1528
1529 2. If the jump in Reached is large, compute its entire image to
1530 recover from fragmentation.
1531
1532 3. A dense subset of the frontier set is computed to be used as the
1533 frontier set in the next iteration. The update of reached is
1534 performed in this step (may not add scrap states if
1535 specified.). If a dead-end has just been performed, the new states
1536 are always added to Reached. Growth rate monitors are also
1537 updated. ]
1538
1539 SideEffects []
1540
1541******************************************************************************/
1542static void
1543HdComputeReachabilityParameters(mdd_manager *mddManager,
1544 Img_ImageInfo_t *imageInfo,
1545 mdd_t **reachableStates,
1546 mdd_t **fromUpperBound,
1547 mdd_t **fromLowerBound,
1548 mdd_t **image,
1549 FsmHdStruct_t *hdInfo,
1550 mdd_t *initialStates,
1551 array_t *mintermVarArray,
1552 int *depth,
1553 int printStep,
1554 int shellFlag,
1555 array_t *onionRings,
1556 int verbosityLevel)
1557{
1558 float growth;
1559 boolean scrapStates;
1560 int nvars = Fsm_FsmHdOptionReadNumVars(hdInfo->options);
1561 int oldSize;
1562 double oldMint;
1563 int sizeOfOnionRings = 0;
1564 if (shellFlag && onionRings) {
1565 sizeOfOnionRings = array_n(onionRings);
1566 }
1567
1568 verbosityLevel = (printStep && (((*depth) % printStep) == 0)) ? verbosityLevel : 0;
1569
1570 /* keep image if small, record size of the image */
1571 oldSize = FsmHdStatsReadSizeReached(hdInfo->stats);
1572 oldMint = FsmHdStatsReadMintermReached(hdInfo->stats);
1573 FsmHdStatsReset(hdInfo->stats, Fsm_Hd_Reached);
1574 FsmHdStatsReset(hdInfo->stats, Fsm_Hd_FromSubset);
1575 FsmHdStatsReset(hdInfo->stats, Fsm_Hd_From);
1576
1577 scrapStates = Fsm_FsmHdOptionReadScrapStates(hdInfo->options);
1578 hdInfo->onlyPartialImage = Fsm_FsmHdOptionReadOnlyPartialImage(hdInfo->options);
1579
1580 /* Step 1: Check comments at the top of this function */
1581 /* Check if this is a dead end */
1582 /* if growth rate of reached is really small, induce a dead-end */
1583 hdInfo->deadEndComputation = FALSE;
1584 if ((hdInfo->imageOfReachedComputed) ||
1585 (mdd_is_tautology(*fromLowerBound, 0)) ||
1586 (hdInfo->slowGrowth >= 5)) {
1587 /*
1588 * if image of reached is computed, add to the dead states.
1589 * Set dead-end computation flag and add all new states to Reached.
1590 */
1591
1592 /* add to interior states */
1593 hdInfo->interiorStates = AddStates(hdInfo->interiorStates,
1594 hdInfo->interiorStateCandidate,
1595 FSM_MDD_FREE, FSM_MDD_FREE);
1596 hdInfo->interiorStateCandidate = NIL(mdd_t);
1597 if ((verbosityLevel >= 2) && (hdInfo->interiorStates != NIL(mdd_t))) {
1598 fprintf(vis_stdout, "Interior states added, Size = %d, Minterms = %g\n",
1599 mdd_size(hdInfo->interiorStates), mdd_count_onset(mddManager,
1600 hdInfo->interiorStates, mintermVarArray));
1601 }
1602
1603 hdInfo->deadEndComputation = TRUE;
1604 hdInfo->firstSubset = FALSE;
1605 hdInfo->slowGrowth = 0;
1606 hdInfo->lastIter = *depth;
1607
1608 if (!hdInfo->imageOfReachedComputed) {
1609 /* Either slow growth or real dead-end */
1610 if (verbosityLevel >= 2) {
1611 if (!mdd_is_tautology(*fromLowerBound, 0))
1612 fprintf(vis_stdout, "Dead-End triggered by slow growth\n");
1613 /* record number of dead ends */
1614 (hdInfo->numDeadEnds)++;
1615 fprintf(vis_stdout, "Dead-End %d at %g seconds\n", hdInfo->numDeadEnds,
1616 (util_cpu_time()/1000.0));
1617 }
1618
1619 /* add another onion ring. */
1620 if (shellFlag && onionRings && !mdd_is_tautology(*fromLowerBound, 0)) {
1621 mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0);
1622 if (!mdd_is_tautology(temp, 0))
1623 array_insert_last(mdd_t *, onionRings, temp);
1624 else
1625 mdd_free(temp);
1626 }
1627 *reachableStates = AddStates(*fromLowerBound, *reachableStates,
1628 FSM_MDD_FREE, FSM_MDD_FREE);
1629 *fromUpperBound = *reachableStates;
1630
1631 /* perform a dead-end computation */
1632 *fromLowerBound = FsmHdDeadEnd(mddManager, imageInfo, *reachableStates,
1633 hdInfo,
1634 mintermVarArray,
1635 FSM_HD_GREEDY, verbosityLevel);
1636
1637 (*depth)++;
1638 }
1639 } /* end of if dead-end computation */
1640
1641 /* Step 2: Check comments at the top of this function */
1642 if (!mdd_is_tautology(*fromLowerBound, 0)) {
1643 /* add another onion ring. */
1644 if (shellFlag && onionRings) {
1645 mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0);
1646 if (!mdd_is_tautology(temp, 0))
1647 array_insert_last(mdd_t *, onionRings, temp);
1648 else
1649 mdd_free(temp);
1650 }
1651 /* compute reachable states with new states */
1652 *fromUpperBound = *reachableStates;
1653 *reachableStates = mdd_or(*fromLowerBound, *fromUpperBound, 1, 1);
1654 FsmHdStatsComputeSizeAndMinterms(mddManager, *reachableStates,
1655 mintermVarArray, nvars,
1656 Fsm_Hd_Reached, hdInfo->stats);
1657
1658
1659 /*
1660 * induce a full dead-end computation if jump in size of Reached is
1661 * large. But when the image of Reached has been computed or a dead-end
1662 * computation was just done, this is not done because deadEndComputation
1663 * has been set to 1.
1664 */
1665 HdInduceFullDeadEndIfNecessary(mddManager, imageInfo, fromLowerBound,
1666 fromUpperBound, reachableStates, image,
1667 hdInfo, depth, shellFlag, onionRings,
1668 mintermVarArray, oldSize,
1669 oldMint, verbosityLevel);
1670 } /* end of if (!mdd_is_tautology(fromLowerBound, 0)) */
1671
1672 /* Step 3: Check comments at the top of this function */
1673 /* Create subset if necessary */
1674 if (!mdd_is_tautology(*fromLowerBound, 0)) {
1675 if (!hdInfo->onlyPartialImage) {
1676 mdd_t *newStates;
1677 /*
1678 * Now fromUpperBound has the old reached states, reachableStates
1679 * has the new set of states.
1680 */
1681 newStates = mdd_dup(*fromLowerBound);
1682 FsmHdFromComputeDenseSubset(mddManager, fromLowerBound,
1683 fromUpperBound, reachableStates,
1684 image, initialStates, hdInfo,
1685 shellFlag, onionRings, sizeOfOnionRings,
1686 mintermVarArray);
1687
1688 /* if all new states are chosen from the previous iteration and
1689 * all these states have been added then add to interior states.
1690 * All new states are sometimes not added when
1691 * hdInfo->options->scrapStates is 0. Dead-end computations need not be
1692 * considered here since the interior states were already added then.
1693 */
1694 if ((hdInfo->interiorStateCandidate != NIL(mdd_t)) &&
1695 ((mdd_lequal(newStates, *fromLowerBound, 1, 1)) ||
1696 (scrapStates == TRUE))) {
1697 hdInfo->interiorStates = AddStates(hdInfo->interiorStates, hdInfo->interiorStateCandidate,
1698 FSM_MDD_FREE, FSM_MDD_FREE);
1699 hdInfo->interiorStateCandidate = NIL(mdd_t);
1700 if (verbosityLevel >= 2) {
1701 fprintf(vis_stdout,
1702 "Interior states added, Size = %d, Minterms = %g\n",
1703 mdd_size(hdInfo->interiorStates),
1704 mdd_count_onset(mddManager, hdInfo->interiorStates,
1705 mintermVarArray));
1706 }
1707 }
1708 mdd_free(newStates);
1709
1710 /* end of if fromLowerbound == 0 && subset Flag*/
1711 } else {
1712 mdd_free(*fromUpperBound);
1713 if (printStep && ((*depth) % printStep == 0)) {
1714 FsmHdStatsComputeSizeAndMinterms(mddManager, *fromLowerBound,
1715 mintermVarArray, nvars, Fsm_Hd_From, hdInfo->stats);
1716 FsmHdStatsSetMintermFromSubset(hdInfo->stats, 0.0);
1717 FsmHdStatsSetSizeFromSubset(hdInfo->stats, 0);
1718 }
1719 *fromUpperBound = *reachableStates;
1720 }
1721 } /* end of if fromLowerBound == 0 */
1722 if (hdInfo->interiorStateCandidate != NIL(mdd_t)) {
1723 mdd_free(hdInfo->interiorStateCandidate);
1724 hdInfo->interiorStateCandidate = NIL(mdd_t);
1725 }
1726
1727 /* monitor growth rate of reached, record if slow growth in consecutive
1728 * iterations
1729 */
1730 if (!mdd_is_tautology(*fromLowerBound, 0)) {
1731 FsmHdStatsComputeSizeAndMinterms(mddManager, *reachableStates,
1732 mintermVarArray, nvars, Fsm_Hd_Reached, hdInfo->stats);
1733 growth = (float)(FsmHdStatsReadMintermReached(hdInfo->stats) - oldMint)/
1734 (float)oldMint;
1735 if ((growth < FSM_HD_GROWTH_RATE) &&
1736 (((hdInfo->slowGrowth) && ((*depth) == (hdInfo->lastIter) + 1)) || (!(hdInfo->slowGrowth)))) {
1737 if (verbosityLevel >= 2) {
1738 fprintf(vis_stdout, "Growth rate = %f\n", growth);
1739 }
1740 (hdInfo->slowGrowth)++;
1741 hdInfo->lastIter = *depth;
1742 } else {
1743 /* reset value */
1744 hdInfo->slowGrowth = 0;
1745 }
1746 }
1747 return;
1748} /* end of HdComputeReachabilityParameters */
1749
1750/**Function********************************************************************
1751
1752 Synopsis [Initializes parameters for incremental computation.]
1753
1754 Description [Initializes parameters for incremental computation.
1755 Instantiates arrayOfRoots and tableOfLeafs, and returns the number of latches
1756 in the sytstem. Upon return, arrayOfRoots is an array of Ntk_Node_t *, and
1757 tableOfLeaves is an st_table of Ntk_Node_t *.]
1758
1759 SideEffects []
1760
1761******************************************************************************/
1762static int
1763InitializeIncrementalParameters(
1764 Fsm_Fsm_t *fsm,
1765 Ntk_Network_t *network,
1766 array_t **arrayOfRoots,
1767 st_table **tableOfLeaves)
1768{
1769 int numLatch;
1770 Ntk_Node_t *node;
1771 lsGen gen;
1772 int i, mddId; /* iterate over the nextStateVars of the fsm */
1773
1774 numLatch = Ntk_NetworkReadNumLatches(network);
1775
1776 /* This changed to fix a bug. Instead of reading the roots using
1777 Ntk_NetworkForEachCombOutput, we now get them from
1778 fsm->fsdData.nextStateVars, which means that the order is consistent with
1779 the latter field, as required later on in the incremental reachability
1780 code
1781
1782 old code:
1783 *arrayOfRoots = array_alloc(Ntk_Node_t *, numLatch);
1784 Ntk_NetworkForEachCombOutput(network, gen, node) {
1785 if(Ntk_NodeTestIsLatchDataInput(node)){
1786 array_insert_last(Ntk_Node_t *, *arrayOfRoots, node);
1787 }
1788 }
1789 */
1790
1791 assert(numLatch == array_n(fsm->fsmData.nextStateVars));
1792 *arrayOfRoots = array_alloc(Ntk_Node_t *, numLatch);
1793
1794 arrayForEachItem(int, fsm->fsmData.nextStateVars, i, mddId){
1795 Ntk_Node_t *shadow;
1796 Ntk_Node_t *latch;
1797 Ntk_Node_t *dataInput;
1798
1799 shadow = Ntk_NetworkFindNodeByMddId(network, mddId);
1800 assert(Ntk_NodeTestIsShadow(shadow));
1801 latch = Ntk_ShadowReadOrigin(shadow);
1802 assert(Ntk_NodeTestIsLatch(latch));
1803 dataInput = Ntk_LatchReadDataInput(latch);
1804 assert(dataInput != NIL(Ntk_Node_t));
1805
1806 array_insert(Ntk_Node_t *, *arrayOfRoots, i, dataInput);
1807 }
1808
1809 *tableOfLeaves = st_init_table(st_ptrcmp, st_ptrhash);
1810 Ntk_NetworkForEachCombInput(network, gen, node) {
1811 st_insert(*tableOfLeaves, (char *)node, (char *) (long) (-1) );
1812 }
1813 return (numLatch);
1814}
1815
1816
1817/**Function********************************************************************
1818
1819 Synopsis [Computes image for incremental computation.]
1820
1821 Description [Computes image for incremental computation.]
1822
1823 SideEffects []
1824
1825******************************************************************************/
1826static mdd_t *
1827IncrementalImageCompute(Ntk_Network_t *network,
1828 Fsm_Fsm_t *fsm,
1829 mdd_manager *mddManager,
1830 mdd_t *fromLowerBound,
1831 mdd_t *fromUpperBound,
1832 mdd_t *toCareSet,
1833 array_t *arrayOfRoots,
1834 st_table *tableOfLeaves,
1835 array_t *smoothVarArray,
1836 array_t *relationArray,
1837 int numLatch)
1838{
1839 Mvf_Function_t *function;
1840 mdd_t *relation, *optimizedRelation, *toCareSetRV, *imageRV;
1841 mdd_t *subOptimizedRelation, *image;
1842 int mddId, i;
1843 array_t *arrayOfMvf;
1844 mdd_t *frontierSet;
1845
1846 frontierSet = bdd_between(fromLowerBound, fromUpperBound);
1847 /* Create the array of transition relations */
1848 toCareSetRV = mdd_substitute(mddManager, toCareSet,
1849 fsm->fsmData.presentStateVars,
1850 fsm->fsmData.nextStateVars);
1851
1852 arrayOfMvf = Ntm_NetworkBuildMvfs(network, arrayOfRoots,
1853 tableOfLeaves, frontierSet);
1854 for (i=0; i < numLatch; i++){
1855 function = array_fetch(Mvf_Function_t *, arrayOfMvf, i);
1856 mddId = array_fetch(int, fsm->fsmData.nextStateVars, i);
1857 /* Since both arrayOfMvf and fsmData have been obtained from */
1858 /* the same generator */
1859 relation = Mvf_FunctionBuildRelationWithVariable(function,
1860 mddId);
1861 subOptimizedRelation = bdd_cofactor(relation, toCareSetRV);
1862 mdd_free(relation);
1863 optimizedRelation = bdd_cofactor(subOptimizedRelation, frontierSet);
1864 mdd_free(subOptimizedRelation);
1865 array_insert(mdd_t *, relationArray, i, optimizedRelation);
1866 }
1867 Mvf_FunctionArrayFree(arrayOfMvf);
1868 mdd_free(toCareSetRV);
1869 array_insert(mdd_t *, relationArray, numLatch, frontierSet);
1870 imageRV = Fsm_MddMultiwayAndSmooth(mddManager, relationArray,
1871 smoothVarArray);
1872 /*
1873 ** The above call can be substituted by more sophisticated
1874 ** Img_MultiwayLinearAndSmooth. However, that will have its
1875 ** associated overhead, and could offset any advantage. We
1876 ** expect that individual transition relation relations should
1877 ** be small and monolithic way to handle them would be ok.
1878 ** However, a good strategy would be find the quantification
1879 ** schedule which does not change with the computation of
1880 ** incremental transition relations.
1881 */
1882 for (i = 0; i <= numLatch; i++){
1883 mdd_free(array_fetch(mdd_t*, relationArray, i));
1884 }
1885 assert(CheckImageValidity(mddManager, imageRV,
1886 fsm->fsmData.presentStateVars,
1887 fsm->fsmData.inputVars));
1888 image = mdd_substitute(mddManager, imageRV,
1889 fsm->fsmData.nextStateVars,
1890 fsm->fsmData.presentStateVars);
1891 mdd_free(imageRV);
1892 assert(CheckImageValidity(mddManager, image,
1893 fsm->fsmData.nextStateVars,
1894 fsm->fsmData.inputVars));
1895 return image;
1896}
1897
1898/**Function********************************************************************
1899
1900 Synopsis [Prints information about onion rings]
1901
1902 Description [Prints information about onion rings.]
1903
1904 SideEffects []
1905
1906******************************************************************************/
1907static void
1908PrintOnionRings(Fsm_Fsm_t *fsm, int printStep,
1909 Fsm_RchType_t approxFlag, int nvars)
1910{
1911 int i;
1912 mdd_t *reachableStates;
1913 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
1914 array_t *mintermVarArray = Fsm_FsmReadPresentStateVars(fsm);
1915
1916 fprintf(vis_stdout, "** rch warning: Not possible to compute size of reachable states at every iteration\n");
1917 if (Fsm_FsmReadReachabilityOnionRings(fsm) != NIL(array_t)) {
1918 arrayForEachItem(mdd_t *, Fsm_FsmReadReachabilityOnionRings(fsm),
1919 i, reachableStates) {
1920 if (printStep && (i % printStep == 0)) {
1921 if (approxFlag != Fsm_Rch_Hd_c) {
1922 if (nvars <= 1023) {
1923 (void)fprintf(vis_stdout, "BFS step = %d\t|onion ring states| = %8g",
1924 i, mdd_count_onset(mddManager, reachableStates,
1925 mintermVarArray));
1926 if (i != array_n(Fsm_FsmReadReachabilityOnionRings(fsm))-1) {
1927 fprintf(vis_stdout, "\n");
1928 } else {
1929 fprintf(vis_stdout, "\tSize = %d\n", mdd_size(reachableStates));
1930 }
1931
1932 } else {
1933 (void)fprintf(vis_stdout, "BFS step = %d\t|onion ring states| = ",
1934 i);
1935 (void) bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6);
1936 if (i != array_n(Fsm_FsmReadReachabilityOnionRings(fsm))-1) {
1937 fprintf(vis_stdout, "Final Size = %d\n", mdd_size(reachableStates));
1938 }
1939 }
1940 } else {
1941
1942 if (nvars <= 1023) {
1943 (void)fprintf(vis_stdout, "Step = %d\t|onion ring states| = %8g",
1944 i, mdd_count_onset(mddManager, reachableStates,
1945 mintermVarArray));
1946 if (i != array_n(Fsm_FsmReadReachabilityOnionRings(fsm))-1) {
1947 fprintf(vis_stdout, "\n");
1948 } else {
1949 fprintf(vis_stdout, "\tSize = %d\n", mdd_size(reachableStates));
1950 }
1951 } else {
1952 (void)fprintf(vis_stdout, "Step = %d\t|onion ring states| = ",
1953 i);
1954 (void) bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6);
1955 if (i != array_n(Fsm_FsmReadReachabilityOnionRings(fsm))-1) {
1956 fprintf(vis_stdout, "Final Size = %d\n", mdd_size(reachableStates));
1957 }
1958 }
1959 }
1960 }
1961 }
1962 }
1963 return;
1964}/* printonionrings */
1965
1966/**Function********************************************************************
1967
1968 Synopsis [Reads in a sequence of integers separated by commas and
1969 stores them in an array.]
1970
1971 Description [Reads in a sequence of integers separated by commas from the
1972 environment variable guided_search_sequence. It stores them in an array that
1973 it returns. Alpha characters and 0 integers are replaced by
1974 -1. Pads the remaining entries corresponding to the guide array with -1.
1975 Every number indicates the number of times the corresponding (in sequence)
1976 hint should be used. The value -1 means `to convergence'.]
1977
1978
1979 SideEffects []
1980
1981******************************************************************************/
1982static array_t *
1983GenerateGuidedSearchSequenceArray(array_t *guideArray)
1984{
1985 char *seqStr = Cmd_FlagReadByName("guided_search_sequence");
1986 char *preStr;
1987 int intEntry;
1988 array_t *depthArray = array_alloc(int, 0);
1989 int i;
1990
1991 /* Skip parsing if we have no guided search sequence */
1992 if (seqStr != NIL(char) && strcmp(seqStr, "") != 0){
1993 preStr = strtok(seqStr, ",");
1994
1995 while(preStr != NIL(char)){
1996 intEntry = strtol(preStr, (char **) NULL, 10);
1997 array_insert_last(int, depthArray, (intEntry == 0 ? -1 : intEntry));
1998 preStr = strtok(NIL(char), ",");
1999 }
2000 }
2001
2002 if(array_n(depthArray) > array_n(guideArray)){
2003 fprintf(vis_stdout, "** rch warning: guided_search_sequence has more entries\n");
2004 fprintf(vis_stdout,"than there are hints. Extra entires will be ignored\n");
2005 }
2006
2007 /* pad with -1s */
2008 for (i = array_n(depthArray); i < array_n(guideArray); i++) {
2009 array_insert_last(int, depthArray, -1);
2010 }
2011
2012 assert(array_n(depthArray) >= array_n(guideArray));
2013
2014 return depthArray;
2015}
2016
2017
2018/**Function********************************************************************
2019
2020 Synopsis [Computes the reachable states, frontier and fromUpperBound.]
2021
2022 Description [Computes the reachable states, frontier and
2023 fromUpperBound. For HD it also generates interior states, interior
2024 state candidates, dead-end residue, number of dead-ends, residue
2025 count, etc. For guided search, this procedure also generates a
2026 dead-end if the frontier is 0. Also this procedure keeps track of
2027 convergence and whether a dead-end is required at the end.]
2028
2029 SideEffects [All arguments are updated.]
2030
2031 SeeAlso [HdComputeReachabilityParameters FsmHdDeadEnd]
2032
2033******************************************************************************/
2034static void
2035ComputeReachabilityParameters(mdd_manager *mddManager,
2036 Img_ImageInfo_t *imageInfo,
2037 Fsm_RchType_t approxFlag,
2038 mdd_t **reachableStates,
2039 mdd_t **fromUpperBound,
2040 mdd_t **fromLowerBound,
2041 mdd_t **image,
2042 FsmHdStruct_t *hdInfo,
2043 mdd_t *initialStates,
2044 array_t *mintermVarArray,
2045 int *depth,
2046 int printStep,
2047 int shellFlag,
2048 array_t *onionRings,
2049 int verbosityLevel,
2050 boolean guidedSearchMode,
2051 mdd_t *hint,
2052 int *hintDepth,
2053 boolean *notConverged)
2054{
2055 if (approxFlag == Fsm_Rch_Bfs_c) {
2056 /* New set of reachable states is old set plus new states in image. */
2057 *reachableStates = AddStates(*fromLowerBound, *reachableStates,
2058 FSM_MDD_DONT_FREE, FSM_MDD_FREE);
2059 *fromUpperBound = *reachableStates;
2060
2061 /* in guided search, if the mode is to convergence or the
2062 limited depth has not been reached, and the frontier is empty,
2063 then generate a frontier in BFS mode (that is a full dead-end). */
2064 if (guidedSearchMode &&
2065 mdd_is_tautology(*fromLowerBound, 0) /* no frontier */ &&
2066 (hdInfo->deadEndWithOriginalTR == FALSE) /* and guided search */ ) {
2067 assert(imageInfo != NIL(Img_ImageInfo_t));
2068 if (*hintDepth != 0) {
2069 /* add another onion ring. */
2070 if (shellFlag && onionRings) {
2071 mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0);
2072 if (!mdd_is_tautology(temp, 0))
2073 array_insert_last(mdd_t *, onionRings, temp);
2074 else
2075 mdd_free(temp);
2076 }
2077 /* do a full dead-end (non-greedy), compute all the frontier states */
2078 mdd_free(*fromLowerBound);
2079 *fromLowerBound = FsmHdDeadEnd(mddManager, imageInfo, *reachableStates,
2080 hdInfo,
2081 mintermVarArray,
2082 FSM_HD_NONGREEDY, verbosityLevel);
2083 mdd_free(hdInfo->interiorStates);
2084 hdInfo->interiorStates = NIL(mdd_t);
2085 *reachableStates = AddStates(*fromLowerBound, *reachableStates,
2086 FSM_MDD_DONT_FREE, FSM_MDD_FREE);
2087 *fromUpperBound = *reachableStates;
2088 (*hintDepth)--;
2089 (*depth)++;
2090 if (mdd_is_tautology(hint, 1)) hdInfo->deadEndWithOriginalTR = TRUE;
2091 } else {
2092 *notConverged = TRUE;
2093 /* set this flag for correct detection of convergence
2094 Corner case: when limited depth and frontier = 0 */
2095 }
2096 }
2097 } else if (approxFlag == Fsm_Rch_Hd_c) {
2098 assert(imageInfo != NIL(Img_ImageInfo_t));
2099 if (!guidedSearchMode || (*hintDepth != 0)) {
2100 /* computes reachable states, fromLowerBound and fromUpperBound.
2101 * Updates all other quantities such as interiorStates,
2102 * deadEndResidue. */
2103 HdComputeReachabilityParameters(mddManager, imageInfo,
2104 reachableStates,
2105 fromUpperBound,
2106 fromLowerBound,
2107 image,
2108 hdInfo,
2109 initialStates,
2110 mintermVarArray,
2111 depth, printStep,
2112 shellFlag, onionRings,
2113 verbosityLevel);
2114 if (guidedSearchMode) (*hintDepth)--;
2115
2116 } else { /* guidedSearchMode and hint depth is 0 */
2117 if (mdd_is_tautology(*fromLowerBound, 0)) {
2118 *notConverged = TRUE;
2119 /* set this flag for correct detection of convergence
2120 Corner case: when limited depth and frontier = 0 */
2121 }
2122 /* add another onion ring. */
2123 if (shellFlag && onionRings) {
2124 mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0);
2125 if (!mdd_is_tautology(temp, 0))
2126 array_insert_last(mdd_t *, onionRings, temp);
2127 else
2128 mdd_free(temp);
2129 }
2130
2131 }
2132 }
2133 return;
2134} /* End of ComputeReachabilityParameters */
Note: See TracBrowser for help on using the repository browser.