source: vis_dev/vis-2.3/src/bmc/bmcUtil.c @ 35

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

vis2.3
File size: 100.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [bmcUtil.c]
4
5  PackageName [bmc]
6
7  Synopsis    [Utilities for BMC package]
8
9  Author      [Mohammad Awedh]
10
11  Copyright   [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14 
15******************************************************************************/
16
17#include "bmcInt.h"
18#include "sat.h"
19#include "baig.h"
20
21static char rcsid[] UNUSED = "$Id: bmcUtil.c,v 1.82 2010/04/10 04:07:06 fabio Exp $";
22
23/*---------------------------------------------------------------------------*/
24/* Constant declarations                                                     */
25/*---------------------------------------------------------------------------*/
26
27#define MAX_LENGTH 320 /* Max. length of a string while reading a file     */
28
29/*---------------------------------------------------------------------------*/
30/* Type declarations                                                         */
31/*---------------------------------------------------------------------------*/
32
33
34/*---------------------------------------------------------------------------*/
35/* Structure declarations                                                    */
36/*---------------------------------------------------------------------------*/
37
38
39/*---------------------------------------------------------------------------*/
40/* Variable declarations                                                     */
41/*---------------------------------------------------------------------------*/
42
43
44/**AutomaticStart*************************************************************/
45
46/*---------------------------------------------------------------------------*/
47/* Static function prototypes                                                */
48/*---------------------------------------------------------------------------*/
49
50static int StringCheckIsInteger(char *string, int *value);
51static int nameCompare(const void * name1, const void * name2);
52static void printValue(mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue);
53static void printValueAiger(mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue);
54static void printValueAigerInputs(mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue);
55
56/**AutomaticEnd***************************************************************/
57
58/*---------------------------------------------------------------------------*/
59/* Definition of exported functions                                          */
60/*---------------------------------------------------------------------------*/
61
62
63/**Function********************************************************************
64
65  Synopsis [Compute cube that is close to target states.]
66
67  SideEffects []
68
69******************************************************************************/
70mdd_t *
71Bmc_ComputeCloseCube( 
72  mdd_t *states,
73  mdd_t *target,
74  int   *dist,
75  Fsm_Fsm_t *modelFsm)
76{
77  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
78  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) ); 
79  mdd_t *result = BmcComputeCloseCube( states, target, dist, PSVars, mddMgr );
80
81  return result;
82}
83
84/**Function********************************************************************
85
86  Synopsis [Build multi-valued function for a given node.]
87
88  SideEffects [The mvf of this node is a function of combinational input
89  nodes.]
90
91******************************************************************************/
92MvfAig_Function_t *
93Bmc_NodeBuildMVF(
94  Ntk_Network_t *network,
95  Ntk_Node_t    *node)
96{
97  MvfAig_Function_t * MvfAig; 
98  lsGen tmpGen;
99  Ntk_Node_t *tmpNode;
100  array_t    *mvfArray;
101  array_t    *tmpRoots = array_alloc(Ntk_Node_t *, 0);
102  st_table   *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
103  array_insert_last(Ntk_Node_t *, tmpRoots, node);
104
105  Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) {
106    st_insert(tmpLeaves, (char *) tmpNode, (char *) ntmaig_UNUSED);
107  }
108
109  mvfArray = ntmaig_NetworkBuildMvfAigs(network, tmpRoots, tmpLeaves);
110  MvfAig   = array_fetch(MvfAig_Function_t *, mvfArray, 0);
111  array_free(tmpRoots);
112  st_free_table(tmpLeaves);
113  array_free(mvfArray);
114  return MvfAig;
115}
116
117
118/**Function********************************************************************
119
120  Synopsis [Returns MvfAig corresponding to a node; returns NIL if node not in
121  table.]
122
123  SideEffects [None]
124
125******************************************************************************/
126MvfAig_Function_t *
127Bmc_ReadMvfAig(
128  Ntk_Node_t * node,
129  st_table   * nodeToMvfAigTable)
130{
131  MvfAig_Function_t *result;
132  if (st_lookup(nodeToMvfAigTable, node, &result)){
133     return result;
134  }
135  return NIL(MvfAig_Function_t);
136}
137
138
139/*---------------------------------------------------------------------------*/
140/* Definition of internal functions                                          */
141/*---------------------------------------------------------------------------*/
142
143/**Function********************************************************************
144
145  Synopsis    [Evaluate states satisfying X target]
146
147  Description [Evaluate states satisfying X target.]
148
149  SideEffects []
150
151******************************************************************************/
152mdd_t *
153BmcFsmEvaluateX(
154  Fsm_Fsm_t *modelFsm,
155  mdd_t     *targetMdd)
156{
157  mdd_t *fromLowerBound;
158  mdd_t *fromUpperBound;
159  mdd_t *result;
160  Img_ImageInfo_t * imageInfo;
161  mdd_t           *careStates;
162  array_t         *careStatesArray = array_alloc(array_t *, 0); 
163
164  imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
165
166  /*
167   * The lower bound is the conjunction of the fair states,
168   * and the target states.
169   */
170  fromLowerBound = mdd_dup(targetMdd);
171  /*
172   * The upper bound is the same as the lower bound.
173   */
174  fromUpperBound = mdd_dup(fromLowerBound);
175  /*
176    careSet is the set of all unreachabel states.
177  */
178  careStates = mdd_one(Fsm_FsmReadMddManager(modelFsm));
179  array_insert(mdd_t *, careStatesArray, 0, careStates);
180 
181  result = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
182                fromLowerBound, fromUpperBound, careStatesArray);
183  mdd_free(fromLowerBound);
184  mdd_free(fromUpperBound);
185 
186  return result;
187
188} /* BmcFsmEvaluateX */
189
190
191/**Function********************************************************************
192
193  Synopsis [Compute cube that is close to target states. Support
194  is an array of mddids representing the total support; that is, all
195  the variables on which aSet may depend. It dos the function only
196  if CUDD is the BDD package.]
197
198  SideEffects []
199
200******************************************************************************/
201mdd_t *
202BmcComputeCloseCube(
203  mdd_t *aSet,
204  mdd_t *target,
205  int   *dist,
206  array_t *Support,
207  mdd_manager *mddMgr)
208{
209  if (bdd_get_package_name() == CUDD && target != NIL(mdd_t)) {
210    mdd_t *range;             /* range of Support             */
211    mdd_t *legalSet;          /* aSet without the don't cares */
212    mdd_t *closeCube;
213
214   
215    /* Check that support of set is contained in Support.
216    assert(SetCheckSupport(aSet, Support, mddMgr)); */ 
217    assert(!mdd_is_tautology(aSet, 0));
218    range      = mdd_range_mdd(mddMgr, Support);
219    legalSet   = bdd_and(aSet, range, 1, 1);
220    mdd_free(range);
221    closeCube = mdd_closest_cube(legalSet, target, dist);
222
223    mdd_free(legalSet);
224   
225    return closeCube;
226  } else {
227    return aSet;
228    /*return BMC_ComputeAMinterm(aSet, Support, mddMgr);*/
229  }/* if CUDD */
230
231} /* BmcComputeCloseCube */
232
233
234/**Function********************************************************************
235
236  Synopsis [Build AND/INV graph for intial states]
237
238  Description [Build AND/INV graph for intial states. Returns bAig Id
239  of the bAig Function that represents the intial states.
240
241  The initial states are computed as follows. For each latch i, the relation
242  (x_i = g_i(u)) is built, where x_i is the present state variable of latch i,
243  and g_i(u) is the multi-valued initialization function of latch i, in terms
244  of the input variables u.  These relations are then conjuncted.
245  ]
246
247  SideEffects []
248
249  SeeAlso     []
250 
251******************************************************************************/
252mAigEdge_t
253BmcCreateMaigOfInitialStates(
254  Ntk_Network_t   *network,
255  st_table        *nodeToMvfAigTable,
256  st_table        *CoiTable)
257{
258  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
259  st_generator    *stGen;
260 
261  Ntk_Node_t         *latch, *latchInit;
262  MvfAig_Function_t  *initMvfAig, *latchMvfAig;
263 
264  bAigEdge_t         resultAnd = bAig_One;
265  bAigEdge_t         resultOr;
266  int                i;
267
268  st_foreach_item(CoiTable, stGen, &latch, NULL) {
269   
270   
271    latchInit  = Ntk_LatchReadInitialInput(latch);
272   
273    /* Get the multi-valued function for each node*/
274    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
275    if (initMvfAig ==  NIL(MvfAig_Function_t)){
276      (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit));
277      return bAig_NULL;
278   }
279   latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
280   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
281     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
282     array_free(latchMvfAig);
283     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
284   }
285   resultOr  = bAig_Zero;
286   for(i=0; i<array_n(initMvfAig); i++){
287     resultOr = mAig_Or(manager, resultOr,
288                        bAig_Eq(manager,
289                                bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(initMvfAig,  i)),
290                                bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i))
291                                )
292                        );
293     if(resultOr == bAig_One){
294       break;
295     }
296   }
297   resultAnd = mAig_And(manager, resultAnd, resultOr);
298   if(resultAnd == bAig_Zero){
299     break;
300   }
301  }/* for each latch*/
302
303  return resultAnd;
304}
305
306
307/**Function********************************************************************
308
309  Synopsis [Builds AND/INVERTER graph (aig) for a propsitional formula]
310
311  Description [Builds AND/INVERTER graph for a propsitional formula.
312  Returns bAig ID of the function that is quivalent to the propositional
313  fomula]
314
315  SideEffects []
316
317  SeeAlso     []
318
319******************************************************************************/
320
321mAigEdge_t
322BmcCreateMaigOfPropFormula(
323  Ntk_Network_t   *network,
324  mAig_Manager_t  *manager,
325  Ctlsp_Formula_t *formula)
326{
327  mAigEdge_t left, right, result;
328
329  if (formula == NIL(Ctlsp_Formula_t)) {
330    return mAig_NULL;
331  }
332  if (formula->type == Ctlsp_TRUE_c){
333    return mAig_One;
334  }
335  if (formula->type == Ctlsp_FALSE_c){
336    return mAig_Zero;
337  }
338 
339  assert(Ctlsp_isPropositionalFormula(formula));
340 
341  if (formula->type == Ctlsp_ID_c){
342      char *nodeNameString  = Ctlsp_FormulaReadVariableName(formula);
343      char *nodeValueString = Ctlsp_FormulaReadValueName(formula);
344      Ntk_Node_t *node      = Ntk_NetworkFindNodeByName(network, nodeNameString);
345
346      Var_Variable_t *nodeVar;
347      int             nodeValue;
348
349      MvfAig_Function_t  *tmpMvfAig;
350      st_table           *nodeToMvfAigTable; /* maps each node to its mvfAig */
351     
352      if (node == NIL(Ntk_Node_t)) {
353          (void) fprintf(vis_stderr, "bmc error: Could not find node corresponding to the name\t %s\n", nodeNameString);
354          return mAig_NULL;
355      }
356      nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
357      if (nodeToMvfAigTable == NIL(st_table)){
358         (void) fprintf(vis_stderr, "bmc error: please run build_partiton_maigs first");
359         return mAig_NULL;
360      }
361      tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
362      if (tmpMvfAig ==  NIL(MvfAig_Function_t)){
363          tmpMvfAig = Bmc_NodeBuildMVF(network, node);
364          array_free(tmpMvfAig);
365          tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
366      }
367      nodeVar = Ntk_NodeReadVariable(node);
368      if (Var_VariableTestIsSymbolic(nodeVar)) {
369        nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
370        if ( nodeValue == -1 ) {
371          (void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
372          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
373          return mAig_NULL;
374        }
375      }
376      else { 
377        int check;   
378         check = StringCheckIsInteger(nodeValueString, &nodeValue);
379         if( check == 0 ) {
380          (void) fprintf(vis_stderr,"Illegal value in the RHS\n");
381          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
382          return mAig_NULL;
383         }
384         if( check == 1 ) {
385          (void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
386          (void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
387          return mAig_NULL;
388         }
389         if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
390          (void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
391          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
392          return mAig_NULL;
393
394         }
395      }
396      result = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue);
397      return bAig_GetCanonical(manager, result);
398  }
399  /*
400    right can be mAig_NULL for unery operators, but left can't be mAig_Null
401   */
402  left  = BmcCreateMaigOfPropFormula(network, manager, formula->left);
403  if (left == mAig_NULL){
404    return mAig_NULL;
405  } 
406  right = BmcCreateMaigOfPropFormula(network, manager, formula->right);
407
408  switch(formula->type) {
409    case Ctlsp_NOT_c:
410      result = mAig_Not(left);
411      break;
412    case Ctlsp_OR_c:
413      result = mAig_Or(manager, left, right);
414      break;
415    case Ctlsp_AND_c:
416      result = mAig_And(manager, left, right);
417      break;
418    case Ctlsp_THEN_c:
419      result = mAig_Then(manager, left, right); 
420      break;
421    case Ctlsp_EQ_c:
422      result = mAig_Eq(manager, left, right);
423      break;
424    case Ctlsp_XOR_c:
425      result = mAig_Xor(manager, left, right);
426      break;
427    default:
428      fail("Unexpected LTL type");
429  }
430  return result;
431} /* BmcCreateMaigOfPropFormula */
432
433/**Function********************************************************************
434
435  Synopsis [Build MDD for safety property in form of AG(p).  Where p is either a
436  propositional formula or a path formula contains only the temporal property X.]
437
438  Description [Build MDD for a safety formula. Returns NIL if the conversion
439  fails. The calling application is responsible for freeing the returned MDD.]
440
441  SideEffects []
442
443  SeeAlso     [Ctlsp_FormulaReadClass]
444
445******************************************************************************/
446mdd_t *
447BmcCreateMddOfSafetyProperty(
448  Fsm_Fsm_t       *fsm,
449  Ctlsp_Formula_t *formula)
450{
451 
452  mdd_manager   *manager = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(fsm));
453  mdd_t         *left, *right, *result;
454
455  if (formula == NIL(Ctlsp_Formula_t)) {
456    return NIL(mdd_t);
457  }
458  if (formula->type == Ctlsp_TRUE_c){
459    return bdd_one(manager);
460  }
461  if (formula->type == Ctlsp_FALSE_c){
462    return  mdd_zero(manager);
463  }
464 
465#if 0
466  if (!Ctlsp_isPropositionalFormula(formula)) {
467    (void) fprintf(vis_stderr, "bmc error: Only propositional formula can be converted to bdd \n");
468    fprintf(vis_stdout, "\nFormula: ");
469    Ctlsp_FormulaPrint(vis_stdout, formula);
470    fprintf(vis_stdout, "\n");
471    return NIL(mdd_t);
472  }
473#endif
474  /*
475    Atomic proposition.
476   */
477  if (formula->type == Ctlsp_ID_c){
478    return BmcModelCheckAtomicFormula(fsm, formula);
479  }
480  /*
481    right can be NIL(mdd_t) for unery operators, but left can't be  NIL(mdd_t)
482   */
483  left  = BmcCreateMddOfSafetyProperty(fsm, formula->left);
484  if (left == NIL(mdd_t)){
485    return NIL(mdd_t);
486  } 
487  right = BmcCreateMddOfSafetyProperty(fsm, formula->right);
488  assert(right !=  NIL(mdd_t)); 
489  switch(formula->type) {
490    case Ctlsp_NOT_c:
491      result = mdd_not(left);
492      break;
493    case Ctlsp_OR_c:
494      result = mdd_or(left, right, 1, 1);
495      break;
496    case Ctlsp_AND_c:
497      result = mdd_and(left, right, 1, 1);
498      break;
499    case Ctlsp_THEN_c:
500      result = mdd_or(left, right, 0, 1); 
501      break;
502    case Ctlsp_EQ_c:
503      result = mdd_xnor(left, right);
504      break;
505    case Ctlsp_XOR_c:
506      result = mdd_xor(left, right);
507      break;
508  case Ctlsp_X_c:
509      result = BmcFsmEvaluateX(fsm, left);
510      break;
511  default:
512    /*
513      return NIL(mdd_t) if the type is not supported
514     */
515     return NIL(mdd_t);
516     /*
517      fail("Unexpected type");
518     */
519  }
520  return result;
521}
522
523
524/**Function********************************************************************
525
526  Synopsis    [Generate the CNF formula of a given function represented by
527               AND/INVERTER graph]
528
529  Description [Generate an array of clausese for a function represented in
530  AND/INVERETER graph structure.
531 
532  the CNF formula of node to the output file specifies by cnfFile.
533               It stores CNF index for each node in the cnfIndexTable. The generated CNF
534               is in dimacs format.
535               It is an error to call this function on a constand zero/one node.]
536
537  SideEffects []
538
539  SeeAlso     []
540
541******************************************************************************/
542int
543BmcGenerateCnfFormulaForAigFunction(
544   bAig_Manager_t *manager,
545   bAigEdge_t      node,
546   int             k,
547   BmcCnfClauses_t *cnfClauses)
548{
549  int        leftIndex, rightIndex, nodeIndex;
550  array_t    *clause;
551
552  assert( (node != bAig_One) && (node != bAig_Zero));
553 
554  if(bAig_IsInverted(node)){
555    /*
556      The generated clauses are in dimacs formate that uses negative number to indicate complement
557     */
558    return -1*BmcGenerateCnfFormulaForAigFunction(manager, bAig_NonInvertedEdge(node), k, cnfClauses);
559  }
560  if (BmcCnfReadOrInsertNode(cnfClauses, bAig_NodeReadName(manager, node), k, &nodeIndex)){
561    return nodeIndex;
562  }
563  if (bAig_isVarNode(manager, node)){
564    return nodeIndex;
565  }
566  leftIndex  = BmcGenerateCnfFormulaForAigFunction(manager,
567                                                   bAig_GetCanonical(manager, leftChild(node)),
568                                                   k, cnfClauses);
569  rightIndex = BmcGenerateCnfFormulaForAigFunction(manager,
570                                                   bAig_GetCanonical(manager, rightChild(node)),
571                                                   k, cnfClauses);
572  clause  = array_alloc(int, 3);
573  array_insert(int, clause, 0, -leftIndex );
574  array_insert(int, clause, 1, -rightIndex);
575  array_insert(int, clause, 2,  nodeIndex );
576  BmcCnfInsertClause(cnfClauses, clause);
577  array_free(clause);
578 
579  clause  = array_alloc(int, 2);
580  array_insert(int, clause, 0,  leftIndex);
581  array_insert(int, clause, 1, -nodeIndex);
582  BmcCnfInsertClause(cnfClauses, clause);
583  array_free(clause);
584 
585  clause  = array_alloc(int, 2);
586  array_insert(int, clause, 0,  rightIndex);
587  array_insert(int, clause, 1, -nodeIndex);
588  BmcCnfInsertClause(cnfClauses, clause); 
589  array_free(clause);
590 
591  return(nodeIndex);
592}
593
594/**Function********************************************************************
595
596  Synopsis [Generate CNF for bdd function]
597
598  Description [
599    The function of each node f = var*thenChild + -var*elseChild
600    var is the variable at this node.
601    For each node there are four cases:
602      - both childeren are constant -> do nothing.
603      - the then child is constant 1 -> generate clauses for f = var + elseChild.
604      - the else child is constant 0 -> generate clauses for f = var * thenChild.
605      - the else child is constant 1 -> generate clauses for f = -var + thenChild.
606      - else -> generate clauses for f = var*thenChild + -var*elseChild.
607  ------------------------------------------------
608    function        |        clauses
609  ------------------------------------------------ 
610    c = a*b         | (-a + -b + c)*(a + -c)*(b + -c)
611    c = a+b         | (a + b + -c)*(-a + c)*(-b + c)
612    f = c*a + -c*b  | (-a + -c + f)*(a + -c + -f)*
613                    | (-b +  c + f)*(b +  c + -f)
614
615  return the cnf index of the bdd function
616  ]
617 
618  SideEffects []
619
620  SeeAlso     []
621 
622******************************************************************************/
623int 
624BmcGenerateCnfFormulaForBdd(
625   bdd_t          *bddFunction,
626   int             k,
627   BmcCnfClauses_t *cnfClauses)
628{
629  bdd_manager *bddManager = bdd_get_manager(bddFunction);
630  bdd_node    *node, *thenNode, *elseNode, *funcNode;
631  int         is_complemented;
632  int         nodeIndex=0, thenIndex, elseIndex;
633  bdd_gen     *gen;
634  int         varIndex, flag; 
635  array_t     *tmpClause;
636 
637  st_table    *bddToCnfIndexTable;
638 
639  bdd_t       *currentBddNode;
640  int         cut = 5;
641 
642  if (bddFunction == NULL){
643    return 0;
644  }
645  funcNode = bdd_get_node(bddFunction, &is_complemented);
646  if (bdd_is_constant(funcNode)){
647    if (is_complemented){
648      /* add an empty clause to indicate FALSE (un-satisfiable)*/
649      BmcAddEmptyClause(cnfClauses);
650    }
651    return 0;
652  }
653  if(bdd_size(bddFunction) <= cut){
654    return BmcGenerateCnfFormulaForBddOffSet(bddFunction, k, cnfClauses);
655  }
656 
657  bddToCnfIndexTable = st_init_table(st_numcmp, st_numhash);
658  foreach_bdd_node(bddFunction, gen, node){
659    if (bdd_is_constant(node)){ /* do nothing */
660      continue;
661    }
662
663    /*
664      bdd_size() returns 1 if bdd is constant one.
665    */
666    /*
667      Use offset method to generate CNF if the size of the node <= cut (include the constant 1 node).
668    */
669    /*#if 0*/   
670    if(bdd_size(currentBddNode = bdd_construct_bdd_t(bddManager, bdd_regular(node))) <= cut){
671      if (bdd_size(currentBddNode) == cut){
672        nodeIndex = BmcGenerateCnfFormulaForBddOffSet(currentBddNode, k, cnfClauses);
673        st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(node),  (char *) (long)nodeIndex);
674        continue;
675      }
676      continue;
677    }
678    /*#endif*/   
679    varIndex  = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), k, cnfClauses);
680    nodeIndex = varIndex;
681   
682    thenNode = bdd_bdd_T(node);
683    elseNode = bdd_bdd_E(node);
684
685    if (!((bdd_is_constant(thenNode)) && (bdd_is_constant(elseNode)))){
686      nodeIndex = cnfClauses->cnfGlobalIndex++;   /* index of the function of this node */
687     
688      if (bdd_is_constant(thenNode)){ /* the thenNode can be only constant one*/
689        flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(elseNode), &elseIndex);
690        assert(flag);
691        /*
692          test if the elseNode is complemented arc?
693        */
694        if (bdd_is_complement(elseNode)){
695          elseIndex = -1*elseIndex;
696        } 
697        BmcCnfGenerateClausesForOR(elseIndex, varIndex, nodeIndex, cnfClauses);
698      } else if (bdd_is_constant(elseNode)){ /* one or zero */
699        flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(thenNode), &thenIndex);
700        assert(flag);
701        /*
702          test if the elseNode is complemented arc?
703        */
704        if (bdd_is_complement(elseNode)){  /* Constant zero */
705         BmcCnfGenerateClausesForAND(thenIndex, varIndex, nodeIndex, cnfClauses);
706        } else { /* Constant one */
707         BmcCnfGenerateClausesForOR(thenIndex, -varIndex, nodeIndex, cnfClauses);
708        }
709      } else {
710        flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(thenNode), &thenIndex);
711        if(flag == 0){
712          thenIndex = BmcGenerateCnfFormulaForBddOffSet(bdd_construct_bdd_t(bddManager, bdd_regular(thenNode)), k, cnfClauses);
713          st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(thenNode),  (char *) (long)thenIndex);
714        }
715        /*assert(flag);*/
716       
717        flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(elseNode), &elseIndex);
718        if(flag == 0){
719          elseIndex = BmcGenerateCnfFormulaForBddOffSet( bdd_construct_bdd_t(bddManager, bdd_regular(elseNode)), k, cnfClauses);
720          st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(elseNode),  (char *)(long) elseIndex);
721        }
722        /*assert(flag);*/
723        /*
724          test if the elseNode is complemented arc?
725        */
726        if (bdd_is_complement(elseNode)){
727          elseIndex = -1*elseIndex;
728        }     
729        tmpClause = array_alloc(int, 3);
730
731        assert(abs(thenIndex) <= cnfClauses->cnfGlobalIndex);
732        assert(abs(varIndex) <= cnfClauses->cnfGlobalIndex);
733        assert(abs(nodeIndex) <= cnfClauses->cnfGlobalIndex);
734         
735        array_insert(int, tmpClause, 0, -thenIndex);
736        array_insert(int, tmpClause, 1, -varIndex);
737        array_insert(int, tmpClause, 2, nodeIndex);
738        BmcCnfInsertClause(cnfClauses, tmpClause);
739       
740        array_insert(int, tmpClause, 0, thenIndex);
741        array_insert(int, tmpClause, 1, -varIndex);
742        array_insert(int, tmpClause, 2, -nodeIndex);
743        BmcCnfInsertClause(cnfClauses, tmpClause);
744       
745        array_insert(int, tmpClause, 0, -elseIndex);
746        array_insert(int, tmpClause, 1, varIndex);
747        array_insert(int, tmpClause, 2, nodeIndex);
748        BmcCnfInsertClause(cnfClauses, tmpClause);
749       
750        array_insert(int, tmpClause, 0, elseIndex);
751        array_insert(int, tmpClause, 1, varIndex);
752        array_insert(int, tmpClause, 2, -nodeIndex);
753        BmcCnfInsertClause(cnfClauses, tmpClause); 
754       
755        array_free(tmpClause);
756      }
757    }
758    st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(node),  (char *) (long) nodeIndex);
759  } /* foreach_bdd_node() */
760  st_free_table(bddToCnfIndexTable);
761  return (is_complemented? -nodeIndex: nodeIndex);
762} /* BmcGenerateCnfFormulaForBdd() */
763
764
765
766/**Function********************************************************************
767
768  Synopsis [Generate CNF for bdd function based on the off set of the
769  bdd function]
770
771  Description [Express the negation of bdd function in disjunctive
772  normal form(DNF), and generate a clause for each disjunct in the
773  DNF.]
774 
775  SideEffects []
776
777  SeeAlso     []
778 
779******************************************************************************/
780int 
781BmcGenerateCnfFormulaForBddOffSet(
782   bdd_t          *bddFunction,
783   int             k,
784   BmcCnfClauses_t *cnfClauses)
785{
786  bdd_manager *bddManager = bdd_get_manager(bddFunction);
787  bdd_node    *node, *funcNode;
788  int         is_complemented;
789  bdd_gen     *gen;
790  int         varIndex; 
791  array_t     *tmpClause;
792  array_t     *cube;
793  int         i, value;
794  bdd_t       *newVar;
795 
796  if (bddFunction == NULL){
797    return 0;
798  }
799  /*
800    Because the top node of bddFunction represents a variable in
801    bddFunction, newVar is used to represent the function of
802    bddFunction.  Setting the cnfIndex of newVar to 1(0) is like
803    setting the function of bddFunction to 1(0).
804  */
805  newVar = bdd_create_variable(bddManager);
806  bddFunction = bdd_xnor(newVar, bddFunction);
807  funcNode = bdd_get_node(bddFunction, &is_complemented);
808  if (bdd_is_constant(funcNode)){
809    if (is_complemented){
810      /* add an empty clause to indicate FALSE (un-satisfiable)*/
811      BmcAddEmptyClause(cnfClauses);
812    }
813    return 0;
814  }
815  bddFunction = bdd_not(bddFunction);
816
817  foreach_bdd_cube(bddFunction, gen, cube){
818    tmpClause = array_alloc(int,0);
819    arrayForEachItem(int, cube, i, value) {
820      if (value != 2){
821        node = bdd_bdd_ith_var(bddManager, i);
822        varIndex  = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), k, cnfClauses);
823        if (value == 1){
824          varIndex = -varIndex; 
825        }
826        array_insert_last(int, tmpClause, varIndex);
827      }
828    }
829    BmcCnfInsertClause(cnfClauses, tmpClause);
830    array_free(tmpClause);
831  }/* foreach_bdd_cube() */
832  varIndex  = BmcGetCnfVarIndexForBddNode(bddManager,
833                                       bdd_regular(bdd_get_node(newVar, &is_complemented)),
834                                       k, cnfClauses);
835  return (varIndex);
836} /* BmcGenerateCnfFormulaForBddOffSet() */
837
838#if 0
839/**Function********************************************************************
840
841  Synopsis    [Generate the CNF formula of a given function represented by
842               AND/INVERTER graph]
843
844  Description [Generate an array of clausese for a function represented in
845  AND/INVERETER graph structure.
846 
847  the CNF formula of node to the output file specifies by cnfFile.
848               It stores CNF index for each node in the cnfIndexTable. The generated CNF
849               is in dimacs format.
850               It is an error to call this function on a constand zero/one node.]
851
852  SideEffects []
853
854  SeeAlso     []
855
856******************************************************************************/
857int
858BmcGenerateCnfForAigFunction(
859   bAig_Manager_t  *manager,
860   Ntk_Network_t   *network,
861   bAigEdge_t      node,
862   int             k,
863   BmcCnfClauses_t *cnfClauses)
864{
865  int        leftIndex, rightIndex, nodeIndex;
866  array_t    *clause;
867
868  if(bAig_IsInverted(node)){
869    /*
870      The generated clauses are in dimacs formate that uses negative number to indicate complement
871     */
872    return -1*BmcGenerateCnfFormulaForAigFunction(manager, bAig_NonInvertedEdge(node), k, cnfClauses);
873  }
874  {
875    char *name   = bAig_NodeReadName(manager, node);
876    char *found  = strchr(name, '=');
877   
878    if (found != NIL(char)){
879      int value = atoi(found+1);
880      int length = found-name;
881      char toName[length+1];
882      Ntk_Node_t *node;
883     
884      toName[length] = '\0';
885      strncpy(toName, name, length);
886      node = Ntk_NetworkFindNodeByName(network, toName);
887      if ((node != NIL( Ntk_Node_t)) && Ntk_NodeTestIsLatch(node)){
888        MvfAig_Function_t  *tmpMvfAig;
889        st_table *nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
890        bAigEdge_t mAigNode;
891
892        if (nodeToMvfAigTable == NIL(st_table)){
893          (void) fprintf(vis_stderr, "bmc error: please run build_partiton_maigs first");
894          return mAig_NULL;
895        }
896        if (k==0){
897          node = Ntk_LatchReadInitialInput(node);
898        } else {
899          node = Ntk_LatchReadDataInput(node);
900          k--;
901        }
902        tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
903        if (tmpMvfAig ==  NIL(MvfAig_Function_t)){
904          tmpMvfAig = Bmc_NodeBuildMVF(network, node);
905          array_free(tmpMvfAig);
906          tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
907        }
908        mAigNode = MvfAig_FunctionReadComponent(tmpMvfAig, value);
909        BmcGenerateCnfForAigFunction(manager, network, mAigNode, k, cnfClauses);
910      }
911    }
912  }
913  if (BmcCnfReadOrInsertNode(cnfClauses, bAig_NodeReadName(manager, node), k, &nodeIndex)){
914    return nodeIndex;
915  }
916  if (bAig_isVarNode(manager, node)){
917    return nodeIndex;
918  }
919  leftIndex  = BmcGenerateCnfForAigFunction(manager, network, leftChild(node),  k, cnfClauses);
920  rightIndex = BmcGenerateCnfForAigFunction(manager, network, rightChild(node), k, cnfClauses);
921 
922  clause  = array_alloc(int, 3);
923  array_insert(int, clause, 0, -leftIndex );
924  array_insert(int, clause, 1, -rightIndex);
925  array_insert(int, clause, 2,  nodeIndex );
926  BmcCnfInsertClause(cnfClauses, clause);
927  array_free(clause);
928 
929  clause  = array_alloc(int, 2);
930  array_insert(int, clause, 0,  leftIndex);
931  array_insert(int, clause, 1, -nodeIndex);
932  BmcCnfInsertClause(cnfClauses, clause);
933  array_free(clause);
934 
935  clause  = array_alloc(int, 2);
936  array_insert(int, clause, 0,  rightIndex);
937  array_insert(int, clause, 1, -nodeIndex);
938  BmcCnfInsertClause(cnfClauses, clause); 
939  array_free(clause);
940
941  return(nodeIndex);
942
943}
944#endif
945/**Function********************************************************************
946
947  Synopsis [
948               c = a <-> b = (a=0)*(b=0) + (a=1)*(b=1) ....
949           For a given term (a=i)*(b=i), if either is Zero,  don't generate
950                                         clauses for this term.
951                                         if both are One, don't generate clauses
952                                         for c.
953  ]
954
955  SideEffects []
956
957******************************************************************************/
958void
959BmcGenerateClausesFromStateTostate(
960   bAig_Manager_t  *manager,
961   bAigEdge_t      *fromAigArray,
962   bAigEdge_t      *toAigArray,
963   int             mvfSize, 
964   int             fromState,
965   int             toState,
966   BmcCnfClauses_t *cnfClauses,
967   int             outIndex) 
968{
969  array_t    *clause, *tmpclause;
970  int        toIndex, fromIndex, cnfIndex;
971  int        i;
972
973  /* used to turn off the warning messages: might be left uninitialized.
974     We are sure that these two variables will not be used uninitialized.
975  */
976  toIndex =0;
977  fromIndex = 0;
978 
979  for(i=0; i< mvfSize; i++){
980    if ((fromAigArray[i] == bAig_One) && (toAigArray[i] == bAig_One)){
981      return;   /* the clause is always true */
982    }
983  }
984  clause  = array_alloc(int, 0);
985  for(i=0; i< mvfSize; i++){
986    if ((fromAigArray[i] != bAig_Zero) && (toAigArray[i] != bAig_Zero)){
987      if (toAigArray[i] != bAig_One){ 
988         /* to State */
989
990         toIndex = BmcGenerateCnfFormulaForAigFunction(manager,toAigArray[i],
991                                                       toState,cnfClauses);
992      }
993      if (fromAigArray[i] != bAig_One){ 
994         /* from State */
995         fromIndex = BmcGenerateCnfFormulaForAigFunction(manager,
996                                                         fromAigArray[i],
997                                                         fromState,
998                                                         cnfClauses);
999      }
1000     /*
1001      Create new var for the output of this node. We don't create variable for this node, we only
1002      use its index number.
1003     */
1004     cnfIndex = cnfClauses->cnfGlobalIndex++;  /* index of the output of the OR of T(from, to) */
1005     
1006     assert(abs(cnfIndex) <= cnfClauses->cnfGlobalIndex);
1007     assert(abs(fromIndex) <= cnfClauses->cnfGlobalIndex);
1008     assert(abs(toIndex) <= cnfClauses->cnfGlobalIndex);
1009     
1010     if (toAigArray[i] == bAig_One){       
1011       tmpclause  = array_alloc(int, 2);
1012       array_insert(int, tmpclause, 0, -fromIndex);
1013       array_insert(int, tmpclause, 1, cnfIndex);
1014       BmcCnfInsertClause(cnfClauses, tmpclause);
1015       array_free(tmpclause); 
1016
1017       tmpclause  = array_alloc(int, 2);
1018       array_insert(int, tmpclause, 0, fromIndex);
1019       array_insert(int, tmpclause, 1, -cnfIndex);
1020       BmcCnfInsertClause(cnfClauses, tmpclause);
1021       array_free(tmpclause);       
1022
1023     } else if (fromAigArray[i] == bAig_One){
1024       tmpclause  = array_alloc(int, 2);
1025       array_insert(int, tmpclause, 0, -toIndex);
1026       array_insert(int, tmpclause, 1, cnfIndex);
1027       BmcCnfInsertClause(cnfClauses, tmpclause);
1028       array_free(tmpclause);
1029
1030       tmpclause  = array_alloc(int, 2);
1031       array_insert(int, tmpclause, 0, toIndex);
1032       array_insert(int, tmpclause, 1, -cnfIndex);
1033       BmcCnfInsertClause(cnfClauses, tmpclause);
1034       array_free(tmpclause);
1035       
1036     } else {
1037       tmpclause  = array_alloc(int, 3);
1038       array_insert(int, tmpclause, 0, -toIndex);
1039       array_insert(int, tmpclause, 1, -fromIndex);
1040       array_insert(int, tmpclause, 2,  cnfIndex);
1041       BmcCnfInsertClause(cnfClauses, tmpclause);
1042       array_free(tmpclause);
1043
1044       tmpclause  = array_alloc(int, 2);
1045       array_insert(int, tmpclause, 0, toIndex);
1046       array_insert(int, tmpclause, 1, -cnfIndex);
1047       BmcCnfInsertClause(cnfClauses, tmpclause);
1048       array_free(tmpclause);
1049
1050       tmpclause  = array_alloc(int, 2);
1051       array_insert(int, tmpclause, 0, fromIndex);
1052       array_insert(int, tmpclause, 1, -cnfIndex);
1053       BmcCnfInsertClause(cnfClauses, tmpclause);
1054       array_free(tmpclause);
1055     }
1056     array_insert_last(int, clause, cnfIndex);
1057    } /* if */
1058  } /* for i loop */
1059  if (outIndex != 0 ){
1060    array_insert_last(int, clause, -outIndex);
1061  }
1062  BmcCnfInsertClause(cnfClauses, clause);
1063  array_free(clause);
1064 
1065  return;
1066}
1067
1068/**Function********************************************************************
1069
1070  Synopsis [Write the set of clauses in diamacs format to the output file.]
1071
1072  SideEffects []
1073
1074******************************************************************************/
1075void
1076BmcWriteClauses(
1077   mAig_Manager_t  *maigManager,
1078   FILE            *cnfFile,
1079   BmcCnfClauses_t *cnfClauses,
1080   BmcOption_t     *options)
1081{
1082  st_generator *stGen;
1083  char         *name;
1084  int          cnfIndex, i, k;
1085
1086  if (options->verbosityLevel == BmcVerbosityMax_c) {     
1087    fprintf(vis_stdout,
1088            "Number of Variables = %d Number of Clauses = %d\n",
1089            cnfClauses->cnfGlobalIndex-1,  cnfClauses->noOfClauses);
1090  }
1091  st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) {
1092    fprintf(cnfFile, "c %s %d\n",name, cnfIndex);
1093  }
1094  (void) fprintf(cnfFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1,
1095                 cnfClauses->noOfClauses);
1096  if (cnfClauses->clauseArray != NIL(array_t)) {
1097    for (i = 0; i < cnfClauses->nextIndex; i++) {
1098      k = array_fetch(int, cnfClauses->clauseArray, i);
1099      (void) fprintf(cnfFile, "%d%c", k, (k == 0) ? '\n' : ' ');
1100    }
1101  }
1102  return;
1103}
1104
1105/**Function********************************************************************
1106
1107  Synopsis [Check the satisfiability of CNF formula written in file]
1108
1109  Description [Run SAT solver on input file]
1110
1111  SideEffects []
1112
1113******************************************************************************/
1114array_t *
1115BmcCheckSAT(BmcOption_t *options)
1116{
1117  array_t     *result = NIL(array_t);
1118 
1119
1120  if(options->satSolver == cusp){
1121    result = BmcCallCusp(options);
1122  }
1123  if(options->satSolver == CirCUs){
1124    result = BmcCallCirCUs(options);
1125  }
1126  /* Adjust alarm if timeout in effect.  This is necessary because the
1127   * alarm may have gone off while the SAT solver is running.  Since
1128   * the CPU time of a child process is charged to the parent only when
1129   * the child terminates, the SIGALRM handler assumes that more time
1130   * is left than it is in reality.  We could do this adjustment right
1131   * after calling the SAT solver, but we prefer to give ourselves the
1132   * extra time to report the result even if this means using more time
1133   * than we are allotted.
1134   */
1135  if (options->timeOutPeriod > 0) {
1136    int residualTime = options->timeOutPeriod -
1137      (util_cpu_ctime() - options->startTime) / 1000;
1138    /* Make sure we do not cancel the alarm if no time is left. */
1139    if (residualTime <= 0) {
1140      residualTime = 1;
1141    }
1142    (void) alarm(residualTime);
1143  }
1144
1145  return result;
1146}
1147
1148/**Function********************************************************************
1149
1150  Synopsis [Check the satisfiability of CNF formula written in file]
1151
1152  Description [Run CirCUs on input file]
1153
1154  SideEffects []
1155
1156******************************************************************************/
1157array_t *
1158BmcCallCirCUs(
1159  BmcOption_t *options)
1160{
1161  satOption_t  *satOption;
1162  array_t      *result = NIL(array_t);
1163  satManager_t *cm;
1164  int          maxSize;
1165
1166  satOption = sat_InitOption();
1167  satOption->verbose = options->verbosityLevel;
1168    satOption->verbose = 0;
1169 
1170  cm = sat_InitManager(0);
1171  cm->comment = ALLOC(char, 2);
1172  cm->comment[0] = ' ';
1173  cm->comment[1] = '\0';
1174  cm->stdOut = stdout;
1175  cm->stdErr = stderr;
1176
1177  cm->option = satOption;
1178  cm->each = sat_InitStatistics();
1179
1180  cm->unitLits = sat_ArrayAlloc(16);
1181  cm->pureLits = sat_ArrayAlloc(16);
1182
1183  maxSize = 10000 << (bAigNodeSize-4);
1184  cm->nodesArray = ALLOC(bAigEdge_t, maxSize);
1185  cm->maxNodesArraySize = maxSize;
1186  cm->nodesArraySize = bAigNodeSize;
1187
1188  sat_AllocLiteralsDB(cm);
1189
1190  sat_ReadCNF(cm, options->satInFile);
1191
1192  if (options->verbosityLevel == BmcVerbosityMax_c) {
1193    (void)fprintf(vis_stdout,"Calling SAT solver (CirCUs) ...");
1194    (void) fflush(vis_stdout);
1195  }
1196  sat_Main(cm);
1197  if (options->verbosityLevel == BmcVerbosityMax_c) {
1198    (void) fprintf(vis_stdout," done ");
1199    (void) fprintf(vis_stdout, "(%g s)\n", cm->each->satTime);
1200  }
1201  if(cm->status == SAT_UNSAT) {
1202    if (options->verbosityLevel != BmcVerbosityNone_c){
1203      (void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
1204     
1205    }
1206    fflush(cm->stdOut);
1207  } else if(cm->status == SAT_SAT) {
1208    if (options->verbosityLevel != BmcVerbosityNone_c){
1209      (void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
1210    }
1211    if (options->verbosityLevel == BmcVerbosityMax_c){
1212      sat_ReportStatistics(cm, cm->each);
1213    }
1214    fflush(cm->stdOut);
1215    result = array_alloc(int, 0);
1216    {
1217      int i, size, value;
1218     
1219      size = cm->initNumVariables * bAigNodeSize;
1220      for(i=bAigNodeSize; i<=size; i+=bAigNodeSize) {
1221        value = SATvalue(i);
1222        if(value == 1) {
1223          array_insert_last(int, result, SATnodeID(i));
1224        }
1225        else if(value == 0) {
1226          array_insert_last(int, result, -(SATnodeID(i)));
1227        }
1228      }
1229    }
1230  }
1231  //Bing: To avoid SEVERE memory leakage
1232  FREE(cm->nodesArray);
1233 
1234  sat_FreeManager(cm);
1235
1236  return result;
1237} /* BmcCallCirCUs */
1238
1239/**Function********************************************************************
1240
1241  Synopsis [Check the satisfiability of CNF formula written in file]
1242
1243  Description [Run external solver on input file]
1244
1245  SideEffects []
1246
1247******************************************************************************/
1248array_t *
1249BmcCallCusp(BmcOption_t *options)
1250{
1251  FILE        *fp;
1252  static char parseBuffer[1024];
1253  int         satStatus;
1254  char        line[MAX_LENGTH];
1255  int         num = 0;
1256  array_t     *result = NIL(array_t);
1257  char        *tmpStr, *tmpStr1, *tmpStr2;
1258  long        solverStart;
1259  int         satTimeOutPeriod = 0;
1260
1261  strcpy(parseBuffer,"cusp -distill -velim -cnf ");
1262  options->satSolverError = FALSE;  /* assume no error*/
1263  if (options->timeOutPeriod > 0) {
1264    /* Compute the residual CPU time and subtract a little time to
1265       give vis a chance to clean up before its own time out expires.
1266    */
1267    satTimeOutPeriod = options->timeOutPeriod - 1 -
1268      (util_cpu_ctime() - options->startTime) / 1000;
1269    if (satTimeOutPeriod <= 0){ /* no time left to run SAT solver*/
1270      options->satSolverError=TRUE;
1271      return NIL(array_t);
1272    }
1273    tmpStr2 = util_inttostr(satTimeOutPeriod);
1274    tmpStr1 = util_strcat3(options->satInFile," -t ", tmpStr2);
1275    tmpStr = util_strcat3(tmpStr1, " >", options->satOutFile);
1276    FREE(tmpStr1);
1277    FREE(tmpStr2);
1278  } else {
1279    tmpStr = util_strcat3(options->satInFile, " >", options->satOutFile);
1280  }
1281  strcat(parseBuffer, tmpStr);
1282  FREE(tmpStr);
1283 
1284  if (options->verbosityLevel == BmcVerbosityMax_c) {
1285    (void)fprintf(vis_stdout,"Calling SAT solver (cusp) ...");
1286    (void) fflush(vis_stdout);
1287    solverStart = util_cpu_ctime();
1288  } else { /* to remove uninitialized variables warning */
1289    solverStart = 0;
1290  }
1291  /* Call Sat Solver*/
1292  satStatus = system(parseBuffer);
1293  if (satStatus != 0){
1294    (void) fprintf(vis_stderr, "Can't run cusp. It may not be in your path. Status = %d\n", satStatus);
1295    options->satSolverError = TRUE;
1296    return NIL(array_t);
1297  }
1298 
1299  if (options->verbosityLevel == BmcVerbosityMax_c) {
1300    (void) fprintf(vis_stdout," done ");
1301    (void) fprintf(vis_stdout, "(%g s)\n",
1302                   (double) (util_cpu_ctime() - solverStart)/1000.0);
1303  }
1304  fp = Cmd_FileOpen(options->satOutFile, "r", NIL(char *), 0);
1305  if (fp == NIL(FILE)) {
1306    (void) fprintf(vis_stderr, "** bmc error: Cannot open the file %s\n",
1307                   options->satOutFile);
1308    options->satSolverError = TRUE;
1309    return NIL(array_t);
1310  }
1311  /* Skip the lines until the result */
1312  while(1) {
1313    if (fgets(line, MAX_LENGTH - 1, fp) == NULL) break;
1314    if(strstr(line,"UNSATISFIABLE") ||
1315       strstr(line,"SATISFIABLE") ||
1316       strstr(line,"MEMOUT") ||
1317       strstr(line,"TIMEOUT"))
1318      break;
1319  }
1320
1321  if(strstr(line,"UNSATISFIABLE") != NIL(char)) {
1322    if (options->verbosityLevel != BmcVerbosityNone_c){
1323      (void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
1324     
1325    }
1326  } else if(strstr(line,"SATISFIABLE") != NIL(char)) {
1327    if (options->verbosityLevel != BmcVerbosityNone_c){
1328      (void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
1329    }
1330    /* Skip the initial v of the result line */
1331    result = array_alloc(int, 0);
1332    while (fgets(line, MAX_LENGTH - 1, fp) != NULL) {
1333      char *word;
1334      if (line[0] != 'v') {
1335        (void) fprintf(vis_stderr,
1336                       "** bmc error: Cannot find assignment in file %s\n",
1337                       options->satOutFile);
1338        options->satSolverError = TRUE;
1339        return NIL(array_t);
1340      }
1341      word = strtok(&(line[1])," \n");
1342      while (word != NIL(char)) {
1343        num = atoi(word);
1344        if (num == 0) break;
1345        array_insert_last(int, result, num);
1346        word = strtok(NIL(char)," \n");
1347      }
1348      if (num == 0) break;
1349    }
1350  } else if(strstr(line,"MEMOUT") != NIL(char)) {
1351    (void) fprintf(vis_stdout,"# SAT: SAT Solver Memory out\n");
1352    options->satSolverError = TRUE;
1353  } else if(strstr(line,"TIMEOUT") != NIL(char)) {
1354    (void) fprintf(vis_stdout,
1355                   "# SAT: SAT Solver Time out occurred after %d seconds.\n",
1356                   satTimeOutPeriod);
1357    options->satSolverError = TRUE;
1358  } else {
1359    (void) fprintf(vis_stdout, "# SAT: SAT Solver failed, try again\n");
1360    options->satSolverError = TRUE;
1361  }
1362  (void) fflush(vis_stdout);
1363  (void) fclose(fp);
1364
1365  return result;
1366} /* BmcCallCusp */
1367
1368
1369/**Function********************************************************************
1370
1371  Synopsis [Print CounterExample.]
1372
1373  SideEffects [Print a counterexample that was returned from the SAT
1374  solver in term of an array of integer "result". The counterexample
1375  starts from state 0 and of lenght eqaual to "length". If loopClause
1376  is not empty, this function print a loopback from the last state to
1377  a state in loopClause that exist in "result".]
1378
1379******************************************************************************/
1380void
1381BmcPrintCounterExample(
1382  Ntk_Network_t   *network,
1383  st_table        *nodeToMvfAigTable,
1384  BmcCnfClauses_t *cnfClauses,
1385  array_t         *result,
1386  int             length,
1387  st_table        *CoiTable,
1388  BmcOption_t     *options,
1389  array_t         *loopClause)
1390{
1391  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
1392  lsGen             gen;
1393  st_generator      *stGen;
1394  Ntk_Node_t        *node;
1395  int               k;
1396  array_t           *latches = array_alloc(int, 0);
1397  int               *prevValueLatches;
1398  array_t           *inputs  = array_alloc(int, 0);
1399  int               *prevValueInputs;
1400  int               tmp;
1401  int               loop;
1402  st_table          *resultTable = st_init_table(st_numcmp, st_numhash);
1403
1404  /*
1405    Initialize resultTable from the result to speed up the search in the result array.
1406   */
1407  for(k=0; k< array_n(result); k++){
1408    st_insert(resultTable, (char *) (long) array_fetch(int, result, k),  (char *) 0);
1409  }
1410  /* sort latches by name */
1411  st_foreach_item(CoiTable, stGen, &node, NULL) {
1412      array_insert_last(char*, latches, Ntk_NodeReadName(node));
1413  }
1414  array_sort(latches, nameCompare);
1415  /*
1416    Use to store the last value of each latch. If the current value of a latch
1417    differs from its corresponding value in this array, we will print the new values.
1418   */
1419  prevValueLatches = ALLOC(int, array_n(latches));
1420  prevValueInputs = 0;
1421  if(options->printInputs == TRUE){
1422    /* sort inputs by name */
1423    Ntk_NetworkForEachInput(network, gen, node){
1424      array_insert_last(char*, inputs, Ntk_NodeReadName(node));
1425    }
1426    array_sort(inputs, nameCompare);
1427    prevValueInputs = ALLOC(int, array_n(inputs));
1428  }
1429  loop = -1; /* no loop back */
1430  if(loopClause != NIL(array_t)){
1431    for(k=0; k < array_n(loopClause); k++){
1432      /*  if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */
1433      if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){
1434        loop = k;
1435        break;
1436      }
1437    }
1438  }
1439  /*
1440  Ntk_NetworkForEachPrimaryOutput(network, gen, node){
1441    array_insert_last(char*, outputs, Ntk_NodeReadName(node));
1442  }
1443  array_sort(outputs, nameCompare);
1444  */
1445  for (k=0; k<= length; k++){
1446    if (k == 0){
1447      (void) fprintf(vis_stdout, "\n--State %d:\n", k);
1448    } else {
1449      (void) fprintf(vis_stdout, "\n--Goes to state %d:\n", k);
1450    }
1451    /*
1452      Print the current values of the latches if they are different form their
1453      previous values.
1454     */
1455    printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1456               latches, resultTable,  k, prevValueLatches); 
1457#if 0
1458    (void) fprintf(vis_stdout, "--Primary output:\n");
1459    printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k);
1460#endif
1461    if((options->printInputs == TRUE) && (k !=0)) {
1462      (void) fprintf(vis_stdout, "--On input:\n");
1463      printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1464                 inputs, resultTable,   k-1, prevValueInputs);   
1465    }
1466  } /* for k loop */
1467  if(loop != -1){
1468    (void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
1469    printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1470               latches, resultTable,  loop, prevValueLatches);
1471    if((options->printInputs == TRUE)) {
1472      (void) fprintf(vis_stdout, "--On input:\n");
1473      printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1474                 inputs, resultTable, length, prevValueInputs);   
1475    }
1476  }
1477  array_free(latches);
1478  FREE(prevValueLatches);
1479  if(options->printInputs == TRUE){
1480    array_free(inputs);
1481    FREE(prevValueInputs);
1482  }
1483  st_free_table(resultTable);
1484  return;
1485} /* BmcPrintCounterExample() */
1486
1487/**Function********************************************************************
1488
1489  Synopsis [Print CounterExample in Aiger format.]
1490
1491  SideEffects [Print a counterexample that was returned from the SAT
1492  solver in term of an array of integer "result". The counterexample
1493  starts from state 0 and of lenght eqaual to "length". If loopClause
1494  is not empty, this function print a loopback from the last state to
1495  a state in loopClause that exist in "result".]
1496
1497******************************************************************************/
1498void
1499BmcPrintCounterExampleAiger(
1500  Ntk_Network_t   *network,
1501  st_table        *nodeToMvfAigTable,
1502  BmcCnfClauses_t *cnfClauses,
1503  array_t         *result,
1504  int             length,
1505  st_table        *CoiTable,
1506  BmcOption_t     *options,
1507  array_t         *loopClause)
1508{
1509  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
1510  lsGen             gen;
1511  st_generator      *stGen;
1512  Ntk_Node_t        *node;
1513  int               k;
1514  array_t           *latches = array_alloc(int, 0);
1515  int               *prevValueLatches;
1516  array_t           *inputs  = array_alloc(int, 0);
1517  array_t           *outputs = array_alloc(int, 0);
1518  int               *prevValueInputs;
1519  int               *prevValueOutputs;
1520  int               tmp;
1521  int               loop;
1522  st_table          *resultTable = st_init_table(st_numcmp, st_numhash);
1523  char              *nodeName;
1524
1525  /*
1526    Initialize resultTable from the result to speed up the search in the result array.
1527   */
1528  for(k=0; k< array_n(result); k++){
1529    st_insert(resultTable, (char *) (long) array_fetch(int, result, k),  (char *) 0);
1530  }
1531  /* sort latches by name */
1532  st_foreach_item(CoiTable, stGen, &node, NULL) {
1533      array_insert_last(char*, latches, Ntk_NodeReadName(node));
1534  }
1535  /*
1536    Use to store the last value of each latch. If the current value of a latch
1537    differs from its corresponding value in this array, we will print the new values.
1538   */
1539
1540  /* the file generation needs to be removed for final vis release */
1541
1542  FILE *order = Cmd_FileOpen("inputOrder.txt", "w", NIL(char *), 0);
1543  for (k=0; k< array_n(latches); k++)
1544  {
1545    nodeName = array_fetch(char *, latches, k);
1546    if((nodeName[0] == '$') && (nodeName[1] == '_'))
1547    {
1548      fprintf(order, "%s\n", &nodeName[2]);
1549    }
1550  }
1551  fclose(order);
1552
1553  prevValueLatches = ALLOC(int, array_n(latches));
1554  Ntk_NetworkForEachInput(network, gen, node){
1555    array_insert_last(char*, inputs, Ntk_NodeReadName(node));
1556  }
1557
1558  prevValueInputs = ALLOC(int, array_n(inputs));
1559  loop = -1; /* no loop back */
1560  if(loopClause != NIL(array_t)){
1561    for(k=0; k < array_n(loopClause); k++){
1562      /*  if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */
1563      if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){
1564        loop = k;
1565        break;
1566      }
1567    }
1568  }
1569 
1570  Ntk_NetworkForEachPrimaryOutput(network, gen, node){
1571    array_insert_last(char*, outputs, Ntk_NodeReadName(node));
1572  }
1573  prevValueOutputs = ALLOC(int, array_n(outputs));
1574
1575  for (k=0; k< length; k++){
1576    /* This will print latches whose name doesn't start with $_. The latches whose
1577       name starts with $_ are latches added to the model by the aigtoblif translator.
1578     */
1579    printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
1580               latches, resultTable,  k, prevValueLatches); 
1581    fprintf(vis_stdout, " ");
1582#if 0
1583    (void) fprintf(vis_stdout, "--Primary output:\n");
1584    printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k);
1585#endif
1586
1587    if((loop<0)||(k<length))
1588    {
1589
1590      /* we augment the original .mv model with latches in front of inputs and hence
1591         instead of inputs we print out the value of latches, this would have to be
1592         restored in the final release */
1593
1594      printValueAigerInputs(manager, network, nodeToMvfAigTable, cnfClauses,
1595                 latches, resultTable,   k, prevValueInputs);   
1596      fprintf(vis_stdout, " ");
1597
1598      /* the sat-solver doesn't propagate the values to output so we generate the output
1599         1 knowing when ouptut would be 1, we will have to remove this for vis release */
1600
1601      if((k+1)==length)
1602      {
1603        fprintf(vis_stdout, "1 ");
1604      }
1605      else
1606      {
1607        fprintf(vis_stdout, "0 ");
1608      }
1609
1610      printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
1611               latches, resultTable,  k+1, prevValueLatches); 
1612    }
1613    if((loop < 0)||(k!=length))
1614    {
1615      fprintf(vis_stdout, "\n");
1616    }
1617
1618  } /* for k loop */
1619  if(loop != -1){
1620    (void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
1621    printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
1622               latches, resultTable,  loop, prevValueLatches);
1623    (void) fprintf(vis_stdout, "--On input:\n");
1624    printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
1625                 inputs, resultTable, length, prevValueInputs);   
1626  }
1627  array_free(latches);
1628  FREE(prevValueLatches);
1629  if(options->printInputs == TRUE){
1630    array_free(inputs);
1631    FREE(prevValueInputs);
1632  }
1633  st_free_table(resultTable);
1634  return;
1635} /* BmcPrintCounterExampleAiger() */
1636
1637
1638/**Function********************************************************************
1639
1640  Synopsis [Print CounterExample.]
1641
1642  SideEffects [Print a counterexample that was returned from the SAT
1643  solver in term of an array of integer "result". The counterexample
1644  starts from state 0 and of lenght eqaual to "length". If loopClause
1645  is not empty, this function print a loopback from the last state to
1646  a state in loopClause that exist in "result".]
1647
1648******************************************************************************/
1649void
1650BmcAutPrintCounterExample(
1651  Ntk_Network_t   *network,
1652  Ltl_Automaton_t *automaton,
1653  st_table        *nodeToMvfAigTable,
1654  BmcCnfClauses_t *cnfClauses,
1655  array_t         *result,
1656  int             length,
1657  st_table        *CoiTable,
1658  BmcOption_t     *options,
1659  array_t         *loopClause)
1660{
1661  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
1662  lsGen             gen;
1663  st_generator      *stGen;
1664  Ntk_Node_t        *node;
1665  int               k;
1666  array_t           *latches = array_alloc(int, 0);
1667  int               *prevValueLatches;
1668  array_t           *inputs  = array_alloc(int, 0);
1669  int               *prevValueInputs;
1670  int               tmp;
1671  int               loop;
1672  st_table          *resultTable = st_init_table(st_numcmp, st_numhash);
1673
1674  /*
1675    Initialize resultTable from the result to speed up the search in the result array.
1676   */
1677  for(k=0; k< array_n(result); k++){
1678    st_insert(resultTable, (char *) (long) array_fetch(int, result, k),  (char *) 0);
1679  }
1680  /* sort latches by name */
1681  st_foreach_item(CoiTable, stGen, &node, NULL) {
1682      array_insert_last(char*, latches, Ntk_NodeReadName(node));
1683  }
1684  array_sort(latches, nameCompare);
1685  /*
1686    Use to store the last value of each latch. If the current value of a latch
1687    differs from its corresponding value in this array, we will print the new values.
1688   */
1689  prevValueLatches = ALLOC(int, array_n(latches));
1690  prevValueInputs = 0;
1691  if(options->printInputs == TRUE){
1692    /* sort inputs by name */
1693    Ntk_NetworkForEachInput(network, gen, node){
1694      array_insert_last(char*, inputs, Ntk_NodeReadName(node));
1695    }
1696    array_sort(inputs, nameCompare);
1697    prevValueInputs = ALLOC(int, array_n(inputs));
1698  }
1699  loop = -1; /* no loop back */
1700  if(loopClause != NIL(array_t)){
1701    for(k=0; k < array_n(loopClause); k++){
1702      /*  if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */
1703      if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){
1704        loop = k;
1705        break;
1706      }
1707    }
1708  }
1709  /*
1710  Ntk_NetworkForEachPrimaryOutput(network, gen, node){
1711    array_insert_last(char*, outputs, Ntk_NodeReadName(node));
1712  }
1713  array_sort(outputs, nameCompare);
1714  */
1715  for (k=0; k<= length; k++){
1716    if (k == 0){
1717      (void) fprintf(vis_stdout, "\n--State %d:\n", k);
1718    } else {
1719      (void) fprintf(vis_stdout, "\n--Goes to state %d:\n", k);
1720    }
1721    /*
1722      Print the current values of the latches if they are different form their
1723      previous values.
1724     */
1725    printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1726               latches, resultTable,  k, prevValueLatches);
1727
1728    {
1729      lsGen               lsGen;
1730      vertex_t            *vtx;
1731      Ltl_AutomatonNode_t *state;
1732      int                 stateIndex;
1733      bdd_node            *node;
1734      int                 is_complemented;
1735     
1736       
1737      foreach_vertex(automaton->G, lsGen, vtx) {
1738        state = (Ltl_AutomatonNode_t *) vtx->user_data;
1739       
1740        node = bdd_get_node(state->Encode, &is_complemented);
1741       
1742        stateIndex  = state->cnfIndex[k];
1743
1744
1745
1746       
1747        if (st_lookup_int(resultTable, (char *)(long)stateIndex, &tmp)){
1748          (void) fprintf(vis_stdout,"n%d \n", state->index);
1749        }
1750      }
1751    }
1752#if 0
1753    (void) fprintf(vis_stdout, "--Primary output:\n");
1754    printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k);
1755#endif
1756    if((options->printInputs == TRUE) && (k !=0)) {
1757      (void) fprintf(vis_stdout, "--On input:\n");
1758      printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1759                 inputs, resultTable,   k-1, prevValueInputs);   
1760    }
1761  } /* for k loop */
1762  if(loop != -1){
1763    (void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
1764    printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1765               latches, resultTable,  loop, prevValueLatches);
1766    if((options->printInputs == TRUE)) {
1767      (void) fprintf(vis_stdout, "--On input:\n");
1768      printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1769                 inputs, resultTable, length, prevValueInputs);   
1770    }
1771  }
1772  array_free(latches);
1773  FREE(prevValueLatches);
1774  if(options->printInputs == TRUE){
1775    array_free(inputs);
1776    FREE(prevValueInputs);
1777  }
1778  st_free_table(resultTable);
1779  return;
1780} /* BmcPrintCounterExample() */
1781
1782
1783/**Function********************************************************************
1784
1785  Synopsis    [Generate CNF formula for a path from state 'from' to state 'to']
1786
1787  Description [Unfold the transition relation 'k' states (k = to-from +1), and
1788  generate clauses for each state.
1789 
1790           For a multi-valued latch of 4 vlaues. Two binary variables are used
1791           to rpresent X, x1 and x0. For this latch, there exist three multi-valued
1792           functions.
1793           One for the binary reoresentation of the variable. For example the
1794           second entry of the mvf = 1, iff ~x1 and x0.
1795           The second mfv is for the data input of the latch. If the And/Inv graph
1796           attached to an entry of this mvf equal to 1, X equal to the binary
1797           representation corresponding to this entry. For example, if the And/
1798           INV graph attached to the first entry =1, then X = ~x1 & ~x0.
1799           To generate the CNF to the transition relation, first generate CNF to
1800           next state varaible using mvf of the latch.  Then, generate CNF for
1801           latch data input using current state variavles. Finaly, generate CNF
1802           for the AND of these two MVF.  This for every entry of the MVF. Then
1803           OR the results.
1804           The third MVF is for the initial value of the latch.  It is treat the
1805           same as the latch data input except if the initial value is constant.
1806   
1807  The initialState value may be either BMC_INITIAL_STATES to generate the clause for the intial states.
1808  BMC_NO_INITIAL_STATES otherwise.
1809  ]
1810
1811  SideEffects []
1812
1813  SeeAlso     []
1814
1815******************************************************************************/
1816void
1817BmcCnfGenerateClausesForPath(
1818   Ntk_Network_t   *network,
1819   int             from,
1820   int             to,
1821   int             initialState,
1822   BmcCnfClauses_t *cnfClauses,
1823   st_table        *nodeToMvfAigTable,
1824   st_table        *CoiTable)
1825{
1826  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
1827  st_generator    *stGen;
1828 
1829  Ntk_Node_t         *latch, *latchData, *latchInit;
1830  MvfAig_Function_t  *initMvfAig, *dataMvfAig, *latchMvfAig;
1831  bAigEdge_t         *initBAig, *latchBAig, *dataBAig;
1832 
1833  int        i, k, mvfSize;
1834
1835  st_foreach_item(CoiTable, stGen, &latch, NULL) {
1836   
1837 
1838   latchInit  = Ntk_LatchReadInitialInput(latch);
1839   latchData  = Ntk_LatchReadDataInput(latch);
1840
1841   /* Get the multi-valued function for each node*/
1842   initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
1843   if (initMvfAig ==  NIL(MvfAig_Function_t)){
1844     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit));
1845     return;
1846   } 
1847   dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
1848   if (dataMvfAig ==  NIL(MvfAig_Function_t)){
1849     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchData));
1850     return;
1851   }
1852   latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1853   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
1854     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
1855     array_free(latchMvfAig);
1856     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1857   }
1858     
1859   mvfSize   = array_n(initMvfAig);
1860   initBAig  = ALLOC(bAigEdge_t, mvfSize);
1861   dataBAig  = ALLOC(bAigEdge_t, mvfSize);
1862   latchBAig = ALLOC(bAigEdge_t, mvfSize);   
1863
1864   for(i=0; i< mvfSize; i++){
1865     dataBAig[i]  = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(dataMvfAig,  i));
1866     latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
1867     initBAig[i]  = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(initMvfAig,  i));
1868   }
1869   /*
1870   if (from == 0){
1871   */
1872   if (initialState == BMC_INITIAL_STATES){
1873   /* Generate the CNF for the initial state of the latch */
1874     BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
1875   }
1876   /* Generate the CNF for the transition functions */   
1877   for (k=from; k < to; k++){
1878     BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
1879   } /* for k state loop */
1880
1881   FREE(initBAig);
1882   FREE(dataBAig);
1883   FREE(latchBAig);
1884  }/* For each latch loop*/
1885 
1886  return;
1887}
1888
1889/**Function********************************************************************
1890
1891  Synopsis    [Generate CNF formula for a loop-free path]
1892
1893  Description [This function generates CNF formula for a loop-free path from
1894  state fromState to state toState. A loop free path is a path from a state S0
1895  to state Sn such that every state in the path is distinct. i.e for all states
1896  in the path Si != Sj for 0<= i < j <= n.
1897           
1898  The initialState value may be either BMC_INITIAL_STATES to generate the clause
1899  for the intial states. BMC_NO_INITIAL_STATES otherwise.
1900  ]
1901
1902  SideEffects []
1903
1904  SeeAlso     []
1905
1906******************************************************************************/
1907void
1908BmcCnfGenerateClausesForLoopFreePath(
1909   Ntk_Network_t   *network,
1910   int             fromState,
1911   int             toState,
1912   int             initialState,
1913   BmcCnfClauses_t *cnfClauses,
1914   st_table        *nodeToMvfAigTable,
1915   st_table        *CoiTable)
1916{
1917  int state;
1918 
1919  /*
1920    Generate clauses for a path from fromState to toState.
1921  */
1922  BmcCnfGenerateClausesForPath(network, fromState, toState, initialState, cnfClauses, nodeToMvfAigTable, CoiTable);
1923 
1924  /*
1925    Restrict the above path to be loop-free path.
1926  */
1927  /*
1928    for(state=0; state< toState; state++){
1929  */
1930  /*
1931    Don't include the last state because we know it is not equal any of the previous states.
1932    The property fails at this state, and true at all other states.
1933   */
1934  /*
1935  for(state=1; state < toState; state++){
1936  */
1937  for(state= fromState + 1; state <= toState; state++){
1938    BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates(network, fromState, state, cnfClauses, nodeToMvfAigTable, CoiTable);
1939  }
1940
1941  return;
1942}
1943
1944/**Function********************************************************************
1945
1946  Synopsis    [Generate Clauses for no loop from last state to any of the
1947  previouse states]
1948
1949  Description [Generate Clauses for no loop from last state (toState) to
1950  any of the previous states starting from fromState. It generates the CNF
1951  clauses such that the last state of the path is not equal to any of the
1952  path previous states.
1953  ]
1954
1955  SideEffects []
1956
1957  SeeAlso     []
1958
1959******************************************************************************/
1960void
1961BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates(
1962   Ntk_Network_t   *network,
1963   int             fromState,
1964   int             toState,
1965   BmcCnfClauses_t *cnfClauses,
1966   st_table        *nodeToMvfAigTable,
1967   st_table        *CoiTable)
1968{
1969  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
1970  st_generator    *stGen;
1971 
1972  Ntk_Node_t         *latch;
1973  MvfAig_Function_t  *latchMvfAig;
1974  bAigEdge_t         *latchBAig;
1975  array_t            *orClause;
1976  int                lastIndex, prevIndex, andIndex1, andIndex2; 
1977  int                i, k, mvfSize;
1978
1979  /*
1980    Generates the clauses to check if the toState is not equal to any previouse states starting
1981    from fromState.
1982   
1983    Assume there are two state varaibles a and b. To check if Si != Sj, we must generate clauses
1984    for the formula ( ai != aj + bi != bj).
1985  */
1986  for(k=fromState; k < toState; k++){
1987    orClause = array_alloc(int,0);
1988    st_foreach_item(CoiTable, stGen, &latch, NULL) {
1989     
1990 
1991      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1992      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
1993        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
1994        array_free(latchMvfAig);
1995        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1996      } 
1997      mvfSize   = array_n(latchMvfAig);
1998      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
1999     
2000      for(i=0; i< mvfSize; i++){
2001        latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
2002      }
2003
2004      for (i=0; i< mvfSize; i++){
2005        prevIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k       ,cnfClauses);
2006        lastIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses);     
2007        andIndex1 = cnfClauses->cnfGlobalIndex++;
2008        BmcCnfGenerateClausesForAND(prevIndex, -lastIndex, andIndex1, cnfClauses);
2009        andIndex2 = cnfClauses->cnfGlobalIndex++;
2010        BmcCnfGenerateClausesForAND(-prevIndex, lastIndex, andIndex2, cnfClauses);
2011
2012        array_insert_last(int, orClause, andIndex1);
2013        array_insert_last(int, orClause, andIndex2);
2014      }
2015      FREE(latchBAig);
2016    }/* For each latch loop*/
2017    BmcCnfInsertClause(cnfClauses, orClause);
2018    array_free(orClause);
2019  } /* foreach k*/
2020  return;
2021}
2022
2023
2024/**Function********************************************************************
2025
2026  Synopsis    [Generate Clauses for last state equal to any of the
2027  previouse states]
2028
2029  Description [ Change it!
2030  Generate Clauses for no loop from last state (toState) to
2031  any of the previous states starting from fromState. It generates the CNF
2032  clauses such that the last state of the path is not equal to any of the
2033  path previous states.
2034  ]
2035
2036  SideEffects []
2037
2038  SeeAlso     []
2039
2040******************************************************************************/
2041void
2042BmcCnfGenerateClausesForLoopToAnyPreviouseStates(
2043   Ntk_Network_t   *network,
2044   int             fromState,
2045   int             toState,
2046   BmcCnfClauses_t *cnfClauses,
2047   st_table        *nodeToMvfAigTable,
2048   st_table        *CoiTable)
2049{
2050  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
2051  st_generator    *stGen;
2052 
2053  Ntk_Node_t         *latch;
2054  MvfAig_Function_t  *latchMvfAig;
2055  bAigEdge_t         *latchBAig;
2056  array_t            *orClause;
2057  int                lastIndex, prevIndex, andIndex1, andIndex2; 
2058  int                i, k, mvfSize;
2059
2060  /*
2061    Generates the clauses to check if the toState is not equal to any previouse states starting
2062    from fromState.
2063   
2064    Assume there are two state varaibles a and b. To check if Si != Sj, we must generate clauses
2065    for the formula ( ai != aj + bi != bj).
2066  */
2067  for(k=fromState; k < toState; k++){
2068    orClause = array_alloc(int,0);
2069    st_foreach_item(CoiTable, stGen, &latch, NULL) {
2070     
2071 
2072      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
2073      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
2074        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
2075        array_free(latchMvfAig);
2076        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
2077      } 
2078      mvfSize   = array_n(latchMvfAig);
2079      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
2080     
2081      for(i=0; i< mvfSize; i++){
2082        latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
2083      }
2084
2085      for (i=0; i< mvfSize; i++){
2086        prevIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k       ,cnfClauses);
2087        lastIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses);     
2088        andIndex1 = cnfClauses->cnfGlobalIndex++;
2089        BmcCnfGenerateClausesForAND(prevIndex, lastIndex, andIndex1, cnfClauses);
2090        andIndex2 = cnfClauses->cnfGlobalIndex++;
2091        BmcCnfGenerateClausesForAND(-prevIndex, -lastIndex, andIndex2, cnfClauses);
2092
2093        array_insert_last(int, orClause, andIndex1);
2094        array_insert_last(int, orClause, andIndex2);
2095      }
2096      FREE(latchBAig);
2097    }/* For each latch loop*/
2098    BmcCnfInsertClause(cnfClauses, orClause);
2099    array_free(orClause);
2100  } /* foreach k*/
2101  return;
2102}
2103
2104/**Function********************************************************************
2105
2106  Synopsis    [Generate CNF formula for a path from state 'from' to state 'to']
2107
2108  Description [Unfold the transition relation 'k' states (k = to-from +1), and
2109  generate clauses for each state.
2110           For a multi-valued latch of 4 vlaues. Two binary variables are used
2111           to rpresent X, x1 and x0. For this latch, there exist three multi-valued
2112           functions.
2113           One for the binary reoresentation of the variable. For example the
2114           second entry of the mvf = 1, iff ~x1 and x0.
2115           The second mfv is for the data input of the latch. If the And/Inv graph
2116           attached to an entry of this mvf equal to 1, X equal to the binary
2117           representation corresponding to this entry. For example, if the And/
2118           INV graph attached to the first entry =1, then X = ~x1 & ~x0.
2119           To generate the CNF to the transition relation, first generate CNF to
2120           next state varaible using mvf of the latch.  Then, generate CNF for
2121           latch data input using current state variavles. Finaly, generate CNF
2122           for the AND of these two MVF.  This for every entry of the MVF. Then
2123           OR the results.
2124           The third MVF is for the initial value of the latch.  It is treat the
2125           same as the latch data input except if the initial value is constant.         
2126           ]
2127
2128  SideEffects []
2129
2130  SeeAlso     []
2131
2132******************************************************************************/
2133void
2134BmcCnfGenerateClausesFromStateToState(
2135   Ntk_Network_t   *network,
2136   int             from,
2137   int             to,
2138   BmcCnfClauses_t *cnfClauses,
2139   st_table        *nodeToMvfAigTable,
2140   st_table        *CoiTable,
2141   int             loop)
2142{
2143  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
2144  st_generator    *stGen;
2145  Ntk_Node_t         *latch, *latchData;
2146  MvfAig_Function_t  *dataMvfAig, *latchMvfAig;
2147  bAigEdge_t         *latchBAig, *dataBAig;
2148  int        i, mvfSize;
2149
2150  st_foreach_item(CoiTable, stGen, &latch, NULL) {
2151    latchData  = Ntk_LatchReadDataInput(latch);
2152   
2153    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
2154    if (dataMvfAig ==  NIL(MvfAig_Function_t)){
2155      (void) fprintf(vis_stdout,
2156                     "No multi-valued function for this node %s \n",
2157                     Ntk_NodeReadName(latchData));
2158      return;
2159    }
2160    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
2161    if (latchMvfAig ==  NIL(MvfAig_Function_t)){
2162      latchMvfAig = Bmc_NodeBuildMVF(network, latch);
2163    }
2164    mvfSize   = array_n(dataMvfAig);
2165    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
2166    latchBAig = ALLOC(bAigEdge_t, mvfSize);
2167    for(i=0; i< mvfSize; i++){
2168      dataBAig[i]  = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(dataMvfAig,  i));
2169      latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
2170    }
2171    BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize,
2172                                       from, to, cnfClauses, loop);
2173    FREE(dataBAig);
2174    FREE(latchBAig);
2175  } /* For each latch loop*/ 
2176  return;
2177}
2178
2179/**Function********************************************************************
2180
2181  Synopsis    [Generate CNF clauses for the AND gate]
2182
2183  Description []
2184
2185  SideEffects []
2186
2187  SeeAlso     []
2188
2189******************************************************************************/
2190void 
2191BmcCnfGenerateClausesForAND(
2192   int             a,
2193   int             b,
2194   int             c,
2195   BmcCnfClauses_t *cnfClauses)
2196{
2197  array_t     *tmpClause;
2198   
2199  tmpClause = array_alloc(int, 3);
2200  array_insert(int, tmpClause, 0, -a);
2201  array_insert(int, tmpClause, 1, -b);
2202  array_insert(int, tmpClause, 2, c);
2203  BmcCnfInsertClause(cnfClauses, tmpClause);
2204  array_free(tmpClause);
2205 
2206  tmpClause = array_alloc(int, 2);
2207 
2208  array_insert(int, tmpClause, 0, a);
2209  array_insert(int, tmpClause, 1, -c);
2210  BmcCnfInsertClause(cnfClauses, tmpClause);
2211 
2212  array_insert(int, tmpClause, 0, b);
2213  BmcCnfInsertClause(cnfClauses, tmpClause);
2214       
2215  array_free(tmpClause);
2216  return;
2217}
2218
2219/**Function********************************************************************
2220
2221  Synopsis    [Generate CNF clauses for the OR gate]
2222
2223  Description []
2224
2225  SideEffects []
2226
2227  SeeAlso     []
2228
2229******************************************************************************/
2230void 
2231BmcCnfGenerateClausesForOR(
2232   int             a,
2233   int             b,
2234   int             c,
2235   BmcCnfClauses_t *cnfClauses)
2236{
2237  array_t     *tmpClause;
2238   
2239  tmpClause = array_alloc(int, 3);
2240  array_insert(int, tmpClause, 0, a);
2241  array_insert(int, tmpClause, 1, b);
2242  array_insert(int, tmpClause, 2, -c);
2243  BmcCnfInsertClause(cnfClauses, tmpClause);
2244  array_free(tmpClause);
2245 
2246  tmpClause = array_alloc(int, 2);
2247  array_insert(int, tmpClause, 0, -a);
2248  array_insert(int, tmpClause, 1, c);
2249  BmcCnfInsertClause(cnfClauses, tmpClause);
2250 
2251  array_insert(int, tmpClause, 0, -b);
2252  BmcCnfInsertClause(cnfClauses, tmpClause);
2253       
2254  array_free(tmpClause);
2255  return;
2256}
2257
2258/**Function********************************************************************
2259
2260  Synopsis [Alloc Memory for BmcCnfClauses_t]
2261
2262  SideEffects []
2263
2264  SeeAlso []
2265******************************************************************************/
2266BmcCnfClauses_t *
2267BmcCnfClausesAlloc(void)
2268{
2269  BmcCnfClauses_t *result = ALLOC(BmcCnfClauses_t, 1);
2270 
2271  if (!result){
2272    return result;
2273  }
2274  result->clauseArray    = array_alloc(int, 0);
2275  result->cnfIndexTable  = st_init_table(strcmp, st_strhash);
2276  result->freezedKeys    = array_alloc(nameType_t *, 0);
2277 
2278  result->nextIndex      = 0;
2279  result->noOfClauses    = 0;
2280  result->cnfGlobalIndex = 1; 
2281  result->emptyClause    = FALSE;
2282  result->freezed        = FALSE;
2283
2284  return result;
2285} /*BmcCnfClausesAlloc()*/
2286
2287/**Function********************************************************************
2288
2289  Synopsis [Free Memory for BmcCnfClauses_t]
2290
2291  SideEffects []
2292
2293  SeeAlso []
2294******************************************************************************/
2295void 
2296BmcCnfClausesFree(
2297  BmcCnfClauses_t *cnfClauses)
2298{
2299  st_generator *stGen;
2300  char         *name;
2301  int          cnfIndex;
2302
2303  array_free(cnfClauses->clauseArray);
2304  array_free(cnfClauses->freezedKeys);
2305
2306  if (cnfClauses->cnfIndexTable != NIL(st_table)){
2307    st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, (char **) &name, &cnfIndex) {
2308      FREE(name);
2309    }
2310    st_free_table(cnfClauses->cnfIndexTable);
2311  }
2312  FREE(cnfClauses);
2313  cnfClauses = NIL(BmcCnfClauses_t);
2314} /* BmcCnfClausesFree() */
2315
2316/**Function********************************************************************
2317
2318  Synopsis [Freeze the current state of CNF]
2319
2320  Description [The current state of CNF is stored in the structure BmcCnfStates_t.
2321  This information may use later to store CNF to this state by calling
2322  BmcCnfClausesRestore().]
2323
2324  SideEffects []
2325
2326  SeeAlso [BmcCnfClausesRestore() BmcCnfClausesUnFreeze() ]
2327******************************************************************************/
2328BmcCnfStates_t *
2329BmcCnfClausesFreeze(
2330  BmcCnfClauses_t * cnfClauses)
2331{
2332  BmcCnfStates_t *state = ALLOC(BmcCnfStates_t, 1);
2333
2334  state->nextIndex      = cnfClauses->nextIndex;
2335  state->noOfClauses    = cnfClauses->noOfClauses;
2336  state->cnfGlobalIndex = cnfClauses->cnfGlobalIndex;
2337
2338  /* This variable is used when deleting any new entries in cnfClauses->freezedKeys
2339   that will be added after CNF is freezed.*/
2340  state->freezedKeySize = array_n(cnfClauses->freezedKeys);
2341 
2342  state->emptyClause    = cnfClauses->emptyClause;
2343  state->freezed        = cnfClauses->freezed;
2344  cnfClauses->freezed   = TRUE;
2345  return state;
2346} /* mcCnfClausesFreeze() */
2347
2348/**Function********************************************************************
2349
2350  Synopsis [Unfreeze CNF]
2351
2352  Description [Keeps the current state of CNF]
2353
2354  SideEffects []
2355
2356  SeeAlso []
2357******************************************************************************/
2358void 
2359BmcCnfClausesUnFreeze(
2360  BmcCnfClauses_t *cnfClauses,
2361  BmcCnfStates_t  *state)
2362{
2363  int i;
2364
2365  cnfClauses->freezed = FALSE;
2366  if (array_n(cnfClauses->freezedKeys) != 0){
2367    int freezedKeySize = array_n(cnfClauses->freezedKeys);
2368   
2369    for (i=0; i< (freezedKeySize-state->freezedKeySize); i++){
2370      (cnfClauses->freezedKeys)->num--;
2371    }
2372  }
2373} /* BmcCnfClausesUnFreeze() */
2374
2375/**Function********************************************************************
2376
2377  Synopsis [Restore the CNF to its previouse state]
2378
2379  Description [Restore the CNF to its previouse state that CNF was when
2380  BmcCnfClausesFreeze() was last called]
2381
2382  SideEffects []
2383 
2384  SeeAlso []
2385******************************************************************************/
2386void 
2387BmcCnfClausesRestore(
2388  BmcCnfClauses_t *cnfClauses,
2389  BmcCnfStates_t  *state)
2390{
2391  int        i, index;
2392  nameType_t *key;
2393
2394  cnfClauses->nextIndex      = state->nextIndex;
2395  cnfClauses->noOfClauses    = state->noOfClauses;
2396  cnfClauses->cnfGlobalIndex = state->cnfGlobalIndex;
2397  cnfClauses->emptyClause    = state->emptyClause;
2398  cnfClauses->freezed        = state->freezed;
2399 
2400  if (array_n(cnfClauses->freezedKeys) != 0){
2401    int freezedKeySize = array_n(cnfClauses->freezedKeys);
2402                       
2403    for (i=0; i< (freezedKeySize-state->freezedKeySize); i++){
2404      key = array_fetch_last(nameType_t *, cnfClauses->freezedKeys);
2405      if (st_delete_int(cnfClauses->cnfIndexTable, &key, &index)){
2406        FREE(key);
2407      } 
2408      (cnfClauses->freezedKeys)->num--;
2409    }
2410  }
2411} /* BmcCnfClausesRestore() */
2412
2413/**Function********************************************************************
2414
2415  Synopsis [Add clause to the clauseArray]
2416
2417  Description [Add a clause to the clause array.  clause is of type array_t.
2418  The user must free clause.]
2419
2420  SideEffects []
2421 
2422  SeeAlso []
2423******************************************************************************/
2424void 
2425BmcCnfInsertClause(
2426  BmcCnfClauses_t *cnfClauses,
2427  array_t         *clause)
2428{
2429  int  i, lit;
2430
2431  if (clause != NIL(array_t)){
2432    if (array_n(clause) == 0){ /* empty clause */
2433      cnfClauses->emptyClause = TRUE;
2434      return;
2435    }
2436    for (i=0; i< array_n(clause); i++){
2437      lit = array_fetch(int, clause, i);
2438      array_insert(int, cnfClauses->clauseArray, cnfClauses->nextIndex++, lit);
2439    }
2440    array_insert(int, cnfClauses->clauseArray, cnfClauses->nextIndex++, 0); /*End Of clause*/
2441    cnfClauses->noOfClauses++;
2442    cnfClauses->emptyClause = FALSE;
2443  }
2444  return;
2445}/* BmcCnfInsertClause() */
2446
2447/**Function********************************************************************
2448
2449  Synopsis [Add an empty clause]
2450
2451  SideEffects []
2452
2453  SeeAlso []
2454******************************************************************************/
2455void
2456BmcAddEmptyClause(
2457  BmcCnfClauses_t *cnfClauses)
2458{
2459  cnfClauses->emptyClause = TRUE;
2460}/* BmcAddEmptyClause() */
2461
2462/**Function********************************************************************
2463
2464  Synopsis [Return the cnfIndex of the node]
2465
2466  Description [If CNF was generated for this node, return its cnfIndex, otherwise
2467  insert the name of this node in the cnfIndexTable, and return its cnfIndex. The
2468  key to the cnfIndexTable is (nodeName_state).]
2469
2470  SideEffects []
2471******************************************************************************/
2472int
2473BmcCnfReadOrInsertNode(
2474   BmcCnfClauses_t *cnfClauses,
2475   nameType_t      *nodeName,
2476   int             state,
2477   int             *nodeIndex)
2478{
2479  nameType_t *varName;
2480  int        index;
2481  char       *stateStr = util_inttostr(state);
2482
2483  varName  = util_strcat3(nodeName, "_", stateStr);
2484  FREE(stateStr);
2485  if (!st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
2486    index = cnfClauses->cnfGlobalIndex++;
2487    st_insert(cnfClauses->cnfIndexTable, varName, (char*) (long) index);
2488    if(cnfClauses->freezed == TRUE){
2489      array_insert_last(nameType_t *, cnfClauses->freezedKeys, varName);
2490    }
2491    *nodeIndex = index;
2492    return 0; /* Inserted */
2493  }
2494  else { /* The node has been visited */
2495    *nodeIndex = index;
2496    FREE(varName);
2497    return 1;     
2498  }
2499}
2500
2501
2502/**Function********************************************************************
2503
2504  Synopsis    [Find the Cone of Influnce (COI) for an LTL formula]
2505
2506  Description [Return a list of state variables (latches) that are in the COI of the
2507  LTL formula.]
2508
2509  SideEffects []
2510
2511******************************************************************************/
2512void
2513BmcGetCoiForLtlFormula(
2514  Ntk_Network_t   *network,
2515  Ctlsp_Formula_t *formula,
2516  st_table        *ltlCoiTable)
2517{
2518  st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);
2519 
2520  BmcGetCoiForLtlFormulaRecursive(network, formula, ltlCoiTable, visited);
2521  st_free_table(visited);
2522  return;
2523} /* BmcGetCoiForLtlFormula() */
2524
2525/**Function********************************************************************
2526
2527  Synopsis    [Recursive function to find the COI of a network node.]
2528
2529  Description []
2530
2531  SideEffects []
2532
2533******************************************************************************/
2534void
2535BmcGetCoiForLtlFormulaRecursive(
2536  Ntk_Network_t   *network,
2537  Ctlsp_Formula_t *formula,
2538  st_table        *ltlCoiTable,
2539  st_table        *visited)
2540{
2541  if (formula == NIL(Ctlsp_Formula_t)) {
2542    return;
2543  }
2544  /* leaf node */
2545  if (formula->type == Ctlsp_ID_c){
2546    char       *name = Ctlsp_FormulaReadVariableName(formula);
2547    Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, name);
2548    int        tmp;
2549
2550    if (st_lookup_int(visited, (char *) node, &tmp)){
2551      /* Node already visited */
2552      return;
2553    }
2554    BmcGetCoiForNtkNode(node, ltlCoiTable, visited);
2555    return;
2556  }
2557  BmcGetCoiForLtlFormulaRecursive(network, formula->left,  ltlCoiTable, visited);
2558  BmcGetCoiForLtlFormulaRecursive(network, formula->right, ltlCoiTable, visited);
2559
2560  return;
2561} /* BmcGetCoiForLtlFormulaRecursive() */
2562
2563/**Function********************************************************************
2564
2565  Synopsis    [Genrate COI for a non-latch network node]
2566
2567  Description [For each fanins of the given node, if its latch, add it
2568  to the CoiTable and return. If it is not latch, call this function to
2569  look for any latches in the fanins of this node.]
2570
2571  SideEffects []
2572
2573******************************************************************************/
2574void
2575BmcGetCoiForNtkNode(
2576  Ntk_Node_t  *node,
2577  st_table    *CoiTable,
2578  st_table    *visited)
2579{
2580  int        i, j;
2581  Ntk_Node_t *faninNode;
2582
2583  if(node == NIL(Ntk_Node_t)){
2584    return;
2585  }
2586  if (st_lookup_int(visited, (char *) node, &j)){
2587    /* Node already visited */
2588    return;
2589  }
2590  st_insert(visited, (char *) node, (char *) 0);
2591  if (Ntk_NodeTestIsLatch(node)){
2592    st_insert(CoiTable, (char *) node, (char *) 0);
2593  }
2594  Ntk_NodeForEachFanin(node, i, faninNode) {
2595    BmcGetCoiForNtkNode(faninNode, CoiTable, visited);
2596  }
2597  return;
2598} /* BmcGetCoiForNtkNode() */
2599
2600
2601/**Function********************************************************************
2602
2603  Synopsis    [Find Mdd for states satisfying Atomic Formula.]
2604
2605  Description [An atomic formula defines a set of states in the following
2606  way: it states a designated ``net'' (specified by the full path name)
2607  takes a certain value. The net should be purely a function of latches;
2608  as a result an evaluation of the net yields a set of states.]
2609
2610  SideEffects []
2611
2612******************************************************************************/
2613
2614mdd_t *
2615BmcModelCheckAtomicFormula(
2616  Fsm_Fsm_t *modelFsm,
2617  Ctlsp_Formula_t *ctlFormula)
2618{
2619  mdd_t * resultMdd;
2620  mdd_t *tmpMdd;
2621  Ntk_Network_t *network = Fsm_FsmReadNetwork(modelFsm);
2622  char *nodeNameString = Ctlsp_FormulaReadVariableName(ctlFormula);
2623  char *nodeValueString = Ctlsp_FormulaReadValueName(ctlFormula);
2624  Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
2625
2626  Var_Variable_t *nodeVar;
2627  int nodeValue;
2628
2629  graph_t *modelPartition;
2630  vertex_t *partitionVertex;
2631  Mvf_Function_t *MVF;
2632
2633  nodeVar = Ntk_NodeReadVariable(node);
2634  if (Var_VariableTestIsSymbolic(nodeVar)) {
2635    nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
2636  }
2637  else {
2638    nodeValue = atoi(nodeValueString);
2639  }
2640
2641  modelPartition = Part_NetworkReadPartition(network);
2642  if (!(partitionVertex = Part_PartitionFindVertexByName(modelPartition,
2643                                                         nodeNameString))) {
2644    lsGen tmpGen;
2645    Ntk_Node_t *tmpNode;
2646    array_t *mvfArray;
2647    array_t *tmpRoots = array_alloc(Ntk_Node_t *, 0);
2648    st_table *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
2649    array_insert_last(Ntk_Node_t *, tmpRoots, node);
2650
2651    Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) {
2652      st_insert(tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED);
2653    }
2654
2655    mvfArray =  Ntm_NetworkBuildMvfs(network, tmpRoots, tmpLeaves,
2656                                      NIL(mdd_t));
2657    MVF = array_fetch(Mvf_Function_t *, mvfArray, 0);
2658    array_free(tmpRoots);
2659    st_free_table(tmpLeaves);
2660    array_free(mvfArray);
2661
2662    tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
2663    resultMdd = mdd_dup(tmpMdd);
2664    Mvf_FunctionFree(MVF);
2665  }
2666  else {
2667    MVF = Part_VertexReadFunction(partitionVertex);
2668    tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
2669    resultMdd = mdd_dup(tmpMdd);
2670  }
2671  if (Part_PartitionReadMethod(modelPartition) == Part_Frontier_c &&
2672      Ntk_NodeTestIsCombOutput(node)) {
2673    array_t     *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
2674    mdd_manager *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));
2675    array_t     *supportList;
2676    st_table    *supportTable = st_init_table(st_numcmp, st_numhash);
2677    int         i, j;
2678    int         existIntermediateVars;
2679    int         mddId;
2680    Mvf_Function_t      *mvf;
2681    vertex_t    *vertex;
2682    array_t     *varBddRelationArray, *varArray;
2683    mdd_t       *iv, *ivMdd, *relation;
2684
2685    for (i = 0; i < array_n(psVars); i++) {
2686      mddId = array_fetch(int, psVars, i);
2687      st_insert(supportTable, (char *)(long)mddId, NULL);
2688    }
2689
2690    existIntermediateVars = 1;
2691    while (existIntermediateVars) {
2692      existIntermediateVars = 0;
2693      supportList = mdd_get_support(mgr, resultMdd);
2694      for (i = 0; i < array_n(supportList); i++) {
2695        mddId = array_fetch(int, supportList, i);
2696        if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) {
2697          vertex = Part_PartitionFindVertexByMddId(modelPartition, mddId);
2698          mvf = Part_VertexReadFunction(vertex);
2699          varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mgr, mddId, mvf);
2700          varArray = mdd_id_to_bdd_array(mgr, mddId);
2701          assert(array_n(varBddRelationArray) == array_n(varArray));
2702          for (j = 0; j < array_n(varBddRelationArray); j++) {
2703            iv = array_fetch(mdd_t *, varArray, j);
2704            relation = array_fetch(mdd_t *, varBddRelationArray, j);
2705            ivMdd = bdd_cofactor(relation, iv);
2706            mdd_free(relation);
2707            tmpMdd = resultMdd;
2708            resultMdd = bdd_compose(resultMdd, iv, ivMdd);
2709            mdd_free(tmpMdd);
2710            mdd_free(iv);
2711            mdd_free(ivMdd);
2712          }
2713          array_free(varBddRelationArray);
2714          array_free(varArray);
2715          existIntermediateVars = 1;
2716        }
2717      }
2718      array_free(supportList);
2719    }
2720    st_free_table(supportTable);
2721  }
2722  return resultMdd;
2723}
2724
2725/**Function********************************************************************
2726
2727  Synopsis    [Read fairness constraints from file and check for errors.]
2728
2729  Description []
2730
2731  SideEffects []
2732
2733  SeeAlso     []
2734
2735******************************************************************************/
2736array_t *
2737BmcReadFairnessConstraints(
2738  FILE *fp /* pointer to the fairness constraint file */)
2739{
2740  array_t *constraintArray;     /* raw fairness constraints */
2741  array_t *ltlConstraintArray;  /* constraints converted to LTL */
2742
2743  if (fp == NIL(FILE) ) {
2744    /* Nothing to be done. */
2745    return NIL(array_t);
2746  }
2747
2748  /* Read constraints from file and check for errors. */
2749  constraintArray = Ctlsp_FileParseFormulaArray(fp);
2750  if (constraintArray == NIL(array_t)) {
2751    (void) fprintf(vis_stderr,
2752                   "** ctlsp error: error reading fairness constraints.\n");
2753    return NIL(array_t);
2754  }
2755  if (array_n(constraintArray) == 0) {
2756    (void) fprintf(vis_stderr, "** ctlsp error: fairness file is empty.\n");
2757    return NIL(array_t);
2758  }
2759  /*
2760   * Check that each constraint is an LTL formula.
2761   */
2762  ltlConstraintArray = Ctlsp_FormulaArrayConvertToLTL(constraintArray);
2763  Ctlsp_FormulaArrayFree(constraintArray);
2764  if (ltlConstraintArray == NIL(array_t)) {
2765    (void) fprintf(vis_stderr,
2766                   "** ctlsp error: fairness constraints are not LTL formulae.\n");
2767    return NIL(array_t);
2768  }
2769
2770  return ltlConstraintArray;
2771
2772} /* BmcReadFairnessConstraints */
2773
2774
2775/**Function********************************************************************
2776
2777  Synopsis [return the cnf index for a bdd node]
2778
2779  SideEffects []
2780
2781******************************************************************************/
2782int
2783BmcGetCnfVarIndexForBddNode(
2784  bdd_manager *bddManager,
2785  bdd_node *node,
2786  int      state,
2787  BmcCnfClauses_t *cnfClauses)
2788{
2789  array_t     *mvar_list  = mdd_ret_mvar_list(bddManager);
2790  array_t     *bvar_list  = mdd_ret_bvar_list(bddManager); 
2791 
2792  char      name[100];
2793  char      *nodeName;
2794  bvar_type bv;
2795  mvar_type mv;
2796  int nodeIndex = bdd_node_read_index(node);
2797  int index, rtnNodeIndex, rtnCode;
2798
2799
2800  /*
2801    If the node is for a multi-valued varaible.
2802  */
2803  if (nodeIndex < array_n(bvar_list)){
2804    bv = array_fetch(bvar_type, bvar_list, nodeIndex);
2805    /*
2806      get the multi-valued varaible.
2807    */
2808    mv = array_fetch(mvar_type, mvar_list, bv.mvar_id);
2809    arrayForEachItem(int, mv.bvars, index, rtnNodeIndex) {
2810      if (nodeIndex == rtnNodeIndex){
2811        break;
2812      }
2813    }
2814    assert(index < mv.encode_length);
2815    /*
2816      printf("Name of bdd node %s %d\n", mv.name, index);
2817    */
2818    sprintf(name, "%s_%d", mv.name, index);
2819  } else {
2820    sprintf(name, "Bdd_%d", nodeIndex);
2821  }
2822  nodeName = util_strsav(name);
2823  rtnCode = BmcCnfReadOrInsertNode(cnfClauses, nodeName, state, &nodeIndex);
2824  if(rtnCode == 1) {
2825    FREE(nodeName);
2826  }
2827  return nodeIndex;
2828}
2829
2830/*---------------------------------------------------------------------------*/
2831/* Definition of static functions                                            */
2832/*---------------------------------------------------------------------------*/
2833
2834/**Function********************************************************************
2835
2836  Synopsis [Test that the given string is an integer. Returns 0 if string is
2837  not an integer, 1 if the integer is too big for int, and 2 if integer fits
2838  in int.]
2839
2840  SideEffects [Sets the pointer value if the string is an integer small enough
2841  for int.]
2842
2843******************************************************************************/
2844static int
2845StringCheckIsInteger(
2846  char *string,
2847  int *value)
2848{
2849  char *ptr;
2850  long l;
2851 
2852  l = strtol (string, &ptr, 0) ;
2853  if(*ptr != '\0')
2854    return 0;
2855  if ((l > MAXINT) || (l < -1 - MAXINT))
2856    return 1 ;
2857  *value = (int) l;
2858  return 2 ;
2859}
2860
2861/**Function********************************************************************
2862
2863  Synopsis    [Compare procedure for name comparison.]
2864
2865  Description [Compare procedure for name comparison.]
2866
2867  SideEffects []
2868
2869******************************************************************************/
2870static int
2871nameCompare(
2872  const void * name1,
2873  const void * name2)
2874{
2875    return(strcmp(*(char**)name1, *(char **)name2));
2876
2877} /* end of signatureCompare */
2878
2879
2880
2881
2882/**Function********************************************************************
2883
2884  Synopsis    [Print the valuse of variables in the variable list "varNames".]
2885
2886  Description [For each variable in the variable list, this functions prints its
2887  value in the resultTable if it is different for its value in prevValue. If this
2888  variable is a symbolic variable, this function prints its symbolic value.]
2889
2890  SideEffects []
2891
2892******************************************************************************/
2893static void
2894printValue(
2895  mAig_Manager_t  *manager,
2896  Ntk_Network_t   *network,
2897  st_table        *nodeToMvfAigTable,
2898  BmcCnfClauses_t *cnfClauses,
2899  array_t         *varNames,
2900  st_table        *resultTable,
2901  int             state,
2902  int             *prevValue)
2903{
2904  Ntk_Node_t        *node;
2905  int               i, j;
2906  bAigEdge_t        bAigId;
2907  nameType_t        *varName, *nodeName;
2908  int               value, index;
2909  MvfAig_Function_t *MvfAig;
2910  int               changed = 0;
2911  int               tmp;
2912
2913  for (j=0; j< array_n(varNames); j++) {
2914    if (state == 0){
2915      prevValue[j] = -1;
2916    }
2917    nodeName = array_fetch(char *, varNames, j);
2918    /*
2919      Fetch the node corresponding to this node name.
2920    */
2921    node = Ntk_NetworkFindNodeByName(network, nodeName);
2922    /*
2923      Get the multi-valued function for each node
2924    */
2925    MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
2926    /*
2927      In case of the multi-valued function is not build for this node, do nothing.
2928      We may notify the user.
2929     */
2930    if (MvfAig ==  NIL(MvfAig_Function_t)){
2931      continue;
2932    }
2933    /*
2934      No CNF index for this variable at time "state in the "
2935     */
2936    value = -1;
2937    for (i=0; i< array_n(MvfAig); i++) {
2938      bAigId = MvfAig_FunctionReadComponent(MvfAig, i);
2939      /*
2940        constant value
2941       */
2942      if (bAigId == bAig_One){
2943        /*
2944          This variable equal the constant i.
2945         */
2946        value = i;
2947        break;
2948      }
2949      if (bAigId != bAig_Zero){
2950        char        *tmpStr;
2951       
2952        nodeName = bAig_NodeReadName(manager, bAigId);
2953        /*
2954          Build the variable name at state "state".
2955         */
2956        tmpStr = util_inttostr(state);
2957        varName  = util_strcat3(nodeName, "_", tmpStr);
2958        if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
2959          if (bAig_IsInverted(bAigId)){
2960            index = -index;
2961          }
2962          /*if (searchArray(result, index) > -1){*/
2963          if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){
2964            value = i;
2965            break;
2966          }
2967        } /* if st_lookup_int()  */
2968        FREE(tmpStr);
2969        FREE(varName);
2970      } /* if (bAigId != bAig_Zero) */
2971    }
2972    if (value >= 0){
2973      if (value != prevValue[j]){
2974        Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
2975
2976        prevValue[j] = value;
2977        changed = 1;
2978        if (Var_VariableTestIsSymbolic(nodeVar)) {
2979          char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
2980
2981          (void) fprintf(vis_stdout,"%s:%s\n",  Ntk_NodeReadName(node), symbolicValue);
2982        }
2983        else {
2984          (void) fprintf(vis_stdout,"%s:%d\n",  Ntk_NodeReadName(node), value);
2985        }
2986      }
2987    } else {
2988      /*
2989        This variable does not have value in the current time frame. It means its value
2990        is not important at this time frame.
2991       */
2992      (void) fprintf(vis_stdout,"%s:X\n",  Ntk_NodeReadName(node));
2993    }
2994  } /* for j loop */
2995  if (changed == 0){
2996    fprintf( vis_stdout, "<Unchanged>\n");
2997  }
2998
2999}/* end of printValue() */
3000
3001
3002
3003/**Function********************************************************************
3004
3005  Synopsis    [Print the valuse of variables in the variable list "varNames".]
3006
3007  Description [For each variable in the variable list, this functions prints the
3008               values of names, which do not start with $_ as these are true
3009               latches of the model. Since this is in aiger format, hence all
3010               the values are printed even if they didn't change from the
3011               previous values.]
3012
3013  SideEffects []
3014
3015******************************************************************************/
3016static void
3017printValueAiger(
3018  mAig_Manager_t  *manager,
3019  Ntk_Network_t   *network,
3020  st_table        *nodeToMvfAigTable,
3021  BmcCnfClauses_t *cnfClauses,
3022  array_t         *varNames,
3023  st_table        *resultTable,
3024  int             state,
3025  int             *prevValue)
3026{
3027  Ntk_Node_t        *node;
3028  int               i, j;
3029  bAigEdge_t        bAigId;
3030  nameType_t        *varName, *nodeName;
3031  int               value, index;
3032  MvfAig_Function_t *MvfAig;
3033  int               tmp;
3034  char *            NodeName;
3035
3036  for (j=0; j< array_n(varNames); j++) {
3037    if (state == 0){
3038      prevValue[j] = -1;
3039    }
3040    nodeName = array_fetch(char *, varNames, j);
3041    /*
3042      Fetch the node corresponding to this node name.
3043    */
3044    node = Ntk_NetworkFindNodeByName(network, nodeName);
3045    /*
3046      Get the multi-valued function for each node
3047    */
3048    MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
3049    /*
3050      In case of the multi-valued function is not build for this node, do nothing.
3051      We may notify the user.
3052     */
3053    if (MvfAig ==  NIL(MvfAig_Function_t)){
3054      continue;
3055    }
3056    /*
3057      No CNF index for this variable at time "state in the "
3058     */
3059    value = -1;
3060    for (i=0; i< array_n(MvfAig); i++) {
3061      bAigId = MvfAig_FunctionReadComponent(MvfAig, i);
3062      /*
3063        constant value
3064       */
3065      if (bAigId == bAig_One){
3066        /*
3067          This variable equal the constant i.
3068         */
3069        value = i;
3070        break;
3071      }
3072      if (bAigId != bAig_Zero){
3073        char        *tmpStr;
3074       
3075        nodeName = bAig_NodeReadName(manager, bAigId);
3076        /*
3077          Build the variable name at state "state".
3078         */
3079        tmpStr = util_inttostr(state);
3080        varName  = util_strcat3(nodeName, "_", tmpStr);
3081        if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
3082          if (bAig_IsInverted(bAigId)){
3083            index = -index;
3084          }
3085          /*if (searchArray(result, index) > -1){*/
3086          if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){
3087            value = i;
3088            break;
3089          }
3090        } /* if st_lookup_int()  */
3091        FREE(tmpStr);
3092        FREE(varName);
3093      } /* if (bAigId != bAig_Zero) */
3094    }
3095    NodeName = Ntk_NodeReadName(node); 
3096    if(!((NodeName[0] == '$') && (NodeName[1] == '_')))
3097    {
3098      if (value >= 0){
3099        Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
3100       
3101        prevValue[j] = value;
3102        if (Var_VariableTestIsSymbolic(nodeVar)) {
3103          char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
3104         
3105          (void) fprintf(vis_stdout,"%s",   symbolicValue);
3106        } 
3107        else {
3108          (void) fprintf(vis_stdout,"%d",  value);
3109        }
3110      } else {
3111      /*
3112        This variable does not have value in the current time frame. It means its value
3113        is not important at this time frame.
3114       */
3115        (void) fprintf(vis_stdout,"x" );
3116      }
3117    } /* these nodes are latches in front of inputs so they will be printed out as inputs */
3118  } /* for j loop */
3119}/* end of printValueAiger() */
3120
3121
3122/**Function********************************************************************
3123
3124  Synopsis    [Print the valuse of variables in the variable list "varNames".]
3125
3126  Description [For each variable in the variable list, this functions checks if
3127               the name starts with $_, which means that those latches are
3128               actually storing the value of inputs. This modification to the
3129               model is externally done and not done by VIS so this method is
3130               only specific to certain type of model, the output of aigtoblif
3131               translator.]
3132
3133  SideEffects []
3134
3135******************************************************************************/
3136static void
3137printValueAigerInputs(
3138  mAig_Manager_t  *manager,
3139  Ntk_Network_t   *network,
3140  st_table        *nodeToMvfAigTable,
3141  BmcCnfClauses_t *cnfClauses,
3142  array_t         *varNames,
3143  st_table        *resultTable,
3144  int             state,
3145  int             *prevValue)
3146{
3147  Ntk_Node_t        *node;
3148  int               i, j;
3149  bAigEdge_t        bAigId;
3150  nameType_t        *varName, *nodeName;
3151  int               value, index;
3152  MvfAig_Function_t *MvfAig;
3153  int               tmp;
3154  char *            NodeName;
3155
3156  for (j=0; j< array_n(varNames); j++) {
3157    if (state == 0){
3158      prevValue[j] = -1;
3159    }
3160    nodeName = array_fetch(char *, varNames, j);
3161    /*
3162      Fetch the node corresponding to this node name.
3163    */
3164    node = Ntk_NetworkFindNodeByName(network, nodeName);
3165    /*
3166      Get the multi-valued function for each node
3167    */
3168    MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
3169    /*
3170      In case of the multi-valued function is not build for this node, do nothing.
3171      We may notify the user.
3172     */
3173    if (MvfAig ==  NIL(MvfAig_Function_t)){
3174      continue;
3175    }
3176    /*
3177      No CNF index for this variable at time "state in the "
3178     */
3179    value = -1;
3180    for (i=0; i< array_n(MvfAig); i++) {
3181      bAigId = MvfAig_FunctionReadComponent(MvfAig, i);
3182      /*
3183        constant value
3184       */
3185      if (bAigId == bAig_One){
3186        /*
3187          This variable equal the constant i.
3188         */
3189        value = i;
3190        break;
3191      }
3192      if (bAigId != bAig_Zero){
3193        char        *tmpStr;
3194       
3195        nodeName = bAig_NodeReadName(manager, bAigId);
3196        /*
3197          Build the variable name at state "state".
3198         */
3199        tmpStr = util_inttostr(state);
3200        varName  = util_strcat3(nodeName, "_", tmpStr);
3201        if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
3202          if (bAig_IsInverted(bAigId)){
3203            index = -index;
3204          }
3205          /*if (searchArray(result, index) > -1){*/
3206          if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){
3207            value = i;
3208            break;
3209          }
3210        } /* if st_lookup_int()  */
3211        FREE(tmpStr);
3212        FREE(varName);
3213      } /* if (bAigId != bAig_Zero) */
3214    }
3215    NodeName = Ntk_NodeReadName(node); 
3216    if((NodeName[0] == '$') && (NodeName[1] == '_'))
3217    {
3218      if (value >= 0){
3219        Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
3220       
3221        prevValue[j] = value;
3222        if (Var_VariableTestIsSymbolic(nodeVar)) {
3223          char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
3224         
3225          (void) fprintf(vis_stdout,"%s",   symbolicValue);
3226        } 
3227        else {
3228          (void) fprintf(vis_stdout,"%d",  value);
3229        }
3230      } else {
3231      /*
3232        This variable does not have value in the current time frame. It means its value
3233        is not important at this time frame.
3234       */
3235        (void) fprintf(vis_stdout,"x" );
3236      }
3237    } /* these nodes are latches in front of inputs so they will be printed out as inputs */
3238  } /* for j loop */
3239}/* end of printValueAigerInputs() */
3240
3241
3242
Note: See TracBrowser for help on using the repository browser.