source: vis_dev/vis-2.3/src/grab/grabBMC.c @ 36

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

vis2.3
File size: 17.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [grabBMC.c]
4
5  PackageName [grab]
6
7  Synopsis    [Check abstract paths on a more concrete model using SAT.]
8
9  Description [Abstract paths are given in an array of MDDs, which
10  capture multiple abstract paths at the same time. MDDs are encoded
11  as AIG graph to allow the check in the more concrete model.]
12   
13  Author      [Chao Wang]
14
15  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
16  All rights reserved.
17
18  Permission is hereby granted, without written agreement and without
19  license or royalty fees, to use, copy, modify, and distribute this
20  software and its documentation for any purpose, provided that the
21  above copyright notice and the following two paragraphs appear in
22  all copies of this software.]
23
24******************************************************************************/
25
26#include "grabInt.h"
27#include "bmcInt.h"
28
29/*---------------------------------------------------------------------------*/
30/* Constant declarations                                                     */
31/*---------------------------------------------------------------------------*/
32
33/*---------------------------------------------------------------------------*/
34/* Structure declarations                                                    */
35/*---------------------------------------------------------------------------*/
36
37/*---------------------------------------------------------------------------*/
38/* Type declarations                                                         */
39/*---------------------------------------------------------------------------*/
40
41/*---------------------------------------------------------------------------*/
42/* Variable declarations                                                     */
43/*---------------------------------------------------------------------------*/
44
45/*---------------------------------------------------------------------------*/
46/* Macro declarations                                                        */
47/*---------------------------------------------------------------------------*/
48
49/**AutomaticStart*************************************************************/
50
51/*---------------------------------------------------------------------------*/
52/* Static function prototypes                                                */
53/*---------------------------------------------------------------------------*/
54
55static bAigEdge_t GrabConvertBddToBaig(bAig_Manager_t *bAigManager, bdd_t *fn, st_table *bddidToNames);
56static st_table * GrabBddGetSupportBaigNames(mdd_manager *mddManager, mdd_t *f);
57static char * GrabBddIdToBaigNames(mdd_manager *mddManager, int bddid);
58
59/**AutomaticEnd***************************************************************/
60
61/*---------------------------------------------------------------------------*/
62/* Definition of exported functions                                          */
63/*---------------------------------------------------------------------------*/
64
65/**Function********************************************************************
66
67  Synopsis    [Check if the abstract paths exist in the model.]
68
69  Description [Check if the abstract paths exist in the model. The
70  paths are given as set of onion rings, where each ring is a set of
71  states. The model is defined by the set of latches in absLatches.]
72
73  SideEffects []
74
75******************************************************************************/
76boolean
77Bmc_AbstractCheckAbstractTraces(
78  Ntk_Network_t *network,
79  array_t *synOnionRings,
80  st_table *absLatches,
81  int verbose, 
82  int dbgLevel,
83  int printInputs)
84{
85  int               pathLength = array_n(synOnionRings) -1;
86  mAig_Manager_t    *maigManager = Ntk_NetworkReadMAigManager(network);
87  st_table          *nodeToMvfAigTable = NIL(st_table); 
88  BmcCnfClauses_t   *cnfClauses;
89  FILE              *cnfFile;
90  BmcOption_t       *options;
91  array_t           *result;
92  int               i;
93  boolean           CexExit = FALSE;
94 
95  nodeToMvfAigTable =
96    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
97  if (nodeToMvfAigTable == NIL(st_table)){
98    fprintf(vis_stderr, 
99            "** bmc error: please run buid_partiton_maigs first\n");
100    return CexExit;
101  }
102
103  options = BmcOptionAlloc();
104  if (verbose) { 
105    options->dbgLevel = dbgLevel;
106    options->printInputs = printInputs;
107  }
108  options->satInFile = BmcCreateTmpFile();
109  if (options->satInFile == NIL(char)){
110    BmcOptionFree(options);
111    return CexExit;
112  }
113
114  /* create SAT Solver output file */
115  options->satOutFile = BmcCreateTmpFile();
116  if (options->satOutFile == NIL(char)){
117    BmcOptionFree(options);
118    fprintf(vis_stderr, "** bmc error: Cannot allocate a temp file name\n");
119    return CexExit;
120  }
121  cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
122  if (cnfFile == NIL(FILE)) {
123    BmcOptionFree(options);
124    fprintf(vis_stderr, "** bmc error: Cannot create CNF output file %s\n",
125            options->satInFile);
126    return CexExit;
127  }
128
129  /* Unroll the model exactly 'pathLength' time frames
130   */
131  cnfClauses = BmcCnfClausesAlloc();
132  BmcCnfGenerateClausesForPath(network, 0, pathLength, BMC_INITIAL_STATES,
133                               cnfClauses, nodeToMvfAigTable, absLatches);
134
135  /* Generate the constraints from the abstract paths
136   *   (1) build a bAigEdge_t (graph) for each ring
137   *   (2) add all the cnf clauses that describe this graph
138   *   (3) make the output bAigEdge_t equals to 1
139  */
140  {
141    bAigEdge_t  bAigState;
142    mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
143    array_t     *clause = array_alloc(int, 1);
144    mdd_t       *ring;
145
146    arrayForEachItem(mdd_t *, synOnionRings, i, ring) {
147      st_table *bddidTobAigNames;
148      bddidTobAigNames = GrabBddGetSupportBaigNames(mddManager, ring);
149      bAigState = GrabConvertBddToBaig(maigManager, ring, bddidTobAigNames);
150      {
151        st_generator *stgen;
152        long tmpId;
153        char *tmpStr;
154        st_foreach_item(bddidTobAigNames, stgen, &tmpId, &tmpStr) {
155          FREE(tmpStr);
156        }
157        st_free_table(bddidTobAigNames);
158      }
159      array_insert(int, clause, 0, BmcGenerateCnfFormulaForAigFunction(
160                                  maigManager, bAigState, i, cnfClauses));
161      BmcCnfInsertClause(cnfClauses, clause);
162    } 
163   
164    array_free(clause);
165  } 
166
167  /* Call the SAT solver
168   */
169  BmcWriteClauses(maigManager, cnfFile, cnfClauses, options); 
170  fclose(cnfFile);
171  result = BmcCheckSAT(options);
172  if(result != NIL(array_t)){
173    if (verbose >= 1 && dbgLevel ==1) {
174      fprintf(vis_stdout,"Found Counterexample of length = %d\n", pathLength);
175      BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
176                             result, pathLength+1, absLatches, options, 
177                             NIL(array_t));
178    }
179    if (verbose >=1 && dbgLevel == 2) {
180      BmcPrintCounterExampleAiger(network, nodeToMvfAigTable, cnfClauses,
181                             result, pathLength+1, absLatches, options,
182                             NIL(array_t));
183    }   
184    CexExit = TRUE;
185  } 
186
187  /* free all used memories */
188  BmcCnfClausesFree(cnfClauses);
189  array_free(result);
190  BmcOptionFree(options);
191
192  return CexExit;
193}
194
195
196/**Function********************************************************************
197
198  Synopsis    [Check if the abstract paths exist in the fine-grain model.]
199
200  Description [Check if the abstract paths exist in the fine-grain
201  model. The paths are given as set of onion rings, where each ring is
202  a set of states.  The model is defined by the set of latches
203  (absLatches) and bnvs (absBnvs). The entire set of bnvs of the
204  network are stored in the table coiBnvTable.
205
206  This procedure first build a NEW maig graph (for the fine-grain
207  model), then check if the abstract paths exist in the model.
208
209  Before it returns, the previous maig graph is restored.]
210 
211  SideEffects []
212
213******************************************************************************/
214boolean
215Bmc_AbstractCheckAbstractTracesWithFineGrain(
216  Ntk_Network_t *network,
217  st_table *coiBnvTable,
218  array_t *synOnionRings,
219  st_table *absLatches,
220  st_table *absBnvs)
221{
222  boolean             result;
223  mAigManagerState_t  oldMaigState;  /* to store the previous AIG */
224  mAig_Manager_t      *maigManager;
225  lsGen               lsgen;
226  Ntk_Node_t          *node;
227  int                 mAigId;
228  int                 i;
229  st_generator        *stgen;
230  st_table            *leaves;
231  array_t             *roots, *combInputs;
232
233  /* save the existing maigManager */
234  oldMaigState.manager = Ntk_NetworkReadMAigManager(network);
235  oldMaigState.nodeToMvfAigTable = 
236    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
237  oldMaigState.nodeToMAigIdTable = st_init_table(st_ptrcmp, st_ptrhash);
238  Ntk_NetworkForEachNode(network, lsgen, node) {
239    mAigId = Ntk_NodeReadMAigId(node);
240    st_insert(oldMaigState.nodeToMAigIdTable, node, (char *)(long)mAigId);
241    Ntk_NodeSetMAigId(node, ntmaig_UNUSED);
242  }
243
244  /* create a new maigManager */
245  maigManager = mAig_initAig();
246  Ntk_NetworkSetMAigManager(network, maigManager);
247  Ntk_NetworkSetApplInfo(network, MVFAIG_NETWORK_APPL_KEY,
248                         (Ntk_ApplInfoFreeFn) ntmAig_MvfAigTableFreeCallback,
249                         (void *) st_init_table(st_ptrcmp, st_ptrhash));
250
251  /* roots are the visible latches, and the visible bnvs (some bnvs
252   * may not be in the transitive fan-in cone of the visible latches
253   */
254  roots = array_alloc(Ntk_Node_t *, 0);
255  st_foreach_item(absLatches, stgen, &node, NIL(char *)) {
256    array_insert_last(Ntk_Node_t *, roots, Ntk_LatchReadDataInput(node));
257    array_insert_last(Ntk_Node_t *, roots, Ntk_LatchReadInitialInput(node));
258  }
259  st_foreach_item(absBnvs, stgen, &node, NIL(char *)) {
260    array_insert_last(Ntk_Node_t *, roots, node);
261  }
262
263  combInputs = Ntk_NodeComputeTransitiveFaninNodes(network, roots, 
264                                                   TRUE, /* stopAtLatches */
265                                                   FALSE /* combInputsOnly*/
266                                                   );
267
268  /* leaves are the combinational inputs or the invisible bnvs */
269  leaves = st_init_table(st_ptrcmp, st_ptrhash);
270  arrayForEachItem(Ntk_Node_t *, combInputs, i, node) {
271    if ( Ntk_NodeTestIsCombInput(node) ||
272         ( st_is_member(coiBnvTable, node) &&
273           !st_is_member(absBnvs, node) ) ) {
274      st_insert(leaves, node, (char *) ntmaig_UNUSED);
275      Ntk_NodeSetMAigId(node, mAig_CreateVar(maigManager,
276                                             Ntk_NodeReadName(node),
277                   Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
278    }
279  }
280  st_foreach_item(absLatches, stgen, &node, NIL(char *)) {
281    if (!st_is_member(leaves, node)) {
282      st_insert(leaves, node, (char *) ntmaig_UNUSED);
283      Ntk_NodeSetMAigId(node, mAig_CreateVar(maigManager,
284                                             Ntk_NodeReadName(node),
285                   Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
286    }
287  }
288  array_free(combInputs);
289
290#if 1
291  /* THIS SEEMS UNNECESSARY---IT'S HERE TO AVOID ERRORS IN CALLING
292   * ntmaig_NetworkBuildMvfAigs()
293   */
294  Ntk_NetworkForEachCombInput(network, lsgen, node) {
295    if (Ntk_NodeReadMAigId(node) == NTK_UNASSIGNED_MAIG_ID) {
296      Ntk_NodeSetMAigId(node, mAig_CreateVar(maigManager,
297                                             Ntk_NodeReadName(node),
298                   Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
299    } 
300  }
301#endif
302
303  /* build the new AIG graph */
304  ntmaig_NetworkBuildMvfAigs(network, roots, leaves);
305
306  array_free(roots);
307  st_free_table(leaves);
308
309
310  /* check the existence of the abstract path on the new AIG graph */
311  result = Bmc_AbstractCheckAbstractTraces(network,
312                                           synOnionRings,
313                                           absLatches,
314                                           0, 0, 0);
315
316  /* restore the previous maigManager */
317  mAig_quit(maigManager);
318  Ntk_NetworkFreeApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
319  Ntk_NetworkSetMAigManager(network, oldMaigState.manager);
320  Ntk_NetworkSetApplInfo(network, MVFAIG_NETWORK_APPL_KEY,
321                         (Ntk_ApplInfoFreeFn) ntmAig_MvfAigTableFreeCallback,
322                         (void *) oldMaigState.nodeToMvfAigTable);
323  st_foreach_item(oldMaigState.nodeToMAigIdTable, stgen, &node,
324                  &mAigId) {
325    Ntk_NodeSetMAigId(node, mAigId);
326  }
327  st_free_table(oldMaigState.nodeToMAigIdTable);
328
329  return result;
330}
331
332/*---------------------------------------------------------------------------*/
333/* Definition of static functions                                            */
334/*---------------------------------------------------------------------------*/
335
336/**Function********************************************************************
337
338  Synopsis [Build the binary Aig for a given bdd]
339
340  SideEffects [Build the binary Aig for a given bdd.  We assume that
341  the return bdd nodes from the foreach_bdd_node are in the order from
342  childeren to parent. i.e all the childeren nodes are returned before
343  the parent node.
344
345  bddidToNames is a hash table from bddid to its bAigEdge_t name.  If
346  provided, this table should contain entiries for all the bddid in
347  the support.]
348
349  SideEffects []
350
351  SeeAlso     []
352 
353******************************************************************************/
354static bAigEdge_t
355GrabConvertBddToBaig(
356   bAig_Manager_t *bAigManager,
357   bdd_t          *fn,
358   st_table       *bddidToNames)
359{
360  bdd_gen     *gen;
361  bdd_node    *node, *thenNode, *elseNode, *funcNode;
362  bdd_manager *bddManager = bdd_get_manager(fn);
363  bdd_node    *one  = bdd_read_one(bddManager);
364  /*bdd_node    *zero = bdd_read_logic_zero(bddManager);*/
365  int         is_complemented;
366  int         flag;
367  bAigEdge_t  var, left, right, result;
368  char        *name;
369  st_table    *bddTObaigTable;
370 
371  bddTObaigTable = st_init_table(st_numcmp, st_numhash);
372
373  if (fn == NULL){
374    return bAig_NULL;
375  }
376 
377  st_insert(bddTObaigTable, (char *) (long) bdd_regular(one), 
378            (char *) bAig_One);
379
380  funcNode = bdd_get_node(fn, &is_complemented);
381 
382  if (bdd_is_constant(funcNode)){
383    flag = st_lookup(bddTObaigTable, 
384                     (char *) (long) (funcNode),
385                     &result);
386    assert(flag);
387    st_free_table(bddTObaigTable);
388
389    if (is_complemented)
390      return bAig_Not(result);
391    else
392      return result;
393  }
394 
395  foreach_bdd_node(fn, gen, node){
396    /* if the node has been processed, skip it. (the constant ONE
397     * should be the only node falls into this category).
398     */
399    if (st_is_member(bddTObaigTable, (char *) (long) bdd_regular(node)))
400      continue;
401   
402    /*  bdd_node_read_index() return the current level's bddId */
403    if (bddidToNames) {
404      flag = st_lookup(bddidToNames, (char *)(long)bdd_node_read_index(node),
405                       &name);
406      assert(flag);
407      name = util_strsav(name);
408    }else {
409      char tempString[1024];
410      sprintf(tempString, "BDD%d", bdd_node_read_index(node));
411      name = util_strsav(tempString);
412    }
413
414    /*  Create or Retrieve the bAigEdge_t  w.r.t. 'name' */
415    var  = bAig_CreateVarNode(bAigManager, name);
416    FREE(name);
417
418    thenNode  = bdd_bdd_T(node);
419    flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(thenNode),
420                     &left);
421    assert(flag);
422     
423    elseNode  = bdd_bdd_E(node);
424    flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(elseNode),
425                      &right);
426    assert(flag);
427
428    /* should we test here whether elseNode is complemented arc? */
429    if (bdd_is_complement(elseNode))
430      right = bAig_Not(right);
431
432    result =  bAig_Or(bAigManager, bAig_And(bAigManager, var, left),
433                                   bAig_And(bAigManager, bAig_Not(var), right));
434    st_insert(bddTObaigTable, (char *) (long) bdd_regular(node),
435              (char *) (long) result);
436  }
437  flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(funcNode),
438                    &result); 
439  assert(flag);
440  st_free_table(bddTObaigTable);
441
442  if (is_complemented){
443    return bAig_Not(result);
444  } else {
445    return result;
446  }
447} /* end of bAig_bddtobAig() */
448
449
450/**Function********************************************************************
451
452Synopsis    [Get a (bddId,baigName) table for the supporting variableS.]
453
454SideEffects [Get a (bddId,baigName) table for the supporting
455variableS. The caller should free the returned table as well as the
456(char *) of its value field.]
457
458SeeAlso     []
459 
460******************************************************************************/
461static st_table *
462GrabBddGetSupportBaigNames(
463  mdd_manager *mddManager,
464  mdd_t *f)
465{
466  int        numOfVars = bdd_num_vars(mddManager);
467  st_table  *bddidTObaigNames = st_init_table(st_numcmp, st_numhash);
468  var_set_t *vset;
469  int        i;
470
471  vset = bdd_get_support(f);
472  for (i=0; i<numOfVars; i++) {
473    if (var_set_get_elt(vset, i) == 1) {
474      st_insert(bddidTObaigNames, (char *)(long)i, 
475                GrabBddIdToBaigNames(mddManager, i));
476    }
477  }
478  var_set_free(vset);
479
480  return bddidTObaigNames;
481}
482
483/**Function********************************************************************
484
485Synopsis    [return the baigName  of a bddid]
486
487SideEffects [The caller should free the returned char *.  This
488  function is based on the assumption that MDD and MAIG shares the
489  same naming convention (which is true in VIS).]
490
491SeeAlso     []
492 
493******************************************************************************/
494static char *
495GrabBddIdToBaigNames(
496  mdd_manager *mddManager,
497  int            bddid)
498{
499  array_t *mvar_list = mdd_ret_mvar_list(mddManager);
500  array_t *bvar_list = mdd_ret_bvar_list(mddManager);
501  bvar_type bv;
502  mvar_type mv;
503  int     mddid, index, id;
504  char    *nodeName;
505  char    baigName[1024];
506
507  /* 1. from bddid, get mddid and the index of this bddid in the mddid
508   */
509  bv = array_fetch(bvar_type, bvar_list, bddid);
510  mddid = bv.mvar_id;
511  mv = array_fetch(mvar_type, mvar_list, mddid);
512  arrayForEachItem(int, mv.bvars, index, id) {
513    if (id == bddid) 
514      break;
515  }
516  assert(index <= mv.encode_length -1);
517 
518  /* 2. assumptions: (1) mv.name = nodeName, 
519   *                 (2) index is the same for MDD and MAIG
520   */
521  nodeName = mv.name;
522 
523  /* 3. the baigEdge_t's name is ("%s_%d",nodeName,index)
524   */
525  sprintf(baigName, "%s_%d", nodeName, index);
526
527  return util_strsav(baigName);
528}
529
530
531
532
533
534
Note: See TracBrowser for help on using the repository browser.