source: vis_dev/vis-2.3/src/bmc/bmcCirCUsUtil.c @ 36

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

vis2.3
File size: 35.0 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [bmcCirCUsUtil.c]
4
5  PackageName [bmc]
6
7  Synopsis    [Utilities for bmcCirCUs]
8
9  Author      [Mohammad Awedh]
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 "bmcInt.h"
18#include "sat.h"
19
20static char rcsid[] UNUSED = "$Id: bmcCirCUsUtil.c,v 1.22 2010/04/10 04:07:06 fabio Exp $";
21
22/*---------------------------------------------------------------------------*/
23/* Constant declarations                                                     */
24/*---------------------------------------------------------------------------*/
25
26#define MAX_LENGTH 320 /* Max. length of a string while reading a file */
27
28/*---------------------------------------------------------------------------*/
29/* Type declarations                                                         */
30/*---------------------------------------------------------------------------*/
31
32/*---------------------------------------------------------------------------*/
33/* Structure declarations                                                    */
34/*---------------------------------------------------------------------------*/
35
36/*---------------------------------------------------------------------------*/
37/* Variable declarations                                                     */
38/*---------------------------------------------------------------------------*/
39
40/**AutomaticStart*************************************************************/
41
42/*---------------------------------------------------------------------------*/
43/* Static function prototypes                                                */
44/*---------------------------------------------------------------------------*/
45
46static char * getBddName(bdd_manager *bddManager, bdd_node *node);
47static bAigEdge_t getAigAtTimeFrame(bAig_Manager_t *manager, bAigEdge_t node, int i, int withInitialState);
48static bAigEdge_t getAigOfBddAtState(Ntk_Network_t *network, bdd_node *node, int state, int withInitialState);
49
50/**AutomaticEnd***************************************************************/
51
52/*---------------------------------------------------------------------------*/
53/* Definition of exported functions                                          */
54/*---------------------------------------------------------------------------*/
55
56/*---------------------------------------------------------------------------*/
57/* Definition of internal functions                                          */
58/*---------------------------------------------------------------------------*/
59
60/**Function********************************************************************
61
62 Synopsis [Check for termination for safety properties.]
63
64  Description [Check for termination for safety properties.]
65  SideEffects []
66
67  SeeAlso     []
68
69******************************************************************************/
70void
71BmcCirCUsAutLtlCheckTerminalAutomaton(
72  Ntk_Network_t            *network,
73  bAig_Manager_t           *aigManager,
74  st_table                 *nodeToMvfAigTable,
75  BmcCheckForTermination_t *terminationStatus,
76  st_table                 *coiIndexTable,
77  BmcOption_t              *options)
78{
79  long            startTime, endTime;
80  int             k = terminationStatus->k;
81  int             returnStatus = 0;
82  Ltl_Automaton_t *automaton = terminationStatus->automaton;
83  satInterface_t  *tInterface, *etInterface;
84  bAigEdge_t      autPath, property;
85  array_t         *objArray;
86  array_t         *previousResultArray;
87
88  startTime = util_cpu_ctime();
89
90  if (options->verbosityLevel == BmcVerbosityMax_c) {
91    (void) fprintf(vis_stdout, "\nBMC: Check for termination\n");
92  }
93  etInterface = 0;
94  tInterface  = 0;
95    /*
96    Hold objects
97  */
98  objArray = array_alloc(bAigEdge_t, 2);
99  previousResultArray    = array_alloc(bAigEdge_t, 0);
100  returnStatus = 0;
101
102  autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
103                                                     0, k+1, nodeToMvfAigTable,
104                                                     coiIndexTable,
105                                                     BMC_NO_INITIAL_STATES);
106
107  property = bAig_Not(
108    BmcCirCUsBdd2Aig(network, automaton->fairSets, k, -1,
109                     automaton, aigManager,  BMC_NO_INITIAL_STATES));
110
111  property = bAig_And(aigManager, property,
112                      BmcCirCUsBdd2Aig(network, automaton->fairSets, k+1, -1,
113                                       automaton, aigManager,  BMC_NO_INITIAL_STATES));
114  options->cnfPrefix = k+1;
115  array_insert(bAigEdge_t, objArray, 0, property);
116  array_insert(bAigEdge_t, objArray, 1, autPath);
117  tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
118                                            previousResultArray, options, tInterface);
119  if(tInterface->status == SAT_UNSAT){
120     returnStatus = 1;
121  }
122
123  /* ===========================
124     Early termination condition
125     ===========================
126  */
127  if ((options->earlyTermination)&&(returnStatus ==0)) {
128    if (options->verbosityLevel == BmcVerbosityMax_c) {
129      (void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
130    }
131
132    autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
133                                                       0, k+1, nodeToMvfAigTable,
134                                                       coiIndexTable,
135                                                       BMC_INITIAL_STATES);
136    array_insert(bAigEdge_t, objArray, 0, autPath);
137    array_insert(bAigEdge_t, objArray, 1, bAig_One);
138    options->cnfPrefix = k+1;
139    etInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
140                                               previousResultArray, options, etInterface);
141
142    if(etInterface->status == SAT_UNSAT){
143      (void) fprintf(vis_stdout, "# BMC: by early termination\n");
144      returnStatus = 1;
145    }
146  } /* Early termination */
147
148  if (options->verbosityLevel != BmcVerbosityNone_c) {
149    endTime = util_cpu_ctime();
150    fprintf(vis_stdout, "-- Check for termination time time = %10g\n",
151            (double)(endTime - startTime) / 1000.0);
152  }
153  array_free(objArray);
154  array_free(previousResultArray);
155
156  terminationStatus->action = returnStatus;
157
158} /* BmcCirCUsAutLtlCheckTerminalAutomaton */
159
160
161
162/**Function********************************************************************
163
164  Synopsis [Build AIG for a given function in BDD at a given time period]
165
166  Description [Build AIG for a BDD at a time period. If next != -1, then the
167  passed BDD represents a transition relation.]
168
169  SideEffects []
170
171  SeeAlso     [BmcAutEncodeAutomatonStates BmcAutBuildTransitionRelation]
172
173******************************************************************************/
174bAigEdge_t
175BmcCirCUsBdd2Aig(
176  Ntk_Network_t   *network,
177  bdd_t           *function,
178  int             current,
179  int             next,
180  Ltl_Automaton_t *automaton,
181  bAig_Manager_t  *aigManager,
182  int             withInitialState)
183{
184  bdd_manager *bddManager;
185  bdd_node    *node;
186  bdd_gen     *gen;
187
188  array_t     *cube;
189  int         i, value;
190  int         state = current;
191  bAigEdge_t  aigFunction, andFunction, aigNode;
192
193  if (function == NULL){
194    return bAig_NULL;
195  }
196  /*
197    If BDD represents a constant value
198   */
199  if(bdd_is_tautology(function, 0)){
200    return bAig_Zero;
201  }
202  if(bdd_is_tautology(function, 1)){
203    return bAig_One;
204  }
205
206  bddManager = bdd_get_manager(function);
207  aigFunction = bAig_Zero;
208  foreach_bdd_cube(function, gen, cube){
209    andFunction = bAig_One;
210    arrayForEachItem(int, cube, i, value){
211      if (value != 2){
212        int j;
213        /*
214          If the BDD varaible is a next state varaible, we use the corresponding
215          current state varaible but with next state index.
216        */
217        if (next != -1 && st_lookup_int(automaton->nsPsTable, (char *)(long)i, &j)){
218          node = bdd_bdd_ith_var(bddManager, j);
219          state = next;
220        } else {
221          node = bdd_bdd_ith_var(bddManager, i);
222          state = current;
223        }
224        aigNode = getAigOfBddAtState(network, node, state, withInitialState);
225        if (value == 0){
226          aigNode = bAig_Not(aigNode);
227        }
228        andFunction = bAig_And(aigManager, andFunction, aigNode);
229      }
230    }
231    aigFunction = bAig_Or(aigManager, aigFunction, andFunction);
232  }/* foreach_bdd_cube */
233
234  return aigFunction;
235} /* BmcCirCUsBdd2Aig */
236
237
238/**Function********************************************************************
239
240  Synopsis [Build AIG for a path in the automaton.]
241
242  Description [Build AIG for a path in the automaton starting from "fromState"
243  and ending at "toState". If "initialState" = BMC_INITIAL_STATES, then the
244  path starts from an initial state.]
245
246  SideEffects []
247
248  SeeAlso     []
249
250******************************************************************************/
251bAigEdge_t
252BmcCirCUsAutCreateAigForPath(
253  Ntk_Network_t   *network,
254  bAig_Manager_t  *aigManager,
255  Ltl_Automaton_t *automaton,
256  int             fromState,
257  int             toState,
258  int             initialState)
259{
260  int        k;
261  bAigEdge_t result, aigFunction = bAig_One;
262
263  if(initialState){
264    result = BmcCirCUsBdd2Aig(network, automaton->initialStates, 0, -1,
265                              automaton, aigManager, initialState);
266    aigFunction = result;
267  }
268  for(k=fromState; k<toState; k++){
269   result = BmcCirCUsBdd2Aig(network, automaton->transitionRelation, k, k+1,
270                              automaton, aigManager, initialState);
271    aigFunction = bAig_And(aigManager , aigFunction, result);
272  }
273  return aigFunction;
274
275} /* BmcCirCUsAutCreateAigForPath */
276
277/**Function********************************************************************
278
279  Synopsis [Build AIG for a simple path in the automaton.]
280
281  Description [Build AIG a simple path in the automaton starting from
282  "fromState" and ending at "toState". If "initialState" =
283  BMC_INITIAL_STATES, the the path starts from an initial state.]
284
285  SideEffects []
286
287  SeeAlso     []
288
289******************************************************************************/
290bAigEdge_t
291BmcCirCUsAutCreateAigForSimplePath(
292  Ntk_Network_t   *network,
293  bAig_Manager_t  *aigManager,
294  Ltl_Automaton_t *automaton,
295  int             fromState,
296  int             toState,
297  int             initialState)
298{
299  int        i, j, bddID;
300  bAigEdge_t result, aigFunction, next, current;
301  mdd_manager        *bddManager = Ntk_NetworkReadMddManager(network);
302  st_generator       *stGen;
303
304  bdd_node           *node;
305
306
307
308  aigFunction = BmcCirCUsAutCreateAigForPath(network, aigManager, automaton,
309                                             fromState, toState, initialState);
310  /*
311    The path is simple path
312  */
313  for(i = fromState + 1; i <= toState; i++){
314    for(j=fromState; j < i; j++){
315      result = bAig_Zero;
316      st_foreach_item(automaton->psNsTable, stGen,&bddID, NULL) {
317        node = bdd_bdd_ith_var(bddManager, bddID);
318
319        current = getAigOfBddAtState(network, node, i, initialState);
320        next    = getAigOfBddAtState(network, node, j, initialState);
321
322        result = bAig_Or(aigManager, result,
323                         bAig_Not(bAig_Eq(aigManager, current, next)));
324      }
325      aigFunction = bAig_And(aigManager, aigFunction, result);
326    }
327  }
328
329  return aigFunction;
330
331} /* BmcCirCUsAutCreateAigForSimplePath */
332
333/**Function********************************************************************
334
335  Synopsis [Build AIG for a simple path in the composite model]
336
337  Description [Build AIG a simple path in the composite mode starting from
338  "fromState" and ending at "toState". If "initialState" = BMC_INITIAL_STATES,
339  the the path starts from an initial state.]
340
341  SideEffects []
342
343  SeeAlso     []
344
345******************************************************************************/
346bAigEdge_t
347BmcCirCUsCreateAigForSimpleCompositePath(
348  Ntk_Network_t   *network,
349  bAig_Manager_t  *aigManager,
350  Ltl_Automaton_t *automaton,
351  int             fromState,
352  int             toState,
353  st_table        *nodeToMvfAigTable,
354  st_table        *coiIndexTable,
355  int             initialState)
356{
357  int        i, j, bddID;
358  bAigEdge_t         result, aigFunction, next, current;
359  mdd_manager        *bddManager = Ntk_NetworkReadMddManager(network);
360  st_generator       *stGen;
361
362  bdd_node           *node;
363
364
365
366  /*
367    Build a path in the original model
368   */
369  bAig_ExpandTimeFrame(network, aigManager, toState+1, initialState);
370  /*
371    Build a path in the automaton
372   */
373  aigFunction = BmcCirCUsAutCreateAigForPath(network, aigManager, automaton,
374                                             fromState, toState, initialState);
375  /*
376    Constrains the two paths to be simple paths
377  */
378  for(i = fromState + 1; i <= toState; i++){
379    for(j=fromState; j < i; j++){
380      result = bAig_Zero;
381
382      /*
383        Unique states in the automaton
384       */
385      st_foreach_item(automaton->psNsTable, stGen, &bddID, NULL) {
386        node = bdd_bdd_ith_var(bddManager, bddID);
387
388        current = BmcCirCUsBdd2Aig(network, bdd_construct_bdd_t(bddManager, node), i, -1,
389                                   automaton, aigManager,
390                                   initialState);
391        next    = BmcCirCUsBdd2Aig(network, bdd_construct_bdd_t(bddManager,node), j, -1,
392                                   automaton, aigManager,
393                                   initialState);
394        /*
395          next    = BmcCirCUsBdd2Aig(network, bdd_construct_bdd_t(bddManager,node), i, j,
396                                   automaton, aigManager,
397                                   initialState);
398
399          result = bAig_Or(aigManager, result,
400                                   bAig_Not(next));
401        */
402        result = bAig_Or(aigManager, result,
403                         bAig_Not(bAig_Eq(aigManager, current, next)));
404      }
405      /*
406        Unique states in the original model
407      */
408      result = bAig_Or(aigManager, result,
409                       bAig_Not(BmcCirCUsConnectFromStateToState(network, i-1, j,
410                                                                 nodeToMvfAigTable,
411                                                                 coiIndexTable,
412                                                                 initialState)));
413      aigFunction = bAig_And(aigManager, aigFunction, result);
414    }
415  }
416
417  return aigFunction;
418
419} /* BmcCirCUsCreateAigForSimpleCompositePath */
420
421
422
423/**Function********************************************************************
424
425 Synopsis [Verify the general LTL formula passes by applying the
426   termination criteria that are described in the paper "Proving More
427   Properties with Bounded Model Checking"]
428
429  Description [Check for the termination on the composition of the
430  automaton that describes the negation of the LTL formula and the
431  model.  We apply the termination criteria as described in the paper
432  "Proving More Properties with Bounded Model Checking".]
433
434  Return value:
435         0 no action
436         1 (m+n-1) <= options->maxK.  If no counterexample of length up to (m+n-1),
437                                      the property passes
438         2 (m+n-1) >  options->maxK   The property is undecided if no counterexample
439                                      of length <= options->maxK.
440         3 Pass by early termination
441
442  SideEffects []
443
444  SeeAlso     []
445
446******************************************************************************/
447void
448BmcCirCUsAutLtlCheckForTermination(
449  Ntk_Network_t            *network,
450  bAig_Manager_t           *aigManager,
451  st_table                 *nodeToMvfAigTable,
452  BmcCheckForTermination_t *terminationStatus,
453  st_table                 *coiIndexTable,
454  BmcOption_t              *options)
455{
456  long            startTime, endTime;
457  int             k = terminationStatus->k;
458  int             returnStatus = 0;
459  Ltl_Automaton_t *automaton = terminationStatus->automaton;
460  Ctlsp_Formula_t *externalConstraints = terminationStatus->externalConstraints;
461  satInterface_t  *tInterface, *etInterface;
462  bAigEdge_t      autPath, property, tmp;
463  array_t         *objArray;
464  array_t         *previousResultArray;
465  array_t         *previousResultArrayWOI;
466
467  /*
468    If checkLevel == 0 -->  check for beta' and beta'' only and if either UNSAT, m=k and chekLevel =1
469    If checkLevel == 1 -->  check for beta  only and if UNSAT, checkLevel = 2.
470    If checkLevel == 2 -->  check for alpha only and if UNSAT, n=k and checkLevel = 3.
471    If gama is UNSAT up to (m+n-1) and checkLvel = 3, formula passes.
472    checkLevel = 4 if (m+n-1) > maxK;
473   */
474  startTime = util_cpu_ctime();
475
476  etInterface = 0;
477  tInterface  = 0;
478    /*
479    Hold objects
480  */
481  objArray = array_alloc(bAigEdge_t, 2);
482
483  previousResultArray    = array_alloc(bAigEdge_t, 0);
484  previousResultArrayWOI = array_alloc(bAigEdge_t, 0);
485
486  /* ===========================
487     Early termination condition
488     ===========================
489  */
490  if (options->earlyTermination) {
491    if (options->verbosityLevel == BmcVerbosityMax_c) {
492      (void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
493    }
494
495    autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
496                                                       0, k, nodeToMvfAigTable,
497                                                       coiIndexTable,
498                                                       BMC_INITIAL_STATES);
499    array_insert(bAigEdge_t, objArray, 0, autPath);
500    array_insert(bAigEdge_t, objArray, 1, bAig_One);
501    options->cnfPrefix = k;
502    etInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
503                                     previousResultArray, options, etInterface);
504
505    if(etInterface->status == SAT_UNSAT){
506      (void) fprintf(vis_stdout, "# BMC: by early termination\n");
507      terminationStatus->action = 3;
508      return;
509    }
510  } /* Early termination */
511  if((!automaton->fairSets) &&
512     (terminationStatus->checkLevel == 0)) {
513    /*
514      All the automaton states are fair states. So, beta' and beta are always UNSAT.
515    */
516    terminationStatus->m = 0;
517    printf("Value of m = %d\n", terminationStatus->m);
518    terminationStatus->checkLevel = 2;
519  }
520
521   /*
522    Check \beta''(k)
523  */
524  if(terminationStatus->checkLevel == 0){
525    int i;
526
527    if (options->verbosityLevel == BmcVerbosityMax_c) {
528      (void) fprintf(vis_stdout, "# BMC: Check Beta''\n");
529    }
530    autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
531                                                       0, k+1, nodeToMvfAigTable,
532                                                       coiIndexTable, BMC_NO_INITIAL_STATES);
533    property = bAig_One;
534    for(i=1; i<=k+1; i++){
535      tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, i, -1,
536                             automaton, aigManager,
537                             BMC_NO_INITIAL_STATES);
538
539      if(externalConstraints){
540        tmp = bAig_Or(aigManager, tmp,
541                      BmcCirCUsCreatebAigOfPropFormula(network, aigManager, i,
542                                                       externalConstraints,
543                                                       BMC_NO_INITIAL_STATES));
544      }
545      property = bAig_And(aigManager, property, bAig_Not(tmp));
546    }
547
548    tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, 0, -1,
549                           automaton, aigManager,  BMC_NO_INITIAL_STATES);
550    if(externalConstraints){
551      tmp = bAig_Or(aigManager, tmp,
552                    BmcCirCUsCreatebAigOfPropFormula(network, aigManager, 0,
553                                                     externalConstraints,
554                                                     BMC_NO_INITIAL_STATES));
555    }
556    property = bAig_And(aigManager, property, tmp);
557
558    options->cnfPrefix = k+1;
559    array_insert(bAigEdge_t, objArray, 0, property);
560    array_insert(bAigEdge_t, objArray, 1, autPath);
561    tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
562                                    previousResultArray, options, tInterface);
563    if(tInterface->status == SAT_UNSAT){
564      terminationStatus->m = k;
565      (void)fprintf(vis_stderr,"m = %d\n", terminationStatus->m);
566      terminationStatus->checkLevel = 1;
567    }
568  } /* Check for Beta'' */
569
570  /*
571    Check \beta'(k)
572  */
573  if(terminationStatus->checkLevel == 0){
574    int i;
575
576    if (options->verbosityLevel == BmcVerbosityMax_c) {
577      (void) fprintf(vis_stdout, "# BMC: Check Beta'\n");
578    }
579    autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
580                                                       0, k+1, nodeToMvfAigTable,
581                                                       coiIndexTable, BMC_NO_INITIAL_STATES);
582    property = bAig_One;
583    for(i=0; i<=k; i++){
584      tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, i, -1,
585                             automaton, aigManager,
586                             BMC_NO_INITIAL_STATES);
587      if(externalConstraints){
588        tmp = bAig_Or(aigManager, tmp,
589                      BmcCirCUsCreatebAigOfPropFormula(network, aigManager, i,
590                                                       externalConstraints,
591                                                       BMC_NO_INITIAL_STATES));
592      }
593      property = bAig_And(aigManager, property, bAig_Not(tmp));
594    }
595    tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, k+1, -1,
596                           automaton, aigManager,
597                           BMC_NO_INITIAL_STATES);
598    if(externalConstraints){
599      tmp = bAig_Or(aigManager, tmp,
600                    BmcCirCUsCreatebAigOfPropFormula(network, aigManager, k+1,
601                                                     externalConstraints,
602                                                     BMC_NO_INITIAL_STATES));
603    }
604    property = bAig_And(aigManager, property, tmp);
605
606    options->cnfPrefix = k+1;
607    array_insert(bAigEdge_t, objArray, 0, property);
608    array_insert(bAigEdge_t, objArray, 1, autPath);
609    tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
610                                    previousResultArray, options, tInterface);
611    if(tInterface->status == SAT_UNSAT){
612      terminationStatus->m = k;
613      (void)fprintf(vis_stderr,"m = %d\n", terminationStatus->m);
614      terminationStatus->checkLevel = 1;
615    }
616  } /* Check for Beta' */
617
618  /*
619    Check for Beta.
620  */
621  if(terminationStatus->checkLevel == 1){
622
623    if (options->verbosityLevel == BmcVerbosityMax_c) {
624      (void) fprintf(vis_stdout, "# BMC: Check Beta\n");
625    }
626    autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
627                                                       0, k+1, nodeToMvfAigTable,
628                                                       coiIndexTable, BMC_NO_INITIAL_STATES);
629    property = bAig_One;
630
631    tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, k, -1,
632                           automaton, aigManager,  BMC_NO_INITIAL_STATES);
633
634    if(externalConstraints){
635      tmp = bAig_Or(aigManager, tmp,
636                    BmcCirCUsCreatebAigOfPropFormula(network, aigManager, k,
637                                                     externalConstraints,
638                                                     BMC_NO_INITIAL_STATES));
639    }
640    property = bAig_And(aigManager, property, bAig_Not(tmp));
641
642    tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, k+1, -1,
643                           automaton, aigManager,  BMC_NO_INITIAL_STATES);
644    if(externalConstraints){
645      tmp = bAig_Or(aigManager, tmp,
646                    BmcCirCUsCreatebAigOfPropFormula(network, aigManager, k+1,
647                                                     externalConstraints,
648                                                     BMC_NO_INITIAL_STATES));
649    }
650    property = bAig_And(aigManager, property, tmp);
651
652    options->cnfPrefix = k+1;
653    array_insert(bAigEdge_t, objArray, 0, property);
654    array_insert(bAigEdge_t, objArray, 1, autPath);
655    tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
656                                    previousResultArray, options, tInterface);
657    if(tInterface->status == SAT_UNSAT){
658      terminationStatus->checkLevel = 2;
659    }
660  } /* Check Beta*/
661
662  if(terminationStatus->checkLevel == 2){ /* we check Alpha if Beta is unsatisfiable */
663
664    if (options->verbosityLevel == BmcVerbosityMax_c) {
665      (void) fprintf(vis_stdout, "# BMC: Check Alpha \n");
666    }
667    autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
668                                                       0, k, nodeToMvfAigTable,
669                                                       coiIndexTable,
670                                                       BMC_INITIAL_STATES);
671    array_insert(bAigEdge_t, objArray, 1, bAig_One);
672    property = bAig_Zero;
673    if(automaton->fairSets){
674      property =  BmcCirCUsBdd2Aig(network, automaton->fairSets, k, -1,
675                                   automaton, aigManager,  BMC_INITIAL_STATES);
676      array_insert(bAigEdge_t, objArray, 1, property);
677    }
678    if(externalConstraints){
679      property = bAig_Or(aigManager, property,
680                         BmcCirCUsCreatebAigOfPropFormula(network, aigManager, k,
681                                                          externalConstraints,
682                                                          BMC_INITIAL_STATES));
683      array_insert(bAigEdge_t, objArray, 1, property);
684    }
685    options->cnfPrefix = k;
686    array_insert(bAigEdge_t, objArray, 0, autPath);
687    tInterface = 0;
688    tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network,
689                                              objArray, previousResultArray,
690                                              options, tInterface);
691    if(tInterface->status == SAT_UNSAT){
692      terminationStatus->n = k;
693      terminationStatus->checkLevel = 3;
694      (void)fprintf(vis_stdout,"Value of m=%d  n=%d\n",terminationStatus->m,terminationStatus->n);
695      if ((terminationStatus->m+terminationStatus->n-1) <= options->maxK){
696        terminationStatus->k = terminationStatus->m+terminationStatus->n-1;
697        if(k==0){
698          /*
699            By induction, the property passes.
700           */
701          terminationStatus->k = 0;
702        }
703        returnStatus = 1;
704      } else {
705        terminationStatus->checkLevel = 4;
706        returnStatus = 2;
707      }
708    }
709  }/* Chek for Alpha */
710
711  if (options->verbosityLevel != BmcVerbosityNone_c) {
712    endTime = util_cpu_ctime();
713    fprintf(vis_stdout, "-- Check for termination time time = %10g\n",
714            (double)(endTime - startTime) / 1000.0);
715  }
716
717  terminationStatus->action = returnStatus;
718
719} /* BmcAutLtlCheckForTermination */
720
721
722/**Function********************************************************************
723
724  Synopsis [Call CirCUs SAT solver on a CNF file]
725
726  Description [Call CirCUs SAT solver on a CNF file. We use CirCUs as
727  CNF SAT solver.  The function returns a file name that contains the
728  assignment if the set of clauses are satisfiable.
729  ]
730
731  SideEffects []
732
733******************************************************************************/
734char *
735BmcCirCUsCallCirCUs(
736  BmcOption_t *options)
737{
738  satOption_t  *satOption;
739  satManager_t *cm;
740  int          maxSize;
741  char         *fileName = NIL(char);
742
743  satOption          = sat_InitOption();
744  satOption->verbose = options->verbosityLevel-1;
745
746  cm = sat_InitManager(0);
747  cm->comment = ALLOC(char, 2);
748  cm->comment[0] = ' ';
749  cm->comment[1] = '\0';
750  cm->stdOut = stdout;
751  cm->stdErr = stderr;
752
753  cm->option = satOption;
754  cm->each = sat_InitStatistics();
755
756  cm->unitLits = sat_ArrayAlloc(16);
757  cm->pureLits = sat_ArrayAlloc(16);
758
759  maxSize = 10000 << 8;
760  cm->nodesArray = ALLOC(bAigEdge_t, maxSize);
761  cm->maxNodesArraySize = maxSize;
762  cm->nodesArraySize = satNodeSize;
763
764  sat_AllocLiteralsDB(cm);
765
766  sat_ReadCNF(cm, options->satInFile);
767
768  if (options->verbosityLevel == BmcVerbosityMax_c) {
769    (void)fprintf(vis_stdout,"Calling SAT solver (CirCUs) ...");
770    (void) fflush(vis_stdout);
771  }
772  sat_Main(cm);
773  if (options->verbosityLevel == BmcVerbosityMax_c) {
774    (void) fprintf(vis_stdout," done ");
775    (void) fprintf(vis_stdout, "(%g s)\n", cm->each->satTime);
776  }
777  if(cm->status == SAT_UNSAT) {
778    if (options->verbosityLevel != BmcVerbosityNone_c){
779      (void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
780
781    }
782    fflush(cm->stdOut);
783  } else if(cm->status == SAT_SAT) {
784    if (options->verbosityLevel != BmcVerbosityNone_c){
785      (void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
786    }
787    if (options->verbosityLevel > BmcVerbosityMax_c){
788      sat_ReportStatistics(cm, cm->each);
789    }
790
791    if(!(cm->stdOut = fopen(options->satOutFile, "w"))) {
792      fprintf(stdout, "ERROR : Can't open file %s\n", options->satOutFile);
793      cm->stdOut = stdout;
794      cm->stdErr = stderr;
795    }
796    sat_PrintSatisfyingAssignment(cm);
797    fileName = options->satOutFile;
798  }
799  sat_FreeManager(cm);
800
801  return fileName;
802} /* BmcCallCirCUs */
803
804/**Function********************************************************************
805
806  Synopsis [Check the satisfiability of CNF formula written in file]
807
808  Description [Run external solver on a CNF file. The function returns
809  a file name that contains the assignment if the set of clauses are
810  satisfiable.]
811
812  SideEffects []
813
814******************************************************************************/
815char *
816BmcCirCUsCallCusp(BmcOption_t *options)
817{
818  FILE        *fp;
819  static char parseBuffer[1024];
820  int         satStatus;
821  char        line[MAX_LENGTH];
822  int         num = 0;
823  array_t     *result = NIL(array_t);
824  char        *tmpStr, *tmpStr1, *tmpStr2;
825  long        solverStart;
826  int         satTimeOutPeriod = 0;
827  char        *fileName = NIL(char);
828
829  /*
830    Prepare to call external CNF SAT solver
831   */
832  strcpy(parseBuffer,"cusp -distill -velim -cnf ");
833  options->satSolverError = FALSE;  /* assume no error */
834  if (options->timeOutPeriod > 0) {
835    /* Compute the residual CPU time and subtract a little time to
836       give vis a chance to clean up before its own time out expires.
837    */
838    satTimeOutPeriod = options->timeOutPeriod - 1 -
839      (util_cpu_ctime() - options->startTime) / 1000;
840    if (satTimeOutPeriod <= 0){ /* no time left to run SAT solver */
841      options->satSolverError=TRUE;
842      return NIL(char);
843    }
844    tmpStr2 = util_inttostr(satTimeOutPeriod);
845    tmpStr1 = util_strcat3(options->satInFile," -t ", tmpStr2);
846    tmpStr = util_strcat3(tmpStr1, " >", options->satOutFile);
847    FREE(tmpStr1);
848    FREE(tmpStr2);
849  } else {
850    tmpStr = util_strcat3(options->satInFile, " >", options->satOutFile);
851  }
852  strcat(parseBuffer, tmpStr);
853  FREE(tmpStr);
854
855  if (options->verbosityLevel == BmcVerbosityMax_c) {
856    (void)fprintf(vis_stdout,"Calling SAT solver (cusp) ...");
857    (void) fflush(vis_stdout);
858    solverStart = util_cpu_ctime();
859  } else { /* to remove uninitialized variables warning */
860    solverStart = 0;
861  }
862  /* Call Sat Solver */
863  satStatus = system(parseBuffer);
864  if (satStatus != 0){
865    (void) fprintf(vis_stderr, "Can't run external sat solver.  It may not be in your path.  Status = %d\n", satStatus);
866    options->satSolverError = TRUE;
867    return NIL(char);
868  }
869
870  if (options->verbosityLevel == BmcVerbosityMax_c) {
871    (void) fprintf(vis_stdout," done ");
872    (void) fprintf(vis_stdout, "(%g s)\n",
873                   (double) (util_cpu_ctime() - solverStart)/1000.0);
874  }
875  fp = Cmd_FileOpen(options->satOutFile, "r", NIL(char *), 0);
876  if (fp == NIL(FILE)) {
877    (void) fprintf(vis_stderr, "** bmc error: Cannot open the file %s\n",
878                   options->satOutFile);
879    options->satSolverError = TRUE;
880    return NIL(char);
881  }
882  /* Skip the lines until the result */
883  while(1) {
884    if (fgets(line, MAX_LENGTH - 1, fp) == NULL) break;
885    if(strstr(line,"UNSATISFIABLE") ||
886       strstr(line,"SATISFIABLE") ||
887       strstr(line,"MEMOUT") ||
888       strstr(line,"TIMEOUT"))
889      break;
890  }
891
892  if(strstr(line,"UNSATISFIABLE") != NIL(char)) {
893    if (options->verbosityLevel != BmcVerbosityNone_c){
894      (void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
895
896    }
897  } else if(strstr(line,"SATISFIABLE") != NIL(char)) {
898    if (options->verbosityLevel != BmcVerbosityNone_c){
899      (void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
900    }
901    /* Skip the initial v of the result line */
902    result = array_alloc(int, 0);
903    while (fgets(line, MAX_LENGTH - 1, fp) != NULL) {
904      char *word;
905      if (line[0] != 'v') {
906        (void) fprintf(vis_stderr,
907                       "** bmc error: Cannot find assignment in file %s\n",
908                       options->satOutFile);
909        options->satSolverError = TRUE;
910        return NIL(char);
911      }
912      word = strtok(&(line[1])," \n");
913      while (word != NIL(char)) {
914        num = atoi(word);
915        if (num == 0) break;
916        array_insert_last(int, result, num);
917        word = strtok(NIL(char)," \n");
918      }
919      if (num == 0) break;
920    }
921    (void) fclose(fp);
922    fp = Cmd_FileOpen(options->satOutFile, "w", NIL(char *), 0);
923    for(num=0; num < array_n(result); num++){
924      fprintf(fp,"%d ", array_fetch(int, result, num));
925      if(((num+1) %10) == 0){
926        fprintf(fp,"\n");
927      }
928    }
929    array_free(result);
930    (void) fclose(fp);
931    fileName = options->satOutFile;
932  } else if(strstr(line,"MEMOUT") != NIL(char)) {
933    (void) fprintf(vis_stdout,"# SAT: SAT Solver Memory out\n");
934    options->satSolverError = TRUE;
935  } else if(strstr(line,"TIMEOUT") != NIL(char)) {
936    (void) fprintf(vis_stdout,
937                   "# SAT: SAT Solver Time out occurred after %d seconds.\n",
938                   satTimeOutPeriod);
939    options->satSolverError = TRUE;
940  } else {
941    (void) fprintf(vis_stdout, "# SAT: SAT Solver failed, try again\n");
942    options->satSolverError = TRUE;
943  }
944  (void) fflush(vis_stdout);
945
946  return fileName;
947} /* BmcCirCUsCallCusp */
948
949
950/*---------------------------------------------------------------------------*/
951/* Definition of static functions                                            */
952/*---------------------------------------------------------------------------*/
953
954/**Function********************************************************************
955
956  Synopsis [retun the name of bdd node]
957
958  Description [return the name of bdd node. If the bdd is for a
959  multi-valued variable, then its name will be the name of the
960  multi-valued variable concatenated with its index. It is the user
961  responsibility to free the returned name]
962
963  SideEffects []
964
965******************************************************************************/
966static char *
967getBddName(
968  bdd_manager *bddManager,
969  bdd_node *node)
970{
971  array_t   *mvar_list  = mdd_ret_mvar_list(bddManager);
972  array_t   *bvar_list  = mdd_ret_bvar_list(bddManager);
973  char      name[100];
974  bvar_type bv;
975  mvar_type mv;
976  int       nodeIndex = bdd_node_read_index(node);
977  int       index, rtnNodeIndex;
978
979  /*
980    If the node is for a multi-valued varaible.
981  */
982  if (nodeIndex < array_n(bvar_list)){
983    bv = array_fetch(bvar_type, bvar_list, nodeIndex);
984    /*
985      get the multi-valued varaible.
986    */
987    mv = array_fetch(mvar_type, mvar_list, bv.mvar_id);
988    arrayForEachItem(int, mv.bvars, index, rtnNodeIndex) {
989      if (nodeIndex == rtnNodeIndex){
990        break;
991      }
992    }
993    assert(index < mv.encode_length);
994    sprintf(name, "%s_%d", mv.name, index);
995  } else {
996    sprintf(name, "Bdd_%d", nodeIndex);
997  }
998  return util_strsav(name);
999}
1000
1001/**Function********************************************************************
1002
1003  Synopsis []
1004
1005  Description []
1006
1007  SideEffects []
1008
1009******************************************************************************/
1010static bAigEdge_t
1011getAigAtTimeFrame(
1012  bAig_Manager_t *manager,
1013  bAigEdge_t node,
1014  int        i,
1015  int withInitialState)
1016{
1017  bAigTimeFrame_t *timeframe;
1018  bAigEdge_t     result, *li;
1019  int            index;
1020
1021  result = bAig_NULL;
1022
1023  if(withInitialState) timeframe = manager->timeframe;
1024  else                 timeframe = manager->timeframeWOI;
1025
1026  if(st_lookup_int(timeframe->li2index, (char *)node, &index)) {
1027    li = timeframe->latchInputs[i];
1028    result = bAig_GetCanonical(manager, li[index]);
1029  }
1030  else if(st_lookup_int(timeframe->o2index, (char *)node, &index)) {
1031    li = timeframe->outputs[i];
1032    result = bAig_GetCanonical(manager, li[index]);
1033  }
1034  else if(st_lookup_int(timeframe->i2index, (char *)node, &index)) {
1035    li = timeframe->internals[i];
1036    result = bAig_GetCanonical(manager, li[index]);
1037  }
1038  else if(st_lookup_int(timeframe->bli2index, (char *)node, &index)) {
1039    li = timeframe->blatchInputs[i];
1040    result = bAig_GetCanonical(manager, li[index]);
1041  }
1042  else if(st_lookup_int(timeframe->bpi2index, (char *)node, &index)) {
1043    li = timeframe->binputs[i];
1044    result = bAig_GetCanonical(manager, li[index]);
1045  }
1046  return result;
1047}
1048
1049/**Function********************************************************************
1050
1051  Synopsis [Get the AIG node corresponding to a BDD node at a given state]
1052
1053  Description [We use BDD name to get the corresponding AIG node.  If no AIG node
1054  exists, we create one]
1055
1056  SideEffects []
1057
1058  SeeAlso     []
1059
1060******************************************************************************/
1061static bAigEdge_t
1062getAigOfBddAtState(
1063  Ntk_Network_t   *network,
1064  bdd_node        *node,
1065  int             state,
1066  int             withInitialState)
1067{
1068  mdd_manager      *bddManager = Ntk_NetworkReadMddManager(network);
1069  mAig_Manager_t   *aigManager = Ntk_NetworkReadMAigManager(network);
1070
1071  char        *nodeName, *nameKey;
1072  char        tmpName[100];
1073  bAigEdge_t  aigNode, rtnAig;
1074
1075  nodeName = getBddName(bddManager, bdd_regular(node));
1076  aigNode  = bAig_FindNodeByName(aigManager, nodeName);
1077  if(aigNode == bAig_NULL){
1078    sprintf(tmpName, "%s_%d_%d", nodeName, withInitialState, state);
1079    nameKey = util_strsav(tmpName);
1080    aigNode  = bAig_FindNodeByName(aigManager, nameKey);
1081    if(aigNode == bAig_NULL){
1082      aigNode = bAig_CreateVarNode(aigManager, nameKey);
1083    } else {
1084      FREE(nameKey);
1085    }
1086    rtnAig = aigNode;
1087  } else {
1088    aigNode = bAig_GetCanonical(aigManager, aigNode);
1089    rtnAig  = getAigAtTimeFrame(aigManager, aigNode, state, withInitialState);
1090    if(rtnAig == bAig_NULL){
1091      rtnAig = bAig_CreateNode(aigManager, bAig_NULL, bAig_NULL);
1092    }
1093  }
1094  return bAig_GetCanonical(aigManager, rtnAig);
1095} /* getAigOfBddAtState */
Note: See TracBrowser for help on using the repository browser.