source: vis_dev/vis-2.3/src/eqv/eqvVerify.c @ 93

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

vis2.3

File size: 23.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [eqvVerify.c]
4
5  PackageName [eqv]
6
7  Synopsis    [This file contains the two routines which do combinational and
8  sequential verification.]
9
10  Description []
11
12  SeeAlso     []
13
14  Author      [Shaz Qadeer]
15
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35******************************************************************************/
36
37#include "eqvInt.h"
38
39static char rcsid[] UNUSED = "$Id: eqvVerify.c,v 1.10 2009/04/11 01:40:06 fabio Exp $";
40
41/**AutomaticStart*************************************************************/
42
43/*---------------------------------------------------------------------------*/
44/* Static function prototypes                                                */
45/*---------------------------------------------------------------------------*/
46
47
48/**AutomaticEnd***************************************************************/
49
50
51/*---------------------------------------------------------------------------*/
52/* Definition of exported functions                                          */
53/*---------------------------------------------------------------------------*/
54
55/**Function********************************************************************
56
57  Synopsis    [This function does combinational verification between network1
58  and network2.]
59
60  Description [roootsMap and leavesMap contain corresponding nodes in network1
61  and network2. It is assumed that the set of leaf nodes forms a complete
62  support of the set of root nodes in both the networks. This function
63  verifies the combinational equivalence of corresponding roots in terms of
64  the leaves. method1 and method2 specify the partition methods to be used for
65  partitioning network1 and network2 respectively. AssignCommonOrder is a
66  pointer to a function which takes two networks, whose mdd managers are
67  identical, and a hash table containing corresponding leaf nodes whose mdd Id
68  should be the same. AssignCommonOrder() orders the two networks ensuring
69  that identical mddIds are assigned to the corresponding leaf nodes in the
70  hash table. This function has to be supplied by the user.
71
72  This function returns TRUE if all the root pairs are combinationally
73  equivalent otherwise it returns FALSE. It is assumed that network1 already
74  has a mdd manager. If a partition is registered with network1, and it has
75  vertices corresponding to the specified roots and leaves it is used
76  otherwise a new partition is created. A new partition is always created for
77  network2.]
78
79  SideEffects []
80
81******************************************************************************/
82boolean
83Eqv_NetworkVerifyCombinationalEquivalence(
84  Ntk_Network_t *network1,
85  Ntk_Network_t *network2,
86  st_table *leavesMap,  /* the mapping between the inputs of the networks;
87                         * hash table from Ntk_Node_t * to Ntk_Node_t * */
88  st_table *rootsMap,   /* the mapping between the outputs of the networks;
89                         * hash table from Ntk_Node_t * to Ntk_Node_t * */
90  OFT AssignCommonOrder,
91  Part_PartitionMethod method1,
92  Part_PartitionMethod method2)
93{
94  mdd_manager *mddMgr;
95  lsList leavesList1, leavesList2;
96  lsList rootsList1, rootsList2;
97  st_table *leaves1, *leaves2;
98  array_t *roots1, *roots2;
99  st_generator *gen;
100  lsGen listGen;
101  graph_t *rootsToLeaves1, *rootsToLeaves2;
102  Ntk_Node_t *node1, *node2;
103  char *name1, *name2, *name;
104  Mvf_Function_t *func1, *func2;
105  int num, i, j;
106  array_t *mvfRoots1, *mvfRoots2;
107  boolean equivalent = TRUE;
108  lsList dummy = (lsList) 0;
109  int mddId1, mddId2;
110  vertex_t *vertex;
111  lsGeneric data;
112  boolean partValid = FALSE;
113  mdd_manager *mgr;
114  int mddId;
115  array_t *mddIdArray;
116  mdd_t *aMinterm, *diff;
117  char *mintermName;
118  mdd_t *comp1, *comp2;
119  int numComponents;
120
121  /* First check whether a partition is registered with network1 */
122  if(Ntk_NetworkReadApplInfo(network1, PART_NETWORK_APPL_KEY) != NIL(void)) {
123    /*
124     * Check whether the registered partition can be used to compute the roots
125     * in terms of the leaves. If it can be used, then i won't create a new
126     * one.
127     */
128    partValid = TestPartitionIsValid(network1, rootsMap, leavesMap);
129    /*
130     * If a partition already exists, an mddManager also exists.
131     * So, don't allocate a new one.
132     */
133    mddMgr = Ntk_NetworkReadMddManager(network1);
134  }
135  else {
136    mddMgr = Ntk_NetworkInitializeMddManager(network1);
137  }
138  assert(mddMgr != NIL(mdd_manager));
139  Ntk_NetworkSetMddManager(network2, mddMgr);
140  (*AssignCommonOrder)(network1, network2, leavesMap);
141
142  /* Create lists of leaves and roots for creating partitions. */
143  leavesList1 = lsCreate();
144  leavesList2 = lsCreate();
145  st_foreach_item(leavesMap, gen, &node1, &node2) {
146    mddId1 = Ntk_NodeReadMddId(node1);
147    mddId2 = Ntk_NodeReadMddId(node2);
148    assert(mddId1 == mddId2);
149    lsNewEnd(leavesList1, (lsGeneric) node1, LS_NH);
150    lsNewEnd(leavesList2, (lsGeneric) node2, LS_NH);
151  }
152
153  rootsList1 = lsCreate();
154  rootsList2 = lsCreate();
155  st_foreach_item(rootsMap, gen, &node1, &node2) {
156    lsNewEnd(rootsList1, (lsGeneric) node1, LS_NH);
157    lsNewEnd(rootsList2, (lsGeneric) node2, LS_NH);
158  }
159
160  if(partValid) {
161    rootsToLeaves1 = Part_NetworkReadPartition(network1);
162  }
163  else {
164    rootsToLeaves1 = Part_NetworkCreatePartition(network1, NIL(Hrc_Node_t),
165                                                 "dummy", rootsList1,
166                                                 leavesList1, NIL(mdd_t),
167                                                 method1, dummy,
168                                                 FALSE, FALSE, TRUE);
169  }
170
171  /*
172   * Generate arrays of root and leaf vertices in the first partition
173   * to pass as arguments to Part_PartitionCollapse().
174   */
175  roots1 = array_alloc(vertex_t *, 0);
176  lsForEachItem(rootsList1, listGen, data) {
177    name = Ntk_NodeReadName((Ntk_Node_t *) data);
178    vertex = Part_PartitionFindVertexByName(rootsToLeaves1, name);
179    assert(vertex != NIL(vertex_t));
180    array_insert_last(vertex_t *, roots1, vertex);
181  }
182  leaves1 = st_init_table(st_ptrcmp, st_ptrhash);
183  lsForEachItem(leavesList1, listGen, data) {
184    name = Ntk_NodeReadName((Ntk_Node_t *) data);
185    vertex = Part_PartitionFindVertexByName(rootsToLeaves1, name);
186/*    assert(vertex != NIL(vertex_t)); */
187    if(vertex != NIL(vertex_t)) {
188      /*
189       * If a leaf is not actually in the support of the roots then
190       * it will not be present in the partition.
191       */
192      mddId = Part_VertexReadMddId(vertex);
193      st_insert(leaves1, (char *) vertex, (char *) (long) mddId);
194    }
195  }
196
197  lsDestroy(rootsList1, (void (*) (lsGeneric)) 0);
198  lsDestroy(leavesList1, (void (*) (lsGeneric)) 0);
199  rootsToLeaves2 = Part_NetworkCreatePartition(network2, NIL(Hrc_Node_t),
200                                               "dummy", rootsList2,
201                                               leavesList2, NIL(mdd_t),
202                                               method2, dummy, FALSE,
203                                               FALSE, TRUE);
204
205  /*
206   * Generate arrays of root and leaf vertices in the second partition
207   * to pass as arguments to Part_PartitionCollapse().
208   */
209  roots2 = array_alloc(vertex_t *, 0);
210  lsForEachItem(rootsList2, listGen, data) {
211    name = Ntk_NodeReadName((Ntk_Node_t *) data);
212    vertex = Part_PartitionFindVertexByName(rootsToLeaves2, name);
213    assert(vertex != NIL(vertex_t));
214    array_insert_last(vertex_t *, roots2, vertex);
215  }
216  leaves2 = st_init_table(st_ptrcmp, st_ptrhash);
217  lsForEachItem(leavesList2, listGen, data) {
218    name = Ntk_NodeReadName((Ntk_Node_t *) data);
219    vertex = Part_PartitionFindVertexByName(rootsToLeaves2, name);
220/*    assert(vertex != NIL(vertex_t)); */
221    if(vertex != NIL(vertex_t)) {
222      /*
223       * If a leaf is not actually in the support of the roots then
224       * it will not be present in the partition.
225       */
226      mddId = Part_VertexReadMddId(vertex);
227      st_insert(leaves2, (char *) vertex, (char *) (long) mddId);
228    }
229  }
230  lsDestroy(rootsList2, (void (*) (lsGeneric)) 0);
231  lsDestroy(leavesList2, (void (*) (lsGeneric)) 0);
232  assert(Part_PartitionReadMddManager(rootsToLeaves1) ==
233         Part_PartitionReadMddManager(rootsToLeaves2));
234
235  mvfRoots1 = Part_PartitionCollapse(rootsToLeaves1, roots1, leaves1, NIL(mdd_t));
236  mvfRoots2 = Part_PartitionCollapse(rootsToLeaves2, roots2, leaves2, NIL(mdd_t));
237
238  assert(array_n(mvfRoots1) == array_n(mvfRoots2));
239  num = array_n(mvfRoots1);
240  mddIdArray = array_alloc(int, 0);
241  st_foreach_item_int(leaves1, gen, &vertex, &mddId) {
242    array_insert_last(int, mddIdArray, mddId);
243  }
244
245  /*
246   * For each pair of corresponding outputs in the two arrays mvfRoots1 and
247   * mvfRoots2, I will compute the mdd representing all the input combinations
248   * for which they are different. For each pair, I will print one input
249   * combination for which they are different.
250   */
251
252  for(i = 0; i<num; ++i) {
253    func1 = array_fetch(Mvf_Function_t *, mvfRoots1, i);
254    func2 = array_fetch(Mvf_Function_t *, mvfRoots2, i);
255    if(!Mvf_FunctionTestIsEqualToFunction(func1, func2)) {
256      mgr = Mvf_FunctionReadMddManager(func1);
257      assert(mgr == Mvf_FunctionReadMddManager(func2));
258      numComponents = Mvf_FunctionReadNumComponents(func1);
259      for(j=0; j<numComponents; ++j) {
260        comp1 = Mvf_FunctionReadComponent(func1, j);
261        comp2 = Mvf_FunctionReadComponent(func2, j);
262        diff = mdd_xor(comp1, comp2);
263        if(!mdd_is_tautology(diff, 0)) {
264          aMinterm = Mc_ComputeAMinterm(diff, mddIdArray, mddMgr);
265          mintermName = Mc_MintermToString(aMinterm, mddIdArray, network1);
266          vertex = array_fetch(vertex_t *, roots1, i);
267          name1 = Part_VertexReadName(vertex);
268          vertex = array_fetch(vertex_t *, roots2, i);
269          name2 = Part_VertexReadName(vertex);
270          (void) fprintf(vis_stdout, "%s from network1 and %s from network2 differ on input values\n%s",
271                         name1, name2, mintermName);
272          FREE(mintermName);
273          mdd_free(aMinterm);
274          mdd_free(diff);
275          break;
276        }
277        mdd_free(diff);
278      }
279      equivalent = FALSE;
280    }
281  }
282  array_free(mddIdArray);
283  if(!partValid) {
284    Part_PartitionFree(rootsToLeaves1);
285  }
286  Part_PartitionFree(rootsToLeaves2);
287  array_free(roots1);
288  array_free(roots2);
289  st_free_table(leaves1);
290  st_free_table(leaves2);
291  arrayForEachItem(Mvf_Function_t *, mvfRoots1, i, func1) {
292    Mvf_FunctionFree(func1);
293  }
294  array_free(mvfRoots1);
295  arrayForEachItem(Mvf_Function_t *, mvfRoots2, i, func2) {
296    Mvf_FunctionFree(func2);
297  }
298  array_free(mvfRoots2);
299  Ntk_NetworkSetMddManager(network2, NIL(mdd_manager));
300  /*
301   * This is needed because Ntk_NetworkFree() will be called on both network1
302   * and network2.
303   */
304  return equivalent;
305}
306
307/**Function********************************************************************
308
309  Synopsis    [This function does sequential verification between network1 and
310  network2.]
311
312  Description [It accepts as input the two networks, and two hash tables of
313  node names - rootsTable and leavesTable. leavesTable gives the names of
314  corresponding primary inputs in the two networks. If leavesTable is NULL,
315  the inputs are simply matched by names. rootsTable gives the names of
316  corresponding nodes in the two networks whose sequential equivalence has to
317  be verified. If rootsTable is NULL, it is assumed that all the
318  primary outputs need to be verified and that they are to be associated by
319  names. The function returns TRUE if the all the corresponding nodes are
320  sequentially equivalent otherwise it returns FALSE. The verification is done
321  by appending network1 to network2, thereby forming the product machine. A
322  set of states in which the corresponding outputs to be verified are
323  different for some input is calculated and it is checked whether any of
324  these states is reachable from an initial state of the product machine.]
325
326  SideEffects [network2 is modified in this function.]
327
328******************************************************************************/
329boolean
330Eqv_NetworkVerifySequentialEquivalence(
331  Ntk_Network_t *network1,
332  Ntk_Network_t *network2,
333  st_table *rootsTable,    /* the mapping between the outputs of the networks;
334                            * hash table from char * to char * */
335  st_table *leavesTable,   /* the mapping between the inputs of the networks;
336                            * hash table from char * to char * */
337  Part_PartitionMethod partMethod,
338  boolean useBackwardReach,
339  boolean reordering)
340{
341  array_t *roots;
342  st_table *leaves;
343  lsList rootsList;
344  lsList rootsPartList = (lsList) 0;
345  st_table *outputMap = NIL(st_table);
346  Ntk_Node_t *node1, *node2, *node;
347  char *name1, *name2, *temp;
348  st_generator *gen;
349  lsGen listGen;
350  graph_t *partition;
351  vertex_t *vertex;
352  mdd_manager *mddMgr;
353  array_t *mvfArray;
354  Mvf_Function_t *mvf1, *mvf2;
355  mdd_t *badStates, *initialStates;
356  mdd_t *mddTemp, *mdd1, *mdd2, *tautology;
357  mdd_t *mddComp1, *mddComp2;
358  int n, i, j, numComponents;
359  int id;
360  array_t *inputIdArray;
361  lsList dummy = (lsList) 0;
362  lsGeneric data;
363  Ntk_Node_t *input;
364  Fsm_Fsm_t *modelFsm;
365  array_t *onionRings;
366  array_t *aPath;
367  boolean inequivalent;
368  boolean rootsFlag = (rootsTable == NIL(st_table)) ? FALSE : TRUE;
369  array_t *careStatesArray = array_alloc(mdd_t *, 0);
370
371  /* If rootsFlag is FALSE, all primary outputs are to be verified */
372  if(rootsFlag == FALSE) {
373    outputMap = MapPrimaryOutputsByName(network1, network2);
374  }
375
376  /*
377   * If leavesFlag is FALSE, the primary inputs in the two networks are
378   * assumed to have same names. In the network returned by
379   * Ntk_NetworkAppendNetwork(), the two corresponding nodes will be merged.
380   * If leavesFlag is TRUE, the name correspondence between the primary inputs
381   * in the two networks is specified in leavesTable.
382   */
383  if(leavesTable == NIL(st_table)) {
384    st_table *emptyTable = st_init_table(strcmp, st_strhash);
385    Ntk_NetworkAppendNetwork(network2, network1, emptyTable);
386    st_free_table(emptyTable);
387  }
388  else {
389    Ntk_NetworkAppendNetwork(network2, network1, leavesTable);
390  }
391
392  /*
393   * network1 has been appended to the erstwhile network2, and the new network
394   * is now called network2.
395   */
396
397  mddMgr = Ntk_NetworkInitializeMddManager(network2);
398
399  Ord_NetworkOrderVariables(network2, Ord_RootsByDefault_c,
400                            Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c,
401                            Ord_Unassigned_c, dummy, FALSE);
402
403  if (reordering)
404    Ntk_NetworkSetDynamicVarOrderingMethod(network2, BDD_REORDER_SIFT,
405                                           BDD_REORDER_VERBOSITY);
406  /*
407   * Ntk_NetworkAppendNetwork() adds $NTK2 to the names of all the
408   * appended nodes. I want to find the appended nodes in new network2
409   * corresponding to the roots in network1. I will add all these nodes to
410   * rootsList. I will also add all the roots of the erstwhile network2, which
411   * exist in the network2 also. rootsList will finally contain all the nodes
412   * in network2 whose mdds have to be created by Part_Partition Collapse().
413   */
414
415  rootsList = lsCreate();
416  if(rootsFlag == FALSE) {
417    st_foreach_item(outputMap, gen, &node1, &node2) {
418      name1 = Ntk_NodeReadName(node1);
419      temp = util_strcat3(name1, "$NTK2", "");
420      name1 = temp;
421      node1 = Ntk_NetworkFindNodeByName(network2, name1);
422      assert(node1 != NIL(Ntk_Node_t));
423      FREE(name1);
424      lsNewEnd(rootsList, (lsGeneric) node1, LS_NH);
425      lsNewEnd(rootsList, (lsGeneric) node2, LS_NH);
426    }
427  }
428  else {
429    st_foreach_item(rootsTable, gen, &name1, &name2) {
430      /* I am finding the node in the new network2 */
431      temp = util_strcat3(name1, "$NTK2", "");
432      name1 = temp;
433      node1 = Ntk_NetworkFindNodeByName(network2, name1);
434      FREE(name1);
435      lsNewEnd(rootsList, (lsGeneric) node1, LS_NH);
436      node2 = Ntk_NetworkFindNodeByName(network2, name2);
437      lsNewEnd(rootsList, (lsGeneric) node2, LS_NH);
438    }
439  }
440  if(outputMap) {
441    st_free_table(outputMap);
442  }
443  /* rootsPartList is the list of nodes which will passed to
444   * Part_NetworkCreatePartition(). I want all the next state functions i.e.
445   * latch data inputs as well as everything in rootsList to be in
446   * rootsPartList. If rootsFlag is FALSE, rootsPartList is simply passed as
447   * (lsList) 0.
448   */
449  if(rootsFlag) {
450    rootsPartList = lsCreate();
451    Ntk_NetworkForEachCombOutput(network2, listGen, node) {
452      if(Ntk_NodeTestIsLatchDataInput(node) ||
453         Ntk_NodeTestIsLatchInitialInput(node)){
454        lsNewEnd(rootsPartList, (lsGeneric) node, LS_NH);
455      }
456    }
457    lsForEachItem(rootsList, listGen, node) {
458      if(!Ntk_NodeTestIsLatchDataInput(node) &&
459         !Ntk_NodeTestIsLatchInitialInput(node)) {
460        lsNewEnd(rootsPartList, (lsGeneric) node, LS_NH);
461      }
462    }
463  }
464  partition = Part_NetworkCreatePartition(network2, NIL(Hrc_Node_t), "dummy",
465                                          rootsPartList,
466                                          (lsList) 0, NIL(mdd_t), partMethod,
467                                          dummy, FALSE, FALSE, TRUE);
468
469  Ntk_NetworkAddApplInfo(network2, PART_NETWORK_APPL_KEY,
470                         (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
471                         (void *) partition);
472  if(rootsPartList) {
473    lsDestroy(rootsPartList, (void (*) (lsGeneric)) 0);
474  }
475  /* Create roots and leaves for Part_PartitionCollapse().
476   */
477  roots = array_alloc(vertex_t *, 0);
478  lsForEachItem(rootsList, listGen, data) {
479    name1 = Ntk_NodeReadName((Ntk_Node_t *) data);
480    vertex = Part_PartitionFindVertexByName(partition, name1);
481    assert(vertex != NIL(vertex_t));
482    array_insert_last(vertex_t *, roots, vertex);
483  }
484  lsDestroy(rootsList, (void (*) (lsGeneric)) 0);
485  leaves = st_init_table(st_ptrcmp, st_ptrhash);
486  Ntk_NetworkForEachCombInput(network2, listGen, node1) {
487    name1 = Ntk_NodeReadName(node1);
488    vertex = Part_PartitionFindVertexByName(partition, name1);
489    if(vertex != NIL(vertex_t)) {
490      /* A combinational input might not be present in the support of any
491         node in rootsPartList. If so, it will not be present in the partition
492         also. */
493      st_insert(leaves, (char *) vertex, (char *) (long) 0);
494    }
495  }
496  mvfArray = Part_PartitionCollapse(partition, roots, leaves, NIL(mdd_t));
497  array_free(roots);
498  st_free_table(leaves);
499  n = array_n(mvfArray);
500  assert(n%2 == 0);
501  n = n/2;
502  assert(mddMgr != NULL);
503
504/* In mvfArray, the mvfs of corresponding nodes occur one after the other,
505   * because of the way rootsList was created. badStates will ultimately
506   * contain all the states for which  any pair of corresponding nodes differ
507   * for some input.
508   */
509  badStates = mdd_zero(mddMgr);
510  for(i=0; i<n; i++) {
511    mvf1 = array_fetch(Mvf_Function_t *, mvfArray, 2*i);
512    mvf2 = array_fetch(Mvf_Function_t *, mvfArray, 2*i +1);
513    numComponents = Mvf_FunctionReadNumComponents(mvf1);
514    mdd2 = mdd_zero(mddMgr);
515    /*
516     * Hopefully, mddMgr of the partition is the same as the mddMgr of the
517     * MVFs.
518     */
519    for(j=0; j<numComponents; j++) {
520      mddComp1 = Mvf_FunctionObtainComponent(mvf1, j);
521      mddComp2 = Mvf_FunctionObtainComponent(mvf2, j);
522      mdd1 = mdd_and(mddComp1, mddComp2, 1, 1);
523      mdd_free(mddComp1);
524      mdd_free(mddComp2);
525      mddTemp = mdd_or(mdd2, mdd1, 1, 1);
526      mdd_free(mdd1);
527      mdd_free(mdd2);
528      mdd2 = mddTemp;
529    }
530
531   /*
532    * At this point, mdd2 represents the set of input and present state
533    * combinations in which mvf1 and mvf2 produce the same value. I want the
534    * set for which mvf1 and mvf2 are different.
535    */
536    mddTemp = mdd_or(badStates, mdd2, 1, 0);
537    mdd_free(mdd2);
538    mdd_free(badStates);
539    badStates = mddTemp;
540  }
541  arrayForEachItem(Mvf_Function_t *, mvfArray, i, mvf1) {
542    Mvf_FunctionFree(mvf1);
543  }
544  array_free(mvfArray);
545  /* existentially quantify out the input variables */
546  inputIdArray = array_alloc(int, 0);
547
548  Ntk_NetworkForEachPrimaryInput(network2, listGen, input) {
549    id = Ntk_NodeReadMddId(input);
550    assert(id >= 0);
551    array_insert_last(int, inputIdArray, id);
552  }
553
554  mddTemp = mdd_smooth(mddMgr, badStates, inputIdArray);
555  mdd_free(badStates);
556  badStates = mddTemp;
557  array_free(inputIdArray);
558  modelFsm = Fsm_FsmCreateFromNetworkWithPartition(network2, NIL(graph_t));
559  assert(modelFsm != NIL(Fsm_Fsm_t));
560  Ntk_NetworkAddApplInfo(network2, FSM_NETWORK_APPL_KEY,
561                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
562                         (void *) modelFsm);
563
564  onionRings = array_alloc(mdd_t *, 0);
565  initialStates = Fsm_FsmComputeInitialStates(modelFsm);
566  tautology = mdd_one(mddMgr);
567
568  /* Model checking function */
569  if (useBackwardReach == TRUE) {
570    array_insert(mdd_t *, careStatesArray, 0, tautology);
571    inequivalent = Mc_FsmComputeStatesReachingToSet(modelFsm, badStates,
572                        careStatesArray, initialStates,
573                        onionRings, McVerbosityNone_c, McDcLevelNone_c);
574    array_free(careStatesArray);
575    mdd_free(badStates);
576    mdd_free(tautology);
577
578    if (inequivalent) {
579      mdd_t *outerOnionRing = array_fetch_last(mdd_t *, onionRings);
580      mdd_t *badInitialStates = mdd_and(initialStates, outerOnionRing, 1, 1);
581      array_t *psVarMddIdArray = Fsm_FsmReadPresentStateVars(modelFsm);
582      mdd_t *aBadInitialState = Mc_ComputeAMinterm(initialStates, psVarMddIdArray, mddMgr);
583      mdd_free(badInitialStates);
584      aPath = Mc_BuildPathToCore(aBadInitialState, onionRings, modelFsm,
585                                 McGreaterOrEqualZero_c);
586      (void) Mc_PrintPath(aPath, modelFsm, TRUE); /* TRUE -> print inputs on path */
587      mdd_free(aBadInitialState);
588      mdd_free(initialStates);
589      mdd_array_free(aPath);
590      mdd_array_free(onionRings);
591      return FALSE;
592    }
593    else {
594      mdd_free(initialStates);
595      return TRUE;
596    }
597  }
598  else { /* do forward search */
599    array_insert(mdd_t *, careStatesArray, 0, tautology);
600    inequivalent = Mc_FsmComputeStatesReachableFromSet(modelFsm, initialStates,
601                        careStatesArray, badStates, onionRings,
602                        McVerbosityNone_c, McDcLevelNone_c);
603    array_free(careStatesArray);
604    mdd_free(tautology);
605    mdd_free(initialStates);
606
607    if (inequivalent) {
608      mdd_t *outerOnionRing = array_fetch_last(mdd_t *, onionRings);
609      mdd_t *reachableBadStates = mdd_and(badStates, outerOnionRing, 1, 1);
610      array_t *psVarMddIdArray = Fsm_FsmReadPresentStateVars(modelFsm);
611      mdd_t *aBadReachableState = Mc_ComputeAMinterm(reachableBadStates, psVarMddIdArray, mddMgr);
612      mdd_free(reachableBadStates);
613      psVarMddIdArray = Fsm_FsmReadPresentStateVars(modelFsm);
614      aPath = Mc_BuildPathFromCore(aBadReachableState, onionRings, modelFsm,
615                                 McGreaterOrEqualZero_c);
616      (void) Mc_PrintPath(aPath, modelFsm, TRUE); /* TRUE -> print inputs on path */
617      mdd_free(aBadReachableState);
618      mdd_free(badStates);
619      mdd_array_free(aPath);
620      mdd_array_free(onionRings);
621      return FALSE;
622    }
623    else {
624      mdd_free(badStates);
625      return TRUE;
626    }
627  }
628}
629
630/*---------------------------------------------------------------------------*/
631/* Definition of internal functions                                          */
632/*---------------------------------------------------------------------------*/
633
634
635/*---------------------------------------------------------------------------*/
636/* Definition of static functions                                            */
637/*---------------------------------------------------------------------------*/
Note: See TracBrowser for help on using the repository browser.