source: vis_dev/vis-2.3/src/ntk/ntkFlt.c @ 56

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

vis2.3

File size: 33.9 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ntkFlt.c]
4
5  PackageName [ntk]
6
7  Synopsis    [Routines for creating a network from a hierarchy manager.]
8
9  Author      [Adnan Aziz, Tom Shiple]
10
11  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
12  All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18
19  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
20  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
21  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
22  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23
24  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
25  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
26  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
27  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
28  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
29
30******************************************************************************/
31
32#include "ntkInt.h"
33
34static char rcsid[] UNUSED = "$Id: ntkFlt.c,v 1.13 2009/04/11 22:17:58 fabio Exp $";
35
36/*---------------------------------------------------------------------------*/
37/* Constant declarations                                                     */
38/*---------------------------------------------------------------------------*/
39#define MAX_NUMBER_BDD_VARS 500
40
41
42/*---------------------------------------------------------------------------*/
43/* Macro declarations                                                        */
44/*---------------------------------------------------------------------------*/
45
46
47/**AutomaticStart*************************************************************/
48
49/*---------------------------------------------------------------------------*/
50/* Static function prototypes                                                */
51/*---------------------------------------------------------------------------*/
52
53static void NetworkBuildFormalToActualTableRecursively(Ntk_Network_t *network, Hrc_Node_t *hrcNode);
54static void NetworkCreateNodesRecursively(Ntk_Network_t *network, Hrc_Node_t *hrcNode);
55static void NodeCreateAsNecessary(Ntk_Network_t *network, char *nodeName, Var_Variable_t *var);
56static boolean NetworkDeclareNodesRecursively(Ntk_Network_t *network, Hrc_Node_t *hrcNode, boolean buildMvfs, mdd_manager **mddMgr);
57static array_t * LocalArrayJoin(array_t *array1, array_t *array2);
58static array_t * TableCreateFormalInputNameArray(Tbl_Table_t *table, char *namePrefix);
59static void NameArrayFree(array_t *nameArray);
60static boolean NetworkAbstractNodes(Ntk_Network_t *network, lsList abstractedNames);
61static boolean NodeDeclareWithTable(Ntk_Node_t *node, Tbl_Table_t *table, int outIndex, char *path, boolean buildMvfs, mdd_manager *mddMgr);
62static void NetworkDeclareIONodes(Ntk_Network_t *network, Hrc_Node_t *hrcNode);
63static void NetworkDeclareLatches(Ntk_Network_t *network, Hrc_Node_t *hrcNode);
64static void MddManagerResetIfNecessary(mdd_manager **mddMgr);
65static Mvf_Function_t * LocalMvfFunctionForTable(Tbl_Table_t *table, int outIndex, mdd_manager *mddMgr, array_t *varMap, int *offset);
66
67/**AutomaticEnd***************************************************************/
68
69
70/*---------------------------------------------------------------------------*/
71/* Definition of exported functions                                          */
72/*---------------------------------------------------------------------------*/
73
74/**Function********************************************************************
75
76  Synopsis [Builds a flat description of a subtree of hierarchy manager.]
77
78  Description [Builds a flat description of a subtree of a hierarchy manager.
79  The flattened names of variables are taken as those hierarchical names where
80  the variables are defined.  The names are relative to the "current" node
81  of the hierarchy manager, which can be set by calling
82  Hrc_ManagerSetCurrentNode() first.  Nodes are created even for unused
83  variables (i.e. variables that don't fanout to anything.)<p>
84
85  AbstractedNames is a list of char*.  If the list is not NULL, then this list
86  is interpreted as a list of variables to abstract.  If a given name in the
87  list does not correspond to the hierarchical name of a node in the network,
88  then NULL is returned, and an error message is written to error_string.
89  Otherwise, a new primary input is created to drive the net identified by the
90  variable name.  See the documentation for the command flatten_hierarchy for
91  more information.<p>
92
93  The verification routines assume deterministic and completely specified
94  tables. If a table is found that is locally non-deterministic or incompletely
95  specified, then a message is written to vis_stderr, and a NIL network is
96  returned (the non-deterministic test is not performed on non-deterministic
97  constant tables).  This test can be bypassed (in order to save time) by
98  passing FALSE for buildMvfs. Note that this should be done with extreme
99  caution, because bad tables could inadvertantly be allowed through and
100  invalidate verification results obtained downstream.<p>
101
102  Also, if a table has no inputs and more than 1 output, and its output space
103  is not complete (i.e. the outputs are correlated), then the table is
104  declared a "relation", and NIL is returned.]
105
106  SideEffects []
107
108  Comment [Proceeds in 3 phases: 1) builds a map from formals to actuals, 2)
109  adds a node for each actual (i.e. for each node that will appear in the
110  network) and 3) sets the types (and tables, where appropriate) for each
111  node.]
112
113  SeeAlso [Ntk_NetworkAlloc NetworkBuildFormalToActualTableRecursively
114  NetworkCreateNodesRecursively NetworkDeclareNodesRecursively]
115
116******************************************************************************/
117Ntk_Network_t *
118Ntk_HrcNodeConvertToNetwork(
119  Hrc_Node_t *hrcNode,
120  boolean     buildMvfs,
121  lsList abstractedNames)
122{
123  mdd_manager   *mddMgr;
124  boolean        status1     = TRUE;
125  boolean        status2     = TRUE;
126  char          *hrcNodeName = Hrc_NodeReadInstanceName(hrcNode);
127  Ntk_Network_t *network     = Ntk_NetworkAlloc(hrcNodeName);
128
129  NetworkBuildFormalToActualTableRecursively(network, hrcNode);
130  NetworkCreateNodesRecursively(network, hrcNode);
131
132  /*
133   * The MDD manager is for building temporary MDDs.  For robustness, enable
134   * reordering.
135   */
136  mddMgr = mdd_init_empty();
137  bdd_dynamic_reordering(mddMgr, BDD_REORDER_SIFT, BDD_REORDER_VERBOSITY_DEFAULT);
138  status1 = NetworkDeclareNodesRecursively(network, hrcNode, buildMvfs, &mddMgr);
139  mdd_quit(mddMgr);
140
141  if (abstractedNames != (lsList) NULL) {
142    status2 = NetworkAbstractNodes(network, abstractedNames);
143  }
144
145  if (!(status1 && status2)) {
146    Ntk_NetworkFree(network);
147    return NIL(Ntk_Network_t);
148  }
149  else {
150    return network;
151  }
152}
153
154
155/*---------------------------------------------------------------------------*/
156/* Definition of internal functions                                          */
157/*---------------------------------------------------------------------------*/
158
159
160/*---------------------------------------------------------------------------*/
161/* Definition of static functions                                            */
162/*---------------------------------------------------------------------------*/
163
164
165/**Function********************************************************************
166
167  Synopsis    [Creates mapping from formal names to actual names.]
168
169  Description [Loads the formal-to-actual table of network.  For each formal
170  variable name in hrcNode, maps it to a unique actual variable name.  The map
171  is many-to-one.  The rule is that a formal is resolved to the actual as high
172  in the hierarchy as possible.  Proceeds recursively by examining
173  subcircuits. Note that only formals are in the domain of the map. Also, care
174  has to be taken when looking at net in parent since they may also be
175  formals.]
176
177  SideEffects []
178
179******************************************************************************/
180static void
181NetworkBuildFormalToActualTableRecursively(
182  Ntk_Network_t *network,
183  Hrc_Node_t *hrcNode)
184{
185  st_generator *stGen;
186  char         *childName;
187  Hrc_Node_t   *childHrcNode;
188
189  /*
190   * For each child of the current hnode, process its I/O variables, and
191   * then recurse on its children.
192   */
193  Hrc_NodeForEachChild(hrcNode, stGen, childName, childHrcNode) {
194
195    int i;
196    array_t *childFormalInputs  = Hrc_NodeReadFormalInputs(childHrcNode);
197    array_t *childFormalOutputs = Hrc_NodeReadFormalOutputs(childHrcNode);
198    array_t *childFormalIoArray = LocalArrayJoin(childFormalInputs, childFormalOutputs);
199
200    array_t *childActualInputs  = Hrc_NodeReadActualInputs(childHrcNode);
201    array_t *childActualOutputs = Hrc_NodeReadActualOutputs(childHrcNode);
202    array_t *childActualIoArray = LocalArrayJoin(childActualInputs, childActualOutputs);
203
204
205    /*
206     * For each I/O variable, construct the appropriate hierarchical name for
207     * the variable in childHrcNode (formalName) and the variable in the
208     * hrcNode (actualName).  If actualName already has a corresponding
209     * actual, then use that, otherwise use actualName as is.  Add
210     * correspondence from formal (formalName) to actual (actualName).
211     */
212    for(i = 0 ; i < array_n(childActualIoArray) ; i++) {
213      Var_Variable_t *actualVar = array_fetch(Var_Variable_t *, childActualIoArray, i);
214      Var_Variable_t *formalVar = array_fetch(Var_Variable_t *, childFormalIoArray, i);
215
216      char *nodeName   = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
217      /* Special case the situation where hrcNode is current node. */
218      char *actualName = (strcmp(nodeName, ""))
219          ? util_strcat3(nodeName, ".",
220                         Var_VariableReadName(actualVar))
221          : util_strsav(Var_VariableReadName(actualVar));
222
223      char *childNodeName = Hrc_NodeFindHierarchicalName(childHrcNode, TRUE);
224      char *formalName = util_strcat3(childNodeName, ".",
225                                      Var_VariableReadName(formalVar));
226
227      /*
228       * It is correct to call this function with actualName.  We want to
229       * check if actualVar is itself a formalVar one level up.
230       */
231      char *tempName   = Ntk_NetworkReadActualNameFromFormalName(network, actualName);
232
233      FREE(nodeName);
234      FREE(childNodeName);
235
236      /*
237       * (tempName != NIL) => this net is a formal in hrcNode
238       */
239      if (tempName != NIL(char)) {
240        FREE(actualName);
241        actualName = tempName;
242      }
243
244      /*
245       * Ntk_NetworkInsertFormalNameToActualName makes copies of the strings
246       */
247      Ntk_NetworkInsertFormalNameToActualName(network, formalName, actualName);
248
249      if (tempName == NIL(char)) {
250        FREE(actualName);
251      }
252      FREE(formalName);
253    }
254    array_free(childFormalIoArray);
255    array_free(childActualIoArray);
256
257    /*
258     * Recurse.
259     */
260    NetworkBuildFormalToActualTableRecursively(network, childHrcNode);
261  }
262}
263
264
265/**Function********************************************************************
266
267  Synopsis    [Creates placeholders for all the nodes in the network.]
268
269  Description [Working top-down, creates placeholders for all the nodes in the
270  network.  After this function is executed, each node will have a name and
271  Var_Variable_t, but nothing else.  Note that nodes are created for reset
272  logic; they are given the name of their corresponding latch, suffixed by
273  $INIT.]
274
275  SideEffects []
276
277  SeeAlso     [NodeCreateAsNecessary]
278
279******************************************************************************/
280static void
281NetworkCreateNodesRecursively(
282  Ntk_Network_t *network,
283  Hrc_Node_t    *hrcNode)
284{
285  st_generator   *stGen;
286  Var_Variable_t *var;
287  Hrc_Latch_t    *latch;
288  char           *varName;
289  char           *latchName;
290  char           *childName;
291  Hrc_Node_t     *childHrcNode;
292  char           *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
293  char           *separator = (char *) ((strcmp(path, "")) ? "." : "");
294
295  /*
296   * The separator is used to handle the special case when hrcNode is the
297   * current node in the hierarchy.  If it is, we don't want a "." before the
298   * variable names.
299   */
300
301  Hrc_NodeForEachVariable(hrcNode, stGen, varName, var) {
302    char *nodeName = util_strcat3(path, separator, varName);
303    NodeCreateAsNecessary(network, nodeName, var);
304    FREE(nodeName);
305  }
306
307  /*
308   * Variable for reset is the same as for present state.  Hence, iterating
309   * through the list of variables gets us just the present state.  Therefore,
310   * we need to special case the reset (or init) nodes.
311   */
312  Hrc_NodeForEachLatch(hrcNode, stGen, latchName, latch) {
313    char *partialNodeName = util_strcat3(path, separator, latchName);
314    char *nodeName        = util_strcat3(partialNodeName, "$INIT", "");
315
316    FREE(partialNodeName);
317    NodeCreateAsNecessary(network, nodeName, Hrc_LatchReadOutput(latch));
318    FREE(nodeName);
319  }
320  FREE(path);
321
322  /* Recurse. */
323  Hrc_NodeForEachChild(hrcNode, stGen, childName, childHrcNode) {
324    NetworkCreateNodesRecursively(network, childHrcNode);
325  }
326}
327
328
329/**Function********************************************************************
330
331  Synopsis [Creates a node with a given name, if one doesn't already exist.]
332
333  Description [If a node with nodeName already exists in the network, then
334  does nothing.  Otherwise, creates a new node in the network with nodeName
335  and variable.]
336
337  SideEffects []
338
339******************************************************************************/
340static void
341NodeCreateAsNecessary(
342  Ntk_Network_t  *network,
343  char           *nodeName,
344  Var_Variable_t *var)
345{
346  if (Ntk_NetworkFindNodeByName(network, nodeName)) {
347    return;
348  }
349
350  (void) Ntk_NodeCreateInNetwork(network, nodeName, var);
351}
352
353
354/**Function********************************************************************
355
356  Synopsis    [Add functionality to the Ntk_Node_t's for this Hrc_Node_t.]
357
358  Description [Add functionality to the Ntk_Node_t's for this Hrc_Node_t.
359  Proceeds in 3 stages: 1) sets PI's and PO's; this is achieved by looking at
360  PI/POs which are not formals, 2) adds tables to combinational logic, taking
361  care to get the non-deterministic/deterministic constants right, 3) iterates
362  over latches, adding type latch to nodes which have a name correspoding to
363  this latch's ps name, and declaring the initialization logic for the
364  latch.<p>
365
366  If a table is found that is non-deterministic or incompletely specified,
367  then a message is written to vis_stderr, and FALSE is returned (the
368  non-deterministic test is not performed on non-deterministic constant
369  tables).  Also, if a table has no inputs and more than 1 output and its
370  output space is not complete, then it's declared a "relation", and FALSE is
371  returned.  However, even if FALSE is returned, the nodes are still
372  declared.<p>
373
374  The non-deterministic or incompletely specified tests can be bypassed by
375  passing FALSE for buildMvfs. See Ntk_HrcNodeConvertToNetwork for more info.]
376
377  SideEffects []
378
379******************************************************************************/
380static boolean
381NetworkDeclareNodesRecursively(
382  Ntk_Network_t *network,
383  Hrc_Node_t    *hrcNode,
384  boolean        buildMvfs,
385  mdd_manager  **mddMgr)
386{
387  int i;
388  st_generator   *stGen;
389  char           *latchName;
390  Var_Variable_t *var;
391  Hrc_Latch_t    *latch;
392  Tbl_Table_t    *table;
393  char           *childName;
394  Hrc_Node_t     *childHrcNode;
395  boolean         result = TRUE;
396  char           *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
397  char           *separator = (char *) ((strcmp(path, "")) ? "." : "");
398
399  /*
400   * First declare the network's PI/PO nodes.
401   */
402  NetworkDeclareIONodes(network, hrcNode);
403
404  /*
405   * Next, declare those nodes whose function is represented by a table.  Note
406   * that his iterator does not pick up those tables that define the
407   * initialization logic of latches.
408   */
409  Hrc_NodeForEachNameTable(hrcNode, i, table) {
410    int index;
411    Tbl_TableForEachOutputVar(table, index, var) {
412      boolean     status;
413      char       *fullVarName = util_strcat3(path, separator,
414                                               Var_VariableReadName(var));
415      Ntk_Node_t *node        = Ntk_NetworkFindNodeByName(network, fullVarName);
416
417      FREE(fullVarName);
418      status = NodeDeclareWithTable(node, table, index, path, buildMvfs, *mddMgr);
419      if (!status) {
420        result = FALSE;
421      }
422      MddManagerResetIfNecessary(mddMgr);
423    }
424  }
425
426  /*
427   * Declare each latch and its corresponding next state shadow node.
428   */
429  NetworkDeclareLatches(network, hrcNode);
430
431  /*
432   * Declare the "initial" node corresponding to each latch.
433   */
434  Hrc_NodeForEachLatch(hrcNode, stGen, latchName, latch) {
435    int index;
436
437    table = Hrc_LatchReadResetTable(latch);
438
439    /*
440     * There is only one output variable (the 0th output) for any table
441     * defining the initial function of a latch, but we use an iterator to get
442     * the variable for convenience.
443     */
444    Tbl_TableForEachOutputVar(table, index, var) {
445      boolean      status;
446      char        *fullVarName = util_strcat3(path, separator, Var_VariableReadName(var));
447      char        *initName    = util_strcat3(fullVarName, "$INIT", "");
448      Ntk_Node_t  *node        = Ntk_NetworkFindNodeByName(network, initName);
449
450      /*
451       * Since the output of this table corresponds to a latch PS, can get name
452       * of the initial node by attaching $INIT.
453       */
454      FREE(fullVarName);
455      FREE(initName);
456
457      status = NodeDeclareWithTable(node, table, index, path, buildMvfs, *mddMgr);
458      if (!status) {
459        result = FALSE;
460      }
461      MddManagerResetIfNecessary(mddMgr);
462    }
463  }
464  FREE(path);
465
466  /* Recurse. */
467  Hrc_NodeForEachChild(hrcNode, stGen, childName, childHrcNode) {
468    boolean status = NetworkDeclareNodesRecursively(network, childHrcNode,
469                                                    buildMvfs, mddMgr);
470    if (!status) {
471      result = FALSE;
472    }
473  }
474
475  return result;
476}
477
478
479/**Function********************************************************************
480
481  Synopsis    [Creates a new array consisting of array1 and array2.]
482
483  Description [Returns a new array which consists of the elements of array 1
484  followed by the elements of array2.]
485
486  Comment     [It is suspected that the array_join from the array package is
487  buggy when one of the arrays has 0 length.  Hence, we defined our own.]
488
489  SideEffects []
490
491******************************************************************************/
492static array_t *
493LocalArrayJoin(
494  array_t *array1,
495  array_t *array2)
496{
497  if (array_n(array1) == 0) {
498    return (array_dup(array2));
499  }
500  else if (array_n(array2) == 0) {
501    return (array_dup(array1));
502  }
503  else {
504    return (array_join(array1, array2));
505  }
506}
507
508
509/**Function********************************************************************
510
511  Synopsis    [Creates an array of table input names.]
512
513  Description [Creates an array of table input names.  For the ith input of
514  table, the string "namePrefix.variableName_i" is placed in the ith position
515  of the returned array, where variableName_i is the name of the variable
516  corresponding to the ith input.  (If namePrefix is "", then just
517  "variableName_i" is used.)  It is the responsiblity of the caller to free
518  the strings in the returned array.]
519
520  SideEffects []
521
522  SeeAlso     [NameArrayFree]
523
524******************************************************************************/
525static array_t *
526TableCreateFormalInputNameArray(
527  Tbl_Table_t *table,
528  char        *namePrefix)
529{
530  int             index;
531  array_t        *nameArray;
532  Var_Variable_t *var;
533  char           *separator = (char *) ((strcmp(namePrefix, "")) ? "." : "");
534
535  /*
536   * Allocate an array of length equal to the number of inputs of the table.
537   * Then, for each input, add the full path name of the input to the array.
538   */
539  nameArray = array_alloc(char *, Tbl_TableReadNumInputs(table));
540  Tbl_TableForEachInputVar(table, index, var) {
541    char *inputFullName = util_strcat3(namePrefix, separator, Var_VariableReadName(var));
542    array_insert(char *, nameArray, index, inputFullName);
543  }
544
545  return (nameArray);
546}
547
548
549/**Function********************************************************************
550
551  Synopsis    [Frees the strings in an array, and frees the array itself.]
552
553  SideEffects []
554
555  SeeAlso     [TableCreateFormalInputNameArray]
556
557******************************************************************************/
558static void
559NameArrayFree(
560  array_t *nameArray)
561{
562  int i;
563
564  for (i = 0; i < array_n(nameArray); i++) {
565    char *name = array_fetch(char *, nameArray, i);
566    FREE(name);
567  }
568  array_free(nameArray);
569}
570
571/**Function********************************************************************
572
573  Synopsis    [Abstract each node named in abstractedNames.]
574
575  Description [Abstract each node named in abstractedNames. A node x is
576  abstracted by creating a single new primary input node, with the name x$ABS
577  and with the same variable as x, which will fanout to every node the
578  original node fanned out to. The old node will continue to exists as before
579  but will have no fanouts after abstraction; it can still be referred to in
580  CTL formulas, etc.]
581
582  SideEffects []
583
584******************************************************************************/
585static boolean
586NetworkAbstractNodes(
587  Ntk_Network_t *network,
588  lsList abstractedNames)
589{
590  char  *name;
591  lsGen gen;
592
593  /*
594   * For each abstracted name, cut the corresponding net, and introduce a new
595   * node.
596   */
597  lsForEachItem(abstractedNames, gen, name) {
598    Var_Variable_t *var;
599    Ntk_Node_t     *abstractNode;
600    array_t        *abstractNodeFanouts;
601    int             i;
602    Ntk_Node_t     *fanout;
603    char           *abstractNodeName;
604    Ntk_Node_t     *node = Ntk_NetworkFindNodeByName(network, name);
605
606    /* Make sure the name corresponds to a node in the network. */
607    if (node == NIL(Ntk_Node_t)) {
608      error_append("Could not find node corresponding to name: ");
609      error_append(name);
610      error_append("\n");
611      return FALSE;
612    }
613
614    /* Create the new node in the network as a primary input. */
615    abstractNodeName = util_strcat3(name, "$ABS", "");
616    var = Ntk_NodeReadVariable(node);
617    abstractNode = Ntk_NodeCreateInNetwork(network, abstractNodeName, var);
618    FREE(abstractNodeName);
619    Ntk_NodeDeclareAsPrimaryInput(abstractNode);
620
621    /*
622     * For each fanout y of the node x being abstracted, replace x in y's
623     * fanin list by the new node, and add y to the fanout list of the new
624     * node.
625     */
626    abstractNodeFanouts = Ntk_NodeReadFanouts(abstractNode);
627    Ntk_NodeForEachFanout(node, i, fanout) {
628      int      index        = Ntk_NodeReadFaninIndex(fanout, node);
629      array_t *fanoutFanins = Ntk_NodeReadFanins(fanout);
630
631      array_insert(Ntk_Node_t *, fanoutFanins, index, abstractNode);
632      array_insert_last(Ntk_Node_t *, abstractNodeFanouts, fanout);
633    }
634
635    /*
636     * Replace the fanout array of the node being abstracted with an empty
637     * array.
638     */
639    array_free(node->fanouts);
640    node->fanouts = array_alloc(Ntk_Node_t *, 0);
641  }
642
643  return TRUE;
644}
645
646
647/**Function********************************************************************
648
649  Synopsis    [Declare a node with a table, and run some tests.]
650
651  Description [Declare a node with a table, and run some tests.  Creates the
652  MVF for the output of table denoted by outIndex, in terms of the table
653  inputs (new MDD variables are created).  This MVF is created within mddMgr,
654  and freed at the end of the function.  The MVF is checked to see if it
655  represents nondeterministic or incompletely specified behavior.  If it does,
656  a message is written to vis_stderr, and FALSE is returned.  Also, if a table
657  has no inputs and more than 1 output and its output space is not complete,
658  then it's declared a "relation", and FALSE is returned.<p>
659
660  If the table passes these tests, then a reduced table is built for this
661  table output, consisting of just that output and the input columns in the
662  support of that output.  The node is then declared as a "pseudo-input" if
663  the table represents a nondeterministic constant, or a "combinational" node
664  otherwise.<p>
665
666  Building the MVF, performing the tests, and building the reduced table, is
667  bypassed if the input buildMvfs is FALSE.  Note that this should be done with
668  extreme caution, because bad tables could inadvertantly be allowed through
669  and invalidate verification results obtained downstream.]
670
671  SideEffects []
672
673******************************************************************************/
674static boolean
675NodeDeclareWithTable(
676  Ntk_Node_t  *node,
677  Tbl_Table_t *table,
678  int          outIndex,
679  char        *path,
680  boolean      buildMvfs,
681  mdd_manager *mddMgr)
682{
683  Tbl_Table_t *newTable;
684  int          newOutIndex;
685  boolean      result   = TRUE;
686  char        *nodeName = Ntk_NodeReadName(node);
687
688  /*
689   * If table has no inputs and more than one output, and its output space is
690   * not complete (i.e. not all output minterms are present, so the outputs
691   * are correlated), then declare the table a relation.
692   */
693  if ((Tbl_TableReadNumInputs(table) == 0)
694      && (Tbl_TableReadNumOutputs(table) > 1)) {
695    if (!Tbl_TableTestIsOutputSpaceComplete(table, mddMgr)) {
696      (void) fprintf(vis_stderr, "Table %s is a relation\n", nodeName);
697      result = FALSE;
698    }
699  }
700
701  if (!buildMvfs) {
702    newTable = Tbl_TableSoftDup(table);
703    newOutIndex = outIndex;
704  }
705  else {
706    Mvf_Function_t *outMvf;
707    int             offset;
708    int             numInputs     = Tbl_TableReadNumInputs(table);
709    array_t        *varMap        = array_alloc(int, numInputs);
710
711    outMvf = LocalMvfFunctionForTable(table, outIndex, mddMgr,
712                                      varMap, &offset);
713    /*
714     * If the function is not a non-deterministic constant, or it has some
715     * inputs, then check that it is deterministic. Always check that it is
716     * completely specified.
717     */
718    if ((numInputs > 0)
719        || !Mvf_FunctionTestIsNonDeterministicConstant(outMvf)) {
720      if (!Mvf_FunctionTestIsDeterministic(outMvf)) {
721        (void) fprintf(vis_stderr, "Table %s is not deterministic\n", nodeName);
722        result = FALSE;
723      }
724    }
725    if (!Mvf_FunctionTestIsCompletelySpecified(outMvf)) {
726      (void) fprintf(vis_stderr, "Table %s is not completely specified\n", nodeName);
727      result = FALSE;
728    }
729
730    /*
731     * Build the reduced table for the output corresponding to outIndex.  The
732     * reduced table will have only one output column (column 0), and will have
733     * only those input columns corresponding to the variables appearing in the
734     * support of outMvf.
735     */
736    newTable = Tbl_TableCreateTrueSupportTableForOutput(table, outMvf, mddMgr,
737                                                        offset, outIndex,
738                                                        varMap);
739    newOutIndex = 0;
740    array_free(varMap);
741    Mvf_FunctionFree(outMvf);
742  }
743
744
745  /*
746   * Declare the node with the reduced table.
747   */
748  if (Tbl_TableTestIsNonDeterministicConstant(newTable, newOutIndex)) {
749    Ntk_NodeDeclareAsPseudoInput(node, newTable, newOutIndex);
750  }
751  else {
752    array_t *formalInputNameArray = TableCreateFormalInputNameArray(newTable, path);
753
754    /* Ntk_NodeDeclareAsCombinational will test for constants. */
755    Ntk_NodeDeclareAsCombinational(node, newTable, formalInputNameArray, newOutIndex);
756    NameArrayFree(formalInputNameArray);
757  }
758
759  return result;
760}
761
762
763/**Function********************************************************************
764
765  Synopsis    [Declares the primary inputs and outputs of the network.]
766
767  Description [Declares the primary inputs and outputs of the network. Does
768  this by iterating over the variables of the hrcNode.  Any variable it finds
769  that doesn't have a corresponding actual name in the network's corresponding
770  formal-to-actual table is considered a primary IO.]
771
772  SideEffects []
773
774******************************************************************************/
775static void
776NetworkDeclareIONodes(
777  Ntk_Network_t *network,
778  Hrc_Node_t    *hrcNode)
779{
780  st_generator   *stGen;
781  char           *varName;
782  Var_Variable_t *var;
783  char           *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
784  char           *separator = (char *) ((strcmp(path, "")) ? "." : "");
785
786  Hrc_NodeForEachVariable(hrcNode, stGen, varName, var) {
787    if (Var_VariableTestIsPO(var) || Var_VariableTestIsPI(var)) {
788      char *fullVarName = util_strcat3(path, separator, Var_VariableReadName(var));
789      char *tmpName     = Ntk_NetworkReadActualNameFromFormalName(network, fullVarName);
790
791      /*
792       * If tmpName == NIL, this must be a PI/PO of the top most node in the hierarchy of
793       * nodes. Hence, this is a true input/output of the hierarchy.
794       */
795      if (tmpName == NIL(char)) {
796        Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, fullVarName);
797        if (Var_VariableTestIsPO(var)) {
798          Ntk_NodeDeclareAsPrimaryOutput(node);
799        }
800        else {
801          Ntk_NodeDeclareAsPrimaryInput(node);
802        }
803      }
804      FREE(fullVarName);
805    }
806  }
807  FREE(path);
808}
809
810
811/**Function********************************************************************
812
813  Synopsis    [Declares the latches of the network.]
814
815  Description [Declares the latches of the network. Does this by iterating
816  over the latches of the hrcNode.  For each latch, also creates and declares
817  a corresponding next state shadow node.]
818
819  SideEffects []
820
821******************************************************************************/
822static void
823NetworkDeclareLatches(
824  Ntk_Network_t *network,
825  Hrc_Node_t    *hrcNode)
826{
827  st_generator   *stGen;
828  char           *name;
829  Hrc_Latch_t    *latch;
830  char           *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
831  char           *separator = (char *) ((strcmp(path, "")) ? "." : "");
832
833  Hrc_NodeForEachLatch(hrcNode, stGen, name, latch) {
834    char       *nextStateName;
835    Ntk_Node_t *nextStateNode;
836    char       *latchName = util_strcat3(path, separator,
837                             Var_VariableReadName(Hrc_LatchReadOutput(latch)));
838    char       *initName  = util_strcat3(latchName, "$INIT", "");
839    char       *dataName  = util_strcat3(path, separator,
840                             Var_VariableReadName(Hrc_LatchReadInput(latch)));
841    Ntk_Node_t *latchNode = Ntk_NetworkFindNodeByName(network, latchName);
842
843    FREE(latchName);
844    Ntk_NodeDeclareAsLatch(latchNode, dataName, initName);
845    FREE(initName);
846    FREE(dataName);
847
848    /*
849     * Create the corresponding shadow next state node for the latch.  This holds
850     * the next state variable.
851     */
852    nextStateName = util_strcat3(Ntk_NodeReadName(latchNode), "$NS", "");
853    nextStateNode = Ntk_NodeCreateInNetwork(network, nextStateName,
854                                            Hrc_LatchReadOutput(latch));
855    FREE(nextStateName);
856    Ntk_NodeDeclareAsShadow(nextStateNode, latchNode);
857  }
858  FREE(path);
859}
860
861
862/**Function********************************************************************
863
864  Synopsis    [Potentially quits mddMgr and starts a new one.]
865
866  Description [Quits mddMgr if the number of binary variables exceeds
867  MAX_NUMBER_BDD_VARS, and starts a new manager with no variables.
868  Initializing an empty MDD manager is costly in some BDD packages, so we want
869  to avoid doing it often (say, once per table).  On the other hand, we don't
870  want the manager to have too many variables, because then reordering becomes
871  expensive.]
872
873  SideEffects []
874
875******************************************************************************/
876static void
877MddManagerResetIfNecessary(
878  mdd_manager **mddMgr)
879{
880  if (bdd_num_vars(*mddMgr) > MAX_NUMBER_BDD_VARS) {
881    mdd_quit(*mddMgr);
882    *mddMgr = mdd_init_empty();
883    bdd_dynamic_reordering(*mddMgr, BDD_REORDER_SIFT, BDD_REORDER_VERBOSITY_DEFAULT);
884  }
885}
886
887
888/**Function********************************************************************
889
890  Synopsis    [Builds the MVF of a table in terms of local variables.]
891
892  Description [Builds the MVF of a table in terms of local variables.  Also
893  computes the offset of the local variables in the MDD manager and builds
894  a map from the input columns of the table to the MDD id's.  The offset is
895  always 0 if the MDD manager is restarted.]
896
897  SideEffects [varMap and offsetPtr are returned as side effects]
898
899******************************************************************************/
900static Mvf_Function_t *
901LocalMvfFunctionForTable(
902  Tbl_Table_t *table,
903  int outIndex,
904  mdd_manager *mddMgr,
905  array_t *varMap,
906  int *offsetPtr
907  )
908{
909  Mvf_Function_t *outMvf;
910  Var_Variable_t *var;
911  int             colNum;
912  int             offset;
913  int             i;
914  int             numInputs     = Tbl_TableReadNumInputs(table);
915  array_t        *faninMvfArray = array_alloc(Mvf_Function_t *, numInputs);
916  array_t        *mvarValues    = array_alloc(int, numInputs);
917  st_table       *varTable      = st_init_table(st_ptrcmp,st_ptrhash);
918
919  /* Create MDD variables for the table inputs.  If there are more inputs
920   * tied to the sameVar_Variable_t, create just one MDD variable.  Record
921   * the mapping from inputs to variable indices in varMap.
922   */
923  Tbl_TableForEachInputVar(table, colNum, var) {
924    int index;
925    if (st_lookup_int(varTable,var,&index)) {
926      array_insert_last(int, varMap, index);
927    } else {
928      index = array_n(mvarValues);
929      array_insert_last(int, varMap, index);
930      st_insert(varTable, var, (char *) (long) index);
931      array_insert_last(int, mvarValues, Var_VariableReadNumValues(var));
932    }
933  }
934  st_free_table(varTable);
935
936  /* Restarting the manager is optional.  The effect is to get rid of the
937   * MDD variable information in the manager, without incurring the cost
938   * of quitting and re-initializing the manager. */
939  mdd_restart(mddMgr);
940  offset = array_n(mdd_ret_mvar_list(mddMgr));  /* number of existing mvars */
941  assert(offset == 0);
942  mdd_create_variables(mddMgr, mvarValues, NIL(array_t), NIL(array_t));
943  array_free(mvarValues);
944
945  /*
946   * Construct an MVF for each table input. The MVF for column i is the MVF
947   * for MDD variable i.
948   */
949  for (i = 0; i < numInputs; i++) {
950    int index = array_fetch(int, varMap, i);
951    Mvf_Function_t *faninMvf = Mvf_FunctionCreateFromVariable(mddMgr, (index + offset));
952    array_insert_last(Mvf_Function_t *, faninMvfArray, faninMvf);
953  }
954
955  /* Compute the MVF of the output indexed by outIndex. */
956  outMvf = Tbl_TableBuildMvfFromFanins(table, outIndex, faninMvfArray, mddMgr);
957  Mvf_FunctionArrayFree(faninMvfArray);
958
959  *offsetPtr = offset;
960  return outMvf;
961
962} /* LocalMvfFunctionForTable */
Note: See TracBrowser for help on using the repository browser.