source: vis_dev/vis-2.3/src/grab/grab.c @ 50

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

vis2.3
File size: 39.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [grab.c]
4
5  PackageName [grab]
6
7  Synopsis    [Abstraction refinement for large scale invariant checking.]
8
9  Description [This file contains the functions to check invariant
10  properties by the GRAB abstraction refinement algorithm. GRAB stands
11  for "Generational Refinement of Ariadne's Bundle," in which the
12  automatic refinement is guided by all shortest abstract
13  counter-examples. For more information, please check the ICCAD'03
14  paper of Wang et al., "Improving Ariadne's Bundle by Following
15  Multiple Counter-Examples in Abstraction Refinement." ]
16 
17  Author      [Chao Wang]
18
19  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
20  All rights reserved.
21
22  Permission is hereby granted, without written agreement and without
23  license or royalty fees, to use, copy, modify, and distribute this
24  software and its documentation for any purpose, provided that the
25  above copyright notice and the following two paragraphs appear in
26  all copies of this software.]
27
28******************************************************************************/
29
30#include "grabInt.h"
31
32/*---------------------------------------------------------------------------*/
33/* Constant declarations                                                     */
34/*---------------------------------------------------------------------------*/
35
36/*---------------------------------------------------------------------------*/
37/* Structure declarations                                                    */
38/*---------------------------------------------------------------------------*/
39
40/*---------------------------------------------------------------------------*/
41/* Type declarations                                                         */
42/*---------------------------------------------------------------------------*/
43
44/*---------------------------------------------------------------------------*/
45/* Variable declarations                                                     */
46/*---------------------------------------------------------------------------*/
47static jmp_buf timeOutEnv;
48
49/*---------------------------------------------------------------------------*/
50/* Macro declarations                                                        */
51/*---------------------------------------------------------------------------*/
52
53/**AutomaticStart*************************************************************/
54
55/*---------------------------------------------------------------------------*/
56/* Static function prototypes                                                */
57/*---------------------------------------------------------------------------*/
58
59static int CommandGrab(Hrc_Manager_t ** hmgr, int argc, char ** argv);
60static void TimeOutHandle(void);
61
62/**AutomaticEnd***************************************************************/
63
64/*---------------------------------------------------------------------------*/
65/* Definition of exported functions                                          */
66/*---------------------------------------------------------------------------*/
67
68/**Function********************************************************************
69
70  Synopsis    [Initializes the grab package. The added command is for
71  testing purpose only; the same algorithm can be activated by the
72  check_invariant command.]
73
74  SideEffects []
75
76  SeeAlso     [Refine_End]
77
78******************************************************************************/
79void
80Grab_Init(void)
81{
82  /*
83   * Add a command to the global command table.  By using the leading
84   * underscore, the command will be listed under "help -a" but not "help".
85   */
86  Cmd_CommandAdd("_grab_test", CommandGrab,  0);
87}
88
89
90/**Function********************************************************************
91
92  Synopsis    [Ends the grab package.]
93
94  SideEffects []
95
96  SeeAlso     [Refine_Init]
97
98******************************************************************************/
99void
100Grab_End(void)
101{
102
103}
104
105
106/**Function********************************************************************
107
108  Synopsis    [Check invariant formulae with abstraction refinement method
109  Grab.]
110
111  Description [Check invariant formulae with the GRAB abstraction
112  refinement method. For each formula, an small initial abstract model
113  is constructed, which contains only the state variables mentioned by
114  the formula. The abstract model is then gradually refined by adding
115  more state variables and Boolean network variables (Bnvs), until it
116  is sufficient to decided the property. Bnvs are internal nodes of
117  the circuit---they are selected in order to partition large
118  combinational logic cones into smaller pieces. The selection of
119  refinement variables (both state vars and Bnvs) is based on the
120  analysis of all the shortest counter-examples, which are captured by
121  a data structure called the Synchronous Onion Rings (SORs). For the
122  algorithmic details, please check the ICCAD'03 paper of Wang et al.,
123  "Improving Ariadne's Bundle by Following Multiple Counter-Examples
124  in Abstraction Refinement," and the ICCD'04 paper of Wang et al.,
125  "Fine-Grain Abstraction and Sequential Don't Cares for Large Scale
126  Model Checking."
127
128  The existence of a network partition is not mandatory for calling
129  this function. However, if it does exist, it will be used by this
130  function; otherwise, the network partition will be constructed
131  incrementally as the abstract model grows. If the default bdd
132  manager is not available, this function will create one and assign
133  bdd ids incrementally as the abstract model grows. (For extremely
134  large models, it is favorable to let the procedure assign bdd ids
135  and construct the partition incrementally.)
136
137  The parameter refineAlgorithm specifies the refinement variable
138  selection algorithm---currently, only GRAB is available. When
139  fineGrainFlag is FALSE, only latches are considered as the
140  abstraction "atoms"; When fineGrainFlag is TRUE, both Bnvs and
141  latches are considered "atoms." To disable the greedy minimization
142  of refinement sets, set refineMinFlag to FALSE. The parameter
143  useArdcFlag is not used at this point. By default, all the shortest
144  counter-examples are analyzed (cexType==GRAB_CEX_SOR); when cexType
145  is set to GRAB_CEX_MINTERM or GRAB_CEX_CUBE, only a minterm or cube
146  state path is analyzed---these two options may be helpful if there
147  is too much overhead of computing the entire SORs.]
148
149  SideEffects [Nothing related to the network is changed: if the
150  default partition and mdd manager are available, they will be left
151  intact; if they are not available, the incrementally created new
152  partition and mdd manager will be freed before exit.]
153
154******************************************************************************/ 
155void 
156Grab_NetworkCheckInvariants(
157  Ntk_Network_t *network,
158  array_t *InvariantFormulaArray,
159  char *refineAlgorithm,
160  int fineGrainFlag,
161  int refineMinFlag,
162  int useArdcFlag,
163  int cexType,
164  int verbosity,
165  int dbgLevel,
166  int printInputs,
167  FILE *debugFile,
168  int useMore,
169  char *driverName)
170{
171  mdd_manager     *mddManager = NIL(mdd_manager);
172  graph_t         *partition;
173  Ctlp_Formula_t  *invFormula;
174  Ctlsp_Formula_t *invFormula_sp;
175  array_t         *invStatesArray;
176  array_t         *resultArray;
177  st_table        *absLatchTable, *absBnvTable;
178  st_table        *coiLatchTable, *coiBnvTable;
179  Fsm_Fsm_t       *absFsm;
180  array_t         *visibleVarMddIds, *invisibleVarMddIds;
181  int             concreteLatchCount, abstractLatchCount;
182  int             concreteBnvCount, abstractBnvCount;
183  st_table        *nodeToFaninNumberTable;
184  mdd_t           *rchStates, *invStates = NIL(mdd_t); /*=mdd_one(mddManager);*/
185  array_t         *SORs, *save_SORs;
186  boolean         refineDirection, runMinimization, isLastStep;
187  int             staticOrderFlag, partitionFlag;
188  int             cexLength, refineIteration;
189  array_t         *addedVarsAtCurrentLevel = NIL(array_t);
190  array_t         *addedBnvsAtCurrentLevel = NIL(array_t);
191  int             auxValue1, auxValue2, flag, i;
192
193  long            startTime, endTime, totalTime;
194  long            mcStartTime, mcEndTime, mcTime;
195  long            sorEndTime, sorTime;
196  long            conEndTime, conTime;
197  long            dirStartTime, dirEndTime, dirTime;
198  long            refStartTime, refEndTime, refTime;
199  long            miniStartTime, miniEndTime, miniTime;
200
201
202  if ( strcmp(refineAlgorithm, "GRAB") ) {
203    fprintf(vis_stdout, 
204            "** ci error: Abstraction refinement method %s not available\n", 
205            refineAlgorithm);
206    return;
207  }
208
209  /* if the mddIds haven't been assigned to the network nodes,
210   * we assign them incrementally (i.e., staticOrderFlag==1).
211   */
212  mddManager = Ntk_NetworkReadMddManager(network);
213  if (mddManager == NIL(mdd_manager))
214    staticOrderFlag = 1;
215  else
216    staticOrderFlag = 0;
217
218  if (staticOrderFlag) {
219    GrabNtkClearAllMddIds(network);
220    mddManager = Ntk_NetworkInitializeMddManager(network);
221    if (verbosity >= 2)
222      bdd_dynamic_reordering(mddManager, BDD_REORDER_SIFT, 
223                             BDD_REORDER_VERBOSITY);
224    else
225      bdd_dynamic_reordering(mddManager, BDD_REORDER_SIFT, 
226                             BDD_REORDER_NO_VERBOSITY);
227  }
228
229  /* if the partition hasn't been created, we create the partition
230   * incrementally (i.e., partitionFlag==1)
231   */
232  partition = Part_NetworkReadPartition(network);
233  if (partition == NIL(graph_t))
234    partitionFlag = GRAB_PARTITION_BUILD;
235  else
236    partitionFlag = GRAB_PARTITION_NOCHANGE;
237
238  /* used by the refinement algorithm as a tie-breaker */
239  nodeToFaninNumberTable = st_init_table(st_ptrcmp, st_ptrhash);
240
241  /***************************************************************************
242   * check the invariants
243   ***************************************************************************/
244  resultArray = array_alloc(int, array_n(InvariantFormulaArray));
245
246  arrayForEachItem(Ctlp_Formula_t *, InvariantFormulaArray, i, invFormula) {
247    invFormula_sp = Ctlsp_CtlFormulaToCtlsp(invFormula);
248
249    /* this is required for the following code to function correctly */
250    visibleVarMddIds = invisibleVarMddIds = NIL(array_t);
251    invStatesArray = SORs = save_SORs = NIL(array_t);
252
253    mcTime = sorTime = conTime = dirTime = refTime = miniTime = 0;
254    startTime = util_cpu_ctime(); 
255
256    /* record the number of latches in the cone-of-influence */
257    coiLatchTable = GrabComputeCOIAbstraction(network, invFormula);
258    concreteLatchCount = st_count(coiLatchTable);
259    /* build the initial abstract model */
260    absLatchTable = GrabComputeInitialAbstraction(network, invFormula);
261    abstractLatchCount = st_count(absLatchTable);
262    if (verbosity >= 3) {
263      GrabPrintNodeHashTable("InitialAbstractLatches", absLatchTable);
264    }
265
266    /* initialize the abs./concrete table for boolean network variables*/
267    coiBnvTable = st_init_table(st_ptrcmp, st_ptrhash);
268    abstractBnvCount = concreteBnvCount = 0;
269    if (fineGrainFlag == 1) {
270      absBnvTable = st_init_table(st_ptrcmp, st_ptrhash);
271    }else {
272      absBnvTable = NIL(st_table); 
273    }
274    /* if the concrete partition is available, retrieve form it the
275     * bnvs; otherwise, we incrementally create bnvs (for the current
276     * absLatches only)---this is designed for performance concerns */
277    if (partitionFlag == GRAB_PARTITION_NOCHANGE) {
278      Part_PartitionReadOrCreateBnvs(network, coiLatchTable, coiBnvTable);
279      concreteBnvCount = st_count(coiBnvTable);
280    }
281   
282    /* Outer Loop---Over Refinements For Different SOR Lengths
283     */
284    refineIteration = 0;
285    isLastStep = 0;
286    while(1) {
287      long  grabStartTime = util_cpu_ctime();
288     
289      /* Build the Abstract Finite State Machine  */
290      absFsm = GrabCreateAbstractFsm(network, coiBnvTable, absLatchTable,
291                                     absBnvTable, partitionFlag, TRUE);
292      concreteBnvCount = st_count(coiBnvTable);     
293      invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm, absLatchTable,
294                                                     absBnvTable);
295      visibleVarMddIds = GrabGetVisibleVarMddIds(absFsm, absLatchTable);
296      /* sanity check  */
297      isLastStep = (array_n(invisibleVarMddIds)==0);
298      if (isLastStep) {
299        assert(abstractLatchCount == concreteLatchCount);
300      }
301
302      /* Compute The Invariant States If They Are Not Available  */
303      if (invStatesArray == NIL(array_t)) {
304        mdd_t * tautology = mdd_one(mddManager);
305        array_t *careSetArray = array_alloc(mdd_t *, 0);
306        array_insert(mdd_t *, careSetArray, 0, tautology);
307        invStates = Mc_FsmEvaluateFormula(absFsm, invFormula, tautology,
308                                          NIL(Fsm_Fairness_t), careSetArray,
309                                          MC_NO_EARLY_TERMINATION,
310                                          NIL(Fsm_HintsArray_t), Mc_None_c,
311                                          McVerbosityNone_c, McDcLevelNone_c,
312                                          0, McGSH_EL_c);
313        mdd_array_free(careSetArray);
314        invStatesArray = array_alloc(mdd_t *, 0);
315        array_insert(mdd_t *, invStatesArray, 0, invStates);
316      }
317
318      /* Conduct Forward Reachability Analysis  */
319      rchStates = GrabFsmComputeReachableStates(absFsm, 
320                                                 absLatchTable,
321                                                 absBnvTable,
322                                                 invStatesArray,
323                                                 verbosity);
324
325      mcEndTime = util_cpu_ctime();
326      mcTime += (mcEndTime - grabStartTime);
327      if (verbosity >= 1) {
328        fprintf(vis_stdout, 
329        "-- grab: absLatch [%d/%d], absBnv [%d/%d], mc  time is %5g s\n",
330                abstractLatchCount, concreteLatchCount, 
331                abstractBnvCount, concreteBnvCount,
332                (double)(mcEndTime-grabStartTime)/1000.0);
333      }
334
335      /* if bad states cannot be reached, the property is true;
336       * if absFsm is concrete, the property is false
337       */
338      flag = mdd_lequal(rchStates, invStates, 1, 1);
339      mdd_free(rchStates);
340      if (flag || isLastStep) {
341        /* set the debugging info, if necessary */
342        if (!flag)
343          SORs = mdd_array_duplicate(Fsm_FsmReadReachabilityOnionRings(absFsm));
344        Fsm_FsmSubsystemFree(absFsm);
345        absFsm = NIL(Fsm_Fsm_t);
346        array_free(invisibleVarMddIds);
347        array_free(visibleVarMddIds);
348        break;
349      }
350
351      /* Build The Synchronous Onion Rings (SORs) */
352      Fsm_FsmFreeImageInfo(absFsm);
353      SORs = GrabFsmComputeSynchronousOnionRings(absFsm, absLatchTable, 
354                                                 absBnvTable, NIL(array_t),
355                                                 invStates, cexType, 
356                                                 verbosity);
357      sorEndTime = util_cpu_ctime();
358      sorTime += (sorEndTime - mcEndTime);
359     
360      /* Concretize Multiple Counter-Examples */
361      cexLength = array_n(SORs)-1;
362      flag = !Bmc_AbstractCheckAbstractTraces(network, SORs, coiLatchTable, 
363                                              0, dbgLevel, printInputs);
364      conEndTime = util_cpu_ctime();
365      conTime += (conEndTime - sorEndTime);
366      if (!flag) {
367        if (verbosity >= 1) 
368          fprintf(vis_stdout, 
369          "-- grab: find length-%d concrete counter-examples\n", 
370                cexLength);
371        Fsm_FsmSubsystemFree(absFsm);
372        absFsm = NIL(Fsm_Fsm_t);
373        array_free(invisibleVarMddIds);
374        array_free(visibleVarMddIds);
375        break;
376      }else {
377        if (verbosity >= 2) 
378          fprintf(vis_stdout, 
379          "-- grab: find length-%d spurious counter-examples\n", 
380                  cexLength);
381      }
382
383      /* Innor Loop---Over Refinements For The Same SOR Length
384       */
385      save_SORs = mdd_array_duplicate(SORs);
386      addedVarsAtCurrentLevel = array_alloc(int, 0);
387      addedBnvsAtCurrentLevel = array_alloc(int, 0);
388      refineDirection = 1;
389      runMinimization = 0;
390
391      while (1) {
392       
393        int skip_refinement = 0;
394
395        /* Get the appropriate refinement direction:
396         *    runMinimization==1  -->  BOOLEAN
397         *    fineGrainFlag==0   -->  SEQUENTIAL
398         *    coiBnvTable is empty  -->  SEQUENTIAL
399         *    refineDirection==0  -->  BOOLEAN
400         */
401        if ( !runMinimization && refineDirection) {
402          if ( fineGrainFlag && st_count(coiBnvTable)>0 ) {
403            dirStartTime = util_cpu_ctime();
404#if 0 
405            refineDirection = !GrabTestRefinementSetSufficient(network,
406                                                               save_SORs,
407                                                               absLatchTable,
408                                                               verbosity);
409#endif
410            runMinimization = (refineDirection==0);
411            dirEndTime = util_cpu_ctime();
412            dirTime += (dirEndTime - dirStartTime);
413          }
414        }
415
416        if (verbosity >= 3 && refineDirection==0)
417          fprintf(vis_stdout, "refinement is in %s direction\n", 
418                  (refineDirection? "both":"boolean"));
419
420        /* Minimize the refinement set of latches  */
421        if (runMinimization) { 
422          int n_latches = st_count(absLatchTable);
423          int break_flag;
424          if (refineMinFlag && array_n(addedVarsAtCurrentLevel) > 1) {
425            miniStartTime = util_cpu_ctime();
426            GrabMinimizeLatchRefinementSet(network, 
427                                           &absLatchTable,
428                                           &absBnvTable,
429                                           addedVarsAtCurrentLevel,
430                                           &addedBnvsAtCurrentLevel,
431                                           save_SORs,
432                                           verbosity);
433            abstractLatchCount = st_count(absLatchTable);
434            abstractBnvCount = absBnvTable? st_count(absBnvTable):st_count(coiBnvTable);
435            array_free(addedVarsAtCurrentLevel);
436            addedVarsAtCurrentLevel = array_alloc(int, 0);         
437            miniEndTime = util_cpu_ctime();
438            miniTime += (miniEndTime - miniStartTime);
439          }
440
441          /* if the refinement set of bnvs is also sufficient, break */
442          break_flag = 1;
443          if (fineGrainFlag && st_count(coiBnvTable)>0) {
444            dirStartTime = util_cpu_ctime();
445            break_flag = GrabTestRefinementBnvSetSufficient(network,
446                                                            coiBnvTable,
447                                                            save_SORs, 
448                                                            absLatchTable,
449                                                            absBnvTable,
450                                                            verbosity);
451            dirEndTime = util_cpu_ctime();
452            dirTime += (dirEndTime - dirStartTime);
453          }
454          if (break_flag) {
455            if (verbosity >= 1)
456              fprintf(vis_stdout, 
457              "-- grab: remove length-%d spurious counter-examples\n\n",
458                      cexLength);
459            break;
460          }
461
462          /* Otherwise, skip this refinement step, because the
463           * current absFsm is not well-defined (some latches have
464           * been droped)
465           */
466          SORs = mdd_array_duplicate(save_SORs);
467          if (n_latches > st_count(absLatchTable))
468            skip_refinement = 1;
469
470          refineDirection = 0;
471          runMinimization = 0;
472        }
473     
474        /* compute the refinement (by Grab)
475         */
476        if (!skip_refinement) {
477          array_t *addedVars = array_alloc(int, 0);
478          array_t *addedBnvs = array_alloc(int, 0);
479          auxValue1 = st_count(absLatchTable) + 
480            ((absBnvTable==NIL(st_table))? 0:st_count(absBnvTable));
481
482          refStartTime = util_cpu_ctime();
483
484          /* create the abstract fsm   */
485          Fsm_FsmSubsystemFree(absFsm);
486          absFsm = GrabCreateAbstractFsm(network, coiBnvTable, absLatchTable,
487                                         absBnvTable, 
488                                         GRAB_PARTITION_NOCHANGE, 
489                                         FALSE);
490          /* pick refinement variables */
491          GrabRefineAbstractionByGrab(absFsm, 
492                                      SORs,
493                                      absLatchTable,
494                                      absBnvTable,
495                                      addedVars,
496                                      addedBnvs,
497                                      refineDirection,
498                                      nodeToFaninNumberTable,
499                                      verbosity);
500          array_append(addedVarsAtCurrentLevel, addedVars);
501          array_append(addedBnvsAtCurrentLevel, addedBnvs);
502          array_free(addedVars);
503          array_free(addedBnvs);
504          /* Sanity check! */
505          auxValue2 = st_count(absLatchTable) + 
506            ((absBnvTable==NIL(st_table))? 0:st_count(absBnvTable));
507          assert(auxValue1 < auxValue2);
508
509          abstractLatchCount = st_count(absLatchTable);
510          abstractBnvCount = absBnvTable? st_count(absBnvTable):st_count(coiBnvTable);
511         
512          refEndTime = util_cpu_ctime();
513          refTime += (refEndTime - refStartTime);
514          if (verbosity >= 3) {
515            fprintf(vis_stdout, 
516              "-- grab: absLatch [%d/%d], absBnv [%d/%d], ref time is %5g s\n",
517                    abstractLatchCount, concreteLatchCount, 
518                    abstractBnvCount, concreteBnvCount,
519                    (double)(refEndTime - refStartTime)/1000.0);
520          }
521
522          refineIteration++;
523        }
524     
525        /* Create The Refined Abstract FSM */
526        Fsm_FsmSubsystemFree(absFsm);
527        array_free(invisibleVarMddIds);
528        array_free(visibleVarMddIds);
529        absFsm = GrabCreateAbstractFsm(network, coiBnvTable, absLatchTable,
530                                       absBnvTable, partitionFlag, TRUE);
531        invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm, absLatchTable,
532                                                       absBnvTable);
533        visibleVarMddIds = GrabGetVisibleVarMddIds(absFsm, absLatchTable);
534        concreteBnvCount = st_count(coiBnvTable);       
535        /* sanity check */
536        isLastStep = (array_n(invisibleVarMddIds)==0);
537        if (isLastStep) {
538          assert(abstractLatchCount == concreteLatchCount);
539        }
540
541        /* Reduce The Current SORs (with forward reachability analysis) */
542        mcStartTime = util_cpu_ctime();
543        rchStates = GrabFsmComputeConstrainedReachableStates(absFsm, 
544                                                             absLatchTable,
545                                                             absBnvTable,
546                                                             SORs, 
547                                                             verbosity);
548        mdd_array_free(SORs);
549        SORs = NIL(array_t);
550        mcEndTime = util_cpu_ctime();
551        mcTime += (mcEndTime - mcStartTime);
552        if (verbosity >= 2) {
553          fprintf(vis_stdout, 
554              "-- grab: absLatch [%d/%d], absBnv [%d/%d], mc  time is %5g s\n",
555                  abstractLatchCount, concreteLatchCount, 
556                  abstractBnvCount, concreteBnvCount,
557                  (double)(mcEndTime-mcStartTime)/1000.0);
558        }
559
560        /* if bad states is no longer reachable, break out  */
561        flag = mdd_lequal(rchStates, invStates, 1, 1);
562        mdd_free(rchStates);
563        if (isLastStep || flag) {
564          if (!isLastStep && refineDirection == 1) {
565            runMinimization = 1;
566            refineDirection = 0;
567            continue;
568          }else
569            break;
570        }
571
572        /* Build the new SORs (with backward reachability analysis)  */
573        Fsm_FsmFreeImageInfo(absFsm);
574        SORs = GrabFsmComputeSynchronousOnionRings(absFsm, 
575                                                   absLatchTable, 
576                                                   absBnvTable,
577                                                   NIL(array_t), 
578                                                   invStates,
579                                                   cexType, 
580                                                   verbosity);
581        sorEndTime = util_cpu_ctime();
582        sorTime += (sorEndTime - mcEndTime);
583
584      } /* End of the Inner Loop */
585
586
587      /* Minimize The Refinement Set of Boolean Network Variables (BNVs)
588       */
589      if (fineGrainFlag==1 && refineMinFlag
590          && array_n(addedBnvsAtCurrentLevel)>1) {
591
592        miniStartTime = util_cpu_ctime();
593        GrabMinimizeBnvRefinementSet(network, 
594                                     coiBnvTable,
595                                     absLatchTable,
596                                     &absBnvTable,
597                                     addedBnvsAtCurrentLevel,
598                                     save_SORs,
599                                     verbosity);
600        abstractLatchCount = st_count(absLatchTable);
601        abstractBnvCount = st_count(absBnvTable);
602        miniEndTime = util_cpu_ctime();
603        miniTime += (miniEndTime - miniStartTime);
604      }
605      mdd_array_free(save_SORs);
606
607      /* Clean-ups
608       */
609      Fsm_FsmSubsystemFree(absFsm);
610      absFsm = NIL(Fsm_Fsm_t);
611      array_free(invisibleVarMddIds);
612      array_free(visibleVarMddIds);
613      array_free(addedVarsAtCurrentLevel);
614      array_free(addedBnvsAtCurrentLevel);
615      addedVarsAtCurrentLevel = NIL(array_t);
616      addedBnvsAtCurrentLevel = NIL(array_t);
617
618    } /* End of the Outer Loop */
619
620    endTime = util_cpu_ctime();
621    totalTime = endTime - startTime;
622
623    /* Print out the debugging information */
624    if (dbgLevel > 0) {
625      FILE        *tmpFile = vis_stdout;
626      extern FILE *vis_stdpipe;
627
628      if (debugFile)
629        vis_stdpipe = debugFile;
630      else if (useMore)
631        vis_stdpipe = popen("more", "w");
632      else
633        vis_stdpipe = vis_stdout;
634      vis_stdout = vis_stdpipe;
635     
636      if (flag) {
637        fprintf(vis_stdout, "# %s: formula passed --- ", driverName);
638        Ctlp_FormulaPrint(vis_stdout, invFormula);
639        fprintf(vis_stdout, "\n");
640      }else {
641        if(dbgLevel != 2)
642        {
643           fprintf(vis_stdout, "# %s: formula p%d failed --- ", driverName, i+1);
644           Ctlp_FormulaPrint(vis_stdout, invFormula);
645           fprintf(vis_stdout, "\n# %s: calling debugger\n", driverName);
646        }
647        flag = !Bmc_AbstractCheckAbstractTraces(network, SORs, coiLatchTable,
648                                                1, dbgLevel, printInputs);
649      }
650
651      if (vis_stdout != tmpFile && vis_stdout != debugFile)
652        (void)pclose(vis_stdpipe);
653      vis_stdout = tmpFile;
654    }
655
656    if (verbosity >= 2 ) {
657      fprintf(vis_stdout, "\n-- grab: total cpu time = %5g\n", 
658              (double)totalTime/1000.0);
659      if (verbosity >= 3) {
660        fprintf(vis_stdout,   "-- grab:       mc  time = %5.1f\t(%3.1f%%)\n", 
661                (double)mcTime/1000.0, (100.0*mcTime/totalTime));
662        fprintf(vis_stdout,   "-- grab:       sor time = %5.1f\t(%3.1f%%)\n", 
663                (double)sorTime/1000.0, (100.0*sorTime/totalTime));
664        fprintf(vis_stdout,   "-- grab:       con time = %5.1f\t(%3.1f%%)\n", 
665                (double)conTime/1000.0, (100.0*conTime/totalTime));
666        fprintf(vis_stdout,   "-- grab:       ref time = %5.1f\t(%3.1f%%)\n", 
667                (double)refTime/1000.0, (100.0*refTime/totalTime));
668        fprintf(vis_stdout,   "-- grab:       min time = %5.1f\t(%3.1f%%)\n", 
669                (double)miniTime/1000.0,(100.0*miniTime/totalTime));
670        fprintf(vis_stdout,   "-- grab:       dir time = %5.1f\t(%3.1f%%)\n", 
671                (double)dirTime/1000.0, (100.0*dirTime/totalTime));
672      }
673    }
674
675    if (verbosity >= 1) {
676      if (concreteLatchCount > 0) {
677        fprintf(vis_stdout, "-- grab: abs latch percentage = %d %%\n", 
678              100 * abstractLatchCount/concreteLatchCount );
679      }
680      if (verbosity >= 3) {
681        fprintf(vis_stdout, "-- grab: abs latch = %d\n", abstractLatchCount);
682        fprintf(vis_stdout, "-- grab: coi latch = %d\n", concreteLatchCount);
683      }
684      if (concreteBnvCount > 0) {
685        fprintf(vis_stdout, "-- grab: abs bnv   percentage = %d %%\n", 
686                (100 * abstractBnvCount/concreteBnvCount) );
687        if (verbosity >= 3) {
688          fprintf(vis_stdout, "-- grab: abs bnv   = %d\n", abstractBnvCount);
689          fprintf(vis_stdout, "-- grab: coi bnv   = %d\n", concreteBnvCount);
690        }
691        abstractBnvCount += abstractLatchCount;
692        concreteBnvCount += concreteLatchCount;
693        fprintf(vis_stdout, "-- grab: total abs var percentage  = %d %%\n", 
694                (100 * abstractBnvCount/concreteBnvCount) );
695        if (verbosity >= 3) {
696          fprintf(vis_stdout, "-- grab:       abs var  = %d\n", 
697                  abstractBnvCount);
698          fprintf(vis_stdout, "-- grab:       coi var  = %d\n", 
699                  concreteBnvCount);
700        }
701      }
702      fprintf(vis_stdout, "-- grab: total refinement iterations = %d\n", 
703              refineIteration);
704      fprintf(vis_stdout,  "-- grab: total image    computations %d\n",
705              Img_GetNumberOfImageComputation(Img_Forward_c));
706      fprintf(vis_stdout,  "-- grab: total preimage computations %d\n",
707              Img_GetNumberOfImageComputation(Img_Backward_c));
708
709      if (verbosity >= 3) {
710        GrabPrintNodeHashTable("AbstractLatchRankings", absLatchTable);
711        if (fineGrainFlag)
712          GrabPrintNodeHashTable("AbstractBnvRankings", absBnvTable);
713      }
714    }
715
716    /* Clean-up's
717     */
718    st_free_table(coiLatchTable);
719    st_free_table(absLatchTable);
720    st_free_table(coiBnvTable);
721    if (fineGrainFlag) {
722      st_free_table(absBnvTable);
723    }
724    mdd_array_free(invStatesArray);
725    if (!flag)  mdd_array_free(SORs);
726
727    Ctlsp_FormulaFree(invFormula_sp);
728
729    /* Store the verification results in an array (1--passed, 0--failed) */
730    array_insert(int, resultArray, i, flag);
731  }
732
733  /* print whether the set of invariants passed or failed
734   */
735  fprintf(vis_stdout, "\n# %s: Summary of invariant pass/fail\n", driverName);
736  arrayForEachItem(Ctlp_Formula_t *, InvariantFormulaArray, i, invFormula) {
737    flag = array_fetch(int, resultArray, i);
738    if (flag) {
739      (void) fprintf(vis_stdout, "# %s: formula passed --- ", driverName);
740      Ctlp_FormulaPrint(vis_stdout, (invFormula));
741      fprintf(vis_stdout, "\n");
742    } else {
743      (void) fprintf(vis_stdout, "# %s: formula failed --- ", driverName);
744      Ctlp_FormulaPrint(vis_stdout, (invFormula));
745      fprintf(vis_stdout, "\n");
746    }
747  }
748
749  /* free the current partition and mdd manager if necessary */
750  if (partitionFlag) {
751    Ntk_NetworkFreeApplInfo(network, PART_NETWORK_APPL_KEY);
752  }
753  if (staticOrderFlag) {
754    mdd_quit(mddManager);
755    Ntk_NetworkSetMddManager(network, NIL(mdd_manager));
756    GrabNtkClearAllMddIds(network);
757  }
758  st_free_table(nodeToFaninNumberTable);
759  array_free(resultArray);
760
761}
762
763
764/*---------------------------------------------------------------------------*/
765/* Definition of internal functions                                          */
766/*---------------------------------------------------------------------------*/
767
768
769/*---------------------------------------------------------------------------*/
770/* Definition of static functions                                            */
771/*---------------------------------------------------------------------------*/
772
773/**Function********************************************************************
774
775  Synopsis    [Implements the test command for Grab.]
776
777  CommandName [_grab_test]
778
779  CommandSynopsis [Performs invairant checking on a flattened network
780  with the GRAB abstraction refinement algorithm.]
781
782  CommandArguments [ \[-a &lt;refine_algorithm&gt;\] \[-c &lt;cex_type&gt;\]
783  \[-d &lt;dbg_level&gt;\] \[-F\] \[-M\] \[-i\] \[-m\]
784  \[-t &lt;time_out_period&gt;\] \[-v &lt;verbosity_level&gt;\]
785  \[-f &lt;dbg_file&gt;\] \[-h\]  &lt;inv_file&gt;]
786
787  CommandDescription [Performs invairant checking on a flattened
788  network with the GRAB abstraction refinement algorithm.  Before
789  calling this command, the user should have created the flattened
790  netowrk by calling the commands <A
791  HREF="flatten_hierarchyCmd.html"><code> flatten_hierarchy</code></A>
792  and <A
793  HREF="build_partition_maigsCmd.html"><code>build_partition_maigs</code></A>.
794  The default BDD manager and network partition are not mandatory for
795  calling this command, though they will be used if available. (In
796  other words, the user doesn't have to run the commands <A
797  HREF="static_orderCmd.html"><code>static_order</code></A> and <A
798  HREF="build_partition_mddsCmd.html"><code>build_partition_mdds</code></A>
799  before calling this command.)
800
801  Regardless of the options, no 'false positive' or 'false negatives'
802  will occurs: the result is correct for the given model.
803
804  Properties to be verified should be provided as invariant formulae
805  in the file <code>inv_file</code>. Node that the support of any wire
806  referred to in a formula should consist only of latches. For the
807  precise syntax of CTL and LTL formulas, see the <A
808  HREF="../ctl/ctl/ctl.html"> VIS CTL and LTL syntax
809  manual</A>.  <p>
810
811  If a formula does not pass, a proof of failure (referred to as a
812  counter-example) is demonstrated. Whether demostrate the proof or
813  not can be specified (see option <code>-d</code>).  <p>
814
815  Command options:
816  <p>
817
818  <dl>
819
820  <dt> -a <code> &lt;refine_algorithm&gt; </code>
821  <dd> Specify the refinement variable selection algorithm.
822  <p>
823  <dd> <code>refine_algorithm</code> must be one of the following:
824 
825  <p><code>GRAB</code>: the GRAB refinement method (Default).
826 
827  <p>
828
829  <dt> -c <code> &lt;cex_type&gt; </code> <dd> Specify the type of
830  abstract counter-examples used in the analysis.
831  <p>
832 
833  <dd> <code>cex_type</code> must be one of the following:
834 
835  <p><code>0</code>: minterm state counter-example.
836  <p><code>1</code>: cube state counter-example.
837  <p><code>2</code>: synchronous onion rings (Default).
838  <p>
839
840  <dt> -d <code> &lt;dbg_level&gt; </code>
841  <dd> Specify whether to demonstrate a counter-example when the
842  system fails a formula being checked.
843
844  <p> <dd> <code> dbg_level</code> must be one of the following:
845
846  <p><code>0</code>: No debugging performed.
847  <code>dbg_level</code>=<code>0</code> is the default.
848
849  <p><code>1</code>: Generate a counter-example (a path to a fair cycle).
850  <p>
851
852  <dt> -F <code> &lt;finegrain_flag&gt; </code> <dd> Enable or disable
853  the use of fine-grain abstraction.
854  <p>
855 
856  <dd> <code>finegrain_flag</code> must be one of the following:
857 
858  <p><code>0</code>: disable fine-grain abstraction.
859  <p><code>1</code>: enable fine-grain abstraction (Default).
860  <p>
861
862  <dt> -M <code> &lt;refinemin_flag&gt; </code> <dd> Enable or disable
863  the use of greedy refinement minimization.
864  <p>
865 
866  <dd> <code>refinemin_flag</code> must be one of the following:
867 
868  <p><code>0</code>: disable greedy refinement minimization.
869  <p><code>1</code>: enable greedy refinement minimization (Default).
870  <p>
871
872  <dt> -i
873  <dd> Print input values causing transitions between states during debugging.
874  Both primary and pseudo inputs are printed.
875  <p>
876
877  <dt> -m
878  <dd> Pipe debugger output through the UNIX utility  more.
879  <p>
880
881  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
882  <dd> Specify the time out period (in seconds) after which the command aborts.
883  By default this option is set to infinity.
884  <p>
885
886   <dt> -v  <code>&lt;verbosity_level&gt;</code>
887  <dd> Specify verbosity level. This sets the amount of feedback  on CPU usage
888  and code status.
889
890  <br><code>verbosity_level</code>  must be one of the following:<p>
891 
892  <code>0</code>: No feedback provided. This is the default.<p>
893
894  <code>1</code>: Feedback on code location.<p>
895
896  <code>2</code>: Feedback on code location and CPU usage.<p>
897
898  <p>
899
900  <dt> -f  <code>&lt;dbg_out&gt;</code>
901  <dd> Specify the name of the file ot which error trace is written.
902  <p>
903
904  <dt> -h
905  <dd> Print the command usage.
906  <p>
907 
908  See also commands : model_check, check_invariant ]
909
910  SideEffects []
911
912******************************************************************************/
913static int
914CommandGrab(
915  Hrc_Manager_t ** hmgr,
916  int              argc,
917  char **          argv)
918{
919  int             c, verbosity;
920  char            InvFileName[256];
921  FILE            *FP, *dbgFile;
922  array_t         *InvariantFormulaArray;
923  Ntk_Network_t   *network;
924  static int      timeOutPeriod = 0;
925 
926  char       refineAlgorithm[256];
927  int        cexType = 0; 
928  int        refineMinFlag;
929  int        fineGrainFlag;
930  int        useArdcFlag = 0;
931  long       startTime, endTime;
932
933  char       *dbgFileName = NIL(char);
934  int        dbgLevel, printInputs, useMore;
935
936  startTime = util_cpu_ctime();
937
938  Img_ResetNumberOfImageComputation(Img_Both_c);
939
940  /* the default setting is Grab+,
941   * Generational Refinement of Ariadne's Bundle of SORs
942   */
943  strcpy(refineAlgorithm, "GRAB");
944  cexType = GRAB_CEX_SOR;
945  fineGrainFlag = 1;
946  refineMinFlag = 1;
947  verbosity = 0;
948
949  dbgLevel = 0;
950  printInputs = 0;
951  useMore = 0;
952 
953  /*
954   * Parse command line options.
955   */
956  util_getopt_reset();
957  while ((c = util_getopt(argc, argv, "a:c:d:F:M:imt:v:f:h")) != EOF) {
958    switch(c) {
959      case 'a':
960        strcpy(refineAlgorithm, util_optarg);
961        break;
962      case 'F':
963        fineGrainFlag = atoi(util_optarg);
964        break;
965      case 'M':
966        refineMinFlag = atoi(util_optarg);
967        break;
968      case 'c':
969        cexType = atoi(util_optarg);
970        break;
971      case 'D':
972        useArdcFlag = 1;
973        break;
974      case 't':
975        timeOutPeriod = atoi(util_optarg);
976        break;
977      case 'v':
978        verbosity = atoi(util_optarg);
979        break;
980      case 'd':
981        dbgLevel = atoi(util_optarg);
982        break;
983      case 'i':
984        printInputs = 1;
985        break;
986      case 'm':
987        useMore = 1;
988        break;
989      case 'f':
990        dbgFileName = util_strsav(util_optarg);
991        break;
992      case 'h':
993        goto usage;
994      default:
995        goto usage;
996    }
997  }
998
999  if (strcmp(refineAlgorithm, "GRAB")) {
1000    fprintf(vis_stdout, "\nunknown refinement algorithm: %s\n", 
1001            refineAlgorithm);
1002    goto usage;
1003  }
1004
1005  /* Make sure the flattened network  is available
1006   */
1007  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
1008  if (network == NIL(Ntk_Network_t)) {
1009    fprintf(vis_stdout, "%s\n", error_string());
1010    error_init();
1011    return 1;
1012  }
1013
1014  /* Make sure the AIG graph is available
1015   */
1016  if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) {
1017    fprintf(vis_stderr, 
1018            "** grab error: please run buid_partiton_maigs first\n");
1019    return 1;
1020  }
1021
1022  /* Open the InvFile. (It must contain a single invariant property)
1023   */
1024  if (argc - util_optind == 0) {
1025    (void) fprintf(vis_stderr, 
1026                "** grab error: file containing inv formula not provided\n");
1027    goto usage;
1028  }else if (argc - util_optind > 1) {
1029    (void) fprintf(vis_stderr, "** grab error: too many arguments\n");
1030    goto usage;
1031  }
1032  strcpy(InvFileName, argv[util_optind]);
1033
1034  /* Parsing the InvFile
1035   */
1036  FP = Cmd_FileOpen(InvFileName, "r", NIL(char *), 0);
1037  if (FP == NIL(FILE)) {
1038    (void) fprintf(vis_stdout,  "** grab error: error in opening file %s\n", 
1039                   InvFileName);
1040    return 1;
1041  }
1042  InvariantFormulaArray = Ctlp_FileParseFormulaArray(FP);
1043  fclose(FP);
1044  if (InvariantFormulaArray == NIL(array_t)) {
1045    (void) fprintf(vis_stdout,
1046                   "** grab error: error in parsing formulas from file %s\n",
1047                   InvFileName);
1048    return 1;
1049  }
1050
1051  if (dbgFileName != NIL(char)) 
1052    dbgFile = Cmd_FileOpen(dbgFileName, "r", NIL(char *), 0);
1053  else
1054    dbgFile = NIL(FILE);
1055
1056
1057  /* Set time out processing (if timeOutPeriod is set)
1058   */
1059  if (timeOutPeriod > 0) {
1060    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
1061    (void) alarm(timeOutPeriod);
1062    if (setjmp(timeOutEnv) > 0) {
1063      fprintf(vis_stdout, 
1064           "\n# GRAB: abstract-refine - timeout occurred after %d seconds.\n", 
1065              timeOutPeriod);
1066      (void) fprintf(vis_stdout, "# GRAB: data may be corrupted.\n");
1067      endTime = util_cpu_ctime();
1068      fprintf(vis_stdout, "# GRAB: elapsed time is %5.1f.\n",
1069              (double)(endTime - startTime)/1000.0);
1070      if (verbosity) {
1071        fprintf(vis_stdout, 
1072              "-- total %d image computations and %d preimage computations\n", 
1073                Img_GetNumberOfImageComputation(Img_Forward_c), 
1074                Img_GetNumberOfImageComputation(Img_Backward_c));
1075      }
1076      alarm(0);
1077      return 1;
1078    }
1079  }
1080
1081  /* Check invariants with the abstraction refinement algorithm GRAB
1082   */
1083  Grab_NetworkCheckInvariants(network, 
1084                              InvariantFormulaArray,
1085                              refineAlgorithm,
1086                              fineGrainFlag,
1087                              refineMinFlag,
1088                              useArdcFlag,
1089                              cexType,
1090                              verbosity,
1091                              dbgLevel,
1092                              printInputs,
1093                              dbgFile,
1094                              useMore,
1095                              "GRAB"
1096                              );
1097
1098
1099  /* Total cost
1100   */
1101  if (verbosity >= 2) {
1102    endTime = util_cpu_ctime();
1103    fprintf(vis_stdout, "# GRAB: elapsed time is %5.1f.\n",
1104            (double)(endTime - startTime)/1000.0);
1105    fprintf(vis_stdout, 
1106            "-- total %d image computations and %d preimage computations\n", 
1107            Img_GetNumberOfImageComputation(Img_Forward_c), 
1108            Img_GetNumberOfImageComputation(Img_Backward_c));
1109  }
1110
1111  alarm(0);
1112  return 0;             /* normal exit */
1113
1114
1115  usage:
1116
1117  (void) fprintf(vis_stderr, "usage: _grab_test [-a refine_algorithm] [-c cex_type] [-d dbg_level] [-F finegrain_flag] [-M refmin_flag] [-i] [-m] [-t period] [-v verbosity_level] [-f dbg_out] [-h] <invar_file>\n");
1118  (void) fprintf(vis_stderr, "    -a <refine_algorithm>\n");
1119  (void) fprintf(vis_stderr, "        refine_algorithm = GRAB => the GRAB refinement method (Default)\n");
1120  (void) fprintf(vis_stderr, "    -c <cex_type>\n");
1121  (void) fprintf(vis_stderr, "        cex_type = 0 => minterm state counter-example\n");
1122  (void) fprintf(vis_stderr, "        cex_type = 1 => cube state counter-example\n");
1123  (void) fprintf(vis_stderr, "        cex_type = 2 => synchronous onion rings (Default)\n");
1124  (void) fprintf(vis_stderr, "    -d <dbg_level>\n");
1125  (void) fprintf(vis_stderr, "        debug_level = 0 => no debugging (Default)\n");
1126  (void) fprintf(vis_stderr, "        debug_level = 1 => print path to state failing invariant\n");
1127  (void) fprintf(vis_stderr, "    -F <finegrain_flag>\n");
1128  (void) fprintf(vis_stderr, "        finegrain_flag = 0 => disable fine-grain abstraction\n");
1129  (void) fprintf(vis_stderr, "        finegrain_flag = 1 => enable fine-grain abstraction (Default)\n");
1130  (void) fprintf(vis_stderr, "    -M <refinemin_flag>\n");
1131  (void) fprintf(vis_stderr, "        refinemin_flag = 0 => disable greedy refinement minimization\n");
1132  (void) fprintf(vis_stderr, "        refinemin_flag = 1 => enable greedy refinement minimization (Default)\n");
1133  (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
1134  (void) fprintf(vis_stderr, "    -m  pipe debugger output through UNIX utility more\n");
1135  (void) fprintf(vis_stderr, "    -t <period> Time out period.\n");
1136  (void) fprintf(vis_stderr, "    -v <verbosity_level>\n");
1137  (void) fprintf(vis_stderr, "        verbosity_level = 0 => no feedback (Default)\n");
1138  (void) fprintf(vis_stderr, "        verbosity_level = 1 => code status\n");
1139  (void) fprintf(vis_stderr, "        verbosity_level = 2 => code status and CPU usage profile\n");
1140  (void) fprintf(vis_stderr, "    -f <dbg_out>\n");
1141  (void) fprintf(vis_stderr, "        write error trace to dbg_out\n");
1142  (void) fprintf(vis_stderr, "    <invar_file> The input file containing invariants to be checked.\n");
1143  (void) fprintf(vis_stderr, "   -h\t\t print the command usage\n");
1144
1145  return 1;             /* error exit */
1146}
1147
1148
1149/**Function********************************************************************
1150
1151  Synopsis    [Handle function for timeout.]
1152
1153  Description [This function is called when the process receives a signal of
1154  type alarm. Since alarm is set with elapsed time, this function checks if the
1155  CPU time corresponds to the timeout of the command. If not, it reprograms the
1156  alarm to fire later and check if the CPU limit has been reached.]
1157
1158  SideEffects []
1159
1160******************************************************************************/
1161static void
1162TimeOutHandle(void)
1163{
1164  longjmp(timeOutEnv, 1);
1165} 
Note: See TracBrowser for help on using the repository browser.