source: vis_dev/vis-2.3/src/amc/amcBlock.c @ 57

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

vis2.3
File size: 44.5 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [amcBlock.c]
4
5  PackageName [amc]
6
7  Synopsis    [Implementation of the block-tearing abstraction.]
8
9  Author      [Woohyuk Lee]
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 "amcInt.h"
18#include "mcInt.h"
19
20static char rcsid[] UNUSED = "$Id: amcBlock.c,v 1.35 2005/04/25 20:24:53 fabio Exp $";
21
22/*---------------------------------------------------------------------------*/
23/* Constant declarations                                                     */
24/*---------------------------------------------------------------------------*/
25
26/*---------------------------------------------------------------------------*/
27/* Structure declarations                                                    */
28/*---------------------------------------------------------------------------*/
29
30/**Struct**********************************************************************
31
32  Synopsis    [Block tearing specific information.]
33
34  Description []
35
36******************************************************************************/
37struct BlockInfoStruct {
38  Amc_SubsystemInfo_t   *optimalSystem; /* temporary storage for Block method */
39  int                   bestSystem;     /* temporary storage for Block method */
40};
41
42struct BlockSubsystemInfoStruct {
43  int           scheduledForRefinement;
44};
45
46
47/*---------------------------------------------------------------------------*/
48/* Type declarations                                                         */
49/*---------------------------------------------------------------------------*/
50typedef struct BlockInfoStruct BlockInfo_t;
51typedef struct BlockSubsystemInfoStruct BlockSubsystemInfo_t;
52
53/*---------------------------------------------------------------------------*/
54/* Variable declarations                                                     */
55/*---------------------------------------------------------------------------*/
56
57/*---------------------------------------------------------------------------*/
58/* Macro declarations                                                        */
59/*---------------------------------------------------------------------------*/
60
61/**AutomaticStart*************************************************************/
62
63/*---------------------------------------------------------------------------*/
64/* Static function prototypes                                                */
65/*---------------------------------------------------------------------------*/
66
67static BlockInfo_t * AmcObtainOptimalSystemUpperBound(Amc_Info_t *amcInfo, Ctlp_Formula_t *formula, BlockInfo_t *BlockInfo, int verbosity);
68static BlockInfo_t * AmcObtainOptimalSystemLowerBound(Amc_Info_t *amcInfo, Ctlp_Formula_t *formula, BlockInfo_t *BlockInfo, int verbosity);
69static void AmcInitializeDependency(array_t *subSystemArray, int isMBM);
70static void AmcInitializeSchedule(Amc_Info_t *amcInfo);
71static int AmcIsEverySubsystemRescheduled(Amc_Info_t *amcInfo);
72static void AmcPrintScheduleInformation(Amc_Info_t *amcInfo);
73#if 0
74static void AmcRescheduleForRefinement(st_table *fanOutSystemTable);
75static mdd_t * AmcRefineWithSatisfyStatesOfFanInSystem(Amc_SubsystemInfo_t *subSystem, mdd_t *careStates);
76#endif
77static array_t * AmcInitializeQuantifyVars(Amc_SubsystemInfo_t *subSystem);
78#if 0
79static void AmcFreeBlockInfo(BlockInfo_t *BlockInfo);
80#endif
81static int AmcBlockSubsystemReadScheduledForRefinement(BlockSubsystemInfo_t *system);
82static void AmcBlockSubsystemSetScheduledForRefinement(BlockSubsystemInfo_t *system, int data);
83#if 0
84static Amc_SubsystemInfo_t * AmcBlockReadOptimalSubsystem(BlockInfo_t *system);
85#endif
86static void AmcBlockSetOptimalSystem(BlockInfo_t *system, Amc_SubsystemInfo_t *data);
87#if 0
88static int AmcBlockReadBestSystem(BlockInfo_t *system);
89#endif
90static void AmcBlockSetBestSystem(BlockInfo_t *system, int data);
91#if 0
92static Amc_SubsystemInfo_t * AmcClearInputVarsFromFSM(Amc_SubsystemInfo_t *subSystem);
93#endif
94
95/**AutomaticEnd***************************************************************/
96
97
98/*---------------------------------------------------------------------------*/
99/* Definition of exported functions                                          */
100/*---------------------------------------------------------------------------*/
101
102
103/*---------------------------------------------------------------------------*/
104/* Definition of internal functions                                          */
105/*---------------------------------------------------------------------------*/
106/**Function********************************************************************
107 
108  Synopsis    [A block-tearing procedure.]
109
110  Description [From an array of subsystems, the routine picks a subsystem
111  that produces best result. When proving true positive, a subsystem that
112  produces smallest cardinality of the error state is chosen as the best
113  subsystem.
114  Error states are defined as;
115  (Initial States) - (Subset of states satisfying given formula).
116  An over-approximation of the transition relation produces a subset of
117  states satisfying the original ACTL formula. Whenever the subset of states
118  satisfying given formula contains the initial states, we conclude that
119  the system models the specification.
120  The routine treats initial states as a monotonically
121  decreasing(cardinality wise) set.  This is because when we identify
122  the set of subsets of states satisfying given ACTL formula cover
123  the initial states, we can conclude that the initial states are entirely
124  contained in the exact set of states satisfying given ACTL formula.
125  Hence, once we identify an error states, the routine updates the
126  error states as new initial states.
127
128  When proving true negative of given ACTL formula, the best subsystem
129  is that produces smallest cardinality of the superset of states satisfying
130  ACTL formula in consideration. An under-approximation of the transition
131  relation of the original system produces a superset of states satisfying
132  the ACTL formulas. Whenever we find an initial state(s) that are not
133  contained in the superset of states satisfying given ACTL formula, we
134  conclude that the system does not model the specification. An initial
135  state(s) that is not contained in the superset of states satisfying
136  an ACTL formula is used to produce a debug trace.
137 
138  When "machine by machine" switch is ON, refinement of either subsets or
139  the supersets of states satisfying given formula is performed. This
140  process is done until the refinements cannot be made.
141  (Note; "machine by machine" refinement is not yet supported. 2/12/97)
142
143  ]
144
145  SideEffects []
146
147******************************************************************************/
148int
149AmcBlockTearingProc(
150  Amc_Info_t     *amcInfo,
151  Ctlp_Formula_t *formula,
152  int            verbosity)
153{
154  array_t               *subSystemArray = amcInfo->subSystemArray;
155  Amc_SubsystemInfo_t   *subSystem;
156  BlockInfo_t           BlockInfo;
157
158
159  /*
160   * Update fan-in subsystems and fan-out subsystems when machine by machine
161   * method is ON.
162   * Update initial states in BlockInfo.
163   * Reschedule every subsystem to be evaluated.
164   */
165
166  if( amcInfo->optimalSystem == NIL(Amc_SubsystemInfo_t) ) {
167    AmcInitializeDependency(subSystemArray, amcInfo->isMBM);
168  }
169
170  AmcInitializeSchedule(amcInfo);
171
172  /* BlockInfo is a temporary storage. optimal system is not freed */
173  BlockInfo.optimalSystem = NIL(Amc_SubsystemInfo_t);
174   
175
176  /*
177   * Outer loop until there's no scheduled subsystem.
178   */
179  while(AmcIsEverySubsystemRescheduled(amcInfo)) {
180
181    if(verbosity == Amc_VerbosityNone_c)
182      AmcPrintScheduleInformation(amcInfo);
183
184
185    if( !amcInfo->lowerBound ) {
186        AmcObtainOptimalSystemUpperBound(amcInfo, formula, &BlockInfo, 
187                                         verbosity);
188        /* AmcObtainOptimalSystemUpperBoundWithDI(amcInfo, formula, &BlockInfo,
189                                                  verbosity); */
190    }
191    else {
192        AmcObtainOptimalSystemLowerBound(amcInfo, formula, &BlockInfo, 
193                                         verbosity);
194        /* AmcObtainOptimalSystemLowerBoundWithMBM(amcInfo, formula, &BlockInfo,
195                                                   verbosity); */
196    }
197
198    if(amcInfo->isVerified) {
199
200        int best = BlockInfo.bestSystem;
201        subSystem = array_fetch(Amc_SubsystemInfo_t *, amcInfo->subSystemArray,
202                                best);
203        subSystem->takenIntoOptimal = 1;
204
205      return 1;
206    }
207
208    if(!amcInfo->isMBM)
209      break;
210
211  } /* End of while() */
212
213  if(verbosity == Amc_VerbosityNone_c)
214    AmcPrintScheduleInformation(amcInfo);
215
216
217  /* Update the subsystem that had been included in optimal system */
218  {
219    int best = BlockInfo.bestSystem;
220    subSystem = array_fetch(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, 
221                            best);
222    subSystem->takenIntoOptimal = 1;
223  }
224
225  /* Update amcInfo's optimal system */
226  if(amcInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
227#ifdef AMC_DEBUG
228    {
229      Amc_SubsystemInfo_t *previousOpt = amcInfo->optimalSystem;
230      Amc_SubsystemInfo_t *currentOpt  = BlockInfo.optimalSystem;
231
232      if(!amcInfo->lowerBound) {
233        if(mdd_lequal(previousOpt->satisfyStates, currentOpt->satisfyStates,
234                      1, 1)) {
235          fprintf(vis_stdout, "\n###AMC : We are ok.");
236        }
237        else {
238          fprintf(vis_stdout, "\n** amc error: Somethings wrong.");
239        }
240      }
241      else {
242        if( mdd_lequal(currentOpt->satisfyStates, previousOpt->satisfyStates,
243                       1, 1)) {
244          fprintf(vis_stdout, "\n###AMC : We are ok.");
245        }
246        else {
247          fprintf(vis_stdout, "\n** amc error: Somethings wrong.");
248        }
249      }
250    }
251#endif
252    Amc_AmcSubsystemFree(amcInfo->optimalSystem);
253  }
254  AmcSetOptimalSystem(amcInfo, BlockInfo.optimalSystem);
255
256  return 1;
257}
258
259/**Function********************************************************************
260
261  Synopsis    [Frees block-tearing specific data structure.]
262
263  SideEffects []
264
265******************************************************************************/
266void
267AmcFreeBlock(
268  Amc_Info_t *amcInfo)
269{
270  Amc_SubsystemInfo_t   *subSystem; 
271  BlockSubsystemInfo_t  *BlockSubsystem;
272  int i ;
273
274  /* what if amc doesn't free partition */
275  arrayForEachItem(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, i, 
276                   subSystem) {
277    BlockSubsystem = (BlockSubsystemInfo_t *)AmcSubsystemReadMethodSpecificData(subSystem);
278    if(BlockSubsystem != NIL(BlockSubsystemInfo_t))
279      FREE(BlockSubsystem);
280
281    Amc_AmcSubsystemFree(subSystem); 
282  }
283  array_free(amcInfo->subSystemArray);
284
285  if(amcInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
286    Amc_AmcSubsystemFree(amcInfo->optimalSystem);
287    amcInfo->optimalSystem = NIL(Amc_SubsystemInfo_t);
288  }
289
290  if( amcInfo->initialStates != NIL(mdd_t)) {
291    mdd_free(amcInfo->initialStates);
292    amcInfo->initialStates = NIL(mdd_t);
293  }
294
295  FREE(amcInfo);
296
297}
298
299/*---------------------------------------------------------------------------*/
300/* Definition of static functions                                            */
301/*---------------------------------------------------------------------------*/
302
303
304
305/**Function********************************************************************
306 
307  Synopsis [Obtain best subsystem that has not taken into the optimal system.]
308
309  Description [The routine is used to prove true positive of given ACTL formula.
310  An over-approximation of transition relation is used. Over-approximation of
311  the transition relation is obtained by simply replacing the subsystems not in
312  consideration into tautology. We are adding more behavior into the system
313  by preserving only the subset of subsystems(subFSMs). We call this
314  procedure a block-tearing abstraction. We do not abstract initial states
315  in any sense.
316
317  The best subsystem is chosen from those subsystems that has not yet been
318  taken into the optimal system. A subsystem that produces best result is
319  determined by the smallest error states. An error states are defined as;
320  Error States =
321  (Initial States) - (Subset of states satisfying given ACTL formula)   
322  For each subsystem, a subset of states satisfying given ACTL formula is
323  computed by using an over-approximation of the transition relation obtained
324  from the subsystem. The routine picks a subsystem whose corresponding
325  error states are cardinality wise minimal.
326 
327  The optimal system is the collection of subsystems that were chosen as
328  the best subsystem in each iteration. A function call to this routine is
329  regarded as a single iteration when "machine by machine" refinement is turned
330  OFF. These subsystems are synchronously combined to form a optimal system.
331
332  Once the best subsystem is chosen(from the set of subsystems that has not
333  been combined into the optimal system), an initial states are updated with
334  an error states. An error states are defined as;
335  (Initial States) - (Subset of states satisfying given ACTL formula)
336
337  A more aggressive update of initial states may also be performed. If we
338  denote a subset of states satisfying given ACTL formula as Sat^L(\phi).
339  New Initial States = (Old Initial States) - \Sigma_{i}(Sat^L_i(\phi)
340  The routine currently does not attempt above aggressive approach. The
341  routine update initial state as;
342  New Initial States = (Old Initial States) - Sat^L_{Best i}(\phi).
343
344 
345  ]
346
347  SideEffects []
348
349******************************************************************************/
350static BlockInfo_t *
351AmcObtainOptimalSystemUpperBound(
352Amc_Info_t              *amcInfo,
353Ctlp_Formula_t          *formula,
354BlockInfo_t             *BlockInfo,
355int                     verbosity)
356{
357  array_t               *subSystemArray = amcInfo->subSystemArray;
358  Amc_SubsystemInfo_t   *subSystem, *bestCombinedSystem;
359  mdd_t                 *initialStates;
360  mdd_t                 *smallestStates, *currentErrorStates, *careStates;
361  int                   i, best = 0;
362  graph_t               *partition = Part_NetworkReadPartition(amcInfo->network);
363  mdd_manager           *mddManager = Part_PartitionReadMddManager(partition);
364  mdd_t                 *mddOne = mdd_one(mddManager);
365  array_t               *quantifyVars;
366  Mc_DcLevel            dcLevel;
367  char  *flagValue;
368
369
370  /*
371   * Initial states must be set before coming into this routine.
372   */
373  initialStates = amcInfo->initialStates;
374  if( initialStates == NIL(mdd_t) ) {
375    (void)fprintf(vis_stderr, "** amc error: \n");
376    return(NIL(BlockInfo_t));
377  }
378 
379  /* Read in the usage of don't care level */
380  flagValue = Cmd_FlagReadByName("amc_DC_level");
381  if(flagValue != NIL(char)){
382    dcLevel = (Mc_DcLevel) atoi(flagValue); 
383    if( dcLevel > McDcLevelRchFrontier_c ) dcLevel = McDcLevelRchFrontier_c;
384  }
385  else{
386    /* default value set to McDcLevelNone_c. Mc's default is McDcLevelRch_c. */
387    dcLevel = McDcLevelNone_c; 
388  }
389
390  /*
391   * Update the set of states satisfying the formula for each sub-systems.
392   * The process of "combining sub-systems" is equivalent of taking a
393   * "synchronous product" of multiple sub-subsystems.
394   */
395  smallestStates = NIL(mdd_t);
396  bestCombinedSystem  = NIL(Amc_SubsystemInfo_t);
397
398  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
399
400    mdd_t                       *reachableStates, *fairStates, *satisfyStates;
401    Fsm_Fsm_t                   *combinedFsm;
402    Fsm_Fairness_t              *fairCond;
403    Amc_SubsystemInfo_t         *combinedSystem; 
404
405    /* Proceed if the subsystem had not yet been taken into the optimal system. */
406    if(!subSystem->takenIntoOptimal) {
407
408      /*
409       * Combine subsystems. If optimal subsystem is NIL, duplicate the
410       * subsystem.
411       */ 
412      combinedSystem = Amc_CombineSubsystems(amcInfo->network,
413                                             amcInfo->optimalSystem,
414                                             subSystem);
415      combinedFsm = AmcSubsystemReadFsm(combinedSystem);
416
417      quantifyVars = AmcInitializeQuantifyVars(combinedSystem);
418     
419      /*
420       * Currently forced not to compute reachable states. This is to reduce
421       * computational overhead of computing it when dealing with complex
422       * examples.
423       */
424      reachableStates = mdd_one(mddManager);
425      fairStates = mdd_one(mddManager);
426      fairCond = Fsm_FsmReadFairnessConstraint(combinedFsm);
427
428
429      /* Obtain new care set from fan-in systems */
430      careStates = mdd_dup(reachableStates);
431
432      Ctlp_FlushStates(formula);
433      satisfyStates = mdd_dup(Amc_AmcEvaluateCTLFormula(combinedSystem,
434                                                        subSystemArray, 
435                                                        formula, fairStates,
436                                                        fairCond,
437                                                        careStates,
438                                                        amcInfo->lowerBound, 
439                                                        quantifyVars,
440                                                        /*NIL(array_t),*/
441                                                        (Mc_VerbosityLevel)
442                                                        verbosity, dcLevel));
443
444      {
445        int x; array_t *quantifyStateVars;
446        arrayForEachItem(array_t *, quantifyVars, x, quantifyStateVars) {
447          array_free(quantifyStateVars); 
448        }
449        array_free(quantifyVars);
450      }
451      /* Free */
452      mdd_free(careStates);
453      mdd_free(reachableStates); mdd_free(fairStates); 
454     
455
456      /*
457       * Update the set of states satisfying the formula for each subsystems
458       * when newly computed states are tighter than the one already stored.
459       * Notice, "satisfySates" holds the set of states satisfying the formula
460       * computed with the combined_system(optimal_system || current_subsystem).
461       *
462       */
463      if( subSystem->satisfyStates != NIL(mdd_t) ) {
464
465        if( !(mdd_equal(subSystem->satisfyStates, satisfyStates )) &&
466            (mdd_lequal(subSystem->satisfyStates, satisfyStates, 1, 1)) ) {
467          /* We got a tighter approximation. */
468          mdd_free(subSystem->satisfyStates);
469          AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates));
470        }
471         
472      }     
473      else {
474        /* We are in the first level of the lattice */
475        AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates));
476
477      }
478
479      /* Update the set of states satisfying the formula for the combined_system. */
480      if( AmcSubsystemReadSatisfy(combinedSystem) != NIL(mdd_t) )
481        mdd_free( AmcSubsystemReadSatisfy(combinedSystem) );
482      AmcSubsystemSetSatisfy(combinedSystem, mdd_dup(satisfyStates));
483
484
485      if( verbosity == Amc_VerbosityVomit_c) {
486         mdd_manager *mddMgr = Fsm_FsmReadMddManager(combinedSystem->fsm);
487         array_t     *psVars = Fsm_FsmReadPresentStateVars(combinedSystem->fsm);
488
489         fprintf(vis_stdout, "\n#AMC STATUS: The states satisfying the formula : %10g",
490                        mdd_count_onset(  mddMgr, combinedSystem->satisfyStates, psVars ) );
491         fflush(vis_stdout);
492       }
493
494      /*
495       * Check whether the formula evaluates to TRUE.
496       */
497      { 
498        mdd_t *notSatisfyStates = mdd_not(satisfyStates);
499        currentErrorStates = mdd_and(initialStates, notSatisfyStates, 1, 1);
500        mdd_free(notSatisfyStates);
501        mdd_free(satisfyStates);
502      }
503
504      if ( mdd_is_tautology(currentErrorStates, 0) ) { 
505        /* The formula is verified TRUE!! */
506
507        AmcBlockSetBestSystem(BlockInfo, i);
508        amcInfo->isVerified = 1; 
509        amcInfo->amcAnswer = Amc_Verified_True_c;
510        fprintf(vis_stdout, "\n# AMC: formula passed --- ");
511        Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));
512
513        if(currentErrorStates != NIL(mdd_t))
514          mdd_free(currentErrorStates); 
515        if(smallestStates != NIL(mdd_t))
516          mdd_free(smallestStates);
517        if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) )
518          Amc_AmcSubsystemFree(bestCombinedSystem); 
519
520        mdd_free(mddOne); Amc_AmcSubsystemFree(combinedSystem); 
521        Ctlp_FlushStates(formula);
522
523        return BlockInfo;
524      } /* end of if */
525      else if (amcInfo->currentLevel == array_n(amcInfo->subSystemArray)){
526        /* The formula is verified FALSE!! */
527        array_t *careStatesArray;
528
529        AmcBlockSetBestSystem(BlockInfo, i);
530        amcInfo->isVerified = 1;
531        amcInfo->amcAnswer = Amc_Verified_False_c;
532        fprintf(vis_stdout, "\n# AMC: formula failed --- ");
533        Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));
534
535        if(currentErrorStates != NIL(mdd_t)) mdd_free(currentErrorStates);
536        if(smallestStates != NIL(mdd_t))     mdd_free(smallestStates);
537
538        if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) )
539          Amc_AmcSubsystemFree(bestCombinedSystem);
540
541        {
542          /* Temporarily stay here until the damn thing becomes visible. */
543          McOptions_t *mcOptions = ALLOC(McOptions_t, 1);
544          mcOptions->useMore = FALSE;
545          mcOptions->fwdBwd = McFwd_c;
546          mcOptions->reduceFsm = FALSE;
547          mcOptions->printInputs = FALSE;
548          mcOptions->simFormat = FALSE;
549          mcOptions->verbosityLevel = McVerbosityNone_c;
550          mcOptions->dbgLevel = McDbgLevelMin_c;
551          mcOptions->dcLevel   = McDcLevelNone_c;
552          mcOptions->ctlFile = NIL(FILE);
553          mcOptions->debugFile = NIL(FILE);
554
555          careStatesArray = array_alloc(mdd_t *, 0);
556          array_insert(mdd_t *, careStatesArray, 0, mddOne);
557          fprintf(vis_stdout, "\n");
558          McFsmDebugFormula((McOptions_t *)mcOptions, formula,
559                            combinedSystem->fsm, careStatesArray);
560          array_free(careStatesArray);
561          FREE(mcOptions);
562        }
563        mdd_free(mddOne);
564        Amc_AmcSubsystemFree(combinedSystem);
565        Ctlp_FlushStates(formula);
566
567        return BlockInfo;       
568      }
569
570      /*
571       * Get the locally optimal subsystem by choosing a subsystem that produces
572       * smallest error states.
573       */
574      if( smallestStates == NIL(mdd_t) ||
575         mdd_count_onset(mddManager, currentErrorStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) <=
576         mdd_count_onset(mddManager, smallestStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) ) {
577
578        if( smallestStates != NIL(mdd_t) )
579          mdd_free(smallestStates);
580
581        smallestStates = currentErrorStates;
582
583        if(bestCombinedSystem != NIL(Amc_SubsystemInfo_t)) {
584          Amc_AmcSubsystemFree(bestCombinedSystem);
585          bestCombinedSystem = NIL(Amc_SubsystemInfo_t);
586        }
587        bestCombinedSystem = combinedSystem; 
588        best = i;
589      }
590
591      else { /* Free combined system, current error states */
592        Amc_AmcSubsystemFree(combinedSystem);
593        combinedSystem = NIL(Amc_SubsystemInfo_t);
594        mdd_free(currentErrorStates); 
595      }
596
597   
598    } /* end of if(!takenIntoOptimal) */
599
600  } /* end of arrayForEachItem(subSystemArray) */
601
602
603  /*
604   * Flush the formula that was kept in last iteration.
605   * Update Block Info. 
606   */
607  Ctlp_FlushStates(formula);
608
609  /* Update the inital states */
610  {
611    mdd_t *initialStates;
612    if((initialStates = AmcReadInitialStates(amcInfo)) != NIL(mdd_t))
613      mdd_free(initialStates);
614    AmcSetInitialStates(amcInfo, smallestStates);
615  }
616
617  if( verbosity == Amc_VerbositySpit_c ) {
618    mdd_manager *mddMgr = Fsm_FsmReadMddManager(bestCombinedSystem->fsm);
619    array_t     *psVars = Fsm_FsmReadPresentStateVars(bestCombinedSystem->fsm);
620
621    fprintf(vis_stdout, "\n#AMC : The BDD size of the states satisfying the formula : %d", 
622                                  mdd_size(bestCombinedSystem->satisfyStates) );
623    fprintf(vis_stdout, "\n#AMC : The cardinality of the states satisfying the formula : %10g ",
624                          mdd_count_onset(  mddMgr, bestCombinedSystem->satisfyStates, psVars ) );
625    fprintf(vis_stdout, "\n#AMC : The BDD size of the states new initial states : %d",
626                                  mdd_size(smallestStates) );
627    fprintf(vis_stdout, "\n#AMC : The cardinality of the new initial states : %10g ",
628                          mdd_count_onset(  mddMgr, smallestStates, psVars ) );
629  }
630
631
632  /*
633   * Update the optimal system BlockInfo->optimalSystem. BlockInfo is a temporary
634   * storage that survive through single level of the lattice.
635   */
636  if(BlockInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
637    Amc_AmcSubsystemFree(BlockInfo->optimalSystem);
638    AmcBlockSetOptimalSystem(BlockInfo, NIL(Amc_SubsystemInfo_t));
639  }
640  AmcSetOptimalSystem(BlockInfo, bestCombinedSystem);
641
642  /* Set the best system. */
643  AmcBlockSetBestSystem(BlockInfo, best);
644
645  mdd_free(mddOne);
646 
647  return BlockInfo;
648
649}
650
651
652/**Function********************************************************************
653 
654  Synopsis [Obtain best subsystem that has not taken into the optimal system.]
655
656  Description [The routine is to choose a subsystem that produces a best result
657  when proving true negative of the formula. An under-approximation of the
658  transition is used to obtain a superset of states satisfying given formula.
659  The best subsystem is a subsystem that produces a smallest cardinality
660  of a superset of states satisfying given ACTL formula.]
661
662  SideEffects []
663
664******************************************************************************/
665static BlockInfo_t *
666AmcObtainOptimalSystemLowerBound(
667Amc_Info_t              *amcInfo,
668Ctlp_Formula_t          *formula,
669BlockInfo_t             *BlockInfo,
670int                     verbosity)
671{
672  array_t               *subSystemArray = amcInfo->subSystemArray;
673  Amc_SubsystemInfo_t   *subSystem, *bestCombinedSystem;
674  mdd_t                 *initialStates;
675  mdd_t                 *smallestStates, *currentErrorStates, *careStates;
676  int                   i, best = 0;
677  graph_t               *partition = Part_NetworkReadPartition(amcInfo->network);
678  mdd_manager           *mddManager = Part_PartitionReadMddManager(partition);
679  mdd_t                 *mddOne = mdd_one(mddManager);
680  array_t               *quantifyVars;
681  Mc_DcLevel            dcLevel;
682  char                  *flagValue;
683 
684  /*
685   * Initial states must be set before coming into this routine.
686   */
687  initialStates = amcInfo->initialStates;
688  if( initialStates == NIL(mdd_t) ) {
689    (void)fprintf(vis_stderr, "** amc error: \n");
690    return(NIL(BlockInfo_t));
691  }
692
693  /* Read in the usage of don't care level. Do not want to pass parameters. */
694  flagValue = Cmd_FlagReadByName("amc_DC_level");
695  if(flagValue != NIL(char)){
696    dcLevel = (Mc_DcLevel) atoi(flagValue);
697    if( dcLevel > McDcLevelRchFrontier_c ) dcLevel = McDcLevelRchFrontier_c;
698  }
699  else{
700    /* default value set to McDcLevelNone_c. Mc's default is McDcLevelRch_c. */
701    dcLevel = McDcLevelNone_c;
702  }
703
704  /*
705   * Update the set of states satisfying the formula for each subsystem.
706   * The process of "combining sub-systems" is equivalent of taking a
707   * "synchronous product" of multiple subsystems.
708   */
709  smallestStates = NIL(mdd_t);
710  bestCombinedSystem  = NIL(Amc_SubsystemInfo_t);
711
712  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
713
714    mdd_t                       *reachableStates, *fairStates, *satisfyStates;
715    Fsm_Fsm_t                   *combinedFsm;
716    Fsm_Fairness_t              *fairCond;
717    Amc_SubsystemInfo_t         *combinedSystem; 
718
719    /* Proceed if the subsystem has not yet been taken into the optimal system. */
720    if(!subSystem->takenIntoOptimal) {
721
722      /*
723       * Combine subsystems. If optimal subsystem is NIL, duplicate the
724       * subsystem.
725       */
726      combinedSystem = Amc_CombineSubsystems(amcInfo->network,
727                                             amcInfo->optimalSystem,
728                                             subSystem);
729      /* Remove input variables from the FSM */
730      /*      combinedSystem = AmcClearInputVarsFromFSM(combinedSystem);*/
731      combinedFsm = AmcSubsystemReadFsm(combinedSystem);
732
733      /*
734       * Use takenIntoOptimal field for the purpose of excluding current block
735       * when universally quantifying variables from transition relation.
736       * Obtain lower bound of transition relation by universal quantification.
737       */
738
739      quantifyVars = AmcInitializeQuantifyVars(combinedSystem);
740      combinedSystem->takenIntoOptimal = i;
741
742
743      /*
744       * Currently forced not to compute reachable states. This is to reduce
745       * computational burden of computing it when dealing with complex
746       * examples.
747       */
748      reachableStates = mdd_one(mddManager);
749      fairStates = mdd_one(mddManager);
750      fairCond = Fsm_FsmReadFairnessConstraint(combinedFsm);
751      careStates = mdd_dup(reachableStates);
752
753      Ctlp_FlushStates(formula);
754      satisfyStates = mdd_dup(Amc_AmcEvaluateCTLFormula(combinedSystem,
755                                                        subSystemArray, 
756                                                        formula, fairStates,
757                                                        fairCond, careStates,
758                                                        amcInfo->lowerBound, 
759                                                        quantifyVars,
760                                                        (Mc_VerbosityLevel)
761                                                        verbosity, dcLevel));
762      {
763        int x; array_t *quantifyStateVars;
764        arrayForEachItem(array_t *, quantifyVars, x, quantifyStateVars) {
765          array_free(quantifyStateVars); 
766        }
767        array_free(quantifyVars);
768      }
769      mdd_free(careStates); mdd_free(reachableStates); mdd_free(fairStates); 
770     
771
772      /*
773       */
774      if( subSystem->satisfyStates != NIL(mdd_t) ) {
775        if( !(mdd_equal(satisfyStates, subSystem->satisfyStates )) &&
776             (mdd_lequal(satisfyStates, subSystem->satisfyStates, 1, 1)) ) {
777          /* We got a tighter approximation. */
778          mdd_free(subSystem->satisfyStates);
779          AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates));
780        }
781      }     /* end of if( subSystem->satisfyStates != NIL(mdd_t) ) */
782      else {
783        /* Update subsystem when we are in level 1 of the lattice */
784        AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates));
785      }
786
787      if( AmcSubsystemReadSatisfy(combinedSystem) != NIL(mdd_t) )
788        mdd_free( AmcSubsystemReadSatisfy(combinedSystem) );
789      AmcSubsystemSetSatisfy(combinedSystem, mdd_dup(satisfyStates));
790
791
792      /* Test if the formula is verified */
793      {
794        mdd_t *notSatisfyStates = mdd_not(satisfyStates);
795        currentErrorStates      = mdd_and(initialStates, notSatisfyStates, 1, 1);
796        mdd_free(notSatisfyStates);
797        mdd_free(satisfyStates);
798      }
799
800      if( verbosity == Amc_VerbosityVomit_c) {
801        mdd_manager *mddMgr = Fsm_FsmReadMddManager(combinedSystem->fsm);
802        array_t *psVars     = Fsm_FsmReadPresentStateVars(combinedSystem->fsm);
803
804        fprintf(vis_stdout,
805                "\n#AMC STATUS: The states satisfying the formula : %10g",
806                mdd_count_onset(mddMgr, combinedSystem->satisfyStates, psVars ) );
807        fflush(vis_stdout);
808      }
809
810      if ( !mdd_is_tautology(currentErrorStates, 0) ) {
811        array_t *careStatesArray;
812
813        /* Verified the formula FALSE!! */
814        AmcBlockSetBestSystem(BlockInfo, i);
815        amcInfo->isVerified = 1;
816        amcInfo->amcAnswer = Amc_Verified_False_c;
817        fprintf(vis_stdout, "\n# AMC: formula failed --- ");
818        Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));
819
820
821        if(currentErrorStates != NIL(mdd_t)) mdd_free(currentErrorStates);
822        if(smallestStates != NIL(mdd_t))     mdd_free(smallestStates);
823
824        if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) )
825          Amc_AmcSubsystemFree(bestCombinedSystem);
826
827        {
828          /* Temporarily stay here until the damn thing becomes visible. */
829          McOptions_t *mcOptions = ALLOC(McOptions_t, 1);
830          mcOptions->useMore = FALSE;
831          mcOptions->fwdBwd = McFwd_c;
832          mcOptions->reduceFsm = FALSE;
833          mcOptions->printInputs = FALSE;
834          mcOptions->simFormat = FALSE;
835          mcOptions->verbosityLevel = McVerbosityNone_c;
836          mcOptions->dbgLevel = McDbgLevelMinVerbose_c;
837          mcOptions->dcLevel   = McDcLevelNone_c;
838          mcOptions->ctlFile = NIL(FILE);
839          mcOptions->debugFile = NIL(FILE);
840
841          careStatesArray = array_alloc(mdd_t *, 0);
842          array_insert(mdd_t *, careStatesArray, 0, mddOne);
843          fprintf(vis_stdout, "\n");
844          McFsmDebugFormula((McOptions_t *)mcOptions, formula,
845                            combinedSystem->fsm, careStatesArray);
846          array_free(careStatesArray);
847          FREE(mcOptions);
848        }
849        mdd_free(mddOne);
850        Amc_AmcSubsystemFree(combinedSystem);
851        Ctlp_FlushStates(formula);
852
853        return BlockInfo;
854
855      }else if (amcInfo->currentLevel == array_n(amcInfo->subSystemArray)){
856        /* The formula is verified true!! */
857        AmcBlockSetBestSystem(BlockInfo, i);
858        amcInfo->isVerified = 1; 
859        amcInfo->amcAnswer = Amc_Verified_True_c;
860        fprintf(vis_stdout, "\n# AMC: formula passed --- ");
861        Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));
862
863
864        if(currentErrorStates != NIL(mdd_t))
865          mdd_free(currentErrorStates); 
866        if(smallestStates != NIL(mdd_t))
867          mdd_free(smallestStates);
868        if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) )
869          Amc_AmcSubsystemFree(bestCombinedSystem); 
870
871        mdd_free(mddOne); Amc_AmcSubsystemFree(combinedSystem); 
872        Ctlp_FlushStates(formula);
873
874        return BlockInfo;
875      }
876
877      mdd_free(currentErrorStates);
878
879
880      /*
881       * Choose a subsystem that produces smallest satisfying states.
882       */
883      if( smallestStates == NIL(mdd_t) ||
884          mdd_count_onset(mddManager, subSystem->satisfyStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) <= 
885          mdd_count_onset(mddManager, smallestStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) ) {
886        /*
887         * Found locally optimal subsystem.
888         * Free smallest-error-state, best combined system so far.
889         * Update smallest-error-states and best combined system.
890         */
891        if( smallestStates != NIL(mdd_t) ) mdd_free(smallestStates);
892
893        smallestStates = mdd_dup(subSystem->satisfyStates);
894
895        if(bestCombinedSystem != NIL(Amc_SubsystemInfo_t)) {
896          Amc_AmcSubsystemFree(bestCombinedSystem);
897          bestCombinedSystem = NIL(Amc_SubsystemInfo_t);
898        }
899        bestCombinedSystem = combinedSystem; 
900        best = i;
901      }
902
903      else { /* Free combined system, current error states */
904        Amc_AmcSubsystemFree(combinedSystem); combinedSystem = NIL(Amc_SubsystemInfo_t);
905      }
906
907    } /* end of if(!takenIntoOptimal) */
908
909  } /* end of arrayForEachItem(subSystemArray) */
910
911  mdd_free(smallestStates);
912
913  /*
914   * Flush formula that was kept in last iteration. Update Block Info. 
915   */
916  Ctlp_FlushStates(formula);
917
918  /*
919   * Update optimal system BlockInfo->optimalSystem. BlockInfo is a temporary
920   * storage that survive through single level of the lattice.
921   */
922  if(BlockInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
923    Amc_AmcSubsystemFree(BlockInfo->optimalSystem);
924    AmcBlockSetOptimalSystem(BlockInfo, NIL(Amc_SubsystemInfo_t));
925  }
926  AmcSetOptimalSystem(BlockInfo, bestCombinedSystem);
927
928  /* Set best system. */
929  AmcBlockSetBestSystem(BlockInfo, best);
930  mdd_free(mddOne);
931
932  return BlockInfo;
933
934}
935
936
937
938/**Function********************************************************************
939
940  Synopsis    [Initialize dependencies between subsystems.]
941
942  SideEffects []
943
944******************************************************************************/
945static void
946AmcInitializeDependency(
947array_t         *subSystemArray,
948int             isMBM)
949{
950  Amc_SubsystemInfo_t   *subSystem; 
951  BlockSubsystemInfo_t  *BlockSubsystem;
952  int   i;
953
954  if(!isMBM) {
955    int i;
956    arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
957      AmcSubsystemSetMethodSpecificData(subSystem, NIL(BlockSubsystemInfo_t));
958    }
959    return;
960  }
961
962  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
963
964    BlockSubsystem = ALLOC(BlockSubsystemInfo_t, 1);
965
966    AmcSubsystemSetMethodSpecificData(subSystem, BlockSubsystem);
967
968  }
969
970}
971
972/**Function********************************************************************
973
974  Synopsis    [Initialize scheduling information.]
975
976  SideEffects []
977
978******************************************************************************/
979static void
980AmcInitializeSchedule(
981Amc_Info_t *amcInfo)
982{
983  array_t                 *subSystemArray = amcInfo->subSystemArray;
984  Amc_SubsystemInfo_t     *subSystem; 
985  BlockSubsystemInfo_t    *BlockSubsystem;
986  int i;
987
988  /* If MBM flag is not set just return */
989  if(!amcInfo->isMBM)
990    return;
991
992  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
993
994    BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem);
995    if(!subSystem->takenIntoOptimal)
996      AmcBlockSubsystemSetScheduledForRefinement(BlockSubsystem, 1);
997   
998  }
999
1000}
1001
1002
1003/**Function********************************************************************
1004
1005  Synopsis    [Test whether there is any subsystems to be reevaluated.]
1006
1007  SideEffects []
1008
1009******************************************************************************/
1010static int
1011AmcIsEverySubsystemRescheduled(
1012Amc_Info_t *amcInfo)
1013{
1014  array_t               *subSystemArray = amcInfo->subSystemArray;
1015  Amc_SubsystemInfo_t   *subSystem; 
1016  BlockSubsystemInfo_t  *BlockSubsystem;
1017  int i;
1018
1019  /* If MBM flag is not set just return */
1020  if( !amcInfo->isMBM )
1021    return 1;
1022
1023  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
1024
1025    BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem);
1026    if( AmcBlockSubsystemReadScheduledForRefinement(BlockSubsystem) )
1027      return 1;
1028   
1029  }
1030  return 0;
1031
1032}
1033
1034/**Function********************************************************************
1035
1036  Synopsis    [Print schedule information.]
1037
1038  SideEffects []
1039
1040******************************************************************************/
1041static void
1042AmcPrintScheduleInformation(
1043Amc_Info_t *amcInfo)
1044{
1045  array_t                 *subSystemArray = amcInfo->subSystemArray;
1046  Amc_SubsystemInfo_t     *subSystem; 
1047  BlockSubsystemInfo_t    *BlockSubsystem;
1048  int i;
1049
1050  /* If MBM flag is not set just return */
1051  if(!amcInfo->isMBM)
1052    return;
1053
1054  fprintf(vis_stdout, "\nSchedule information : ");
1055
1056  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
1057
1058    BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem);
1059    fprintf(vis_stdout, " %d ", AmcBlockSubsystemReadScheduledForRefinement(BlockSubsystem) );
1060   
1061  }
1062
1063}
1064
1065
1066#if 0
1067/**Function********************************************************************
1068
1069  Synopsis    [Update scheduling information for reevaluation.]
1070
1071  SideEffects []
1072
1073******************************************************************************/
1074static void
1075AmcRescheduleForRefinement(
1076st_table        *fanOutSystemTable)
1077{
1078  Amc_SubsystemInfo_t   *subSystem;
1079  BlockSubsystemInfo_t  *BlockSubsystem;
1080  st_generator *stGen;
1081
1082  st_foreach_item(fanOutSystemTable, stGen, &subSystem, NIL(char *)) {
1083
1084    /* reschedule only ones that are not taken */
1085    if(!subSystem->takenIntoOptimal) {
1086      BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem);
1087      AmcBlockSubsystemSetScheduledForRefinement(BlockSubsystem, 1);
1088    }
1089
1090  }
1091
1092}
1093
1094/**Function********************************************************************
1095
1096  Synopsis    [Refine result with transitive fanin subsystems.]
1097
1098  SideEffects []
1099
1100******************************************************************************/
1101static mdd_t *
1102AmcRefineWithSatisfyStatesOfFanInSystem(
1103Amc_SubsystemInfo_t     *subSystem,
1104mdd_t                   *careStates)
1105{
1106  st_table              *fanInTable = AmcSubsystemReadFanInTable(subSystem);
1107  Amc_SubsystemInfo_t   *fanInSystem;
1108  st_generator          *stGen;
1109
1110  mdd_t                 *oldCareStates = careStates;
1111  st_foreach_item(fanInTable, stGen, &fanInSystem, NIL(char *)) {
1112
1113    if(fanInSystem->satisfyStates != NIL(mdd_t)) {
1114      mdd_t     *fanInSatisfyStates = mdd_dup(fanInSystem->satisfyStates);
1115      careStates = mdd_and(fanInSatisfyStates, oldCareStates, 1, 1);
1116      mdd_free(oldCareStates); mdd_free(fanInSatisfyStates);
1117      oldCareStates = careStates;
1118    }
1119
1120  }
1121
1122  return(careStates);
1123} /* end of "machine by machine" refinement of the careset */
1124#endif
1125
1126
1127/**Function********************************************************************
1128
1129  Synopsis [Initialize mdd variables to be quantified. Used in
1130  under-approximation of the transition relation.]
1131
1132  SideEffects []
1133
1134******************************************************************************/
1135static array_t *
1136AmcInitializeQuantifyVars(
1137Amc_SubsystemInfo_t *subSystem)
1138{
1139  array_t             *quantifyVars             = array_alloc(array_t *, 0);
1140  array_t             *quantifyPresentVars      = array_alloc(int, 0);
1141  array_t             *quantifyNextVars         = array_alloc(int, 0);
1142  array_t             *quantifyInputVars        = array_alloc(int, 0);
1143  Ntk_Network_t       *network = Fsm_FsmReadNetwork(AmcSubsystemReadFsm(subSystem));
1144  Ntk_Node_t          *latch;
1145  st_table            *vertexTable = AmcSubsystemReadVertexTable(subSystem);
1146  lsGen               gen;
1147   
1148  Ntk_NetworkForEachLatch(network, gen, latch) {
1149    char *latchName = Ntk_NodeReadName(latch); 
1150#ifdef AMC_DEBUG
1151        fprintf(vis_stdout, "\nlatch name: %s", latchName);
1152        fprintf(vis_stdout, "\n latch id: %d", Ntk_NodeReadMddId(latch));
1153        fprintf(vis_stdout, "\n latch id: %d", Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
1154        fflush(vis_stdout);
1155#endif
1156    if(!st_lookup(vertexTable, latchName, (char **)0)) {
1157   
1158      /* Next state variables. */
1159      array_insert_last(int, quantifyNextVars, Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
1160      /* Present state variables. */
1161      array_insert_last(int, quantifyPresentVars, Ntk_NodeReadMddId(latch));
1162
1163    } /* end of if(st_lookup(vertexTable)) */
1164  } /* end of Ntk_NetworkForEachLatch */
1165
1166
1167  {
1168    st_table    *inputVarTable = st_init_table(st_numcmp, st_numhash);
1169    Ntk_Node_t  *primaryInput;
1170    /* Build the hash table of input vars of this subsystem. */
1171    /* arrayForEachItem(int, inputVarArray, i, inputVar) {
1172      st_insert(inputVarTable, (char *)(long)inputVar, (char *)0);
1173    } */
1174
1175    Ntk_NetworkForEachInput(network, gen, primaryInput) {
1176      int       mddId = Ntk_NodeReadMddId(primaryInput);
1177#ifdef AMC_DEBUG
1178      char *inputName = Ntk_NodeReadName(primaryInput); 
1179      int       testMddId = Ntk_NodeReadMddId(primaryInput);
1180      fprintf(vis_stdout, "\nprimary input name : %s", inputName);
1181      fprintf(vis_stdout, "\nprimary input mdd id : %d", testMddId);
1182      fflush(vis_stdout);
1183#endif
1184      /* if(!st_lookup(inputVarTable, (char *)(long)mddId, (char **)0)) { */
1185        array_insert_last(int, quantifyInputVars, mddId);
1186      /* } */
1187    }
1188    st_free_table(inputVarTable);
1189  }
1190
1191  array_insert_last(array_t *, quantifyVars, quantifyPresentVars); 
1192  array_insert_last(array_t *, quantifyVars, quantifyNextVars); 
1193  array_insert_last(array_t *, quantifyVars, quantifyInputVars); 
1194 
1195  return quantifyVars;
1196
1197}
1198
1199
1200#if 0
1201/**Function********************************************************************
1202
1203  Synopsis    [Frees block-tearing specific data structure.]
1204
1205  SideEffects []
1206
1207******************************************************************************/
1208static void
1209AmcFreeBlockInfo(
1210BlockInfo_t     *BlockInfo)
1211{
1212
1213  if(BlockInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
1214    Amc_AmcSubsystemFree(BlockInfo->optimalSystem);
1215  }
1216
1217}
1218#endif
1219
1220
1221/**Function********************************************************************
1222
1223  Synopsis    [Read scheduling information.]
1224
1225  SideEffects []
1226
1227******************************************************************************/
1228static int
1229AmcBlockSubsystemReadScheduledForRefinement(
1230BlockSubsystemInfo_t        *system)
1231{
1232  return system->scheduledForRefinement;
1233}
1234
1235/**Function********************************************************************
1236
1237  Synopsis    [Set scheduling information.]
1238
1239  SideEffects []
1240
1241******************************************************************************/
1242static void
1243AmcBlockSubsystemSetScheduledForRefinement(
1244BlockSubsystemInfo_t        *system,
1245int                   data)
1246{
1247  system->scheduledForRefinement = data;
1248}
1249
1250
1251#if 0
1252/**Function********************************************************************
1253
1254  Synopsis    [Read optimal system.]
1255
1256  SideEffects []
1257
1258******************************************************************************/
1259static Amc_SubsystemInfo_t *
1260AmcBlockReadOptimalSubsystem(
1261BlockInfo_t        *system)
1262{
1263  return system->optimalSystem;
1264}
1265#endif
1266
1267/**Function********************************************************************
1268
1269  Synopsis    [Set optimal system.]
1270
1271  SideEffects []
1272
1273******************************************************************************/
1274static void
1275AmcBlockSetOptimalSystem(
1276BlockInfo_t                  *system,
1277Amc_SubsystemInfo_t  *data)
1278{
1279  system->optimalSystem = data;
1280}
1281
1282#if 0
1283/**Function********************************************************************
1284
1285  Synopsis    [Read best system.]
1286
1287  SideEffects []
1288
1289******************************************************************************/
1290static int
1291AmcBlockReadBestSystem(
1292BlockInfo_t        *system)
1293{
1294  return system->bestSystem;
1295}
1296#endif
1297
1298/**Function********************************************************************
1299
1300  Synopsis    [Set best system.]
1301
1302  SideEffects []
1303
1304******************************************************************************/
1305static void
1306AmcBlockSetBestSystem(
1307BlockInfo_t                *system,
1308int                  data)
1309{
1310  system->bestSystem = data;
1311}
1312
1313#if 0
1314/**Function********************************************************************
1315
1316  Synopsis    [Clear input variables from the FSM of the subsystem.]
1317
1318  Description [Preimage computation existentially abstract both range variables
1319  and input variables. This function is used to prevent existential
1320  abstraction of input variables when computing the preimage.]
1321
1322  SideEffects []
1323
1324******************************************************************************/
1325static Amc_SubsystemInfo_t *
1326AmcClearInputVarsFromFSM(
1327Amc_SubsystemInfo_t   *subSystem)
1328{
1329  Fsm_Fsm_t     *fsm = subSystem->fsm;
1330  array_t       *inputVarArray = Fsm_FsmReadInputVars(fsm);
1331  array_t       *newInputVarArray = array_alloc(int, 0);
1332
1333  array_free(inputVarArray);
1334  (void) Fsm_FsmSetInputVars(fsm, newInputVarArray);
1335
1336  return(subSystem);
1337}
1338#endif
Note: See TracBrowser for help on using the repository browser.