source: vis_dev/vis-2.3/src/abs/absInternal.c @ 36

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

vis2.3
File size: 41.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [absInternal.c]
4
5  PackageName [abs]
6
7  Synopsis    [Miscelaneous functions to handle caches, don't care conditions, initialization and deallocation of structures, etc]
8
9  Author      [Abelardo Pardo <abel@vlsi.colorado.edu>]
10
11  Copyright [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14
15******************************************************************************/
16
17#include "absInt.h"
18
19static char rcsid[] UNUSED = "$Id: absInternal.c,v 1.30 2005/04/16 04:22:21 fabio Exp $";
20
21
22/*---------------------------------------------------------------------------*/
23/* Macro declarations                                                        */
24/*---------------------------------------------------------------------------*/
25
26/*---------------------------------------------------------------------------*/
27/* Variable declarations                                                     */
28/*---------------------------------------------------------------------------*/
29static int vertexCounter = 0;
30
31/**AutomaticStart*************************************************************/
32
33/*---------------------------------------------------------------------------*/
34/* Static function prototypes                                                */
35/*---------------------------------------------------------------------------*/
36
37static mdd_t * ComputeEGtrue(Abs_VerificationInfo_t *absInfo, mdd_t *careStates);
38static void SelectIdentifierVertices(AbsVertexInfo_t *vertexPtr, array_t *result, st_table *visited);
39
40/**AutomaticEnd***************************************************************/
41
42
43/*---------------------------------------------------------------------------*/
44/* Definition of exported functions                                          */
45/*---------------------------------------------------------------------------*/
46
47/**Function********************************************************************
48
49  Synopsis [Fill the fields of the data structure storing the information
50  required for the verification process]
51
52  SideEffects        []
53
54******************************************************************************/
55Abs_VerificationInfo_t *
56Abs_VerificationComputeInfo(
57  Ntk_Network_t *network)
58{
59  Abs_VerificationInfo_t *absInfo;
60  Ntk_Node_t            *nodePtr;
61  graph_t               *partition;
62  mdd_manager           *mddManager;
63  st_table              *table;
64  lsGen                 lsgen;
65
66
67  /* Create the data structure to store all the needed info */
68  absInfo = AbsVerificationInfoInitialize();
69
70  /* Fill the data structure in */
71  AbsVerificationInfoSetNetwork(absInfo, network);
72  partition = Part_NetworkReadPartition(network);
73  AbsVerificationInfoSetPartition(absInfo, partition);
74  mddManager = Part_PartitionReadMddManager(partition);
75  AbsVerificationInfoSetMddManager(absInfo, mddManager);
76 
77  /* Compute the state variable pairs */
78  table = st_init_table(st_numcmp, st_numhash);
79  Ntk_NetworkForEachLatch(network, lsgen, nodePtr) {
80    Ntk_Node_t *latchInputPtr;
81    int        mddId, mddId2;
82   
83    mddId = Ntk_NodeReadMddId(nodePtr);
84    latchInputPtr = Ntk_NodeReadShadow(nodePtr);
85    mddId2 = Ntk_NodeReadMddId(latchInputPtr);
86    st_insert(table, (char *)(long)mddId, (char *)(long)mddId2);
87  }
88  AbsVerificationInfoSetStateVars(absInfo, table);
89 
90  /* Compute the quantify variables */
91  table = st_init_table(st_numcmp, st_numhash);
92  Ntk_NetworkForEachInput(network, lsgen, nodePtr) {
93    int mddId;
94   
95    mddId = Ntk_NodeReadMddId(nodePtr);
96    st_insert(table, (char *)(long)mddId, NIL(char));
97  }
98  AbsVerificationInfoSetQuantifyVars(absInfo, table);
99 
100  /* Initalize the catalog to detect common expressions */
101  AbsVerificationInfoSetCatalog(absInfo, AbsVertexCatalogInitialize());
102 
103  return absInfo;
104} /* End of Abs_VerificationComputeInfo */
105
106
107/*---------------------------------------------------------------------------*/
108/* Definition of internal functions                                          */
109/*---------------------------------------------------------------------------*/
110
111/**Function********************************************************************
112
113  Synopsis [Create a new structure of type VertexInfo and initialize
114  all its fields.]
115
116  SideEffects        []
117
118  SeeAlso            [AbsVertexInfo_t]
119
120******************************************************************************/
121AbsVertexInfo_t *
122AbsVertexInitialize(void)
123{
124  AbsVertexInfo_t *result;
125
126  result = ALLOC(AbsVertexInfo_t, 1);
127
128  AbsVertexSetType(result, false_c);
129  AbsVertexSetId(result, vertexCounter++);
130  AbsVertexSetSat(result, NIL(mdd_t));
131  AbsVertexSetRefs(result, 1);
132  AbsVertexSetServed(result, 0);
133  AbsVertexSetPolarity(result, FALSE);
134  AbsVertexSetDepth(result, -1);
135  AbsVertexSetLocalApprox(result, FALSE);
136  AbsVertexSetGlobalApprox(result, FALSE);
137  AbsVertexSetConstant(result, FALSE);
138  AbsVertexSetTrueRefine(result, FALSE);
139  AbsVertexSetLeftKid(result, NIL(AbsVertexInfo_t));
140  AbsVertexSetRightKid(result, NIL(AbsVertexInfo_t));
141  result->parent = lsCreate();
142 
143  /* Not all of these need to be initialized, but to be sure... */
144  AbsVertexSetSolutions(result, NIL(st_table));
145  AbsVertexSetVarId(result, 0);
146  AbsVertexSetFpVar(result, NIL(AbsVertexInfo_t));
147  AbsVertexSetVarId(result, 0);
148  AbsVertexSetGoalSet(result, NIL(mdd_t));
149  AbsVertexSetRings(result, NIL(array_t));
150  AbsVertexSetRingApprox(result, NIL(array_t));
151  AbsVertexSetSubApprox(result, NIL(array_t));
152  AbsVertexSetUseExtraCareSet(result, FALSE);
153  AbsVertexSetName(result, NIL(char));
154  AbsVertexSetValue(result, NIL(char));
155
156  return result;
157} /* End of AbsVertexInitialize */
158
159/**Function********************************************************************
160
161  Synopsis           [Free a structure of type AbsVertexInfo.]
162
163  Description        [optional]
164
165  SideEffects        []
166
167  SeeAlso            [AbsVertexInfo_t]
168
169******************************************************************************/
170void
171AbsVertexFree(
172  AbsVertexCatalog_t *catalog,
173  AbsVertexInfo_t *v,
174  AbsVertexInfo_t *fromVertex)
175{
176  /* Decrement the number of references */
177  AbsVertexReadRefs(v)--;
178
179  /* Remove the pointer from its parent to itself */
180  if (fromVertex != NIL(AbsVertexInfo_t)) {
181    AbsVertexInfo_t *result;
182    lsGen listGen;
183    lsHandle item, toDelete;
184    lsGeneric userData;
185
186    listGen = lsStart(AbsVertexReadParent(v));
187    toDelete = (lsHandle) 0;
188    while(toDelete == (lsHandle) 0 &&
189          lsNext(listGen, &result, &item) == LS_OK) {
190      if (result == fromVertex) {
191        toDelete = item;
192      }
193    }
194    lsFinish(listGen);
195
196    if (toDelete != (lsHandle)0) {
197      lsRemoveItem(toDelete, &userData);
198    }
199  }
200
201  /* If it is not the last reference we are done */
202  if (AbsVertexReadRefs(v) != 0) {
203    return;
204  }
205
206  /* Vertices that need recursion over the leftKid */
207  if (AbsVertexReadType(v) == fixedPoint_c ||
208      AbsVertexReadType(v) == and_c ||
209      AbsVertexReadType(v) == xor_c ||
210      AbsVertexReadType(v) == xnor_c ||
211      AbsVertexReadType(v) == not_c ||
212      AbsVertexReadType(v) == preImage_c) {
213    AbsVertexFree(catalog, AbsVertexReadLeftKid(v), v);
214  }
215 
216  /* Vertices that need recursion over the rightKid */
217  if (AbsVertexReadType(v) == and_c ||
218      AbsVertexReadType(v) == xor_c ||
219      AbsVertexReadType(v) == xnor_c) {
220    AbsVertexFree(catalog, AbsVertexReadRightKid(v), v);
221  }
222
223  /* Remove the vertex from the catalog */
224  AbsCatalogDelete(catalog, v);
225
226  /* The variable vertex does not reference the sat set */
227  if (AbsVertexReadType(v) != variable_c && 
228      AbsVertexReadSat(v) != NIL(mdd_t)) {
229    mdd_free(AbsVertexReadSat(v));
230  }
231
232  if (AbsVertexReadType(v) == variable_c && 
233      AbsVertexReadGoalSet(v) != NIL(mdd_t)) {
234    mdd_free(AbsVertexReadGoalSet(v));
235  }
236 
237  lsDestroy(AbsVertexReadParent(v), (void (*)(lsGeneric))0);
238
239  /* Free the union fields depending on the type of vertex */
240  if (AbsVertexReadType(v) == preImage_c) {
241    if (AbsVertexReadSolutions(v) != NIL(st_table)) {
242      AbsEvalCacheEntry_t *value;
243      bdd_node            *key;
244      st_generator        *stgen;
245
246      st_foreach_item(AbsVertexReadSolutions(v), stgen, &key, &value) {
247        AbsCacheEntryFree(value);
248      }
249      st_free_table(AbsVertexReadSolutions(v));
250    }
251  }
252  else if (AbsVertexReadType(v) == fixedPoint_c) {
253    if (AbsVertexReadRings(v) != NIL(array_t)) {
254      mdd_t *unit;
255      int i;
256
257      arrayForEachItem(mdd_t *, AbsVertexReadRings(v), i, unit) {
258        mdd_free(unit);
259      }
260      array_free(AbsVertexReadRings(v));
261    }
262    if (AbsVertexReadRingApprox(v) != NIL(array_t)) {
263      array_free(AbsVertexReadRingApprox(v));
264    }
265    if (AbsVertexReadSubApprox(v) != NIL(array_t)) {
266      array_free(AbsVertexReadSubApprox(v));
267    }
268  }
269  else if (AbsVertexReadType(v) == identifier_c) {
270    FREE(AbsVertexReadName(v));
271    FREE(AbsVertexReadValue(v));
272  }
273
274  /* Deallocate the memory for the structure itself */
275  FREE(v);
276} /* End of AbsVertexFree */
277
278/**Function********************************************************************
279
280  Synopsis [Allocates the data structure to store information about
281  the general verification process.]
282
283  SideEffects        []
284
285  SeeAlso            [AbsVerificationInfo AbsVertexInfo]
286
287******************************************************************************/
288Abs_VerificationInfo_t *
289AbsVerificationInfoInitialize(void)
290{
291  Abs_VerificationInfo_t *result;
292
293  result = ALLOC(Abs_VerificationInfo_t, 1);
294
295  AbsVerificationInfoSetNetwork(result, NIL(Ntk_Network_t));
296  AbsVerificationInfoSetPartition(result, NIL(graph_t));
297  AbsVerificationInfoSetFsm(result, NIL(Fsm_Fsm_t));
298  AbsVerificationInfoSetNumStateVars(result, 0);
299  AbsVerificationInfoSetApproxFsm(result, NIL(Fsm_Fsm_t));
300  AbsVerificationInfoSetStateVars(result, NIL(st_table));
301  AbsVerificationInfoSetQuantifyVars(result, NIL(st_table));
302  AbsVerificationInfoSetCareSet(result, NIL(mdd_t));
303  AbsVerificationInfoSetTmpCareSet(result, NIL(mdd_t));
304  AbsVerificationInfoSetImageCache(result, NIL(st_table));
305  AbsVerificationInfoSetMddManager(result, NIL(mdd_manager));
306  AbsVerificationInfoSetCatalog(result, NIL(AbsVertexCatalog_t));
307  AbsVerificationInfoSetStats(result, AbsStatsInitialize());
308  AbsVerificationInfoSetOptions(result, NIL(AbsOptions_t));
309 
310  return result;
311} /* End of AbsVerificationInfoInitialize */
312
313/**Function********************************************************************
314
315  Synopsis           [Free the structure storing the verification info.]
316
317  Description [Some of the fields in this structure are owned by this
318  package and some others are simply pointers to a data structure that
319  is owned by some other package. Refer to the definition of
320  Abs_VerificationInfo_t to know which fields are onwed and which are
321  not.]
322
323  SideEffects        []
324
325  SeeAlso            [AbsVerificationInfo AbsVertexInfo]
326
327******************************************************************************/
328void
329AbsVerificationInfoFree(
330  Abs_VerificationInfo_t *v)
331{
332  if (AbsVerificationInfoReadStateVars(v) != NIL(st_table)) {
333    st_free_table(AbsVerificationInfoReadStateVars(v));
334  }
335
336  if (AbsVerificationInfoReadQuantifyVars(v) != NIL(st_table)) {
337    st_free_table(AbsVerificationInfoReadQuantifyVars(v));
338  }
339
340  if (AbsVerificationInfoReadImageCache(v) != NIL(st_table)) {
341    AbsEvalCacheEntry_t *value;
342    bdd_node            *key;
343    st_generator        *stgen;
344
345    st_foreach_item(AbsVerificationInfoReadImageCache(v), stgen,
346                    &key, &value) {
347      AbsCacheEntryFree(value);
348    }
349    st_free_table(AbsVerificationInfoReadImageCache(v));
350  }
351
352  if (AbsVerificationInfoReadCareSet(v) != NIL(mdd_t)) {
353    mdd_free(AbsVerificationInfoReadCareSet(v));
354  }
355
356  if (AbsVerificationInfoReadTmpCareSet(v) != NIL(mdd_t)) {
357    mdd_free(AbsVerificationInfoReadTmpCareSet(v));
358  }
359
360  if (AbsVerificationInfoReadCatalog(v) != NIL(AbsVertexCatalog_t)) {
361    AbsVertexCatalogFree(AbsVerificationInfoReadCatalog(v));
362  }
363
364  AbsStatsFree(AbsVerificationInfoReadStats(v));
365
366  FREE(v);
367
368  /*
369   * The options field is not freed since it is assumed that it has been
370   * allocated outside the AbsVerificationInitialize procedure
371   */
372
373  return;
374} /* End of AbsVerificationInfoFree */
375
376/**Function********************************************************************
377
378  Synopsis [Allocate the structure to store the value of the options.]
379
380  SideEffects        []
381
382  SeeAlso            [AbsOptions]
383
384******************************************************************************/
385AbsOptions_t *
386AbsOptionsInitialize(void)
387{
388  AbsOptions_t *result;
389
390  result = ALLOC(AbsOptions_t, 1);
391
392  AbsOptionsSetVerbosity(result, 0);
393  AbsOptionsSetTimeOut(result, 0);
394  AbsOptionsSetFileName(result, NIL(char));
395  AbsOptionsSetReachability(result, FALSE);
396  AbsOptionsSetFairFileName(result, NIL(char));
397  AbsOptionsSetExact(result, FALSE);
398  AbsOptionsSetPrintStats(result, FALSE);
399  AbsOptionsSetMinimizeIterate(result, FALSE);
400  AbsOptionsSetNegateFormula(result, FALSE);
401  AbsOptionsSetPartApprox(result, FALSE);
402
403  return result;
404} /* End of AbsOptionsInitialize */
405
406/**Function********************************************************************
407
408  Synopsis [Deallocate the structure storing the value of the options.]
409
410  SideEffects        []
411
412  SeeAlso            [AbsOptions]
413
414******************************************************************************/
415void
416AbsOptionsFree(AbsOptions_t *unit)
417{
418  if (AbsOptionsReadFileName(unit) != NIL(char)) {
419    FREE(AbsOptionsReadFileName(unit));
420  }
421 
422  if (AbsOptionsReadFairFileName(unit) != NIL(char)) {
423    FREE(AbsOptionsReadFairFileName(unit));
424  }
425
426  FREE(unit);
427 
428  return;
429} /* End of AbsOptionsInitialize */
430
431
432/**Function********************************************************************
433
434  Synopsis [Allocate the data structure storing the different statistics
435  measurements collected by the algorithms]
436
437  SideEffects        []
438
439  SeeAlso            [AbsStats]
440
441******************************************************************************/
442AbsStats_t *
443AbsStatsInitialize(void)
444{
445  AbsStats_t *result;
446
447  result = ALLOC(AbsStats_t, 1);
448 
449  AbsStatsSetNumReorderings(result, 0);
450  AbsStatsSetEvalFixedPoint(result, 0);
451  AbsStatsSetEvalAnd(result, 0);
452  AbsStatsSetEvalNot(result, 0);
453  AbsStatsSetEvalPreImage(result, 0);
454  AbsStatsSetEvalIdentifier(result, 0);
455  AbsStatsSetEvalVariable(result, 0);
456  AbsStatsSetRefineFixedPoint(result, 0);
457  AbsStatsSetRefineAnd(result, 0);
458  AbsStatsSetRefineNot(result, 0);
459  AbsStatsSetRefinePreImage(result, 0);
460  AbsStatsSetRefineIdentifier(result, 0);
461  AbsStatsSetRefineVariable(result, 0);
462  AbsStatsSetExactPreImage(result, 0);
463  AbsStatsSetApproxPreImage(result, 0);
464  AbsStatsSetExactImage(result, 0);
465  AbsStatsSetPreImageCacheEntries(result, 0);
466  AbsStatsSetImageCacheEntries(result, 0);
467  AbsStatsSetImageCpuTime(result, 0);
468  AbsStatsSetPreImageCpuTime(result, 0);
469  AbsStatsSetAppPreCpuTime(result, 0);
470
471  return result;
472
473} /* End of AbsStatsInitialize */
474
475/**Function********************************************************************
476
477  Synopsis           [Function to free the AbsStats structure]
478
479  SideEffects        []
480
481  SeeAlso            [AbsStats]
482
483******************************************************************************/
484void
485AbsStatsFree(
486  AbsStats_t *unit)
487{
488  FREE(unit);
489} /* End of AbsStatsFree */
490
491/**Function********************************************************************
492
493  Synopsis [Initalize the entry of the cache for previously computed results]
494
495  SideEffects        []
496
497  SeeAlso            [AbsEvalCacheEntry]
498
499******************************************************************************/
500AbsEvalCacheEntry_t *
501AbsCacheEntryInitialize(void)
502{
503  AbsEvalCacheEntry_t *result;
504
505  result = ALLOC(AbsEvalCacheEntry_t, 1);
506
507  AbsEvalCacheEntrySetKey(result, NIL(mdd_t));
508  AbsEvalCacheEntrySetApprox(result, FALSE);
509  AbsEvalCacheEntrySetComplement(result, 0);
510  AbsEvalCacheEntrySetResult(result, NIL(mdd_t));
511  AbsEvalCacheEntrySetCareSet(result, NIL(mdd_t));
512
513  return result;
514} /* End of AbsCacheEntryInitialize */
515
516/**Function********************************************************************
517
518  Synopsis           [Function to de-allocate the AbsEvalCacheEntry]
519
520  SideEffects        []
521
522  SeeAlso            [AbsEvalCacheEntry]
523
524******************************************************************************/
525void
526AbsCacheEntryFree(
527  AbsEvalCacheEntry_t *unit)
528{
529  mdd_free(AbsEvalCacheEntryReadKey(unit));
530  mdd_free(AbsEvalCacheEntryReadResult(unit));
531  mdd_free(AbsEvalCacheEntryReadCareSet(unit));
532
533  FREE(unit);
534} /* End of AbsCacheEntryFree */
535
536/**Function********************************************************************
537
538  Synopsis           [Insert an item in the evaluation cache]
539
540  SideEffects        []
541
542  SeeAlso            [AbsEvalCacheEntry]
543
544******************************************************************************/
545void
546AbsEvalCacheInsert(
547  st_table *solutions,
548  mdd_t *key,
549  mdd_t *result,
550  mdd_t *careSet,
551  boolean approx,
552  boolean replace)
553{
554  AbsEvalCacheEntry_t *entry;
555  int                 complement;
556  bdd_node            *f;
557
558  entry = NIL(AbsEvalCacheEntry_t);
559  f = bdd_get_node(key, &complement);
560
561  /* If the replacement is required, delete the element from the table */
562  if (replace) {
563    st_delete(solutions, &f, &entry);
564
565    mdd_free(AbsEvalCacheEntryReadKey(entry));
566    mdd_free(AbsEvalCacheEntryReadResult(entry));
567    mdd_free(AbsEvalCacheEntryReadCareSet(entry));
568  }
569
570  assert(!st_is_member(solutions, (char *)f));
571
572  if (entry == NIL(AbsEvalCacheEntry_t)) {
573    entry = AbsCacheEntryInitialize();
574  }
575
576  AbsEvalCacheEntrySetKey(entry, mdd_dup(key));
577  AbsEvalCacheEntrySetApprox(entry, approx);
578  AbsEvalCacheEntrySetComplement(entry, complement);
579  AbsEvalCacheEntrySetResult(entry, mdd_dup(result));
580  AbsEvalCacheEntrySetCareSet(entry, mdd_dup(careSet));
581 
582  /* Insert the new entry in the cache */
583  st_insert(solutions, (char *)f, (char *)entry);
584
585  return;
586} /* End of AbsEvalCacheInsert */
587
588/**Function********************************************************************
589
590  Synopsis           [Lookup a previous evaluation in the cache]
591
592  SideEffects        []
593
594  SeeAlso            [AbsEvalCacheEntry]
595
596******************************************************************************/
597boolean
598AbsEvalCacheLookup(
599  st_table *solutions,
600  mdd_t *key,
601  mdd_t *careSet,
602  boolean approx,
603  mdd_t **result,
604  boolean *storedApprox)
605{
606  AbsEvalCacheEntry_t *entry;
607  bdd_node            *f;
608  int                 complement;
609 
610  f = bdd_get_node(key, &complement);
611
612  if (st_lookup(solutions, f, &entry)) {
613    if (complement == AbsEvalCacheEntryReadComplement(entry) &&
614        (approx || !AbsEvalCacheEntryReadApprox(entry)) &&
615        mdd_lequal(careSet, AbsEvalCacheEntryReadCareSet(entry), 1, 1)) {
616      *result = AbsEvalCacheEntryReadResult(entry);
617      if (storedApprox != 0) {
618        *storedApprox = AbsEvalCacheEntryReadApprox(entry);
619      }
620      return TRUE;
621    }
622    else {
623      st_delete(solutions, &f, &entry);
624      AbsCacheEntryFree(entry);
625    }
626  }
627
628  return FALSE;
629} /* End of AbsEvalCacheLookup */
630
631/**Function********************************************************************
632
633  Synopsis           [Delete all the entries in the evaluation cache]
634
635  SideEffects        []
636
637  SeeAlso            [AbsEvalCacheEntry]
638
639******************************************************************************/
640void
641AbsVerificationFlushCache(
642  Abs_VerificationInfo_t *absInfo)
643{
644  AbsEvalCacheEntry_t *value;
645  st_table            *table;
646  bdd_node            *key;
647  st_generator        *stgen;
648
649  table = AbsVerificationInfoReadImageCache(absInfo);
650
651  if (table == NIL(st_table)) {
652    return;
653  }
654
655  st_foreach_item(table, stgen, &key, &value) {
656    AbsCacheEntryFree(value);
657  }
658
659  st_free_table(table);
660  AbsVerificationInfoSetImageCache(absInfo, NIL(st_table));
661
662  return;
663} /* End of AbsVerificationFlushCache */
664
665/**Function********************************************************************
666
667  Synopsis [Delete all the entries stored in the local evaluation cache that a
668  given vertex has attached to it]
669
670  SideEffects        []
671
672  SeeAlso            [AbsVertexInfo]
673
674******************************************************************************/
675void
676AbsVertexFlushCache(
677  AbsVertexInfo_t *vertexPtr)
678{
679  if (AbsVertexReadType(vertexPtr) == preImage_c) {
680    if (AbsVertexReadSolutions(vertexPtr) != NIL(st_table)) {
681      AbsEvalCacheEntry_t *value;
682      bdd_node            *key;
683      st_generator        *stgen;
684     
685      st_foreach_item(AbsVertexReadSolutions(vertexPtr), stgen, &key,
686                      &value) {
687        AbsCacheEntryFree(value);
688      }
689      st_free_table(AbsVertexReadSolutions(vertexPtr));
690      AbsVertexSetSolutions(vertexPtr, NIL(st_table));
691    }
692  }
693
694  if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
695    AbsVertexFlushCache(AbsVertexReadLeftKid(vertexPtr));
696  }
697
698  if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
699    AbsVertexFlushCache(AbsVertexReadRightKid(vertexPtr));
700  }
701
702  return;
703} /* End of AbsVertexFlushCache */
704
705/**Function********************************************************************
706
707  Synopsis [Read an image computation from the cache, and if it is not present,
708  invoke the image algorithm and store its result]
709
710  SideEffects        []
711
712  SeeAlso            [AbsEvalCacheEntry]
713
714******************************************************************************/
715mdd_t *
716AbsImageReadOrCompute(
717  Abs_VerificationInfo_t *absInfo,
718  Img_ImageInfo_t *imageInfo,
719  mdd_t *set,
720  mdd_t *careSet
721)
722{
723  AbsEvalCacheEntry_t *entry;
724  st_table            *table;
725  bdd_node            *f;
726  mdd_t               *result;
727  long                cpuTime;
728  int                 complement;
729
730  entry = NIL(AbsEvalCacheEntry_t);
731  table = AbsVerificationInfoReadImageCache(absInfo);
732  f = bdd_get_node(set, &complement);
733
734  /* See if the table has been created */
735  if (table == NIL(st_table)) {
736    table = st_init_table(st_ptrcmp, st_ptrhash);
737    AbsVerificationInfoSetImageCache(absInfo, table);
738  }
739  else {
740    /* Look up for the operation */
741    if (st_lookup(table, f, &entry)) {
742      if (complement == AbsEvalCacheEntryReadComplement(entry) &&
743          mdd_lequal(careSet, AbsEvalCacheEntryReadCareSet(entry), 1, 1)) {
744        result = mdd_dup(AbsEvalCacheEntryReadResult(entry));
745        return result;
746      }
747      else {
748        st_delete(table, &f, &entry);
749
750        mdd_free(AbsEvalCacheEntryReadKey(entry));
751        mdd_free(AbsEvalCacheEntryReadResult(entry));
752        mdd_free(AbsEvalCacheEntryReadCareSet(entry));
753      }
754    }
755  }
756
757  /* The result has not been found. Compute it and insert it in the cache */
758  cpuTime = util_cpu_time();
759  result = Img_ImageInfoComputeFwdWithDomainVars(imageInfo, set, set, careSet);
760  AbsStatsReadImageCpuTime(AbsVerificationInfoReadStats(absInfo))+= 
761    util_cpu_time() - cpuTime;
762  AbsStatsReadExactImage(AbsVerificationInfoReadStats(absInfo))++;
763
764  if (entry == NIL(AbsEvalCacheEntry_t)) {
765    entry = AbsCacheEntryInitialize();
766  }
767
768  AbsEvalCacheEntrySetKey(entry, mdd_dup(set));
769  AbsEvalCacheEntrySetComplement(entry, complement);
770  AbsEvalCacheEntrySetResult(entry, mdd_dup(result));
771  AbsEvalCacheEntrySetCareSet(entry, mdd_dup(careSet));
772 
773  /* Insert the new entry in the cache */
774  st_insert(table, (char *)f, (char *)entry);
775
776  AbsStatsReadImageCacheEntries(AbsVerificationInfoReadStats(absInfo))++;
777
778  return result;
779} /* End of AbsImageReadOrCompute */
780
781/**Function********************************************************************
782
783  Synopsis [Procedure to fire the evaluation process for a collection of
784  formulas given in an array]
785
786  Description [This is the main procedure of the package. The command
787  abs_model_check invokes this function. This procedure invokes the procedure
788  AbsSubFormulaVerify]
789 
790  SideEffects []
791
792******************************************************************************/
793array_t *
794AbsFormulaArrayVerify(
795  Abs_VerificationInfo_t *absInfo,
796  array_t *formulaArray)
797{
798  AbsOptions_t    *options;
799  AbsVertexInfo_t *formulaPtr;
800  Fsm_Fsm_t       *fsm;
801  array_t         *result;
802  mdd_manager     *mddManager;
803  int             fIndex;
804  int             numReorderings;
805
806  /* Initialize some variables */
807  options = AbsVerificationInfoReadOptions(absInfo);
808  mddManager = AbsVerificationInfoReadMddManager(absInfo);
809  numReorderings = bdd_read_reorderings(mddManager);
810 
811  /* Print the configuration of the system */
812  if (AbsOptionsReadVerbosity(options) & ABS_VB_PIFF) {
813    (void) fprintf(vis_stdout, "ABS: System with (PI,FF) = (%d,%d)\n", 
814                   st_count(AbsVerificationInfoReadQuantifyVars(absInfo)), 
815                   st_count(AbsVerificationInfoReadStateVars(absInfo)));
816  }
817
818  /* Create the array of results */
819  result = array_alloc(AbsVerificationResult_t, array_n(formulaArray));
820
821  /* Obtain the fsm representing the complete circuit */
822  fsm = Fsm_FsmCreateFromNetworkWithPartition(
823          AbsVerificationInfoReadNetwork(absInfo), NIL(graph_t));
824
825  /* Traverse the array of formulas and verify all of them */
826  arrayForEachItem(AbsVertexInfo_t *, formulaArray, fIndex, formulaPtr) {
827    Fsm_Fsm_t *localSystem;
828    Fsm_Fsm_t *approxSystem;
829    array_t   *stateVarIds;
830    mdd_t     *initialStates;
831    mdd_t     *careStates;
832    long      cpuTime;
833    int       numBddVars;
834    int       mddId;
835    int       i;
836
837    /* Variable Initialization */
838    approxSystem = NIL(Fsm_Fsm_t);
839
840    /* Set the cpu-time lap */
841    cpuTime = util_cpu_time();
842
843    /* Print the labeled operational graph */
844    if (AbsOptionsReadVerbosity(options) & ABS_VB_GRAPH) {
845      (void) fprintf(vis_stdout, "ABS: === Labeled Operational Graph ===\n");
846      AbsVertexPrint(formulaPtr, NIL(st_table), TRUE,
847                     AbsOptionsReadVerbosity(options));
848      (void) fprintf(vis_stdout, "ABS: === End of Graph ===\n");
849    }
850   
851    /* Simplify the system with respect to the given formula */
852    localSystem = AbsCreateReducedFsm(absInfo, formulaPtr, &approxSystem);
853    if (localSystem == NIL(Fsm_Fsm_t)) {
854      localSystem = fsm;
855    }
856    if (approxSystem == NIL(Fsm_Fsm_t)) {
857      approxSystem = fsm;
858    }
859
860    AbsVerificationInfoSetFsm(absInfo, localSystem);
861
862    /* Compute the number of bdd variables needed to encode the state space */
863    stateVarIds = Fsm_FsmReadPresentStateVars(localSystem);
864    numBddVars = 0;
865    arrayForEachItem(int, stateVarIds, i, mddId) {
866      array_t *mvarList = mdd_ret_mvar_list(mddManager);
867      mvar_type mddVar  = array_fetch(mvar_type, mvarList, mddId);
868      numBddVars += mddVar.encode_length;
869    }
870    AbsVerificationInfoSetNumStateVars(absInfo, numBddVars);
871
872    AbsVerificationInfoSetApproxFsm(absInfo, approxSystem);
873
874    if (AbsOptionsReadVerbosity(options) & ABS_VB_SIMPLE) {
875      (void) fprintf(vis_stdout, 
876                     "ABS: System Simplified from %d to %d latches\n",
877                     array_n(Fsm_FsmReadPresentStateVars(fsm)),
878                     array_n(Fsm_FsmReadPresentStateVars(localSystem)));
879      (void) fprintf(vis_stdout, 
880                     "ABS: System Approximated by %d of %d latches\n",
881                     array_n(Fsm_FsmReadPresentStateVars(approxSystem)),
882                     array_n(Fsm_FsmReadPresentStateVars(localSystem)));
883    }
884                   
885    /* Compute reachability if requested */
886    if (AbsOptionsReadReachability(options)) {
887      mdd_t *reachableStates;
888      long  cpuTime;
889     
890      cpuTime = util_cpu_time();
891     
892      reachableStates = Fsm_FsmComputeReachableStates(localSystem, 0, 1, 0, 0, 
893                        0, 0, 0,Fsm_Rch_Default_c, 0, 0, NIL(array_t), FALSE,
894                        NIL(array_t));
895      if (AbsOptionsReadVerbosity(options) & ABS_VB_PPROGR) {
896        (void) fprintf(vis_stdout, "ABS: %7.1f secs spent in reachability \n",
897                       (util_cpu_time() - cpuTime)/1000.0);
898      }
899
900      /* Print the number of reachable states */
901      if (AbsOptionsReadVerbosity(options) & ABS_VB_PRCH) {
902        array_t *sVars;
903       
904        sVars = Fsm_FsmReadPresentStateVars(localSystem);
905        (void) fprintf(vis_stdout, "ABS: System with %.0f reachable states.\n",
906                       mdd_count_onset(mddManager, reachableStates, sVars));
907      }
908     
909      careStates = reachableStates;
910    } /* End of reachability analysis */
911    else {
912      careStates = mdd_one(mddManager);
913    }
914
915    /* Compute the initial states */
916    initialStates = Fsm_FsmComputeInitialStates(localSystem);
917    if (initialStates == NIL(mdd_t)) {
918      (void) fprintf(vis_stdout, "** abs error: Unable to compute initial states.\n");
919      (void) fprintf(vis_stdout, "ABS: %s\n", error_string());
920     
921      AbsVerificationInfoFree(absInfo);
922      array_free(result);
923      /* Deallocate the FSM if the system was reduced */
924      if (localSystem != fsm) {
925        Fsm_FsmFree(localSystem);
926      }
927      return NIL(array_t);
928    }
929
930    /* Set the don't care information */
931    if (AbsVerificationInfoReadCareSet(absInfo) != NIL(mdd_t)) {
932      mdd_free(AbsVerificationInfoReadCareSet(absInfo));
933    }
934    AbsVerificationInfoSetCareSet(absInfo, careStates);
935    if (AbsVerificationInfoReadTmpCareSet(absInfo) != NIL(mdd_t)) {
936      mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
937    }
938    AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager));
939
940    /* Compute the formula EG(true) if required */
941    if (AbsOptionsReadEnvelope(options)) {
942      mdd_t *newCareStates;
943      mdd_t *tmp1;
944
945      newCareStates = ComputeEGtrue(absInfo, careStates);
946      tmp1 = mdd_and(newCareStates, careStates, 1, 1);
947      mdd_free(careStates);
948      mdd_free(newCareStates);
949      careStates = tmp1;
950      AbsVerificationInfoSetCareSet(absInfo, careStates);
951    }
952
953    /* Print verbosity message */
954    if (AbsOptionsReadVerbosity(options) & ABS_VB_VTXCNT) {
955      (void) fprintf(vis_stdout, "ABS: === Initial Verification ===\n");
956    }
957   
958    /* Create the initial evaluation of the formula */
959    AbsSubFormulaVerify(absInfo, formulaPtr);
960   
961    assert(!AbsVertexReadTrueRefine(formulaPtr));
962
963    /* Print verbosity message */
964    if (AbsOptionsReadVerbosity(options) & ABS_VB_VTXCNT) {
965      (void) fprintf(vis_stdout, "ABS: === End of Initial Verification ===\n");
966    }
967   
968    /* Print cpu-time information */
969    if (AbsOptionsReadVerbosity(options) & ABS_VB_PPROGR) {
970      (void) fprintf(vis_stdout, "ABS: Initial verification: %7.1f secs.\n",
971                     (util_cpu_time() - cpuTime)/1000.0);
972    }
973
974    /* Check if the initial states satisfy the formula */
975    if (mdd_lequal(initialStates, AbsVertexReadSat(formulaPtr), 1, 1)) {
976        array_insert(int, result, fIndex, trueVerification_c);
977    }
978    else {
979      if (AbsVertexReadGlobalApprox(formulaPtr)) {
980        mdd_t *goalSet;
981        mdd_t *refinement;
982
983        /*
984         * Compute the set of states remaining in the goal. We are assuming
985         * that the parity of the top vertex is negative
986         */
987        assert(!AbsVertexReadPolarity(formulaPtr));
988
989        /* Compute the initial goal set */
990        goalSet = mdd_and(initialStates, AbsVertexReadSat(formulaPtr), 1, 0);
991
992        /* Notify that the refinement process is beginning */
993        if (AbsOptionsReadVerbosity(options) &ABS_VB_PPROGR) {
994          (void) fprintf(vis_stdout, 
995                         "ABS: Verification has been approximated. ");
996          (void) fprintf(vis_stdout, "Beginning approximation refinement\n");
997        }
998
999        /* Print the number of states to refine */
1000        if (AbsOptionsReadVerbosity(options) & ABS_VB_PRINIT) {
1001          array_t *sVars;
1002
1003          sVars = Fsm_FsmReadPresentStateVars(fsm);
1004          (void) fprintf(vis_stdout, 
1005                         "ABS: %.0f states out of %.0f to be refined\n",
1006                         mdd_count_onset(mddManager, goalSet, sVars),
1007                         mdd_count_onset(mddManager, initialStates, sVars));
1008        }
1009
1010        /* Effectively perform the refinement */
1011        refinement = AbsSubFormulaRefine(absInfo, formulaPtr, goalSet); 
1012
1013        /* Insert the outcome of the refinement in the solution */
1014        if (mdd_is_tautology(refinement, 0)) {
1015          array_insert(int, result, fIndex, trueVerification_c);
1016        }
1017        else {
1018          if (!AbsVertexReadTrueRefine(formulaPtr)) {
1019            array_insert(int, result, fIndex, inconclusiveVerification_c);
1020          }
1021          else {
1022            array_insert(int, result, fIndex, falseVerification_c);
1023          }
1024        }
1025        mdd_free(goalSet);
1026        mdd_free(refinement);
1027      }
1028      else {
1029        array_insert(int, result, fIndex, falseVerification_c);
1030      }
1031    }
1032    mdd_free(initialStates);
1033   
1034    /* Print cpu-time information */
1035    if (AbsOptionsReadVerbosity(options) & ABS_VB_PPROGR) {
1036      (void) fprintf(vis_stdout, "ABS: Formula #%d verified in %7.1f secs.\n",
1037                     fIndex + 1, (util_cpu_time() - cpuTime)/1000.0);
1038    }
1039
1040    /* Print the number of states in the on set of Sat */
1041    if (AbsOptionsReadVerbosity(options) & ABS_VB_TSAT) {
1042      array_t *sVars;
1043     
1044      sVars = Fsm_FsmReadPresentStateVars(localSystem);
1045      (void) fprintf(vis_stdout, "ABS: %.0f States in sat of the formula.\n",
1046                     mdd_count_onset(mddManager, AbsVertexReadSat(formulaPtr), 
1047                                     sVars));
1048    }
1049
1050    /* Clean up */
1051    AbsVertexFlushCache(formulaPtr);
1052    AbsVerificationFlushCache(absInfo);
1053    if (approxSystem != fsm) {
1054      Fsm_FsmFree(approxSystem);
1055    }
1056    if (localSystem != fsm) {
1057      Fsm_FsmFree(localSystem);
1058    }
1059  } /* End of the loop over the array of formulas to be verified */
1060
1061  /* Set the number of reorderings in the stats */
1062  AbsStatsSetNumReorderings(AbsVerificationInfoReadStats(absInfo),
1063                            bdd_read_reorderings(mddManager) - numReorderings);
1064
1065  /* Clean up */
1066  Fsm_FsmFree(fsm);
1067
1068  return result;
1069}
1070
1071/**Function********************************************************************
1072
1073  Synopsis [Given a FSM and operational graph, simplify the FSM based on
1074  topological analysis of the FSM]
1075
1076  SideEffects        []
1077
1078******************************************************************************/
1079Fsm_Fsm_t *
1080AbsCreateReducedFsm(
1081  Abs_VerificationInfo_t *absInfo,
1082  AbsVertexInfo_t *vertexPtr,
1083  Fsm_Fsm_t **approxFsm)
1084{
1085  AbsVertexInfo_t *vPtr;
1086  Ntk_Network_t   *network;
1087  Ntk_Node_t      *nodePtr;
1088  Fsm_Fsm_t       *result;
1089  lsGen           gen;
1090  array_t         *vertexArray;
1091  array_t         *nodeArray;
1092  array_t         *supportArray;
1093  array_t         *inputs;
1094  array_t         *latches;
1095  st_table        *visited;
1096  int             i;
1097
1098  if (vertexPtr == NIL(AbsVertexInfo_t)) {
1099    return NIL(Fsm_Fsm_t);
1100  }
1101
1102  network = AbsVerificationInfoReadNetwork(absInfo);
1103
1104  /* Select the vertices of type "identifier" */
1105  visited = st_init_table(st_ptrcmp, st_ptrhash);
1106  vertexArray = array_alloc(AbsVertexInfo_t *, 0);
1107  SelectIdentifierVertices(vertexPtr, vertexArray, visited);
1108  st_free_table(visited);
1109
1110  if (array_n(vertexArray) == 0) {
1111    array_free(vertexArray);
1112    return NIL(Fsm_Fsm_t);
1113  }
1114
1115  /* Create the array of network nodes corresponding to the identifiers */
1116  visited = st_init_table(st_ptrcmp, st_ptrhash);
1117  nodeArray = array_alloc(Ntk_Node_t *, 0);
1118  arrayForEachItem(AbsVertexInfo_t *, vertexArray, i, vPtr) {
1119    nodePtr = Ntk_NetworkFindNodeByName(network, AbsVertexReadName(vPtr));
1120
1121    assert(nodePtr != NIL(Ntk_Node_t));
1122
1123    if (!st_is_member(visited, (char *)nodePtr)) {
1124      array_insert_last(Ntk_Node_t *, nodeArray, nodePtr);
1125      st_insert(visited, (char *)nodePtr, NIL(char));
1126    }
1127  }
1128  array_free(vertexArray);
1129
1130  /* Create the input and array latches to compute the approxFsm */
1131  inputs = array_alloc(Ntk_Node_t *, 0);
1132  Ntk_NetworkForEachInput(network, gen, nodePtr) {
1133    array_insert_last(Ntk_Node_t *, inputs, nodePtr);
1134  }
1135  latches = array_alloc(Ntk_Node_t *, 0);
1136  Ntk_NetworkForEachLatch(network, gen, nodePtr) {
1137    if (st_is_member(visited, (char *)nodePtr)) {
1138      array_insert_last(Ntk_Node_t *, latches, nodePtr);
1139    }
1140    else {
1141      array_insert_last(Ntk_Node_t *, inputs, nodePtr);
1142    }
1143  }
1144  st_free_table(visited);
1145
1146  /* Obtain the approximated system */
1147  *approxFsm = Fsm_FsmCreateReducedFsm(network, NIL(graph_t), latches, inputs, 
1148                                       NIL(array_t));
1149  array_free(inputs);
1150  array_free(latches);
1151
1152  /* Obtain the transitive fanin of the nodes */
1153  supportArray = Ntk_NodeComputeCombinationalSupport(network, nodeArray, FALSE);
1154  array_free(nodeArray);
1155
1156  /* If the transitive fanin of the nodes is empty, return */
1157  if (array_n(supportArray) == 0) {
1158    array_free(supportArray);
1159    return NIL(Fsm_Fsm_t);
1160  }
1161
1162  /* Divide the nodes between inputs and latches and create the final FSM */
1163  inputs = array_alloc(Ntk_Node_t *, 0);
1164  latches = array_alloc(Ntk_Node_t *, 0);
1165  arrayForEachItem(Ntk_Node_t *, supportArray, i, nodePtr) {
1166    if (Ntk_NodeTestIsInput(nodePtr)) {
1167      array_insert_last(Ntk_Node_t *, inputs, nodePtr);
1168    }
1169    else {
1170      assert(Ntk_NodeTestIsLatch(nodePtr));
1171      array_insert_last(Ntk_Node_t *, latches, nodePtr);
1172    }
1173  }
1174  array_free(supportArray);
1175
1176  /* If the collection of inputs and latches is the whole FSM, return */
1177  if (array_n(inputs) == Ntk_NetworkReadNumInputs(network) &&
1178      array_n(latches) == Ntk_NetworkReadNumLatches(network)) {
1179    array_free(inputs);
1180    array_free(latches);
1181    return NIL(Fsm_Fsm_t);
1182  }
1183
1184  result = Fsm_FsmCreateReducedFsm(network, NIL(graph_t), latches, inputs, 
1185                                   NIL(array_t));
1186
1187  /* Clean up */
1188  array_free(inputs);
1189  array_free(latches);
1190
1191  return result;
1192} /* End of AbsCreateReducedFsm */
1193
1194/**Function********************************************************************
1195
1196  Synopsis [Check if two functions are identical modulo the don't care function
1197  provided]
1198
1199  SideEffects        []
1200
1201******************************************************************************/
1202boolean
1203AbsMddEqualModCareSet(
1204  mdd_t *f,
1205  mdd_t *g,
1206  mdd_t *careSet)
1207{
1208  boolean result = mdd_equal_mod_care_set(f, g, careSet);
1209  return result;
1210} /* End of AbsMddEqualModCareSet */
1211
1212/**Function********************************************************************
1213
1214  Synopsis [Check if function f is contained in function g but taking into
1215  account the provided care set]
1216
1217  SideEffects        []
1218
1219******************************************************************************/
1220boolean
1221AbsMddLEqualModCareSet(
1222  mdd_t *f,
1223  mdd_t *g,
1224  mdd_t *careSet)
1225{
1226  boolean result = mdd_lequal_mod_care_set(f, g, 1, 1, careSet);
1227  return result;
1228} /* End of AbsMddLEqualModCareSet */
1229
1230/*---------------------------------------------------------------------------*/
1231/* Definition of static functions                                            */
1232/*---------------------------------------------------------------------------*/
1233
1234/**Function********************************************************************
1235
1236  Synopsis           [Compute the verification of the formula EG(true)]
1237
1238  Description [This is provided as an option. The computation of this formula
1239  might reduce the state space to be explored. Specifically, it gets rid of
1240  states that do not have any successor as well as any other states leading to
1241  them. The benefit of this computation is unclear, specially because some
1242  tools that read verilog and produce blif-mv might produce a self loop in
1243  every state for which no transition is specified. If that is so, there will
1244  never be a state without a successor.]
1245
1246  SideEffects        []
1247
1248******************************************************************************/
1249static mdd_t *
1250ComputeEGtrue(
1251  Abs_VerificationInfo_t *absInfo,
1252  mdd_t *careStates)
1253{
1254  AbsOptions_t    *options;
1255  AbsVertexInfo_t *vertex;
1256  Ctlp_Formula_t  *egFormula;
1257  Ctlp_Formula_t  *trueFormula;
1258  mdd_manager     *mddManager;
1259  array_t         *inputTranslation;
1260  array_t         *outputTranslation;
1261  mdd_t           *envelope;
1262  long            cpuTime;
1263 
1264  cpuTime = util_cpu_time();
1265  options = AbsVerificationInfoReadOptions(absInfo);
1266  mddManager = AbsVerificationInfoReadMddManager(absInfo);
1267 
1268  /* Compute the EG(true) fixed point */
1269  trueFormula = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(void), NIL(void));
1270  egFormula = Ctlp_FormulaCreate(Ctlp_EG_c, trueFormula, NIL(void));
1271 
1272  /* Translate into the graph representation */
1273  inputTranslation = array_alloc(Ctlp_Formula_t *, 1);
1274  array_insert(Ctlp_Formula_t *, inputTranslation, 0, egFormula);
1275  outputTranslation = AbsCtlFormulaArrayTranslate(absInfo, inputTranslation, 
1276                                                  NIL(array_t));
1277  vertex = array_fetch(AbsVertexInfo_t *, outputTranslation, 0);
1278  array_free(inputTranslation);
1279  array_free(outputTranslation);
1280 
1281  /* Evaluate the formula */
1282  AbsSubFormulaVerify(absInfo, vertex);
1283 
1284  envelope = mdd_dup(AbsVertexReadSat(vertex));
1285 
1286  /* Clean up */
1287  Ctlp_FormulaFree(egFormula);
1288  AbsVertexFree(AbsVerificationInfoReadCatalog(absInfo), vertex, 
1289                NIL(AbsVertexInfo_t));
1290 
1291  /* Print the number of envelope states */
1292  if (AbsOptionsReadVerbosity(options) & ABS_VB_PENV) {
1293    array_t *sVars;
1294    mdd_t *states;
1295 
1296    sVars = Fsm_FsmReadPresentStateVars(AbsVerificationInfoReadFsm(absInfo));
1297    states = mdd_and(envelope, careStates, 1, 1);
1298    (void) fprintf(vis_stdout, "ABS: Envelope with %.0f care states.\n",
1299                   mdd_count_onset(mddManager, states, sVars));
1300    mdd_free(states);
1301  }
1302 
1303  if (AbsOptionsReadVerbosity(options) & ABS_VB_PENV) {
1304    (void) fprintf(vis_stdout, "ABS: %7.1f secs computing EG(TRUE)\n",
1305                   (util_cpu_time() - cpuTime)/1000.0);
1306  }
1307
1308  return envelope;
1309} /* End of ComputeEGtrue */
1310
1311/**Function********************************************************************
1312
1313  Synopsis [Given a graph, select the set of vertices that represent
1314  identifiers]
1315
1316  SideEffects        []
1317
1318******************************************************************************/
1319static void
1320SelectIdentifierVertices(
1321  AbsVertexInfo_t *vertexPtr,
1322  array_t *result,
1323  st_table *visited)
1324{
1325  assert(result != NIL(array_t));
1326
1327  if (vertexPtr == NIL(AbsVertexInfo_t)) {
1328    return;
1329  }
1330
1331  if (st_is_member(visited, (char *)vertexPtr)) {
1332    return;
1333  }
1334
1335  if (AbsVertexReadType(vertexPtr) == identifier_c) {
1336    array_insert_last(AbsVertexInfo_t *, result, vertexPtr);
1337    st_insert(visited, (char *)vertexPtr, NIL(char));
1338    return;
1339  }
1340  else {
1341    SelectIdentifierVertices(AbsVertexReadLeftKid(vertexPtr), result, visited);
1342    SelectIdentifierVertices(AbsVertexReadRightKid(vertexPtr), result, visited);
1343  }
1344
1345  st_insert(visited, (char *)vertexPtr, NIL(char));
1346
1347  return;
1348} /* End of SelectIdentifierVertices */
Note: See TracBrowser for help on using the repository browser.