source: vis_dev/vis-2.3/src/bmc/bmcBmc.c @ 58

Last change on this file since 58 was 38, checked in by cecile, 14 years ago

first attempt debug with ltl formula
File size: 91.8 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [bmcBmc.c]
4
5  PackageName [bmc]
6
7  Synopsis    [SAT-based ltl model checker.]
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
19static char rcsid[] UNUSED = "$Id: bmcBmc.c,v 1.72 2005/10/14 04:41:11 awedh Exp $";
20
21/*---------------------------------------------------------------------------*/
22/* Constant declarations                                                     */
23/*---------------------------------------------------------------------------*/
24
25/*---------------------------------------------------------------------------*/
26/* Type declarations                                                         */
27/*---------------------------------------------------------------------------*/
28
29/*---------------------------------------------------------------------------*/
30/* Structure declarations                                                    */
31/*---------------------------------------------------------------------------*/
32
33/*---------------------------------------------------------------------------*/
34/* Variable declarations                                                     */
35/*---------------------------------------------------------------------------*/
36
37/**AutomaticStart*************************************************************/
38
39/*---------------------------------------------------------------------------*/
40/* Static function prototypes                                                */
41/*---------------------------------------------------------------------------*/
42
43static int checkIndex(int index, BmcCnfClauses_t *cnfClauses);
44static int doAnd(int left, int right);
45static int doOr(int left, int right);
46
47/**AutomaticEnd***************************************************************/
48
49/*---------------------------------------------------------------------------*/
50/* Definition of exported functions                                          */
51/*---------------------------------------------------------------------------*/
52
53/*---------------------------------------------------------------------------*/
54/* Definition of internal functions                                          */
55/*---------------------------------------------------------------------------*/
56
57/**Function********************************************************************
58
59   Synopsis [Apply Bounded Model Checking (BMC) on a propositional formula.]
60
61   Description [If the property dos not hold in any initial state, the
62   property holds.
63
64   Note: Before calling this function, the LTL formula must be negated.
65   
66   ]
67
68   SideEffects []
69   
70   SeeAlso     []
71   
72******************************************************************************/
73void
74BmcLtlVerifyProp(
75   Ntk_Network_t   *network,
76   Ctlsp_Formula_t *ltlFormula,
77   st_table        *CoiTable,
78   BmcOption_t     *options)
79{
80  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
81  st_table          *nodeToMvfAigTable = NIL(st_table);  /* maps each node to its mvfAig */
82  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
83 
84
85  FILE              *cnfFile;
86
87  array_t           *result = NIL(array_t);
88  long              startTime, endTime;
89  bAigEdge_t        property;
90  array_t           *unitClause;
91 
92  assert(Ctlsp_isPropositionalFormula(ltlFormula));
93 
94  startTime = util_cpu_ctime();
95 
96  if (options->verbosityLevel != BmcVerbosityNone_c){
97    (void) fprintf(vis_stdout, "LTL formula is propositional\n");
98  }
99  property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula);
100 
101  if (property == mAig_NULL){
102    return;
103  }
104  if (property == bAig_One){
105    (void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
106    (void) fprintf(vis_stdout,"# BMC: formula failed\n");
107    if (options->verbosityLevel != BmcVerbosityNone_c){
108      fprintf(vis_stdout, "-- bmc time = %10g\n",
109              (double)(util_cpu_ctime() - startTime) / 1000.0);
110    }
111    return;
112  } else if (property == bAig_Zero){
113    (void) fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
114    (void) fprintf(vis_stdout,"# BMC: formula passed\n");
115    if (options->verbosityLevel != BmcVerbosityNone_c){
116      fprintf(vis_stdout, "-- bmc time = %10g\n",
117              (double)(util_cpu_ctime() - startTime) / 1000.0);
118    }
119    return;
120  }
121  cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);   
122  if (cnfFile == NIL(FILE)) {
123    (void) fprintf(vis_stderr,
124                   "** bmc error: Cannot create CNF output file %s\n",
125                   options->satInFile);
126    return;
127  }
128  /* nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph */
129  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network,
130                                                           MVFAIG_NETWORK_APPL_KEY);
131  assert(nodeToMvfAigTable != NIL(st_table));
132  /*
133    Create clauses database
134  */
135  cnfClauses = BmcCnfClausesAlloc();
136  unitClause = array_alloc(int, 1);
137
138  /*
139    Create an initialized path of length 0
140   */
141  BmcCnfGenerateClausesForPath(network, 0, 0, BMC_INITIAL_STATES, cnfClauses, nodeToMvfAigTable, CoiTable);
142   
143  /* Generate CNF for the property */
144  array_insert(int, unitClause, 0,
145               BmcGenerateCnfFormulaForAigFunction(manager, property, 0, cnfClauses));
146 
147  BmcCnfInsertClause(cnfClauses, unitClause);
148  BmcWriteClauses(manager, cnfFile, cnfClauses, options);
149  (void) fclose(cnfFile);
150
151  result = BmcCheckSAT(options);
152  if (options->satSolverError){
153    (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
154  } else {
155    if (result != NIL(array_t)){
156      (void) fprintf(vis_stdout, "# BMC: formula failed\n");
157      if(options->verbosityLevel != BmcVerbosityNone_c){
158        (void) fprintf(vis_stdout,
159                       "# BMC: Found a counterexample of length = 0 \n");
160      }
161      if (options->dbgLevel == 1) {
162        BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
163                               result, 0, CoiTable, options, NIL(array_t));
164      }
165      array_free(result);
166    } else {
167      if(options->verbosityLevel != BmcVerbosityNone_c){
168        fprintf(vis_stdout,"# BMC: no counterexample found of length up to 0\n");
169      }
170      (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
171    }
172  }
173  array_free(unitClause);   
174  BmcCnfClausesFree(cnfClauses);
175 
176  if (options->verbosityLevel != BmcVerbosityNone_c){
177    endTime = util_cpu_ctime();
178    fprintf(vis_stdout, "-- bmc time = %10g\n",
179            (double)(endTime - startTime) / 1000.0);
180  }
181  fflush(vis_stdout);
182  return;
183} /* BmcLtlVerifyProp  */
184
185
186/**Function********************************************************************
187
188  Synopsis [Check if the LTL formula in the form G(p) (invariant),
189  where p is a propositional formula, is an Inductive Invariant]
190
191  Description [Check if the LTL formula in the form G(p), where p is a
192  propositional formula, is an Inductive Invariant
193
194  An LTL formula G(p), where p is a propositional formul, is an
195  inductive invariant if the following two conditions hold:
196 
197     1- p holds in all the intial states.
198     2- If p holds in a state s, then it also holds in all states
199        that are reachable from s.
200
201  G(p) is an inductive invariant if :
202    SAT( I(0) and !p(0)) return UNSAT and
203    SAT( p(i) and T(i, i+1) and !p(i+1)) returns UNSAT.
204
205  Return value:
206    0 if the property is not an inductive invariant
207    1 if the property is an inductive invariant
208   -1 error
209   ]
210
211  SideEffects []
212
213  SeeAlso     []
214
215******************************************************************************/
216int
217BmcLtlCheckInductiveInvariant(
218  Ntk_Network_t   *network,
219  bAigEdge_t      property,
220  BmcOption_t     *options,
221  st_table        *CoiTable)
222{
223  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
224  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
225  array_t           *unitClause;
226  int               cnfIndex;
227  array_t           *result = NIL(array_t);
228  FILE              *cnfFile;
229  st_table          *nodeToMvfAigTable = NIL(st_table);  /* maps each node to its mvfAig */
230  int               savedVerbosityLevel = options->verbosityLevel;
231  int               returnValue = 0;  /* the property is not an inductive invariant */
232
233  cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);   
234  if (cnfFile == NIL(FILE)) {
235    (void) fprintf(vis_stderr,
236                   "** bmc error: Cannot create CNF output file %s\n",
237                   options->satInFile);
238    return -1;
239  }
240  /*
241    nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph
242  */
243  nodeToMvfAigTable =
244    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
245 
246  assert(nodeToMvfAigTable != NIL(st_table));
247
248  /*
249    Clause database
250   */
251  cnfClauses = BmcCnfClausesAlloc();
252  /*
253    Check if the property holds in all intial states
254  */
255  /*
256    Generate CNF clauses for initial states
257  */
258  BmcCnfGenerateClausesForPath(network, 0, 0, BMC_INITIAL_STATES,
259                               cnfClauses, nodeToMvfAigTable, CoiTable);
260  /*
261    Generate CNF clauses for the property
262  */
263  cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, 0, cnfClauses);
264  unitClause = array_alloc(int, 1);
265  array_insert(int, unitClause, 0, cnfIndex); /* because property is the negation of
266                                                the LTL formula*/
267  BmcCnfInsertClause(cnfClauses, unitClause);
268 
269  options->verbosityLevel = BmcVerbosityNone_c;
270  BmcWriteClauses(manager, cnfFile, cnfClauses, options);
271  (void) fclose(cnfFile);
272  result = BmcCheckSAT(options);   
273  options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
274  BmcCnfClausesFree(cnfClauses);
275  if (options->satSolverError){
276    return -1;
277  }
278  if (result == NIL(array_t)){ /* the property holds at all initial states */
279    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);   
280    if (cnfFile == NIL(FILE)) {
281      (void) fprintf(vis_stderr,
282                     "** bmc error: Cannot create CNF output file %s\n",
283                     options->satInFile);
284      return -1;
285    }
286    /*
287      Check if the property holds in state i, it also holds in state i+1
288    */
289    cnfClauses = BmcCnfClausesAlloc(); 
290    /*
291      Generate CNF clauses for a transition from state i to state i+1.
292    */
293    BmcCnfGenerateClausesForPath(network, 0, 1, BMC_NO_INITIAL_STATES,
294                                 cnfClauses, nodeToMvfAigTable, CoiTable);
295   
296    cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, 0, cnfClauses);
297    array_insert(int, unitClause, 0, -cnfIndex); /* because property is the negation of
298                                                    the LTL formula */
299    BmcCnfInsertClause(cnfClauses, unitClause);
300   
301    cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, 1, cnfClauses);
302    array_insert(int, unitClause, 0, cnfIndex); /* because property is the negation of
303                                                   the LTL formula */
304    BmcCnfInsertClause(cnfClauses, unitClause);
305    options->verbosityLevel = BmcVerbosityNone_c;
306    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
307    (void) fclose(cnfFile);
308    result = BmcCheckSAT(options);
309    options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
310    BmcCnfClausesFree(cnfClauses);
311    if (options->satSolverError){
312      returnValue = -1;
313    }
314    if (result != NIL(array_t)){
315      returnValue = 0; /* the property is not an inductive invariant */
316    } else {
317      returnValue = 1;  /* the property is an inductive invariant */
318    }
319  }
320  array_free(unitClause);
321  return returnValue; 
322} /* BmcLtlCheckInductiveInvariant() */
323
324
325/**Function********************************************************************
326
327   Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of
328   the form G(p), where p is a propositional formula.]
329
330   Description [Given a model M, an LTL formula f = Gp, and a bound k,
331   we first find a counterexample of length k to a state that violates
332   p.  If -r switch of the BMC command is specified, we apply the
333   induction proof to check if the property f passes. The property f
334   passes if there is no simple path in M that leads to a state that
335   violates p, or no simple path in M starting at an initial state.
336
337   Note: Before calling this function, the LTL formula must be negated.
338   
339   ]
340
341   SideEffects []
342   
343   SeeAlso     []
344   
345******************************************************************************/
346void
347BmcLtlVerifyGp( 
348   Ntk_Network_t   *network,
349   Ctlsp_Formula_t *ltlFormula,
350   st_table        *CoiTable,
351   BmcOption_t     *options)
352{
353  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
354  st_table          *nodeToMvfAigTable = NIL(st_table);  /* maps each node to its mvfAig */
355  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
356  BmcCnfStates_t    *state;
357
358  FILE              *cnfFile;
359  array_t           *Pclause = array_alloc(int, 0);
360
361  int               k, bound, initK, propK;
362  array_t           *result = NIL(array_t);
363  long              startTime, endTime;
364  bAigEdge_t        property;
365  int               minK = options->minK;
366  int               maxK = options->maxK;
367  int               i, initState = BMC_INITIAL_STATES;
368  array_t           *unitClause;
369 
370  int               bmcError = FALSE;
371 
372  Bmc_PropertyStatus formulaStatus;
373 
374  assert(Ctlsp_LtlFormulaIsFp(ltlFormula));
375 
376  startTime = util_cpu_ctime();
377
378  if (options->verbosityLevel != BmcVerbosityNone_c){
379    (void)fprintf(vis_stdout, "LTL formula is of type G(p)\n");
380  }
381  property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula->right);
382
383  if (property == mAig_NULL){
384    return;
385  }
386  if (property == bAig_One){
387    (void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
388    (void) fprintf(vis_stdout,"# BMC: formula failed\n");
389    if (options->verbosityLevel != BmcVerbosityNone_c){
390      fprintf(vis_stdout, "-- bmc time = %10g\n",
391              (double)(util_cpu_ctime() - startTime) / 1000.0);
392    }
393    return;
394  } else if (property == bAig_Zero){
395    (void) fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
396    (void) fprintf(vis_stdout,"# BMC: formula passed\n");
397    if (options->verbosityLevel != BmcVerbosityNone_c){
398      fprintf(vis_stdout, "-- bmc time = %10g\n",
399              (double)(util_cpu_ctime() - startTime) / 1000.0);
400    }
401    return;
402  }
403
404#if 0
405  if (options->verbosityLevel == BmcVerbosityMax_c){
406    (void) fprintf(vis_stdout, "\nBMC: Check if the property is an inductive invariant\n");
407  }
408  checkInductiveInvariant = BmcLtlCheckInductiveInvariant(network, property, options, CoiTable);
409 
410  if(checkInductiveInvariant == -1){
411    return;
412  }
413  if (checkInductiveInvariant == 1){
414    (void) fprintf(vis_stdout,"# BMC: The property is an inductive invariant\n");
415    (void) fprintf(vis_stdout,"# BMC: formula passed\n");
416    if (options->verbosityLevel != BmcVerbosityNone_c){
417      fprintf(vis_stdout, "-- bmc time = %10g\n",
418              (double)(util_cpu_ctime() - startTime) / 1000.0);
419    }
420    return;
421  }
422#endif
423  if (options->verbosityLevel != BmcVerbosityNone_c){
424    (void)fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d)\n",
425                  minK, maxK, options->step);
426  }
427  initK  = 0;
428  propK  = 0;
429  formulaStatus = BmcPropertyUndecided_c;
430 
431  /* nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph */
432  nodeToMvfAigTable =
433    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
434  assert(nodeToMvfAigTable != NIL(st_table));
435
436  /*
437    Create clauses database
438  */
439  cnfClauses = BmcCnfClausesAlloc();
440  /*
441    init = BmcCreateMaigOfInitialStates(network, nodeToMvfAigTable, CoiTable);
442  */
443  for(bound = minK; bound <= maxK; bound += options->step){
444    if (options->verbosityLevel == BmcVerbosityMax_c) {
445      (void) fprintf(vis_stdout,
446                     "\nBMC: Generate counterexample of length %d\n",
447                     bound);
448    }
449    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);   
450    if (cnfFile == NIL(FILE)) {
451      (void) fprintf(vis_stderr,
452                     "** bmc error: Cannot create CNF output file %s\n",
453                     options->satInFile);
454      bmcError = TRUE;
455      break;
456    }
457    BmcCnfGenerateClausesForPath(network, initK, bound, initState, cnfClauses, nodeToMvfAigTable, CoiTable);
458
459    initState = BMC_NO_INITIAL_STATES;
460   
461    /* Generate CNF for the property */
462    Pclause = array_alloc(int, 0);
463    /*
464    state = BmcCnfClausesFreeze(cnfClauses);
465    */
466    for(k=propK; k <= bound; k++){
467      array_insert_last(
468        int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager, property,
469                                                          k, cnfClauses));
470    }
471   
472    state = BmcCnfClausesFreeze(cnfClauses);
473   
474    BmcCnfInsertClause(cnfClauses, Pclause);
475    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
476    (void) fclose(cnfFile);
477    BmcCnfClausesRestore(cnfClauses, state);
478    result = BmcCheckSAT(options);
479    if (options->satSolverError){
480      array_free(Pclause);
481      break;
482    }
483    if (result != NIL(array_t)){
484      bound++;
485      array_free(Pclause);
486      /*
487        formula failed\n"
488      */
489      formulaStatus = BmcPropertyFailed_c;
490      break;
491    }
492    unitClause = array_alloc(int, 1);
493    for(i=0; i<array_n(Pclause); i++){
494      array_insert(int, unitClause, 0, -array_fetch(int, Pclause, i));
495      BmcCnfInsertClause(cnfClauses, unitClause);
496    }
497    array_free(unitClause);   
498    array_free(Pclause);
499    FREE(state);
500    initK = bound;
501    propK = bound+1;
502
503    /*
504      Prove if the property passes using the induction proof of SSS0.
505     */
506    if((result == NIL(array_t)) &&
507       (options->inductiveStep !=0) &&
508       (bound % options->inductiveStep == 0)){
509      BmcCnfClauses_t   *cnfClauses;
510      array_t           *result = NIL(array_t);
511      array_t           *unitClause =  array_alloc(int, 1);
512      int               savedVerbosityLevel = options->verbosityLevel;
513      long              startTime = util_cpu_ctime();
514       
515      if (options->verbosityLevel == BmcVerbosityMax_c) {
516        (void) fprintf(vis_stdout, "\nBMC: Check for induction\n");
517      }
518      options->verbosityLevel = BmcVerbosityNone_c;
519
520      if(options->earlyTermination){
521        /*
522          Early termination condition
523         
524          Check if there is no simple path of length 'bound' starts from
525          initial states
526         
527        */
528        cnfClauses = BmcCnfClausesAlloc();
529       
530        cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
531        if (cnfFile == NIL(FILE)) {
532          (void)fprintf(vis_stderr,
533                        "** bmc error: Cannot create CNF output file %s\n",
534                        options->satInFile);
535          bmcError = TRUE;
536          break;
537        }
538        /*
539          Generate an initialized simple path path of length bound.
540        */
541        BmcCnfGenerateClausesForLoopFreePath(network, 0, bound, BMC_INITIAL_STATES,
542                                             cnfClauses, nodeToMvfAigTable, CoiTable);
543        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
544        (void) fclose(cnfFile);
545        BmcCnfClausesFree(cnfClauses);
546       
547        result = BmcCheckSAT(options);
548        if(options->satSolverError){
549          break;
550        }
551        if(result == NIL(array_t)){
552          if (savedVerbosityLevel == BmcVerbosityMax_c) {
553            (void) fprintf(vis_stdout,
554                           "# BMC: No simple path starting at an initial state\n");
555          }
556          formulaStatus = BmcPropertyPassed_c;
557        } else {
558          array_free(result);
559        }
560      } /* Early termination */
561      if(formulaStatus != BmcPropertyPassed_c){
562        cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
563        if (cnfFile == NIL(FILE)) {
564          (void)fprintf(vis_stderr,
565                        "** bmc error: Cannot create CNF output file %s\n",
566                        options->satInFile);
567          bmcError = TRUE;
568          break;
569        }
570        cnfClauses = BmcCnfClausesAlloc();
571        /*
572          Generate a simple path of length k+1
573        */
574        BmcCnfGenerateClausesForLoopFreePath(network, 0, bound+1, BMC_NO_INITIAL_STATES,
575                                             cnfClauses, nodeToMvfAigTable, CoiTable);
576        /*
577          All the states to bound satisfy the property.
578        */
579        unitClause = array_alloc(int, 1);
580        for(k=0; k <= bound; k++){
581          array_insert(
582            int, unitClause, 0, -BmcGenerateCnfFormulaForAigFunction(manager, property,
583                                                                     k, cnfClauses));
584          BmcCnfInsertClause(cnfClauses, unitClause);
585        }
586        /*
587          The property fails at bound +1
588        */
589        array_insert(int, unitClause, 0,
590                     BmcGenerateCnfFormulaForAigFunction(manager, property,
591                                                         bound+1, cnfClauses));
592        BmcCnfInsertClause(cnfClauses, unitClause);
593        array_free(unitClause);
594       
595        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
596        BmcCnfClausesFree(cnfClauses);
597        (void) fclose(cnfFile);
598        result = BmcCheckSAT(options);
599        if (options->satSolverError){
600          break;
601        }
602        if(result == NIL(array_t)) {
603          if (savedVerbosityLevel == BmcVerbosityMax_c) {
604            (void) fprintf(vis_stdout,
605                           "# BMC: No simple path leading to a bad state\n");
606          }
607          formulaStatus = BmcPropertyPassed_c;
608        }
609      }
610      options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
611      if (options->verbosityLevel != BmcVerbosityNone_c){
612        endTime = util_cpu_ctime();
613        fprintf(vis_stdout, "-- check for induction time = %10g\n",
614                (double)(endTime - startTime) / 1000.0);
615      }
616    } /* Check induction */
617    if(formulaStatus != BmcPropertyUndecided_c){
618      break;
619    }
620  } /* for bound loop */
621  if( bmcError == FALSE){
622    if (options->satSolverError){
623      (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
624    } else {
625      if(formulaStatus == BmcPropertyUndecided_c){
626        if (options->verbosityLevel != BmcVerbosityNone_c){
627          (void) fprintf(vis_stdout,
628                         "# BMC: no counterexample found of length up to %d \n",
629                         options->maxK);
630        }
631      }
632      if(formulaStatus == BmcPropertyFailed_c) {
633        (void) fprintf(vis_stdout, "# BMC: formula failed\n");
634         if(options->verbosityLevel != BmcVerbosityNone_c){
635           (void) fprintf(vis_stdout,
636                          "# BMC: Found a counterexample of length = %d \n", bound-1);
637         }
638        if (options->dbgLevel == 1) {
639          BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
640                                 result, bound-1, CoiTable, options, NIL(array_t));
641        }
642      } else if(formulaStatus == BmcPropertyPassed_c) {
643        (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
644      } else if(formulaStatus == BmcPropertyUndecided_c) {
645        (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
646      }
647    }
648  }
649  /* free all used memories */
650  if(cnfClauses != NIL(BmcCnfClauses_t)){
651    BmcCnfClausesFree(cnfClauses);
652  }
653  if(result != NIL(array_t)) {
654    array_free(result);
655  }
656  /*
657  array_free(Pclause);
658  */
659  if (options->verbosityLevel != BmcVerbosityNone_c){
660    endTime = util_cpu_ctime();
661    fprintf(vis_stdout, "-- bmc time = %10g\n",
662            (double)(endTime - startTime) / 1000.0);
663  }
664  fflush(vis_stdout);
665  return;
666} /* BmcLtlVerifyGp()  */
667
668/**Function********************************************************************
669
670   Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of
671   the form F(p), where p is propositional.]
672
673   Description [Given a model M, an LTL formula f = Fp, and a bound k,
674   we first find a k-loop counterexample of length k at which all
675   states violate p.  If -r switch of the BMC command is specified, we
676   apply the method in the paper "Proving More Properties with Bounded
677   Model Checking" to check if the property f passes.
678
679   Note: Before calling this function, the LTL formula must be negated.
680   
681   ]   
682   SideEffects []
683   
684   SeeAlso     []
685
686******************************************************************************/
687void
688BmcLtlVerifyFp(
689   Ntk_Network_t   *network,
690   Ctlsp_Formula_t *ltlFormula,
691   st_table        *CoiTable,
692   BmcOption_t     *options)
693{
694  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
695  st_table        *nodeToMvfAigTable = NIL(st_table);  /* maps each node to its mvfAig */
696  BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
697 
698 
699  FILE       *cnfFile;
700  array_t    *unitClause= array_alloc(int, 1), *outClause;
701  int        outIndex;
702  int        k;
703  array_t    *result  = NIL(array_t);
704  long       startTime, endTime;
705  bAigEdge_t property;
706  int        bound;
707  int        bmcError = FALSE;
708   
709  Bmc_PropertyStatus formulaStatus = BmcPropertyUndecided_c;
710
711  assert(Ctlsp_LtlFormulaIsGp(ltlFormula));
712   
713  startTime = util_cpu_ctime();
714  if (options->verbosityLevel != BmcVerbosityNone_c){
715    (void)fprintf(vis_stdout, "LTL formula is of type F(p)\n");
716  }
717  property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula->right);
718  if (property == mAig_NULL){
719    return;
720  }
721  if (property == bAig_One){
722    (void) fprintf(vis_stdout, "# BMC: formula failed\n");
723    (void) fprintf(vis_stdout, "       Empty counterexample because the property is always FALSE\n");
724    if (options->verbosityLevel != BmcVerbosityNone_c) {
725      endTime = util_cpu_ctime();
726      fprintf(vis_stdout, "-- bmc time = %10g\n",
727              (double)(endTime - startTime) / 1000.0);
728    }
729    return;
730  } else if (property == bAig_Zero){
731    (void) fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
732    formulaStatus = BmcPropertyPassed_c;
733    (void) fprintf(vis_stdout,"# BMC: formula passed\n");
734    if (options->verbosityLevel != BmcVerbosityNone_c) {
735      endTime = util_cpu_ctime();
736      fprintf(vis_stdout, "-- bmc time = %10g\n",
737              (double)(endTime - startTime) / 1000.0);
738    }
739    return;
740  }
741  if (options->verbosityLevel != BmcVerbosityNone_c){
742    (void)fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
743                  options->minK, options->maxK, options->step);
744  }
745  /*
746    nodeToMvfAigTable Maps each node to its Multi-function AIG graph
747  */
748  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
749  assert(nodeToMvfAigTable != NIL(st_table));
750  outClause = NIL(array_t);
751  bound = options->minK;
752  BmcGetCoiForLtlFormula(network, ltlFormula, CoiTable);
753 
754  while( (result == NIL(array_t)) && (bound <= options->maxK)){
755    if (options->verbosityLevel == BmcVerbosityMax_c) {
756      (void) fprintf(vis_stdout,
757                     "\nBMC: Generate counterexample of length %d\n", bound);
758    }
759    cnfClauses = BmcCnfClausesAlloc();
760    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);   
761    if (cnfFile == NIL(FILE)) {
762      (void)fprintf(vis_stderr,
763                    "** bmc error: Cannot create CNF output file %s\n",
764                    options->satInFile);
765      bmcError = TRUE;
766      break;
767    }
768    /*
769      Generate clauses for an initialized path of length "bound".
770    */
771    BmcCnfGenerateClausesForPath(network, 0, bound, BMC_INITIAL_STATES,
772                                 cnfClauses, nodeToMvfAigTable, CoiTable);
773    /*
774      Generate CNF for the property. Property fails at all states
775     */
776    for(k=0; k <= bound; k++){
777      array_insert(int, unitClause, 0,
778                   BmcGenerateCnfFormulaForAigFunction(manager, property,
779                                                       k, cnfClauses));
780      BmcCnfInsertClause(cnfClauses, unitClause);
781    }
782
783    /* Generate CNF for a loop-back (loop from the last state to any
784       state) path.
785       (Sk -> S0) + (Sk -> S1) + ..... + (Sk-> Sk-1) + (Sk-> Sk)
786       Each transition consisits of one or more latches.  We
787       AND the transiton relation of these latches.  For multi-valued
788       latches, we OR the equivalence of each value of the latch. To
789       do the AND we use the CNF equivalent of the AND.  a = b*c => (b
790       + !a) * (c + !a)
791    */
792    outClause = array_alloc(int, bound);   
793    for (k=0; k <= bound; k++){
794      /*
795        Create new var for the output of the AND node.
796      */
797      outIndex = cnfClauses->cnfGlobalIndex++;
798      BmcCnfGenerateClausesFromStateToState(network, bound, k, cnfClauses,
799                                            nodeToMvfAigTable, CoiTable, outIndex);
800      array_insert(int, outClause, k, outIndex);
801    }  /* for k state loop */
802    BmcCnfInsertClause(cnfClauses, outClause);
803 
804    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
805    (void) fclose(cnfFile);
806   
807    result = BmcCheckSAT(options);
808    if (options->satSolverError){
809      break;
810    }
811    if(result != NIL(array_t)){
812      formulaStatus = BmcPropertyFailed_c;
813      break;
814    }
815    BmcCnfClausesFree(cnfClauses);
816    array_free(outClause);
817    if((result == NIL(array_t)) &&
818       (options->inductiveStep !=0) &&
819       (bound % options->inductiveStep == 0)
820       )   
821      {
822      int     savedVerbosityLevel = options->verbosityLevel;
823      long    startTime = util_cpu_ctime();
824      array_t *result  = NIL(array_t);
825
826      if (options->verbosityLevel == BmcVerbosityMax_c) {
827        (void) fprintf(vis_stdout,
828                       "\nBMC: Check if the property passes\n");
829      }
830      cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
831      if (cnfFile == NIL(FILE)) {
832        (void)fprintf(vis_stderr,
833                      "** bmc error: Cannot create CNF output file %s\n",
834                      options->satInFile);
835        bmcError = TRUE;
836        break;
837      }
838      cnfClauses = BmcCnfClausesAlloc();
839      /*
840        CNF for an initialized simple path.
841       */
842      BmcCnfGenerateClausesForLoopFreePath(network, 0, bound, BMC_INITIAL_STATES,
843                                           cnfClauses, nodeToMvfAigTable, CoiTable);
844      /*
845        Generate CNF for the property. Property fails at all states
846      */
847      for(k=0; k <= bound; k++){
848        array_insert(int, unitClause, 0,
849                     BmcGenerateCnfFormulaForAigFunction(manager, property,
850                                                         k, cnfClauses));
851        BmcCnfInsertClause(cnfClauses, unitClause);
852      }
853      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
854      BmcCnfClausesFree(cnfClauses);
855      (void) fclose(cnfFile);
856      /*
857        Do not print any detail information when checking the clauses
858       */
859      options->verbosityLevel = BmcVerbosityNone_c;
860      result = BmcCheckSAT(options);
861      options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
862      if (options->satSolverError){
863        break;
864      }
865      if (options->verbosityLevel != BmcVerbosityNone_c){
866        endTime = util_cpu_ctime();
867        fprintf(vis_stdout, "--  checking time = %10g\n",
868                (double)(endTime - startTime) / 1000.0);
869      }
870      if (result == NIL(array_t)){ /* UNSAT */
871        formulaStatus = BmcPropertyPassed_c;
872        break;  /* formula is satisfiable */
873      }
874      array_free(result);
875    } /* Check induction */
876
877    /* free all used memories
878    BmcCnfClausesFree(cnfClauses); */
879
880    bound += options->step;
881  } /* while result and bound */
882  if (bmcError == FALSE){
883    if(!options->satSolverError){
884      if(formulaStatus == BmcPropertyFailed_c) {
885        (void) fprintf(vis_stdout, "# BMC: formula failed\n");
886        if(options->verbosityLevel != BmcVerbosityNone_c){
887          (void) fprintf(vis_stdout,
888                         "# BMC: Found a counterexample of length = %d \n", bound);
889        }
890        if (options->dbgLevel == 1) {
891          BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
892                                 result, bound, CoiTable, options, outClause);
893        }
894        array_free(result);
895        BmcCnfClausesFree(cnfClauses);
896        array_free(outClause);
897      } else if(formulaStatus == BmcPropertyPassed_c) {
898        (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
899      } else if(formulaStatus == BmcPropertyUndecided_c) {
900        (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
901        if (options->verbosityLevel != BmcVerbosityNone_c){
902          (void) fprintf(vis_stdout,
903                       "# BMC: no counterexample found of length up to %d \n",
904                         options->maxK);
905        }
906      }
907    } else {
908      (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
909    }
910  }
911  if (options->verbosityLevel != BmcVerbosityNone_c) {
912    endTime = util_cpu_ctime();
913    fprintf(vis_stdout, "-- bmc time = %10g\n",
914            (double)(endTime - startTime) / 1000.0);
915  }
916  if(unitClause != NIL(array_t)) {
917    array_free(unitClause);
918  }
919  fflush(vis_stdout); 
920  return;
921} /* BmcLtlVerifyFp() */
922
923/**Function********************************************************************
924
925   Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of
926   the form FG(p), where p is propositional.]
927
928   Description [Given a model M, an LTL formula f = FGp, and a bound
929   k, we first find a k-loop counterexample of length k at which p
930   false inside the loop.  If -r switch of the BMC command is
931   specified, we apply the method in the paper "Proving More
932   Properties with Bounded Model Checking" to check if the property f
933   passes.
934
935   Note: Before calling this function, the LTL formula must be negated.
936   
937   ]
938 
939  SideEffects []
940
941  SeeAlso     []
942
943******************************************************************************/
944void
945BmcLtlVerifyFGp(
946   Ntk_Network_t   *network,
947   Ctlsp_Formula_t *ltlFormula,
948   st_table        *CoiTable,
949   BmcOption_t     *options)
950{
951  mAig_Manager_t   *manager = Ntk_NetworkReadMAigManager(network);
952  st_table         *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
953  BmcCnfClauses_t  *cnfClauses = NIL(BmcCnfClauses_t);
954  FILE             *cnfFile;
955 
956  array_t          *orClause, *tmpClause, *loopClause;
957  int              k, l, andIndex, loop;
958  array_t          *result = NIL(array_t);
959  long             startTime, endTime;
960  int              minK = options->minK;
961  int              maxK = options->maxK;
962  Ctlsp_Formula_t  *propFormula;
963  bAigEdge_t       property;
964
965  Bmc_PropertyStatus formulaStatus;
966  int                bmcError = FALSE;
967 
968  int              m=-1, n=-1;
969  int              checkLevel = 0;
970  /*
971    Refer to Theorem 1 in the paper "Proving More Properties with Bounded Model Checking"
972   
973    If checkLevel == 0 -->  check for beta' only. If UNSAT, m=k and chekLevel = 1
974    If checkLevel == 1 -->  check for beta  only. If UNSAT, checkLevel = 2.
975    If checkLevel == 2 -->  check for alpha only. If UNSAT, n=k and checkLevel = 3.
976    If gama is UNSAT up to (m+n-1) and checkLvel = 3, formula passes.
977    checkLevel = 4 if (m+n-1) > maxK; */
978
979  /*
980    Remember the LTL property was negated
981   */
982  assert(Ctlsp_LtlFormulaIsGFp(ltlFormula));
983
984  /* ************** */
985 
986  /* Initialization */
987 
988  /* ************** */
989  loopClause = NIL(array_t);
990  startTime = util_cpu_ctime();
991  /*
992    nodeToMvfAigTable maps each node to its multi-function And/Inv graph
993  */
994  nodeToMvfAigTable =
995    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
996  if (nodeToMvfAigTable == NIL(st_table)){
997    (void) fprintf(vis_stderr,
998                   "** bmc error: you need to build the AIG structure first\n");
999    return;
1000  }
1001  propFormula = Ctlsp_FormulaReadRightChild(Ctlsp_FormulaReadRightChild(ltlFormula));
1002  property    = BmcCreateMaigOfPropFormula(network, manager, propFormula);
1003  if (options->verbosityLevel != BmcVerbosityNone_c){
1004    (void)fprintf(vis_stdout, "LTL formula is of type FG(p)\n");
1005    (void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
1006                  minK, maxK, options->step);
1007  }
1008  tmpClause  = array_alloc(int, 2);
1009  k= minK;
1010  formulaStatus = BmcPropertyUndecided_c;
1011  while( (result == NIL(array_t)) && (k <= maxK)){
1012    /*
1013      Search for a k-loop counterexample of length k.
1014     */
1015    if (options->verbosityLevel == BmcVerbosityMax_c) {
1016      (void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
1017    }
1018    /*
1019      Create a clause database
1020     */
1021    cnfClauses = BmcCnfClausesAlloc();
1022
1023    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
1024    if (cnfFile == NIL(FILE)) {
1025      (void)fprintf(vis_stderr,
1026                    "** bmc error: Cannot create CNF output file %s\n",
1027                    options->satInFile);
1028      bmcError = TRUE;
1029      break;
1030    }
1031   
1032    /**********************************************
1033       \gama(k)
1034    ***********************************************/
1035    /*
1036      Generate an initialized path of length k.
1037     */
1038    BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES, cnfClauses, nodeToMvfAigTable, CoiTable);
1039    /*
1040      k-loop
1041     */
1042    orClause   = array_alloc(int, 0);
1043    loopClause = array_alloc(int, k+1);
1044    for(l=0; l<=k; l++){
1045      /*
1046        Use to check if there is a loop from k to l.
1047       */
1048      loop = cnfClauses->cnfGlobalIndex++;
1049      BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses, nodeToMvfAigTable, CoiTable, loop);
1050      array_insert(int, loopClause, l, loop);
1051     
1052      andIndex   = cnfClauses->cnfGlobalIndex++;
1053      array_insert(int, tmpClause, 0, loop);
1054      array_insert(int, tmpClause, 1, -andIndex);
1055      BmcCnfInsertClause(cnfClauses, tmpClause);
1056
1057      /*
1058                 l
1059        If [[F p]]  if p true in a state from l to k.
1060                 k
1061       */
1062      array_insert(int, tmpClause, 0,
1063                   BmcGenerateCnfForLtl(network, Ctlsp_FormulaCreate(Ctlsp_F_c, propFormula, NIL(Ctlsp_Formula_t)),
1064                                        l, k, -1, cnfClauses));
1065      BmcCnfInsertClause(cnfClauses, tmpClause);
1066     
1067      array_insert_last(int, orClause, andIndex);
1068    } /* for l loop */
1069    BmcCnfInsertClause(cnfClauses, orClause);
1070    array_free(orClause);
1071    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1072    (void) fclose(cnfFile);
1073     
1074    result = BmcCheckSAT(options);
1075    if(options->satSolverError){
1076      break;
1077    }
1078    if(result != NIL(array_t)) {
1079      formulaStatus = BmcPropertyFailed_c;
1080      break;
1081    }
1082    array_free(loopClause);
1083    /* free all used memories */
1084    BmcCnfClausesFree(cnfClauses);
1085
1086    /* ====================================================================
1087             Use termination criteria to prove that the property passes.
1088       ==================================================================== */
1089    if((result == NIL(array_t)) &&
1090       (options->inductiveStep !=0) &&
1091       (k % options->inductiveStep == 0)
1092       )
1093      {
1094        array_t *unitClause = array_alloc(int, 0);
1095        array_t *result = NIL(array_t);
1096        int     savedVerbosityLevel = options->verbosityLevel;
1097
1098        options->verbosityLevel = BmcVerbosityNone_c;
1099        /* ===========================
1100           Early termination condition
1101           =========================== */
1102        if(options->earlyTermination){
1103          if (savedVerbosityLevel == BmcVerbosityMax_c) {
1104            (void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
1105          }
1106          cnfClauses = BmcCnfClausesAlloc();
1107
1108          cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
1109          if (cnfFile == NIL(FILE)) {
1110            (void)fprintf(vis_stderr,
1111                          "** abmc error: Cannot create CNF output file %s\n",
1112                          options->satInFile);
1113            bmcError = TRUE;
1114            break;
1115          }
1116          /*
1117            Generate an initialized simple path path of length k.
1118          */
1119          BmcCnfGenerateClausesForLoopFreePath(network, 0, k, BMC_INITIAL_STATES,
1120                                               cnfClauses, nodeToMvfAigTable, CoiTable);
1121          BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1122          (void) fclose(cnfFile);
1123          BmcCnfClausesFree(cnfClauses);
1124         
1125          result = BmcCheckSAT(options);
1126          if(options->satSolverError){
1127            break;
1128          }
1129          if(result == NIL(array_t)) {
1130            formulaStatus = BmcPropertyPassed_c;
1131            if (savedVerbosityLevel == BmcVerbosityMax_c) {
1132              (void) fprintf(vis_stdout, "# BMC: By early termination\n");
1133            }
1134            break;
1135          }
1136        } /* Early termination */
1137
1138        /*
1139          Check \beta''(k)
1140        */
1141        if(checkLevel == 0){
1142          int i;
1143         
1144          cnfClauses = BmcCnfClausesAlloc();
1145          if (savedVerbosityLevel == BmcVerbosityMax_c) {
1146            (void) fprintf(vis_stdout, "# BMC: Check beta'' \n");
1147          }
1148          cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
1149          if (cnfFile == NIL(FILE)) {
1150            (void)fprintf(vis_stderr,
1151                          "** bmc error: Cannot create CNF output file %s\n",
1152                          options->satInFile);
1153            bmcError = TRUE;
1154            break;
1155          }
1156          /*
1157            Generate a simple path of length k+1.
1158          */
1159          BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
1160                                               cnfClauses, nodeToMvfAigTable, CoiTable);
1161          for(i=1; i<=k+1; i++){
1162            array_insert(int, unitClause, 0,
1163                         -BmcGenerateCnfFormulaForAigFunction(manager, property,
1164                                                              i, cnfClauses));
1165            BmcCnfInsertClause(cnfClauses, unitClause);
1166          }
1167          array_insert(int, unitClause, 0,
1168                       BmcGenerateCnfFormulaForAigFunction(manager, property,
1169                                                           0, cnfClauses));
1170          BmcCnfInsertClause(cnfClauses, unitClause);
1171         
1172          BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1173          (void) fclose(cnfFile);
1174         
1175          result = BmcCheckSAT(options);
1176          BmcCnfClausesFree(cnfClauses);
1177          if(options->satSolverError){
1178            break;
1179          }
1180          if(result == NIL(array_t)) {
1181            m = k;
1182            printf("Beta'': Value of m = %d\n", m);
1183            checkLevel = 1;
1184          }
1185        } /* Check for beta'' */
1186       
1187        /*
1188          Check \beta'(k)
1189        */
1190        if(checkLevel == 0){
1191          int i;
1192         
1193          cnfClauses = BmcCnfClausesAlloc();
1194          if (savedVerbosityLevel == BmcVerbosityMax_c) {
1195            (void) fprintf(vis_stdout, "# BMC: Check beta' \n");
1196          }
1197          cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
1198          if (cnfFile == NIL(FILE)) {
1199            (void)fprintf(vis_stderr,
1200                          "** bmc error: Cannot create CNF output file %s\n",
1201                          options->satInFile);
1202            bmcError = TRUE;
1203            break;
1204          }
1205          /*
1206            Generate a simple path of length k+1.
1207          */
1208          BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
1209                                               cnfClauses, nodeToMvfAigTable, CoiTable);
1210          for(i=0; i<=k; i++){
1211            array_insert(int, unitClause, 0,
1212                         -BmcGenerateCnfFormulaForAigFunction(manager, property,
1213                                                              i, cnfClauses));
1214            BmcCnfInsertClause(cnfClauses, unitClause);
1215          }
1216          array_insert(int, unitClause, 0,
1217                       BmcGenerateCnfFormulaForAigFunction(manager, property,
1218                                                           k+1, cnfClauses));
1219          BmcCnfInsertClause(cnfClauses, unitClause);
1220         
1221          BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1222          (void) fclose(cnfFile);
1223         
1224          result = BmcCheckSAT(options);
1225          BmcCnfClausesFree(cnfClauses);
1226          if(options->satSolverError){
1227            break;
1228          }
1229          if(result == NIL(array_t)) {
1230            m = k;
1231            printf("Beta': Value of m = %d\n", m);
1232            checkLevel = 1;
1233          }
1234        } /* Check for beta' */
1235        /*
1236          Check for beta
1237        */
1238        if(checkLevel == 1){
1239          cnfClauses = BmcCnfClausesAlloc();
1240          if (savedVerbosityLevel == BmcVerbosityMax_c) {
1241            (void) fprintf(vis_stdout, "# BMC: Check beta\n");
1242          }       
1243          cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
1244          if (cnfFile == NIL(FILE)) {
1245            (void)fprintf(vis_stderr,
1246                          "** bmc error: Cannot create CNF output file %s\n",
1247                          options->satInFile);
1248            bmcError = TRUE;
1249            break;
1250          }
1251          /*
1252            Generate a simple path of length k+1.
1253          */
1254          BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
1255                                               cnfClauses, nodeToMvfAigTable, CoiTable);
1256          array_insert(int, unitClause, 0,
1257                       -BmcGenerateCnfFormulaForAigFunction(manager, property,
1258                                                            k, cnfClauses));
1259          BmcCnfInsertClause(cnfClauses, unitClause);
1260          array_insert(int, unitClause, 0,
1261                       BmcGenerateCnfFormulaForAigFunction(manager, property,
1262                                                           k+1, cnfClauses));
1263          BmcCnfInsertClause(cnfClauses, unitClause);
1264         
1265          BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1266          (void) fclose(cnfFile);
1267         
1268          result = BmcCheckSAT(options);
1269          BmcCnfClausesFree(cnfClauses);
1270          if(options->satSolverError){
1271            break;
1272          }
1273          if(result == NIL(array_t)) {
1274            checkLevel = 2;
1275          }
1276        } /* Check beta */
1277     
1278        if(checkLevel == 2){ /* we check \alpha if \beta UNSAT */
1279          if (savedVerbosityLevel == BmcVerbosityMax_c) {
1280            (void) fprintf(vis_stdout, "# BMC: Check alpha \n");
1281          }       
1282          /*
1283            \alpha(k)
1284          */
1285          cnfClauses = BmcCnfClausesAlloc();
1286         
1287          cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
1288          if (cnfFile == NIL(FILE)) {
1289            (void)fprintf(vis_stderr,
1290                          "** bmc error: Cannot create CNF output file %s\n",
1291                          options->satInFile);
1292            bmcError = TRUE;
1293            break;
1294          }
1295          /*
1296            Generate an initialized path of length k.
1297          */
1298          BmcCnfGenerateClausesForLoopFreePath(network, 0, k, BMC_INITIAL_STATES,
1299                                               cnfClauses, nodeToMvfAigTable, CoiTable);
1300         
1301          array_insert(int, unitClause, 0,
1302                       BmcGenerateCnfFormulaForAigFunction(manager, property,
1303                                                           k, cnfClauses));
1304          BmcCnfInsertClause(cnfClauses, unitClause);
1305         
1306         
1307          BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1308          (void) fclose(cnfFile);
1309         
1310          result = BmcCheckSAT(options);
1311          BmcCnfClausesFree(cnfClauses);
1312          if(options->satSolverError){
1313            break;
1314          }
1315          if(result == NIL(array_t)) {
1316            n = k;
1317            checkLevel = 3;
1318            printf("m=%d  n=%d\n",m,n);
1319            if ((m+n-1) <= maxK){
1320              maxK = m+n-1;
1321            } else {
1322              checkLevel = 4;
1323            }
1324          }
1325        }/* Check alpha */
1326        array_free(unitClause);
1327        options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
1328      } /* Prove the property passes*/
1329    k += options->step;
1330  } /* while result and k*/
1331  if (bmcError == FALSE){
1332    if(options->satSolverError){
1333      (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
1334    } else {
1335      if(checkLevel == 3){
1336        (void) fprintf(vis_stdout, "# BMC: (m+n-1) Complete the theorem\n");
1337        formulaStatus = BmcPropertyPassed_c;
1338      }
1339      if(formulaStatus == BmcPropertyFailed_c) {
1340        (void) fprintf(vis_stdout, "# BMC: formula failed\n");
1341        if(options->verbosityLevel != BmcVerbosityNone_c){
1342          (void) fprintf(vis_stdout,
1343                         "# BMC: Found a counterexample of length = %d \n", k);
1344        }
1345        if (options->dbgLevel == 1) {
1346          BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
1347                                 result, k, CoiTable, options, loopClause);
1348          BmcCnfClausesFree(cnfClauses);
1349          array_free(loopClause);
1350        }
1351      } else if(formulaStatus == BmcPropertyPassed_c) {
1352        (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
1353      } else if(formulaStatus == BmcPropertyUndecided_c) {
1354        (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
1355        if (options->verbosityLevel != BmcVerbosityNone_c){
1356          (void) fprintf(vis_stdout,
1357                         "# BMC: no counterexample found of length up to %d \n",
1358                         maxK);
1359        }
1360      }
1361    }
1362  }
1363  /*
1364    free all used memories
1365  */
1366  array_free(tmpClause);
1367 
1368  if(result != NIL(array_t)){
1369    array_free(result);
1370  }
1371  if (options->verbosityLevel != BmcVerbosityNone_c) {
1372    endTime = util_cpu_ctime();
1373    fprintf(vis_stdout, "-- abmc time = %10g\n",
1374            (double)(endTime - startTime) / 1000.0);
1375  }
1376  fflush(vis_stdout);
1377  return;
1378} /* BmcLtlVerifyGFp() */
1379
1380/**Function********************************************************************
1381
1382   Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of
1383   depth = 1]
1384
1385   Description [The depth of the LTL formula f is the maximum level of
1386   nesting of temporal operators in f.  If the depth of the LTL
1387   formula = 1, the translation of the formula in case of loop is
1388   independent of the loop.
1389
1390   Note: Before calling this function, the LTL formula must be negated.
1391   
1392   ]
1393
1394  SideEffects []
1395
1396  SeeAlso     []
1397
1398******************************************************************************/
1399void
1400BmcLtlVerifyUnitDepth(
1401   Ntk_Network_t   *network,
1402   Ctlsp_Formula_t *ltlFormula,
1403   st_table        *CoiTable,
1404   BmcOption_t     *options)
1405{
1406  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
1407  st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
1408  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
1409  FILE              *cnfFile;
1410
1411  array_t           *orClause =NIL(array_t);
1412  array_t           *loopClause, *tmpclause;
1413  int               l, loopIndex, andIndex, loop;
1414  int               noLoopIndex;
1415  array_t           *result = NIL(array_t);
1416 
1417  int               leftValue  = 0;
1418  int               rightValue = 0;
1419  long              startTime, endTime;
1420  int               k;
1421  int               minK = options->minK;
1422  int               maxK = options->maxK;
1423                    /* Store the index of a loop from k to all sate from 0 to k */
1424 
1425  Bmc_PropertyStatus       formulaStatus;
1426  BmcCheckForTermination_t *terminationStatus = 0;
1427  int                      bmcStatus=0; /* Holds the status of running BMC
1428                                           = -1 if there is an error */
1429 
1430  assert(Ctlsp_LtlFormulaDepth(ltlFormula) == 1);
1431 
1432  /* ************** */
1433  /* Initialization */
1434  /* ************** */
1435 
1436  startTime = util_cpu_ctime();
1437  /*
1438    nodeToMvfAigTable maps each node to its multi-function AIG graph
1439  */
1440  nodeToMvfAigTable =
1441    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
1442  assert(nodeToMvfAigTable != NIL(st_table));
1443
1444  loopClause = NIL(array_t);
1445 
1446  if (options->verbosityLevel != BmcVerbosityNone_c){
1447    (void) fprintf(vis_stdout, "Unit depth LTL formula\n");
1448    (void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
1449                  minK, maxK, options->step);
1450  }
1451   if(options->inductiveStep !=0){
1452     /*
1453       Use the termination criteria to prove the property passes.   
1454     */
1455     terminationStatus = BmcAutTerminationAlloc(network,
1456                                                Ctlsp_LtllFormulaNegate(ltlFormula),
1457                                                NIL(array_t));
1458     assert(terminationStatus);
1459   }
1460  k = minK;
1461  formulaStatus = BmcPropertyUndecided_c;
1462  while( (result == NIL(array_t)) && (k <= maxK)){
1463    if (options->verbosityLevel == BmcVerbosityMax_c) {
1464      (void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
1465    }
1466    /*
1467      Create clause database
1468     */
1469    cnfClauses = BmcCnfClausesAlloc();
1470
1471    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
1472    if (cnfFile == NIL(FILE)) {
1473      (void)fprintf(vis_stderr,
1474                    "** bmc error: Cannot create CNF output file %s\n",
1475                    options->satInFile);
1476      bmcStatus = -1;
1477      break;
1478    }
1479    /*
1480      Generate clauses represent an initialized path of length k
1481     */
1482    BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
1483                                 cnfClauses, nodeToMvfAigTable, CoiTable);
1484    /*
1485      Generate clauses represent paths which satisfy the LTL formula if
1486      there is no loop.
1487    */
1488    noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
1489    leftValue   = checkIndex(noLoopIndex, cnfClauses);
1490    if (leftValue != 1) { /* no loop  part of the basic encoding is not TRUE */
1491      orClause = array_alloc(int, 0);   
1492      /*
1493        No need to check for !Lk in the basic encoding
1494      */
1495      if (leftValue == -1){ /* no loop part of the basic encoding is not FALSE */
1496        array_insert_last(int, orClause, noLoopIndex);
1497      }
1498      /*
1499        Generate clauses represent paths which satisfy the LTL formula if
1500        there is a loop.
1501      */
1502      loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, 0, cnfClauses);
1503      rightValue = checkIndex(loopIndex, cnfClauses);
1504      if (rightValue == 0){ /* loop  part of the basic encoding is FALSE */
1505        break;
1506      }
1507      /*
1508        rightValue can be 1 or -1
1509        leftValue can be 0 or -1
1510       */
1511      if (noLoopIndex == loopIndex){ /* do not check for the existence of a loop*/
1512        break;
1513      }
1514      /*
1515        Clauses for loop-back path.
1516       */
1517      loopClause = array_alloc(int, k+2);
1518      for(l=0; l<=k; l++){
1519          loop = cnfClauses->cnfGlobalIndex++;
1520          BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses,
1521                                                nodeToMvfAigTable, CoiTable, loop);
1522          array_insert(int, loopClause, l, loop);
1523      } /* for l loop */
1524      loop = cnfClauses->cnfGlobalIndex++;
1525      array_insert(int, loopClause, k+1, -loop);
1526      BmcCnfInsertClause(cnfClauses, loopClause);
1527      if(rightValue == -1){
1528        andIndex   = cnfClauses->cnfGlobalIndex++;
1529        tmpclause  = array_alloc(int, 2);
1530       
1531        array_insert(int, tmpclause, 0, loop);
1532        array_insert(int, tmpclause, 1, -andIndex);
1533        BmcCnfInsertClause(cnfClauses, tmpclause);
1534       
1535        array_insert(int, tmpclause, 0, loopIndex);
1536        array_insert(int, tmpclause, 1, -andIndex);
1537        BmcCnfInsertClause(cnfClauses, tmpclause);
1538       
1539        array_free(tmpclause);
1540        array_insert_last(int, orClause, andIndex);
1541      } else {
1542        array_insert_last(int, orClause, loop);
1543      }
1544    }
1545    /* if((leftValue == 1) || (rightValue == 1)){ */
1546    if(leftValue == 1){
1547      assert(k==1);
1548      /*
1549        formula failed
1550      */
1551      formulaStatus = BmcPropertyFailed_c;
1552      if (options->verbosityLevel != BmcVerbosityNone_c){
1553        (void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
1554      }
1555      break;
1556    } else if((leftValue == 0) && (rightValue == 0)){
1557      if (options->verbosityLevel != BmcVerbosityNone_c){
1558        (void) fprintf(vis_stdout,"# BMC: the formula is trivially true");
1559        (void) fprintf(vis_stdout," for counterexamples of length %d\n", k);
1560      }
1561    } else {
1562      BmcCnfInsertClause(cnfClauses, orClause);
1563      array_free(orClause);
1564      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1565      (void) fclose(cnfFile);
1566     
1567      result = BmcCheckSAT(options);
1568      if(options->satSolverError){
1569        break;
1570      }
1571      if(result != NIL(array_t)) {
1572        /*
1573          formula failed
1574        */
1575        formulaStatus = BmcPropertyFailed_c;
1576      } else {
1577        /* free some used memories */
1578        BmcCnfClausesFree(cnfClauses);
1579        array_free(loopClause);
1580        /*
1581          Use the termination check
1582        */
1583
1584        if(terminationStatus && (formulaStatus == BmcPropertyUndecided_c) && (bmcStatus != 1)){
1585          if((options->inductiveStep !=0) &&
1586             (k % options->inductiveStep == 0)
1587             )
1588            {
1589              /*
1590                Check for termination for the current value of k.
1591              */
1592              terminationStatus->k = k;
1593              bmcStatus = BmcAutLtlCheckForTermination(network,
1594                                                       NIL(array_t), terminationStatus,
1595                                                       nodeToMvfAigTable, CoiTable, options);
1596              if(bmcStatus == 1){
1597                maxK = options->maxK;
1598              }
1599              if(bmcStatus == 3){
1600                formulaStatus = BmcPropertyPassed_c;
1601                break;
1602              }
1603              if(bmcStatus == -1){
1604                break;
1605              }
1606            }
1607        } /* terminationStatus */
1608      }
1609    }
1610    k += options->step;
1611  } /* while result and k*/
1612
1613 /*
1614    If no error.
1615   */
1616  if(bmcStatus != -1){
1617    if(bmcStatus == 1){
1618      (void) fprintf(vis_stdout,
1619                     "# BMC: no counterexample found of length up to %d \n", options->maxK);
1620      (void) fprintf(vis_stdout, "# BMC: By termination criterion (m+n-1)\n");
1621      formulaStatus = BmcPropertyPassed_c;
1622    }
1623    if(options->satSolverError){
1624      (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
1625    } else {
1626      if(formulaStatus == BmcPropertyFailed_c) {
1627        (void) fprintf(vis_stdout, "# BMC: formula failed\n");
1628        if(options->verbosityLevel != BmcVerbosityNone_c){
1629          (void) fprintf(vis_stdout,
1630                         "# BMC: Found a counterexample of length = %d \n", k);
1631        }
1632        if ((options->dbgLevel == 1) && (result != NIL(array_t))) {
1633          BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
1634                                 result, k, CoiTable, options, loopClause);
1635        }
1636        /* free some used memories */
1637        BmcCnfClausesFree(cnfClauses);
1638        array_free(loopClause);
1639        array_free(result);
1640      } else if(formulaStatus == BmcPropertyPassed_c) {
1641        (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
1642        (void) fprintf(vis_stdout, "#      Termination depth = %d\n", maxK);
1643      } else if(formulaStatus == BmcPropertyUndecided_c) {
1644        (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
1645        if (options->verbosityLevel != BmcVerbosityNone_c){
1646          (void) fprintf(vis_stdout,
1647                         "# BMC: no counterexample found of length up to %d \n",
1648                         maxK);
1649        }
1650      }
1651    }
1652  }
1653  if (options->verbosityLevel != BmcVerbosityNone_c) {
1654    endTime = util_cpu_ctime();
1655    fprintf(vis_stdout, "-- bmc time = %10g\n",
1656            (double)(endTime - startTime) / 1000.0);
1657  }
1658  if(terminationStatus){
1659    BmcAutTerminationFree(terminationStatus);
1660  }
1661  fflush(vis_stdout);
1662  return;
1663} /* Bmc_VerifyUnitDepth() */
1664
1665/**Function********************************************************************
1666
1667  Synopsis    [Use BMC to verify a general LTL formulae]
1668
1669  Description [Implements the Bounded Model Checking technique as in the paper
1670  "Symbolic Model Checking without BDDs".  We also have implemented some of the
1671  improvements in the BMC encoding described in the paper "Improving the
1672  Encoding of LTL Model Checking into SAT" ]
1673
1674  SideEffects []
1675
1676  SeeAlso     []
1677
1678******************************************************************************/
1679void
1680BmcLtlVerifyGeneralLtl(
1681   Ntk_Network_t   *network,
1682   Ctlsp_Formula_t *ltlFormula,
1683   st_table        *CoiTable,
1684   array_t         *constraintArray,
1685   BmcOption_t     *options)
1686{
1687  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
1688  st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
1689  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
1690  FILE              *cnfFile;
1691
1692  array_t           *orClause = NIL(array_t);
1693  array_t           *loopClause, *tmpclause;
1694  int               l, loopIndex, andIndex, loop;
1695  int               noLoopIndex;
1696  array_t           *result = NIL(array_t);
1697  array_t           *fairnessArray = NIL(array_t);
1698  int               leftValue  = 0;
1699  int               rightValue = 0;
1700  long              startTime, endTime;
1701  int               k;
1702  int               minK = options->minK;
1703  int               maxK = options->maxK;
1704  boolean           boundedFormula;
1705  int               depth;
1706                    /* Store the index of loop from k to all sate from 0 to k */
1707 
1708  array_t           *ltlConstraintArray;        /* constraints converted to LTL */
1709  int               f;
1710  boolean           fairness  = (constraintArray != NIL(array_t));
1711
1712  BmcCheckForTermination_t *terminationStatus = 0;
1713  Bmc_PropertyStatus       formulaStatus;
1714  int                      bmcStatus=0; /* Holds the status of running BMC
1715                                           = -1 if there is an error */
1716 
1717  /* ************** */
1718  /* Initialization */
1719  /* ************** */
1720  startTime = util_cpu_ctime();
1721  /*
1722    nodeToMvfAigTable maps each node to its multi-function And/Inv graph
1723  */
1724  nodeToMvfAigTable =
1725    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
1726  assert(nodeToMvfAigTable != NIL(st_table));
1727
1728  loopClause = NIL(array_t);
1729  noLoopIndex = 0;
1730  ltlConstraintArray = NIL(array_t);
1731  if(fairness){
1732    Ctlsp_Formula_t *formula;
1733    int              i;
1734    /*
1735      All formulae in constraintArray are propositional, propositional
1736      constraint.
1737    */
1738    ltlConstraintArray = array_alloc(Ctlsp_Formula_t *, 0);
1739    arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) {
1740      /*
1741        To help making propositional constraint easy to encode.
1742      */
1743      formula =  Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t));
1744      array_insert(Ctlsp_Formula_t *, ltlConstraintArray, i, formula);
1745      BmcGetCoiForLtlFormula(network, formula, CoiTable);
1746    }
1747  }
1748  /*
1749    For bounded formulae use a tighter upper bound if possible.
1750  */
1751  boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltlFormula, &depth);
1752  if (boundedFormula && depth < maxK && depth >= minK) {
1753    maxK = depth;
1754  } else {
1755    if(options->inductiveStep !=0){
1756      /*
1757        Use the termination criteria to prove the property passes.   
1758      */
1759      terminationStatus = BmcAutTerminationAlloc(network,
1760                                                 Ctlsp_LtllFormulaNegate(ltlFormula),
1761                                                 constraintArray);
1762      assert(terminationStatus);
1763    }
1764  }
1765  if (options->verbosityLevel != BmcVerbosityNone_c){
1766    (void) fprintf(vis_stdout, "General LTL BMC\n");
1767    if (boundedFormula){
1768      (void) fprintf(vis_stdout, "Bounded formula of depth %d\n", depth);
1769    }
1770    (void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
1771                  minK, maxK, options->step);
1772  }
1773  k= minK;
1774  formulaStatus = BmcPropertyUndecided_c;
1775  while( (result == NIL(array_t)) && (k <= maxK)){
1776    if (options->verbosityLevel == BmcVerbosityMax_c) {
1777      (void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
1778    }
1779
1780    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
1781    if (cnfFile == NIL(FILE)) {
1782      (void)fprintf(vis_stderr,
1783                    "** bmc error: Cannot create CNF output file %s\n",
1784                    options->satInFile);
1785      bmcStatus = -1;
1786      break;
1787    }
1788    /*
1789      Create a clause database
1790     */
1791    cnfClauses = BmcCnfClausesAlloc();
1792    /*
1793      Gnerate clauses for an initialized path of length k
1794     */
1795    BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
1796                                 cnfClauses, nodeToMvfAigTable, CoiTable);
1797
1798    if(!fairness){ /* No fairness constraint */
1799      noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
1800      leftValue   = checkIndex(noLoopIndex, cnfClauses);
1801    } else {
1802      leftValue = 0; /* the path must have a loop*/
1803    }
1804    if (leftValue != 1) {
1805      orClause = array_alloc(int, 0);   
1806      /*
1807        No need to check for !Lk in the basic encoding
1808      */
1809      if (leftValue == -1){
1810        array_insert_last(int, orClause, noLoopIndex);
1811      }
1812      loopClause = array_alloc(int, k+1);
1813     
1814      for(l=0; l<=k; l++){
1815        loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, l, cnfClauses);
1816        rightValue = checkIndex(loopIndex, cnfClauses);
1817        if (rightValue == 0){
1818          break;
[38]1819         }
[14]1820        if(fairness){
1821          Ctlsp_Formula_t *formula;
1822          int             i;
1823
1824          fairnessArray = array_alloc(int, 0);
1825          arrayForEachItem(Ctlsp_Formula_t *, ltlConstraintArray, i, formula) {
1826            array_insert_last(int, fairnessArray,
1827                              BmcGenerateCnfForLtl(network, formula, l, k, -1, cnfClauses));
1828          }
1829        }
1830        if (rightValue !=0){
1831          loop = cnfClauses->cnfGlobalIndex++;
1832          BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses,
1833                                                nodeToMvfAigTable, CoiTable, loop);
1834          array_insert(int, loopClause, l, loop);
1835          if(rightValue == -1){
1836           
1837            andIndex   = cnfClauses->cnfGlobalIndex++;
1838            tmpclause  = array_alloc(int, 2);
1839            array_insert(int, tmpclause, 0, loop);
1840            array_insert(int, tmpclause, 1, -andIndex);
1841            BmcCnfInsertClause(cnfClauses, tmpclause);
1842
1843            array_insert(int, tmpclause, 0, loopIndex);
1844            array_insert(int, tmpclause, 1, -andIndex);
1845            BmcCnfInsertClause(cnfClauses, tmpclause);
1846           
1847            if(fairness){
1848              for(f=0; f < array_n(fairnessArray); f++){
1849                array_insert(int, tmpclause, 0, array_fetch(int, fairnessArray, f)); 
1850                array_insert(int, tmpclause, 1, -andIndex);
1851                BmcCnfInsertClause(cnfClauses, tmpclause);
1852              }
1853            }
1854            array_free(tmpclause);
1855            array_insert_last(int, orClause, andIndex);
1856          } else {
1857            array_insert_last(int, orClause, loop);
1858          }
1859        }
1860        if(fairness){
1861          array_free(fairnessArray);
1862        }
1863      } /* for l loop */
1864    }
1865    if((leftValue == 1) || (rightValue == 1)){
1866      assert(k==1);
1867      if (options->verbosityLevel != BmcVerbosityNone_c){
1868        formulaStatus = BmcPropertyFailed_c;
1869        (void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
1870      }
1871      break;
1872    } else if((leftValue == 0) && (rightValue == 0)){
1873      if (options->verbosityLevel != BmcVerbosityNone_c){
1874        (void) fprintf(vis_stdout,"# BMC: the formula is trivially true");
1875        (void) fprintf(vis_stdout," for counterexamples of length %d\n", k);
1876      }
1877    } else {
1878      /*
1879      BmcCnfInsertClause(cnfClauses, loopClause);
1880      */
1881      BmcCnfInsertClause(cnfClauses, orClause);
1882      /*
1883      array_free(loopClause);
1884      */
1885      array_free(orClause);
1886      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1887      (void) fclose(cnfFile);
1888     
1889      result = BmcCheckSAT(options);
1890      if(options->satSolverError){
1891        break;
1892      }
1893      if(result != NIL(array_t)) {
1894        /*
1895          formula failed\n"
1896         */
1897        formulaStatus = BmcPropertyFailed_c;
1898        break;
1899      }
1900      array_free(loopClause);
1901    }
1902    /* free all used memories */
1903    BmcCnfClausesFree(cnfClauses);
1904    cnfClauses = NIL(BmcCnfClauses_t);
1905   
1906    /*
1907      Use the termination check if the the LTL formula is not bounded
1908     */
1909    if(terminationStatus && (formulaStatus == BmcPropertyUndecided_c) && (bmcStatus != 1)){
1910      if((options->inductiveStep !=0) &&
1911         (k % options->inductiveStep == 0)
1912         )
1913        {
1914          /*
1915            Check for termination for the current value of k.
1916           */
1917          terminationStatus->k = k;
1918          bmcStatus = BmcAutLtlCheckForTermination(network,
1919                                                   constraintArray, terminationStatus,
1920                                                   nodeToMvfAigTable, CoiTable, options);
1921          if(bmcStatus == 1){
1922            maxK = terminationStatus->k;
1923          }
1924          if(bmcStatus == 3){
1925            formulaStatus = BmcPropertyPassed_c;
1926            break;
1927          }
1928          if(bmcStatus == -1){
1929            break;
1930          }
1931        }
1932    } /* terminationStatus */
1933    k += options->step;
1934  } /* while result and k*/
1935
1936  /*
1937    If no error.
1938   */
1939  if(bmcStatus != -1){
1940    /*
1941    if(result == NIL(array_t)){
1942    */
1943    if(formulaStatus == BmcPropertyUndecided_c){
1944      if(bmcStatus == 1){
1945        (void) fprintf(vis_stdout,
1946                       "# BMC: no counterexample found of length up to %d \n", maxK);
1947        (void) fprintf(vis_stdout, "# BMC: By termination criterion (m+n-1)\n");
1948        formulaStatus = BmcPropertyPassed_c;
1949      }
1950      if (boundedFormula && depth <= options->maxK){
1951        (void) fprintf(vis_stdout,
1952                       "# BMC: no counterexample found of length up to %d \n", depth);
1953        formulaStatus = BmcPropertyPassed_c;
1954      }
1955    }
1956    if(options->satSolverError){
1957      (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
1958    } else {
1959      if(formulaStatus == BmcPropertyFailed_c) {
1960        (void) fprintf(vis_stdout, "# BMC: formula failed\n");
1961        if(options->verbosityLevel != BmcVerbosityNone_c){
1962          (void) fprintf(vis_stdout,
1963                         "# BMC: Found a counterexample of length = %d \n", k);
1964        }
1965        if ((options->dbgLevel == 1) && (result != NIL(array_t))) {
1966          BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
1967                                 result, k, CoiTable, options, loopClause);
1968        }
1969        /*BmcCnfClausesFree(cnfClauses);*/
1970        array_free(loopClause);
1971      } else if(formulaStatus == BmcPropertyPassed_c) {
1972        (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
1973        (void) fprintf(vis_stdout, "#      Termination depth = %d\n", maxK);
1974      } else if(formulaStatus == BmcPropertyUndecided_c) {
1975        (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
1976        if (options->verbosityLevel != BmcVerbosityNone_c){
1977          (void) fprintf(vis_stdout,
1978                         "# BMC: no counterexample found of length up to %d \n",
1979                         maxK);
1980        }
1981      }
1982    }
1983  }
1984  if (options->verbosityLevel != BmcVerbosityNone_c) {
1985    endTime = util_cpu_ctime();
1986    fprintf(vis_stdout, "-- bmc time = %10g\n",
1987            (double)(endTime - startTime) / 1000.0);
1988  }
1989  /*
1990    free all used memories
1991  */
1992  if(terminationStatus){
1993    BmcAutTerminationFree(terminationStatus);
1994  }
1995  if(result != NIL(array_t)){
1996    array_free(result);
1997  }
1998  if(cnfClauses != NIL(BmcCnfClauses_t)){
1999    BmcCnfClausesFree(cnfClauses);
2000  }
2001  if(fairness){
2002    /*Ctlsp_FormulaArrayFree(ltlConstraintArray);*/
2003  }
2004  fflush(vis_stdout);
2005  return;
2006} /* BmcLtlVerifyGeneralLtl() */
2007
2008/**Function********************************************************************
2009
2010  Synopsis    [Generate CNF for an LTL formula]
2011
2012  Description [Generate array of clauses for a trnasition from state i to
2013              state k. If l is non-zero, it will also generate the clauses
2014              from state l to state i.
2015             
2016              if the clause array is empty {}, the propety is always TRUE
2017              if the the clause array has one empty clause {{}}, the property
2018              is always FALSE.
2019              return the clause index number.
2020  ]
2021
2022  SideEffects []
2023
2024  SeeAlso     []
2025
2026******************************************************************************/
2027int
2028BmcGenerateCnfForLtl(
2029   Ntk_Network_t   *network,
2030   Ctlsp_Formula_t *ltlFormula,
2031   int             i /* from state i */,
2032   int             k /* to state k   */,
2033   int             l /* loop         */,
2034   BmcCnfClauses_t *cnfClauses)
2035{
2036  int left, right, cnfIndex;
2037  int andIndex, orIndex;
2038  int j, n;
2039  int leftValue, rightValue, andValue, orValue;
2040 
2041  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
2042  array_t         *clause, *tmpclause, *orClause, *rightClause, *leftClause;
2043  BmcCnfStates_t  *state;
2044 
2045  assert(ltlFormula != NIL(Ctlsp_Formula_t));
2046  right = 0;
2047  rightValue = 0;
2048 
2049  if(Ctlsp_isPropositionalFormula(ltlFormula)){
2050    bAigEdge_t property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula);
2051       
2052    if (property == bAig_Zero){ /* FALSE */
2053      /* add an empty clause to indicate FALSE property */
2054      BmcAddEmptyClause(cnfClauses);
2055      return 0;
2056    }
2057    if (property == bAig_One){ /* TRUE */
2058      /* Don't generate any clause to indicate TRUE property.*/
2059      return 0;
2060    }
2061    /* Generate the clause of the propositional formula */
2062    /* The state of the input variables is the same as the state of the state variables. */
2063    cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, i, cnfClauses);   
2064    return cnfIndex;
2065  }
2066  /*
2067   * Formula is NOT propositional formula
2068   */
2069  switch(ltlFormula->type) {
2070    case Ctlsp_NOT_c:
2071      /* reach here if formula-left is always not propositional*/
2072      /* NOT must only appears infront of a propositional formula.*/
2073      if (!Ctlsp_isPropositionalFormula(ltlFormula->left)){
2074        fprintf(vis_stderr,"BMC error: the LTL formula is not in NNF\n");
2075        return 0;
2076      }
2077      /*
2078      return -1*BmcGenerateCnfForLtlNoLoop(network, ltlFormula->left, i, k,
2079                                           cnfIndexTable, clauseArray);
2080      */
2081      break;
2082    case Ctlsp_AND_c:
2083      /*
2084          c = a * b  -->  (!a + !b + c) * (a + !c) * (b + !c).
2085          Because a and b must be one, so we need only the last two clauses.
2086       */
2087     
2088      state = BmcCnfClausesFreeze(cnfClauses);
2089      rightValue = 1;
2090     
2091      left      = BmcGenerateCnfForLtl(network, ltlFormula->left,  i, k, l, cnfClauses);
2092      leftValue = checkIndex(left, cnfClauses);
2093
2094      if (leftValue !=0){
2095        right      = BmcGenerateCnfForLtl(network, ltlFormula->right, i, k, l, cnfClauses);
2096        rightValue = checkIndex(right, cnfClauses);
2097      }
2098      if ((leftValue == 0) || (rightValue == 0)){
2099        /* restore the information */
2100        BmcCnfClausesRestore(cnfClauses, state);
2101        /* add an empty clause*/
2102        BmcAddEmptyClause(cnfClauses);
2103        FREE(state);
2104        return 0;  /* FALSE */
2105      }
2106      if ((leftValue == 1) && (rightValue == 1)){
2107        /* restore the information */
2108        BmcCnfClausesRestore(cnfClauses, state);
2109        FREE(state);
2110        return 0; /* TRUE */
2111      }
2112      BmcCnfClausesUnFreeze(cnfClauses, state);
2113      FREE(state);
2114      /*
2115      tmpclause  = array_alloc(int, 3);
2116      array_insert(int, tmpclause, 0, -left);
2117      array_insert(int, tmpclause, 1, -right);
2118      array_insert(int, tmpclause, 2,  cnfIndex);
2119      array_insert_last(array_t *, clauseArray, tmpclause);
2120      */
2121      if (leftValue == 1){
2122        return right;
2123      }
2124      if (rightValue == 1){
2125        return left;
2126      }
2127      cnfIndex = cnfClauses->cnfGlobalIndex++;     
2128      tmpclause  = array_alloc(int, 2);
2129     
2130      array_insert(int, tmpclause, 0, left);
2131      array_insert(int, tmpclause, 1, -cnfIndex);
2132      BmcCnfInsertClause(cnfClauses, tmpclause);
2133     
2134      array_insert(int, tmpclause, 0, right);
2135      array_insert(int, tmpclause, 1, -cnfIndex);
2136      BmcCnfInsertClause(cnfClauses, tmpclause);
2137      array_free(tmpclause);
2138
2139      return cnfIndex;
2140    case Ctlsp_OR_c:
2141      /*
2142          c = a + b  -->  (a + b + !c) * (!a + c) * (!b + c).
2143          Because a and b must be one, so we need only the first clause.
2144       */
2145      state = BmcCnfClausesFreeze(cnfClauses);
2146           
2147      left      = BmcGenerateCnfForLtl(network, ltlFormula->left,  i, k, l, cnfClauses);
2148      leftValue = checkIndex(left, cnfClauses);
2149
2150      if (leftValue !=1){
2151        right      = BmcGenerateCnfForLtl(network, ltlFormula->right, i, k, l, cnfClauses);
2152        rightValue = checkIndex(right, cnfClauses);
2153      }
2154      if ((leftValue == 1) || (rightValue == 1)){
2155        /* restore the information */
2156        BmcCnfClausesRestore(cnfClauses, state);
2157        FREE(state);
2158        return 0;  /* TRUE */
2159      } 
2160      if ((leftValue == 0) && (rightValue == 0)){
2161        /* restore the information */
2162        BmcCnfClausesRestore(cnfClauses, state);
2163        /* add an empty clause*/
2164        BmcAddEmptyClause(cnfClauses);
2165        FREE(state);
2166        return 0;  /* FALSE */
2167      }
2168      BmcCnfClausesUnFreeze(cnfClauses, state);
2169      FREE(state);
2170      /* Either leftValue or rightValue = 0 and the other != 1
2171         At least one clause will be added
2172       */
2173      if (leftValue == 0){
2174        return right;
2175      }
2176      if (rightValue == 0){
2177        return left;
2178      }     
2179      cnfIndex = cnfClauses->cnfGlobalIndex++;
2180
2181      tmpclause  = array_alloc(int, 0);
2182      array_insert_last(int, tmpclause, -cnfIndex);
2183     
2184      array_insert_last(int, tmpclause, left);
2185        /*
2186        tmpclause  = array_alloc(int, 2);
2187        array_insert(int, tmpclause, 0, -left);
2188        array_insert(int, tmpclause, 1, cnfIndex);
2189        array_insert_last(array_t *, clauseArray, tmpclause);
2190        */
2191      array_insert_last(int, tmpclause, right);
2192        /*
2193        tmpclause  = array_alloc(int, 2);
2194        array_insert(int, tmpclause, 0, -right);
2195        array_insert(int, tmpclause, 1, cnfIndex);
2196        array_insert_last(array_t *, clauseArray, tmpclause);
2197        */
2198      BmcCnfInsertClause(cnfClauses, tmpclause);
2199      array_free(tmpclause);
2200     
2201      return cnfIndex;
2202    case Ctlsp_F_c:
2203      if (l >= 0){ /* loop */
2204        i = (l < i)? l: i;
2205      }
2206      cnfIndex = cnfClauses->cnfGlobalIndex++;
2207      clause   = array_alloc(int, 0);
2208      for (j=i; j<= k; j++){
2209        left      = BmcGenerateCnfForLtl(network, ltlFormula->left, j, k, l, cnfClauses);
2210        leftValue = checkIndex(left, cnfClauses);
2211        if (leftValue != -1){
2212          array_free(clause);
2213          return 0;
2214        }
2215        array_insert_last(int, clause, left);
2216          /*
2217          tmpclause  = array_alloc(int, 2);
2218          array_insert(int, tmpclause, 1, cnfIndex);
2219          array_insert(int, tmpclause, 0, -left);
2220          array_insert_last(array_t *, clauseArray, tmpclause);
2221          */
2222      }
2223      array_insert_last(int, clause, -cnfIndex);
2224      BmcCnfInsertClause(cnfClauses, clause);
2225      array_free(clause);
2226 
2227      return cnfIndex;
2228    case Ctlsp_G_c:
2229      if (l < 0){ /* FALSE */
2230        /* add an empty clause */
2231        BmcAddEmptyClause(cnfClauses);
2232        return 0;
2233      } else {
2234       i = (l < i)? l: i;
2235       andIndex = cnfClauses->cnfGlobalIndex++;
2236       for (j=i; j<= k; j++){
2237         left      = BmcGenerateCnfForLtl(network, ltlFormula->left, j, k, l, cnfClauses);
2238         leftValue = checkIndex(left, cnfClauses);
2239         if (leftValue != -1){
2240           return 0;
2241         }
2242         tmpclause  = array_alloc(int, 2);
2243         array_insert(int, tmpclause, 0, left);
2244         array_insert(int, tmpclause, 1, -andIndex);
2245         BmcCnfInsertClause(cnfClauses, tmpclause);
2246         array_free(tmpclause);
2247       }/* for j loop*/
2248      } /* else */
2249      return andIndex;
2250    case Ctlsp_X_c:
2251      /* X left */
2252      if((l >= 0) && (i == k) ){
2253        i = l;
2254      } else if (i < k){
2255        i = i + 1;
2256      } else { /* FALSE */
2257        /* add an empty clause */
2258        BmcAddEmptyClause(cnfClauses);
2259        return 0;
2260      }
2261      return BmcGenerateCnfForLtl(network, ltlFormula->left, i, k, l, cnfClauses);
2262    case Ctlsp_U_c: /* (left U right) */
2263      state = BmcCnfClausesFreeze(cnfClauses);
2264     
2265      leftValue  = 1; /* left is TRUE*/
2266      rightValue = 1; /* right is TRUE*/
2267      orIndex    = cnfClauses->cnfGlobalIndex++;
2268      orClause   = array_alloc(int, 0);
2269      array_insert_last(int, orClause, -orIndex);
2270
2271      orValue = 0;
2272      for (j=i; j<= k; j++){
2273        right = BmcGenerateCnfForLtl(network, ltlFormula->right, j, k, l, cnfClauses);
2274        rightValue = checkIndex(right, cnfClauses);
2275        andIndex   = cnfClauses->cnfGlobalIndex++;
2276        if (rightValue == -1){
2277          rightClause  = array_alloc(int, 2);
2278          array_insert(int, rightClause, 0, right);
2279          array_insert(int, rightClause, 1, -andIndex);
2280          BmcCnfInsertClause(cnfClauses, rightClause);
2281          array_free(rightClause);
2282        }
2283        andValue = rightValue;
2284        for (n=i; (n <= j-1) && (andValue != 0); n++){
2285          left = BmcGenerateCnfForLtl(network, ltlFormula->left, n, k, l, cnfClauses);
2286          leftValue = checkIndex(left, cnfClauses);
2287          andValue  = doAnd(andValue, leftValue);
2288          if (leftValue == -1){
2289            leftClause  = array_alloc(int, 2);
2290            array_insert(int, leftClause, 0, left);
2291            array_insert(int, leftClause, 1, -andIndex);
2292            BmcCnfInsertClause(cnfClauses, leftClause);
2293            array_free(leftClause);
2294          }
2295        } /* for n loop */
2296        orValue = doOr(orValue, andValue);
2297        if (orValue == 1){ /* TRUE */
2298          break;
2299        }
2300        if (andValue != 0){
2301          array_insert_last(int, orClause, andIndex);
2302        }
2303      } /* for j loop*/
2304      if ( (l >=0) && (orValue !=1)){ /* loop */
2305        for (j=l; j<= i-1; j++){
2306          right = BmcGenerateCnfForLtl(network, ltlFormula->right, j, k, l, cnfClauses);
2307          rightValue = checkIndex(right, cnfClauses);
2308          andIndex   = cnfClauses->cnfGlobalIndex++;
2309          if (rightValue == -1){
2310            rightClause  = array_alloc(int, 2);
2311            array_insert(int, rightClause, 0, right);
2312            array_insert(int, rightClause, 1, -andIndex);
2313            BmcCnfInsertClause(cnfClauses, rightClause);
2314            array_free(rightClause);
2315          }
2316          andValue = rightValue; 
2317          for (n=i; (n<= k) && (andValue != 0); n++){
2318            left = BmcGenerateCnfForLtl(network, ltlFormula->left, n, k, l, cnfClauses);
2319            leftValue = checkIndex(left, cnfClauses);
2320            andValue  = doAnd(andValue, leftValue);
2321            if (leftValue == -1){
2322              leftClause  = array_alloc(int, 2);
2323              array_insert(int, leftClause, 0, left);
2324              array_insert(int, leftClause, 1, -andIndex);
2325              BmcCnfInsertClause(cnfClauses, leftClause);
2326              array_free(leftClause);
2327            }
2328          } /* for n loop */
2329          for (n=l; (n<= j-1)  && (andValue != 0); n++){
2330            left = BmcGenerateCnfForLtl(network, ltlFormula->left, n, k, l, cnfClauses);
2331            leftValue = checkIndex(left, cnfClauses);
2332            andValue  = doAnd(andValue, leftValue);
2333            if (leftValue == -1){
2334              leftClause  = array_alloc(int, 2);
2335              array_insert(int, leftClause, 0, left);
2336              array_insert(int, leftClause, 1, -andIndex);
2337              BmcCnfInsertClause(cnfClauses, leftClause);
2338              array_free(leftClause);
2339            }
2340          } /* for n loop */
2341          orValue = doOr(orValue, andValue);
2342          if (orValue == 1){ /* TRUE */
2343            break;
2344          }
2345          if (andValue != 0){
2346            array_insert_last(int, orClause, andIndex);
2347          }
2348        }/* j loop*/
2349      } /* if (l>=0) */
2350      if ((orValue == 1) || (orValue == 0)){
2351        /*restore the infomration back*/
2352        BmcCnfClausesRestore(cnfClauses, state);
2353        FREE(state);
2354        array_free(orClause);
2355        if (orValue == 0){
2356          /* add an empty clause*/
2357          BmcAddEmptyClause(cnfClauses);
2358        }
2359        return 0;
2360      } else {
2361        BmcCnfClausesUnFreeze(cnfClauses, state);
2362        FREE(state);
2363        BmcCnfInsertClause(cnfClauses, orClause);
2364        array_free(orClause);
2365        return orIndex;
2366      }
2367    case Ctlsp_R_c:
2368      /* (left R right) */
2369      state = BmcCnfClausesFreeze(cnfClauses);
2370     
2371      orIndex  = cnfClauses->cnfGlobalIndex++;
2372      orClause = array_alloc(int, 0);
2373      array_insert_last(int, orClause, -orIndex);
2374     
2375      orValue = 0;
2376      if (l >= 0){ /* loop */
2377        andIndex = cnfClauses->cnfGlobalIndex++;
2378        andValue = 1;
2379        for (j=(i<l?i:l); (j<= k) && (andValue != 0); j++){
2380          right = BmcGenerateCnfForLtl(network, ltlFormula->right, j, k, l, cnfClauses);
2381          rightValue = checkIndex(right, cnfClauses);
2382          andValue  = doAnd(andValue, rightValue);
2383          if (rightValue == -1){
2384            rightClause  = array_alloc(int, 2);
2385            array_insert(int, rightClause, 0, right);
2386            array_insert(int, rightClause, 1, -andIndex);
2387            BmcCnfInsertClause(cnfClauses, rightClause);
2388            array_free(rightClause);
2389          }
2390        } /* for j loop*/
2391        if (andValue == -1){
2392          array_insert_last(int, orClause, andIndex);
2393        }
2394        orValue = doOr(orValue, andValue);
2395      } /* loop */
2396      if(orValue != 1){
2397        for (j=i; j<= k; j++){
2398          left = BmcGenerateCnfForLtl(network, ltlFormula->left,
2399                                      j, k, l, cnfClauses);
2400          leftValue = checkIndex(left, cnfClauses);
2401          andIndex = cnfClauses->cnfGlobalIndex++;
2402          if (leftValue == -1){
2403            leftClause  = array_alloc(int, 2);
2404            array_insert(int, leftClause, 0, left);
2405            array_insert(int, leftClause, 1, -andIndex);
2406            BmcCnfInsertClause(cnfClauses, leftClause);
2407            array_free(leftClause);
2408          }
2409          andValue = leftValue;
2410          for (n=i; (n<= j) && (andValue != 0); n++){
2411            right = BmcGenerateCnfForLtl(network, ltlFormula->right,
2412                                         n, k, l, cnfClauses);
2413            rightValue = checkIndex(right, cnfClauses);
2414            andValue   = doAnd(andValue, rightValue);
2415            if (rightValue == -1){
2416              rightClause  = array_alloc(int, 2);
2417              array_insert(int, rightClause, 0, right);
2418              array_insert(int, rightClause, 1, -andIndex);
2419              BmcCnfInsertClause(cnfClauses, rightClause);
2420              array_free(rightClause);
2421            }
2422          } /* for n loop */
2423          orValue = doOr(orValue, andValue);
2424          if (orValue == 1){ /* TRUE */
2425            break;
2426          }
2427          if (andValue != 0){
2428            array_insert_last(int, orClause, andIndex);
2429          }
2430        }/* for j loop*/
2431        if ((l >= 0)  && (orValue !=1)) { /* loop */
2432          for (j=l; j<= i-1; j++){
2433            left = BmcGenerateCnfForLtl(network, ltlFormula->left,
2434                                        j, k, l, cnfClauses);
2435            leftValue = checkIndex(left, cnfClauses);
2436            andIndex = cnfClauses->cnfGlobalIndex++;
2437            if (leftValue == -1){
2438              leftClause  = array_alloc(int, 2);
2439              array_insert(int, leftClause, 0, left);
2440              array_insert(int, leftClause, 1, -andIndex);
2441              BmcCnfInsertClause(cnfClauses, leftClause);
2442              array_free(leftClause);
2443            }
2444            andValue = leftValue;
2445            for (n=i; (n<= k)  && (andValue != 0); n++){
2446              right = BmcGenerateCnfForLtl(network, ltlFormula->right,
2447                                           n, k, l, cnfClauses);
2448              rightValue = checkIndex(right, cnfClauses);
2449              andValue = doAnd(andValue, rightValue);
2450              if (rightValue == -1){
2451                rightClause  = array_alloc(int, 2);
2452                array_insert(int, rightClause, 0, right);
2453                array_insert(int, rightClause, 1, -andIndex);
2454                BmcCnfInsertClause(cnfClauses, rightClause);
2455                array_free(rightClause);
2456              }
2457            } /* for n loop */
2458            for (n=l; (n<= j) && (andValue != 0); n++){
2459              right = BmcGenerateCnfForLtl(network, ltlFormula->right,
2460                                           n, k, l, cnfClauses);
2461              rightValue = checkIndex(right, cnfClauses);
2462              andValue = doAnd(andValue, rightValue);
2463              if (rightValue == -1){
2464                rightClause  = array_alloc(int, 2);
2465                array_insert(int, rightClause, 0, right);
2466                array_insert(int, rightClause, 1, -andIndex);
2467                BmcCnfInsertClause(cnfClauses, rightClause);
2468                array_free(rightClause);
2469              }
2470            } /* for n loop */
2471            orValue = doOr(orValue, andValue);
2472            if (orValue == 1){ /* TRUE */
2473              break;
2474            }
2475            if (andValue != 0){
2476              array_insert_last(int, orClause, andIndex);
2477            }
2478          } /* for j loop*/
2479        } /* if (l>=0) */
2480      }/* orValue !=1*/
2481      if ((orValue == 1) || (orValue == 0)){
2482        /*restore the infomration back*/
2483        BmcCnfClausesRestore(cnfClauses, state);
2484        FREE(state);
2485        array_free(orClause);
2486        if (orValue == 0){
2487          /* add an empty clause*/
2488          BmcAddEmptyClause(cnfClauses);
2489        }
2490        return 0;
2491      } else {
2492        BmcCnfClausesUnFreeze(cnfClauses, state);
2493        FREE(state);
2494        BmcCnfInsertClause(cnfClauses, orClause);
2495        array_free(orClause);
2496        return orIndex;
2497      }
2498    default:
2499      fail("Unexpected LTL formula type");
2500      break;
2501  }
2502  return -1; /* we should never get here */
2503}
2504/*  BmcLTLFormulaNoLoopTranslation() */
2505
2506
2507/**Function********************************************************************
2508
2509  Synopsis    [Apply bmc on an abbreviation-free LTL formula that expresses
2510  safety propery]
2511
2512  Description [If an LTL formula expresses a safety property, we generate CNF
2513                                        0
2514  caluse for the part with no loop: [[f]]
2515                                        k
2516  ]
2517
2518  SideEffects []
2519
2520  SeeAlso     []
2521
2522******************************************************************************/
2523void
2524BmcLtlCheckSafety(
2525   Ntk_Network_t   *network,
2526   Ctlsp_Formula_t *ltlFormula,
2527   BmcOption_t     *options,
2528   st_table        *CoiTable)
2529{
2530  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
2531  st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
2532  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
2533  FILE              *cnfFile;
2534  int               noLoopIndex;
2535  array_t           *result = NIL(array_t);
2536  int               leftValue  = 0;
2537  long              startTime, endTime;
2538  int               k;
2539  int               minK = options->minK;
2540  int               maxK = options->maxK;
2541  boolean           boundedFormula;
2542  int               depth;
2543  array_t           *unitClause =  array_alloc(int, 1);
2544 
2545  array_t           *orClause =  array_alloc(int, 2);
2546
2547  /* ************** */
2548  /* Initialization */
2549  /* ************** */
2550  startTime = util_cpu_ctime();
2551  /* nodeToMvfAigTable maps each node to its multi-function And/Inv graph */
2552  nodeToMvfAigTable =
2553    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
2554  assert(nodeToMvfAigTable != NIL(st_table));
2555
2556  /* For bounded formulae use a tighter upper bound if possible. */
2557  boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltlFormula, &depth);
2558  if (boundedFormula && depth < maxK && depth >= minK) {
2559    maxK = depth;
2560  }
2561  if (options->verbosityLevel != BmcVerbosityNone_c){
2562    (void) fprintf(vis_stdout, "saftey LTL BMC\n");
2563    if (boundedFormula){
2564      (void) fprintf(vis_stdout, "Bounded formula of depth %d\n", depth);
2565    }
2566    (void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
2567                  minK, maxK, options->step);
2568  }
2569  k= minK;
2570  while( (result == NIL(array_t)) && (k <= maxK)){
2571    if (options->verbosityLevel == BmcVerbosityMax_c) {
2572      (void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
2573    }
2574    cnfClauses = BmcCnfClausesAlloc();
2575    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
2576    if (cnfFile == NIL(FILE)) {
2577      (void)fprintf(vis_stderr,
2578                    "** bmc error: Cannot create CNF output file %s\n",
2579                    options->satInFile);
2580      return;
2581    }
2582    BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
2583                                 cnfClauses, nodeToMvfAigTable, CoiTable);
2584    noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
2585    leftValue   = checkIndex(noLoopIndex, cnfClauses);
2586
2587    if(leftValue == 1){
2588      assert(k==1);
2589      if (options->verbosityLevel != BmcVerbosityNone_c){
2590        (void) fprintf(vis_stdout,"# BMC: formula failed\n");
2591        (void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
2592      }
2593      break;
2594    } else if(leftValue == 0){
2595      if (options->verbosityLevel != BmcVerbosityNone_c){
2596        (void) fprintf(vis_stdout,"# BMC: the formula is trivially true");
2597        (void) fprintf(vis_stdout," for counterexamples of length %d\n", k);
2598      }
2599      /*
2600      break;
2601      */
2602    } else {
2603      array_insert(int, unitClause, 0, noLoopIndex);
2604     
2605      BmcCnfInsertClause(cnfClauses, unitClause);
2606     
2607      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
2608      (void) fclose(cnfFile);
2609      result = BmcCheckSAT(options);
2610      if (options->satSolverError){
2611        break;
2612      }
2613      if(result != NIL(array_t)) {
2614        (void) fprintf(vis_stdout, "# BMC: formula failed\n");
2615        if(options->verbosityLevel != BmcVerbosityNone_c){
2616          (void) fprintf(vis_stdout,
2617                         "# BMC: Found a counterexample of length = %d \n", k);
2618        }
2619        if (options->dbgLevel == 1) {
2620          BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
2621                                 result, k, CoiTable, options, NIL(array_t));
2622        }
2623        break;
2624      }
2625    }
2626    /* free all used memories */
2627    BmcCnfClausesFree(cnfClauses);
2628#if 0
2629
2630    /*
2631      Check induction
2632     */
2633    {
2634      BmcCnfClauses_t   *noLoopCnfClauses = BmcCnfClausesAlloc();
2635      array_t           *noLoopResult = NIL(array_t);
2636      array_t           *unitClause =  array_alloc(int, 1);
2637      int               i;
2638
2639      printf("Check Induction \n");
2640
2641      cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
2642      if (cnfFile == NIL(FILE)) {
2643        (void)fprintf(vis_stderr,
2644                      "** bmc error: Cannot create CNF output file %s\n",
2645                      options->satInFile);
2646        return;
2647      }
2648      /*
2649        Generate a loop free path
2650      */
2651      BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
2652                                           noLoopCnfClauses, nodeToMvfAigTable, CoiTable);
2653      /*
2654        The property true at states from 0 to k
2655       */
2656      unitClause = array_alloc(int, 1);
2657      for(i=0; i<=k; i++){
2658        array_insert(int, unitClause, 0,
2659                     -BmcGenerateCnfForLtl(network, ltlFormula, i, k, -1, noLoopCnfClauses));
2660        BmcCnfInsertClause(noLoopCnfClauses, unitClause);
2661      }
2662     
2663      /*
2664        The property fails at k +1
2665       */
2666      array_insert(int, unitClause, 0,
2667                   BmcGenerateCnfForLtl(network, ltlFormula, 0, k+1, -1, noLoopCnfClauses));
2668      BmcCnfInsertClause(noLoopCnfClauses, unitClause);
2669      array_free(unitClause);
2670   
2671      BmcWriteClauses(manager, cnfFile, noLoopCnfClauses, options);
2672      (void) fclose(cnfFile);
2673      noLoopResult = BmcCheckSAT(options);
2674      if(noLoopResult == NIL(array_t)) {
2675        (void) fprintf(vis_stdout, "# BMC: formula passed\n");
2676        (void) fprintf(vis_stdout,
2677                       "# BMC: No more loop free path \n");
2678       
2679        break;
2680      }
2681      /*
2682        BmcPrintCounterExample(network, nodeToMvfAigTable, noLoopCnfClauses,
2683        noLoopResult, bound+1, CoiTable, options, NIL(array_t));
2684      */
2685      BmcCnfClausesFree(noLoopCnfClauses);
2686    } /* Check induction */
2687 
2688#endif
2689    k += options->step;
2690
2691#if 0
2692   
2693    /* Check if reach the depth of the model */
2694    cnfClauses = BmcCnfClausesAlloc();
2695    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
2696    if (cnfFile == NIL(FILE)) {
2697      (void)fprintf(vis_stderr,
2698                    "** bmc error: Cannot create CNF output file %s\n",
2699                    options->satInFile);
2700      return;
2701    }
2702    /*
2703      Generate a loop free path
2704     */
2705    {
2706      BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
2707                                   cnfClauses, nodeToMvfAigTable, CoiTable);
2708      /*
2709        initIndex   = BmcCnfGenerateClausesFromStateToState(network, -1, 0, cnfClauses, nodeToMvfAigTable, CoiTable, -1);
2710        noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
2711       
2712        array_insert(int, orClause, 0, initIndex);
2713        array_insert(int, orClause, 1, -noLoopIndex);
2714       
2715        BmcCnfInsertClause(cnfClauses, orClause);
2716      */
2717      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
2718      (void) fclose(cnfFile);
2719      result = BmcCheckSAT(options);
2720      if(result == NIL(array_t)) {
2721        (void) fprintf(vis_stdout, "# BMC: formula passed\n");
2722        (void) fprintf(vis_stdout,
2723                       "# BMC: No more loop free path \n");
2724       
2725        return;
2726      }
2727      /*
2728        BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
2729        result, k, CoiTable, options, NIL(array_t));
2730      */
2731      result = NIL(array_t);
2732    }
2733    BmcCnfClausesFree(cnfClauses);
2734
2735
2736    /* Check if reach the depth of the model */
2737    cnfClauses = BmcCnfClausesAlloc();
2738    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
2739    if (cnfFile == NIL(FILE)) {
2740      (void)fprintf(vis_stderr,
2741                    "** bmc error: Cannot create CNF output file %s\n",
2742                    options->satInFile);
2743      return;
2744    }
2745    /*
2746      Generate a loop free path
2747     */
2748    {
2749      BmcCnfGenerateClausesForPath(network, 0, k, BMC_NO_INITIAL_STATES,
2750                                   cnfClauses, nodeToMvfAigTable, CoiTable);
2751      /*
2752        initIndex   = BmcCnfGenerateClausesFromStateToState(network, -1, 0, cnfClauses, nodeToMvfAigTable, CoiTable, -1);
2753      */
2754      noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
2755      array_insert(int, unitClause, 0, noLoopIndex);
2756     
2757      BmcCnfInsertClause(cnfClauses, unitClause);
2758      /*
2759        array_insert(int, orClause, 0, initIndex);
2760        array_insert(int, orClause, 1, -noLoopIndex);
2761       
2762        BmcCnfInsertClause(cnfClauses, orClause);
2763      */
2764      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
2765      (void) fclose(cnfFile);
2766      result = BmcCheckSAT(options);
2767      if(result == NIL(array_t)) {
2768        (void) fprintf(vis_stdout, "# BMC: (Bad state) formula passed\n");
2769        (void) fprintf(vis_stdout,
2770                       "# BMC: No more loop free path \n");
2771       
2772        return;
2773      }
2774      /*
2775        BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
2776        result, k, CoiTable, options, NIL(array_t));
2777      */
2778      result = NIL(array_t);
2779    }
2780    BmcCnfClausesFree(cnfClauses);
2781#endif
2782   
2783   
2784  } /* while result and k*/
2785  if (options->satSolverError == FALSE){
2786    if ((result == NIL(array_t)) && (k > maxK)){
2787      if (boundedFormula && depth <= options->maxK){
2788        (void) fprintf(vis_stdout,"# BMC: formula passed\n");
2789      } else {
2790        (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
2791      }
2792      if (options->verbosityLevel != BmcVerbosityNone_c){
2793        (void) fprintf(vis_stdout,
2794                       "# BMC: no counterexample found of length up to %d \n",
2795                       maxK);
2796      }
2797    }
2798  }
2799  /* free all used memories */
2800  if (k == 0){
2801     BmcCnfClausesFree(cnfClauses);
2802  }
2803  if(result != NIL(array_t)){
2804    array_free(result);
2805  }
2806  if (options->verbosityLevel != BmcVerbosityNone_c) {
2807    endTime = util_cpu_ctime();
2808    fprintf(vis_stdout, "-- bmc time = %10g\n",
2809            (double)(endTime - startTime) / 1000.0);
2810  }
2811  array_free(unitClause);
2812  array_free(orClause);
2813  fflush(vis_stdout);
2814  return;
2815} /* BmcLtlCheckSafety() */
2816
2817
2818/*---------------------------------------------------------------------------*/
2819/* Definition of static functions                                            */
2820/*---------------------------------------------------------------------------*/
2821
2822
2823/**Function********************************************************************
2824
2825  Synopsis    [Check if the index of the varaible in CNF is TURE, FALSE, or
2826               none]
2827
2828  Description []
2829
2830  SideEffects []
2831
2832******************************************************************************/
2833static int
2834checkIndex(
2835  int             index,
2836  BmcCnfClauses_t *cnfClauses)
2837{
2838  int     rtnValue = -1; /* it is not TRUE or FALSE*/
2839
2840  if (index == 0){ /* TRUE or FALSE*/
2841    if (cnfClauses->emptyClause){   /* last added clause was empty = FALSE*/
2842      rtnValue = 0; /* FALSE */
2843    } else {
2844      /*
2845        if (cnfClauses->noOfClauses == 0)
2846        rtnValue = 1;
2847        }
2848      */
2849      rtnValue = 1; /* TRUE */
2850    }
2851  }
2852  return rtnValue;
2853}
2854
2855/**Function********************************************************************
2856
2857  Synopsis    []
2858
2859  Description [
2860                0  1  -1
2861               ----------       
2862             0  0  0   0
2863             1  0  1  -1
2864            -1  0  -1 -1
2865
2866  ]
2867
2868  SideEffects []
2869
2870******************************************************************************/
2871static int
2872doAnd(
2873  int left,
2874  int right)
2875{
2876  if ((left == -1) && (right == -1)){
2877    return -1;
2878  }
2879  return (left * right);
2880 
2881} /* doAnd */
2882
2883/**Function********************************************************************
2884
2885  Synopsis    []
2886
2887  Description [
2888                 0   1  -1
2889                -----------
2890             0   0   1  -1
2891             1   1   1  -1
2892            -1  -1  -1  -1
2893
2894  ]
2895
2896  SideEffects []
2897
2898******************************************************************************/
2899static int
2900doOr(
2901  int left,
2902  int right)
2903{
2904  if ((left == -1) || (right == -1)){
2905    return -1;
2906  }
2907  if ((left == 1) || (right == 1)){
2908    return 1;
2909  }
2910  return 0;
2911 
2912} /* doOr */
Note: See TracBrowser for help on using the repository browser.