source: vis_dev/vis-2.3/src/bmc/bmcCirCUs.c @ 17

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

vis2.3
File size: 117.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [bmcCirCUs.c]
4
5  PackageName [bmc]
6
7  Synopsis    [BMC ltl model checker using CirCUs.]
8
9  Author      [HoonSang Jin, Mohammad Awedh]
10
11  Copyright   [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14 
15******************************************************************************/
16
17#include "bmcInt.h"
18#include "sat.h"
19#include "baig.h"
20
21static char rcsid[] UNUSED = "$Id: bmcCirCUs.c,v 1.56 2010/04/09 23:50:57 fabio Exp $";
22
23/*---------------------------------------------------------------------------*/
24/* Constant declarations                                                     */
25/*---------------------------------------------------------------------------*/
26
27/*---------------------------------------------------------------------------*/
28/* Type declarations                                                         */
29/*---------------------------------------------------------------------------*/
30
31/*---------------------------------------------------------------------------*/
32/* Structure declarations                                                    */
33/*---------------------------------------------------------------------------*/
34
35/*---------------------------------------------------------------------------*/
36/* Variable declarations                                                     */
37/*---------------------------------------------------------------------------*/
38
39/**AutomaticStart*************************************************************/
40
41/*---------------------------------------------------------------------------*/
42/* Static function prototypes                                                */
43/*---------------------------------------------------------------------------*/
44
45static int printSatValue(bAig_Manager_t *manager, st_table *nodeToMvfAigTable, st_table *li2index, bAigEdge_t **baigArr, array_t *nodeArr, int bound, int *prevValue);
46static int printSatValueAiger(bAig_Manager_t *manager, st_table *nodeToMvfAigTable, st_table *li2index, bAigEdge_t **baigArr, array_t *nodeArr, int bound, int *prevValue);
47static int StringCheckIsInteger(char *string, int *value);
48static int verifyIfConstant(bAigEdge_t property);
49
50/**AutomaticEnd***************************************************************/
51
52/*---------------------------------------------------------------------------*/
53/* Definition of exported functions                                          */
54/*---------------------------------------------------------------------------*/
55
56/*---------------------------------------------------------------------------*/
57/* Definition of internal functions                                          */
58/*---------------------------------------------------------------------------*/
59
60/**Function********************************************************************
61
62   Synopsis [Apply Bounded Model Checking (BMC) technique on a propositional
63   formula.]
64
65   Description [If the property dos not hold in any initial state, the
66   property holds.
67
68   Note: Before calling this function, the LTL formula must be negated.
69   
70   ]
71
72   SideEffects []
73   
74   SeeAlso     []
75   
76******************************************************************************/
77void
78BmcCirCUsLtlVerifyProp(
79    Ntk_Network_t   *network,
80    Ctlsp_Formula_t *ltl,
81    st_table        *coiTable,
82    BmcOption_t     *options)
83{
84  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
85  st_table          *nodeToMvfAigTable = NIL(st_table);
86  long              startTime, endTime;
87  bAigEdge_t        property;
88  int               satFlag;
89  satInterface_t    *interface;
90  array_t           *objArray;
91
92  assert(Ctlsp_isPropositionalFormula(ltl));
93
94  startTime = util_cpu_ctime();
95  if (options->verbosityLevel >= BmcVerbosityNone_c){
96    fprintf(vis_stdout, "LTL formula is propositional\n");
97  }
98  property = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager, ltl);
99  if (property == mAig_NULL){
100    return;
101  }
102  if (verifyIfConstant(property)){
103    if (options->verbosityLevel != BmcVerbosityNone_c){
104      fprintf(vis_stdout, "-- bmc time = %10g\n",
105              (double)(util_cpu_ctime() - startTime) / 1000.0);
106    }
107    return;
108  }
109 
110  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network,
111                                                           MVFAIG_NETWORK_APPL_KEY);
112  assert(nodeToMvfAigTable != NIL(st_table));
113 
114  interface = 0;
115  objArray  = array_alloc(bAigEdge_t, 0);
116  bAig_ExpandTimeFrame(network, manager, 1, BMC_INITIAL_STATES);
117  property = BmcCirCUsCreatebAigOfPropFormula(network, manager,
118                                              0, ltl, BMC_INITIAL_STATES);
119  array_insert(bAigEdge_t, objArray, 0, property);
120  options->cnfPrefix = 0;
121  interface = BmcCirCUsInterfaceWithObjArr(manager, network,
122                                           objArray, NIL(array_t),
123                                           options, interface);
124  satFlag = interface->status;
125  sat_FreeInterface(interface);
126
127  if(satFlag == SAT_SAT) {
128    fprintf(vis_stdout, "# BMC: formula failed\n");
129    if(options->dbgLevel == 1){
130      fprintf(vis_stdout, "# BMC: found a counterexample of length 0\n");
131      BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, 0, 0,
132                                   options, BMC_INITIAL_STATES);
133    }
134    if(options->dbgLevel == 2){
135      fprintf(vis_stdout, "# BMC: found a counterexample of length 0\n");
136      fprintf(vis_stdout, "# The counterexample for Structural Sat problem is incomplete.\n");
137      BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, 0, 0,
138                                   options, BMC_INITIAL_STATES);
139    }
140
141  }
142  else if(satFlag != SAT_SAT) {
143    if(options->verbosityLevel != BmcVerbosityNone_c){
144      fprintf(vis_stdout,"# BMC: no counterexample found of length 0\n");
145    }
146    fprintf(vis_stdout,"# BMC: formula passed\n");
147    (void) fprintf(vis_stdout, "#      Termination depth = 0\n");
148  }
149  if (options->verbosityLevel != BmcVerbosityNone_c){
150    endTime = util_cpu_ctime();
151    fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
152  }
153  array_free(objArray);
154  fflush(vis_stdout);
155  return;
156} /* BmcCirCUsLtlVerifyProp() */
157
158
159/**Function********************************************************************
160
161  Synopsis [Check if the LTL formula in the form G(p) (invariant), p is a
162            propositional formula, is an Inductive Invariant using SAT]
163
164  Description [Check if the LTL formula in the form G(p), p is a
165               propositional formula, is an Inductive Invariant
166
167  An LTL formula G(p), where p is a propositional formula, is an
168  inductive invariant if the following two conditions hold:
169 
170     1- p holds in all intial states.
171     2- If p holds in a state s, then it also holds in all states
172        that are reachable from s.
173
174  G(p) is an inductive invariant if :
175    SAT( I(0) and !p(0)) return UNSAT and
176    SAT( p(i) and T(i, i+1) and !p(i+1)) returns UNSAT.
177
178  Return value:
179    0 if the property is not an inductive invariant
180    1 if the property is an inductive invariant
181   ]
182
183  SideEffects []
184
185  SeeAlso     []
186
187******************************************************************************/
188int
189BmcCirCUsLtlCheckInductiveInvariant(
190  Ntk_Network_t   *network,
191  Ctlsp_Formula_t *ltl,
192  BmcOption_t     *options,
193  st_table        *CoiTable)
194{
195  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
196  bAigEdge_t      property, result;
197  int             satFlag;
198  satInterface_t  *interface;
199  array_t         *objArray   = array_alloc(bAigEdge_t, 1);
200  int             returnValue = 0;  /* the property is not an inductive
201                                       invariant */
202  /*
203    Check if the property holds in all initial states.
204   */
205  interface = 0;
206  bAig_ExpandTimeFrame(network, manager, 1, BMC_INITIAL_STATES);
207  property = BmcCirCUsCreatebAigOfPropFormula(network, manager, 0, ltl->right, BMC_INITIAL_STATES);
208
209  array_insert(bAigEdge_t, objArray, 0, property);
210  options->cnfPrefix = 0;
211  interface = BmcCirCUsInterfaceWithObjArr(manager, network, objArray,
212                                 NIL(array_t), options, interface);
213  satFlag = interface->status;
214  sat_FreeInterface(interface);
215
216  if(satFlag == SAT_UNSAT) {
217    /*
218      Check the induction step.
219    */
220    interface = 0;
221    bAig_ExpandTimeFrame(network, manager, 2, BMC_NO_INITIAL_STATES);
222    property = BmcCirCUsCreatebAigOfPropFormula(network, manager, 0, ltl->right, BMC_NO_INITIAL_STATES);
223    /*
224      The property is true at state 0.  Remember that the passing property is
225      the negation of the original property.
226    */
227    result = bAig_Not(property);
228    property = BmcCirCUsCreatebAigOfPropFormula(network, manager, 1, ltl->right, BMC_NO_INITIAL_STATES);
229    /*
230      The property is false at state 1
231    */
232    result = bAig_And(manager, result, property);
233    array_insert(bAigEdge_t, objArray, 0, result);
234    options->cnfPrefix = 1;
235    interface = BmcCirCUsInterfaceWithObjArr(manager, network, objArray,
236                                   NIL(array_t), options, interface);
237    satFlag = interface->status;
238    sat_FreeInterface(interface);
239    if(satFlag == SAT_UNSAT) {
240      returnValue = 1; /* the property is an inductive invariant */
241     
242    }
243  }
244  array_free(objArray);
245  return returnValue; 
246} /* BmcCirCUsLtlCheckInductiveInvariant */
247
248
249/**Function********************************************************************
250
251   Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of
252   the form G(p), where p is a propositional formula.]
253
254   Description [Given a model M, an LTL formula f = Gp, and a bound k,
255   we first find a counterexample of length k to a state that violates
256   p.  If -r switch of the BMC command is specified, we apply the
257   induction proof to check if the property f passes. The property f
258   passes if there is no simple path in M that leads to a state that
259   violates p, or no simple path in M starting at an initial state.
260
261   Note: Before calling this function, the LTL formula must be negated.
262
263   Using sat as SAT solver.
264   
265   ]
266
267   SideEffects []
268   
269   SeeAlso     []
270   
271******************************************************************************/
272void
273BmcCirCUsLtlVerifyGp(
274    Ntk_Network_t   *network,
275    Ctlsp_Formula_t *ltl,
276    st_table        *coiTable,
277    BmcOption_t     *options)
278{
279  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
280  st_table          *nodeToMvfAigTable = NIL(st_table);
281  long              startTime, endTime;
282  bAigEdge_t        property, result, simplePath;
283  int               j, satFlag, k;
284  int               checkInductiveInvariant;
285  array_t           *objArray;
286  array_t           *auxObjArray;
287  satInterface_t    *ceInterface, *etInterface, *tInterface;
288  st_table          *coiIndexTable;
289  Bmc_PropertyStatus formulaStatus;
290
291  assert(Ctlsp_LtlFormulaIsFp(ltl));
292 
293  startTime = util_cpu_ctime();
294
295  if (options->verbosityLevel != BmcVerbosityNone_c){
296    fprintf(vis_stdout, "LTL formula is of type G(p)\n");
297  }
298  property = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager, ltl->right);
299 
300  if (property == mAig_NULL){
301    return;
302  }
303  if (verifyIfConstant(property)){
304    if (options->verbosityLevel != BmcVerbosityNone_c){
305      fprintf(vis_stdout, "-- bmc time = %10g\n",
306              (double)(util_cpu_ctime() - startTime) / 1000.0);
307    }
308    return;
309  }
310
311  if (options->verbosityLevel >= BmcVerbosityMax_c){
312    (void) fprintf(vis_stdout, "\nBMC: Check if the property is an inductive invariant\n");
313  }
314  checkInductiveInvariant = BmcCirCUsLtlCheckInductiveInvariant(network, ltl, options, coiTable);
315  if (checkInductiveInvariant == 1){
316    (void) fprintf(vis_stdout,"# BMC: The property is an inductive invariant\n");
317    (void) fprintf(vis_stdout,"# BMC: formula passed\n");
318    (void) fprintf(vis_stdout, "#      Termination depth = 0\n");
319    if (options->verbosityLevel != BmcVerbosityNone_c){
320      fprintf(vis_stdout, "-- bmc time = %10g\n",
321              (double)(util_cpu_ctime() - startTime) / 1000.0);
322    }
323    return;
324  }
325 
326  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network,
327                                                           MVFAIG_NETWORK_APPL_KEY);
328  assert(nodeToMvfAigTable != NIL(st_table));
329
330  ceInterface = 0;
331  etInterface = 0;
332  tInterface  = 0;
333  if (options->verbosityLevel != BmcVerbosityNone_c){
334    (void)fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d)\n",
335                  options->minK, options->maxK, options->step);
336  }
337  /*
338    Hold objects
339  */
340  objArray = array_alloc(bAigEdge_t, 2);
341  /*
342    Unused entry is set to bAig_One
343   */
344  array_insert(bAigEdge_t, objArray, 1, bAig_One);
345  /*
346    Hold auxiliary objects (constraints on the path)
347  */
348  auxObjArray = array_alloc(bAigEdge_t, 0);
349 
350  bAig_ExpandTimeFrame(network, manager, 1, BMC_NO_INITIAL_STATES); 
351  coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
352 
353  formulaStatus = BmcPropertyUndecided_c;
354  for(k = options->minK; k <= options->maxK; k += options->step){
355    if (options->verbosityLevel == BmcVerbosityMax_c){
356      fprintf(vis_stdout, "\nBMC: Generate counterexample of length %d\n", k);
357    }
358    /*
359      Expand counterexample length to k.  In BMC, counterexample of length k means
360      k+1 time frames.
361     */
362    bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES);
363    /*
364      The property true at any states from (k-step+1) to k
365     */
366    result = bAig_Zero;
367    for(j=k-options->step+1; j<=k; j++) {
368      /*
369        For k = options->minK, j goes outside the lower boundary of
370        counterexample search.
371      */
372      if(j < options->minK) continue;
373     
374      property = BmcCirCUsCreatebAigOfPropFormula(network, manager, j, ltl->right, BMC_INITIAL_STATES);
375      result   = bAig_Or(manager, result, property);
376    }
377    array_insert(bAigEdge_t, objArray, 0, result);
378    options->cnfPrefix = k;
379    ceInterface = BmcCirCUsInterfaceWithObjArr(manager, network, objArray,
380                                           auxObjArray, options,
381                                           ceInterface);
382    satFlag = ceInterface->status;
383    if(satFlag == SAT_SAT){
384      formulaStatus = BmcPropertyFailed_c;
385      break;
386    }
387    /*
388      Given that the property does not hold at all previous states.
389     */
390    array_insert_last(bAigEdge_t, auxObjArray, bAig_Not(result));
391
392    /*
393      Prove if the property passes using the induction proof of SSS0.
394    */
395    if((options->inductiveStep !=0) &&
396       (k % options->inductiveStep == 0)){
397      array_t *auxArray;
398      int i;
399     
400      if (options->verbosityLevel == BmcVerbosityMax_c) {
401        (void) fprintf(vis_stdout, "\nBMC: Check for termination\n");
402      }     
403      /*
404        Expand counterexample length to k+1.  In BMC, counterexample of length k+1 means
405        k+2 time frames.
406      */
407      bAig_ExpandTimeFrame(network, manager, k+2, BMC_NO_INITIAL_STATES);
408      simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
409                                                coiIndexTable, BMC_NO_INITIAL_STATES);
410      property = BmcCirCUsCreatebAigOfPropFormula(network, manager, k+1, ltl->right,
411                                                  BMC_NO_INITIAL_STATES);
412      array_insert(bAigEdge_t, objArray, 0, simplePath);
413      array_insert(bAigEdge_t, objArray, 1, property);
414      auxArray = array_alloc(bAigEdge_t, 0);
415      for(i=0; i<=k; i++){
416        array_insert_last(bAigEdge_t, auxArray,
417                          bAig_Not(
418                            BmcCirCUsCreatebAigOfPropFormula(network, manager, i, ltl->right,
419                                                             BMC_NO_INITIAL_STATES)
420                            ));
421      }
422      options->cnfPrefix = k+1;
423      tInterface = BmcCirCUsInterfaceWithObjArr(manager, network,
424                                      objArray, auxArray,
425                                      options, tInterface);
426      array_free(auxArray); 
427      array_insert(bAigEdge_t, objArray, 1, bAig_One);
428      if(tInterface->status == SAT_UNSAT){
429        if (options->verbosityLevel == BmcVerbosityMax_c) {
430          (void) fprintf(vis_stdout,
431                         "# BMC: No simple path leading to a bad state\n");
432        }
433        formulaStatus = BmcPropertyPassed_c;
434        break;
435      }
436     
437      if(options->earlyTermination){
438        /*
439          Early termination condition
440         
441          Check if there is no simple path starts from initial states
442         
443        */
444        simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
445                                                  coiIndexTable,
446                                                  BMC_INITIAL_STATES);
447        array_insert(bAigEdge_t, objArray, 0, simplePath);
448        etInterface = BmcCirCUsInterfaceWithObjArr(manager, network,
449                                               objArray, NIL(array_t),
450                                               options, etInterface);
451        options->cnfPrefix = k+1;
452        if(etInterface->status == SAT_UNSAT){
453          if (options->verbosityLevel == BmcVerbosityMax_c) {
454            (void) fprintf(vis_stdout,
455                           "# BMC: No simple path starting at an initial state\n");
456          }
457          formulaStatus = BmcPropertyPassed_c;
458          break;
459        }
460      }
461     
462    } /* check for termination*/
463  } /* loop over k*/
464  array_free(objArray);
465  array_free(auxObjArray);
466  sat_FreeInterface(ceInterface);
467  if(etInterface !=0){
468    sat_FreeInterface(etInterface);
469  }
470  if(tInterface !=0){
471    sat_FreeInterface(tInterface);
472  }
473  st_free_table(coiIndexTable);
474
475  if(formulaStatus == BmcPropertyUndecided_c){
476    if (options->verbosityLevel != BmcVerbosityNone_c){
477      (void) fprintf(vis_stdout,
478                     "# BMC: no counterexample found of length up to %d\n",
479                     options->maxK);
480    }
481  }
482  if(formulaStatus == BmcPropertyFailed_c) {
483    (void) fprintf(vis_stdout, "# BMC: formula failed\n");
484    if(options->verbosityLevel != BmcVerbosityNone_c){
485      (void) fprintf(vis_stdout,
486                     "# BMC: Found a counterexample of length = %d \n", k);
487    }
488    if(options->dbgLevel == 1){
489      BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, k, 0,
490                                   options, BMC_INITIAL_STATES);
491    }
492    if(options->dbgLevel == 2){
493      BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, k, 0,
494                                   options, BMC_INITIAL_STATES);
495    }
496  } else if(formulaStatus == BmcPropertyPassed_c) {
497    (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
498    (void) fprintf(vis_stdout, "#      Termination depth = %d\n", k);
499  } else if(formulaStatus == BmcPropertyUndecided_c) {
500    (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
501  }
502 
503  if (options->verbosityLevel != BmcVerbosityNone_c){
504    endTime = util_cpu_ctime();
505    fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
506  }
507  fflush(vis_stdout);
508
509  return;
510} /* BmcCirCUsLtlVerifyGp() */
511
512/**Function********************************************************************
513
514   Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of
515   the form F(p), where p is propositional.]
516
517   Description [Given a model M, an LTL formula f = Fp, and a bound k,
518   we first find a k-loop counterexample of length k at which all
519   states violate p.  If -r switch of the BMC command is specified, we
520   apply the method in the paper "Proving More Properties with Bounded
521   Model Checking" to check if the property f passes.
522
523   Note: Before calling this function, the LTL formula must be negated.
524
525   Using sat as SAT solver.
526   
527   ]   
528   SideEffects []
529   
530   SeeAlso     []
531
532******************************************************************************/
533
534void
535BmcCirCUsLtlVerifyFp(
536    Ntk_Network_t   *network,
537    Ctlsp_Formula_t *ltl,
538    st_table        *coiTable,
539    BmcOption_t     *options)
540{
541  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
542  st_table          *nodeToMvfAigTable = NIL(st_table);
543  long              startTime, endTime;
544  bAigEdge_t        property, pathProperty, simplePath, tloop, loop;
545  int               bound, k, satFlag;
546  array_t           *loop_array = NIL(array_t);
547  array_t           *objArray;
548  array_t           *auxObjArray;
549  st_table          *coiIndexTable;
550  satInterface_t    *ceInterface;
551  satInterface_t    *tInterface;
552  Bmc_PropertyStatus formulaStatus;
553
554  startTime = util_cpu_ctime();
555  if(options->verbosityLevel != BmcVerbosityNone_c){
556    fprintf(vis_stdout,"LTL formula is of type F(p)\n");
557  }
558  property = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager,
559                                                      ltl->right);
560  if (verifyIfConstant(property)){
561    if (options->verbosityLevel != BmcVerbosityNone_c){
562      fprintf(vis_stdout, "-- bmc time = %10g\n",
563              (double)(util_cpu_ctime() - startTime) / 1000.0);
564    }
565    return;
566  }
567
568  nodeToMvfAigTable = 
569          (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
570  assert(nodeToMvfAigTable != NIL(st_table));
571 
572  bAig_ExpandTimeFrame(network, manager, 0, BMC_INITIAL_STATES);
573  coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
574
575 /*
576    Hold objects
577  */
578  objArray = array_alloc(bAigEdge_t, 2);
579  /*
580    Unused entry is set to bAig_One
581   */
582  array_insert(bAigEdge_t, objArray, 1, bAig_One);
583  /*
584    Hold auxiliary objects (constraints on the path)
585  */
586  auxObjArray = array_alloc(bAigEdge_t, 0);
587 
588  ceInterface = 0;
589  tInterface  = 0;
590  formulaStatus = BmcPropertyUndecided_c;
591  if(options->verbosityLevel != BmcVerbosityNone_c){
592    fprintf(vis_stdout,"Apply BMC on counterexample of length >= %d and <= %d (+%d)\n",
593                       options->minK, options->maxK, options->step);
594
595  }
596  bound = options->minK;
597  while(bound<=options->maxK) {
598    if(options->verbosityLevel == BmcVerbosityMax_c)
599      fprintf(vis_stdout, "\nBMC: Generate counterexample of length %d\n", bound);
600    /*
601      Expand counterexample length to bound.  In BMC, counterexample of length bound means
602      bound+1 time frames.
603    */
604    bAig_ExpandTimeFrame(network, manager, bound+1, BMC_INITIAL_STATES );
605    /**
606     * How can we manage cone of influence with this part ?
607     **/
608    loop_array = array_alloc(bAigEdge_t *, 0);
609    tloop = bAig_Zero;
610    /*
611      Loop from state 'bound' to any previous states.
612     */
613    for(k=0; k<=bound; k++) {
614      loop = BmcCirCUsConnectFromStateToState(network, bound, k, nodeToMvfAigTable,
615                                              coiIndexTable, BMC_INITIAL_STATES);
616      array_insert(bAigEdge_t, loop_array, k, loop);
617      tloop = bAig_Or(manager, tloop, loop);
618    }
619    array_insert(bAigEdge_t, objArray, 0, tloop);
620    /*
621      tloop equals true for k-loop path
622     */
623    /*
624      Property false at all states
625     */
626    pathProperty = bAig_One;
627    for(k=bound; k>=0; k--) {
628      property = BmcCirCUsCreatebAigOfPropFormula(network, manager, k, ltl->right, BMC_INITIAL_STATES);
629      pathProperty = bAig_And(manager, pathProperty, property);
630    }
631    array_insert(bAigEdge_t, objArray, 1, pathProperty);
632   
633    options->cnfPrefix = bound;
634    ceInterface = BmcCirCUsInterfaceWithObjArr(manager, network,
635                                               objArray, auxObjArray,
636                                               options, ceInterface);
637    satFlag = ceInterface->status;
638    if(satFlag == SAT_SAT){
639      formulaStatus = BmcPropertyFailed_c;
640      break;
641    }
642
643    array_insert_last(bAigEdge_t, auxObjArray, bAig_Not(tloop));
644
645    if((options->inductiveStep !=0) &&
646       (bound % options->inductiveStep == 0)){
647
648      if (options->verbosityLevel == BmcVerbosityMax_c) {
649        (void) fprintf(vis_stdout,
650                       "\nBMC: Check for termination\n");
651      }
652      simplePath = BmcCirCUsSimlePathConstraint(network, 0, bound, nodeToMvfAigTable,
653                                                coiIndexTable,
654                                                BMC_INITIAL_STATES);
655      array_insert(bAigEdge_t, objArray, 0, simplePath);
656      array_insert(bAigEdge_t, objArray, 1, pathProperty);
657      tInterface = BmcCirCUsInterfaceWithObjArr(manager, network,
658                                                objArray, auxObjArray,
659                                                options, tInterface);
660      if(tInterface->status == SAT_UNSAT){
661        formulaStatus = BmcPropertyPassed_c;
662        break;
663      }
664    }
665    bound += options->step;
666  }
667  array_free(objArray);
668  array_free(auxObjArray);
669  st_free_table(coiIndexTable);
670  sat_FreeInterface(ceInterface);
671  sat_FreeInterface(tInterface);
672
673  if(formulaStatus == BmcPropertyUndecided_c){
674    if (options->verbosityLevel != BmcVerbosityNone_c){
675      (void) fprintf(vis_stdout,
676                     "# BMC: no counterexample found of length up to %d\n",
677                     options->maxK);
678    }
679  }
680  if(formulaStatus == BmcPropertyFailed_c) {
681    (void) fprintf(vis_stdout, "# BMC: formula failed\n");
682    if(options->verbosityLevel != BmcVerbosityNone_c){
683      (void) fprintf(vis_stdout,
684                     "# BMC: Found a counterexample of length = %d \n", bound);
685    }
686    if(options->dbgLevel == 1){
687     BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, bound, loop_array,
688                                   options, BMC_INITIAL_STATES);
689    }
690    if(options->dbgLevel == 2){
691     BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, bound, loop_array,
692                                   options, BMC_INITIAL_STATES);
693    }
694
695  } else if(formulaStatus == BmcPropertyPassed_c) {
696    (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
697    (void) fprintf(vis_stdout, "#      Termination depth = %d\n", bound);
698  } else if(formulaStatus == BmcPropertyUndecided_c) {
699    (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
700  }
701  if (options->verbosityLevel != BmcVerbosityNone_c) {
702    endTime = util_cpu_ctime();
703    fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
704  }
705  fflush(vis_stdout); 
706  array_free(loop_array);
707
708} /* BmcCirCUsLtlVerifyFp() */
709
710/**Function********************************************************************
711
712   Synopsis [Build AIG graph of BMC encoding for a path]
713
714   Description [Build AIG graph of BMC encoding for a path. If loop = -1,
715   then the BMC encoding is for no loop path.  Otherwise, it is for
716   (to, loop)-loop path]
717
718   SideEffects []
719   
720   SeeAlso     []
721   
722******************************************************************************/
723bAigEdge_t
724BmcCirCUsGenerateLogicForLtl(
725    Ntk_Network_t   *network,
726    Ctlsp_Formula_t *ltl,
727    int from,
728    int to,
729    int loop)
730{
731  bAigEdge_t property, temp;
732  bAigEdge_t left, right, result;
733  int j, k;
734  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
735
736  if(Ctlsp_isPropositionalFormula(ltl)){
737    property = BmcCirCUsCreatebAigOfPropFormula(network, manager, from, ltl, BMC_INITIAL_STATES);
738    return(property);
739  }
740
741  switch(ltl->type) {
742    case Ctlsp_NOT_c:
743      if (!Ctlsp_isPropositionalFormula(ltl->left)){
744        fprintf(vis_stderr,"BMC error: the LTL formula is not in NNF\n");
745        return 0;
746      }
747    case Ctlsp_AND_c:
748      left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, from, to, loop);
749      if(left == bAig_Zero)     return(bAig_Zero);
750      right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, from, to, loop);
751      return(bAig_And(manager, left, right));
752    case Ctlsp_OR_c:
753      left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, from, to, loop);
754      if(left == bAig_One)      return(bAig_One);
755      right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, from, to, loop);
756      return(bAig_Or(manager, left, right));
757    case Ctlsp_F_c:
758      if(loop >= 0)     from = (loop<from) ? loop : from;
759      result = bAig_Zero;
760      for(j=from; j<=to; j++)  {
761        left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, j, to, loop);
762        if(left == bAig_One)    return(left);
763        result = bAig_Or(manager, left, result);
764      }
765      return(result);
766    case Ctlsp_G_c:
767      if(loop < 0)      return(bAig_Zero);
768      from = (loop < from) ? loop : from;
769      result = bAig_One;
770      for(j=from; j<=to; j++) {
771        left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, j, to, loop);
772        result = bAig_And(manager, result, left);
773        if(result == bAig_Zero) break;
774      }
775      return(result);
776    case Ctlsp_X_c:
777      if(loop>=0 && from == to) from = loop;
778      else if(from < to)        from = from + 1;
779      else                      return(bAig_Zero);
780      left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, from, to, loop);
781      return(left);
782    case Ctlsp_U_c:
783      result = bAig_Zero;
784      for(j=from; j<=to; j++) {
785        right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, j, to, loop);
786        temp = right;
787        for(k=from; (k<=j-1); k++) {
788          left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, k, to, loop);
789          temp = bAig_And(manager, temp, left);
790          if(temp == bAig_Zero) break;
791        }
792        result = bAig_Or(manager, result, temp);
793        if(result == bAig_One) break;
794      }
795      if(loop>=0 && result != bAig_One) {
796        for(j=loop; j<=from-1; j++) {
797          right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, j, to, loop);
798          temp = right;
799          for(k=from; k<=to; k++) {
800            left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, k, to, loop);
801            temp = bAig_And(manager, temp, left);
802            if(temp == bAig_Zero)       break;
803          }
804          for(k=loop; k<=j-1; k++) {
805            left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, k, to, loop);
806            temp = bAig_And(manager, temp, left);
807            if(temp == bAig_Zero)       break;
808          }
809          result = bAig_Or(manager, result, temp);
810          if(result == bAig_One) break;
811        }
812      }
813      return(result);
814    case Ctlsp_R_c:
815      result = bAig_Zero;
816      if(loop >= 0) {
817        temp = bAig_One;
818        for(j=(from<loop ? from : loop); j<=to; j++) {
819          right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, j, to, loop);
820          temp = bAig_And(manager, temp, right);
821          if(temp == bAig_Zero) break;
822        }
823        result = bAig_Or(manager, result, temp);
824      }
825      if(result != bAig_One) {
826        for(j=from; j<=to; j++) {
827          left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, j, to, loop);
828          temp = left;
829          for(k=from; k<=j; k++) {
830            right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, k, to, loop);
831            temp = bAig_And(manager, temp, right);
832            if(temp == bAig_Zero)       break;
833          }
834          result = bAig_Or(manager, temp, result);
835          if(result == bAig_One) break;
836        }
837        if(loop >= 0 && result != bAig_One) {
838          for(j=loop; j<=from-1; j++) {
839            left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, j, to, loop);
840
841            temp = left;
842            for(k=from; k<=to; k++) {
843              right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, k, to, loop);
844              temp = bAig_And(manager, temp, right);
845              if(temp == bAig_Zero)     break;
846            }
847
848            for(k=loop; k<=j; k++) {
849              right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, k, to, loop);
850              temp = bAig_And(manager, temp, right);
851              if(temp == bAig_Zero)     break;
852            }
853
854            result = bAig_Or(manager, result, temp);
855            if(result == bAig_One) break;
856          }
857        }
858      }
859      return(result);
860    default:
861      fail("Unexpected LTL formula type");
862      break;
863  }
864  assert(0);
865  return(-1);
866
867}
868
869/**Function********************************************************************
870   
871   Synopsis [Build AIG graph for BMC encoding using Separated Normal Form
872   (SNF)]
873   
874   Description []
875   
876   SideEffects []
877   
878   SeeAlso     []
879   
880******************************************************************************/
881bAigEdge_t
882BmcCirCUsGenerateLogicForLtlSNF(
883  Ntk_Network_t   *network,
884  array_t         *formulaArray,
885  int             fromState,
886  int             toState,
887  int             loop)
888{
889  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
890  Ctlsp_Formula_t *formula;
891  bAigEdge_t      property = bAig_One;
892  bAigEdge_t      left, right, result;
893  int             i, k;
894  Ctlsp_Formula_t *leftChild, *rightChild;
895
896  for (i = 0; i < array_n(formulaArray); i++) { 
897    formula    = array_fetch(Ctlsp_Formula_t *, formulaArray, i); 
898    leftChild  = Ctlsp_FormulaReadLeftChild(formula);
899    rightChild = Ctlsp_FormulaReadRightChild(formula);
900
901    if(!strcmp(Ctlsp_FormulaReadVariableName(leftChild), " SNFstart")){
902      result = BmcCirCUsGenerateLogicForLtl(network, rightChild,
903                                            0, toState, loop);
904    } else 
905      if(!strcmp(Ctlsp_FormulaReadVariableName(leftChild), " SNFbound")){
906        result =  BmcCirCUsGenerateLogicForLtl(network, rightChild,
907                                               toState, toState, loop);
908      } else {
909        result = bAig_One;
910        for(k=fromState; k<= toState; k++){
911          left  = BmcCirCUsGenerateLogicForLtl(network, leftChild,
912                                               k, toState, loop);
913          right = BmcCirCUsGenerateLogicForLtl(network, rightChild,
914                                               k, toState, loop);
915          result = bAig_And(manager, result,
916                            bAig_Then(manager, left, right));
917        }
918      }
919    property = bAig_And(manager, property, result);
920  }
921  return property;
922} /* BmcCirCUsGenerateLogicForLtlSNF */
923
924
925/**Function********************************************************************
926
927   Synopsis [Build AIG graph of BMC encoding for LTL formulae based on fixpoint
928   characteristics of LTL formulae.]
929
930   Description [We use BMC encoding based on FMCAD'04 paper: Simple Bounded LTL
931   Model Checking.
932
933   This function can only be applied to abbreviation-free LTL formulae. The
934   formula must be in Negation Normal Form.  For LTL formula of the form Fp,
935   where p is propositional, this function build AIG for auxiliary
936   translation.]
937
938   SideEffects []
939   
940   SeeAlso     []
941   
942******************************************************************************/
943bAigEdge_t
944BmcCirCUsGenerateLogicForLtlFixPoint(
945  Ntk_Network_t   *network,
946  Ctlsp_Formula_t *ltl,
947  int             from,
948  int             to,
949  array_t         *loopArray)
950{
951  bAigEdge_t result;
952  st_table   *ltl2AigTable;
953
954  assert(ltl != NIL(Ctlsp_Formula_t));
955 
956  ltl2AigTable = st_init_table(strcmp, st_strhash);
957  result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl,
958                                  from, to, 0, loopArray, ltl2AigTable);
959  st_free_table(ltl2AigTable);
960
961  return result;
962} /* BmcCirCUsGenerateLogicForLtlFixPoint */
963
964/**Function********************************************************************
965
966   Synopsis [The recursive function of BmcCirCUsGenerateLogicForLtlFixPoint]
967
968   Description []
969
970   SideEffects []
971   
972   SeeAlso     []
973   
974******************************************************************************/
975bAigEdge_t
976BmcCirCUsGenerateLogicForLtlFixPointRecursive(
977  Ntk_Network_t   *network,
978  Ctlsp_Formula_t *ltl,
979  int             from,
980  int             to,
981  int             translation, /* 0 auxilary translation. 1 final translation */
982  array_t         *loopArray,
983  st_table        *ltl2AigTable)
984{
985  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
986  bAigEdge_t      property, temp;
987  bAigEdge_t      left, right, result;
988
989  int      j;
990
991  char     *nameKey;
992  char     tmpName[100];
993
994  /*
995    Check if AIG was built for this LTL formula at a given time
996   */
997  sprintf(tmpName, "%ld_%d%d", (long)ltl, from, translation);
998  nameKey = util_strsav(tmpName);
999  if(st_lookup(ltl2AigTable, nameKey, &result)){
1000    FREE(nameKey);
1001    return result;
1002  }
1003  FREE(nameKey);
1004 
1005  if(Ctlsp_isPropositionalFormula(ltl)){
1006    property = BmcCirCUsCreatebAigOfPropFormula(network, manager,
1007                                                from, ltl, BMC_INITIAL_STATES);
1008    sprintf(tmpName, "%ld_%d%d", (long)ltl, from, 1);
1009    nameKey = util_strsav(tmpName);
1010    st_insert(ltl2AigTable, nameKey, (char*) (long) property);
1011    return(property);
1012  }
1013  switch(ltl->type) {
1014  case Ctlsp_NOT_c:
1015    if (!Ctlsp_isPropositionalFormula(ltl->left)){
1016      fprintf(vis_stderr,"BMC error: the LTL formula is not in NNF\n");
1017
1018      return 0;
1019    }
1020  case Ctlsp_AND_c:
1021    left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, from, to,
1022                                                         translation, loopArray, ltl2AigTable);
1023    if(left == bAig_Zero){
1024      return(bAig_Zero);
1025    }
1026    right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, from, to,
1027                                                          translation, loopArray, ltl2AigTable);
1028    return(bAig_And(manager, left, right));
1029  case Ctlsp_OR_c:
1030    left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, from, to,
1031                                                         translation, loopArray, ltl2AigTable);
1032    if(left == bAig_One){
1033      return(bAig_One);
1034    }
1035    right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, from, to,
1036                                                          translation, loopArray, ltl2AigTable);
1037    return(bAig_Or(manager, left, right));
1038  case Ctlsp_X_c:
1039    if(from < to){
1040      result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, from+1, to,
1041                                                             1, loopArray, ltl2AigTable);
1042    } else {
1043      result =  bAig_Zero;
1044      for(j=1; j<=to; j++) {
1045        left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,  j, to,
1046                                                              1, loopArray, ltl2AigTable);
1047        temp = bAig_And(manager, array_fetch(bAigEdge_t, loopArray, j), left);
1048        result = bAig_Or(manager, result, temp);
1049      }
1050    }
1051    sprintf(tmpName, "%ld_%d%d", (long) ltl, from, 1);
1052    nameKey = util_strsav(tmpName);
1053    st_insert(ltl2AigTable, nameKey, (char*) (long) result);
1054    return result;
1055  case Ctlsp_U_c:
1056    sprintf(tmpName, "%ld_%d%d", (long) ltl, to, 0); /* 0 for auxiliary translation*/
1057    nameKey = util_strsav(tmpName);
1058    right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, to, to, 1, loopArray, ltl2AigTable);
1059    st_insert(ltl2AigTable, nameKey, (char*) (long) right);
1060    /*
1061      Compute the auxiliary translation.
1062    */
1063    for(j=to-1; j>=from; j--) {
1064      result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl, j+1, to, 0, loopArray, ltl2AigTable);
1065     
1066      right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, j, to, 1, loopArray, ltl2AigTable);
1067      left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,  j, to, 1, loopArray, ltl2AigTable);
1068     
1069      result  = bAig_And(manager,left, result);
1070      result  = bAig_Or(manager,right, result);
1071     
1072      sprintf(tmpName, "%ld_%d%d", (long)ltl, j, 0); /* 0 for auxiliary translation*/
1073      nameKey = util_strsav(tmpName);
1074      st_insert(ltl2AigTable, nameKey, (char*) (long) result);
1075    }
1076    /*
1077      Compute the final translation at k.
1078    */
1079    result =  bAig_Zero;
1080    for(j=1; j<=to; j++) {
1081      temp = bAig_And(manager, array_fetch(bAigEdge_t, loopArray, j),
1082                      BmcCirCUsGenerateLogicForLtlFixPointRecursive(
1083                        network, ltl, j, to, 0, loopArray, ltl2AigTable));
1084      result = bAig_Or(manager, result, temp);
1085    }
1086    right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, to, to, 1, loopArray, ltl2AigTable);
1087    left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,
1088                                                          to, to, 1, loopArray,
1089                                                          ltl2AigTable);
1090   
1091    result  = bAig_And(manager,left, result);
1092    result  = bAig_Or(manager,right, result);
1093   
1094    sprintf(tmpName, "%ld_%d%d", (long)ltl, to, 1); /* 1 for final translation*/
1095    nameKey = util_strsav(tmpName);
1096    st_insert(ltl2AigTable, nameKey, (char*) (long) result);
1097    /*
1098      Compute the final translation.
1099    */
1100    for(j=to-1; j>=from; j--) {
1101      result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl, j+1, to, 1, loopArray, ltl2AigTable);
1102
1103      right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, j, to, 1, loopArray, ltl2AigTable);
1104      left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,  j, to, 1, loopArray, ltl2AigTable);
1105   
1106      result  = bAig_And(manager,left, result);
1107      result  = bAig_Or(manager,right, result);
1108
1109      sprintf(tmpName, "%ld_%d%d", (long)ltl, j, 1);
1110      nameKey = util_strsav(tmpName);
1111      st_insert(ltl2AigTable, nameKey, (char*) (long) result);
1112    }
1113    return(result);
1114  case Ctlsp_R_c:
1115    sprintf(tmpName, "%ld_%d%d", (long)ltl, to, 0); /* 0 for auxiliary translation*/
1116    right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, to, to, 1, loopArray, ltl2AigTable);
1117    nameKey = util_strsav(tmpName);
1118    st_insert(ltl2AigTable, nameKey, (char*) (long) right);
1119    /*
1120      Compute the auxiliary translation.
1121    */
1122    for(j=to-1; j>=from; j--) {
1123      result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl, j+1, to, 0, loopArray, ltl2AigTable);
1124     
1125      right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, j, to, 1, loopArray, ltl2AigTable);
1126      left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,  j, to, 1, loopArray, ltl2AigTable);
1127     
1128      result  = bAig_Or(manager,left, result);
1129      result  = bAig_And(manager,right, result);
1130     
1131      sprintf(tmpName, "%ld_%d%d", (long) ltl, j, 0); /* 0 for auxiliary translation*/
1132      nameKey = util_strsav(tmpName);
1133      st_insert(ltl2AigTable, nameKey, (char*) (long) result);
1134    }
1135    /*
1136      Compute the final translation at k.
1137    */
1138    result =  bAig_Zero;
1139    for(j=1; j<=to; j++) {
1140      temp = bAig_And(manager, array_fetch(bAigEdge_t, loopArray, j),
1141                      BmcCirCUsGenerateLogicForLtlFixPointRecursive(
1142                        network, ltl, j, to, 0, loopArray, ltl2AigTable));
1143      result = bAig_Or(manager, result, temp);
1144    }
1145    right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right,
1146                                                          to, to, 1, loopArray,
1147                                                          ltl2AigTable);
1148    left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,
1149                                                          to, to, 1, loopArray,
1150                                                          ltl2AigTable);   
1151    result  = bAig_Or(manager,left, result);
1152    result  = bAig_And(manager,right, result);
1153   
1154    sprintf(tmpName, "%ld_%d%d", (long) ltl, to+1, 1); /* 1 for final translation*/
1155    nameKey = util_strsav(tmpName);
1156    st_insert(ltl2AigTable, nameKey, (char*) (long) result);
1157    /*
1158      Compute the final translation.
1159    */
1160    for(j=to-1; j>=from; j--) {
1161      result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl, j+1, to, 1, loopArray, ltl2AigTable);
1162
1163      right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, j, to, 1, loopArray, ltl2AigTable);
1164      left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,  j, to, 1, loopArray, ltl2AigTable);
1165   
1166      result  = bAig_Or(manager,left, result);
1167      result  = bAig_And(manager,right, result);
1168
1169      sprintf(tmpName, "%ld_%d%d", (long)ltl, j, 1);
1170      nameKey = util_strsav(tmpName);
1171      st_insert(ltl2AigTable, nameKey, (char*) (long) result);
1172    }
1173    return(result);
1174  case Ctlsp_F_c:
1175    /*
1176      Compute only the auxiliary translation.
1177    */
1178    sprintf(tmpName, "%ld_%d%d", (long)ltl, to, 0); /* 0 for auxiliary translation*/
1179    nameKey = util_strsav(tmpName);
1180    left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,
1181                                                         to, to, 1, loopArray,
1182                                                         ltl2AigTable);
1183    st_insert(ltl2AigTable, nameKey, (char*) (long) left);
1184
1185    for(j=to-1; j>=from; j--) {
1186      result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl,
1187                                                             j+1, to, 0,
1188                                                             loopArray,
1189                                                             ltl2AigTable);
1190      left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,
1191                                                           j, to, 1, loopArray,
1192                                                           ltl2AigTable);
1193      result  = bAig_Or(manager,left, result);
1194     
1195      sprintf(tmpName, "%ld_%d%d", (long)ltl, j, 0); /* 0 for auxiliary translation*/
1196      nameKey = util_strsav(tmpName);
1197      st_insert(ltl2AigTable, nameKey, (char*) (long) result);
1198    }
1199    result =  bAig_Zero;
1200    for(j=1; j<=to; j++) {
1201      temp = bAig_And(manager, array_fetch(bAigEdge_t, loopArray, j),
1202                      BmcCirCUsGenerateLogicForLtlFixPointRecursive(
1203                        network, ltl, j, to, 0, loopArray, ltl2AigTable));
1204      result = bAig_Or(manager, result, temp);
1205    }
1206    return(result);
1207  default:
1208    fail("Unexpected LTL formula type");
1209    break;
1210  }
1211  assert(0);
1212  return(-1);
1213}
1214
1215/**Function********************************************************************
1216
1217   Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of
1218   the form FG(p), where p is propositional.]
1219
1220   Description [Given a model M, an LTL formula f = FGp, and a bound k, we
1221   first find a k-loop counterexample of length k at which p false inside the
1222   loop.  If -r switch of the BMC command is specified, we apply the method in
1223   the paper "Proving More Properties with Bounded Model Checking" to check if
1224   the property passes.
1225
1226   Note: Before calling this function, the LTL formula must be negated.
1227   
1228   ]
1229 
1230  SideEffects []
1231
1232  SeeAlso     []
1233
1234******************************************************************************/
1235void
1236BmcCirCUsLtlVerifyFGp(
1237   Ntk_Network_t   *network,
1238   Ctlsp_Formula_t *ltlFormula,
1239   st_table        *coiTable,
1240   BmcOption_t     *options)
1241{
1242  mAig_Manager_t   *manager = Ntk_NetworkReadMAigManager(network);
1243  st_table         *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
1244
1245  int              j, k, l, satFlag;
1246
1247  long             startTime, endTime;
1248  int              minK = options->minK;
1249  int              maxK = options->maxK;
1250  Ctlsp_Formula_t  *propFormula;
1251  bAigEdge_t       property, loop, pathProperty, tloop;
1252  array_t          *loop_array = NIL(array_t);
1253  array_t          *previousResultArray;
1254  st_table         *coiIndexTable;
1255  satInterface_t   *ceInterface;
1256 
1257  Bmc_PropertyStatus formulaStatus;
1258
1259  int              m=-1, n=-1;
1260  int              checkLevel = 0;
1261  /*
1262    Refer to Theorem 1 in the paper "Proving More Properties with Bounded Model Checking"
1263   
1264    If checkLevel == 0 -->  check for beta' only. If UNSAT, m=k and chekLevel = 1
1265    If checkLevel == 1 -->  check for beta  only. If UNSAT, checkLevel = 2.
1266    If checkLevel == 2 -->  check for alpha only. If UNSAT, n=k and checkLevel = 3.
1267    If gama is UNSAT up to (m+n-1) and checkLvel = 3, formula passes.
1268    checkLevel = 4 if (m+n-1) > maxK; */
1269
1270  /*
1271    Remember the LTL property was negated
1272  */
1273  assert(Ctlsp_LtlFormulaIsGFp(ltlFormula));
1274
1275  /* ************** */
1276  /* Initialization */
1277  /* ************** */
1278 
1279  startTime = util_cpu_ctime();
1280  if(options->verbosityLevel >= BmcVerbosityMax_c){
1281    fprintf(vis_stdout,"LTL formula is of type FG(p)\n");
1282  }
1283  propFormula = Ctlsp_FormulaReadRightChild(Ctlsp_FormulaReadRightChild(ltlFormula));
1284  property = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager,
1285                                                      propFormula);
1286  if (verifyIfConstant(property)){
1287    if (options->verbosityLevel != BmcVerbosityNone_c){
1288      fprintf(vis_stdout, "-- bmc time = %10g\n",
1289              (double)(util_cpu_ctime() - startTime) / 1000.0);
1290    }
1291    return;
1292  }
1293 
1294  /*
1295    nodeToMvfAigTable maps each node to its multi-function And/Inv graph
1296  */
1297  nodeToMvfAigTable =
1298    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
1299  assert(nodeToMvfAigTable != NIL(st_table));
1300 
1301  bAig_ExpandTimeFrame(network, manager, 0, BMC_INITIAL_STATES);
1302  coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
1303 
1304  previousResultArray = array_alloc(bAigEdge_t, 0);
1305  ceInterface = 0;
1306  if(options->verbosityLevel != BmcVerbosityNone_c){
1307    fprintf(vis_stdout,"Apply BMC on counterexample of length >= %d and <= %d (+%d)\n",
1308            options->minK, options->maxK, options->step);
1309   
1310  }
1311  k= minK;
1312  formulaStatus = BmcPropertyUndecided_c;
1313  while(k <= maxK){
1314    if (options->verbosityLevel >= BmcVerbosityMax_c) {
1315      (void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
1316    }
1317   /*
1318     Expand counterexample length to bound.  In BMC, counterexample of length bound means
1319     k+1 time frames.
1320   */
1321    bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES );
1322
1323    /*
1324      k-loop
1325    */
1326    loop_array = array_alloc(bAigEdge_t *, 0);
1327    tloop = bAig_Zero;
1328    /*
1329      Loop from last state to any previous states.
1330    */
1331    for(l=0; l<=k; l++) {
1332      loop = BmcCirCUsConnectFromStateToState(network, k, l, nodeToMvfAigTable,
1333                                              coiIndexTable, BMC_INITIAL_STATES);
1334      array_insert(bAigEdge_t, loop_array, l, loop);
1335      pathProperty = bAig_Zero;
1336      for(j=l; j<=k; j++){
1337        property = BmcCirCUsCreatebAigOfPropFormula(network, manager, j, propFormula, BMC_INITIAL_STATES);
1338        pathProperty = bAig_Or(manager, pathProperty, property);
1339      }
1340     
1341      tloop = bAig_Or(manager, tloop, bAig_And(manager, pathProperty, loop));
1342    }
1343    options->cnfPrefix = k;
1344    ceInterface = BmcCirCUsInterface(manager, network, tloop,
1345                                     previousResultArray, options,
1346                                     ceInterface);
1347    satFlag = ceInterface->status;
1348    if(satFlag == SAT_SAT){
1349      formulaStatus = BmcPropertyFailed_c;
1350      break;
1351    }
1352    array_free(loop_array);
1353
1354    /* ==================
1355       Prove termination
1356       ================== */
1357    if((checkLevel < 3) &&
1358       (options->inductiveStep !=0) &&
1359       (k % options->inductiveStep == 0))
1360      {
1361        satInterface_t *tInterface=0, *etInterface=0;
1362        bAigEdge_t     simplePath, property;
1363        int            i;
1364       
1365        /* ===========================
1366           Early termination condition
1367           ===========================
1368        */
1369        if (options->earlyTermination) {
1370          if (options->verbosityLevel >= BmcVerbosityMax_c) {
1371            (void) fprintf(vis_stdout, "\nChecking for early termination at k= %d\n", k);
1372          }
1373          bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES);
1374          simplePath = BmcCirCUsSimlePathConstraint(network, 0, k, nodeToMvfAigTable,
1375                                                    coiIndexTable, BMC_INITIAL_STATES);
1376          options->cnfPrefix = k;
1377          etInterface = BmcCirCUsInterface(manager, network,
1378                                           simplePath,
1379                                           previousResultArray,
1380                                           options, etInterface);
1381          if(etInterface->status == SAT_UNSAT){
1382            formulaStatus = BmcPropertyPassed_c;
1383            if (options->verbosityLevel >= BmcVerbosityMax_c) {
1384              (void) fprintf(vis_stdout, "# BMC: by early termination\n");
1385            }
1386            break;
1387          }
1388        } /* Early termination */
1389        /*
1390          Check for \beta''(k)
1391        */
1392        if(checkLevel == 0){
1393          if (options->verbosityLevel == BmcVerbosityMax_c) {
1394            (void) fprintf(vis_stdout, "# BMC: Check Beta''\n");
1395          }
1396         
1397          bAig_ExpandTimeFrame(network, manager, k+2, BMC_NO_INITIAL_STATES);
1398          simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
1399                                                 coiIndexTable, BMC_NO_INITIAL_STATES);
1400          property = bAig_One;
1401          for(i=1; i<=k+1; i++){
1402            property = bAig_And(manager, property,
1403                                bAig_Not(BmcCirCUsCreatebAigOfPropFormula(
1404                                  network, manager, i,
1405                                  propFormula, BMC_NO_INITIAL_STATES)));
1406          }
1407          property = bAig_And(manager, property,
1408                              BmcCirCUsCreatebAigOfPropFormula(
1409                                network, manager, 0,
1410                                propFormula, BMC_NO_INITIAL_STATES));
1411          options->cnfPrefix = k+1;
1412          tInterface = 0;
1413          tInterface = BmcCirCUsInterface(manager, network,
1414                                          bAig_And(manager, property, simplePath),
1415                                          previousResultArray, options, tInterface);
1416          if(tInterface->status == SAT_UNSAT){
1417            m = k;
1418            if (options->verbosityLevel >= BmcVerbosityMax_c) {
1419              (void)fprintf(vis_stderr,"m = %d\n", m);
1420            }
1421            checkLevel = 1;
1422          }
1423        } /* Check for Beta'' */
1424        /*
1425          Check for \beta'(k)
1426        */
1427        if(checkLevel == 0){
1428          if (options->verbosityLevel == BmcVerbosityMax_c) {
1429            (void) fprintf(vis_stdout, "# BMC: Check Beta'\n");
1430          }
1431          bAig_ExpandTimeFrame(network, manager, k+2, BMC_NO_INITIAL_STATES);
1432          simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
1433                                                 coiIndexTable, BMC_NO_INITIAL_STATES);
1434          property = bAig_One;
1435          for(i=0; i<=k; i++){
1436            property = bAig_And(manager, property,
1437                                bAig_Not(BmcCirCUsCreatebAigOfPropFormula(
1438                                  network, manager, i,
1439                                  propFormula, BMC_NO_INITIAL_STATES)));
1440          }
1441          property = bAig_And(manager, property,
1442                              BmcCirCUsCreatebAigOfPropFormula(
1443                                network, manager, k+1,
1444                                propFormula, BMC_NO_INITIAL_STATES));
1445          options->cnfPrefix = k+1;
1446          tInterface = 0;
1447          tInterface = BmcCirCUsInterface(manager, network,
1448                                          bAig_And(manager, property, simplePath),
1449                                          previousResultArray, options, tInterface);
1450          if(tInterface->status == SAT_UNSAT){
1451            m = k;
1452            if (options->verbosityLevel >= BmcVerbosityMax_c) {
1453              (void)fprintf(vis_stderr,"m = %d\n", m);
1454            }
1455            checkLevel = 1;
1456          } 
1457        } /* Check for Beta' */
1458        /*
1459          Check for Beta
1460        */
1461        if(checkLevel == 1){
1462          if (options->verbosityLevel == BmcVerbosityMax_c) {
1463            (void) fprintf(vis_stdout, "# BMC: Check Beta\n");
1464          }
1465          bAig_ExpandTimeFrame(network, manager, k+2, BMC_NO_INITIAL_STATES);
1466          simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
1467                                                 coiIndexTable, BMC_NO_INITIAL_STATES);
1468          property = bAig_And(manager,
1469                              bAig_Not(BmcCirCUsCreatebAigOfPropFormula(
1470                                network, manager, k,
1471                                propFormula, BMC_NO_INITIAL_STATES)),
1472                              BmcCirCUsCreatebAigOfPropFormula(
1473                                network, manager, k+1,
1474                                propFormula, BMC_NO_INITIAL_STATES));
1475          options->cnfPrefix = k+1;
1476          tInterface = BmcCirCUsInterface(manager, network,
1477                                          bAig_And(manager, property, simplePath),
1478                                          previousResultArray, options, tInterface);
1479          if(tInterface->status == SAT_UNSAT){
1480            checkLevel = 2;
1481          }
1482        } /* Check Beta*/
1483 
1484        if(checkLevel == 2){ /* we check Alpha if Beta is unsatisfiable */
1485          if (options->verbosityLevel == BmcVerbosityMax_c) {
1486            (void) fprintf(vis_stdout, "# BMC: Check Alpha \n");
1487          }
1488          bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES);
1489          simplePath = BmcCirCUsSimlePathConstraint(network, 0, k, nodeToMvfAigTable,
1490                                                  coiIndexTable, BMC_INITIAL_STATES);
1491          property = BmcCirCUsCreatebAigOfPropFormula(
1492                                  network, manager, k,
1493                                  propFormula, BMC_INITIAL_STATES);
1494          options->cnfPrefix = k;
1495          tInterface = 0;
1496          tInterface = BmcCirCUsInterface(manager, network,
1497                                          bAig_And(manager, property, simplePath),
1498                                          previousResultArray, options, tInterface);
1499          if(tInterface->status == SAT_UNSAT){
1500            n = k;
1501            checkLevel = 3;
1502            if (options->verbosityLevel == BmcVerbosityMax_c) {
1503              (void)fprintf(vis_stdout,"Value of m=%d  n=%d\n", m, n);
1504            }
1505            if (m+n-1 <= maxK){
1506              maxK = m+n-1;
1507              checkLevel = 3;
1508            } else {
1509              checkLevel = 4;
1510            }
1511          }
1512        }/* Chek for Alpha */
1513       
1514        if (options->verbosityLevel != BmcVerbosityNone_c) {
1515          endTime = util_cpu_ctime();
1516          fprintf(vis_stdout, "-- Check for termination time = %10g\n",
1517                  (double)(endTime - startTime) / 1000.0);
1518        }
1519 
1520      } /* Check for termination */
1521    k += options->step;
1522  } /* while result and k*/
1523 
1524  if(formulaStatus == BmcPropertyFailed_c) {
1525    (void) fprintf(vis_stdout, "# BMC: formula failed\n");
1526    if(options->verbosityLevel != BmcVerbosityNone_c){
1527      (void) fprintf(vis_stdout,
1528                       "# BMC: Found a counterexample of length = %d \n", k);
1529    }
1530    if(options->dbgLevel == 1){
1531      BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, k, loop_array,
1532                                   options, BMC_INITIAL_STATES);
1533    }
1534    if(options->dbgLevel == 2){
1535      BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, k, loop_array,
1536                                   options, BMC_INITIAL_STATES);
1537    }
1538
1539    array_free(loop_array);
1540  }
1541  if(checkLevel == 3){
1542    (void) fprintf(vis_stdout, "# BMC: no counterexample of length <= (m+n-1) %d is found \n", m+n-1);
1543    formulaStatus = BmcPropertyPassed_c;
1544  }
1545  if(formulaStatus == BmcPropertyPassed_c) {
1546    (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
1547    (void) fprintf(vis_stdout, "#      Termination depth = %d\n", k);
1548  } else if(formulaStatus == BmcPropertyUndecided_c) {
1549    (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
1550    if (options->verbosityLevel != BmcVerbosityNone_c){
1551      (void) fprintf(vis_stdout,
1552                     "# BMC: no counterexample found of length up to %d\n",
1553                     maxK);
1554    }
1555  }
1556  if (options->verbosityLevel != BmcVerbosityNone_c) {
1557    endTime = util_cpu_ctime();
1558    fprintf(vis_stdout, "-- bmc time = %10g\n",
1559            (double)(endTime - startTime) / 1000.0);
1560  }
1561 
1562  array_free(previousResultArray);
1563 
1564  fflush(vis_stdout);
1565  return;
1566} /* BmcCirCUsLtlVerifyGFp() */
1567
1568/**Function********************************************************************
1569
1570  Synopsis    [Use BMC technique to verify a general LTL formulae]
1571
1572  Description [Implements the Bounded Model Checking technique as in the paper
1573  "Symbolic Model Checking without BDDs".  We also have implemented some of the
1574  improvements in the BMC encoding as were described in the paper "Improving
1575  the Encoding of LTL Model Checking into SAT". If snf=1, we use Separated
1576  Normal Form technique to encode LTL properties, otherwise we use the original
1577  encoding. ]
1578
1579  SideEffects []
1580
1581  SeeAlso     []
1582
1583******************************************************************************/
1584
1585void
1586BmcCirCUsLtlVerifyGeneralLtl(
1587    Ntk_Network_t   *network,
1588    Ctlsp_Formula_t *ltl,
1589    st_table        *coiTable,
1590    array_t         *constraintArray,
1591    BmcOption_t     *options,
1592    int             snf)
1593{
1594  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
1595  st_table          *nodeToMvfAigTable = NIL(st_table);
1596  long              startTime, endTime;
1597  boolean           fairness  = (options->fairFile != NIL(FILE));
1598  int               minK = options->minK;
1599  int               maxK = options->maxK;
1600  boolean           boundedFormula;
1601  array_t           *ltlConstraintArray = NIL(array_t);
1602  array_t           *fairnessArray = NIL(array_t);
1603  int               depth, l, bound, f, satFlag, i;
1604  bAigEdge_t        noLoop, loop, ploop; 
1605  bAigEdge_t        result=bAig_NULL, temp, fair;
1606  array_t           *loop_arr = NIL(array_t);
1607  array_t           *objArray;
1608  array_t           *auxObjArray;
1609  st_table          *coiIndexTable;
1610  Ctlsp_Formula_t   *formula;
1611  satInterface_t    *interface;
1612  array_t           *formulaArray = NIL(array_t);
1613  int               nextAction = 0;
1614  /*
1615    Use when proving termination
1616   */
1617  BmcCheckForTermination_t *terminationStatus = 0;
1618  Bmc_PropertyStatus       formulaStatus;
1619
1620  nodeToMvfAigTable = 
1621          (st_table *) Ntk_NetworkReadApplInfo(network,
1622                                               MVFAIG_NETWORK_APPL_KEY);
1623  assert(nodeToMvfAigTable != NIL(st_table));
1624
1625  if(fairness) {
1626    Ctlsp_Formula_t *formula; /* a generic LTL formula */
1627    int              i;       /* iteration variable */
1628
1629    ltlConstraintArray = array_alloc(Ctlsp_Formula_t *, 0);
1630   
1631    arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) {
1632      fprintf(vis_stdout, "Formula: ddd");
1633      Ctlsp_FormulaPrint(vis_stdout, formula);
1634      fprintf(vis_stdout, "\n");
1635      BmcGetCoiForLtlFormula(network, formula, coiTable);
1636      formula =  Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t));
1637      array_insert_last(Ctlsp_Formula_t *, ltlConstraintArray, formula);
1638    }
1639  }
1640  /*
1641    For bounded formulae use a tighter upper bound if possible.
1642  */
1643  boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltl, &depth);
1644  if (boundedFormula && depth < maxK && depth >= minK) {
1645    maxK = depth;
1646  } else {
1647    if(options->inductiveStep !=0){
1648      /*
1649        Use the termination criteria to prove the property passes.   
1650      */
1651      terminationStatus = BmcAutTerminationAlloc(network,
1652                                                 Ctlsp_LtllFormulaNegate(ltl),
1653                                                 constraintArray);
1654      assert(terminationStatus);
1655    }
1656  }
1657  if (options->verbosityLevel != BmcVerbosityNone_c){
1658    (void) fprintf(vis_stdout, "General LTL BMC\n");
1659    if (boundedFormula){
1660      (void) fprintf(vis_stdout, "Bounded formula of depth %d\n", depth);
1661    }
1662    (void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
1663                  minK, maxK, options->step);
1664  }
1665  bAig_ExpandTimeFrame(network, manager, 1, 1);
1666  coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
1667  interface    = 0;
1668  /*
1669    Hold objects
1670  */
1671  objArray = array_alloc(bAigEdge_t, 1);
1672  /*
1673    Hold auxiliary objects (constraints on the path)
1674  */
1675  auxObjArray = array_alloc(bAigEdge_t, 0);
1676
1677  formulaStatus = BmcPropertyUndecided_c;
1678  bound = minK;
1679  if(snf){
1680    formulaArray = Ctlsp_LtlTranslateIntoSNF(ltl);
1681  }
1682  startTime = util_cpu_ctime();
1683  while(bound<=maxK) {
1684    if(options->verbosityLevel == BmcVerbosityMax_c){
1685      fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", bound);
1686    }
1687
1688    loop_arr = 0;
1689    bAig_ExpandTimeFrame(network, manager, bound+1, BMC_INITIAL_STATES);
1690
1691    if(fairness){
1692      /*
1693        In case of fairness constraints, we only include a loop part of BMC
1694        encoding
1695      */
1696      noLoop = bAig_Zero;
1697    } else {
1698      if(snf){
1699        noLoop = BmcCirCUsGenerateLogicForLtlSNF(network, formulaArray, 0, bound, -1);
1700      } else {
1701        noLoop = BmcCirCUsGenerateLogicForLtl(network, ltl, 0, bound, -1);
1702      }
1703    }
1704    result = noLoop;
1705    if(noLoop != bAig_One) {
1706      loop_arr = array_alloc(bAigEdge_t, 0);
1707      for(l=0; l<=bound; l++) {
1708        if(snf){
1709          loop = BmcCirCUsGenerateLogicForLtlSNF(network, formulaArray, 0,
1710                                                 bound, l);
1711        } else { 
1712          loop = BmcCirCUsGenerateLogicForLtl(network, ltl, 0, bound, l);
1713        }
1714        if(loop == bAig_Zero)   continue;
1715
1716        if(fairness) {
1717          fairnessArray = array_alloc(bAigEdge_t, 0);
1718          arrayForEachItem(Ctlsp_Formula_t *, ltlConstraintArray, i, formula) {
1719            fair = BmcCirCUsGenerateLogicForLtl(network, formula, l, bound, -1);
1720            array_insert_last(bAigEdge_t, fairnessArray, fair);
1721          }
1722        }
1723
1724        if(loop != bAig_Zero) {
1725          ploop = BmcCirCUsConnectFromStateToState(network, bound, l, nodeToMvfAigTable, coiIndexTable, 1);
1726          array_insert(bAigEdge_t, loop_arr, l, ploop);
1727          temp = bAig_And(manager, loop, ploop);
1728          if(fairness) {
1729            for(f=0; f < array_n(fairnessArray); f++){
1730              fair = array_fetch(bAigEdge_t, fairnessArray, f);
1731              temp = bAig_And(manager, temp, fair); 
1732            }
1733          }
1734          result = bAig_Or(manager, result, temp);
1735        }
1736        if(fairness){
1737          array_free(fairnessArray);
1738        }
1739      }
1740    }
1741    /*
1742    loop = result;
1743   
1744    if((noLoop == bAig_Zero) && (loop == bAig_Zero)){
1745    */
1746    /*
1747      result = noLoop | loop(0) | loop(1) ... | loop(bound)
1748     */
1749   
1750    if(result == bAig_Zero){
1751      if (options->verbosityLevel != BmcVerbosityNone_c){
1752        fprintf(vis_stdout,"# BMC: the formula is trivially true");
1753        fprintf(vis_stdout," for counterexamples of length %d\n", bound);
1754      }
1755    } else {
1756      array_insert(bAigEdge_t, objArray, 0, result);
1757      options->cnfPrefix = bound;
1758      interface = BmcCirCUsInterfaceWithObjArr(manager, network,
1759                                               objArray, auxObjArray,
1760                                               options, interface);
1761      satFlag = interface->status;
1762      if(satFlag == SAT_SAT) {
1763        formulaStatus = BmcPropertyFailed_c;
1764        break;
1765      }
1766      array_insert_last(bAigEdge_t, auxObjArray, bAig_Not(result));
1767    }
1768    /*
1769      Use the termination check if the the LTL formula is not bounded
1770    */
1771    if(!boundedFormula &&
1772       (formulaStatus == BmcPropertyUndecided_c) &&
1773       (nextAction != 1)){
1774      if((options->inductiveStep !=0) &&
1775         (bound % options->inductiveStep == 0))
1776        {
1777          /*
1778            Check for termination for the current value of k.
1779          */
1780          terminationStatus->k = bound;
1781          BmcCirCUsAutLtlCheckForTermination(network, manager,
1782                                             nodeToMvfAigTable,
1783                                             terminationStatus,
1784                                             coiIndexTable, options);
1785          nextAction = terminationStatus->action;
1786          if(nextAction == 1){
1787            maxK = terminationStatus->k;
1788          } else
1789            if(nextAction == 3){
1790              formulaStatus = BmcPropertyPassed_c;
1791              break;
1792            }
1793        }
1794    } /* terminationStatus */
1795   
1796    if(loop_arr) {
1797      array_free(loop_arr);
1798    }
1799    bound += options->step;
1800  }
1801  array_free(objArray);
1802  array_free(auxObjArray);
1803  st_free_table(coiIndexTable);
1804  sat_FreeInterface(interface);
1805
1806  if(formulaStatus == BmcPropertyUndecided_c){
1807    if(nextAction == 1){
1808      /*
1809        No counterexample of length up to maxK is found. By termination
1810        criterion, formula passes
1811      */
1812      formulaStatus = BmcPropertyPassed_c;
1813    } else 
1814      if (boundedFormula && depth <= options->maxK){
1815        /*
1816          No counterexample of length up to the bounded depth of the LTL formula is
1817          found. Formula passes
1818        */
1819        formulaStatus = BmcPropertyPassed_c;
1820      }
1821  }
1822 
1823  if(options->satSolverError){
1824    (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
1825  } else {
1826    if(formulaStatus == BmcPropertyFailed_c) {
1827      (void) fprintf(vis_stdout, "# BMC: formula failed\n");
1828      if(options->verbosityLevel != BmcVerbosityNone_c){
1829        (void) fprintf(vis_stdout,
1830                       "# BMC: Found a counterexample of length = %d \n", bound);
1831      }
1832      if (options->dbgLevel == 1) {
1833        BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, bound, loop_arr,
1834                                     options, BMC_INITIAL_STATES);
1835      }
1836      if (options->dbgLevel == 2) {
1837        BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, bound, loop_arr,
1838                                     options, BMC_INITIAL_STATES);
1839      }
1840    } else if(formulaStatus == BmcPropertyPassed_c) {
1841      (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
1842      (void) fprintf(vis_stdout, "#      Termination depth = %d\n", maxK);
1843    } else if(formulaStatus == BmcPropertyUndecided_c) {
1844      (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
1845      if (options->verbosityLevel != BmcVerbosityNone_c){
1846        (void) fprintf(vis_stdout,
1847                       "# BMC: no counterexample found of length up to %d\n",
1848                       maxK);
1849      }
1850    }
1851  }
1852 
1853  /*
1854    free all used memories
1855  */
1856  if(terminationStatus){
1857    BmcAutTerminationFree(terminationStatus);
1858  }
1859  if(fairness){
1860    array_free(ltlConstraintArray);
1861  }
1862  if(snf){
1863    Ctlsp_FormulaArrayFree(formulaArray);
1864  }
1865  if (options->verbosityLevel != BmcVerbosityNone_c) {
1866    endTime = util_cpu_ctime();
1867    fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
1868  }
1869
1870  fflush(vis_stdout);
1871}
1872
1873/**Function********************************************************************
1874
1875   Synopsis [Verify LTL property using BMC]
1876
1877   Description [We use the encoding of "Simple Bounded LTL Model
1878   Checking", FMCAD04]
1879
1880   SideEffects []
1881   
1882   SeeAlso     [BmcCirCUsConnectFromStateToState]
1883   
1884******************************************************************************/
1885void
1886BmcCirCUsLtlVerifyGeneralLtlFixPoint(
1887    Ntk_Network_t   *network,
1888    Ctlsp_Formula_t *ltl,
1889    st_table        *coiTable,
1890    array_t         *constraintArray,
1891    BmcOption_t     *options)
1892{
1893  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
1894  st_table          *nodeToMvfAigTable = NIL(st_table);
1895  long              startTime, endTime;
1896  bAigEdge_t        property, fair;
1897  boolean           fairness  = (options->fairFile != NIL(FILE));
1898  int               minK = options->minK;
1899  int               maxK = options->maxK;
1900  boolean           boundedFormula;
1901  array_t           *ltlConstraintArray = NIL(array_t);
1902  array_t           *objArray;
1903  array_t           *auxObjArray;
1904  st_table          *coiIndexTable;
1905  Ctlsp_Formula_t   *formula;
1906  satInterface_t    *interface;
1907  int               nextAction = 0;
1908 
1909  BmcCheckForTermination_t *terminationStatus = 0;
1910  Bmc_PropertyStatus       formulaStatus;
1911 
1912  array_t    *loopArray = NIL(array_t), *smallerExists;
1913  bAigEdge_t tmp, loop, atMostOnce, loopConstraints;
1914  int        i, k, depth, satFlag;
1915 
1916  startTime = util_cpu_ctime();
1917
1918  nodeToMvfAigTable = 
1919          (st_table *) Ntk_NetworkReadApplInfo(network,
1920                                               MVFAIG_NETWORK_APPL_KEY);
1921  assert(nodeToMvfAigTable != NIL(st_table));
1922
1923  if(fairness) {   
1924    ltlConstraintArray = array_alloc(Ctlsp_Formula_t *, 0);
1925
1926    arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) {
1927      BmcGetCoiForLtlFormula(network, formula, coiTable);
1928      formula =  Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t));
1929      array_insert(Ctlsp_Formula_t *, ltlConstraintArray, i, formula);
1930    }
1931  }
1932
1933  /*
1934    For bounded formulae use a tighter upper bound if possible.
1935  */
1936  boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltl, &depth);
1937  if (boundedFormula && depth < maxK && depth >= minK) {
1938    maxK = depth;
1939  } else {
1940    if(options->inductiveStep !=0){
1941      /*
1942        Use the termination criteria to prove the property passes.   
1943      */
1944      terminationStatus = BmcAutTerminationAlloc(network,
1945                                                 Ctlsp_LtllFormulaNegate(ltl),
1946                                                 constraintArray);
1947      assert(terminationStatus);
1948    }
1949  }
1950 
1951  if (options->verbosityLevel != BmcVerbosityNone_c){
1952    (void) fprintf(vis_stdout, "General LTL BMC\n");
1953    (void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
1954                  minK, maxK, options->step);
1955  }
1956
1957  bAig_ExpandTimeFrame(network, manager, 1, BMC_INITIAL_STATES);
1958  /*
1959    We need the above line inorder to run the next one.
1960   */
1961  coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
1962  interface = 0;
1963
1964  /*
1965    Hold objects
1966  */
1967  objArray = array_alloc(bAigEdge_t, 3);
1968  /*
1969    Hold auxiliary objects (constraints on the path)
1970  */
1971  auxObjArray = array_alloc(bAigEdge_t, 0);
1972
1973  formulaStatus = BmcPropertyUndecided_c;
1974  k = minK;
1975  while(k<=maxK) {
1976    if(options->verbosityLevel == BmcVerbosityMax_c){
1977      fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
1978    }
1979    bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES);
1980
1981    loopArray = array_alloc(bAigEdge_t, k+1);
1982    array_insert(bAigEdge_t, loopArray, 0, bAig_Zero);
1983    smallerExists   = array_alloc(bAigEdge_t, k+1);
1984    array_insert(bAigEdge_t, smallerExists, 0, bAig_Zero);
1985
1986    loop = bAig_One;
1987    for(i=1; i<= k; i++){
1988      tmp = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
1989      array_insert(bAigEdge_t, loopArray, i, tmp);
1990      tmp = bAig_Then(manager, tmp,
1991                      BmcCirCUsConnectFromStateToState(network, k-1, i-1, nodeToMvfAigTable,
1992                                                       coiIndexTable, BMC_INITIAL_STATES));
1993      loop = bAig_And(manager, loop, tmp); 
1994    }
1995    array_insert(bAigEdge_t, smallerExists, 1, bAig_Zero);
1996    for(i=1; i<= k; i++){
1997      bAigEdge_t left, right;
1998
1999      left = array_fetch(bAigEdge_t, smallerExists, i);
2000      right = array_fetch(bAigEdge_t, loopArray, i);
2001     
2002      array_insert(bAigEdge_t, smallerExists, i+1,
2003                   bAig_Or(manager, left, right));
2004    }
2005    atMostOnce =  bAig_One;
2006    for(i=1; i<= k; i++){
2007      bAigEdge_t left, right;
2008
2009      left = array_fetch(bAigEdge_t, smallerExists, i);
2010      right = array_fetch(bAigEdge_t, loopArray, i);
2011     
2012      tmp = bAig_Then(manager, left, bAig_Not(right));
2013      atMostOnce = bAig_And(manager, atMostOnce, tmp);
2014    }
2015
2016    loopConstraints = bAig_And(manager, loop, atMostOnce);
2017
2018    property = BmcCirCUsGenerateLogicForLtlFixPoint(network, ltl, 0, k, loopArray);
2019
2020    if(fairness) {
2021      fair = bAig_One;
2022      arrayForEachItem(Ctlsp_Formula_t *, ltlConstraintArray, i, formula) {
2023        fair = bAig_And(manager, fair,
2024                        BmcCirCUsGenerateLogicForLtlFixPoint(network, formula,
2025                                                             0, k, loopArray));
2026      }
2027      array_insert(bAigEdge_t, objArray, 2, fair);
2028    } else {
2029      array_insert(bAigEdge_t, objArray, 2,  bAig_One);
2030    }
2031
2032    array_insert(bAigEdge_t, objArray, 0, loopConstraints);
2033    array_insert(bAigEdge_t, objArray, 1, property);
2034    options->cnfPrefix = k;
2035    interface = BmcCirCUsInterfaceWithObjArr(manager, network,
2036                                             objArray, objArray,
2037                                             options, interface);
2038    array_free(smallerExists);
2039   
2040    satFlag = interface->status;
2041    if(satFlag == SAT_SAT) {
2042      formulaStatus = BmcPropertyFailed_c;
2043      break;
2044    }
2045    array_free(loopArray);
2046    /*
2047      Use the termination check if the the LTL formula is not bounded
2048    */
2049    if(!boundedFormula &&
2050       (formulaStatus == BmcPropertyUndecided_c) &&
2051       (nextAction != 1)){
2052      if((options->inductiveStep !=0) &&
2053         (k % options->inductiveStep == 0))
2054        {
2055          /*
2056            Check for termination for the current value of k.
2057          */
2058          terminationStatus->k = k;
2059          BmcCirCUsAutLtlCheckForTermination(network, manager,
2060                                             nodeToMvfAigTable,
2061                                             terminationStatus,
2062                                             coiIndexTable, options);
2063          nextAction = terminationStatus->action;
2064          if(nextAction == 1){
2065            maxK = terminationStatus->k;
2066          } else 
2067            if(nextAction == 3){
2068              formulaStatus = BmcPropertyPassed_c;
2069              maxK = k;
2070              break;
2071            }
2072
2073        }
2074    } /* terminationStatus */
2075     
2076    k += options->step;
2077  }
2078  array_free(objArray);
2079  array_free(auxObjArray);
2080  st_free_table(coiIndexTable);
2081  sat_FreeInterface(interface);
2082
2083  if(formulaStatus == BmcPropertyUndecided_c){
2084    /*
2085      If no counterexample of length up to a certain bound, then the property
2086      passes.
2087    */
2088    if(nextAction == 1){
2089      formulaStatus = BmcPropertyPassed_c;
2090    } else 
2091      if (boundedFormula && depth <= options->maxK){
2092        formulaStatus = BmcPropertyPassed_c;
2093      }
2094  }
2095  if(options->satSolverError){
2096    (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
2097  } else {
2098    if(formulaStatus == BmcPropertyFailed_c) {
2099      (void) fprintf(vis_stdout, "# BMC: formula failed\n");
2100      if(options->verbosityLevel != BmcVerbosityNone_c){
2101        (void) fprintf(vis_stdout,
2102                       "# BMC: Found a counterexample of length = %d \n", k);
2103      }
2104      if (options->dbgLevel == 1) {
2105        int loop = k;
2106        /*
2107          Adjust loopArray to print a proper counterexample.  The encoding
2108          scheme does not differentiate between loop and no-loop path.  If the
2109          path has a loop, then the path length is k-1.
2110        */
2111        for(i=1; i< k; i++){
2112          bAigEdge_t   v      = array_fetch(bAigEdge_t, loopArray, i+1);
2113          unsigned int lvalue = aig_value(v); 
2114         
2115          if(lvalue == 1) {
2116            loop = k-1;
2117          }
2118          array_insert(bAigEdge_t, loopArray, i, v);
2119        }
2120        if (options->dbgLevel == 1) {
2121          BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable,
2122                                     coiTable, loop, loopArray,
2123                                     options, BMC_INITIAL_STATES);
2124        }
2125        if (options->dbgLevel == 1) {
2126          BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable,
2127                                     coiTable, loop, loopArray,
2128                                     options, BMC_INITIAL_STATES);
2129        }
2130        array_free(loopArray);
2131      }
2132    } else if(formulaStatus == BmcPropertyPassed_c) {
2133      (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
2134      (void) fprintf(vis_stdout, "#      Termination depth = %d\n", maxK);
2135    } else if(formulaStatus == BmcPropertyUndecided_c) {
2136      (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
2137      if (options->verbosityLevel != BmcVerbosityNone_c){
2138        (void) fprintf(vis_stdout,
2139                       "# BMC: no counterexample found of length up to %d\n",
2140                       maxK);
2141      }
2142    }
2143  }
2144 
2145  /*
2146    free all used memories
2147  */
2148  if(terminationStatus){
2149    BmcAutTerminationFree(terminationStatus);
2150  }
2151  if(fairness){
2152     array_free(ltlConstraintArray);
2153  }
2154 
2155  if (options->verbosityLevel != BmcVerbosityNone_c) {
2156    endTime = util_cpu_ctime();
2157    fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
2158  }
2159
2160  fflush(vis_stdout);
2161}
2162
2163
2164/**Function********************************************************************
2165
2166   Synopsis [Apply BMC on a safety properties]
2167
2168   Description []
2169
2170   SideEffects []
2171   
2172   SeeAlso     []
2173   
2174******************************************************************************/
2175
2176void
2177BmcCirCUsLtlCheckSafety(
2178    Ntk_Network_t   *network,
2179    Ctlsp_Formula_t *ltl,
2180    BmcOption_t     *options,
2181    st_table        *coiTable)
2182{
2183  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
2184  st_table          *nodeToMvfAigTable = NIL(st_table);
2185  long              startTime, endTime;
2186  bAigEdge_t        noLoop;
2187  int               depth, satFlag, bound;
2188  int               minK = options->minK;
2189  int               maxK = options->maxK;
2190  int               boundedFormula;
2191  array_t           *previousResultArray;
2192  satInterface_t    *interface;
2193  array_t           *objArray;
2194  BmcCheckForTermination_t *terminationStatus = 0;
2195  Bmc_PropertyStatus       formulaStatus;
2196  st_table          *coiIndexTable;
2197
2198  assert(Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(ltl));
2199 
2200  startTime = util_cpu_ctime();
2201
2202  nodeToMvfAigTable = 
2203    (st_table *) Ntk_NetworkReadApplInfo(network,
2204                                         MVFAIG_NETWORK_APPL_KEY);
2205  assert(nodeToMvfAigTable != NIL(st_table));
2206 
2207  /*
2208    For bounded formulae use a tighter upper bound if possible.
2209  */
2210  boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltl, &depth);
2211  if (boundedFormula && depth < maxK && depth >= minK) {
2212    maxK = depth;
2213  } else {
2214    if(options->inductiveStep !=0){
2215      /*
2216        Use the termination criteria to prove the property passes.   
2217      */
2218      terminationStatus = BmcAutTerminationAlloc(network,
2219                                                 Ctlsp_LtllFormulaNegate(ltl),
2220                                                 NIL(array_t));
2221      assert(Ltl_AutomatonGetStrength(terminationStatus->automaton) == 0); /* Terminal Automaton*/
2222      assert(terminationStatus);
2223    }
2224  }
2225  if (options->verbosityLevel != BmcVerbosityNone_c){
2226    (void) fprintf(vis_stdout, "saftey LTL BMC\n");
2227    if (boundedFormula){
2228      (void) fprintf(vis_stdout, "Bounded formula of depth %d\n", depth);
2229    }
2230    (void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
2231                  minK, maxK, options->step);
2232  }
2233  satFlag   = SAT_UNSAT;
2234  bAig_ExpandTimeFrame(network, manager, 0, BMC_INITIAL_STATES);
2235  coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
2236  interface = 0;
2237  formulaStatus = BmcPropertyUndecided_c;
2238  /*
2239    Hold objects
2240  */
2241  objArray = array_alloc(bAigEdge_t, 1);
2242
2243  previousResultArray = array_alloc(bAigEdge_t, 0);
2244  bound=minK;
2245  while(bound<=maxK) {
2246   
2247    if(options->verbosityLevel == BmcVerbosityMax_c)
2248      fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", bound);
2249    fflush(vis_stdout);
2250
2251    bAig_ExpandTimeFrame(network, manager, bound+1, BMC_INITIAL_STATES);
2252
2253    /*
2254      A counterexample to a safety property is finite path at which the
2255      safety property does not hold.
2256     */
2257    noLoop = BmcCirCUsGenerateLogicForLtl(network, ltl, 0, bound, -1);
2258    array_insert(bAigEdge_t, objArray, 0, noLoop);
2259   
2260    options->cnfPrefix = bound;
2261    interface = BmcCirCUsInterfaceWithObjArr(manager, network,
2262                                             objArray,
2263                                             previousResultArray,
2264                                             options,
2265                                             interface);
2266    satFlag = interface->status;
2267    if(satFlag == SAT_SAT) {
2268      formulaStatus = BmcPropertyFailed_c;
2269      break;
2270    }
2271    array_insert_last(bAigEdge_t, previousResultArray, bAig_Not(noLoop));
2272
2273    /*
2274      Use the termination check if the the LTL formula is not bounded
2275    */
2276    if(!boundedFormula &&
2277       (options->inductiveStep !=0) &&
2278       (bound % options->inductiveStep == 0))
2279      {
2280        terminationStatus->k = bound;
2281        BmcCirCUsAutLtlCheckTerminalAutomaton(network, manager,
2282                                              nodeToMvfAigTable,
2283                                              terminationStatus,
2284                                              coiIndexTable, options);
2285        if(terminationStatus->action == 1){
2286          formulaStatus = BmcPropertyPassed_c;
2287          maxK = bound;
2288          break;
2289        }
2290      }
2291    bound += options->step;
2292  }
2293  array_free(objArray);
2294  array_free(previousResultArray);
2295  sat_FreeInterface(interface);
2296
2297  if ((formulaStatus != BmcPropertyFailed_c) && boundedFormula && depth <= options->maxK){
2298    /*
2299      No counterexample of length up to the bounded depth of the LTL formula is
2300      found. Formula passes
2301    */
2302    formulaStatus = BmcPropertyPassed_c;
2303  }
2304 
2305  if(options->satSolverError){
2306    (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
2307  } else {
2308    if(formulaStatus == BmcPropertyFailed_c) {
2309      (void) fprintf(vis_stdout, "# BMC: formula failed\n");
2310      if(options->verbosityLevel != BmcVerbosityNone_c){
2311        (void) fprintf(vis_stdout,
2312                       "# BMC: Found a counterexample of length = %d \n", bound);
2313      }
2314      if (options->dbgLevel == 1) {
2315        BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, bound, NIL(array_t),
2316                                     options, BMC_INITIAL_STATES);
2317      }
2318      if (options->dbgLevel == 2) {
2319        BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, bound, NIL(array_t),
2320                                     options, BMC_INITIAL_STATES);
2321      }
2322    } else if(formulaStatus == BmcPropertyPassed_c) {
2323      (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
2324      (void) fprintf(vis_stdout, "#      Termination depth = %d\n", maxK);
2325    } else if(formulaStatus == BmcPropertyUndecided_c) {
2326      (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
2327      if (options->verbosityLevel != BmcVerbosityNone_c){
2328        (void) fprintf(vis_stdout,
2329                       "# BMC: no counterexample found of length up to %d \n",
2330                       maxK);
2331      }
2332    }
2333  }
2334
2335  if (options->verbosityLevel != BmcVerbosityNone_c) {
2336    endTime = util_cpu_ctime();
2337    fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
2338  }
2339  fflush(vis_stdout); 
2340  return;
2341
2342}
2343
2344
2345/**Function********************************************************************
2346
2347   Synopsis [Build AIG for a transition from state "from" to state "to"]
2348
2349   Description [The state next to "from" equal to "to".  (from+1) == to]
2350
2351   SideEffects []
2352   
2353   SeeAlso     []
2354   
2355******************************************************************************/
2356
2357bAigEdge_t
2358BmcCirCUsConnectFromStateToState(
2359    Ntk_Network_t   *network,
2360    int from,
2361    int to,
2362    st_table *nodeToMvfAigTable,
2363    st_table *coiIndexTable,
2364    int withInitialState)
2365{
2366  bAigEdge_t *fli, *tli;
2367  bAigEdge_t loop, tv;
2368  int l, index, nLatches;
2369  bAigTimeFrame_t *timeframe;
2370  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
2371
2372  if(withInitialState)  timeframe = manager->timeframe;
2373  else                  timeframe = manager->timeframeWOI;
2374
2375  fli = timeframe->latchInputs[from+1];
2376  tli = timeframe->latchInputs[to]; 
2377  loop = bAig_One;
2378  nLatches = timeframe->nLatches;
2379  for(l=0; l<nLatches; l++) {
2380    if(!st_lookup_int(coiIndexTable, (char *)(long)l, &index))  continue;
2381    tv = bAig_Eq(manager, fli[l], tli[l]);
2382    loop = bAig_And(manager, tv, loop);
2383    if(loop == bAig_Zero)       break;
2384  }
2385  return(loop);
2386}
2387
2388
2389/**Function********************************************************************
2390
2391   Synopsis [Create AIG graph for simple path constraint]
2392
2393   Description [Create AIG graph that constrains a path starting from
2394   'fromState' and ending at 'toState' to be a simple path.  A simple
2395   path is a path such that every state in the path is distinct. i.e
2396   for all states in the path Si != Sj for fromState <= i < j <=
2397   toState.]
2398
2399   SideEffects []
2400   
2401   SeeAlso     []
2402   
2403******************************************************************************/
2404bAigEdge_t
2405BmcCirCUsSimlePathConstraint(
2406  Ntk_Network_t *network,
2407  int           fromState,
2408  int           toState,
2409  st_table      *nodeToMvfAigTable,
2410  st_table      *coiIndexTable,
2411  int withInitialState)
2412{
2413  int             i, j; 
2414  bAigEdge_t      loop, nLoop;
2415  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
2416
2417  nLoop = bAig_One;
2418  for(i=fromState+1; i<=toState; i++) {
2419    for(j=fromState; j<i; j++) {
2420      /*
2421        We want state Si == Sj, but the following function returns
2422        S(i+1) == Sj.  So we call the function with i-1.
2423      */
2424      loop = BmcCirCUsConnectFromStateToState(
2425             network, i-1, j, nodeToMvfAigTable, coiIndexTable, withInitialState);
2426      nLoop = bAig_And(manager, nLoop, bAig_Not(loop));
2427    }
2428  }
2429  return(nLoop);
2430} /* BmcCirCUsSimplePathConstraint */
2431
2432
2433/**Function********************************************************************
2434
2435   Synopsis [Build an AIG graph for a simple path]
2436
2437   Description []
2438
2439   SideEffects []
2440   
2441   SeeAlso     []
2442   
2443******************************************************************************/
2444
2445bAigEdge_t
2446BmcCirCUsGenerateSimplePath(
2447        Ntk_Network_t   *network,
2448        int from,
2449        int to,
2450        st_table *nodeToMvfAigTable,
2451        st_table *coiIndexTable,
2452        int withInitialState)
2453{
2454int i, j; 
2455bAigEdge_t loop, nloop;
2456mAig_Manager_t    *manager;
2457   
2458  manager = Ntk_NetworkReadMAigManager(network);
2459
2460  bAig_ExpandTimeFrame(network, manager, to, withInitialState);
2461
2462  nloop = bAig_One;
2463  for(i=from+1; i<=to; i++) {
2464    for(j=from; j<i; j++) {
2465      loop = BmcCirCUsConnectFromStateToState(
2466             network, i-1, j, nodeToMvfAigTable, coiIndexTable, withInitialState);
2467      nloop = bAig_And(manager, nloop, bAig_Not(loop));
2468    }
2469  }
2470  return(nloop);
2471}
2472
2473
2474/**Function********************************************************************
2475
2476   Synopsis []
2477
2478   Description []
2479
2480   SideEffects []
2481   
2482   SeeAlso     []
2483   
2484******************************************************************************/
2485
2486void
2487BmcCirCUsPrintCounterExample(
2488  Ntk_Network_t   *network,
2489  st_table        *nodeToMvfAigTable,
2490  st_table        *coiTable,
2491  int             length,
2492  array_t         *loop_arr,
2493  BmcOption_t     *options,
2494  int withInitialState)
2495{
2496  int *prevLatchValues, *prevInputValues;
2497  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
2498  int loop, k;
2499  unsigned int lvalue;
2500  bAigEdge_t v;
2501  array_t *latchArr;
2502  lsGen gen;
2503  Ntk_Node_t *node;
2504  int tmp;
2505  bAigTimeFrame_t *timeframe;
2506  FILE *dbgOut = NULL;
2507
2508  latchArr = array_alloc(Ntk_Node_t *, 0);
2509  Ntk_NetworkForEachLatch(network, gen, node){
2510    if (st_lookup_int(coiTable, (char *) node, &tmp)){
2511      array_insert_last(Ntk_Node_t *, latchArr, node);
2512    }
2513  }
2514
2515  if(options->dbgOut)
2516  {
2517    dbgOut = vis_stdout;
2518    vis_stdout = options->dbgOut;
2519  }
2520
2521  /** check index such as, k, length, loop */
2522
2523  if(withInitialState)  timeframe = manager->timeframe;
2524  else                  timeframe = manager->timeframeWOI;
2525
2526  prevLatchValues = ALLOC(int, timeframe->nLatches);
2527  prevInputValues = ALLOC(int, timeframe->nInputs);
2528
2529  loop = -1;
2530  if(loop_arr != 0) {
2531    for(k=array_n(loop_arr)-1; k>=0; k--) {
2532      v = array_fetch(bAigEdge_t, loop_arr, k);
2533      lvalue = aig_value(v);
2534      if(lvalue == 1) {
2535        loop = k;
2536        break;
2537      }
2538    }
2539  }
2540  for(k=0; k<=length; k++) {
2541    if(k == 0) fprintf(vis_stdout, "\n--State %d:\n", k);
2542    else       fprintf(vis_stdout, "\n--Goes to state %d:\n", k);
2543 
2544    printSatValue(manager, nodeToMvfAigTable, 
2545                    timeframe->li2index, 
2546                    timeframe->latchInputs, latchArr,
2547                    k, prevLatchValues);
2548
2549    if(options->printInputs == TRUE && k!=0) {
2550      fprintf(vis_stdout, "--On input:\n");
2551      printSatValue(manager, nodeToMvfAigTable, 
2552                    timeframe->pi2index,
2553                    timeframe->inputs, timeframe->inputArr,
2554                    k-1, prevInputValues);
2555    }
2556  }
2557
2558  if(loop >=0) {
2559    fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
2560
2561    printSatValue(manager, nodeToMvfAigTable, 
2562                    timeframe->li2index,
2563                    timeframe->latchInputs, latchArr,
2564                    loop, prevLatchValues);
2565
2566    if(options->printInputs == TRUE && k!=0) {
2567      fprintf(vis_stdout, "--On input:\n");
2568      printSatValue(manager, nodeToMvfAigTable, 
2569                    timeframe->pi2index,
2570                    timeframe->inputs, timeframe->inputArr,
2571                    length, prevInputValues);
2572    }
2573  }
2574
2575  array_free(latchArr);
2576  if(options->dbgOut)
2577  {
2578    vis_stdout = dbgOut;
2579  }
2580  return;
2581}
2582
2583
2584
2585/**Function********************************************************************
2586
2587   Synopsis [Prints the counter-example in Aiger format.]
2588
2589   Description [The Aiger format is as follows,
2590                currentState, input, output, nextState
2591                the names of the variables aren't printed rather their values
2592                are only printed, -i option is set by default.]
2593
2594   SideEffects []
2595   
2596   SeeAlso     []
2597   
2598******************************************************************************/
2599
2600void
2601BmcCirCUsPrintCounterExampleAiger(
2602  Ntk_Network_t   *network,
2603  st_table        *nodeToMvfAigTable,
2604  st_table        *coiTable,
2605  int             length,
2606  array_t         *loop_arr,
2607  BmcOption_t     *options,
2608  int withInitialState)
2609{
2610  int *prevLatchValues, *prevInputValues;
2611  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
2612  int loop, k;
2613  unsigned int lvalue;
2614  bAigEdge_t v;
2615  array_t *latchArr;
2616  lsGen gen;
2617  Ntk_Node_t *node;
2618  int tmp;
2619  bAigTimeFrame_t *timeframe;
2620  FILE *dbgOut = NULL;
2621
2622  latchArr = array_alloc(Ntk_Node_t *, 0);
2623  Ntk_NetworkForEachLatch(network, gen, node){
2624    if (st_lookup_int(coiTable, (char *) node, &tmp)){
2625      array_insert_last(Ntk_Node_t *, latchArr, node);
2626    }
2627  }
2628
2629  /* writing into a file is not being done in a standard way, need to confirm
2630     the writing of trace into a file with the vis standard */
2631
2632  if(options->dbgOut)
2633  {
2634    dbgOut = vis_stdout;
2635    vis_stdout = options->dbgOut;
2636  }
2637
2638  /** check index such as, k, length, loop */
2639
2640  if(withInitialState)  timeframe = manager->timeframe;
2641  else                  timeframe = manager->timeframeWOI;
2642
2643  prevLatchValues = ALLOC(int, timeframe->nLatches);
2644  prevInputValues = ALLOC(int, timeframe->nInputs);
2645
2646  loop = -1;
2647  if(loop_arr != 0) {
2648    for(k=array_n(loop_arr)-1; k>=0; k--) {
2649      v = array_fetch(bAigEdge_t, loop_arr, k);
2650      lvalue = aig_value(v);
2651      if(lvalue == 1) {
2652        loop = k;
2653        break;
2654      }
2655    }
2656  }
2657 
2658  /* we need to get rid of the file generation for next vis release and look
2659     into ntk package so that the original order can be maintained */
2660
2661  FILE *order = Cmd_FileOpen("inputOrder.txt", "w", NIL(char *), 0) ;
2662  for(k=0; k<array_n(timeframe->inputArr); k++)
2663  {
2664    node = array_fetch(Ntk_Node_t *, timeframe->inputArr, k);
2665    fprintf(order, "%s\n", Ntk_NodeReadName(node));
2666  }
2667  fclose(order);
2668   
2669  for(k=0; k<=length; k++) {
2670    /*if(k == 0) fprintf(vis_stdout, "\n--State %d:\n", k);
2671    else       fprintf(vis_stdout, "\n--Goes to state %d:\n", k);*/
2672
2673    /*if((loop>=0)||(k<length))
2674    { */
2675      printSatValueAiger(manager, nodeToMvfAigTable, 
2676                    timeframe->li2index, 
2677                    timeframe->latchInputs, latchArr,
2678                    k, prevLatchValues);
2679      fprintf(vis_stdout, " ");
2680
2681    if((loop<0)||(k<length))
2682    { 
2683      if(k!=length+1) {
2684        printSatValueAiger(manager, nodeToMvfAigTable, 
2685                    timeframe->pi2index,
2686                    timeframe->inputs, timeframe->inputArr,
2687                    k, prevInputValues);
2688        fprintf(vis_stdout, " ");
2689      }
2690
2691      if(k!=length+1) {
2692        printSatValueAiger(manager, nodeToMvfAigTable, 
2693                    timeframe->o2index,
2694                    timeframe->outputs, timeframe->outputArr,
2695                    k, prevInputValues);
2696        fprintf(vis_stdout, " ");
2697      }
2698
2699      if(k!=length+1) {
2700        printSatValueAiger(manager, nodeToMvfAigTable,
2701                    timeframe->li2index,
2702                    timeframe->latchInputs, latchArr,
2703                    k+1, prevLatchValues);
2704        fprintf(vis_stdout, " ");
2705      }
2706      if((loop < 0)||(k!=length))
2707      {
2708        fprintf(vis_stdout, "\n");
2709      }
2710    }
2711  }
2712
2713  if(loop >=0) {
2714    /*fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);*/
2715
2716    if(k!=0) {
2717      printSatValueAiger(manager, nodeToMvfAigTable,
2718                    timeframe->pi2index,
2719                    timeframe->inputs, timeframe->inputArr,
2720                    length, prevInputValues);
2721      fprintf(vis_stdout, " ");
2722    }
2723
2724    printSatValueAiger(manager, nodeToMvfAigTable,
2725                    timeframe->o2index,
2726                    timeframe->outputs, timeframe->outputArr,
2727                    k, prevInputValues);
2728    fprintf(vis_stdout, " ");
2729
2730    printSatValueAiger(manager, nodeToMvfAigTable, 
2731                    timeframe->li2index,
2732                    timeframe->latchInputs, latchArr,
2733                    loop, prevLatchValues);
2734   
2735    fprintf(vis_stdout, "\n");
2736  }
2737
2738  array_free(latchArr);
2739  if(options->dbgOut)
2740  {
2741    vis_stdout = dbgOut;
2742  }
2743  return;
2744} /* BmcCirCUsPrintCounterExampleAiger */
2745
2746/**Function********************************************************************
2747
2748   Synopsis []
2749
2750   Description []
2751
2752   SideEffects []
2753   
2754   SeeAlso     []
2755   
2756******************************************************************************/
2757
2758
2759static int
2760printSatValue(
2761    bAig_Manager_t *manager,
2762    st_table        *nodeToMvfAigTable,
2763    st_table *li2index,
2764    bAigEdge_t **baigArr,
2765    array_t *nodeArr, 
2766    int bound,
2767    int *prevValue)
2768{
2769  Ntk_Node_t * node;
2770  int value, lvalue;
2771  char *symbolicValue;
2772  bAigEdge_t *li, v, tv;
2773  int i, j, timeframe, index;
2774  int changed=0;
2775  MvfAig_Function_t  *mvfAig;
2776
2777  timeframe = bound;
2778  li = baigArr[timeframe];
2779  for(i=0; i<array_n(nodeArr); i++) {
2780    if(timeframe == 0)  prevValue[i] = -1;
2781    node = array_fetch(Ntk_Node_t *, nodeArr, i);
2782    mvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
2783
2784    if(mvfAig == 0)     continue;
2785
2786    value = -1;
2787    for (j=0; j< array_n(mvfAig); j++) {
2788      v = MvfAig_FunctionReadComponent(mvfAig, j);
2789      index = -1;
2790      if(!st_lookup_int(li2index, (char *)v, &index)) {
2791        fprintf(vis_stdout, "printSatValueERROR \n");
2792      }
2793      v = li[index];
2794      if(v == bAig_One) {
2795        value = j;
2796        break;
2797      }
2798
2799      if(v != bAig_Zero) {
2800        tv = bAig_GetCanonical(manager, v);
2801        lvalue = bAig_GetValueOfNode(manager, tv);
2802        if(lvalue == 1){       
2803          value = j;
2804          break;
2805        }
2806      }
2807    }
2808    if(value >=0) {
2809      if (value != prevValue[i]){
2810        Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
2811        prevValue[i] = value;
2812        changed = 1;
2813        if (Var_VariableTestIsSymbolic(nodeVar)) {
2814          symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
2815          fprintf(vis_stdout,"%s:%s\n",  Ntk_NodeReadName(node), symbolicValue);
2816        } 
2817        else {
2818          fprintf(vis_stdout,"%s:%d\n",  Ntk_NodeReadName(node), value);
2819        }
2820      }
2821    }
2822  } /* for j loop */
2823  if (changed == 0){
2824    fprintf(vis_stdout, "<Unchanged>\n");
2825  }
2826  return 0;
2827}
2828
2829/**Function********************************************************************
2830
2831   Synopsis [Prints the counter-example in the Aiger Format.]
2832
2833   Description []
2834
2835   SideEffects []
2836   
2837   SeeAlso     [BmcCirCUsPrintCounterExampleAiger]
2838   
2839******************************************************************************/
2840
2841static int
2842printSatValueAiger(
2843    bAig_Manager_t *manager,
2844    st_table        *nodeToMvfAigTable,
2845    st_table *li2index,
2846    bAigEdge_t **baigArr,
2847    array_t *nodeArr, 
2848    int bound,
2849    int *prevValue)
2850{
2851  Ntk_Node_t * node;
2852  int value, lvalue;
2853  char *symbolicValue;
2854  bAigEdge_t *li, v, tv;
2855  int i, j, timeframe, index;
2856  MvfAig_Function_t  *mvfAig;
2857
2858  timeframe = bound;
2859  li = baigArr[timeframe];
2860  for(i=0; i<array_n(nodeArr); i++) {
2861    if(timeframe == 0)  prevValue[i] = -1;
2862    node = array_fetch(Ntk_Node_t *, nodeArr, i);
2863    mvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
2864
2865    if(mvfAig == 0)     continue;
2866
2867    value = -1;
2868    for (j=0; j< array_n(mvfAig); j++) {
2869      v = MvfAig_FunctionReadComponent(mvfAig, j);
2870      index = -1;
2871      if(!st_lookup_int(li2index, (char *)v, &index)) {
2872        fprintf(vis_stdout, "printSatValueERROR \n");
2873      }
2874      v = li[index];
2875      if(v == bAig_One) {
2876        value = j;
2877        break;
2878      }
2879
2880      if(v != bAig_Zero) {
2881        tv = bAig_GetCanonical(manager, v);
2882        lvalue = bAig_GetValueOfNode(manager, tv);
2883        if(lvalue == 1){       
2884          value = j;
2885          break;
2886        }
2887      }
2888    }
2889    if(value >=0) {
2890      Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
2891      prevValue[i] = value;
2892      if (Var_VariableTestIsSymbolic(nodeVar)) {
2893        symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
2894        fprintf(vis_stdout,"%s", symbolicValue);
2895      } 
2896      else {
2897        fprintf(vis_stdout,"%d", value);
2898      }
2899    }
2900    else
2901    {
2902      fprintf(vis_stdout,"x");
2903    }
2904  } /* for j loop */
2905  return 0;
2906} /* printSatValueAiger */
2907
2908/**Function********************************************************************
2909
2910  Synopsis [Builds AND/INVERTER graph (aig) for a propsitional formula
2911  at time frame bound]
2912
2913  Description [Builds AND/INVERTER graph for a propsitional formula at
2914  time frame bound.  Returns bAig ID of the function that is quivalent
2915  to the propositional fomula]
2916
2917  SideEffects []
2918
2919  SeeAlso     []
2920
2921******************************************************************************/
2922bAigEdge_t
2923BmcCirCUsCreatebAigOfPropFormula(
2924    Ntk_Network_t *network,
2925    bAig_Manager_t *manager,
2926    int bound,
2927    Ctlsp_Formula_t *ltl,
2928    int withInitialState)
2929{
2930  int index;
2931  bAigEdge_t result, left, right, *li;
2932  bAigTimeFrame_t *timeframe;
2933
2934  if (ltl == NIL(Ctlsp_Formula_t))      return mAig_NULL; 
2935  if (ltl->type == Ctlsp_TRUE_c)        return mAig_One; 
2936  if (ltl->type == Ctlsp_FALSE_c)       return mAig_Zero; 
2937
2938  assert(Ctlsp_isPropositionalFormula(ltl));
2939 
2940  if(withInitialState) timeframe = manager->timeframe;
2941  else                 timeframe = manager->timeframeWOI;
2942
2943  if (ltl->type == Ctlsp_ID_c){
2944      char *nodeNameString  = Ctlsp_FormulaReadVariableName(ltl);
2945      char *nodeValueString = Ctlsp_FormulaReadValueName(ltl);
2946      Ntk_Node_t *node      = Ntk_NetworkFindNodeByName(network, nodeNameString);
2947
2948      Var_Variable_t *nodeVar;
2949      int             nodeValue;
2950
2951      MvfAig_Function_t  *tmpMvfAig;
2952      st_table           *nodeToMvfAigTable; /* maps each node to its mvfAig */
2953     
2954      if (node == NIL(Ntk_Node_t)) {
2955        char   *nameKey;
2956        char   tmpName[100];
2957       
2958        sprintf(tmpName, "%s_%d", nodeNameString, bound);
2959        nameKey = util_strsav(tmpName);
2960
2961        result  = bAig_FindNodeByName(manager, nameKey);
2962        if(result == bAig_NULL){
2963           result = bAig_CreateVarNode(manager, nameKey); 
2964        } else {
2965         
2966          FREE(nameKey);
2967        }
2968
2969       
2970        return result;
2971      }
2972
2973      nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
2974      assert(nodeToMvfAigTable != NIL(st_table));
2975
2976      tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
2977      if (tmpMvfAig ==  NIL(MvfAig_Function_t)){
2978          tmpMvfAig = Bmc_NodeBuildMVF(network, node);
2979          array_free(tmpMvfAig);
2980          tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
2981      }
2982     
2983      nodeVar = Ntk_NodeReadVariable(node);
2984      if (Var_VariableTestIsSymbolic(nodeVar)) {
2985        nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
2986        if ( nodeValue == -1 ) {
2987          (void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
2988          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
2989          return mAig_NULL;
2990        }
2991      }
2992      else { 
2993        int check;   
2994         check = StringCheckIsInteger(nodeValueString, &nodeValue);
2995         if( check == 0 ) {
2996          (void) fprintf(vis_stderr,"Illegal value in the RHS\n");
2997          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
2998          return mAig_NULL;
2999         }
3000         if( check == 1 ) {
3001          (void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
3002          (void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
3003          return mAig_NULL;
3004         }
3005         if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
3006          (void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
3007          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
3008          return mAig_NULL;
3009
3010         }
3011      }
3012      result = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue);
3013      result = bAig_GetCanonical(manager, result);
3014      if(st_lookup_int(timeframe->li2index, (char *)result, &index)) {
3015        li = timeframe->latchInputs[bound];
3016        result = bAig_GetCanonical(manager, li[index]);
3017      }
3018      else if(st_lookup_int(timeframe->o2index, (char *)result, &index)) {
3019        li = timeframe->outputs[bound];
3020        result = bAig_GetCanonical(manager, li[index]);
3021      }
3022      else if(st_lookup_int(timeframe->i2index, (char *)result, &index)) {
3023        li = timeframe->internals[bound];
3024        result = bAig_GetCanonical(manager, li[index]);
3025      }
3026      return result;
3027  }
3028
3029  left = BmcCirCUsCreatebAigOfPropFormula(network, manager, bound, ltl->left, withInitialState);
3030  if (left == mAig_NULL){
3031    return mAig_NULL;
3032  } 
3033  right = BmcCirCUsCreatebAigOfPropFormula(network, manager, bound, ltl->right, withInitialState);
3034  if (right == mAig_NULL && ltl->type ==Ctlsp_NOT_c ){
3035    return mAig_Not(left);
3036  } 
3037  else if(right == mAig_NULL) {
3038    return mAig_NULL;
3039  }
3040
3041  switch(ltl->type) {
3042/**
3043    case Ctlsp_NOT_c:
3044      result = mAig_Not(left);
3045      break;
3046      **/
3047    case Ctlsp_OR_c:
3048      result = mAig_Or(manager, left, right);
3049      break;
3050    case Ctlsp_AND_c:
3051      result = mAig_And(manager, left, right);
3052      break;
3053    case Ctlsp_THEN_c:
3054      result = mAig_Then(manager, left, right); 
3055      break;
3056    case Ctlsp_EQ_c:
3057      result = mAig_Eq(manager, left, right);
3058      break;
3059    case Ctlsp_XOR_c:
3060      result = mAig_Xor(manager, left, right);
3061      break;
3062    default:
3063      fail("Unexpected type");
3064  }
3065  return result;
3066} /* BmcCirCUsCreatebAigOfPropFormula */
3067
3068/**Function********************************************************************
3069
3070  Synopsis [Builds AND/INVERTER graph (aig) for a propsitional formula]
3071
3072  Description [Builds AND/INVERTER graph for a propsitional formula.
3073  Returns bAig ID of the function that is quivalent to the propositional
3074  fomula]
3075
3076  SideEffects []
3077
3078  SeeAlso     []
3079
3080******************************************************************************/
3081
3082bAigEdge_t
3083BmcCirCUsCreatebAigOfPropFormulaOriginal(
3084    Ntk_Network_t *network,
3085    bAig_Manager_t *manager,
3086    Ctlsp_Formula_t *ltl
3087    )
3088{
3089  bAigEdge_t result, left, right;
3090
3091  if (ltl == NIL(Ctlsp_Formula_t))      return mAig_NULL; 
3092  if (ltl->type == Ctlsp_TRUE_c)        return mAig_One; 
3093  if (ltl->type == Ctlsp_FALSE_c)       return mAig_Zero; 
3094
3095  assert(Ctlsp_isPropositionalFormula(ltl));
3096   
3097  if (ltl->type == Ctlsp_ID_c){
3098      char *nodeNameString  = Ctlsp_FormulaReadVariableName(ltl);
3099      char *nodeValueString = Ctlsp_FormulaReadValueName(ltl);
3100      Ntk_Node_t *node      = Ntk_NetworkFindNodeByName(network, nodeNameString);
3101
3102      Var_Variable_t *nodeVar;
3103      int             nodeValue;
3104
3105      MvfAig_Function_t  *tmpMvfAig;
3106      st_table           *nodeToMvfAigTable; /* maps each node to its mvfAig */
3107     
3108      if (node == NIL(Ntk_Node_t)) {
3109          (void) fprintf(vis_stderr, "bmc error: Could not find node corresponding to the name\t %s\n", nodeNameString);
3110          return mAig_NULL;
3111      }
3112
3113      nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
3114      if (nodeToMvfAigTable == NIL(st_table)){
3115         (void) fprintf(vis_stderr, "bmc error: please run build_partiton_maigs first");
3116         return mAig_NULL;
3117      }
3118      tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
3119      if (tmpMvfAig ==  NIL(MvfAig_Function_t)){
3120          tmpMvfAig = Bmc_NodeBuildMVF(network, node);
3121          array_free(tmpMvfAig);
3122          tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
3123      }
3124     
3125      nodeVar = Ntk_NodeReadVariable(node);
3126      if (Var_VariableTestIsSymbolic(nodeVar)) {
3127        nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
3128        if ( nodeValue == -1 ) {
3129          (void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
3130          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
3131          return mAig_NULL;
3132        }
3133      }
3134      else { 
3135        int check;   
3136         check = StringCheckIsInteger(nodeValueString, &nodeValue);
3137         if( check == 0 ) {
3138          (void) fprintf(vis_stderr,"Illegal value in the RHS\n");
3139          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
3140          return mAig_NULL;
3141         }
3142         if( check == 1 ) {
3143          (void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
3144          (void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
3145          return mAig_NULL;
3146         }
3147         if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
3148          (void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
3149          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
3150          return mAig_NULL;
3151
3152         }
3153      }
3154      result = bAig_GetCanonical(manager,
3155              MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue));
3156      return result;
3157  }
3158
3159  left = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager, ltl->left);
3160  if (left == mAig_NULL){
3161    return mAig_NULL;
3162  } 
3163  right = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager, ltl->right);
3164  if (right == mAig_NULL && ltl->type ==Ctlsp_NOT_c ){
3165    return mAig_Not(left);
3166  } 
3167  else if(right == mAig_NULL) {
3168    return mAig_NULL;
3169  }
3170
3171  switch(ltl->type) {
3172/**
3173    case Ctlsp_NOT_c:
3174      result = mAig_Not(left);
3175      break;
3176      **/
3177    case Ctlsp_OR_c:
3178      result = mAig_Or(manager, left, right);
3179      break;
3180    case Ctlsp_AND_c:
3181      result = mAig_And(manager, left, right);
3182      break;
3183    case Ctlsp_THEN_c:
3184      result = mAig_Then(manager, left, right); 
3185      break;
3186    case Ctlsp_EQ_c:
3187      result = mAig_Eq(manager, left, right);
3188      break;
3189    case Ctlsp_XOR_c:
3190      result = mAig_Xor(manager, left, right);
3191      break;
3192    default:
3193      fail("Unexpected LTL type");
3194  }
3195  return result;
3196} /* BmcCirCUsCreatebAigOfPropFormulaOriginal */
3197
3198/**Function********************************************************************
3199
3200   Synopsis [ Check the given string is integer]
3201
3202   Description [ Check the given string is integer]
3203
3204   SideEffects []
3205   
3206   SeeAlso     []
3207   
3208******************************************************************************/
3209
3210static int
3211StringCheckIsInteger(
3212  char *string,
3213  int *value)
3214{
3215  char *ptr;
3216  long l;
3217 
3218  l = strtol (string, &ptr, 0) ;
3219  if(*ptr != '\0')
3220    return 0;
3221  if ((l > MAXINT) || (l < -1 - MAXINT))
3222    return 1 ;
3223  *value = (int) l;
3224  return 2 ;
3225}
3226
3227
3228/**Function********************************************************************
3229
3230   Synopsis [ CirCUs interface for bounded model checking.]
3231
3232   Description [ CirCUs interface for bounded model checking. ]
3233
3234   SideEffects []
3235   
3236   SeeAlso     []
3237   
3238******************************************************************************/
3239
3240satInterface_t *
3241BmcCirCUsInterface(
3242    bAig_Manager_t *manager,
3243    Ntk_Network_t  *network,
3244    bAigEdge_t     object,
3245    array_t        *auxObjectArray,
3246    BmcOption_t    *bmcOption,
3247    satInterface_t *interface)
3248{
3249satManager_t   *cm;
3250satOption_t    *option;
3251satLevel_t *d;
3252int i, size;
3253bAigEdge_t tv;
3254
3255/* allocate sat manager */
3256  cm = sat_InitManager(interface);
3257  cm->nodesArraySize = manager->nodesArraySize;
3258  cm->initNodesArraySize = manager->nodesArraySize;
3259  cm->maxNodesArraySize = manager->maxNodesArraySize;
3260  cm->nodesArray = manager->NodesArray;
3261  cm->HashTable = manager->HashTable;
3262  cm->literals = manager->literals;
3263  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize);
3264  cm->initNumClauses = 0;
3265  cm->initNumLiterals = 0;
3266  cm->comment = ALLOC(char, 2);
3267  cm->comment[0] = ' ';
3268  cm->comment[1] = '\0';
3269  cm->stdErr = vis_stderr;
3270  cm->stdOut = vis_stdout;
3271  cm->status = 0;
3272  cm->orderedVariableArray = 0;
3273  cm->unitLits = sat_ArrayAlloc(16);
3274  cm->pureLits = sat_ArrayAlloc(16);
3275  cm->option = 0;
3276  cm->each = 0;
3277  cm->decisionHead = 0;
3278  cm->variableArray = 0;
3279  cm->queue = 0;
3280  cm->BDDQueue = 0;
3281  cm->unusedAigQueue = 0;
3282  if(interface)
3283    cm->nonobjUnitLitArray = interface->nonobjUnitLitArray;
3284
3285  if(auxObjectArray) {
3286    cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
3287    size = auxObjectArray->num;
3288    for(i=0; i<size; i++) {
3289      tv = array_fetch(bAigEdge_t, auxObjectArray, i);
3290      if(tv == 1)       continue;
3291      else if(tv == 0) {
3292        cm->status = SAT_UNSAT;
3293        break;
3294      }
3295      sat_ArrayInsert(cm->auxObj, tv);
3296    }
3297  }
3298  if(object == 0)      cm->status = SAT_UNSAT;
3299  else if(object == 1) cm->status = SAT_SAT;
3300
3301  if(cm->status == 0) {
3302    cm->obj = sat_ArrayAlloc(1);
3303    sat_ArrayInsert(cm->obj, object);
3304
3305    /* initialize option */
3306    option = sat_InitOption();
3307    option->cnfPrefix = bmcOption->cnfPrefix;
3308    /*option->verbose = bmcOption->verbosityLevel; */
3309    option->verbose = 0;
3310    option->timeoutLimit = bmcOption->timeOutPeriod;
3311
3312    sat_SetIncrementalOption(option, bmcOption->incremental);
3313
3314    cm->option = option;
3315    cm->each = sat_InitStatistics();
3316
3317    BmcRestoreAssertion(manager, cm);
3318    /* value reset.. */
3319    sat_CleanDatabase(cm);
3320    /* set cone of influence */
3321    sat_SetConeOfInfluence(cm);
3322    sat_AllocLiteralsDB(cm);
3323
3324    if(bmcOption->cnfFileName != NIL(char)) {
3325      sat_WriteCNF(cm, bmcOption->cnfFileName);
3326    }
3327    if(bmcOption->clauses == 0){ /* CirCUs circuit*/
3328      if (bmcOption->verbosityLevel == BmcVerbosityMax_c) {     
3329        fprintf(vis_stdout,
3330                "Number of Variables = %d Number of Clauses = %d\n",
3331                sat_GetNumberOfInitialVariables(cm),  sat_GetNumberOfInitialClauses(cm));
3332      }
3333      if (bmcOption->verbosityLevel >= BmcVerbosityMax_c) {
3334        (void)fprintf(vis_stdout,"Calling SAT solver (CirCUs) ...");
3335        (void) fflush(vis_stdout);
3336      }
3337      sat_Main(cm);
3338      if (bmcOption->verbosityLevel >= BmcVerbosityMax_c) {
3339        (void) fprintf(vis_stdout," done ");
3340        (void) fprintf(vis_stdout, "(%g s)\n", cm->each->satTime);
3341      }
3342     
3343    } else if(bmcOption->clauses == 1) { /* CirCUs CNF */
3344      satArray_t *result;
3345      char       *fileName = NIL(char);
3346   
3347      sat_WriteCNF(cm, bmcOption->satInFile);
3348      if(bmcOption->satSolver == cusp){
3349        fileName = BmcCirCUsCallCusp(bmcOption);
3350      }
3351      if(bmcOption->satSolver == CirCUs){
3352        fileName = BmcCirCUsCallCirCUs(bmcOption);
3353      }
3354      if(fileName != NIL(char)){
3355        result = sat_ReadForcedAssignment(fileName);
3356        d =  sat_AllocLevel(cm);
3357        sat_PutAssignmentValueMain(cm, d, result);
3358        sat_ArrayFree(result);
3359      }
3360    }   
3361  }
3362  sat_CombineStatistics(cm);
3363
3364  if(interface == 0)
3365    interface = ALLOC(satInterface_t, 1);
3366
3367  interface->total = cm->total;
3368  interface->nonobjUnitLitArray = cm->nonobjUnitLitArray;
3369  interface->objUnitLitArray = 0;
3370  interface->savedConflictClauses = cm->savedConflictClauses;
3371  interface->trieArray = cm->trieArray;
3372  interface->status = cm->status;
3373  cm->total = 0;
3374  cm->nonobjUnitLitArray = 0;
3375  cm->savedConflictClauses = 0;
3376
3377  if(cm->maxNodesArraySize > manager->maxNodesArraySize) {
3378    manager->maxNodesArraySize = cm->maxNodesArraySize;
3379    manager->nameList   = REALLOC(char *, manager->nameList  , manager->maxNodesArraySize/bAigNodeSize);
3380    manager->bddIdArray = REALLOC(int ,   manager->bddIdArray  , manager->maxNodesArraySize/bAigNodeSize);
3381    manager->bddArray   = REALLOC(bdd_t *, manager->bddArray  , manager->maxNodesArraySize/bAigNodeSize);
3382  }
3383  manager->NodesArray = cm->nodesArray;
3384  manager->literals = cm->literals;
3385
3386  /* For the case that the input contains CNF clauese; */
3387  if(cm->literals)
3388    cm->literals->last = cm->literals->initialSize;
3389  cm->nodesArray = 0;
3390  cm->HashTable = 0;
3391  cm->timeframe = 0;
3392  cm->timeframeWOI = 0;
3393  cm->literals = 0;
3394
3395  sat_FreeManager(cm);
3396
3397  return(interface);
3398}
3399
3400/**Function********************************************************************
3401
3402   Synopsis [ CirCUs interface for bounded model checking.]
3403
3404   Description [ CirCUs interface for bounded model checking. ]
3405
3406   SideEffects []
3407   
3408   SeeAlso     []
3409   
3410******************************************************************************/
3411
3412satInterface_t *
3413BmcCirCUsInterfaceWithObjArr(
3414    bAig_Manager_t *manager,
3415    Ntk_Network_t *network,
3416    array_t *objectArray,
3417    array_t *auxObjectArray,
3418    BmcOption_t *bmcOption,
3419    satInterface_t *interface)
3420{
3421satManager_t *cm;
3422satOption_t *option;
3423int i, size;
3424bAigEdge_t tv;
3425
3426/* allocate sat manager */
3427  cm = sat_InitManager(interface);
3428  cm->nodesArraySize = manager->nodesArraySize;
3429  cm->initNodesArraySize = manager->nodesArraySize;
3430  cm->maxNodesArraySize = manager->maxNodesArraySize;
3431  cm->nodesArray = manager->NodesArray;
3432  cm->HashTable = manager->HashTable;
3433  cm->literals = manager->literals;
3434  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize);
3435  cm->initNumClauses = 0;
3436  cm->initNumLiterals = 0;
3437  cm->comment = ALLOC(char, 2);
3438  cm->comment[0] = ' ';
3439  cm->comment[1] = '\0';
3440  cm->stdErr = vis_stderr;
3441  cm->stdOut = vis_stdout;
3442  cm->status = 0;
3443  cm->orderedVariableArray = 0;
3444  cm->unitLits = sat_ArrayAlloc(16);
3445  cm->pureLits = sat_ArrayAlloc(16);
3446  cm->option = 0;
3447  cm->each = 0;
3448  cm->decisionHead = 0;
3449  cm->variableArray = 0;
3450  cm->queue = 0;
3451  cm->BDDQueue = 0;
3452  cm->unusedAigQueue = 0;
3453  if(interface)
3454    cm->nonobjUnitLitArray = interface->nonobjUnitLitArray;
3455
3456  if(auxObjectArray) {
3457    cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
3458    size = auxObjectArray->num;
3459    for(i=0; i<size; i++) {
3460      tv = array_fetch(bAigEdge_t, auxObjectArray, i);
3461      if(tv == 1)       continue;
3462      else if(tv == 0) {
3463        cm->status = SAT_UNSAT;
3464        break;
3465      }
3466      sat_ArrayInsert(cm->auxObj, tv);
3467    }
3468  }
3469  if(objectArray) {
3470    cm->obj = sat_ArrayAlloc(objectArray->num+1);
3471    size = objectArray->num;
3472    for(i=0; i<size; i++) {
3473      tv = array_fetch(bAigEdge_t, objectArray, i);
3474      if(tv == 1)       continue;
3475      else if(tv == 0) {
3476        cm->status = SAT_UNSAT;
3477        break;
3478      }
3479      sat_ArrayInsert(cm->obj, tv);
3480    }
3481  }
3482
3483  if(cm->status == 0) {
3484    /* initialize option */
3485    option = sat_InitOption();
3486    option->cnfPrefix = bmcOption->cnfPrefix;
3487    /*option->verbose = bmcOption->verbosityLevel; */
3488    option->verbose = 0;
3489    option->timeoutLimit = bmcOption->timeOutPeriod;
3490
3491    sat_SetIncrementalOption(option, bmcOption->incremental);
3492
3493    cm->option = option;
3494    cm->each = sat_InitStatistics();
3495
3496    BmcRestoreAssertion(manager, cm);
3497    /* value reset.. */
3498    sat_CleanDatabase(cm);
3499    /* set cone of influence */
3500    sat_SetConeOfInfluence(cm);
3501    sat_AllocLiteralsDB(cm);
3502
3503    if(bmcOption->cnfFileName != NIL(char)) {
3504      sat_WriteCNF(cm, bmcOption->cnfFileName);
3505    }
3506    if(bmcOption->clauses == 0){ /* CirCUs circuit*/
3507      if (bmcOption->verbosityLevel == BmcVerbosityMax_c) {     
3508        fprintf(vis_stdout,
3509                "Number of Variables = %d Number of Clauses = %d\n",
3510                sat_GetNumberOfInitialVariables(cm),  sat_GetNumberOfInitialClauses(cm));
3511      }
3512      if (bmcOption->verbosityLevel >= BmcVerbosityMax_c) {
3513        (void)fprintf(vis_stdout,"Calling SAT solver (CirCUs) ...");
3514        (void) fflush(vis_stdout);
3515      }
3516      sat_Main(cm);
3517      if (bmcOption->verbosityLevel >= BmcVerbosityMax_c) {
3518        (void) fprintf(vis_stdout," done ");
3519        (void) fprintf(vis_stdout, "(%g s)\n", cm->each->satTime);
3520      }
3521    }else if(bmcOption->clauses == 1) { /* CirCUs CNF */
3522      satArray_t *result;
3523      char       *fileName = NIL(char);
3524   
3525      sat_WriteCNF(cm, bmcOption->satInFile);
3526      if(bmcOption->satSolver == cusp){
3527        fileName = BmcCirCUsCallCusp(bmcOption);
3528      } else{ 
3529        if(bmcOption->satSolver == CirCUs){
3530          fileName = BmcCirCUsCallCirCUs(bmcOption);
3531        }
3532      }
3533      if(fileName != NIL(char)){
3534        satLevel_t *d;
3535       
3536        cm->status = SAT_SAT;
3537        result = sat_ReadForcedAssignment(fileName);
3538        d =  sat_AllocLevel(cm);
3539        sat_PutAssignmentValueMain(cm, d, result);
3540        sat_ArrayFree(result);
3541      } else {
3542        cm->status = SAT_UNSAT;
3543      }
3544    }
3545    /*sat_ReportStatistics(cm, cm->each);*/
3546  }
3547  sat_CombineStatistics(cm);
3548
3549  if(interface == 0){
3550    interface = ALLOC(satInterface_t, 1);
3551  }
3552  interface->total = cm->total;
3553  interface->nonobjUnitLitArray = cm->nonobjUnitLitArray;
3554  interface->objUnitLitArray = 0;
3555  interface->savedConflictClauses = cm->savedConflictClauses;
3556  interface->trieArray = cm->trieArray;
3557  interface->status = cm->status;
3558  cm->total = 0;
3559  cm->nonobjUnitLitArray = 0;
3560  cm->savedConflictClauses = 0;
3561
3562  if(cm->maxNodesArraySize > manager->maxNodesArraySize) {
3563    manager->maxNodesArraySize = cm->maxNodesArraySize;
3564    manager->nameList   = REALLOC(char *, manager->nameList  , manager->maxNodesArraySize/bAigNodeSize);
3565    manager->bddIdArray = REALLOC(int ,   manager->bddIdArray  , manager->maxNodesArraySize/bAigNodeSize);
3566    manager->bddArray   = REALLOC(bdd_t *, manager->bddArray  , manager->maxNodesArraySize/bAigNodeSize);
3567  }
3568  manager->NodesArray = cm->nodesArray;
3569  manager->literals = cm->literals;
3570
3571  /*
3572    For the case that the input contains CNF clauses;
3573  */
3574  if(cm->literals)
3575    cm->literals->last = cm->literals->initialSize;
3576  cm->nodesArray = 0;
3577  cm->HashTable = 0;
3578  cm->timeframe = 0;
3579  cm->timeframeWOI = 0;
3580  cm->literals = 0;
3581
3582  sat_FreeManager(cm);
3583
3584  return(interface);
3585}
3586
3587
3588/**Function********************************************************************
3589
3590   Synopsis [ Create Manager for debug purpose.]
3591
3592   Description [ Create Manager for debug purpose.]
3593
3594   SideEffects []
3595   
3596   SeeAlso     []
3597   
3598******************************************************************************/
3599satManager_t *
3600BmcCirCUsCreateManager(
3601  Ntk_Network_t *network)
3602{
3603  satManager_t *cm;
3604  bAig_Manager_t *manager;
3605  satOption_t *option;
3606
3607  manager = Ntk_NetworkReadMAigManager(network);
3608  /* allocate sat manager*/
3609  cm = sat_InitManager(0);
3610  cm->nodesArraySize = manager->nodesArraySize;
3611  cm->initNodesArraySize = manager->nodesArraySize;
3612  cm->maxNodesArraySize = manager->maxNodesArraySize;
3613  cm->nodesArray = manager->NodesArray;
3614  cm->HashTable = manager->HashTable;
3615  cm->literals = manager->literals;
3616  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize);
3617  cm->initNumClauses = 0;
3618  cm->initNumLiterals = 0;
3619  cm->comment = ALLOC(char, 2);
3620  cm->comment[0] = ' ';
3621  cm->comment[1] = '\0';
3622  cm->stdErr = vis_stderr;
3623  cm->stdOut = vis_stdout;
3624  cm->status = 0;
3625  cm->orderedVariableArray = 0;
3626  cm->unitLits = sat_ArrayAlloc(16);
3627  cm->pureLits = sat_ArrayAlloc(16);
3628  cm->option = 0;
3629  cm->each = 0;
3630  cm->decisionHead = 0;
3631  cm->variableArray = 0;
3632  cm->queue = 0;
3633  cm->BDDQueue = 0;
3634  cm->unusedAigQueue = 0;
3635
3636  if(cm->status == 0) {
3637    /* initialize option*/
3638    option = sat_InitOption();
3639    /*option->verbose = bmcOption->verbosityLevel;*/
3640    option->verbose = 0;
3641
3642    cm->option = option;
3643    cm->each = sat_InitStatistics();
3644
3645    BmcRestoreAssertion(manager, cm);
3646    /* value reset..*/
3647    sat_CleanDatabase(cm);
3648    /* set cone of influence*/
3649    sat_SetConeOfInfluence(cm);
3650    sat_AllocLiteralsDB(cm);
3651
3652    /*sat_ReportStatistics(cm, cm->each);*/
3653  }
3654  sat_CombineStatistics(cm);
3655
3656  /*
3657    For the case that the input contains CNF clauese;
3658  */
3659  if(cm->literals)
3660    cm->literals->last = cm->literals->initialSize;
3661
3662  return(cm);
3663}
3664/**Function********************************************************************
3665
3666   Synopsis [Return a list of AIG in the initialized timeframe corrsponding to
3667   the input of all lateches in COI table]
3668
3669   Description []
3670
3671   SideEffects []
3672   
3673   SeeAlso     []
3674   
3675******************************************************************************/
3676
3677st_table *
3678BmcCirCUsGetCoiIndexTable(
3679        Ntk_Network_t *network,
3680        st_table *coiTable)
3681{
3682  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
3683  Ntk_Node_t   *node;
3684  st_generator *gen;
3685  int          tmp;
3686  st_table     *node2MvfAigTable = 
3687    (st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
3688  int mvfSize, index, i;
3689  bAigEdge_t         v;
3690  MvfAig_Function_t  *mvfAig;
3691  st_table           *li2index, *coiIndexTable;
3692 
3693  assert(manager->timeframe != 0);
3694  /*
3695    Mohammad Says:
3696    This may solve the problem of calling expandTimeframe before calling this
3697    function. Check with HoonSang.
3698   
3699    if(timeframe == 0)
3700    timeframe = bAig_InitTimeFrame(network, manager, 1);
3701  */
3702 
3703  /*
3704    li2index stores AIG id for inputs of all latches
3705   */
3706  li2index = manager->timeframe->li2index;
3707  coiIndexTable = st_init_table(st_numcmp, st_numhash);
3708
3709  st_foreach_item_int(coiTable, gen, &node, &tmp) {
3710    if(!Ntk_NodeTestIsLatch(node))      continue;
3711    st_lookup(node2MvfAigTable, node, &mvfAig);
3712    mvfSize = array_n(mvfAig);
3713    for(i=0; i< mvfSize; i++){
3714      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
3715      if(st_lookup_int(li2index, (char *)v, &index)) 
3716        st_insert(coiIndexTable, (char *)(long)index, (char *)(long)index);
3717    }
3718  }
3719  return(coiIndexTable);
3720}
3721
3722/**Function********************************************************************
3723
3724  Synopsis    [ Restore aseerted node for SAT solving]
3725
3726  Description [ Restore aseerted node for SAT solving]
3727
3728  SideEffects []
3729
3730  SeeAlso     [bAig_ExpandTimeFrame]
3731
3732******************************************************************************/
3733void
3734BmcRestoreAssertion(bAig_Manager_t *manager, satManager_t *cm)
3735{
3736int size, i, v;
3737array_t *asserted;
3738
3739  if(manager->timeframe && manager->timeframe->assertedArray) {
3740    asserted = manager->timeframe->assertedArray;
3741    size = asserted->num;
3742    cm->assertion = sat_ArrayAlloc(size);
3743    for(i=0; i<size; i++) {
3744      v = array_fetch(int, asserted, i);
3745      sat_ArrayInsert(cm->assertion, v);
3746    }
3747  }
3748  else {
3749    cm->assertion = 0;
3750  }
3751}
3752
3753
3754
3755/*---------------------------------------------------------------------------*/
3756/* Definition of static functions                                            */
3757/*---------------------------------------------------------------------------*/
3758
3759/**Function********************************************************************
3760
3761   Synopsis [Check if the property is TRUE or FALSE]
3762
3763   Description []
3764
3765   SideEffects []
3766   
3767   SeeAlso     []
3768   
3769******************************************************************************/
3770static int
3771verifyIfConstant(
3772  bAigEdge_t   property)
3773{
3774
3775  if (property == bAig_One){
3776    fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
3777    fprintf(vis_stdout,"# BMC: formula failed\n");
3778    return 1;
3779  } else if (property == bAig_Zero){
3780    fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
3781    fprintf(vis_stdout,"# BMC: formula passed\n");
3782    return 1;
3783  }
3784  return 0;
3785}
Note: See TracBrowser for help on using the repository browser.