source: vis_dev/vis-2.3/src/imc/imcImc.c

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

vis2.3
File size: 104.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [imcImc.c]
4
5  PackageName [imc]
6
7  Synopsis    [Incremental Model Checker.]
8
9  Author      [Jae-Young Jang <jjang@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 "imcInt.h"
18#include "part.h"
19#include "img.h"
20#include "ntm.h"
21
22static char rcsid[] UNUSED = "$Id: imcImc.c,v 1.21 2005/04/27 00:13:01 fabio Exp $";
23
24/*---------------------------------------------------------------------------*/
25/* Constant declarations                                                     */
26/*---------------------------------------------------------------------------*/
27
28
29/*---------------------------------------------------------------------------*/
30/* Type declarations                                                         */
31/*---------------------------------------------------------------------------*/
32
33
34/*---------------------------------------------------------------------------*/
35/* Structure declarations                                                    */
36/*---------------------------------------------------------------------------*/
37
38
39/*---------------------------------------------------------------------------*/
40/* Variable declarations                                                     */
41/*---------------------------------------------------------------------------*/
42
43
44/*---------------------------------------------------------------------------*/
45/* Macro declarations                                                        */
46/*---------------------------------------------------------------------------*/
47
48
49/**AutomaticStart*************************************************************/
50
51/*---------------------------------------------------------------------------*/
52/* Static function prototypes                                                */
53/*---------------------------------------------------------------------------*/
54
55static int stringCompare(const void * s1, const void * s2);
56
57/**AutomaticEnd***************************************************************/
58
59
60/*---------------------------------------------------------------------------*/
61/* Definition of exported functions                                          */
62/*---------------------------------------------------------------------------*/
63
64/**Function********************************************************************
65
66  Synopsis    [Verify a formula with incremental refinement.]
67
68  Description [Verify a formula with incremental refinement.]
69
70  SideEffects []
71
72  SeeAlso     []
73
74******************************************************************************/
75Imc_VerificationResult
76Imc_ImcEvaluateFormulaLinearRefine(
77  Ntk_Network_t         *network,
78  Ctlp_Formula_t        *orgFormula,
79  Ctlp_Formula_t        *formula,
80  Ctlp_FormulaClass     formulaClass,
81  int                   incrementalSize,
82  Imc_VerbosityLevel    verbosity,
83  Imc_RefineMethod      refine,
84  mdd_t                 *careStates,
85  Fsm_Fsm_t             *exactFsm,
86  Imc_DcLevel           dcLevel,
87  Imc_GraphType         graphType,
88  Imc_LowerMethod       lowerMethod,
89  Imc_UpperMethod       upperMethod,
90  boolean               computeExact,
91  boolean               needLower,
92  boolean               needUpper,
93  Imc_PartMethod        partMethod,
94  Hrc_Node_t            *currentNode,
95  char                  *modelName)
96{
97  Imc_Info_t            *imcInfo;
98  st_table              *latchNameTable;
99  int                   numberOfLatches, numberOfIncludedLatches;
100  int                   iterationCount;
101  Imc_VerificationResult verification = Imc_VerificationError_c;
102
103  /*
104   * Initialize data structures.
105   */
106  imcInfo = Imc_ImcInfoInitialize(network, formula, formulaClass, verbosity,
107                                  refine, careStates, dcLevel, incrementalSize,
108                                  graphType, exactFsm, lowerMethod, upperMethod,
109                                  computeExact, needLower, needUpper,
110                                  partMethod, currentNode, modelName);
111
112  if (imcInfo == NIL(Imc_Info_t))return(Imc_VerificationError_c); /* FIXED */
113
114  numberOfLatches = array_n(imcInfo->systemInfo->latchNameArray);
115 
116  iterationCount = 1;
117
118  numberOfIncludedLatches = array_n(imcInfo->systemInfo->includedLatchIndex);
119
120  if (verbosity != Imc_VerbosityNone_c) {
121    fprintf(vis_stdout, "IMC : Reduced system has ");
122    Imc_ImcPrintSystemSize(imcInfo);
123  }
124  if(verbosity != Imc_VerbosityNone_c) {
125    fprintf(vis_stdout, "IMC : Approximate system has ");
126    Imc_ImcPrintApproxSystemSize(imcInfo);
127  }
128
129  assert(numberOfLatches >= numberOfIncludedLatches);
130  while(numberOfLatches >= numberOfIncludedLatches) {
131 
132    /*
133     * verification is one of {Imc_VerificationTrue_c, Imc_VerificationFalse_c,
134     * Imc_VerificationInconclusive_c}.
135     */
136    verification = Imc_ImcVerifyFormula(imcInfo, formula);
137
138    if (verification == Imc_VerificationError_c) {
139
140      (void)fprintf(vis_stdout, "# IMC: formula inconclusive.\n");
141
142      /* Free all */
143      Imc_ImcInfoFree(imcInfo);
144      return verification;
145
146    }else if (verification != Imc_VerificationInconclusive_c){ 
147
148      if ((verification == Imc_VerificationTrue_c)) {
149        (void) fprintf(vis_stdout, "# IMC: formula passed.\n");
150      }else{
151        (void) fprintf(vis_stdout, "# IMC: formula failed.\n");
152      }
153      fprintf(vis_stdout, "IMC : ");
154      Ctlp_FormulaPrint( vis_stdout, orgFormula );
155      fprintf(vis_stdout, "\n");
156      fprintf(vis_stdout, "IMC : ");
157      Ctlp_FormulaPrint( vis_stdout, formula);
158      fprintf(vis_stdout, "\n");
159
160      Imc_ImcInfoFree(imcInfo);
161      return verification;
162    }else{
163      if (numberOfLatches == numberOfIncludedLatches){
164        if (imcInfo->graphType == Imc_GraphPDOG_c){
165          (void) fprintf(vis_stdout, "# IMC: formula passed.\n");
166        }else if (imcInfo->graphType == Imc_GraphNDOG_c){
167          (void) fprintf(vis_stdout, "# IMC: formula failed.\n");
168        }
169        fprintf(vis_stdout, "IMC : ");
170        Ctlp_FormulaPrint( vis_stdout,orgFormula);
171        fprintf(vis_stdout, "\n");
172        fprintf(vis_stdout, "IMC : ");
173        Ctlp_FormulaPrint( vis_stdout, formula); 
174        fprintf(vis_stdout, "\n");
175
176        Imc_ImcInfoFree(imcInfo);
177        return verification;
178      }
179    }       
180
181    latchNameTable = array_fetch(st_table *, 
182                     imcInfo->staticRefineSchedule, iterationCount);
183   
184    Imc_ImcSystemInfoUpdate(imcInfo, latchNameTable);
185
186    /*
187     * Refine the approximate system.
188     */ 
189    if (imcInfo->needUpper){
190      Imc_UpperSystemInfoFree(imcInfo->upperSystemInfo);
191      Imc_UpperSystemInfoInitialize(imcInfo, latchNameTable);
192    }
193
194    if (imcInfo->needLower){
195      Imc_LowerSystemInfoFree(imcInfo->lowerSystemInfo);
196      Imc_LowerSystemInfoInitialize(imcInfo, latchNameTable);
197    }
198
199    Imc_NodeInfoReset(imcInfo);
200
201    numberOfIncludedLatches = 
202        array_n(imcInfo->systemInfo->includedLatchIndex);
203
204    iterationCount++;
205
206    if(verbosity != Imc_VerbosityNone_c) {
207      fprintf(vis_stdout, "IMC : Approximate system has ");
208      Imc_ImcPrintApproxSystemSize(imcInfo);
209    }
210
211  } /* end of while(numberOfLatches >= numberOfIncludedLatches) */
212
213  return(verification); /* FIXED */
214}
215
216/**Function********************************************************************
217
218  Synopsis    [Verify a formula.]
219
220  Description [Verify a formula.]
221
222  SideEffects []
223
224  SeeAlso     []
225
226******************************************************************************/
227Imc_VerificationResult
228Imc_ImcVerifyFormula(
229  Imc_Info_t *imcInfo,
230  Ctlp_Formula_t *formula)
231{
232  Imc_VerificationResult result;
233
234  if (!Imc_ImcEvaluateCTLFormula(imcInfo, formula, Imc_PolarityPos_c)){
235    return Imc_VerificationError_c;
236  }
237
238  result = Imc_SatCheck(imcInfo, formula);
239
240  return result;
241}
242
243/**Function********************************************************************
244
245  Synopsis    [Check if a formula is true or false.]
246
247  Description [Check if a formula is true or false. If all initial states are
248  contained in a lowerbound satisfying states, a formula is true. If any of
249  initial states is not contained by a upperbound satisfying states, a formula
250  is false. Otherwise, inconclusive.]
251
252  SideEffects []
253
254  SeeAlso     []
255
256******************************************************************************/
257Imc_VerificationResult
258Imc_SatCheck(
259  Imc_Info_t *imcInfo,
260  Ctlp_Formula_t *formula)
261{
262  mdd_t *initialStates = imcInfo->initialStates;
263  Imc_NodeInfo_t *nodeInfo;
264
265  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
266    return Imc_VerificationError_c; /* FIXED */
267  }
268 
269  if (nodeInfo->lowerSat != NIL(mdd_t)){
270    if (mdd_lequal(initialStates, nodeInfo->lowerSat, 1, 1)){
271      return Imc_VerificationTrue_c;
272    }
273  }
274  if (nodeInfo->upperSat != NIL(mdd_t)){
275    if (!mdd_lequal_mod_care_set(initialStates, nodeInfo->upperSat, 1, 1,
276                                 imcInfo->modelCareStates)){ /* FIXED */
277      return Imc_VerificationFalse_c;
278    }
279  }
280  return Imc_VerificationInconclusive_c;
281}
282
283/**Function********************************************************************
284
285  Synopsis    [Initializes an imcInfo structure for the given method.]
286
287  Description [Regardless of the method type, the initialization procedure
288  starts from constructing set of subsystems. A subsystem contains a subset
289  of vertices of the partition. Based on the subset of vertices, subFSM is
290  created. The subsystems are stored as an array. After the creation of
291  the subsystem array, the function initializes remaining field of
292  (Imc_Info_t *) imcInfo.
293  The function returns initialized (Imc_Info_t *) imcInfo.]
294
295  SideEffects        []
296
297  SeeAlso     []
298
299******************************************************************************/
300Imc_Info_t *
301Imc_ImcInfoInitialize(
302  Ntk_Network_t      *network,
303  Ctlp_Formula_t     *formula,
304  Ctlp_FormulaClass  formulaClass,
305  Imc_VerbosityLevel verbosity,
306  Imc_RefineMethod   refine,
307  mdd_t              *careStates,
308  Imc_DcLevel        dcLevel,
309  int                incrementalSize,
310  Imc_GraphType      graphType,
311  Fsm_Fsm_t          *exactFsm,
312  Imc_LowerMethod    lowerMethod,
313  Imc_UpperMethod    upperMethod,
314  boolean            computeExact,
315  boolean            needLower,
316  boolean            needUpper,
317  Imc_PartMethod     partMethod,
318  Hrc_Node_t         *currentNode, 
319  char               *modelName)
320{
321  int                 i;
322  char                *flagValue; 
323  Imc_Info_t          *imcInfo;
324  mdd_t               *initialStates;
325  array_t             *scheduleArray;
326  st_table            *latchNameTable;
327  st_table            *newLatchNameTable;
328  st_table            *globalLatchNameTable;
329  array_t             *psMddIdArray;
330  array_t             *nsMddIdArray;
331  array_t             *inputMddIdArray;
332  array_t             *supportMddIdArray;
333  array_t             *preQMddIdArray;
334  array_t             *imgQMddIdArray;
335  Part_CMethod        correlationMethod;
336  Ntk_Node_t          *latch, *input;
337  lsGen               gen;
338  array_t             *latchNameArray;
339
340  imcInfo = ALLOC(Imc_Info_t, 1);
341
342  /*
343   * Initialize
344   */
345  imcInfo->network         = network;
346  imcInfo->globalFsm       = exactFsm;
347  imcInfo->formulaClass    = formulaClass;
348  imcInfo->incrementalSize = incrementalSize;
349  imcInfo->dcLevel         = dcLevel;
350  imcInfo->refine          = refine;
351  imcInfo->verbosity       = verbosity;
352  imcInfo->upperSystemInfo = NIL(Imc_UpperSystemInfo_t);
353  imcInfo->lowerSystemInfo = NIL(Imc_LowerSystemInfo_t);
354  imcInfo->initialStates   = NIL(mdd_t); 
355  imcInfo->nodeInfoTable   = NIL(st_table);
356  imcInfo->graphType       = graphType;
357  imcInfo->nodeInfoTable   = st_init_table(st_ptrcmp , st_ptrhash);
358  imcInfo->mddMgr          = Ntk_NetworkReadMddManager(network);
359  imcInfo->lowerMethod     = lowerMethod;
360  imcInfo->upperMethod     = upperMethod;
361  imcInfo->currentNode     = currentNode;
362  imcInfo->modelName       = modelName;
363
364  if (exactFsm == NIL(Fsm_Fsm_t)){
365    imcInfo->useLocalFsm = TRUE;
366  }else{
367    imcInfo->useLocalFsm = FALSE;
368  }
369
370  /*
371   * Initialize image and preimage computation info.
372   */
373  if (exactFsm != NIL(Fsm_Fsm_t)){
374    psMddIdArray = array_dup(Fsm_FsmReadPresentStateVars(exactFsm));
375    nsMddIdArray = array_dup(Fsm_FsmReadNextStateVars(exactFsm));
376    inputMddIdArray = array_dup(Fsm_FsmReadInputVars(exactFsm));
377  }else{
378    latchNameArray = array_alloc(char *, 0);
379    psMddIdArray = array_alloc(int, 0);
380    nsMddIdArray = array_alloc(int, 0);
381    inputMddIdArray = array_alloc(int, 0);
382    /* sort by name of latch */
383    Ntk_NetworkForEachLatch(network, gen, latch){
384      array_insert_last(char*, latchNameArray,
385                        Ntk_NodeReadName(latch));
386    }
387
388    array_sort(latchNameArray, stringCompare);
389
390    for (i = 0; i < array_n(latchNameArray); i++) {
391      char *nodeName;
392      nodeName = array_fetch(char *, latchNameArray, i);
393      latch = Ntk_NetworkFindNodeByName(network, nodeName);
394      array_insert_last(int, psMddIdArray,
395                      Ntk_NodeReadMddId(latch));
396      array_insert_last(int, nsMddIdArray,
397                      Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
398    }
399 
400    array_free(latchNameArray);
401 
402    Ntk_NetworkForEachInput(network, gen, input){
403      array_insert_last(int, inputMddIdArray, Ntk_NodeReadMddId(input));
404    }
405  }
406
407  imgQMddIdArray = array_dup(psMddIdArray);
408  array_append(imgQMddIdArray,inputMddIdArray); 
409
410  supportMddIdArray = array_dup(imgQMddIdArray);
411  array_append(supportMddIdArray,nsMddIdArray);
412
413  preQMddIdArray = array_dup(nsMddIdArray);
414  array_append(preQMddIdArray,inputMddIdArray); 
415
416  array_free(psMddIdArray);
417  array_free(nsMddIdArray);
418  array_free(inputMddIdArray);
419 
420  imcInfo->supportMddIdArray = supportMddIdArray;
421  imcInfo->imgQMddIdArray = imgQMddIdArray;
422  imcInfo->preQMddIdArray = preQMddIdArray;
423  imcInfo->needLower = needLower;
424  imcInfo->needUpper = needUpper;
425  imcInfo->partMethod = partMethod;
426
427  if (careStates == NIL(mdd_t)){
428    imcInfo->modelCareStates = mdd_one(imcInfo->mddMgr);
429  }else{
430    imcInfo->modelCareStates = mdd_dup(careStates);
431  }
432
433  /*
434   * If refine oprion is Imc_RefineLatchRelation_c,
435   * correlation method should be defined.
436   */
437  flagValue = Cmd_FlagReadByName("part_group_correlation_method");
438  if(flagValue == NIL(char)){
439    correlationMethod = Part_CorrelationWithBDD; 
440  }else if (strcmp(flagValue, "support") == 0){
441    correlationMethod = Part_CorrelationWithSupport; 
442  }else if (strcmp(flagValue, "mdd") == 0){
443    correlationMethod = Part_CorrelationWithBDD;
444  }else{
445    correlationMethod = Part_CorrelationWithSupport;
446  }
447
448  if ((refine == Imc_RefineLatchRelation_c) &&
449      (correlationMethod == Part_CorrelationWithBDD) &&
450      (partMethod == Imc_PartInc_c)){
451    correlationMethod = Part_CorrelationWithSupport;
452  }
453  imcInfo->correlationMethod = correlationMethod;
454
455  if (computeExact){
456    scheduleArray = ImcCreateScheduleArray(network, formula, TRUE, 
457                      Imc_RefineLatchRelation_c, verbosity, incrementalSize,
458                      correlationMethod);
459    imcInfo->staticRefineSchedule = NIL(array_t);
460    latchNameTable = array_fetch(st_table *, scheduleArray, 0);
461    st_free_table(latchNameTable);
462    latchNameTable = array_fetch(st_table *, scheduleArray, 1);
463    newLatchNameTable = st_copy(latchNameTable);
464    array_insert(st_table *, scheduleArray, 0, newLatchNameTable);
465
466  }else if (refine == Imc_RefineLatchRelation_c){
467    scheduleArray = ImcCreateScheduleArray(network, formula, FALSE, refine, 
468                    verbosity, incrementalSize, correlationMethod);
469    imcInfo->staticRefineSchedule = scheduleArray;
470
471  }else if (refine == Imc_RefineSort_c){
472    scheduleArray = ImcCreateScheduleArray(network, formula, TRUE, refine, 
473                    verbosity, incrementalSize, correlationMethod);
474    imcInfo->staticRefineSchedule = scheduleArray;
475
476  }else{
477    fprintf(vis_stdout, "** imc error: Unkown refinement method.\n");
478    Imc_ImcInfoFree(imcInfo);
479    return NIL(Imc_Info_t);
480  }
481
482  if (scheduleArray == NIL(array_t)){
483    fprintf(vis_stdout, "** imc error: Can't get an initial system.\n");
484    Imc_ImcInfoFree(imcInfo);
485    return NIL(Imc_Info_t);
486  }
487   
488  globalLatchNameTable = array_fetch(st_table *, scheduleArray, array_n(scheduleArray)-1);
489  latchNameTable = array_fetch(st_table *, scheduleArray, 0); 
490
491  /*
492   * Initialize a total system info.
493   */
494  Imc_SystemInfoInitialize(imcInfo, globalLatchNameTable, latchNameTable); 
495
496  /*
497   * Initialize an initial approximate system info.
498   */
499  if (needUpper){
500    Imc_UpperSystemInfoInitialize(imcInfo,latchNameTable);
501  }
502  if (needLower){
503    Imc_LowerSystemInfoInitialize(imcInfo,latchNameTable);
504  }
505
506  initialStates = Fsm_FsmComputeInitialStates(imcInfo->globalFsm); 
507  if (initialStates == NIL(mdd_t)){
508    fprintf(vis_stdout,"** imc error : System has no initial state.\n");
509    Imc_ImcInfoFree(imcInfo);
510    return NIL(Imc_Info_t);
511  }
512  imcInfo->initialStates = initialStates; 
513
514  if (computeExact){
515    arrayForEachItem(st_table *, scheduleArray, i, latchNameTable){
516      st_free_table(latchNameTable);
517    }
518    array_free(scheduleArray);
519  }
520
521  return(imcInfo);
522}
523
524
525/**Function********************************************************************
526
527  Synopsis    [Free an imcInfo structure for the given method.]
528
529  Description [Free an imcInfo structure for the given method.]
530
531  SideEffects []
532
533  SeeAlso     []
534
535******************************************************************************/
536void
537Imc_ImcInfoFree(
538  Imc_Info_t *imcInfo)
539{
540  int i;
541  st_table *latchNameTable;
542
543  Imc_UpperSystemInfoFree(imcInfo->upperSystemInfo);
544  Imc_LowerSystemInfoFree(imcInfo->lowerSystemInfo);
545  ImcNodeInfoTableFree(imcInfo->nodeInfoTable);
546  if (imcInfo->initialStates != NIL(mdd_t)) mdd_free(imcInfo->initialStates); 
547
548  if (imcInfo->modelCareStates!=NIL(mdd_t)) mdd_free(imcInfo->modelCareStates);
549  if (imcInfo->staticRefineSchedule != NIL(array_t)){
550    arrayForEachItem(st_table *,imcInfo->staticRefineSchedule, i, latchNameTable){
551      st_free_table(latchNameTable);
552    }
553    array_free(imcInfo->staticRefineSchedule);
554  }
555  if (imcInfo->supportMddIdArray != NIL(array_t)) 
556    array_free(imcInfo->supportMddIdArray);
557  if (imcInfo->imgQMddIdArray != NIL(array_t)) 
558    array_free(imcInfo->imgQMddIdArray);
559  if (imcInfo->preQMddIdArray != NIL(array_t)) 
560    array_free(imcInfo->preQMddIdArray);
561
562  if ((imcInfo->useLocalFsm) && (imcInfo->globalFsm != NIL(Fsm_Fsm_t))){
563    Fsm_FsmSubsystemFree(imcInfo->globalFsm);
564  }
565
566  Imc_SystemInfoFree(imcInfo->systemInfo);
567
568  FREE(imcInfo);
569}
570
571
572/**Function********************************************************************
573
574  Synopsis    [Initilalize a system info.]
575
576  Description [Initilalize a system info.]
577
578  SideEffects []
579
580  SeeAlso     []
581
582******************************************************************************/
583void
584Imc_SystemInfoInitialize(
585  Imc_Info_t *imcInfo,
586  st_table *globalLatchNameTable,
587  st_table *initialLatchNameTable)
588{
589  int i, psMddId, nsMddId, latchSize;
590  char *name, *dataInputName;
591  Ntk_Node_t *node, *latchInput; 
592  Ntk_Network_t *network = imcInfo->network;
593  graph_t *partition = Part_NetworkReadPartition(network);
594  vertex_t *vertex;
595  Mvf_Function_t *mvf;
596  mdd_t *singleTR, *subTR, *tempMdd;
597  st_generator *stGen;
598  lsList latchInputList;
599  lsGen gen;
600  st_table *partNameTable;
601  Imc_SystemInfo_t *systemInfo;
602  array_t *bddIdArray;
603  array_t *latchNameArray = 
604           array_alloc(char *, st_count(globalLatchNameTable));
605  st_table *latchNameTable = st_init_table(strcmp, st_strhash );
606  st_table *latchInputTable = st_init_table(st_ptrcmp, st_ptrhash );
607  st_table *nsMddIdToIndex = st_init_table(st_numcmp, st_numhash);
608  st_table *psMddIdToIndex = st_init_table(st_numcmp, st_numhash);
609  array_t *latchNodeArray = 
610           array_alloc(Ntk_Node_t *, st_count(globalLatchNameTable));
611  array_t *nsMddIdArray = array_alloc(int,st_count(globalLatchNameTable));
612  array_t *psMddIdArray = array_alloc(int,st_count(globalLatchNameTable));
613  array_t *TRArray = array_alloc(mdd_t *,st_count(globalLatchNameTable));
614  array_t *lowerTRArray = array_alloc(mdd_t *,st_count(globalLatchNameTable));
615  array_t *mvfArray = array_alloc(mdd_t *,st_count(globalLatchNameTable));
616  array_t *latchSizeArray = array_alloc(int,st_count(globalLatchNameTable));
617  array_t *includedLatchIndex = array_alloc(int, 0);
618  array_t *includedNsMddId = array_alloc(int, 0);
619  array_t *excludedLatchIndex = array_alloc(int, 0);
620  array_t *excludedNsMddId = array_alloc(int, 0);
621  array_t *excludedPsMddId = array_alloc(int, 0);
622  array_t *includedPsMddId = array_alloc(int, 0);
623  st_table *excludedPsMddIdTable = st_init_table(st_numcmp, st_numhash);
624
625  systemInfo = ALLOC(Imc_SystemInfo_t, 1);
626
627  st_foreach_item(globalLatchNameTable, stGen, &name, NIL(char *)){
628    array_insert_last(char *, latchNameArray, name);
629  }
630
631  array_sort(latchNameArray, stringCompare);
632
633  if (partition == NIL(graph_t)){
634    if ((imcInfo->partMethod == Imc_PartInc_c) &&
635        !((imcInfo->needLower) && 
636         (imcInfo->lowerMethod != Imc_LowerUniversalQuantification_c))){
637      partNameTable = initialLatchNameTable;
638    }else{
639      partNameTable = globalLatchNameTable;
640    }
641    st_foreach_item(partNameTable, stGen, &name, NIL(char *)){
642      node = Ntk_NetworkFindNodeByName(network, name);
643      latchInput = Ntk_LatchReadDataInput(node);
644      st_insert(latchInputTable, (char *)latchInput, (char *)(long)(-1));
645    }
646    latchInputList = lsCreate();
647    st_foreach_item(latchInputTable, stGen, &node, NULL){
648      lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
649    }
650    st_free_table(latchInputTable);
651    Ntk_NetworkForEachCombOutput(network, gen, node){
652      if (Ntk_NodeTestIsLatchInitialInput(node)){
653        lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
654      }
655    }
656
657    partition = Part_NetworkCreatePartition(network, imcInfo->currentNode, 
658                  imcInfo->modelName, latchInputList, (lsList)0, NIL(mdd_t),
659                  Part_InOut_c, (lsList)0, FALSE, 0, 0);
660    lsDestroy(latchInputList, (void (*)(lsGeneric))0); 
661   
662    Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY,
663                  (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
664                  (void *) partition);
665
666    imcInfo->globalFsm = Fsm_FsmCreateSubsystemFromNetwork(network,partition,
667                                                    partNameTable, FALSE, 0);
668
669    imcInfo->useLocalFsm = TRUE;
670  }else{
671    st_foreach_item(initialLatchNameTable, stGen, &name, NIL(char *)){
672      node = Ntk_NetworkFindNodeByName(network, name);
673      latchInput = Ntk_LatchReadDataInput(node);
674      st_insert(latchInputTable, (char *)latchInput, (char *)(long)(-1));
675    }
676    latchInputList = lsCreate();
677    st_foreach_item(latchInputTable, stGen, &node, NIL(char *)){
678      lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
679    }
680    st_free_table(latchInputTable);
681    Ntk_NetworkForEachCombOutput(network, gen, node){
682      if (Ntk_NodeTestIsLatchInitialInput(node)){
683        lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
684      }
685    }
686    (void) Part_PartitionChangeRoots(network, partition,
687                                     latchInputList, 0);
688    lsDestroy(latchInputList, (void (*)(lsGeneric))0);
689  }
690
691  for (i=0;i<array_n(latchNameArray);i++){
692    name = array_fetch(char *, latchNameArray, i);
693    node = Ntk_NetworkFindNodeByName(network, name);
694    psMddId = Ntk_NodeReadMddId(node);
695    nsMddId = Ntk_NodeReadMddId(Ntk_NodeReadShadow(node));
696
697    dataInputName = Ntk_NodeReadName(Ntk_LatchReadDataInput(node));
698
699    if (st_is_member(initialLatchNameTable, name)) { 
700      vertex = Part_PartitionFindVertexByName(partition, dataInputName);
701      mvf = Part_VertexReadFunction(vertex);     
702      singleTR = Mvf_FunctionBuildRelationWithVariable(mvf, nsMddId);
703      array_insert(mdd_t *, TRArray, i, 
704                   bdd_minimize(singleTR, imcInfo->modelCareStates));
705      array_insert(mdd_t *, lowerTRArray, i, NIL(mdd_t));
706      array_insert(Mvf_Function_t *, mvfArray, i, NIL(Mvf_Function_t));
707      mdd_free(singleTR);
708    }else{
709      array_insert(Mvf_Function_t *, mvfArray, i, NIL(Mvf_Function_t));
710      array_insert(mdd_t *, lowerTRArray, i, NIL(mdd_t));
711      array_insert(mdd_t *, TRArray, i, NIL(mdd_t));
712    }
713   
714
715    if (!st_is_member(initialLatchNameTable, name)){
716      if (imcInfo->needLower && 
717         imcInfo->lowerMethod != Imc_LowerUniversalQuantification_c){
718        singleTR = array_fetch(mdd_t *, TRArray, i);
719        if (singleTR == NIL(mdd_t)){
720          vertex = Part_PartitionFindVertexByName(partition, dataInputName);
721          mvf = Part_VertexReadFunction(vertex);                 
722          singleTR = Mvf_FunctionBuildRelationWithVariable(mvf, nsMddId);
723          tempMdd = mdd_and(singleTR, imcInfo->modelCareStates, 1, 1);
724          mdd_free(singleTR);
725        }else{
726          tempMdd = mdd_and(singleTR, imcInfo->modelCareStates, 1, 1);
727        }           
728        subTR = bdd_approx_remap_ua(tempMdd,(bdd_approx_dir_t)BDD_UNDER_APPROX,
729                                    array_n(imcInfo->supportMddIdArray), 0, 1.0);
730        mdd_free(tempMdd);
731        tempMdd = bdd_minimize(subTR, imcInfo->modelCareStates);
732        mdd_free(subTR);
733        subTR = tempMdd;
734        array_insert(mdd_t *, lowerTRArray, i, subTR);
735        array_insert(Mvf_Function_t *, mvfArray, i, NIL(Mvf_Function_t));
736      }   
737    }
738
739    if (st_is_member(initialLatchNameTable, name)){
740      array_insert_last(int, includedLatchIndex, i);
741      array_insert_last(int, includedNsMddId, nsMddId);
742      array_insert_last(int, includedPsMddId, psMddId);
743    }else{
744      array_insert_last(int, excludedLatchIndex, i);
745      array_insert_last(int, excludedNsMddId, nsMddId);
746      array_insert_last(int, excludedPsMddId, psMddId);
747      st_insert(excludedPsMddIdTable, (char *)(long)psMddId, 
748                      (char *)0);
749    }     
750    bddIdArray = mdd_id_to_bdd_id_array(imcInfo->mddMgr, nsMddId);
751    latchSize = array_n(bddIdArray);
752    array_free(bddIdArray);
753    st_insert(latchNameTable, name, (char *)(long)i);
754    st_insert(nsMddIdToIndex,(char *)(long)nsMddId, (char *)(long)i); 
755    st_insert(psMddIdToIndex,(char *)(long)psMddId, (char *)(long)i);
756    array_insert(Ntk_Node_t *, latchNodeArray, i, node);
757    array_insert(int, latchSizeArray, i, latchSize);
758 
759    array_insert(int, nsMddIdArray, i, nsMddId);
760    array_insert(int, psMddIdArray, i, psMddId);
761  }
762 
763  systemInfo->latchNameTable = latchNameTable;
764  systemInfo->latchNameArray = latchNameArray;
765  systemInfo->latchNodeArray = latchNodeArray; 
766  systemInfo->nsMddIdArray = nsMddIdArray;
767  systemInfo->psMddIdArray = psMddIdArray;
768  systemInfo->inputMddIdArray = 
769    array_dup(Fsm_FsmReadInputVars(imcInfo->globalFsm));
770  systemInfo->TRArray = TRArray;
771  systemInfo->lowerTRArray = lowerTRArray;
772  systemInfo->mvfArray = mvfArray;
773  systemInfo->latchSizeArray = latchSizeArray;
774  systemInfo->nsMddIdToIndex = nsMddIdToIndex;
775  systemInfo->psMddIdToIndex = psMddIdToIndex;
776  systemInfo->excludedLatchIndex  = excludedLatchIndex;
777  systemInfo->includedLatchIndex  = includedLatchIndex; 
778  systemInfo->excludedNsMddId  = excludedNsMddId;
779  systemInfo->includedNsMddId  = includedNsMddId; 
780  systemInfo->excludedPsMddId  = excludedPsMddId; 
781  systemInfo->includedPsMddId  = includedPsMddId; 
782  systemInfo->excludedPsMddIdTable  = excludedPsMddIdTable;
783
784  imcInfo->systemInfo = systemInfo;
785}
786
787/**Function********************************************************************
788
789  Synopsis    [Free a system info.]
790
791  Description [Free a system info.]
792
793  SideEffects []
794
795  SeeAlso     []
796
797******************************************************************************/
798void
799Imc_SystemInfoFree(
800  Imc_SystemInfo_t *systemInfo)
801{
802  int i;
803  mdd_t *singleTR;
804
805  if (systemInfo->latchNameTable != NIL(st_table))
806    st_free_table(systemInfo->latchNameTable);
807  if (systemInfo->latchNameArray != NIL(array_t))
808    array_free(systemInfo->latchNameArray);
809  if (systemInfo->latchNodeArray != NIL(array_t))
810    array_free(systemInfo->latchNodeArray);
811  if (systemInfo->nsMddIdArray != NIL(array_t))
812    array_free(systemInfo->nsMddIdArray);
813  if (systemInfo->psMddIdArray != NIL(array_t))
814    array_free(systemInfo->psMddIdArray);
815  if (systemInfo->inputMddIdArray != NIL(array_t))
816    array_free(systemInfo->inputMddIdArray);
817  if (systemInfo->TRArray != NIL(array_t)){
818    for(i=0;i<array_n(systemInfo->TRArray);i++){
819      singleTR = array_fetch(mdd_t *, systemInfo->TRArray, i);
820      if (singleTR != NIL(mdd_t)){
821        mdd_free(singleTR);
822      }
823    }
824    array_free(systemInfo->TRArray);   
825  }
826
827  if (systemInfo->lowerTRArray != NIL(array_t)){
828    for(i=0;i<array_n(systemInfo->lowerTRArray);i++){
829      singleTR = array_fetch(mdd_t *, systemInfo->lowerTRArray, i);
830      if (singleTR != NIL(mdd_t)){
831        mdd_free(singleTR);
832      }
833    }
834    array_free(systemInfo->lowerTRArray);
835  }
836
837  if (systemInfo->mvfArray != NIL(array_t))
838    array_free(systemInfo->mvfArray);
839  if (systemInfo->latchSizeArray != NIL(array_t))
840    array_free(systemInfo->latchSizeArray);
841  if (systemInfo->nsMddIdToIndex != NIL(st_table))
842    st_free_table(systemInfo->nsMddIdToIndex);
843  if (systemInfo->psMddIdToIndex != NIL(st_table))
844    st_free_table(systemInfo->psMddIdToIndex);
845  if (systemInfo->excludedLatchIndex != NIL(array_t))
846    array_free(systemInfo->excludedLatchIndex);
847  if (systemInfo->includedLatchIndex != NIL(array_t))
848    array_free(systemInfo->includedLatchIndex);
849  if (systemInfo->excludedNsMddId != NIL(array_t))
850    array_free(systemInfo->excludedNsMddId);
851  if (systemInfo->includedNsMddId != NIL(array_t))
852    array_free(systemInfo->includedNsMddId);
853  if (systemInfo->excludedPsMddId != NIL(array_t))
854     array_free(systemInfo->excludedPsMddId);
855  if (systemInfo->includedPsMddId != NIL(array_t))
856     array_free(systemInfo->includedPsMddId);
857  if (systemInfo->excludedPsMddIdTable != NIL(st_table))
858    st_free_table(systemInfo->excludedPsMddIdTable);
859
860  FREE(systemInfo);
861}
862
863/**Function********************************************************************
864
865  Synopsis    [Update a system info.]
866
867  Description [Update a system info. All variables in newLatchNameTable are now
868  computed exactly.]
869
870  SideEffects []
871
872  SeeAlso     []
873
874******************************************************************************/
875void
876Imc_ImcSystemInfoUpdate(
877  Imc_Info_t *imcInfo,
878  st_table *newLatchNameTable)
879{
880  int i, nsMddId, psMddId, index;
881  char *name, *dataInputName;
882  mdd_t *singleTR;
883  st_generator *stGen;
884  Ntk_Node_t *node, *latchInput;
885  Mvf_Function_t *mvf;
886  vertex_t *vertex;
887  lsList latchInputList;
888  lsGen gen;
889  graph_t *partition = Part_NetworkReadPartition(imcInfo->network);
890  st_table *latchInputTable;
891  Imc_SystemInfo_t *systemInfo = imcInfo->systemInfo;
892
893  if ((imcInfo->partMethod == Imc_PartInc_c) &&
894      !(imcInfo->needLower && 
895        imcInfo->lowerMethod != Imc_LowerUniversalQuantification_c)){
896    latchInputTable = st_init_table(st_ptrcmp, st_ptrhash );
897    st_foreach_item(newLatchNameTable, stGen, &name, NIL(char *)){
898      node = Ntk_NetworkFindNodeByName(imcInfo->network, name);
899      latchInput = Ntk_LatchReadDataInput(node);
900      st_insert(latchInputTable, (char *)latchInput, (char *)(long)(-1));
901    }
902    latchInputList = lsCreate();
903    st_foreach_item(latchInputTable, stGen, &node, NULL){
904      lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
905    }
906    st_free_table(latchInputTable);
907    Ntk_NetworkForEachCombOutput(imcInfo->network, gen, node){
908      if (Ntk_NodeTestIsLatchInitialInput(node)){
909        lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
910      }
911    }
912    (void) Part_PartitionChangeRoots(imcInfo->network, partition,
913                                     latchInputList, 0);
914    lsDestroy(latchInputList, (void (*)(lsGeneric))0); 
915  }
916
917  if (systemInfo->excludedLatchIndex != NIL(array_t)){
918    array_free(systemInfo->excludedLatchIndex);
919    systemInfo->excludedLatchIndex = array_alloc(int, 0);
920  }
921  if (systemInfo->includedLatchIndex != NIL(array_t)){
922    array_free(systemInfo->includedLatchIndex);
923    systemInfo->includedLatchIndex = array_alloc(int, 0);
924  }
925  if (systemInfo->excludedNsMddId != NIL(array_t)){
926    array_free(systemInfo->excludedNsMddId);
927    systemInfo->excludedNsMddId = array_alloc(int, 0);
928  }
929  if (systemInfo->includedNsMddId != NIL(array_t)){
930    array_free(systemInfo->includedNsMddId);
931    systemInfo->includedNsMddId = array_alloc(int, 0);
932  }
933  if (systemInfo->excludedPsMddId != NIL(array_t)){
934     array_free(systemInfo->excludedPsMddId);
935     systemInfo->excludedPsMddId = array_alloc(int, 0);
936  }
937  if (systemInfo->includedPsMddId != NIL(array_t)){
938     array_free(systemInfo->includedPsMddId);
939     systemInfo->includedPsMddId = array_alloc(int, 0);
940  }
941  if (systemInfo->excludedPsMddIdTable != NIL(st_table)){
942    st_free_table(systemInfo->excludedPsMddIdTable);
943    systemInfo->excludedPsMddIdTable = st_init_table(st_numcmp, st_numhash);
944  }
945 
946  for(i=0;i<array_n(imcInfo->systemInfo->latchNameArray);i++){
947    name = array_fetch(char *,imcInfo->systemInfo->latchNameArray,i);
948    node = Ntk_NetworkFindNodeByName(imcInfo->network, name);
949    psMddId = Ntk_NodeReadMddId(node);
950    nsMddId = Ntk_NodeReadMddId(Ntk_NodeReadShadow(node));
951
952    if (st_is_member(newLatchNameTable, name)){
953      array_insert_last(int, systemInfo->includedLatchIndex, i);
954      array_insert_last(int, systemInfo->includedNsMddId, nsMddId);
955      array_insert_last(int, systemInfo->includedPsMddId, psMddId);
956    }else{
957      array_insert_last(int, systemInfo->excludedLatchIndex, i);
958      array_insert_last(int, systemInfo->excludedNsMddId, nsMddId);
959      array_insert_last(int, systemInfo->excludedPsMddId, psMddId);
960      st_insert(systemInfo->excludedPsMddIdTable, (char *)(long)psMddId, 
961                      (char *)0);
962    }     
963  }
964     
965  st_foreach_item(newLatchNameTable, stGen, &name, NIL(char *)){
966    st_lookup_int(imcInfo->systemInfo->latchNameTable,name, &index);
967    nsMddId = array_fetch(int, imcInfo->systemInfo->nsMddIdArray, index);
968    psMddId = array_fetch(int, imcInfo->systemInfo->psMddIdArray, index);
969
970    mvf = array_fetch(Mvf_Function_t *, imcInfo->systemInfo->mvfArray, index);
971
972    if (mvf == NIL(Mvf_Function_t)){
973      node = Ntk_NetworkFindNodeByName(imcInfo->network, name); 
974      latchInput = Ntk_LatchReadDataInput(node);
975      dataInputName = Ntk_NodeReadName(Ntk_LatchReadDataInput(node)); 
976      vertex = Part_PartitionFindVertexByName(partition, dataInputName);
977      mvf = Part_VertexReadFunction(vertex);
978    }
979
980    singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->TRArray, index);
981
982    if (singleTR == NIL(mdd_t)){ 
983      singleTR = Mvf_FunctionBuildRelationWithVariable(mvf, nsMddId);
984      array_insert(mdd_t *, imcInfo->systemInfo->TRArray, index, 
985                   bdd_minimize(singleTR, imcInfo->modelCareStates));
986
987      array_insert(Mvf_Function_t *, imcInfo->systemInfo->mvfArray, index, 
988                   NIL(Mvf_Function_t));
989      mdd_free(singleTR);
990    }
991
992    singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->lowerTRArray, index);
993    if (singleTR != NIL(mdd_t)){ 
994      mdd_free(singleTR);
995      array_insert(mdd_t *,imcInfo->systemInfo->lowerTRArray,index,NIL(mdd_t));
996    }       
997  }
998}
999
1000/**Function********************************************************************
1001
1002  Synopsis    [Initilalize an upper-bound approximate system info.]
1003
1004  Description [Initilalize an upper-bound approximate system info.]
1005
1006  SideEffects []
1007
1008  SeeAlso     []
1009
1010******************************************************************************/
1011void
1012Imc_UpperSystemInfoInitialize(
1013  Imc_Info_t *imcInfo,
1014  st_table   *latchNameTable)
1015{
1016  int                   i, index;
1017  int                   count;
1018  char                  *name;
1019  Imc_UpperSystemInfo_t *upperSystem;
1020  st_table              *globalLatchNameTable;
1021  array_t               *globalLatchNameArray;
1022  array_t               *relationArray;
1023  mdd_t                 *singleTR;
1024
1025  upperSystem = ALLOC(Imc_UpperSystemInfo_t, 1);
1026  upperSystem->systemInfo = imcInfo->systemInfo;
1027
1028  globalLatchNameTable = imcInfo->systemInfo->latchNameTable;
1029  globalLatchNameArray = imcInfo->systemInfo->latchNameArray;
1030
1031  relationArray = array_alloc(mdd_t *, st_count(latchNameTable));
1032
1033  count = 0;
1034
1035  for (i=0;i<array_n(globalLatchNameArray);i++){
1036    name = array_fetch(char *, globalLatchNameArray, i); 
1037    if (st_is_member(latchNameTable, name)){
1038      st_lookup_int(globalLatchNameTable, name, (int *)&index);
1039      singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->TRArray, index);
1040      array_insert(mdd_t *, relationArray, count++, singleTR);
1041    }
1042  }
1043
1044  Img_ClusterRelationArray(imcInfo->mddMgr, Img_Iwls95_c, Img_Backward_c,
1045                           relationArray,
1046                           imcInfo->systemInfo->psMddIdArray,
1047                           imcInfo->systemInfo->nsMddIdArray,
1048                           imcInfo->systemInfo->inputMddIdArray,
1049                           &upperSystem->bwdRealationArray,
1050                           &upperSystem->bwdSmoothVarsArray,
1051                           NIL(array_t *), 0); /* FIXED */
1052  upperSystem->fwdRealationArray = NIL(array_t);
1053  upperSystem->fwdSmoothVarsArray = NIL(array_t);
1054  upperSystem->bwdMinimizedRealationArray = NIL(array_t);
1055
1056  upperSystem->careStates = mdd_dup(imcInfo->modelCareStates);
1057
1058  array_free(relationArray);
1059 
1060  imcInfo->upperSystemInfo = upperSystem;
1061
1062  if ((imcInfo->verbosity == Imc_VerbosityMin_c) ||
1063      (imcInfo->verbosity == Imc_VerbosityMax_c)){
1064    fprintf(vis_stdout, "IMC: |BWD Upper T| = %10ld BDD nodes (%-4d components)\n",
1065      bdd_size_multiple(upperSystem->bwdRealationArray),
1066      array_n(upperSystem->bwdRealationArray));
1067  }
1068  return;
1069}
1070
1071/**Function********************************************************************
1072
1073  Synopsis    [Minimize the size of a upper-bound transition relation.]
1074
1075  Description [Minimize the size of a upper-bound transition relation with
1076  respect to a given care states.]
1077
1078  SideEffects []
1079
1080  SeeAlso     []
1081
1082******************************************************************************/
1083void
1084Imc_UpperSystemMinimize(
1085  Imc_Info_t *imcInfo,
1086  mdd_t *careStates)
1087{
1088  int i;
1089  mdd_t *singleTR;
1090  mdd_t *tempMdd;
1091  Imc_UpperSystemInfo_t *upperSystem = imcInfo->upperSystemInfo;
1092
1093  if (mdd_equal(careStates,upperSystem->careStates)) return;
1094
1095  if (upperSystem->bwdMinimizedRealationArray == NIL(array_t)){
1096    upperSystem->bwdMinimizedRealationArray = 
1097      array_alloc(mdd_t *, array_n(upperSystem->bwdRealationArray));
1098    for (i=0;i<array_n(upperSystem->bwdRealationArray);i++){
1099      array_insert(mdd_t *, upperSystem->bwdMinimizedRealationArray, i, NIL(mdd_t));
1100    }
1101  }
1102
1103  for (i=0;i<array_n(upperSystem->bwdRealationArray);i++){ 
1104    singleTR = array_fetch(mdd_t *, upperSystem->bwdMinimizedRealationArray, i);
1105    if (singleTR != NIL(mdd_t)){
1106      mdd_free(singleTR);
1107    }
1108    singleTR = array_fetch(mdd_t *, upperSystem->bwdRealationArray, i);
1109    tempMdd = bdd_minimize(singleTR, careStates);
1110    array_insert(mdd_t *, upperSystem->bwdMinimizedRealationArray, i, tempMdd);
1111  }
1112 
1113  if (upperSystem->careStates != NIL(mdd_t)){
1114    mdd_free(upperSystem->careStates);
1115  }
1116  upperSystem->careStates = mdd_dup(careStates);
1117
1118  if ((imcInfo->verbosity == Imc_VerbosityMin_c) ||
1119      (imcInfo->verbosity == Imc_VerbosityMax_c)){
1120    fprintf(vis_stdout, "IMC: |Minimized BWD Upper T| = %10ld BDD nodes (%-4d components)\n",
1121      bdd_size_multiple(upperSystem->bwdMinimizedRealationArray),
1122      array_n(upperSystem->bwdMinimizedRealationArray));
1123  }
1124
1125  return;
1126}
1127
1128/**Function********************************************************************
1129
1130  Synopsis    [Free a upper-bound approximate system info.]
1131
1132  Description [Free a upper-bound approximate system info.]
1133
1134  SideEffects []
1135
1136  SeeAlso     []
1137
1138******************************************************************************/
1139void
1140Imc_UpperSystemInfoFree(
1141  Imc_UpperSystemInfo_t *upperSystem)
1142{
1143  int i;
1144  array_t *tempArray;
1145
1146  if (upperSystem == NIL(Imc_UpperSystemInfo_t)) return;   
1147
1148  if (upperSystem->careStates != NIL(mdd_t)){
1149    mdd_free(upperSystem->careStates);
1150  }
1151
1152  if (upperSystem->fwdRealationArray != NIL(array_t)){
1153    mdd_array_free(upperSystem->fwdRealationArray);
1154    upperSystem->fwdRealationArray = NIL(array_t);
1155  }
1156  if (upperSystem->fwdSmoothVarsArray != NIL(array_t)){
1157    array_free(upperSystem->fwdSmoothVarsArray);
1158    upperSystem->fwdSmoothVarsArray = NIL(array_t);
1159  }
1160  if (upperSystem->bwdRealationArray != NIL(array_t)){
1161    mdd_array_free(upperSystem->bwdRealationArray);
1162    upperSystem->bwdRealationArray = NIL(array_t);
1163  }
1164  if (upperSystem->bwdMinimizedRealationArray != NIL(array_t)){
1165    mdd_array_free(upperSystem->bwdMinimizedRealationArray);
1166    upperSystem->bwdMinimizedRealationArray = NIL(array_t);
1167  }
1168  if (upperSystem->bwdSmoothVarsArray != NIL(array_t)){
1169    for (i=0; i<array_n(upperSystem->bwdSmoothVarsArray);i++){
1170      tempArray = array_fetch(array_t *, upperSystem->bwdSmoothVarsArray, i);
1171      mdd_array_free(tempArray);
1172    }
1173    array_free(upperSystem->bwdSmoothVarsArray);
1174    upperSystem->bwdSmoothVarsArray = NIL(array_t);
1175  }
1176
1177  FREE(upperSystem);
1178  return;
1179}
1180
1181
1182/**Function********************************************************************
1183
1184  Synopsis    [Initilalize a lower-bound approximate system info.]
1185
1186  Description [Initilalize a lower-bound approximate system info.]
1187
1188  SideEffects []
1189
1190  SeeAlso     []
1191
1192******************************************************************************/
1193void
1194Imc_LowerSystemInfoInitialize(
1195  Imc_Info_t *imcInfo,
1196  st_table   *latchNameTable)
1197{
1198  int                   i, index;
1199  char                  *name;
1200  st_generator          *stGen;
1201  mdd_t                 *singleTR;
1202  Imc_LowerSystemInfo_t *lowerSystem;
1203  array_t               *tempArray;
1204  array_t               *relationArray;
1205  st_table              *globalLatchNameTable;
1206  array_t               *latchNameArray;
1207
1208  lowerSystem = ALLOC(Imc_LowerSystemInfo_t, 1);
1209
1210  if ((imcInfo->lowerMethod == Imc_LowerUniversalQuantification_c) &&
1211      (imcInfo->upperSystemInfo != NIL(Imc_UpperSystemInfo_t))){
1212    lowerSystem->bwdRealationArray = mdd_array_duplicate(
1213      imcInfo->upperSystemInfo->bwdRealationArray);
1214    lowerSystem->bwdSmoothVarsArray = array_alloc(array_t *,
1215      array_n(imcInfo->upperSystemInfo->bwdSmoothVarsArray));
1216    for (i=0;i<array_n(imcInfo->upperSystemInfo->bwdSmoothVarsArray);i++){
1217      tempArray =  array_fetch(array_t *,
1218        imcInfo->upperSystemInfo->bwdSmoothVarsArray, i);
1219      array_insert(array_t *, lowerSystem->bwdSmoothVarsArray, i,
1220        mdd_array_duplicate(tempArray));
1221    }
1222    lowerSystem->careStates = mdd_dup(imcInfo->modelCareStates);
1223    lowerSystem->bwdMinimizedRealationArray = NIL(array_t);
1224    imcInfo->lowerSystemInfo = lowerSystem;
1225    return;
1226  }
1227
1228  globalLatchNameTable = imcInfo->systemInfo->latchNameTable;
1229
1230  latchNameArray = array_alloc(char *, 0);
1231  st_foreach_item(globalLatchNameTable, stGen, &name, NIL(char *)){
1232    array_insert_last(char *, latchNameArray, name);
1233  }
1234
1235  array_sort(latchNameArray, stringCompare);
1236
1237  relationArray = array_alloc(mdd_t *, 0);
1238
1239  for (i=0;i<array_n(latchNameArray);i++){
1240    name = array_fetch(char *, latchNameArray, i);
1241    st_lookup_int(globalLatchNameTable, name, (int *)&index);
1242    if (st_lookup(latchNameTable, name, NIL(char *))){
1243      singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->TRArray, index);
1244    }else{
1245      singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->lowerTRArray, index);
1246    }
1247    if (singleTR != NIL(mdd_t)){
1248      array_insert_last(mdd_t *, relationArray, singleTR);
1249    }
1250  }
1251
1252  array_free(latchNameArray);
1253
1254  Img_ClusterRelationArray(imcInfo->mddMgr, Img_Iwls95_c, Img_Backward_c,
1255                           relationArray,
1256                           imcInfo->systemInfo->psMddIdArray,
1257                           imcInfo->systemInfo->nsMddIdArray,
1258                           imcInfo->systemInfo->inputMddIdArray,
1259                           &lowerSystem->bwdRealationArray,
1260                           &lowerSystem->bwdSmoothVarsArray,
1261                           NIL(array_t *), 0); /* FIXED */
1262  lowerSystem->bwdMinimizedRealationArray = NIL(array_t);
1263
1264  lowerSystem->careStates = mdd_dup(imcInfo->modelCareStates);;
1265
1266  imcInfo->lowerSystemInfo = lowerSystem;
1267
1268  if ((imcInfo->verbosity == Imc_VerbosityMin_c) ||
1269      (imcInfo->verbosity == Imc_VerbosityMax_c)){
1270    fprintf(vis_stdout, "IMC: |BWD Lower T| = %10ld BDD nodes (%-4d components)\n",
1271      bdd_size_multiple(lowerSystem->bwdRealationArray),
1272      array_n(lowerSystem->bwdRealationArray));
1273  }
1274
1275  array_free(relationArray); /* Should be freed here, I guess, Chao Wang */
1276 
1277  return;
1278}
1279
1280/**Function********************************************************************
1281
1282  Synopsis    [Minimize the size of a lower-bound transition relation.]
1283
1284  Description [Minimize the size of a lower-bound transition relation with
1285  respect to a given care states.]
1286
1287  SideEffects []
1288
1289  SeeAlso     []
1290
1291******************************************************************************/
1292void
1293Imc_LowerSystemMinimize(
1294  Imc_Info_t *imcInfo,
1295  mdd_t *careStates)
1296{
1297  int i;
1298  mdd_t *singleTR;
1299  mdd_t *tempMdd;
1300
1301  Imc_LowerSystemInfo_t *lowerSystem = imcInfo->lowerSystemInfo;
1302
1303  if (mdd_equal(careStates,lowerSystem->careStates)) return;
1304
1305  if (lowerSystem->bwdMinimizedRealationArray == NIL(array_t)){
1306    lowerSystem->bwdMinimizedRealationArray = 
1307      array_alloc(mdd_t *, array_n(lowerSystem->bwdRealationArray));
1308    for (i=0;i<array_n(lowerSystem->bwdRealationArray);i++){
1309      array_insert(mdd_t *, lowerSystem->bwdMinimizedRealationArray, i, NIL(mdd_t));
1310    }
1311  } 
1312
1313  for (i=0;i<array_n(lowerSystem->bwdRealationArray);i++){
1314    singleTR = array_fetch(mdd_t *, lowerSystem->bwdMinimizedRealationArray, i);
1315    if (singleTR != NIL(mdd_t)){
1316      mdd_free(singleTR);
1317    }
1318    singleTR = array_fetch(mdd_t *, lowerSystem->bwdRealationArray, i);
1319    tempMdd = bdd_minimize(singleTR, careStates);
1320    array_insert(mdd_t *, lowerSystem->bwdMinimizedRealationArray, i, tempMdd);
1321  }
1322
1323  if (lowerSystem->careStates != NIL(mdd_t)){
1324    mdd_free(lowerSystem->careStates);
1325  }
1326
1327  lowerSystem->careStates = mdd_dup(careStates);
1328  if ((imcInfo->verbosity == Imc_VerbosityMin_c) ||
1329      (imcInfo->verbosity == Imc_VerbosityMax_c)){
1330    fprintf(vis_stdout, "IMC: |Minimized BWD Lower T| = %10ld BDD nodes (%-4d components)\n",
1331      bdd_size_multiple(lowerSystem->bwdMinimizedRealationArray),
1332      array_n(lowerSystem->bwdMinimizedRealationArray));
1333  }
1334}
1335
1336
1337/**Function********************************************************************
1338
1339  Synopsis    [Free a lower-bound approximate system info.]
1340
1341  Description [Free a lower-bound approximate system info.]
1342
1343  SideEffects []
1344
1345  SeeAlso     []
1346
1347******************************************************************************/
1348void
1349Imc_LowerSystemInfoFree(
1350  Imc_LowerSystemInfo_t *lowerSystem)
1351{
1352  int i;
1353  array_t *tempArray;
1354
1355  if (lowerSystem == NIL(Imc_LowerSystemInfo_t)) return;   
1356
1357  if (lowerSystem->careStates != NIL(mdd_t)){
1358    mdd_free(lowerSystem->careStates);
1359  }
1360
1361  if (lowerSystem->bwdRealationArray != NIL(array_t)){
1362    mdd_array_free(lowerSystem->bwdRealationArray);
1363    lowerSystem->bwdRealationArray = NIL(array_t);
1364  }
1365  if (lowerSystem->bwdMinimizedRealationArray != NIL(array_t)){
1366    mdd_array_free(lowerSystem->bwdMinimizedRealationArray);
1367    lowerSystem->bwdMinimizedRealationArray = NIL(array_t);
1368  }
1369  if (lowerSystem->bwdSmoothVarsArray != NIL(array_t)){
1370    for (i=0; i<array_n(lowerSystem->bwdSmoothVarsArray);i++){
1371      tempArray = array_fetch(array_t *, lowerSystem->bwdSmoothVarsArray, i);
1372      mdd_array_free(tempArray);
1373    }
1374    array_free(lowerSystem->bwdSmoothVarsArray);
1375    lowerSystem->bwdSmoothVarsArray = NIL(array_t); /* FIXED */
1376  }
1377
1378  FREE(lowerSystem);
1379  return;
1380}
1381
1382/**Function********************************************************************
1383
1384  Synopsis    [Initilalize node info.]
1385
1386  Description [Initilalize node info.]
1387
1388  SideEffects []
1389
1390  SeeAlso     []
1391
1392******************************************************************************/
1393Imc_NodeInfo_t *
1394Imc_NodeInfoInitialize(
1395  Imc_Polarity polarity)
1396{
1397  Imc_NodeInfo_t *nodeInfo; 
1398
1399  nodeInfo = ALLOC(Imc_NodeInfo_t, 1);
1400
1401  nodeInfo->isExact = FALSE;
1402  nodeInfo->polarity = polarity;
1403  nodeInfo->upperSat = NIL(mdd_t);
1404  nodeInfo->lowerSat = NIL(mdd_t);
1405  nodeInfo->propagatedGoalSet = NIL(mdd_t);
1406  nodeInfo->propagatedGoalSetTrue = NIL(mdd_t);
1407  nodeInfo->goalSet = NIL(mdd_t);
1408  nodeInfo->goalSetTrue = NIL(mdd_t);
1409  nodeInfo->answer = Imc_VerificationInconclusive_c;
1410  nodeInfo->upperDone = FALSE;
1411  nodeInfo->lowerDone = FALSE;
1412  nodeInfo->pseudoEdges = NIL(mdd_t);
1413  return nodeInfo;
1414}
1415
1416
1417/**Function********************************************************************
1418
1419  Synopsis    [Reset node info.]
1420
1421  Description [Reset node info.]
1422
1423  SideEffects []
1424
1425  SeeAlso     []
1426
1427******************************************************************************/
1428void
1429Imc_NodeInfoReset(
1430  Imc_Info_t *imcInfo)
1431{
1432  Ctlp_Formula_t *formula;
1433  st_table *nodeInfoTable = imcInfo->nodeInfoTable;
1434  st_generator *stGen;
1435  Imc_NodeInfo_t *nodeInfo;
1436
1437  st_foreach_item(nodeInfoTable, stGen, &formula, &nodeInfo){
1438    if (!nodeInfo->isExact){
1439      nodeInfo->lowerDone = FALSE;
1440      nodeInfo->upperDone = FALSE;
1441    }
1442    if (nodeInfo->propagatedGoalSet != NIL(mdd_t)){
1443      mdd_free(nodeInfo->propagatedGoalSet);
1444      nodeInfo->propagatedGoalSet = NIL(mdd_t);
1445    }
1446    if (nodeInfo->propagatedGoalSetTrue != NIL(mdd_t)){
1447      mdd_free(nodeInfo->propagatedGoalSetTrue);
1448      nodeInfo->propagatedGoalSetTrue = NIL(mdd_t);
1449    }
1450    if (nodeInfo->goalSet != NIL(mdd_t)){
1451      mdd_free(nodeInfo->goalSet);
1452      nodeInfo->goalSet = NIL(mdd_t);
1453    }
1454    if (nodeInfo->goalSetTrue != NIL(mdd_t)){
1455      mdd_free(nodeInfo->goalSetTrue);
1456      nodeInfo->goalSetTrue = NIL(mdd_t);
1457    }
1458    if (nodeInfo->pseudoEdges != NIL(mdd_t)){
1459      mdd_free(nodeInfo->pseudoEdges);
1460      nodeInfo->pseudoEdges = NIL(mdd_t);
1461    }   
1462  }
1463}
1464
1465
1466/**Function********************************************************************
1467
1468  Synopsis    [Free node info.]
1469
1470  Description [Free node info.]
1471
1472  SideEffects []
1473
1474  SeeAlso     []
1475
1476******************************************************************************/
1477void
1478Imc_NodeInfoFree(
1479  Imc_NodeInfo_t *nodeInfo)
1480{
1481  if (nodeInfo->upperSat != NIL(mdd_t)){
1482    mdd_free(nodeInfo->upperSat);
1483  }
1484  if (nodeInfo->lowerSat != NIL(mdd_t)){
1485    mdd_free(nodeInfo->lowerSat);
1486  }
1487  if (nodeInfo->goalSet != NIL(mdd_t)){
1488    mdd_free(nodeInfo->goalSet);
1489  }
1490  if (nodeInfo->goalSetTrue != NIL(mdd_t)){ 
1491    mdd_free(nodeInfo->goalSetTrue);
1492  }
1493  if (nodeInfo->propagatedGoalSet != NIL(mdd_t)){
1494    mdd_free(nodeInfo->propagatedGoalSet);
1495  }
1496  if (nodeInfo->propagatedGoalSetTrue != NIL(mdd_t)){ 
1497    mdd_free(nodeInfo->propagatedGoalSetTrue);
1498  }
1499  if (nodeInfo->pseudoEdges != NIL(mdd_t)){ 
1500    mdd_free(nodeInfo->pseudoEdges);
1501  }
1502  FREE(nodeInfo);
1503}
1504
1505
1506/**Function********************************************************************
1507
1508  Synopsis    [Print global system size.]
1509
1510  Description [Print global system size by multi-value and boolean value latch.]
1511
1512  SideEffects []
1513
1514  SeeAlso     []
1515
1516******************************************************************************/
1517void
1518Imc_ImcPrintSystemSize(
1519  Imc_Info_t *imcInfo)
1520{
1521  array_t *includedBooleanVars;
1522  array_t *psMddIdArray = imcInfo->systemInfo->psMddIdArray;
1523
1524  includedBooleanVars = mdd_id_array_to_bdd_id_array(imcInfo->mddMgr,
1525                        psMddIdArray);
1526
1527  fprintf(vis_stdout, "%d(%d) ",
1528          array_n(psMddIdArray), array_n(includedBooleanVars));
1529  fprintf(vis_stdout, "multi-value(boolean) latches.\n");
1530
1531  array_free(includedBooleanVars); 
1532}
1533
1534
1535/**Function********************************************************************
1536
1537  Synopsis    [Print upper-system size.]
1538
1539  Description [Print upper-system size by multi-value and boolean value latch.]
1540
1541  SideEffects []
1542
1543  SeeAlso     []
1544
1545******************************************************************************/
1546void
1547Imc_ImcPrintApproxSystemSize(
1548  Imc_Info_t *imcInfo)
1549{
1550  int i, index, psMddId;
1551  array_t *includedBooleanVars;
1552  array_t *includedPsMddIdArray;
1553  array_t *psMddIdArray = imcInfo->systemInfo->psMddIdArray;
1554  array_t *includedLatchIndex = imcInfo->systemInfo->includedLatchIndex;
1555 
1556  includedPsMddIdArray = array_alloc(int,array_n(includedLatchIndex));
1557
1558  for(i=0;i<array_n(includedLatchIndex);i++){
1559    index = array_fetch(int,includedLatchIndex, i); 
1560    psMddId = array_fetch(int, psMddIdArray, index); 
1561    array_insert(int, includedPsMddIdArray, i, psMddId);
1562  }
1563 
1564  includedBooleanVars = mdd_id_array_to_bdd_id_array(imcInfo->mddMgr,
1565                        includedPsMddIdArray);
1566
1567  fprintf(vis_stdout, "%d(%d) ",
1568          array_n(includedPsMddIdArray), array_n(includedBooleanVars));
1569  fprintf(vis_stdout, "multi-value(boolean) latches.\n");
1570
1571  array_free(includedPsMddIdArray);
1572  array_free(includedBooleanVars); 
1573}
1574
1575/**Function********************************************************************
1576
1577  Synopsis    [Get a upperbound satisfying states of a given formula.]
1578
1579  Description [Get a upperbound satisfying states of a given formula if is is
1580  already computed.]
1581 
1582  Comment     []
1583
1584  SideEffects []
1585
1586******************************************************************************/
1587mdd_t *
1588Imc_GetUpperSat(
1589  Imc_Info_t *imcInfo,
1590  Ctlp_Formula_t *formula)
1591{
1592  Imc_NodeInfo_t *nodeInfo;
1593
1594  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
1595    return NIL(mdd_t); 
1596  }
1597
1598  return nodeInfo->upperSat;
1599}
1600
1601/**Function********************************************************************
1602
1603  Synopsis    [Get a lowerbound satisfying states of a given formula.]
1604
1605  Description [Get a lowerbound satisfying states of a given formula if is is
1606  already computed.]
1607 
1608  Comment     []
1609
1610  SideEffects []
1611
1612******************************************************************************/
1613mdd_t *
1614Imc_GetLowerSat(
1615  Imc_Info_t *imcInfo,
1616  Ctlp_Formula_t *formula)
1617{
1618  Imc_NodeInfo_t *nodeInfo;
1619
1620  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
1621    return NIL(mdd_t); 
1622  }
1623
1624  return nodeInfo->lowerSat;
1625}
1626
1627/**Function********************************************************************
1628
1629  Synopsis    [Model check formula with approxmiations.]
1630
1631  Description [The routine evaluates given formula with approximations.
1632  If polarity is set, upper approximation is computed. Otherwise, lower
1633  approximation is computed.]
1634 
1635  Comment     []
1636
1637  SideEffects []
1638
1639******************************************************************************/
1640int 
1641Imc_ImcEvaluateCTLFormula(
1642  Imc_Info_t            *imcInfo,
1643  Ctlp_Formula_t        *ctlFormula, 
1644  Imc_Polarity          polarity)
1645{
1646  Imc_Polarity newPolarity, approxPolarity;
1647  Ctlp_Formula_t *leftChild, *rightChild;
1648  Imc_NodeInfo_t *nodeInfo;
1649  Imc_GraphType graphType = imcInfo->graphType;
1650
1651  if (Ctlp_FormulaReadType( ctlFormula ) == Ctlp_NOT_c){
1652    newPolarity = (polarity == Imc_PolarityNeg_c) ? Imc_PolarityPos_c: 
1653                  (polarity == Imc_PolarityPos_c) ? Imc_PolarityNeg_c:
1654                  polarity;
1655  }else{
1656    newPolarity = polarity;
1657  }
1658
1659  if (graphType == Imc_GraphNDOG_c){
1660    /* In-Ho : Why change the polarity ? */
1661    approxPolarity = (polarity == Imc_PolarityNeg_c) ? Imc_PolarityPos_c:
1662                     Imc_PolarityNeg_c;
1663  }else{
1664    approxPolarity = polarity;
1665  } 
1666
1667  if (!st_lookup(imcInfo->nodeInfoTable, ctlFormula, &nodeInfo)){
1668    nodeInfo = Imc_NodeInfoInitialize(polarity);
1669    st_insert(imcInfo->nodeInfoTable, ctlFormula, nodeInfo);
1670  }else if ((nodeInfo->isExact) ||
1671            ((approxPolarity == Imc_PolarityNeg_c) && (nodeInfo->lowerDone)) ||
1672            ((approxPolarity == Imc_PolarityPos_c) && (nodeInfo->upperDone))){
1673    if (imcInfo->verbosity == Imc_VerbosityMax_c){
1674      if ((Ctlp_FormulaReadType( ctlFormula ) == Ctlp_ID_c ) ||
1675          (Ctlp_FormulaReadType( ctlFormula ) == Ctlp_TRUE_c ) ||
1676          (Ctlp_FormulaReadType( ctlFormula ) == Ctlp_FALSE_c )){ 
1677        fprintf(vis_stdout, "IMC : node simple already computed.\n");
1678      }else if ((Ctlp_FormulaReadType( ctlFormula ) == Ctlp_AND_c ) ||
1679                (Ctlp_FormulaReadType( ctlFormula ) == Ctlp_NOT_c )){ 
1680        fprintf(vis_stdout, "IMC : node boolean already computed.\n");
1681      }else{
1682        /* In-Ho : Why only ECTL? */
1683        fprintf(vis_stdout, "IMC : node ECTL already computed.\n");
1684      }
1685    }
1686    return 1;
1687  }
1688 
1689  leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
1690  if (leftChild) {
1691    if (!Imc_ImcEvaluateCTLFormula(imcInfo,leftChild,newPolarity)){
1692       return 0;
1693    } 
1694  }
1695  rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
1696  if (rightChild) {
1697    if (!Imc_ImcEvaluateCTLFormula(imcInfo,rightChild,newPolarity)){ 
1698       return 0;
1699    } 
1700  }
1701
1702  switch ( Ctlp_FormulaReadType( ctlFormula ) ) {
1703
1704    case Ctlp_ID_c : 
1705      if (!ImcModelCheckAtomicFormula(imcInfo,ctlFormula)) return 0; 
1706      break;
1707    case Ctlp_TRUE_c : 
1708      if (!ImcModelCheckTrueFalseFormula(imcInfo,ctlFormula, TRUE)) return 0; 
1709      break;
1710    case Ctlp_FALSE_c : 
1711      if (!ImcModelCheckTrueFalseFormula(imcInfo,ctlFormula, FALSE)) return 0;
1712      break;
1713    case Ctlp_NOT_c :
1714      if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){
1715              if (!ImcModelCheckNotFormula(imcInfo,ctlFormula, TRUE)) return 0;
1716      }
1717      if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){
1718              if(!ImcModelCheckNotFormula(imcInfo,ctlFormula, FALSE)) return 0;
1719      } 
1720      break;
1721    case Ctlp_AND_c :
1722      if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){       
1723        if (!ImcModelCheckAndFormula(imcInfo,ctlFormula,TRUE))return 0;
1724      }
1725      if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){
1726        if (!ImcModelCheckAndFormula(imcInfo,ctlFormula,FALSE)) return 0;
1727      }   
1728      break;
1729    case Ctlp_EX_c :
1730      if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){
1731        if (!Imc_ImcEvaluateEXApprox(imcInfo,ctlFormula, TRUE, FALSE)) return 0;
1732      }
1733      if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){
1734        if (!Imc_ImcEvaluateEXApprox(imcInfo,ctlFormula, FALSE, FALSE)) return 0;
1735      }
1736      break;
1737
1738    case Ctlp_EU_c :
1739      if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){ 
1740        if (!Imc_ImcEvaluateEUApprox(imcInfo,ctlFormula,TRUE, FALSE)) return 0;
1741      }
1742      if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){
1743        if (!Imc_ImcEvaluateEUApprox(imcInfo,ctlFormula, FALSE, FALSE)) return 0;
1744      }
1745      break;
1746
1747    case Ctlp_EG_c :
1748      if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){
1749        if (!Imc_ImcEvaluateEGApprox(imcInfo,ctlFormula,TRUE, FALSE)) return 0;
1750      }
1751      if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){
1752        if (!Imc_ImcEvaluateEGApprox(imcInfo,ctlFormula, FALSE, FALSE)) return 0;
1753      } 
1754      break;
1755
1756    default: fail("Encountered unknown type of CTL formula\n");
1757  }
1758
1759  if (nodeInfo->upperDone && nodeInfo->lowerDone){
1760    if (!nodeInfo->isExact && mdd_equal_mod_care_set(nodeInfo->upperSat, 
1761         nodeInfo->lowerSat, imcInfo->modelCareStates)){ /* FIXED */
1762      nodeInfo->isExact = TRUE;
1763    }
1764  }
1765
1766  return 1;
1767}
1768
1769/**Function********************************************************************
1770
1771  Synopsis      [Evaluate EX formula with approximations.]
1772
1773  Description   [Evaluate EX formula with approximations. If isUpper is set,
1774  a superset of exact satisfying states of EG formula is computed. Otherwise,
1775  a subset is computed.]
1776
1777  SideEffects   []
1778
1779  SeeAlso       []
1780
1781******************************************************************************/
1782int
1783Imc_ImcEvaluateEXApprox(
1784  Imc_Info_t *imcInfo,
1785  Ctlp_Formula_t *formula,
1786  boolean isUpper,
1787  boolean isRecomputation)
1788{
1789  mdd_t *targetStates;
1790  Ctlp_Formula_t *leftChild;
1791  mdd_t *result = NIL(mdd_t);
1792  mdd_t *tempResult;
1793  mdd_t *localCareStates;
1794  mdd_t *globalCareStates;
1795  boolean useLocalCare = FALSE;
1796  Imc_NodeInfo_t *nodeInfo, *lNodeInfo;
1797  boolean isExact;
1798 
1799  globalCareStates = imcInfo->modelCareStates;
1800
1801  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
1802    fprintf(vis_stdout, "** imc error : EX nodeinfo is not initilize.\n");
1803    return 0;
1804  }
1805
1806  leftChild = Ctlp_FormulaReadLeftChild(formula);
1807  if (!st_lookup(imcInfo->nodeInfoTable, leftChild, &lNodeInfo)){
1808    fprintf(vis_stdout, "** imc error : EX left nodeinfo is not initilize.\n");
1809    return 0;
1810  }
1811
1812  if ( imcInfo->verbosity == Imc_VerbosityMax_c ){     
1813     if (isUpper){
1814      fprintf(vis_stdout, "IMC :  SAT(EX)+ computation start.\n");
1815    }else{
1816      fprintf(vis_stdout, "IMC :  SAT(EX)- computation start.\n");
1817    }
1818  }
1819
1820  /*
1821   * If exact sat is already computed from other side of approximation,
1822   * use it.
1823   */
1824  if (nodeInfo->isExact){
1825    if ( imcInfo->verbosity == Imc_VerbosityMax_c ){     
1826      if (isUpper){
1827        fprintf(vis_stdout, "IMC :  SAT(EX)+ computation end.\n");
1828      }else{
1829        fprintf(vis_stdout, "IMC :  SAT(EX)- computation end.\n");
1830      }
1831    }
1832    return 1;
1833  }
1834
1835
1836  /*
1837   * If this is not for recomputation, do general satisfying states computation.
1838   * Otherwise, compute the subset of the propagated goalset where the formula
1839   * satisfies.
1840   * Test if tighter satisfying don't care states(ASDC) can be used to reduce
1841   * transition sub-relations.
1842   */
1843  if (nodeInfo->upperSat != NIL(mdd_t)){
1844    localCareStates = mdd_and(nodeInfo->upperSat,globalCareStates, 1, 1); 
1845  }else{
1846    localCareStates = mdd_dup(globalCareStates);
1847  }
1848
1849  if ((mdd_lequal(localCareStates,globalCareStates, 1, 1)) &&
1850      (!mdd_equal(localCareStates,globalCareStates))){
1851    useLocalCare = TRUE;
1852  }
1853
1854  if (!isRecomputation){
1855    if (isUpper){
1856      targetStates = lNodeInfo->upperSat;
1857    }else{
1858      targetStates = lNodeInfo->lowerSat;
1859    }
1860  }else{
1861    targetStates = lNodeInfo->propagatedGoalSetTrue;
1862  }
1863
1864  if (targetStates == NIL(mdd_t)) return 0;
1865
1866  if ((isUpper)|| (isRecomputation)) 
1867    Imc_UpperSystemMinimize(imcInfo, localCareStates);
1868  else
1869    Imc_LowerSystemMinimize(imcInfo, localCareStates); 
1870
1871  if ((isUpper) || (isRecomputation)){
1872    tempResult = Imc_ComputeUpperPreimage(imcInfo, localCareStates, targetStates, 
1873                                          &isExact);
1874  }else{
1875    tempResult = Imc_ComputeLowerPreimage(imcInfo, localCareStates, targetStates, 
1876                                          &isExact);
1877  }
1878
1879  if (tempResult == NIL(mdd_t)) return 0;
1880
1881  if ((imcInfo->verbosity == Imc_VerbosityMax_c) ||
1882      (imcInfo->verbosity == Imc_VerbosityMin_c)) {
1883    mdd_t *tmpMdd = mdd_and(tempResult, localCareStates, 1, 1 );
1884    double minterm = mdd_count_onset(imcInfo->mddMgr, tmpMdd, 
1885              imcInfo->systemInfo->psMddIdArray);
1886    if (isUpper){
1887      fprintf(vis_stdout, "IMC : |SAT(EX)+| = %.0f (%10g)\n", minterm, minterm);
1888    }else{
1889      fprintf(vis_stdout, "IMC : |SAT(EX)-| = %.0f (%10g)\n", minterm, minterm);
1890    }
1891    mdd_free(tmpMdd);
1892  }
1893
1894  if (useLocalCare){
1895     result = mdd_and(tempResult, localCareStates, 1, 1); 
1896     mdd_free(tempResult);
1897     tempResult = bdd_minimize(result, globalCareStates);
1898     mdd_free(result);
1899     result = tempResult;
1900  }else{
1901     result = tempResult;
1902  }
1903
1904  mdd_free(localCareStates);
1905
1906  if (isRecomputation){
1907    tempResult = mdd_and(nodeInfo->goalSet, result, 1, 1);
1908    mdd_free(result);
1909    nodeInfo->propagatedGoalSetTrue = 
1910      mdd_or(nodeInfo->goalSetTrue, tempResult, 1, 1);
1911    mdd_free(tempResult);
1912    return 1;
1913  }
1914
1915  if (isUpper){
1916    if (nodeInfo->upperSat != NIL(mdd_t)){
1917      mdd_free(nodeInfo->upperSat);
1918    }
1919    nodeInfo->upperSat = result;
1920    nodeInfo->upperDone = TRUE;
1921  }else{
1922    if (nodeInfo->lowerSat != NIL(mdd_t)){
1923      tempResult = mdd_or(nodeInfo->lowerSat, result, 1, 1);
1924      mdd_free(nodeInfo->lowerSat);
1925      mdd_free(result);
1926      result = tempResult;
1927    }
1928    nodeInfo->lowerSat = result;
1929    nodeInfo->lowerDone = TRUE;
1930  }
1931
1932  if ( imcInfo->verbosity == Imc_VerbosityMax_c ){     
1933    if (isUpper){
1934      fprintf(vis_stdout, "IMC :  SAT(EX)+ computation end.\n");
1935    }else{
1936      fprintf(vis_stdout, "IMC :  SAT(EX)- computation end.\n");
1937    }
1938  }
1939
1940  if (lNodeInfo->isExact && isExact){
1941    nodeInfo->isExact = TRUE;
1942    if ( imcInfo->verbosity == Imc_VerbosityMax_c ){
1943      if (isUpper){
1944        fprintf(vis_stdout, "IMC :  SAT(EX)+ computation is exact.\n");
1945      }else{
1946        fprintf(vis_stdout, "IMC :  SAT(EX)- computation is exact.\n");
1947      }
1948    }     
1949    if (isUpper){
1950      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
1951      nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat);
1952      nodeInfo->lowerDone = TRUE;
1953    }else{
1954      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
1955      nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat);
1956      nodeInfo->upperDone = TRUE;
1957    } 
1958  }else{
1959    nodeInfo->isExact = FALSE;
1960  } 
1961
1962  return 1;
1963}
1964
1965/**Function********************************************************************
1966
1967  Synopsis    [Evaluate EU formula with approximations.]
1968
1969  Description [Evaluate EU formula with approximations. If isUpper is set,
1970  a superset of exact satisfying states of EG formula is computed. Otherwise,
1971  a subset is computed.]
1972
1973  Comment     []
1974
1975  SideEffects []
1976
1977******************************************************************************/
1978int
1979Imc_ImcEvaluateEUApprox(
1980  Imc_Info_t *imcInfo,
1981  Ctlp_Formula_t *formula,
1982  boolean isUpper,
1983  boolean isRecomputation)
1984{
1985  mdd_t *localCareStates;
1986  mdd_t *targetStates, *invariantStates;
1987  mdd_t *aMdd, *bMdd, *cMdd;
1988  mdd_t *result;
1989  mdd_t *tmpMdd1, *tmpMdd2;
1990  mdd_t * globalCareStates;
1991  double size1, size2;
1992  Ctlp_Formula_t *lFormula, *rFormula;
1993  Imc_NodeInfo_t *nodeInfo, *lNodeInfo, *rNodeInfo;
1994  boolean isExact, globalIsExact;
1995
1996  globalIsExact = TRUE;
1997  globalCareStates = imcInfo->modelCareStates;
1998  lFormula = Ctlp_FormulaReadLeftChild(formula);
1999  rFormula = Ctlp_FormulaReadRightChild(formula);
2000
2001  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
2002    fprintf(vis_stdout, "** imc error : EU nodeinfo is not initilize.\n");
2003    return 0;
2004  }
2005  if (!st_lookup(imcInfo->nodeInfoTable, lFormula, &lNodeInfo)){
2006    fprintf(vis_stdout, "** imc error : EU left nodeinfo is not initilize.\n");
2007    return 0;
2008  }
2009  if (!st_lookup(imcInfo->nodeInfoTable, rFormula, &rNodeInfo)){
2010    fprintf(vis_stdout, "** imc error : EU right nodeinfo is not initilize.\n");
2011    return 0;
2012  }
2013
2014  if ( imcInfo->verbosity == Imc_VerbosityMax_c ){     
2015    if (isUpper){
2016      fprintf(vis_stdout, "IMC :  SAT(EU)+ computation start.\n");
2017    }else{
2018      fprintf(vis_stdout, "IMC :  SAT(EU)- computation start.\n");
2019    }
2020  }
2021
2022  /*
2023   * If exact sat is already computed from other side of approximation,
2024   * use it.
2025   */
2026  if (nodeInfo->isExact){
2027    if ( imcInfo->verbosity == Imc_VerbosityMax_c ){     
2028      if (isUpper){
2029        fprintf(vis_stdout, "IMC :  SAT(EU)+ computation end.\n");
2030      }else{
2031        fprintf(vis_stdout, "IMC :  SAT(EU)- computation end.\n");
2032      }
2033    }
2034    return 1;
2035  }
2036
2037
2038  /*
2039   * Test if tighter satisfying don't care states(ASDC) can be used to reduce
2040   * transition sub-relations.
2041   */
2042 
2043  if (nodeInfo->upperSat != NIL(mdd_t)){
2044    localCareStates = mdd_and(nodeInfo->upperSat,globalCareStates, 1, 1); 
2045  }else{
2046    localCareStates = mdd_dup(globalCareStates);
2047  }
2048
2049  if ((mdd_lequal(localCareStates,globalCareStates, 1, 1)) &&
2050      (!mdd_equal(localCareStates,globalCareStates))){
2051  }
2052
2053  if (!isRecomputation){
2054    if (isUpper){
2055      if (nodeInfo->lowerSat != NIL(mdd_t)){
2056        targetStates = mdd_or(rNodeInfo->upperSat, nodeInfo->lowerSat, 1, 1);
2057      }else{
2058        targetStates = mdd_dup(rNodeInfo->upperSat);
2059      }
2060      invariantStates = lNodeInfo->upperSat;
2061    }else{
2062      targetStates = mdd_dup(rNodeInfo->lowerSat);
2063      invariantStates = lNodeInfo->lowerSat;
2064    }
2065  }else{
2066    targetStates = mdd_dup(rNodeInfo->propagatedGoalSetTrue);
2067    invariantStates = lNodeInfo->propagatedGoalSetTrue;   
2068  }
2069
2070  result = targetStates;
2071
2072  if ((isUpper) || (isRecomputation))
2073    Imc_UpperSystemMinimize(imcInfo, localCareStates);
2074  else
2075    Imc_LowerSystemMinimize(imcInfo, localCareStates);
2076
2077  while (TRUE) { 
2078
2079    if (isUpper){
2080      aMdd = Imc_ComputeUpperPreimage(imcInfo, localCareStates, 
2081                                      result, &isExact);     
2082    }else{
2083      aMdd = Imc_ComputeLowerPreimage(imcInfo, localCareStates, 
2084                                      result, &isExact);
2085    }
2086    if (aMdd == NIL(mdd_t)) return 0;
2087
2088    globalIsExact = (globalIsExact && isExact);
2089
2090    bMdd = mdd_and( aMdd, invariantStates, 1, 1 );
2091    mdd_free( aMdd );
2092    aMdd = mdd_and(bMdd, localCareStates, 1, 1);
2093    mdd_free(bMdd);
2094    bMdd = bdd_minimize(aMdd, globalCareStates);
2095    mdd_free(aMdd);
2096    cMdd = mdd_or(result, bMdd, 1, 1);
2097    mdd_free( bMdd );
2098   
2099    tmpMdd1 = mdd_and( result, globalCareStates, 1, 1 );
2100    tmpMdd2 = mdd_and( cMdd, globalCareStates, 1, 1 );
2101    if (mdd_equal(tmpMdd1, tmpMdd2)){
2102      mdd_free(cMdd);
2103      break;
2104    }else if (mdd_equal(tmpMdd2, localCareStates)){ 
2105      mdd_free(result);
2106      result = cMdd;     
2107      break;
2108    }else if (( imcInfo->verbosity == Imc_VerbosityMax_c ) ||
2109              (imcInfo->verbosity == Imc_VerbosityMin_c)) { 
2110      size1 = mdd_count_onset(imcInfo->mddMgr, tmpMdd1,
2111                               imcInfo->systemInfo->psMddIdArray);
2112      size2 = mdd_count_onset(imcInfo->mddMgr, tmpMdd2,
2113                               imcInfo->systemInfo->psMddIdArray);
2114      if (isUpper){
2115        fprintf(vis_stdout, "IMC : |SAT(EU)+| = %.0f (%10g)-> %.0f (%10g)\n", 
2116                size1, size1, size2, size2);
2117      }else{
2118        fprintf(vis_stdout, "IMC : |SAT(EU)-| = %.0f (%10g)-> %.0f (%10g)\n", 
2119                size1, size1, size2, size2);
2120      }
2121    }     
2122    mdd_free(tmpMdd1);
2123    mdd_free(tmpMdd2);
2124
2125    mdd_free( result );
2126    result = bdd_minimize(cMdd, globalCareStates);
2127    mdd_free(cMdd);
2128  }
2129
2130  if ((imcInfo->verbosity == Imc_VerbosityMax_c) ||
2131      (imcInfo->verbosity == Imc_VerbosityMin_c)) {
2132    size1 = mdd_count_onset(imcInfo->mddMgr, tmpMdd1,
2133                             imcInfo->systemInfo->psMddIdArray);
2134    size2 = mdd_count_onset(imcInfo->mddMgr, tmpMdd2,
2135                       imcInfo->systemInfo->psMddIdArray);   
2136    if (isUpper){
2137      fprintf(vis_stdout, "IMC : |SAT(EU)+| = %.0f (%10g)-> %.0f (%10g)\n", 
2138              size1, size1, size2, size2);
2139    }else{
2140      fprintf(vis_stdout, "IMC : |SAT(EU)-| = %.0f (%10g)-> %.0f (%10g)\n", 
2141              size1, size1, size2, size2);
2142    }
2143  }
2144
2145  mdd_free(tmpMdd1);
2146  mdd_free(tmpMdd2);
2147
2148  mdd_free(localCareStates);
2149
2150  if (isRecomputation){
2151    tmpMdd1 = mdd_and(nodeInfo->goalSet, result, 1, 1);
2152    mdd_free(result);
2153    nodeInfo->propagatedGoalSetTrue = mdd_or(nodeInfo->goalSetTrue, tmpMdd1, 1, 1);
2154    mdd_free(tmpMdd1);
2155    return 1;
2156  }
2157
2158  if (isUpper){
2159    if (nodeInfo->upperSat != NIL(mdd_t)){
2160      mdd_free(nodeInfo->upperSat);
2161    }
2162    nodeInfo->upperSat = result;
2163    nodeInfo->upperDone = TRUE;
2164  }else{
2165    if (nodeInfo->lowerSat != NIL(mdd_t)){
2166      tmpMdd1 = mdd_or(nodeInfo->lowerSat, result, 1, 1);
2167      mdd_free(nodeInfo->lowerSat);
2168      mdd_free(result);
2169      result = tmpMdd1;
2170    }
2171    nodeInfo->lowerSat = result;
2172    nodeInfo->lowerDone = TRUE;
2173  } 
2174
2175  if ( imcInfo->verbosity == Imc_VerbosityMax_c ){     
2176    if (isUpper){
2177      fprintf(vis_stdout, "IMC :  SAT(EU)+ computation end.\n");
2178    }else{
2179      fprintf(vis_stdout, "IMC :  SAT(EU)- computation end.\n");
2180    }
2181  }
2182
2183  if (lNodeInfo->isExact && rNodeInfo->isExact && globalIsExact){
2184    nodeInfo->isExact = TRUE;
2185    if ( imcInfo->verbosity == Imc_VerbosityMax_c ){
2186      if (isUpper){
2187        fprintf(vis_stdout, "IMC :  SAT(EU)+ computation is exact.\n");
2188      }else{
2189        fprintf(vis_stdout, "IMC :  SAT(EU)- computation is exact.\n");
2190      }
2191    }   
2192    if (isUpper){
2193      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
2194      nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat);
2195      nodeInfo->lowerDone = TRUE;
2196    }else{
2197      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
2198      nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat);
2199      nodeInfo->upperDone = TRUE;
2200    } 
2201  }else{
2202    nodeInfo->isExact = FALSE;
2203  } 
2204
2205  return 1;
2206}
2207
2208/**Function********************************************************************
2209
2210  Synopsis    [Evaluate EG formula with approximations.]
2211
2212  Description [Evaluate EG formula with approximations. If isUpper is set,
2213  a superset of exact satisfying states of EG formula is computed. Otherwise,
2214  a subset is computed.]
2215
2216  SideEffects []
2217
2218******************************************************************************/
2219int
2220Imc_ImcEvaluateEGApprox( 
2221  Imc_Info_t *imcInfo,
2222  Ctlp_Formula_t *formula,
2223  boolean isUpper,
2224  boolean isRecomputation)
2225{
2226  mdd_t *Zmdd;
2227  mdd_t *bMdd;
2228  mdd_t *ZprimeMdd;
2229  mdd_t *tmpMdd1, *tmpMdd2;
2230  mdd_t *result;
2231  mdd_t *localCareStates;
2232  mdd_t *globalCareStates;
2233  mdd_t *invariantStates;
2234  double size1, size2;
2235  Ctlp_Formula_t *lFormula;
2236  Imc_NodeInfo_t *nodeInfo, *lNodeInfo;
2237  boolean isExact, globalIsExact;
2238 
2239
2240  lFormula = Ctlp_FormulaReadLeftChild(formula);
2241
2242  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
2243    fprintf(vis_stdout, "** imc error : EG nodeinfo is not initilize.\n");
2244    return 0;
2245  }
2246  if (!st_lookup(imcInfo->nodeInfoTable, lFormula, &lNodeInfo)){
2247    fprintf(vis_stdout, "** imc error : EG left nodeinfo is not initilize.\n");
2248    return 0;
2249  }
2250
2251  if ( imcInfo->verbosity == Imc_VerbosityMax_c ){     
2252    if (isUpper){
2253      fprintf(vis_stdout, "IMC :  SAT(EG)+ computation start.\n");
2254    }else{
2255      fprintf(vis_stdout, "IMC :  SAT(EG)- computation start.\n");
2256    }
2257  }
2258
2259  /*
2260   * If exact sat is already computed from other side of approximation,
2261   * use it.
2262   */
2263  if (nodeInfo->isExact){
2264    if ( imcInfo->verbosity == Imc_VerbosityMax_c ){     
2265      if (isUpper){
2266        fprintf(vis_stdout, "IMC :  SAT(EG)+ computation end.\n");
2267      }else{
2268        fprintf(vis_stdout, "IMC :  SAT(EG)- computation end.\n");
2269      }
2270    }
2271    return 1;
2272  }
2273
2274  globalCareStates = imcInfo->modelCareStates;
2275
2276  /*
2277   * Test if tighter satisfying don't care states(ASDC) can be used to reduce
2278   * transition sub-relations.
2279   */
2280  if (nodeInfo->upperSat != NIL(mdd_t)){ 
2281    localCareStates = mdd_and(nodeInfo->upperSat,globalCareStates, 1, 1); 
2282  }else{
2283    localCareStates = mdd_dup(globalCareStates);
2284  }
2285
2286  if ((mdd_lequal(localCareStates,globalCareStates, 1, 1)) &&
2287      (!mdd_equal(localCareStates,globalCareStates))){
2288  }
2289
2290  if (!isRecomputation){
2291    if (isUpper){
2292      if (nodeInfo->upperSat != NIL(mdd_t)){
2293        invariantStates = mdd_and(lNodeInfo->upperSat, nodeInfo->upperSat,1,1);
2294      }else{
2295        invariantStates = mdd_dup(lNodeInfo->upperSat);
2296      } 
2297    }else{
2298      if (nodeInfo->upperSat != NIL(mdd_t)){
2299        invariantStates = mdd_and(lNodeInfo->lowerSat, nodeInfo->upperSat,1,1);
2300      }else{
2301        invariantStates = mdd_dup(lNodeInfo->lowerSat);
2302      }
2303    }
2304  }else{
2305    invariantStates = mdd_dup(lNodeInfo->propagatedGoalSetTrue);
2306  }
2307
2308  Zmdd = mdd_dup(invariantStates);
2309  ZprimeMdd = NIL(mdd_t);
2310
2311  globalIsExact = TRUE;
2312
2313  if ((isUpper) || (isRecomputation))
2314    Imc_UpperSystemMinimize(imcInfo, localCareStates);
2315  else
2316    Imc_LowerSystemMinimize(imcInfo, localCareStates);
2317
2318  while (TRUE) {
2319
2320    if (isUpper){
2321      bMdd = Imc_ComputeUpperPreimage(imcInfo, localCareStates, 
2322                                      Zmdd, &isExact);
2323    }else{
2324      bMdd = Imc_ComputeLowerPreimage(imcInfo, localCareStates, 
2325                                      Zmdd, &isExact);
2326    }
2327    if (bMdd == NIL(mdd_t)){
2328      mdd_free(invariantStates);
2329      mdd_free(Zmdd);
2330      if (ZprimeMdd !=NIL(mdd_t)) mdd_free(ZprimeMdd);
2331      return 0;
2332    }
2333
2334    ZprimeMdd = mdd_and(Zmdd, bMdd, 1, 1);
2335    globalIsExact = (globalIsExact && isExact);
2336
2337    mdd_free(bMdd);
2338   
2339    tmpMdd1 = mdd_and( Zmdd, globalCareStates, 1, 1 );
2340    tmpMdd2 = mdd_and( ZprimeMdd, localCareStates, 1, 1 );
2341
2342    mdd_free(Zmdd);
2343    mdd_free(ZprimeMdd);
2344
2345    if ((mdd_equal(tmpMdd1, tmpMdd2)) ||
2346        (mdd_is_tautology(tmpMdd2, 0))){
2347      break;
2348    }else if (( imcInfo->verbosity == Imc_VerbosityMax_c ) ||
2349              (imcInfo->verbosity == Imc_VerbosityMin_c)) {     
2350      size1 = mdd_count_onset(imcInfo->mddMgr, tmpMdd1,
2351                               imcInfo->systemInfo->psMddIdArray);
2352      size2 = mdd_count_onset(imcInfo->mddMgr, tmpMdd2,
2353                               imcInfo->systemInfo->psMddIdArray);
2354      if (isUpper){
2355        fprintf(vis_stdout, "IMC : |SAT(EG)+| = %.0f (%10g)-> %.0f (%10g)\n", 
2356                size1, size1, size2, size2);
2357      }else{
2358        fprintf(vis_stdout, "IMC : |SAT(EG)-| = %.0f (%10g)-> %.0f (%10g)\n", 
2359                size1, size1, size2, size2);
2360      }
2361    }
2362
2363    mdd_free(tmpMdd1);
2364    Zmdd = bdd_minimize(tmpMdd2, globalCareStates);
2365    mdd_free(tmpMdd2);
2366  }
2367       
2368  if (( imcInfo->verbosity == Imc_VerbosityMax_c ) ||
2369      (imcInfo->verbosity == Imc_VerbosityMin_c)) {
2370    size1 = mdd_count_onset(imcInfo->mddMgr, tmpMdd1,
2371                             imcInfo->systemInfo->psMddIdArray);
2372    size2 = mdd_count_onset(imcInfo->mddMgr, tmpMdd2,
2373                             imcInfo->systemInfo->psMddIdArray);
2374    if (isUpper){
2375      fprintf(vis_stdout, "IMC : |SAT(EG)+| = %.0f (%10g)-> %.0f (%10g)\n", 
2376              size1, size1, size2, size2);
2377    }else{
2378      fprintf(vis_stdout, "IMC : |SAT(EG)-| = %.0f (%10g)-> %.0f (%10g)\n", 
2379              size1, size1, size2, size2);
2380    }
2381  }
2382
2383  mdd_free(tmpMdd1);
2384  mdd_free(localCareStates);
2385
2386  result = bdd_minimize(tmpMdd2, globalCareStates);
2387  mdd_free(tmpMdd2);
2388
2389  if (isRecomputation){
2390    tmpMdd1 = mdd_and(nodeInfo->goalSet, result, 1, 1);
2391    mdd_free(result);
2392    nodeInfo->propagatedGoalSetTrue = mdd_or(nodeInfo->goalSetTrue,tmpMdd1,1,1);
2393    mdd_free(tmpMdd1);
2394    return 1;
2395  }
2396
2397  mdd_free(invariantStates);
2398
2399  if (isUpper){
2400    if (nodeInfo->upperSat != NIL(mdd_t)){
2401      mdd_free(nodeInfo->upperSat);
2402    }
2403    nodeInfo->upperSat = result;
2404    nodeInfo->upperDone = TRUE;
2405  }else{
2406    if (nodeInfo->lowerSat != NIL(mdd_t)){
2407      tmpMdd1 = mdd_or(nodeInfo->lowerSat, result, 1, 1);
2408      mdd_free(nodeInfo->lowerSat);
2409      mdd_free(result);
2410      result = bdd_minimize(tmpMdd1, globalCareStates);
2411      mdd_free(tmpMdd1);
2412    }
2413    nodeInfo->lowerSat = result;
2414    nodeInfo->lowerDone = TRUE;
2415  } 
2416
2417  if ( imcInfo->verbosity == Imc_VerbosityMax_c ){     
2418    if (isUpper){
2419      fprintf(vis_stdout, "IMC :  SAT(EG)+ computation end.\n");
2420    }else{
2421      fprintf(vis_stdout, "IMC :  SAT(EG)- computation end.\n");
2422    }
2423  }
2424
2425  if (lNodeInfo->isExact && globalIsExact){
2426    nodeInfo->isExact = TRUE;
2427    if ( imcInfo->verbosity == Imc_VerbosityMax_c ){
2428      if (isUpper){
2429        fprintf(vis_stdout, "IMC :  SAT(EG)+ computation is exact.\n");
2430      }else{
2431        fprintf(vis_stdout, "IMC :  SAT(EG)- computation is exact.\n");
2432      }
2433    }   
2434    if (isUpper){
2435      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
2436      nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat);
2437      nodeInfo->lowerDone = TRUE;
2438    }else{
2439      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
2440      nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat);
2441      nodeInfo->upperDone = TRUE;
2442    } 
2443  }else{
2444    nodeInfo->isExact = FALSE;
2445  } 
2446
2447  return 1;
2448}
2449
2450/**Function*******************************************************************
2451
2452  Synopsis [Compte a supperset of exact pre image.]
2453
2454  Description [Compte a supperset of exact pre image. If result is exact pre
2455  image, isExact is set.]
2456
2457  SideEffects []
2458
2459******************************************************************************/
2460mdd_t *
2461Imc_ComputeUpperPreimage(
2462  Imc_Info_t *imcInfo,
2463  mdd_t *rangeCareStates,
2464  mdd_t *targetStates,
2465  boolean *isExact)
2466{
2467  if (imcInfo->upperMethod == Imc_UpperExistentialQuantification_c){
2468    return Imc_ComputeApproxPreimageByQuantification(imcInfo, rangeCareStates,
2469             targetStates, isExact, FALSE);
2470  }
2471
2472  return NIL(mdd_t);
2473}
2474
2475
2476/**Function*******************************************************************
2477
2478  Synopsis [Compte a superset or a subset of exact pre image.]
2479
2480  Description [Compte a superset or a subset of exact pre image accrding to
2481  computeLower parameter. If result is exact pre image, isExact is set.]
2482
2483  SideEffects []
2484
2485******************************************************************************/
2486mdd_t *
2487Imc_ComputeApproxPreimageByQuantification(
2488  Imc_Info_t *imcInfo, 
2489  mdd_t *rangeCareStates, 
2490  mdd_t *targetStates,
2491  boolean *isExact,
2492  boolean computeLower)
2493{
2494  int i;
2495  int psMddId;
2496  double orgSize, newSize;
2497  mdd_t *result;
2498  mdd_t *nextTarget;
2499  mdd_t *reducedTarget;
2500  mdd_t *tempMdd;
2501  mdd_t *reducedTargetInCare;
2502  mdd_t *targetInCare;
2503  array_t *supportArray;
2504
2505  *isExact = TRUE;
2506  if (mdd_is_tautology(targetStates, 0)){
2507    return mdd_zero(imcInfo->mddMgr);
2508  }
2509
2510  supportArray = mdd_get_support(imcInfo->mddMgr, targetStates);
2511
2512  for(i=0;i<array_n(supportArray);i++){
2513    psMddId = array_fetch(int, supportArray, i);
2514    if (st_is_member(imcInfo->systemInfo->excludedPsMddIdTable, 
2515                     (char *)(long)psMddId)){
2516      *isExact = FALSE;
2517      break;
2518    }
2519  }
2520  array_free(supportArray);
2521 
2522  if (array_n(imcInfo->systemInfo->excludedPsMddId) >0){
2523    if (!computeLower){
2524      reducedTarget = mdd_smooth(imcInfo->mddMgr, targetStates, 
2525                               imcInfo->systemInfo->excludedPsMddId);
2526    }else{
2527      reducedTarget = mdd_consensus(imcInfo->mddMgr, targetStates, 
2528                               imcInfo->systemInfo->excludedPsMddId);
2529    }
2530    if ((mdd_is_tautology(reducedTarget,1)) || (mdd_is_tautology(reducedTarget,0))){
2531      return reducedTarget;
2532    }
2533  }else{
2534    reducedTarget = mdd_dup(targetStates);
2535  }
2536
2537  if (imcInfo->verbosity == Imc_VerbosityMax_c){
2538    targetInCare = mdd_and(targetStates, imcInfo->modelCareStates, 1, 1);
2539    reducedTargetInCare = mdd_and(reducedTarget, imcInfo->modelCareStates, 1, 1);
2540    orgSize = mdd_count_onset(imcInfo->mddMgr, targetInCare,
2541                        imcInfo->systemInfo->psMddIdArray);
2542    newSize = mdd_count_onset(imcInfo->mddMgr, reducedTargetInCare,
2543                          imcInfo->systemInfo->psMddIdArray);
2544    if (!computeLower){
2545      fprintf(vis_stdout, "IMC : Upper Approximation    |S| = %.0f (%10g)-> %.0f (%10g)\n",
2546              orgSize, orgSize, newSize, newSize);
2547    }else{
2548      fprintf(vis_stdout, "IMC : Lower Approximation    |S| = %.0f (%10g)-> %.0f (%10g)\n",
2549              orgSize, orgSize, newSize, newSize);
2550    }
2551    mdd_free(targetInCare);
2552    mdd_free(reducedTargetInCare);
2553  }
2554
2555  nextTarget = mdd_substitute(imcInfo->mddMgr, reducedTarget,
2556                              imcInfo->systemInfo->psMddIdArray,
2557                              imcInfo->systemInfo->nsMddIdArray);
2558
2559  mdd_free(reducedTarget);
2560
2561  if (!computeLower){
2562    if (imcInfo->upperSystemInfo->bwdMinimizedRealationArray == NIL(array_t)){
2563      result = Imc_ProductAbstract(imcInfo->mddMgr, 
2564                                   imcInfo->upperSystemInfo->bwdRealationArray,
2565                                   imcInfo->upperSystemInfo->bwdSmoothVarsArray,
2566                                   nextTarget);
2567    }else{
2568      result = Imc_ProductAbstract(imcInfo->mddMgr, 
2569                                   imcInfo->upperSystemInfo->bwdMinimizedRealationArray,
2570                                   imcInfo->upperSystemInfo->bwdSmoothVarsArray,
2571                                   nextTarget);
2572    }
2573  }else{
2574    if (imcInfo->lowerSystemInfo->bwdMinimizedRealationArray == NIL(array_t)){
2575      result = Imc_ProductAbstract(imcInfo->mddMgr, 
2576                                   imcInfo->lowerSystemInfo->bwdRealationArray,
2577                                   imcInfo->lowerSystemInfo->bwdSmoothVarsArray,
2578                                   nextTarget);
2579    }else{
2580      result = Imc_ProductAbstract(imcInfo->mddMgr, 
2581                                   imcInfo->lowerSystemInfo->bwdMinimizedRealationArray,
2582                                   imcInfo->lowerSystemInfo->bwdSmoothVarsArray,
2583                                   nextTarget);
2584    }
2585  }
2586
2587  mdd_free(nextTarget);
2588
2589  if (imcInfo->verbosity == Imc_VerbosityMax_c){
2590    double exactSize, approxSize;
2591    tempMdd = mdd_and(result, rangeCareStates, 1, 1); 
2592    approxSize = mdd_count_onset(imcInfo->mddMgr, result,
2593                    imcInfo->systemInfo->psMddIdArray);
2594    exactSize = mdd_count_onset(imcInfo->mddMgr, tempMdd,
2595                      imcInfo->systemInfo->psMddIdArray);
2596    mdd_free(tempMdd);
2597    if (!computeLower){
2598      fprintf(vis_stdout, "IMC : Upper Preimage      |S+DC| = %.0f (%10g)\n",
2599              approxSize, approxSize);
2600      fprintf(vis_stdout, "IMC : Upper Preimage         |S| = %.0f (%10g)\n",
2601              exactSize, exactSize);
2602    }else{
2603      fprintf(vis_stdout, "IMC : Lower Preimage      |S+DC| = %.0f (%10g)\n",
2604              approxSize, approxSize);
2605      fprintf(vis_stdout, "IMC : Lower Preimage         |S| = %.0f (%10g)\n",
2606              exactSize, exactSize);
2607    } 
2608  }
2609
2610  /*
2611   * If preimage is zero, don't need compute again
2612   */
2613  if (mdd_is_tautology(result,0)){
2614    *isExact = TRUE;
2615  }
2616
2617  return result;
2618}
2619
2620/**Function*******************************************************************
2621
2622  Synopsis [Compte a subset of exact pre image.]
2623
2624  Description [Compte a subset of exact pre image. If result is exact pre
2625  image, isExact is set.]
2626
2627  SideEffects []
2628
2629******************************************************************************/
2630mdd_t *
2631Imc_ComputeLowerPreimage(
2632  Imc_Info_t *imcInfo,
2633  mdd_t *rangeCareStates,
2634  mdd_t *targetStates,
2635  boolean *isExact)
2636{
2637  if (imcInfo->lowerMethod == Imc_LowerSubsetTR_c){
2638    return Imc_ComputeLowerPreimageBySubsetTR(imcInfo, rangeCareStates,
2639                                                targetStates, isExact);
2640  }else if (imcInfo->lowerMethod == Imc_LowerUniversalQuantification_c){
2641    return Imc_ComputeApproxPreimageByQuantification(imcInfo, rangeCareStates,
2642             targetStates, isExact, TRUE);
2643  }
2644
2645  return NIL(mdd_t);
2646}
2647
2648
2649/**Function*******************************************************************
2650
2651  Synopsis [Compte a subset of exact pre image by subsetting some transition
2652  sub-relations.]
2653
2654  Description [Compte a subset of exact pre image by subsetting some transition
2655  sub-relations. If result is exact pre image, isExact is set.]
2656
2657  SideEffects []
2658
2659******************************************************************************/
2660mdd_t *
2661Imc_ComputeLowerPreimageBySubsetTR(
2662  Imc_Info_t *imcInfo,
2663  mdd_t *rangeCareStates,
2664  mdd_t *targetStates,
2665  boolean *isExact)
2666{
2667  mdd_t *tempMdd, *result;
2668  mdd_t *toStates;
2669
2670  *isExact = TRUE;
2671
2672  if (mdd_is_tautology(targetStates,0)){
2673    return mdd_zero(imcInfo->mddMgr);
2674  }
2675
2676  if (mdd_is_tautology(targetStates, 1)){
2677    return mdd_one(imcInfo->mddMgr);
2678  }
2679
2680  /*
2681   * T_i is T_i for all included latches.
2682   */
2683
2684  /*arrayOfMdd = array_alloc(mdd_t *, 0); never used, I guess. Chao Wang*/
2685
2686  toStates = mdd_substitute(imcInfo->mddMgr, targetStates,
2687                            imcInfo->systemInfo->psMddIdArray,
2688                            imcInfo->systemInfo->nsMddIdArray);
2689
2690  /* Not works with partitioned transition relation
2691  supportArray = mdd_get_support(imcInfo->mddMgr, targetStates);
2692
2693  for(i=0;i<array_n(supportArray);i++){
2694    psMddId = array_fetch(int, supportArray,i);
2695
2696    if (st_is_member(imcInfo->systemInfo->excludedPsMddIdTable,
2697        (char *)(long)psMddId)){
2698      *isExact = FALSE;
2699    }
2700  }
2701  array_free(supportArray);
2702  */
2703  if (st_count(imcInfo->systemInfo->excludedPsMddIdTable)>0){
2704    *isExact = FALSE;
2705  }
2706
2707  if (imcInfo->lowerSystemInfo->bwdMinimizedRealationArray == NIL(array_t)){
2708    result = Imc_ProductAbstract(imcInfo->mddMgr,
2709                                 imcInfo->lowerSystemInfo->bwdRealationArray,
2710                                 imcInfo->lowerSystemInfo->bwdSmoothVarsArray,
2711                                 toStates);
2712  }else{
2713    result = Imc_ProductAbstract(imcInfo->mddMgr,
2714                                 imcInfo->lowerSystemInfo->bwdMinimizedRealationArray,
2715                                 imcInfo->lowerSystemInfo->bwdSmoothVarsArray,
2716                                 toStates);
2717  }
2718
2719  mdd_free(toStates);
2720
2721  if (imcInfo->verbosity == Imc_VerbosityMax_c){
2722    double exactSize, approxSize;
2723    tempMdd = mdd_and(result, rangeCareStates, 1, 1); 
2724    approxSize = mdd_count_onset(imcInfo->mddMgr, result,
2725                    imcInfo->systemInfo->psMddIdArray);
2726    exactSize = mdd_count_onset(imcInfo->mddMgr, tempMdd,
2727                      imcInfo->systemInfo->psMddIdArray);
2728    mdd_free(tempMdd);
2729    fprintf(vis_stdout, "IMC : Lower Preimage      |S+DC| = %.0f (%10g)\n",
2730            approxSize, approxSize);
2731    fprintf(vis_stdout, "IMC : Lower Preimage         |S| = %.0f (%10g)\n",
2732            exactSize, exactSize);
2733  }
2734
2735  return result;
2736}
2737
2738/**Function********************************************************************
2739
2740  Synopsis           [Compute a product of relation array. All variables in
2741  smoothVarsMddIdArray are quntified during product.]
2742
2743  Description        [Compute a product of relation array. All variables in
2744  smoothVarsMddIdArray are quntified during product.]
2745
2746  SideEffects        []
2747
2748  SeeAlso            []
2749
2750******************************************************************************/
2751mdd_t *
2752Imc_ProductAbstract(
2753  mdd_manager *mddMgr,
2754  array_t *relationArray,
2755  array_t *smoothVarsMddIdArray,
2756  mdd_t *toStates)
2757{
2758  int i;
2759  mdd_t *product, *tempProd;
2760  mdd_t *singleTR;
2761  array_t *smoothVars;
2762
2763  product = mdd_dup(toStates);
2764
2765  for(i=0;i<array_n(relationArray);i++){
2766    singleTR = array_fetch(mdd_t *, relationArray, i);
2767    smoothVars = array_fetch(array_t*, smoothVarsMddIdArray, i);
2768    if (array_n(smoothVars) == 0){
2769      tempProd = mdd_and(product, singleTR, 1, 1);
2770    }else{
2771      tempProd = bdd_and_smooth(product, singleTR, smoothVars);
2772    }
2773    mdd_free(product);
2774    product = tempProd;
2775  }
2776  if (i < array_n(smoothVarsMddIdArray)) {
2777    smoothVars = array_fetch(array_t*, smoothVarsMddIdArray, i);
2778    tempProd = bdd_smooth(product, smoothVars);
2779    mdd_free(product);
2780    product = tempProd;
2781  }
2782
2783  return product; 
2784}
2785
2786
2787/*---------------------------------------------------------------------------*/
2788/* Definition of internal functions                                          */
2789/*---------------------------------------------------------------------------*/
2790
2791/**Function********************************************************************
2792
2793  Synopsis           [Create an refinement schedule array.]
2794
2795  Description        [If dynamicIncrease is true, the first element of return
2796  array includes varibales appered in formula. The size of the first element
2797  should be less than or equal to incrementalSize. The second element includes
2798  all variables in formula's cone of influence. When dynamicIncrease is false,
2799  all vaiables in formula's cone of influence (let's say n variables) are
2800  partitioned into ceil(n/incrementalSize) elements. Then one more element
2801  which includes all n variables are added to return array.]
2802
2803  SideEffects        []
2804
2805  SeeAlso            [Part_SubsystemInfo_t]
2806
2807******************************************************************************/
2808array_t *
2809ImcCreateScheduleArray(
2810  Ntk_Network_t         *network,
2811  Ctlp_Formula_t        *formula,
2812  boolean               dynamicIncrease,
2813  Imc_RefineMethod      refine,
2814  int                   verbosity,
2815  int                   incrementalSize,
2816  Part_CMethod          correlationMethod)
2817{
2818  array_t               *partitionArray;
2819  Part_Subsystem_t      *partitionSubsystem;
2820  Part_SubsystemInfo_t  *subsystemInfo; 
2821  st_table              *latchNameTable;
2822  st_table              *latchNameTableSum, *latchNameTableSumCopy;
2823  int                   i;
2824  char                  *flagValue;
2825  st_generator          *stGen;
2826  char                  *name;
2827  array_t               *ctlArray;
2828  double                affinityFactor;
2829  array_t               *scheduleArray;
2830  boolean               dynamicAndDependency;
2831  array_t               *tempArray, *tempArray2;
2832  int                   count;
2833
2834  /* affinity factor to decompose state space */
2835  flagValue = Cmd_FlagReadByName("part_group_affinity_factor");
2836  if(flagValue != NIL(char)){
2837    affinityFactor = atof(flagValue); 
2838  }
2839  else{
2840    /* default value */
2841    affinityFactor = 0.5; 
2842  }
2843
2844  if (refine == Imc_RefineSort_c) dynamicAndDependency = TRUE;
2845  else dynamicAndDependency = FALSE;
2846
2847  /*
2848   * Obtain submachines as array.
2849   * The first sub-system includes variables in CTL formulas and other
2850   * latches are groupted in the same way as Part_PartCreateSubsystems()
2851   */
2852  ctlArray = array_alloc(Ctlp_Formula_t *, 1);
2853  subsystemInfo = Part_PartitionSubsystemInfoInit(network);
2854  Part_PartitionSubsystemInfoSetBound(subsystemInfo, incrementalSize);
2855  Part_PartitionSubsystemInfoSetVerbosity(subsystemInfo, verbosity);
2856  Part_PartitionSubsystemInfoSetCorrelationMethod(subsystemInfo,
2857    correlationMethod); 
2858  Part_PartitionSubsystemInfoSetAffinityFactor(subsystemInfo, affinityFactor);
2859  array_insert(Ctlp_Formula_t *, ctlArray, 0, formula);
2860
2861  partitionArray = Part_PartCreateSubsystemsWithCTL(subsystemInfo,
2862                   ctlArray, NIL(array_t), dynamicIncrease,dynamicAndDependency);
2863  Part_PartitionSubsystemInfoFree(subsystemInfo);
2864  array_free(ctlArray);
2865  scheduleArray = array_alloc(st_table *, 0);
2866
2867
2868  /*
2869   * For each partitioned submachines build an FSM.
2870   */
2871  latchNameTableSum = st_init_table(strcmp, st_strhash);
2872  if (!dynamicAndDependency){
2873    for (i=0;i<array_n(partitionArray);i++){
2874      partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, i);
2875      if (partitionSubsystem != NIL(Part_Subsystem_t)) {
2876        latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
2877        st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
2878          if (!st_lookup(latchNameTableSum, name, NIL(char *))){ 
2879            st_insert(latchNameTableSum, name, NIL(char));
2880          }
2881        }
2882        Part_PartitionSubsystemFree(partitionSubsystem);
2883      } 
2884      latchNameTableSumCopy = st_copy(latchNameTableSum);
2885      array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
2886    }
2887  }else{
2888    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 0);
2889    latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
2890    st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
2891      st_insert(latchNameTableSum, name, NIL(char));
2892    }
2893    latchNameTableSumCopy = st_copy(latchNameTableSum);
2894    array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
2895    Part_PartitionSubsystemFree(partitionSubsystem);
2896
2897    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 1);
2898    tempArray = array_alloc(char *, 0);   
2899    if (partitionSubsystem != NIL(Part_Subsystem_t)){
2900      latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
2901      st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
2902        array_insert_last(char *, tempArray, name);
2903      }
2904      array_sort(tempArray, stringCompare);
2905      Part_PartitionSubsystemFree(partitionSubsystem);
2906    }
2907   
2908    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 2);
2909    tempArray2 = array_alloc(char *, 0);
2910    if (partitionSubsystem != NIL(Part_Subsystem_t)) {
2911      latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
2912      st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
2913        array_insert_last(char *, tempArray2, name);
2914      }
2915      array_sort(tempArray2, stringCompare);
2916      Part_PartitionSubsystemFree(partitionSubsystem);
2917    }
2918
2919    array_append(tempArray, tempArray2);
2920    array_free(tempArray2);
2921
2922    count = 0;
2923    arrayForEachItem(char *, tempArray, i, name){   
2924      if (!st_lookup(latchNameTableSum, name, NIL(char *))){ 
2925        st_insert(latchNameTableSum, (char *)name, (char *)0);
2926        count++;
2927      }
2928      if ((count == incrementalSize) && (i < array_n(tempArray)-1)){
2929        latchNameTableSumCopy = st_copy(latchNameTableSum);
2930        array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
2931        count = 0;
2932      }
2933    }
2934    array_free(tempArray);
2935    latchNameTableSumCopy = st_copy(latchNameTableSum);
2936    array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
2937  }
2938
2939  array_free(partitionArray);
2940  st_free_table(latchNameTableSum);
2941
2942  return scheduleArray;
2943}
2944
2945
2946/**Function********************************************************************
2947
2948  Synopsis    [Find Mdd for states satisfying Atomic Formula.]
2949
2950  Description [This is a duplicate copy of static function,
2951  ModelCheckAtomicFormula(). ]
2952
2953  SideEffects []
2954
2955******************************************************************************/
2956int
2957ImcModelCheckAtomicFormula(
2958  Imc_Info_t *imcInfo, 
2959  Ctlp_Formula_t *formula)
2960{
2961  mdd_t * resultMdd;
2962  mdd_t *tmpMdd;
2963  Fsm_Fsm_t *modelFsm = imcInfo->globalFsm;
2964  Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm );
2965  char *nodeNameString = Ctlp_FormulaReadVariableName( formula );
2966  char *nodeValueString = Ctlp_FormulaReadValueName( formula );
2967  Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
2968  Var_Variable_t *nodeVar;
2969  int nodeValue;
2970  graph_t *modelPartition;
2971  vertex_t *partitionVertex;
2972  Mvf_Function_t *MVF;
2973  Imc_NodeInfo_t *nodeInfo;
2974
2975  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
2976    fprintf(vis_stdout, "** imc error : Atomic nodeinfo is not initilize.\n");
2977    return 0;
2978  }
2979
2980  nodeVar = Ntk_NodeReadVariable( node );
2981  if ( Var_VariableTestIsSymbolic( nodeVar ) ){
2982    nodeValue = Var_VariableReadIndexFromSymbolicValue( nodeVar, nodeValueString );
2983  }
2984  else {
2985    nodeValue = atoi( nodeValueString );
2986  } 
2987
2988  modelPartition = Part_NetworkReadPartition( network );
2989  if ( !( partitionVertex = Part_PartitionFindVertexByName( modelPartition,
2990                                                            nodeNameString ) )) { 
2991    lsGen tmpGen;
2992    Ntk_Node_t *tmpNode;
2993    array_t *mvfArray;
2994    array_t *tmpRoots = array_alloc( Ntk_Node_t *, 0 );
2995    st_table *tmpLeaves = st_init_table( st_ptrcmp, st_ptrhash );
2996    array_insert_last( Ntk_Node_t *, tmpRoots, node );
2997
2998    Ntk_NetworkForEachCombInput( network, tmpGen, tmpNode ) {
2999      st_insert( tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED );
3000    }
3001
3002    mvfArray =  Ntm_NetworkBuildMvfs( network, tmpRoots, tmpLeaves,
3003                                      NIL(mdd_t) );
3004    MVF = array_fetch( Mvf_Function_t *, mvfArray, 0 );
3005    array_free( tmpRoots );
3006    st_free_table( tmpLeaves );
3007    array_free( mvfArray );
3008
3009    tmpMdd = Mvf_FunctionReadComponent( MVF, nodeValue );
3010    resultMdd = mdd_dup( tmpMdd );
3011    Mvf_FunctionFree( MVF );
3012  }
3013  else {
3014    MVF = Part_VertexReadFunction( partitionVertex );
3015    tmpMdd = Mvf_FunctionReadComponent( MVF, nodeValue );
3016    resultMdd = mdd_dup( tmpMdd );
3017  }
3018
3019  tmpMdd = bdd_minimize(resultMdd, imcInfo->modelCareStates);
3020  mdd_free(resultMdd);
3021  resultMdd = tmpMdd;
3022
3023  nodeInfo->upperSat = resultMdd;
3024  nodeInfo->lowerSat = mdd_dup(resultMdd);
3025  nodeInfo->upperDone = TRUE;
3026  nodeInfo->lowerDone = TRUE;
3027  nodeInfo->isExact = TRUE;
3028  return 1; 
3029}
3030
3031/**Function********************************************************************
3032
3033  Synopsis    [Compute TRUE or FALSE expression.]
3034
3035  Description [Compute TRUE or FALSE expression.]
3036
3037  SideEffects []
3038
3039******************************************************************************/
3040int
3041ImcModelCheckTrueFalseFormula(
3042  Imc_Info_t *imcInfo, 
3043  Ctlp_Formula_t *formula,
3044  boolean isTrue)
3045{
3046  mdd_t *resultMdd;
3047  Imc_NodeInfo_t *nodeInfo;
3048
3049  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
3050    fprintf(vis_stdout, "** imc error : TRUE or FALSE nodeinfo is not initilize.\n");
3051    return 0;
3052  }
3053
3054  /*
3055   * Already computed, then return.
3056   */
3057  if (nodeInfo->isExact) return 1;
3058
3059  if (isTrue)
3060    resultMdd = mdd_one(imcInfo->mddMgr);
3061  else
3062    resultMdd = mdd_zero(imcInfo->mddMgr);
3063
3064  nodeInfo->upperSat = resultMdd;
3065  nodeInfo->lowerSat = mdd_dup(resultMdd); 
3066  nodeInfo->upperDone = TRUE;
3067  nodeInfo->lowerDone = TRUE;
3068  nodeInfo->isExact = TRUE;
3069  return 1;
3070}
3071
3072/**Function********************************************************************
3073
3074  Synopsis    [Compute NOT expression.]
3075
3076  Description [Compute NOT expression.]
3077
3078  SideEffects []
3079
3080******************************************************************************/
3081int
3082ImcModelCheckNotFormula(
3083  Imc_Info_t *imcInfo, 
3084  Ctlp_Formula_t *formula,
3085  boolean isUpper
3086  )
3087{
3088  mdd_t *upperSAT, *lowerSAT;
3089  Ctlp_Formula_t *leftChild;
3090  Imc_NodeInfo_t *nodeInfo, *leftNodeInfo;
3091
3092  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
3093    return 0;
3094  }
3095
3096
3097  leftChild = Ctlp_FormulaReadLeftChild(formula);
3098  if (!st_lookup(imcInfo->nodeInfoTable, leftChild, &leftNodeInfo)){
3099    fprintf(vis_stdout, "** imc error : NOT nodeinfo is not initilize.\n");
3100    return 0;
3101  }
3102
3103
3104  if (isUpper){
3105    if  (leftNodeInfo->lowerSat == NIL(mdd_t)){
3106      return 0;
3107    }else{
3108      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
3109      upperSAT = mdd_not(leftNodeInfo->lowerSat);
3110      nodeInfo->upperSat = upperSAT;
3111      nodeInfo->upperDone = TRUE;
3112    }
3113  }else{
3114    if  (leftNodeInfo->upperSat == NIL(mdd_t)){
3115      return 0;
3116    }else{
3117      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
3118      lowerSAT = mdd_not(leftNodeInfo->upperSat);
3119      nodeInfo->lowerSat = lowerSAT;
3120      nodeInfo->lowerDone = TRUE;
3121    }
3122  }
3123
3124  if (leftNodeInfo->isExact){
3125    nodeInfo->isExact = TRUE;
3126    if (isUpper){
3127      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
3128      nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat);
3129      nodeInfo->lowerDone = TRUE;
3130    }else{
3131      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
3132      nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat);
3133      nodeInfo->upperDone = TRUE;
3134    }
3135  }
3136
3137  return 1;
3138}
3139
3140/**Function********************************************************************
3141
3142  Synopsis    [Compute AND expression.]
3143
3144  Description [Compute AND expression.]
3145
3146  SideEffects []
3147
3148******************************************************************************/
3149int
3150ImcModelCheckAndFormula(
3151  Imc_Info_t *imcInfo, 
3152  Ctlp_Formula_t *formula,
3153  boolean isUpper)
3154{
3155  mdd_t *tmpMdd;
3156  mdd_t *upperSat, *lowerSat;
3157  Ctlp_Formula_t *leftChild, *rightChild;
3158  Imc_NodeInfo_t *nodeInfo, *leftNodeInfo, *rightNodeInfo;
3159
3160  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
3161    return 0;
3162  }
3163
3164  /*
3165   * Already computed, then return.
3166   */
3167  if (nodeInfo->isExact) return 1;
3168
3169  leftChild = Ctlp_FormulaReadLeftChild(formula);
3170  rightChild = Ctlp_FormulaReadRightChild(formula);
3171  if (!st_lookup(imcInfo->nodeInfoTable, leftChild, &leftNodeInfo)){
3172    fprintf(vis_stdout, "** imc error : AND left nodeinfo is not initilize.\n");
3173    return 0;
3174  }
3175  if (!st_lookup(imcInfo->nodeInfoTable, rightChild, &rightNodeInfo)){
3176    fprintf(vis_stdout, "** imc error : AND right nodeinfo is not initilize.\n");
3177    return 0;
3178  } 
3179
3180  /*
3181   * Already computed, then return.
3182   */
3183  if (isUpper){
3184    if ((leftNodeInfo->upperSat == NIL(mdd_t))||
3185        (rightNodeInfo->upperSat == NIL(mdd_t))){
3186      fprintf(vis_stdout, "** imc error : AND child nodeinfo->upperSat is not computed.\n");
3187      return 0;
3188    }else{
3189      tmpMdd = mdd_and(leftNodeInfo->upperSat,rightNodeInfo->upperSat, 1, 1);
3190      upperSat = bdd_minimize(tmpMdd, imcInfo->modelCareStates);
3191      mdd_free(tmpMdd);
3192      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
3193      nodeInfo->upperSat = upperSat;
3194      nodeInfo->upperDone = TRUE;
3195    }
3196  }else{
3197    if ((leftNodeInfo->lowerSat == NIL(mdd_t))||
3198        (rightNodeInfo->lowerSat == NIL(mdd_t))){
3199      fprintf(vis_stdout, "** imc error : AND child nodeinfo->lowerSat is not computed.\n");
3200      return 0;
3201    }else{
3202      tmpMdd = mdd_and(leftNodeInfo->lowerSat,rightNodeInfo->lowerSat, 1, 1);
3203     
3204      lowerSat = bdd_minimize(tmpMdd, imcInfo->modelCareStates);
3205      mdd_free(tmpMdd);
3206      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
3207      nodeInfo->lowerSat = lowerSat;
3208      nodeInfo->lowerDone = TRUE;
3209    }
3210  }
3211
3212  if ((leftNodeInfo->isExact) && (rightNodeInfo->isExact)){
3213    nodeInfo->isExact = TRUE;
3214    if (isUpper){
3215      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
3216      nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat);
3217      nodeInfo->lowerDone = TRUE;
3218    }else{
3219      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
3220      nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat);
3221      nodeInfo->upperDone = TRUE;
3222    }
3223  }
3224
3225  return 1;
3226}
3227
3228/**Function********************************************************************
3229
3230  Synopsis    [Print latch names in an upper approximate system.]
3231
3232  Description [Print latch names in an upper approximate system.]
3233
3234  SideEffects []
3235
3236******************************************************************************/
3237void
3238ImcPrintLatchInApproxSystem(
3239  Imc_Info_t *imcInfo)
3240{
3241  int i, index;
3242  char *name;
3243  array_t *includedLatchIndex = imcInfo->systemInfo->includedLatchIndex;
3244
3245  fprintf(vis_stdout, "Latches in approximate system\n");
3246  fprintf(vis_stdout, "-----------------------------\n");
3247
3248  for(i=0;i<array_n(includedLatchIndex);i++){
3249    index = array_fetch(int,includedLatchIndex,i);
3250    name = array_fetch(char *, imcInfo->systemInfo->latchNameArray, index);
3251    fprintf(vis_stdout, "%s\n", name);
3252  }
3253}
3254
3255/**Function********************************************************************
3256
3257  Synopsis    [Free node info table.]
3258
3259  Description [Free node info table.]
3260
3261  SideEffects []
3262
3263******************************************************************************/
3264void
3265ImcNodeInfoTableFree(
3266  st_table *nodeInfoTable)
3267{
3268  Ctlp_Formula_t *formula;
3269  Imc_NodeInfo_t *nodeInfo;
3270  st_generator *stGen;
3271
3272  st_foreach_item(nodeInfoTable, stGen, &formula, &nodeInfo){
3273    Imc_NodeInfoFree(nodeInfo);
3274  }
3275
3276  st_free_table(nodeInfoTable);
3277}
3278
3279/*---------------------------------------------------------------------------*/
3280/* Definition of static functions                                            */
3281/*---------------------------------------------------------------------------*/
3282
3283/**Function********************************************************************
3284
3285  Synopsis [Compare two strings]
3286
3287  SideEffects []
3288
3289******************************************************************************/
3290static int
3291stringCompare(
3292  const void * s1,
3293  const void * s2)
3294{
3295  return(strcmp(*(char **)s1, *(char **)s2));
3296}
3297
Note: See TracBrowser for help on using the repository browser.