#include "ntkInt.h"
Include dependency graph for ntkFlt.c:
Go to the source code of this file.
Defines | |
| #define | MAX_NUMBER_BDD_VARS 500 |
Functions | |
| static void | NetworkBuildFormalToActualTableRecursively (Ntk_Network_t *network, Hrc_Node_t *hrcNode) |
| static void | NetworkCreateNodesRecursively (Ntk_Network_t *network, Hrc_Node_t *hrcNode) |
| static void | NodeCreateAsNecessary (Ntk_Network_t *network, char *nodeName, Var_Variable_t *var) |
| static boolean | NetworkDeclareNodesRecursively (Ntk_Network_t *network, Hrc_Node_t *hrcNode, boolean buildMvfs, mdd_manager **mddMgr) |
| static array_t * | LocalArrayJoin (array_t *array1, array_t *array2) |
| static array_t * | TableCreateFormalInputNameArray (Tbl_Table_t *table, char *namePrefix) |
| static void | NameArrayFree (array_t *nameArray) |
| static boolean | NetworkAbstractNodes (Ntk_Network_t *network, lsList abstractedNames) |
| static boolean | NodeDeclareWithTable (Ntk_Node_t *node, Tbl_Table_t *table, int outIndex, char *path, boolean buildMvfs, mdd_manager *mddMgr) |
| static void | NetworkDeclareIONodes (Ntk_Network_t *network, Hrc_Node_t *hrcNode) |
| static void | NetworkDeclareLatches (Ntk_Network_t *network, Hrc_Node_t *hrcNode) |
| static void | MddManagerResetIfNecessary (mdd_manager **mddMgr) |
| static Mvf_Function_t * | LocalMvfFunctionForTable (Tbl_Table_t *table, int outIndex, mdd_manager *mddMgr, array_t *varMap, int *offset) |
| Ntk_Network_t * | Ntk_HrcNodeConvertToNetwork (Hrc_Node_t *hrcNode, boolean buildMvfs, lsList abstractedNames) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: ntkFlt.c,v 1.13 2009/04/11 22:17:58 fabio Exp $" |
Define Documentation
Function Documentation
| static array_t * LocalArrayJoin | ( | array_t * | array1, |
| array_t * | array2 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Creates a new array consisting of array1 and array2.]
Description [Returns a new array which consists of the elements of array 1 followed by the elements of array2.]
Comment [It is suspected that the array_join from the array package is buggy when one of the arrays has 0 length. Hence, we defined our own.]
SideEffects []
Definition at line 493 of file ntkFlt.c.
{
if (array_n(array1) == 0) {
return (array_dup(array2));
}
else if (array_n(array2) == 0) {
return (array_dup(array1));
}
else {
return (array_join(array1, array2));
}
}
Here is the caller graph for this function:
| static Mvf_Function_t * LocalMvfFunctionForTable | ( | Tbl_Table_t * | table, |
| int | outIndex, | ||
| mdd_manager * | mddMgr, | ||
| array_t * | varMap, | ||
| int * | offsetPtr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Builds the MVF of a table in terms of local variables.]
Description [Builds the MVF of a table in terms of local variables. Also computes the offset of the local variables in the MDD manager and builds a map from the input columns of the table to the MDD id's. The offset is always 0 if the MDD manager is restarted.]
SideEffects [varMap and offsetPtr are returned as side effects]
Definition at line 901 of file ntkFlt.c.
{
Mvf_Function_t *outMvf;
Var_Variable_t *var;
int colNum;
int offset;
int i;
int numInputs = Tbl_TableReadNumInputs(table);
array_t *faninMvfArray = array_alloc(Mvf_Function_t *, numInputs);
array_t *mvarValues = array_alloc(int, numInputs);
st_table *varTable = st_init_table(st_ptrcmp,st_ptrhash);
/* Create MDD variables for the table inputs. If there are more inputs
* tied to the sameVar_Variable_t, create just one MDD variable. Record
* the mapping from inputs to variable indices in varMap.
*/
Tbl_TableForEachInputVar(table, colNum, var) {
int index;
if (st_lookup_int(varTable,var,&index)) {
array_insert_last(int, varMap, index);
} else {
index = array_n(mvarValues);
array_insert_last(int, varMap, index);
st_insert(varTable, var, (char *) (long) index);
array_insert_last(int, mvarValues, Var_VariableReadNumValues(var));
}
}
st_free_table(varTable);
/* Restarting the manager is optional. The effect is to get rid of the
* MDD variable information in the manager, without incurring the cost
* of quitting and re-initializing the manager. */
mdd_restart(mddMgr);
offset = array_n(mdd_ret_mvar_list(mddMgr)); /* number of existing mvars */
assert(offset == 0);
mdd_create_variables(mddMgr, mvarValues, NIL(array_t), NIL(array_t));
array_free(mvarValues);
/*
* Construct an MVF for each table input. The MVF for column i is the MVF
* for MDD variable i.
*/
for (i = 0; i < numInputs; i++) {
int index = array_fetch(int, varMap, i);
Mvf_Function_t *faninMvf = Mvf_FunctionCreateFromVariable(mddMgr, (index + offset));
array_insert_last(Mvf_Function_t *, faninMvfArray, faninMvf);
}
/* Compute the MVF of the output indexed by outIndex. */
outMvf = Tbl_TableBuildMvfFromFanins(table, outIndex, faninMvfArray, mddMgr);
Mvf_FunctionArrayFree(faninMvfArray);
*offsetPtr = offset;
return outMvf;
} /* LocalMvfFunctionForTable */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void MddManagerResetIfNecessary | ( | mdd_manager ** | mddMgr | ) | [static] |
Function********************************************************************
Synopsis [Potentially quits mddMgr and starts a new one.]
Description [Quits mddMgr if the number of binary variables exceeds MAX_NUMBER_BDD_VARS, and starts a new manager with no variables. Initializing an empty MDD manager is costly in some BDD packages, so we want to avoid doing it often (say, once per table). On the other hand, we don't want the manager to have too many variables, because then reordering becomes expensive.]
SideEffects []
Definition at line 877 of file ntkFlt.c.
{
if (bdd_num_vars(*mddMgr) > MAX_NUMBER_BDD_VARS) {
mdd_quit(*mddMgr);
*mddMgr = mdd_init_empty();
bdd_dynamic_reordering(*mddMgr, BDD_REORDER_SIFT, BDD_REORDER_VERBOSITY_DEFAULT);
}
}
Here is the caller graph for this function:
| static void NameArrayFree | ( | array_t * | nameArray | ) | [static] |
Function********************************************************************
Synopsis [Frees the strings in an array, and frees the array itself.]
SideEffects []
SeeAlso [TableCreateFormalInputNameArray]
Definition at line 559 of file ntkFlt.c.
{
int i;
for (i = 0; i < array_n(nameArray); i++) {
char *name = array_fetch(char *, nameArray, i);
FREE(name);
}
array_free(nameArray);
}
Here is the caller graph for this function:
| static boolean NetworkAbstractNodes | ( | Ntk_Network_t * | network, |
| lsList | abstractedNames | ||
| ) | [static] |
Function********************************************************************
Synopsis [Abstract each node named in abstractedNames.]
Description [Abstract each node named in abstractedNames. A node x is abstracted by creating a single new primary input node, with the name x$ABS and with the same variable as x, which will fanout to every node the original node fanned out to. The old node will continue to exists as before but will have no fanouts after abstraction; it can still be referred to in CTL formulas, etc.]
SideEffects []
Definition at line 586 of file ntkFlt.c.
{
char *name;
lsGen gen;
/*
* For each abstracted name, cut the corresponding net, and introduce a new
* node.
*/
lsForEachItem(abstractedNames, gen, name) {
Var_Variable_t *var;
Ntk_Node_t *abstractNode;
array_t *abstractNodeFanouts;
int i;
Ntk_Node_t *fanout;
char *abstractNodeName;
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, name);
/* Make sure the name corresponds to a node in the network. */
if (node == NIL(Ntk_Node_t)) {
error_append("Could not find node corresponding to name: ");
error_append(name);
error_append("\n");
return FALSE;
}
/* Create the new node in the network as a primary input. */
abstractNodeName = util_strcat3(name, "$ABS", "");
var = Ntk_NodeReadVariable(node);
abstractNode = Ntk_NodeCreateInNetwork(network, abstractNodeName, var);
FREE(abstractNodeName);
Ntk_NodeDeclareAsPrimaryInput(abstractNode);
/*
* For each fanout y of the node x being abstracted, replace x in y's
* fanin list by the new node, and add y to the fanout list of the new
* node.
*/
abstractNodeFanouts = Ntk_NodeReadFanouts(abstractNode);
Ntk_NodeForEachFanout(node, i, fanout) {
int index = Ntk_NodeReadFaninIndex(fanout, node);
array_t *fanoutFanins = Ntk_NodeReadFanins(fanout);
array_insert(Ntk_Node_t *, fanoutFanins, index, abstractNode);
array_insert_last(Ntk_Node_t *, abstractNodeFanouts, fanout);
}
/*
* Replace the fanout array of the node being abstracted with an empty
* array.
*/
array_free(node->fanouts);
node->fanouts = array_alloc(Ntk_Node_t *, 0);
}
return TRUE;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void NetworkBuildFormalToActualTableRecursively | ( | Ntk_Network_t * | network, |
| Hrc_Node_t * | hrcNode | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Creates mapping from formal names to actual names.]
Description [Loads the formal-to-actual table of network. For each formal variable name in hrcNode, maps it to a unique actual variable name. The map is many-to-one. The rule is that a formal is resolved to the actual as high in the hierarchy as possible. Proceeds recursively by examining subcircuits. Note that only formals are in the domain of the map. Also, care has to be taken when looking at net in parent since they may also be formals.]
SideEffects []
Definition at line 181 of file ntkFlt.c.
{
st_generator *stGen;
char *childName;
Hrc_Node_t *childHrcNode;
/*
* For each child of the current hnode, process its I/O variables, and
* then recurse on its children.
*/
Hrc_NodeForEachChild(hrcNode, stGen, childName, childHrcNode) {
int i;
array_t *childFormalInputs = Hrc_NodeReadFormalInputs(childHrcNode);
array_t *childFormalOutputs = Hrc_NodeReadFormalOutputs(childHrcNode);
array_t *childFormalIoArray = LocalArrayJoin(childFormalInputs, childFormalOutputs);
array_t *childActualInputs = Hrc_NodeReadActualInputs(childHrcNode);
array_t *childActualOutputs = Hrc_NodeReadActualOutputs(childHrcNode);
array_t *childActualIoArray = LocalArrayJoin(childActualInputs, childActualOutputs);
/*
* For each I/O variable, construct the appropriate hierarchical name for
* the variable in childHrcNode (formalName) and the variable in the
* hrcNode (actualName). If actualName already has a corresponding
* actual, then use that, otherwise use actualName as is. Add
* correspondence from formal (formalName) to actual (actualName).
*/
for(i = 0 ; i < array_n(childActualIoArray) ; i++) {
Var_Variable_t *actualVar = array_fetch(Var_Variable_t *, childActualIoArray, i);
Var_Variable_t *formalVar = array_fetch(Var_Variable_t *, childFormalIoArray, i);
char *nodeName = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
/* Special case the situation where hrcNode is current node. */
char *actualName = (strcmp(nodeName, ""))
? util_strcat3(nodeName, ".",
Var_VariableReadName(actualVar))
: util_strsav(Var_VariableReadName(actualVar));
char *childNodeName = Hrc_NodeFindHierarchicalName(childHrcNode, TRUE);
char *formalName = util_strcat3(childNodeName, ".",
Var_VariableReadName(formalVar));
/*
* It is correct to call this function with actualName. We want to
* check if actualVar is itself a formalVar one level up.
*/
char *tempName = Ntk_NetworkReadActualNameFromFormalName(network, actualName);
FREE(nodeName);
FREE(childNodeName);
/*
* (tempName != NIL) => this net is a formal in hrcNode
*/
if (tempName != NIL(char)) {
FREE(actualName);
actualName = tempName;
}
/*
* Ntk_NetworkInsertFormalNameToActualName makes copies of the strings
*/
Ntk_NetworkInsertFormalNameToActualName(network, formalName, actualName);
if (tempName == NIL(char)) {
FREE(actualName);
}
FREE(formalName);
}
array_free(childFormalIoArray);
array_free(childActualIoArray);
/*
* Recurse.
*/
NetworkBuildFormalToActualTableRecursively(network, childHrcNode);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void NetworkCreateNodesRecursively | ( | Ntk_Network_t * | network, |
| Hrc_Node_t * | hrcNode | ||
| ) | [static] |
Function********************************************************************
Synopsis [Creates placeholders for all the nodes in the network.]
Description [Working top-down, creates placeholders for all the nodes in the network. After this function is executed, each node will have a name and Var_Variable_t, but nothing else. Note that nodes are created for reset logic; they are given the name of their corresponding latch, suffixed by $INIT.]
SideEffects []
SeeAlso [NodeCreateAsNecessary]
Definition at line 281 of file ntkFlt.c.
{
st_generator *stGen;
Var_Variable_t *var;
Hrc_Latch_t *latch;
char *varName;
char *latchName;
char *childName;
Hrc_Node_t *childHrcNode;
char *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
char *separator = (char *) ((strcmp(path, "")) ? "." : "");
/*
* The separator is used to handle the special case when hrcNode is the
* current node in the hierarchy. If it is, we don't want a "." before the
* variable names.
*/
Hrc_NodeForEachVariable(hrcNode, stGen, varName, var) {
char *nodeName = util_strcat3(path, separator, varName);
NodeCreateAsNecessary(network, nodeName, var);
FREE(nodeName);
}
/*
* Variable for reset is the same as for present state. Hence, iterating
* through the list of variables gets us just the present state. Therefore,
* we need to special case the reset (or init) nodes.
*/
Hrc_NodeForEachLatch(hrcNode, stGen, latchName, latch) {
char *partialNodeName = util_strcat3(path, separator, latchName);
char *nodeName = util_strcat3(partialNodeName, "$INIT", "");
FREE(partialNodeName);
NodeCreateAsNecessary(network, nodeName, Hrc_LatchReadOutput(latch));
FREE(nodeName);
}
FREE(path);
/* Recurse. */
Hrc_NodeForEachChild(hrcNode, stGen, childName, childHrcNode) {
NetworkCreateNodesRecursively(network, childHrcNode);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void NetworkDeclareIONodes | ( | Ntk_Network_t * | network, |
| Hrc_Node_t * | hrcNode | ||
| ) | [static] |
Function********************************************************************
Synopsis [Declares the primary inputs and outputs of the network.]
Description [Declares the primary inputs and outputs of the network. Does this by iterating over the variables of the hrcNode. Any variable it finds that doesn't have a corresponding actual name in the network's corresponding formal-to-actual table is considered a primary IO.]
SideEffects []
Definition at line 776 of file ntkFlt.c.
{
st_generator *stGen;
char *varName;
Var_Variable_t *var;
char *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
char *separator = (char *) ((strcmp(path, "")) ? "." : "");
Hrc_NodeForEachVariable(hrcNode, stGen, varName, var) {
if (Var_VariableTestIsPO(var) || Var_VariableTestIsPI(var)) {
char *fullVarName = util_strcat3(path, separator, Var_VariableReadName(var));
char *tmpName = Ntk_NetworkReadActualNameFromFormalName(network, fullVarName);
/*
* If tmpName == NIL, this must be a PI/PO of the top most node in the hierarchy of
* nodes. Hence, this is a true input/output of the hierarchy.
*/
if (tmpName == NIL(char)) {
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, fullVarName);
if (Var_VariableTestIsPO(var)) {
Ntk_NodeDeclareAsPrimaryOutput(node);
}
else {
Ntk_NodeDeclareAsPrimaryInput(node);
}
}
FREE(fullVarName);
}
}
FREE(path);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void NetworkDeclareLatches | ( | Ntk_Network_t * | network, |
| Hrc_Node_t * | hrcNode | ||
| ) | [static] |
Function********************************************************************
Synopsis [Declares the latches of the network.]
Description [Declares the latches of the network. Does this by iterating over the latches of the hrcNode. For each latch, also creates and declares a corresponding next state shadow node.]
SideEffects []
Definition at line 823 of file ntkFlt.c.
{
st_generator *stGen;
char *name;
Hrc_Latch_t *latch;
char *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
char *separator = (char *) ((strcmp(path, "")) ? "." : "");
Hrc_NodeForEachLatch(hrcNode, stGen, name, latch) {
char *nextStateName;
Ntk_Node_t *nextStateNode;
char *latchName = util_strcat3(path, separator,
Var_VariableReadName(Hrc_LatchReadOutput(latch)));
char *initName = util_strcat3(latchName, "$INIT", "");
char *dataName = util_strcat3(path, separator,
Var_VariableReadName(Hrc_LatchReadInput(latch)));
Ntk_Node_t *latchNode = Ntk_NetworkFindNodeByName(network, latchName);
FREE(latchName);
Ntk_NodeDeclareAsLatch(latchNode, dataName, initName);
FREE(initName);
FREE(dataName);
/*
* Create the corresponding shadow next state node for the latch. This holds
* the next state variable.
*/
nextStateName = util_strcat3(Ntk_NodeReadName(latchNode), "$NS", "");
nextStateNode = Ntk_NodeCreateInNetwork(network, nextStateName,
Hrc_LatchReadOutput(latch));
FREE(nextStateName);
Ntk_NodeDeclareAsShadow(nextStateNode, latchNode);
}
FREE(path);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static boolean NetworkDeclareNodesRecursively | ( | Ntk_Network_t * | network, |
| Hrc_Node_t * | hrcNode, | ||
| boolean | buildMvfs, | ||
| mdd_manager ** | mddMgr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Add functionality to the Ntk_Node_t's for this Hrc_Node_t.]
Description [Add functionality to the Ntk_Node_t's for this Hrc_Node_t. Proceeds in 3 stages: 1) sets PI's and PO's; this is achieved by looking at PI/POs which are not formals, 2) adds tables to combinational logic, taking care to get the non-deterministic/deterministic constants right, 3) iterates over latches, adding type latch to nodes which have a name correspoding to this latch's ps name, and declaring the initialization logic for the latch.
If a table is found that is non-deterministic or incompletely specified, then a message is written to vis_stderr, and FALSE is returned (the non-deterministic test is not performed on non-deterministic constant tables). Also, if a table has no inputs and more than 1 output and its output space is not complete, then it's declared a "relation", and FALSE is returned. However, even if FALSE is returned, the nodes are still declared.
The non-deterministic or incompletely specified tests can be bypassed by passing FALSE for buildMvfs. See Ntk_HrcNodeConvertToNetwork for more info.]
SideEffects []
Definition at line 381 of file ntkFlt.c.
{
int i;
st_generator *stGen;
char *latchName;
Var_Variable_t *var;
Hrc_Latch_t *latch;
Tbl_Table_t *table;
char *childName;
Hrc_Node_t *childHrcNode;
boolean result = TRUE;
char *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
char *separator = (char *) ((strcmp(path, "")) ? "." : "");
/*
* First declare the network's PI/PO nodes.
*/
NetworkDeclareIONodes(network, hrcNode);
/*
* Next, declare those nodes whose function is represented by a table. Note
* that his iterator does not pick up those tables that define the
* initialization logic of latches.
*/
Hrc_NodeForEachNameTable(hrcNode, i, table) {
int index;
Tbl_TableForEachOutputVar(table, index, var) {
boolean status;
char *fullVarName = util_strcat3(path, separator,
Var_VariableReadName(var));
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, fullVarName);
FREE(fullVarName);
status = NodeDeclareWithTable(node, table, index, path, buildMvfs, *mddMgr);
if (!status) {
result = FALSE;
}
MddManagerResetIfNecessary(mddMgr);
}
}
/*
* Declare each latch and its corresponding next state shadow node.
*/
NetworkDeclareLatches(network, hrcNode);
/*
* Declare the "initial" node corresponding to each latch.
*/
Hrc_NodeForEachLatch(hrcNode, stGen, latchName, latch) {
int index;
table = Hrc_LatchReadResetTable(latch);
/*
* There is only one output variable (the 0th output) for any table
* defining the initial function of a latch, but we use an iterator to get
* the variable for convenience.
*/
Tbl_TableForEachOutputVar(table, index, var) {
boolean status;
char *fullVarName = util_strcat3(path, separator, Var_VariableReadName(var));
char *initName = util_strcat3(fullVarName, "$INIT", "");
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, initName);
/*
* Since the output of this table corresponds to a latch PS, can get name
* of the initial node by attaching $INIT.
*/
FREE(fullVarName);
FREE(initName);
status = NodeDeclareWithTable(node, table, index, path, buildMvfs, *mddMgr);
if (!status) {
result = FALSE;
}
MddManagerResetIfNecessary(mddMgr);
}
}
FREE(path);
/* Recurse. */
Hrc_NodeForEachChild(hrcNode, stGen, childName, childHrcNode) {
boolean status = NetworkDeclareNodesRecursively(network, childHrcNode,
buildMvfs, mddMgr);
if (!status) {
result = FALSE;
}
}
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void NodeCreateAsNecessary | ( | Ntk_Network_t * | network, |
| char * | nodeName, | ||
| Var_Variable_t * | var | ||
| ) | [static] |
Function********************************************************************
Synopsis [Creates a node with a given name, if one doesn't already exist.]
Description [If a node with nodeName already exists in the network, then does nothing. Otherwise, creates a new node in the network with nodeName and variable.]
SideEffects []
Definition at line 341 of file ntkFlt.c.
{
if (Ntk_NetworkFindNodeByName(network, nodeName)) {
return;
}
(void) Ntk_NodeCreateInNetwork(network, nodeName, var);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static boolean NodeDeclareWithTable | ( | Ntk_Node_t * | node, |
| Tbl_Table_t * | table, | ||
| int | outIndex, | ||
| char * | path, | ||
| boolean | buildMvfs, | ||
| mdd_manager * | mddMgr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Declare a node with a table, and run some tests.]
Description [Declare a node with a table, and run some tests. Creates the MVF for the output of table denoted by outIndex, in terms of the table inputs (new MDD variables are created). This MVF is created within mddMgr, and freed at the end of the function. The MVF is checked to see if it represents nondeterministic or incompletely specified behavior. If it does, a message is written to vis_stderr, and FALSE is returned. Also, if a table has no inputs and more than 1 output and its output space is not complete, then it's declared a "relation", and FALSE is returned.
If the table passes these tests, then a reduced table is built for this table output, consisting of just that output and the input columns in the support of that output. The node is then declared as a "pseudo-input" if the table represents a nondeterministic constant, or a "combinational" node otherwise.
Building the MVF, performing the tests, and building the reduced table, is bypassed if the input buildMvfs is FALSE. Note that this should be done with extreme caution, because bad tables could inadvertantly be allowed through and invalidate verification results obtained downstream.]
SideEffects []
Definition at line 675 of file ntkFlt.c.
{
Tbl_Table_t *newTable;
int newOutIndex;
boolean result = TRUE;
char *nodeName = Ntk_NodeReadName(node);
/*
* If table has no inputs and more than one output, and its output space is
* not complete (i.e. not all output minterms are present, so the outputs
* are correlated), then declare the table a relation.
*/
if ((Tbl_TableReadNumInputs(table) == 0)
&& (Tbl_TableReadNumOutputs(table) > 1)) {
if (!Tbl_TableTestIsOutputSpaceComplete(table, mddMgr)) {
(void) fprintf(vis_stderr, "Table %s is a relation\n", nodeName);
result = FALSE;
}
}
if (!buildMvfs) {
newTable = Tbl_TableSoftDup(table);
newOutIndex = outIndex;
}
else {
Mvf_Function_t *outMvf;
int offset;
int numInputs = Tbl_TableReadNumInputs(table);
array_t *varMap = array_alloc(int, numInputs);
outMvf = LocalMvfFunctionForTable(table, outIndex, mddMgr,
varMap, &offset);
/*
* If the function is not a non-deterministic constant, or it has some
* inputs, then check that it is deterministic. Always check that it is
* completely specified.
*/
if ((numInputs > 0)
|| !Mvf_FunctionTestIsNonDeterministicConstant(outMvf)) {
if (!Mvf_FunctionTestIsDeterministic(outMvf)) {
(void) fprintf(vis_stderr, "Table %s is not deterministic\n", nodeName);
result = FALSE;
}
}
if (!Mvf_FunctionTestIsCompletelySpecified(outMvf)) {
(void) fprintf(vis_stderr, "Table %s is not completely specified\n", nodeName);
result = FALSE;
}
/*
* Build the reduced table for the output corresponding to outIndex. The
* reduced table will have only one output column (column 0), and will have
* only those input columns corresponding to the variables appearing in the
* support of outMvf.
*/
newTable = Tbl_TableCreateTrueSupportTableForOutput(table, outMvf, mddMgr,
offset, outIndex,
varMap);
newOutIndex = 0;
array_free(varMap);
Mvf_FunctionFree(outMvf);
}
/*
* Declare the node with the reduced table.
*/
if (Tbl_TableTestIsNonDeterministicConstant(newTable, newOutIndex)) {
Ntk_NodeDeclareAsPseudoInput(node, newTable, newOutIndex);
}
else {
array_t *formalInputNameArray = TableCreateFormalInputNameArray(newTable, path);
/* Ntk_NodeDeclareAsCombinational will test for constants. */
Ntk_NodeDeclareAsCombinational(node, newTable, formalInputNameArray, newOutIndex);
NameArrayFree(formalInputNameArray);
}
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Ntk_Network_t* Ntk_HrcNodeConvertToNetwork | ( | Hrc_Node_t * | hrcNode, |
| boolean | buildMvfs, | ||
| lsList | abstractedNames | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Builds a flat description of a subtree of hierarchy manager.]
Description [Builds a flat description of a subtree of a hierarchy manager. The flattened names of variables are taken as those hierarchical names where the variables are defined. The names are relative to the "current" node of the hierarchy manager, which can be set by calling Hrc_ManagerSetCurrentNode() first. Nodes are created even for unused variables (i.e. variables that don't fanout to anything.)
AbstractedNames is a list of char*. If the list is not NULL, then this list is interpreted as a list of variables to abstract. If a given name in the list does not correspond to the hierarchical name of a node in the network, then NULL is returned, and an error message is written to error_string. Otherwise, a new primary input is created to drive the net identified by the variable name. See the documentation for the command flatten_hierarchy for more information.
The verification routines assume deterministic and completely specified tables. If a table is found that is locally non-deterministic or incompletely specified, then a message is written to vis_stderr, and a NIL network is returned (the non-deterministic test is not performed on non-deterministic constant tables). This test can be bypassed (in order to save time) by passing FALSE for buildMvfs. Note that this should be done with extreme caution, because bad tables could inadvertantly be allowed through and invalidate verification results obtained downstream.
Also, if a table has no inputs and more than 1 output, and its output space is not complete (i.e. the outputs are correlated), then the table is declared a "relation", and NIL is returned.]
SideEffects []
Comment [Proceeds in 3 phases: 1) builds a map from formals to actuals, 2) adds a node for each actual (i.e. for each node that will appear in the network) and 3) sets the types (and tables, where appropriate) for each node.]
SeeAlso [Ntk_NetworkAlloc NetworkBuildFormalToActualTableRecursively NetworkCreateNodesRecursively NetworkDeclareNodesRecursively]
Definition at line 118 of file ntkFlt.c.
{
mdd_manager *mddMgr;
boolean status1 = TRUE;
boolean status2 = TRUE;
char *hrcNodeName = Hrc_NodeReadInstanceName(hrcNode);
Ntk_Network_t *network = Ntk_NetworkAlloc(hrcNodeName);
NetworkBuildFormalToActualTableRecursively(network, hrcNode);
NetworkCreateNodesRecursively(network, hrcNode);
/*
* The MDD manager is for building temporary MDDs. For robustness, enable
* reordering.
*/
mddMgr = mdd_init_empty();
bdd_dynamic_reordering(mddMgr, BDD_REORDER_SIFT, BDD_REORDER_VERBOSITY_DEFAULT);
status1 = NetworkDeclareNodesRecursively(network, hrcNode, buildMvfs, &mddMgr);
mdd_quit(mddMgr);
if (abstractedNames != (lsList) NULL) {
status2 = NetworkAbstractNodes(network, abstractedNames);
}
if (!(status1 && status2)) {
Ntk_NetworkFree(network);
return NIL(Ntk_Network_t);
}
else {
return network;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static array_t * TableCreateFormalInputNameArray | ( | Tbl_Table_t * | table, |
| char * | namePrefix | ||
| ) | [static] |
Function********************************************************************
Synopsis [Creates an array of table input names.]
Description [Creates an array of table input names. For the ith input of table, the string "namePrefix.variableName_i" is placed in the ith position of the returned array, where variableName_i is the name of the variable corresponding to the ith input. (If namePrefix is "", then just "variableName_i" is used.) It is the responsiblity of the caller to free the strings in the returned array.]
SideEffects []
SeeAlso [NameArrayFree]
Definition at line 526 of file ntkFlt.c.
{
int index;
array_t *nameArray;
Var_Variable_t *var;
char *separator = (char *) ((strcmp(namePrefix, "")) ? "." : "");
/*
* Allocate an array of length equal to the number of inputs of the table.
* Then, for each input, add the full path name of the input to the array.
*/
nameArray = array_alloc(char *, Tbl_TableReadNumInputs(table));
Tbl_TableForEachInputVar(table, index, var) {
char *inputFullName = util_strcat3(namePrefix, separator, Var_VariableReadName(var));
array_insert(char *, nameArray, index, inputFullName);
}
return (nameArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: ntkFlt.c,v 1.13 2009/04/11 22:17:58 fabio Exp $" [static] |
CFile***********************************************************************
FileName [ntkFlt.c]
PackageName [ntk]
Synopsis [Routines for creating a network from a hierarchy manager.]
Author [Adnan Aziz, Tom Shiple]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
