source: vis_dev/vis-2.3/src/grab/grabUtil.c @ 101

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

vis2.3
File size: 38.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [grabUtil.c]
4
5  PackageName [grab]
6
7  Synopsis    [The utility functions for abstraction refinement.]
8
9  Description [This file contains the functions to check invariant
10  properties by the GRAB abstraction refinement algorithm. GRAB stands
11  for "Generational Refinement of Ariadne's Bundle," in which the
12  automatic refinement is guided by all shortest abstract
13  counter-examples. For more information, please check the ICCAD'03
14  paper of Wang et al., "Improving Ariadne's Bundle by Following
15  Multiple Counter-Examples in Abstraction Refinement." ]
16 
17  Author      [Chao Wang]
18
19  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
20  All rights reserved.
21
22  Permission is hereby granted, without written agreement and without
23  license or royalty fees, to use, copy, modify, and distribute this
24  software and its documentation for any purpose, provided that the
25  above copyright notice and the following two paragraphs appear in
26  all copies of this software.]
27
28******************************************************************************/
29
30#include "grabInt.h"
31
32/*---------------------------------------------------------------------------*/
33/* Constant declarations                                                     */
34/*---------------------------------------------------------------------------*/
35
36/*---------------------------------------------------------------------------*/
37/* Structure declarations                                                    */
38/*---------------------------------------------------------------------------*/
39
40/*---------------------------------------------------------------------------*/
41/* Type declarations                                                         */
42/*---------------------------------------------------------------------------*/
43
44/*---------------------------------------------------------------------------*/
45/* Variable declarations                                                     */
46/*---------------------------------------------------------------------------*/
47
48/*---------------------------------------------------------------------------*/
49/* Macro declarations                                                        */
50/*---------------------------------------------------------------------------*/
51
52/**AutomaticStart*************************************************************/
53
54/*---------------------------------------------------------------------------*/
55/* Static function prototypes                                                */
56/*---------------------------------------------------------------------------*/
57
58static void GetFormulaNodes(Ntk_Network_t *network, Ctlp_Formula_t *F, array_t *formulaNodes);
59static void GetFaninLatches(Ntk_Node_t *node, st_table *visited, st_table *absVarTable);
60static void NodeTableAddCtlFormulaNodes(Ntk_Network_t *network, Ctlp_Formula_t *formula, st_table * nodesTable);
61
62/**AutomaticEnd***************************************************************/
63
64/*---------------------------------------------------------------------------*/
65/* Definition of internal functions                                          */
66/*---------------------------------------------------------------------------*/
67
68/**Function********************************************************************
69
70  Synopsis    [Compute the Cone-Of-Influence abstract model.]
71
72  Description [Compute the Cone-Of-Influence abstraction, which
73  consists of latches in the transitive supprot of the property.]
74
75  SideEffects []
76
77******************************************************************************/
78st_table *
79GrabComputeCOIAbstraction(
80  Ntk_Network_t *network,
81  Ctlp_Formula_t *invFormula)
82{
83  st_table     *formulaNodes;
84  array_t      *formulaCombNodes;
85  Ntk_Node_t   *node;
86  array_t      *nodeArray;
87  int          i;
88  st_generator *stGen;
89  st_table *absVarTable;
90
91  /* find network nodes in the immediate support of the property */
92  formulaNodes = st_init_table(st_ptrcmp, st_ptrhash);
93  NodeTableAddCtlFormulaNodes(network, invFormula, formulaNodes);
94
95  /* find network nodes in the transitive fan-in */
96  nodeArray = array_alloc(Ntk_Node_t *, 0);
97  st_foreach_item(formulaNodes, stGen,  & node, NIL(char *)) {
98    array_insert_last( Ntk_Node_t *, nodeArray, node);
99  }
100  st_free_table(formulaNodes);
101  formulaCombNodes = Ntk_NodeComputeTransitiveFaninNodes(network, nodeArray,
102                                                         FALSE, TRUE);
103  array_free(nodeArray);
104
105  /* extract all the latches */
106  absVarTable = st_init_table(st_ptrcmp, st_ptrhash);
107  arrayForEachItem(Ntk_Node_t *, formulaCombNodes, i, node) {
108    if (Ntk_NodeTestIsLatch(node) == TRUE) {
109      st_insert(absVarTable, node, (char *)0);
110    }
111  }
112  array_free(formulaCombNodes);
113 
114  return absVarTable;
115}
116
117/**Function********************************************************************
118
119  Synopsis    [Compute the initial abstract model.]
120
121  Description [Compute the he initial abstraction, which consists of
122  latches in the immediate supprot of the property.]
123
124  SideEffects []
125
126******************************************************************************/
127st_table *
128GrabComputeInitialAbstraction(
129  Ntk_Network_t *network, 
130  Ctlp_Formula_t *invFormula)
131{
132  array_t    *formulaNodes = array_alloc(Ntk_Node_t *, 0);
133  Ntk_Node_t *node;
134  int        i;
135  st_table   *absVarTable, *visited;
136
137  GetFormulaNodes(network, invFormula, formulaNodes);
138
139  absVarTable = st_init_table(st_ptrcmp, st_ptrhash);
140  visited = st_init_table(st_ptrcmp, st_ptrhash);
141  arrayForEachItem(Ntk_Node_t *, formulaNodes, i, node) {
142    GetFaninLatches(node, visited, absVarTable);
143  }
144
145  st_free_table(visited);
146  array_free(formulaNodes);
147 
148  return absVarTable;
149}
150
151/**Function********************************************************************
152
153  Synopsis    [Build or update partition for the current abstract model.]
154
155  Description [Build or update partition for the current abstract
156  model. It is a two-phase process, in which the first phase generated
157  the Bnvs---intermediate variables that should be created; while the
158  second phase actually create the BDDs.
159
160  When a non-empty hash table 'absBnvTable' is given, BNVs not in this
161  table should be treated as inputs---they should not appear in the
162  partition either.
163
164  When 'absBnvTable' is not provided (e.g. when fine-grain abstraction
165  is disabled), all relevant BNVs should appear in the partition.]
166
167  SideEffects []
168
169******************************************************************************/
170void
171GrabUpdateAbstractPartition(
172  Ntk_Network_t *network,
173  st_table *coiBnvTable,
174  st_table *absVarTable,
175  st_table *absBnvTable,
176  int partitionFlag)
177{
178  graph_t *newPart;
179  st_table *useAbsBnvTable = absBnvTable? absBnvTable:coiBnvTable;
180 
181  if (partitionFlag == GRAB_PARTITION_BUILD) {
182
183    /* free the existing partition */
184    Ntk_NetworkFreeApplInfo(network, PART_NETWORK_APPL_KEY);
185
186    /* insert bnvs whenever necessary. Note that when the current
187     * partition is not available, this function will create new bnvs
188     * and put them into the coiBnvTable. Otherwise, it retrieves
189     * existing bnvs from the current partiton */
190    Part_PartitionReadOrCreateBnvs(network, absVarTable, coiBnvTable);
191
192    /* create the new partition */
193    newPart = g_alloc();
194    newPart->user_data = (gGeneric)PartPartitionInfoCreate("default",
195                                        Ntk_NetworkReadMddManager(network),
196                                                           Part_Frontier_c);
197    Part_PartitionWithExistingBnvs(network, newPart, coiBnvTable, 
198                                   absVarTable, useAbsBnvTable);
199    Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY,
200                           (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
201                           (void *) newPart);
202
203  }else if (partitionFlag == GRAB_PARTITION_UPDATE) {
204    fprintf(vis_stdout, 
205            "\n ** grab error: GRAB_PARTITION_UPDATE not implemented\n");
206    assert(0);
207  }
208
209}
210
211/**Function********************************************************************
212
213  Synopsis    [Create the abstract FSM.]
214
215  Description [Create the abstract FSM. Table 'coiBnvTable' contains
216  all the BNVs (i.e. intermediate variables), while Table
217  'absBnvTable' contains all the visible BNVs. BNVs not in absBnvTable
218  should be treated as inputs.
219
220  When absBnvTable is NULL (e.g. fine-grain abstraction is disabled),
221  no BNV is treated as input.
222
223  If independentFlag is TRUE, invisible latches are regarded as
224  inputs; otherwise, they are regarded as latches.]
225
226  SideEffects []
227
228******************************************************************************/
229Fsm_Fsm_t *
230GrabCreateAbstractFsm( 
231  Ntk_Network_t *network,
232  st_table *coiBnvTable,
233  st_table *absVarTable,
234  st_table *absBnvTable,
235  int partitionFlag,
236  int independentFlag)
237{
238  Fsm_Fsm_t    *fsm;
239  array_t *absLatches = array_alloc(Ntk_Node_t *, 0);
240  array_t *invisibleVars = array_alloc(Ntk_Node_t *, 0);
241  array_t *absInputs = array_alloc(Ntk_Node_t *, 0);
242  array_t *rootNodesArray = array_alloc(Ntk_Node_t *, 0);
243  st_table *rawLeafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
244  lsList topologicalNodeList;
245  lsGen  lsgen;
246  st_generator *stgen;
247  Ntk_Node_t *node;
248
249  GrabUpdateAbstractPartition(network, coiBnvTable, absVarTable, absBnvTable,
250                              partitionFlag);
251
252  /* first, compute the absLatches, invisibleVars, and absInputs:
253   * absLatches includes all the visible latch variables;
254   * invisibleVars includes all the invisible latches variables;
255   * absInputs includes all the primary and pseudo inputs.
256   */
257  st_foreach_item(absVarTable, stgen, &node, NIL(char *)) {
258    array_insert_last(Ntk_Node_t *, absLatches, node);
259    array_insert_last(Ntk_Node_t *, rootNodesArray, 
260                      Ntk_LatchReadDataInput(node));
261    array_insert_last(Ntk_Node_t *, rootNodesArray, 
262                      Ntk_LatchReadInitialInput(node));
263  }
264   
265  Ntk_NetworkForEachCombInput(network, lsgen, node) {
266    st_insert(rawLeafNodesTable, node, (char *) (long) (-1) );
267  }
268  st_foreach_item(coiBnvTable, stgen, &node, NIL(char *)) {
269    /* unless it blongs to the current Abstract Model */
270    if (absBnvTable && !st_is_member(absBnvTable, node))
271      st_insert(rawLeafNodesTable, node, (char *) (long) (-1) );
272  }
273
274  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
275                                                           rootNodesArray,
276                                                           rawLeafNodesTable);
277  lsForEachItem(topologicalNodeList, lsgen, node){
278    if (st_is_member(rawLeafNodesTable, node) &&
279        !st_is_member(absVarTable, node) ) {
280      /*if (Ntk_NodeTestIsLatch(node) ||
281        coiBnvTable && st_is_member(coiBnvTable, node))*/
282      if (Ntk_NodeTestIsLatch(node) || 
283          (coiBnvTable && st_is_member(coiBnvTable, node)))
284        array_insert_last(Ntk_Node_t *, invisibleVars, node);
285      else
286        array_insert_last(Ntk_Node_t *, absInputs, node);
287    }
288  }
289 
290  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
291  st_free_table(rawLeafNodesTable);
292  array_free(rootNodesArray);
293
294
295  /* now, create the abstract Fsm according to the value of
296   * independentFlag when independentFlag is TRUE, the present state
297   * varaibles are absLatches; otherwise, they contain both absLatches
298   * and invisibleVars (with such a FSM, preimages may contain
299   * invisible vars in their supports)
300   */
301  fsm = Fsm_FsmCreateAbstractFsm(network, NIL(graph_t), 
302                                 absLatches, invisibleVars, absInputs, 
303                                 NIL(array_t), independentFlag);
304
305#if 0
306  /* for debugging */
307  if (partitionFlag == GRAB_PARTITION_NOCHANGE) {
308    GrabPrintNodeArray("absLatches", absLatches);
309    GrabPrintNodeArray("invisibleVars", invisibleVars);
310    GrabPrintNodeArray("absInputs", absInputs);
311  }
312#endif
313
314  array_free(invisibleVars);
315  array_free(absInputs);
316  array_free(absLatches);
317
318
319  return fsm;
320}
321
322/**Function********************************************************************
323
324  Synopsis [Computes the set of initial states of set of latches.]
325
326  Description [Computes the set of initial states of a set of latches.
327  The nodes driving the initial inputs of the latches, called the
328  initial nodes, must not have latches in their support.  If an
329  initial node is found that has a latch in its transitive fanin, then
330  a NULL MDD is returned, and a message is written to the
331  error_string.<p>
332 
333  The initial states are computed as follows. For each latch i, the relation
334  (x_i = g_i(u)) is built, where x_i is the present state variable of latch i,
335  and g_i(u) is the multi-valued initialization function of latch i, in terms
336  of the input variables u.  These relations are then conjuncted, and the
337  input variables are existentially quantified from the result
338  (i.e. init_states(x) = \exists u \[\prod (x_i = g_i(u))\]).]
339
340  SideEffects [The result of the initial state computation is stored with
341  the FSM.]
342
343  SeeAlso [Fsm_FsmComputeReachableStates]
344 
345******************************************************************************/
346mdd_t *
347GrabComputeInitialStates(
348  Ntk_Network_t *network,
349  array_t *psVars)
350{
351  int            i = 0;
352  mdd_t         *initStates;
353  Ntk_Node_t    *node;
354  array_t       *initRelnArray;
355  array_t       *initMvfs;
356  array_t       *initNodes;
357  array_t       *initVertices;
358  array_t       *latchMddIds;
359  array_t       *inputVars = array_alloc(int, 0);
360  array_t       *combArray;
361  st_table      *supportNodes;
362  st_table      *supportVertices;
363  mdd_manager   *mddManager = Ntk_NetworkReadMddManager(network);
364  graph_t       *partition  =
365    (graph_t *) Ntk_NetworkReadApplInfo(network, PART_NETWORK_APPL_KEY);
366  int            numLatches;
367  Img_MethodType imageMethod;
368 
369  numLatches = array_n(psVars);
370
371  /* Get the array of initial nodes, both as network nodes and as
372   * partition vertices.
373   */
374  initNodes    = array_alloc(Ntk_Node_t *, numLatches);
375  initVertices = array_alloc(vertex_t *, numLatches);
376  latchMddIds  = array_alloc(int, numLatches);
377  for (i=0; i<numLatches; i++){
378    int latchMddId = array_fetch(int, psVars, i);
379    Ntk_Node_t *latch = Ntk_NetworkFindNodeByMddId(network, latchMddId);
380    Ntk_Node_t *initNode   = Ntk_LatchReadInitialInput(latch);
381    vertex_t   *initVertex = Part_PartitionFindVertexByName(partition,
382                                Ntk_NodeReadName(initNode));
383    array_insert(Ntk_Node_t *, initNodes, i, initNode);
384    array_insert(vertex_t *, initVertices, i, initVertex);
385    array_insert(int, latchMddIds, i, Ntk_NodeReadMddId(latch));
386  }
387
388  /* Get the table of legal support nodes, both as network nodes and
389   * as partition vertices. Inputs (both primary and pseudo) and
390   * constants constitute the legal support nodes.
391   */
392  supportNodes    = st_init_table(st_ptrcmp, st_ptrhash);
393  supportVertices = st_init_table(st_ptrcmp, st_ptrhash);
394  combArray = Ntk_NodeComputeTransitiveFaninNodes(network, initNodes, TRUE,
395                                                  TRUE);
396  arrayForEachItem(Ntk_Node_t *, combArray, i, node) {
397    vertex_t *vertex = Part_PartitionFindVertexByName(partition,
398                                                      Ntk_NodeReadName(node));
399    if (Ntk_NodeTestIsConstant(node) || Ntk_NodeTestIsInput(node)) {
400      st_insert(supportNodes,  node, NIL(char));
401      st_insert(supportVertices,  vertex, NIL(char));
402    }
403    if (Ntk_NodeTestIsInput(node)) {
404      assert(Ntk_NodeReadMddId(node) != -1);
405      array_insert_last(int, inputVars, Ntk_NodeReadMddId(node));
406    }
407  }
408  array_free(combArray);
409  array_free(initNodes);
410  st_free_table(supportNodes);
411
412  /* Compute the initial states
413   */
414  initMvfs = Part_PartitionCollapse(partition, initVertices,
415                                    supportVertices, NIL(mdd_t)); 
416  array_free(initVertices);
417  st_free_table(supportVertices);
418
419  /* Compute the relation (x_i = g_i(u)) for each latch. */
420  initRelnArray = array_alloc(mdd_t*, numLatches);
421  for (i = 0; i < numLatches; i++) {
422    int latchMddId = array_fetch(int, latchMddIds, i);
423    Mvf_Function_t *initMvf = array_fetch(Mvf_Function_t *, initMvfs, i);
424    mdd_t *initLatchReln = Mvf_FunctionBuildRelationWithVariable(initMvf,
425                                                                latchMddId);
426    array_insert(mdd_t *, initRelnArray, i, initLatchReln);
427  }
428
429  array_free(latchMddIds);
430  Mvf_FunctionArrayFree(initMvfs);
431
432  imageMethod = Img_UserSpecifiedMethod();
433  if (imageMethod != Img_Iwls95_c && imageMethod != Img_Mlp_c)
434    imageMethod = Img_Iwls95_c;
435
436  initStates = Img_MultiwayLinearAndSmooth(mddManager, initRelnArray,
437                                           inputVars, psVars,
438                                           imageMethod, Img_Forward_c); 
439 
440  mdd_array_free(initRelnArray); 
441 
442  array_free(inputVars);
443 
444  return (initStates);
445}
446
447/**Function********************************************************************
448
449  Synopsis [Compute the reachable states of the abstract model.]
450
451  Description [Compute the reachable states of the abstract model.]
452 
453  SideEffects []
454
455******************************************************************************/
456mdd_t *
457GrabFsmComputeReachableStates(
458  Fsm_Fsm_t *absFsm,
459  st_table  *absVarTable,
460  st_table  *absBnvTable,
461  array_t   *invStatesArray,
462  int       verbose)
463{
464  mdd_manager     *mddManager = Fsm_FsmReadMddManager(absFsm);
465  Img_ImageInfo_t *imageInfo;
466  array_t         *fwdOnionRings;
467  mdd_t           *initStates, *mdd1,  *mddOne, *rchStates, *frontier;
468 
469  imageInfo = Fsm_FsmReadOrCreateImageInfo(absFsm, 0, 1);
470
471  fwdOnionRings = array_alloc(mdd_t *, 0);
472  mddOne = mdd_one(mddManager);
473  initStates = Fsm_FsmComputeInitialStates(absFsm);
474  array_insert_last(mdd_t *, fwdOnionRings, initStates);
475  rchStates = mdd_dup(initStates);
476
477  frontier = initStates;
478  while(TRUE) {
479    mdd1 = Img_ImageInfoComputeFwdWithDomainVars(imageInfo, frontier,
480                                                 rchStates, mddOne);
481    frontier = mdd_and(mdd1, rchStates, 1, 0);
482    mdd_free(mdd1);
483
484    mdd1 = rchStates;
485    rchStates = mdd_or(rchStates, frontier, 1, 1);
486    mdd_free(mdd1);
487
488    if (mdd_is_tautology(frontier, 0)) {
489      mdd_free(frontier);
490      break;
491    }
492    array_insert_last(mdd_t *, fwdOnionRings, frontier);
493
494    /* if this happens, the invariant is voilated */
495    if (!mdd_lequal_array(frontier, invStatesArray, 1, 1))
496      break;
497  }
498
499  mdd_free(mddOne);
500
501  FsmSetReachabilityOnionRings(absFsm, fwdOnionRings);
502
503  return rchStates;
504}
505
506/**Function********************************************************************
507
508  Synopsis [Compute the reachable states inside the SORs.]
509
510  Description [Compute the reachable states inside the SORs.]
511 
512  SideEffects []
513
514******************************************************************************/
515mdd_t *
516GrabFsmComputeConstrainedReachableStates(
517  Fsm_Fsm_t *absFsm,
518  st_table *absVarTable,
519  st_table *absBnvTable,
520  array_t *SORs,
521  int verbose)
522{
523  mdd_manager     *mddManager = Fsm_FsmReadMddManager(absFsm);
524  Img_ImageInfo_t *imageInfo;
525  array_t         *rchOnionRings;
526  mdd_t           *mdd1, *mdd2, *mdd3, *mdd4;
527  mdd_t           *mddOne, *initStates, *rchStates;
528  int             i;
529
530  assert (SORs != NIL(array_t));
531
532  imageInfo = Fsm_FsmReadOrCreateImageInfo(absFsm, 0, 1);
533
534  rchOnionRings = array_alloc(mdd_t *, 0);
535  mddOne = mdd_one(mddManager);
536
537  /* the new initial states */
538  mdd2 = array_fetch(mdd_t *, SORs, 0);
539  mdd1 = Fsm_FsmComputeInitialStates(absFsm);
540  initStates = mdd_and(mdd1, mdd2, 1, 1);
541  mdd_free(mdd1);
542  array_insert(mdd_t *, rchOnionRings, 0, initStates);
543
544  /* compute the reachable states inside the previous SORs */
545  rchStates = mdd_dup(initStates);
546  for (i=0; i<array_n(SORs)-1; i++) {
547    mdd1 = array_fetch(mdd_t *, rchOnionRings, i);
548    mdd2 = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
549                                                 mdd1,
550                                                 rchStates,
551                                                 mddOne);
552
553    mdd3 = array_fetch(mdd_t *, SORs, i+1);
554    mdd4 = mdd_and(mdd2, mdd3, 1, 1);
555    mdd_free(mdd2);
556
557    /* if this happens, the last ring is no longer reachable */
558    if (mdd_is_tautology(mdd4, 0)) {
559      mdd_free(mdd4);
560      break;
561    }
562    array_insert(mdd_t *, rchOnionRings, i+1, mdd4);
563
564    mdd1 = rchStates;
565    rchStates = mdd_or(rchStates, mdd4, 1, 1);
566    mdd_free(mdd1);
567  }
568
569  mdd_free(mddOne);
570
571  FsmSetReachabilityOnionRings(absFsm, rchOnionRings);
572
573  return rchStates;
574}
575
576/**Function********************************************************************
577
578  Synopsis [Compute the Synchronous Onion Rings (SORs).]
579
580  Description [Compute the Synchronous Onion Rings (SORs) with
581  backward reachability analysis. The SORs capture all the shortest
582  counter-examples to an invariant property. If the forward
583  reachability onion rings is not provided (as oldRings), it will be
584  retrived from absFsm.
585
586  cexType controls the type of the counter-example envelope:
587      GRAB_CEX_MINTERM, a single-state path,
588      GRAB_CEX_CUBE, a cube-states path,
589      GRAB_CEX_SOR, the SORs.
590  ]
591 
592  SideEffects []
593
594******************************************************************************/
595array_t *
596GrabFsmComputeSynchronousOnionRings(
597  Fsm_Fsm_t *absFsm,
598  st_table  *absVarTable,
599  st_table  *absBnvTable,
600  array_t   *oldRings,
601  mdd_t     *inv_states,
602  int       cexType,
603  int       verbose)
604{
605  mdd_manager     *mddManager = Fsm_FsmReadMddManager(absFsm);
606  Img_ImageInfo_t *imageInfo;
607  array_t         *onionRings, *synOnionRings;
608  array_t         *allPSVars;
609  mdd_t           *mddOne, *ring;
610  mdd_t           *mdd1, *mdd2, *mdd3, *mdd4;
611  int             j;
612
613  imageInfo = Fsm_FsmReadOrCreateImageInfo(absFsm, 1, 0);
614
615  /* get the forward reachability onion rings */
616  onionRings = oldRings;
617  if (onionRings == NIL(array_t))
618    onionRings = Fsm_FsmReadReachabilityOnionRings(absFsm);
619  assert(onionRings);
620
621  synOnionRings = array_alloc(mdd_t *, array_n(onionRings));
622
623  mddOne = mdd_one(mddManager);
624  allPSVars = Fsm_FsmReadPresentStateVars(absFsm);
625
626  /* the last ring */
627  mdd2 = array_fetch_last(mdd_t *, onionRings);
628  mdd1 = mdd_and(mdd2, inv_states, 1, 0);
629  if (cexType == GRAB_CEX_MINTERM)
630    ring = Mc_ComputeAMinterm(mdd1, allPSVars, mddManager);
631  else if (cexType == GRAB_CEX_CUBE) {
632    array_t *bddIds = mdd_get_bdd_support_ids(mddManager, mdd1);
633    int nvars = array_n(bddIds);
634    array_free(bddIds);
635    ring = bdd_approx_remap_ua(mdd1, (bdd_approx_dir_t)BDD_UNDER_APPROX,
636                               nvars, 1024, 1);
637    if (ring == NIL(mdd_t)) 
638      ring = mdd_dup(mdd1);   
639  }else 
640    ring = mdd_dup(mdd1);
641  mdd_free(mdd1);
642  array_insert(mdd_t *, synOnionRings, array_n(onionRings)-1, ring);
643
644  /* the rest rings */
645  for (j=array_n(onionRings)-2; j>=0; j--) {
646    mdd1 = array_fetch(mdd_t *, synOnionRings, j+1);
647    mdd2 = Img_ImageInfoComputeBwdWithDomainVars(imageInfo,
648                                                 mdd1,
649                                                 mdd1,
650                                                 mddOne);
651
652    mdd3 = array_fetch(mdd_t *, onionRings, j);
653    mdd4 = mdd_and(mdd2, mdd3, 1, 1);
654    mdd_free(mdd2);
655
656    if (cexType == GRAB_CEX_MINTERM) 
657      ring = Mc_ComputeAMinterm(mdd4, allPSVars, mddManager);
658    else if (cexType == GRAB_CEX_CUBE) {
659      array_t *bddIds = mdd_get_bdd_support_ids(mddManager, mdd4);
660      int nvars = array_n(bddIds);
661      array_free(bddIds);
662      ring = bdd_approx_remap_ua(mdd4, (bdd_approx_dir_t)BDD_UNDER_APPROX,
663                                 nvars, 1024, 1);
664      if (ring == NIL(mdd_t)) 
665        ring = mdd_dup(mdd4);   
666    }else 
667      ring = mdd_dup(mdd4);
668    mdd_free(mdd4);
669    array_insert(mdd_t *, synOnionRings, j, ring);
670  }
671 
672  mdd_free(mddOne);
673
674  return synOnionRings;
675}
676
677/**Function********************************************************************
678
679  Synopsis    [Get the visible variable mddIds of the current abstraction.]
680
681  Description [Get the visible variable mddIds of the current
682  abstraction. Note that they are the state variables.]
683
684  SideEffects []
685
686******************************************************************************/
687array_t *
688GrabGetVisibleVarMddIds (
689  Fsm_Fsm_t *absFsm,
690  st_table *absVarTable)
691{
692  array_t       *visibleVarMddIds = array_alloc(int, 0);
693  st_generator  *stgen;
694  Ntk_Node_t    *node;
695  int           mddId;
696
697  st_foreach_item(absVarTable, stgen, &node, NIL(char *)) {
698    mddId = Ntk_NodeReadMddId(node);
699    array_insert_last(int, visibleVarMddIds, mddId);
700  }
701
702  return visibleVarMddIds;
703}
704
705
706/**Function********************************************************************
707
708  Synopsis    [Get the invisible variable mddIds of the current abstraction.]
709
710  Description [Get the invisible variable mddIds of the current
711  abstraction. Note that they include both state variables and boolean
712  network variables.]
713
714  SideEffects []
715
716******************************************************************************/
717array_t *
718GrabGetInvisibleVarMddIds(
719  Fsm_Fsm_t *absFsm,
720  st_table *absVarTable,
721  st_table *absBnvTable)
722{
723  Ntk_Network_t *network = Fsm_FsmReadNetwork(absFsm);
724  array_t       *inputVars = Fsm_FsmReadInputVars(absFsm);
725  array_t       *invisibleVarMddIds = array_alloc(int, 0);
726  Ntk_Node_t    *node;
727  int           i, mddId;
728
729  arrayForEachItem(int, inputVars, i, mddId) {
730    node = Ntk_NetworkFindNodeByMddId(network, mddId);
731    if ( !Ntk_NodeTestIsInput(node) && 
732         !st_is_member(absVarTable, node) ) {
733      if (absBnvTable != NIL(st_table)) {
734        if (!st_is_member(absBnvTable, node)) {
735          array_insert_last(int, invisibleVarMddIds, mddId);
736        }
737      }else
738        array_insert_last(int, invisibleVarMddIds, mddId);
739    }
740  }
741
742  return invisibleVarMddIds;
743}
744
745/**Function********************************************************************
746
747  Synopsis    [Test whether the refinement set of latches is sufficient.]
748
749  Description [Test whether the refinement set of latches is sufficient.]
750
751  SideEffects []
752
753******************************************************************************/
754int
755GrabTestRefinementSetSufficient(
756  Ntk_Network_t *network,
757  array_t *SORs,
758  st_table *absVarTable,
759  int verbose)
760{
761  int  is_sufficient;
762
763  is_sufficient = !Bmc_AbstractCheckAbstractTraces(network,
764                                                   SORs,
765                                                   absVarTable,
766                                                   0, 0, 0);
767  return is_sufficient;
768}
769
770/**Function********************************************************************
771
772  Synopsis    [Test whether the refinement set of BNVs is sufficient.]
773
774  Description [Test whether the refinement set of BNVs is sufficient.]
775
776  SideEffects []
777
778******************************************************************************/
779int
780GrabTestRefinementBnvSetSufficient(
781  Ntk_Network_t   *network,
782  st_table        *coiBnvTable,
783  array_t         *SORs,
784  st_table        *absVarTable,
785  st_table        *absBnvTable,
786  int             verbose)
787{
788  int     is_sufficient;
789 
790  assert(absBnvTable && coiBnvTable);
791
792  is_sufficient = 
793    !Bmc_AbstractCheckAbstractTracesWithFineGrain(network,
794                                                  coiBnvTable,
795                                                  SORs,
796                                                  absVarTable,
797                                                  absBnvTable);
798  return is_sufficient;
799}
800
801/**Function********************************************************************
802
803  Synopsis    [Minimize the refinement set of latch variable.]
804
805  Description [Minimize the refinement set of latch variable. After
806  that, also prune away the boolean network variables that are no
807  longer in the transitive fan-in.]
808
809  SideEffects []
810
811******************************************************************************/
812void
813GrabMinimizeLatchRefinementSet(
814  Ntk_Network_t *network,
815  st_table **absVarTable,
816  st_table **absBnvTable,
817  array_t *newlyAddedLatches, 
818  array_t **newlyAddedBnvs, 
819  array_t *SORs,
820  int verbose)
821{
822  st_table      *newVertexTable, *oldBnvTable, *transFaninTable;
823  array_t       *rootArray, *transFanins, *oldNewlyAddedBnvs;
824  st_generator  *stgen;
825  Ntk_Node_t    *node;
826  int           i, flag, n_size, mddId;
827 
828  n_size = array_n(newlyAddedLatches);
829
830  if (verbose >= 3) 
831    fprintf(vis_stdout,
832            "-- grab: minimize latch refinement set: previous size is %d\n", 
833            n_size);
834
835  arrayForEachItem(int, newlyAddedLatches, i, mddId) {
836    node = Ntk_NetworkFindNodeByMddId(network, mddId);
837    /* first, try to drop it */
838    newVertexTable = st_copy(*absVarTable);
839    flag = st_delete(newVertexTable, &node, NIL(char *));
840    assert(flag);
841    /* if the counter-example does not come back, drop it officially */
842    flag = Bmc_AbstractCheckAbstractTraces(network,SORs,
843                                           newVertexTable, 0, 0, 0);
844    if (!flag) {
845      st_free_table(*absVarTable);
846      *absVarTable = newVertexTable;
847      n_size--;
848    }else {
849      st_free_table(newVertexTable);
850      if (verbose >= 3)
851        fprintf(vis_stdout,"         add back %s (latch)\n", 
852                Ntk_NodeReadName(node));
853    }
854  }
855
856  if (verbose >= 3)
857    fprintf(vis_stdout,
858            "-- grab: minimize latch refinement set: current  size is %d\n", 
859            n_size);
860
861  /* prune away irrelevant BNVs */
862  if (*absBnvTable != NIL(st_table) && st_count(*absBnvTable)>0) {
863
864    rootArray = array_alloc(Ntk_Node_t *, 0);
865    st_foreach_item(*absVarTable, stgen, &node, NIL(char *)) {
866      array_insert_last(Ntk_Node_t *, rootArray, Ntk_LatchReadDataInput(node));
867      array_insert_last(Ntk_Node_t *, rootArray, 
868                        Ntk_LatchReadInitialInput(node));
869    }
870    transFanins = Ntk_NodeComputeTransitiveFaninNodes(network, rootArray,
871                                                      TRUE, /*stopAtLatch*/
872                                                      FALSE /*combInputsOnly*/
873                                                      );
874    array_free(rootArray);
875
876    transFaninTable = st_init_table(st_ptrcmp, st_ptrhash);
877    arrayForEachItem(Ntk_Node_t *, transFanins, i, node) {
878      st_insert(transFaninTable, node, NIL(char));
879    }
880    array_free(transFanins);
881       
882    oldBnvTable = *absBnvTable;
883    oldNewlyAddedBnvs = *newlyAddedBnvs;
884    *absBnvTable = st_init_table(st_ptrcmp, st_ptrhash);
885    *newlyAddedBnvs = array_alloc(int, 0);
886    st_foreach_item(oldBnvTable, stgen, &node, NIL(char *)) {
887      if (st_is_member(transFaninTable, node))
888        st_insert(*absBnvTable, node, NIL(char));
889    }
890    arrayForEachItem(int, oldNewlyAddedBnvs, i, mddId) {
891      node = Ntk_NetworkFindNodeByMddId(network, mddId);
892      if (st_is_member(transFaninTable, node))
893        array_insert_last(int, *newlyAddedBnvs, mddId);
894    }
895    st_free_table(transFaninTable);
896
897    if (verbose >= 5) {
898      st_foreach_item(oldBnvTable, stgen, &node, NIL(char *)) {
899        if (!st_is_member(*absBnvTable, node)) 
900          fprintf(vis_stdout, "         prune away BNV %s\n", Ntk_NodeReadName(node));
901      }
902    }
903   
904    array_free(oldNewlyAddedBnvs);
905    st_free_table(oldBnvTable);
906  }
907 
908}
909
910
911/**Function********************************************************************
912
913  Synopsis    [Minimize the refinement set of latch variable.]
914
915  Description [Minimize the refinement set of latch variable. After
916  that, also prune away the boolean network variables that are no
917  longer in the transitive fan-in.]
918
919  SideEffects []
920
921******************************************************************************/
922void
923GrabMinimizeBnvRefinementSet(
924  Ntk_Network_t *network,
925  st_table *coiBnvTable,
926  st_table *absVarTable,
927  st_table **absBnvTable,
928  array_t *newlyAddedBnvs,   
929  array_t *SORs,
930  int verbose)
931{
932  st_table   *newBnvTable;
933  Ntk_Node_t *node;
934  int        i, flag, n_size, mddId;
935 
936  n_size = array_n(newlyAddedBnvs);
937
938  if (verbose >= 3)
939    fprintf(vis_stdout,
940            "-- grab: minimize bnv refinement set: previous size is %d\n", 
941            n_size);
942
943  arrayForEachItem(int, newlyAddedBnvs, i, mddId) {
944    node = Ntk_NetworkFindNodeByMddId(network, mddId);
945    /* first, try to drop it */
946    newBnvTable = st_copy(*absBnvTable);
947    flag = st_delete(newBnvTable, &node, NIL(char *));
948    assert(flag);
949    /* if the counter-example does not come back, drop it officially */
950    flag = Bmc_AbstractCheckAbstractTracesWithFineGrain(network,
951                                                        coiBnvTable, 
952                                                        SORs,
953                                                        absVarTable,
954                                                        newBnvTable);
955    if (!flag) {
956      st_free_table(*absBnvTable);
957      *absBnvTable = newBnvTable;
958      n_size--;
959    }else {
960      st_free_table(newBnvTable);
961      if (verbose >= 3)
962        fprintf(vis_stdout,"         add back %s (BNV)\n", 
963                Ntk_NodeReadName(node));
964    }
965  }
966
967  if (verbose >= 3)
968    fprintf(vis_stdout,
969            "-- grab: minimize bnv refinement set: current  size is %d\n", 
970            n_size);
971} 
972
973/**Function********************************************************************
974
975  Synopsis    [Clear the fields of mddId for all network nodes.]
976
977  Description [Clear the fields of mddId for all network nodes.]
978
979  SideEffects []
980
981******************************************************************************/
982void 
983GrabNtkClearAllMddIds(
984  Ntk_Network_t *network)
985{
986#ifndef NDEBUG
987  mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
988#endif
989  Ntk_Node_t *node;
990  lsGen lsgen;
991
992  assert(mddManager == NIL(mdd_manager));
993
994  Ntk_NetworkForEachNode(network, lsgen, node) {
995    Ntk_NodeSetMddId(node, NTK_UNASSIGNED_MDD_ID);
996  }
997}
998
999/**Function********************************************************************
1000
1001  Synopsis    [Print an array of network nodes.]
1002
1003  Description [Print an array of network nodes.]
1004 
1005  SideEffects []
1006
1007******************************************************************************/
1008void 
1009GrabPrintNodeArray(
1010  char *caption,
1011  array_t *theArray)
1012{
1013  Ntk_Node_t *node;
1014  char string[32];
1015  int i;
1016
1017  fprintf(vis_stdout, "\n%s[%d] =\n", caption, theArray?array_n(theArray):0);
1018
1019  if (!theArray) return;
1020
1021  arrayForEachItem(Ntk_Node_t *, theArray, i, node) {
1022    if (Ntk_NodeTestIsLatch(node))
1023      strcpy(string, "latch");
1024    else if (Ntk_NodeTestIsInput(node))
1025      strcpy(string, "input");
1026    else if (Ntk_NodeTestIsLatchDataInput(node))
1027      strcpy(string, "latchDataIn");
1028    else if (Ntk_NodeTestIsLatchInitialInput(node))
1029      strcpy(string, "latchInitIn");
1030    else if (Ntk_NodeTestIsConstant(node))
1031      strcpy(string, "const");
1032    else 
1033      strcpy(string, "BNV");
1034
1035    fprintf(vis_stdout, "%s\t(%s)\n", Ntk_NodeReadName(node), string);
1036  }
1037}
1038
1039/**Function********************************************************************
1040
1041  Synopsis    [Print an array of network nodes.]
1042
1043  Description [Print an array of network nodes.]
1044 
1045  SideEffects []
1046
1047******************************************************************************/
1048void 
1049GrabPrintMddIdArray(
1050  Ntk_Network_t *network,
1051  char *caption,
1052  array_t *mddIdArray)
1053{
1054  Ntk_Node_t *node;
1055  array_t *theArray = array_alloc(Ntk_Node_t *, array_n(mddIdArray));
1056  int i, mddId;
1057
1058  arrayForEachItem(int, mddIdArray, i, mddId) {
1059    node = Ntk_NetworkFindNodeByMddId(network, mddId);
1060    array_insert(Ntk_Node_t *, theArray, i, node);
1061  }
1062
1063  GrabPrintNodeArray(caption, theArray);
1064
1065  array_free(theArray);
1066
1067}
1068
1069/**Function********************************************************************
1070
1071  Synopsis    [Print a list of network nodes.]
1072
1073  Description [Print a list of network nodes.]
1074 
1075  SideEffects []
1076
1077******************************************************************************/
1078void 
1079GrabPrintNodeList(
1080  char *caption, 
1081  lsList theList)
1082{
1083  Ntk_Node_t *node;
1084  char string[32];
1085  lsGen lsgen;
1086
1087  fprintf(vis_stdout, "\n%s[%d] =\n", caption, theList?lsLength(theList):0);
1088 
1089  if (!theList) return;
1090
1091  lsForEachItem(theList, lsgen, node) {
1092    if (Ntk_NodeTestIsLatch(node))
1093      strcpy(string, "latch");
1094    else if (Ntk_NodeTestIsInput(node))
1095      strcpy(string, "input");
1096    else if (Ntk_NodeTestIsLatchDataInput(node))
1097      strcpy(string, "latchDataIn");
1098    else if (Ntk_NodeTestIsLatchInitialInput(node))
1099      strcpy(string, "latchInitIn");
1100    else if (Ntk_NodeTestIsConstant(node))
1101      strcpy(string, "const");
1102    else 
1103      strcpy(string, "BNV");
1104
1105    fprintf(vis_stdout, "   %s\t %s\n", string, Ntk_NodeReadName(node));
1106  }
1107}
1108
1109/**Function********************************************************************
1110
1111  Synopsis    [Print a hash table of network nodes.]
1112
1113  Description [Print a hash table of network nodes.]
1114 
1115  SideEffects []
1116
1117******************************************************************************/
1118void 
1119GrabPrintNodeHashTable(
1120  char *caption,
1121  st_table *theTable)
1122{
1123  Ntk_Node_t *node;
1124  char string[32];
1125  long  value;
1126  st_generator *stgen;
1127
1128  fprintf(vis_stdout, "\n%s[%d] =\n", caption, theTable?st_count(theTable):0);
1129
1130  if (!theTable) return;
1131
1132  st_foreach_item(theTable, stgen, &node, &value) {
1133    if (Ntk_NodeTestIsLatch(node))
1134      strcpy(string, "latch");
1135    else if (Ntk_NodeTestIsInput(node))
1136      strcpy(string, "input");
1137    else if (Ntk_NodeTestIsLatchDataInput(node))
1138      strcpy(string, "latchDataIn");
1139    else if (Ntk_NodeTestIsLatchInitialInput(node))
1140      strcpy(string, "latchInitIn");
1141    else if (Ntk_NodeTestIsConstant(node))
1142      strcpy(string, "const");
1143    else 
1144      strcpy(string, "BNV");
1145
1146    if (value != 0)
1147      fprintf(vis_stdout, "   %s\t %s\t %ld\n", string, Ntk_NodeReadName(node),
1148              value);
1149    else
1150      fprintf(vis_stdout, "   %s\t %s \n", string, Ntk_NodeReadName(node));
1151  }
1152}
1153
1154/*---------------------------------------------------------------------------*/
1155/* Definition of static functions                                            */
1156/*---------------------------------------------------------------------------*/
1157
1158/**Function********************************************************************
1159
1160  Synopsis    [Get network nodes that are mentioned by the formula.]
1161
1162  Description [Get network nodes that are mentioned by the formula.]
1163
1164  SideEffects []
1165
1166******************************************************************************/
1167static void
1168GetFormulaNodes(
1169  Ntk_Network_t *network,
1170  Ctlp_Formula_t *F,
1171  array_t *formulaNodes)
1172{
1173
1174  if (F == NIL(Ctlp_Formula_t))
1175    return;
1176
1177  if (Ctlp_FormulaReadType(F) == Ctlp_ID_c) {
1178    char *nodeNameString = Ctlp_FormulaReadVariableName(F);
1179    Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
1180    assert(node);
1181    array_insert_last(Ntk_Node_t *, formulaNodes, node);
1182    return;
1183  }
1184 
1185  GetFormulaNodes(network, Ctlp_FormulaReadRightChild(F), formulaNodes);
1186  GetFormulaNodes(network, Ctlp_FormulaReadLeftChild(F),  formulaNodes);
1187}
1188
1189
1190/**Function********************************************************************
1191
1192  Synopsis    [Get the fan-in latches of those already in the table.]
1193
1194  Description [Get the fan-in latches of those already in the table.]
1195
1196  SideEffects []
1197
1198******************************************************************************/
1199static void 
1200GetFaninLatches(
1201  Ntk_Node_t *node,
1202  st_table *visited,
1203  st_table *absVarTable)
1204{
1205  if (st_is_member(visited, node))
1206    return;
1207
1208  st_insert(visited, node, (char *)0);
1209
1210  if (Ntk_NodeTestIsLatch(node)) 
1211    st_insert(absVarTable, node, (char *)0);
1212  else {
1213    int i;
1214    Ntk_Node_t *fanin;
1215    Ntk_NodeForEachFanin(node, i, fanin) {
1216      GetFaninLatches(fanin, visited, absVarTable);
1217    }
1218  }
1219}
1220
1221/**Function********************************************************************
1222
1223  Synopsis [Add nodes for wires referred to in formula to nodesTable.]
1224
1225  SideEffects []
1226
1227******************************************************************************/
1228static void
1229NodeTableAddCtlFormulaNodes( 
1230  Ntk_Network_t *network,
1231  Ctlp_Formula_t *formula, 
1232  st_table * nodesTable )
1233{
1234  if (formula == NIL(Ctlp_Formula_t)) 
1235    return;
1236
1237  if ( Ctlp_FormulaReadType( formula ) == Ctlp_ID_c ) {
1238    char *nodeNameString = Ctlp_FormulaReadVariableName( formula );
1239    Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
1240    if( node ) 
1241      st_insert( nodesTable, ( char *) node, NIL(char) );
1242    return;
1243  }
1244 
1245  NodeTableAddCtlFormulaNodes( network, Ctlp_FormulaReadRightChild( formula ), nodesTable );
1246  NodeTableAddCtlFormulaNodes( network, Ctlp_FormulaReadLeftChild( formula ), nodesTable );
1247}
1248
1249
Note: See TracBrowser for help on using the repository browser.