type | attributes
---------------+-------------------------------------------
| primary latch data latch init constant
| output input input
---------------+-------------------------------------------
pseudo input | x x x
primary input | x x x
latch | x x
shadow |
combinational | x x x x
Legend:
primary input: a node with no fanins that is a port of the network;
does not have a table defining its function - it can
take any value in its domain
pseudo input: a node with no fanins, introduced to model
nondeterminism; its table defines which values it can
take
latch: an edge triggered latch with data and initial inputs
shadow: a node with no fanins and no fanouts; it serves as a
"shadow" for a node; for example, a shadow node for a
latch is used to store information about the next
state variable; any node can have a shadow, except a
shadow node
combinational: a node that has a table and is not a primary or pseudo
input
primary output: a node that is a port of the network
latch data input: a node driving the data input of a latch
latch init input: a node driving the initial input of a latch
constant: a combinational node with no fanins that can take
exactly one value
An "x" in the table means that it's permissible for a node of the given type
to have the given attribute; the absence of an "x" means it's not
permissible.In addition, there are several derived attributes: all primary inputs, pseudo inputs, and latches are "combinational inputs"; all latch data inputs, latch initial inputs, and primary outputs are "combinational outputs"; all primary inputs and pseudo inputs are "inputs".
Each combinational node has a table defining the function of the node in terms of its immediate fanins. This function must be deterministic (i.e. for a given valuation of the fanins, the function can assume at most one value) and completely specified (i.e. for a given valuation of the fanins, the function can assume at least one value) in order to ensure correctness of verification results downstream . (The exception is that pseudo inputs are nondeterministic.) The table may have multiple output columns, so the node keeps an index giving the output column to which it refers.
The ntk package contains facilities to create a network (Ntk_Network_t) from a hierarchical network. In particular, it supports the concept of "actual names" and "formal names". Consider the following hierarchical network:
+--------------------+
| A |
| |
| +-----+ +----+ |
| | B | | C | |
| | | | | |
| | x | y | z | |
| | ---+----+-- | |
| | | | | |
| +-----+ +----+ |
| |
+--------------------+
This is meant to depict a block A that contains two blocks B and C. There
is a wire originating in block B, passing through block A, and terminating
in block C. This wire has three different names, A.y, A.B.x, and A.C.z,
depending on from which block it is viewed. When a hierarchical network is
flattened into a Ntk_Network_t, each node is assigned a unique name,
referred to as the "actual name". The actual name is the name with the
fewest levels of hierarchy in it (in this example, A.y). All other names
are referred to as "formal names" (in this example, A.B.x, and A.C.z). The
following functions deal with actual and formal names: Ntk_NodeReadName,
Ntk_NetworkFindNodeByActualName, Ntk_NetworkReadActualNameFromFormalName,
Ntk_NetworkInsertFormalNameToActualName, Ntk_NetworkFindNodeByName. See the
function descriptions for more details.A network may have an MDD manager associated with it, and the nodes may have MDD ids. However, the network itself does not keep track of any MDDs. This is the job of the partition package.] Author [Adnan Aziz, Tom Shiple] Comment [The authors would like to acknowledge the ideas of Olivier Coudert, Jean Christophe Madre, and Herve Touati on how to organize the network and node data structures, and functions.] 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.] Revision [$Id: ntk.h,v 1.24 2010/04/09 23:44:05 fabio Exp $] ******************************************************************************/ #ifndef _NTK #define _NTK /*---------------------------------------------------------------------------*/ /* Nested includes */ /*---------------------------------------------------------------------------*/ #include "var.h" #include "tbl.h" #include "hrc.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ #define NTK_UNASSIGNED_MDD_ID -1 #define NTK_UNASSIGNED_MAIG_ID -1 #define NTK_UNDEFINED_FANIN_INDEX -1 #define NTK_HRC_NODE_APPL_KEY "Ntk_HrcNodeApplKey" /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ typedef struct NtkNetworkStruct Ntk_Network_t; typedef struct NtkNodeStruct Ntk_Node_t; typedef void (*Ntk_ApplInfoFreeFn) (void *); /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**Macro*********************************************************************** Synopsis [Iterates over the fanins of a node.] Description [This macro iterates over the fanins of a node. It is an error to modify the fanins of a node while iterating its fanins.] SideEffects [This macro instantiates macros from the array package. Hence it is advisable not to nest this macro within array macros.] SeeAlso [Ntk_NodeForEachFanout] ******************************************************************************/ #define Ntk_NodeForEachFanin( \ /* Ntk_Node_t * */ node /* node to iterate fanins */, \ /* int */ i /* local variable for iterator */, \ /* Ntk_Node_t * */ fanin /* fanin of node */ \ ) \ arrayForEachItem(Ntk_Node_t *, Ntk_NodeReadFanins(node), i, fanin) /**Macro*********************************************************************** Synopsis [Iterates over the fanouts of a node.] Description [This macro iterates over the fanouts of a node. It is an error to modify the fanouts of a node while iterating its fanouts.] SideEffects [This macro instantiates macros from the array package. Hence it is advisable not to nest this macro within array macros.] SeeAlso [Ntk_NodeForEachFanout] ******************************************************************************/ #define Ntk_NodeForEachFanout( \ /* Ntk_Node_t * */ node /* node to iterate fanouts */, \ /* int */ i /* local variable for iterator */, \ /* Ntk_Node_t * */ fanout /* fanout of node */ \ ) \ arrayForEachItem(Ntk_Node_t *, Ntk_NodeReadFanouts(node), i, fanout) /**Macro*********************************************************************** Synopsis [Iterates over the nodes of a network.] Description [This macro iterates over the nodes of a network. It is an error to modify the nodes of a network while iterating its nodes.] SideEffects [] SeeAlso [Ntk_NetworkForEachPrimaryOutput Ntk_NetworkForEachPrimaryInput] ******************************************************************************/ #define Ntk_NetworkForEachNode( \ /* Ntk_Network_t * */ network /* network to iterate nodes */, \ /* lsGen */ gen /* local variable for iterator */, \ /* Ntk_Node_t * */ node /* node of network */ \ ) \ lsForEachItem(Ntk_NetworkReadNodes(network), gen, node) /**Macro*********************************************************************** Synopsis [Iterates over the latches of a network.] Description [This macro iterates over the latches of a network. It is an error to modify the latches of a network while iterating its latches.] SideEffects [] SeeAlso [Ntk_NetworkForEachPrimaryOutput Ntk_NetworkForEachPrimaryInput] ******************************************************************************/ #define Ntk_NetworkForEachLatch( \ /* Ntk_Network_t * */ network /* network to iterate latches */, \ /* lsGen */ gen /* local variable for iterator */, \ /* Ntk_Node_t * */ latch /* latch of network */ \ ) \ lsForEachItem(Ntk_NetworkReadLatches(network), gen, latch) /**Macro*********************************************************************** Synopsis [Iterates over the combinational inputs of a network.] Description [This macro iterates over the combinational inputs of a network. Primary inputs, pseudo inputs, and latches are combinational inputs. It is an error to modify the combinational inputs of a network while iterating its combinational inputs.] SideEffects [] SeeAlso [Ntk_NetworkForEachPrimaryOutput Ntk_NetworkForEachPrimaryInput] ******************************************************************************/ #define Ntk_NetworkForEachCombInput( \ /* Ntk_Network_t * */ network /* network to iterate comb inputs */, \ /* lsGen */ gen /* local variable for iterator */, \ /* Ntk_Node_t * */ node /* node of network */ \ ) \ lsForEachItem(Ntk_NetworkReadCombInputs(network), gen, node) /**Macro*********************************************************************** Synopsis [Iterates over the combinational outputs of a network.] Description [This macro iterates over the combinational outputs of a network. Primary outputs, latch data inputs, and latch initial inputs, are combinational outputs. A node may be a combinational output for more than one reason (e.g. both a latch data input and a primary output), however, it appears only once in the iteration. It is an error to modify the combinational outputs of a network while iterating its combinational outputs.] SideEffects [] SeeAlso [Ntk_NetworkForEachPrimaryOutput Ntk_NetworkForEachPrimaryInput] ******************************************************************************/ #define Ntk_NetworkForEachCombOutput( \ /* Ntk_Network_t * */ network /* network to iterate comb outputs */, \ /* lsGen */ gen /* local variable for iterator */, \ /* Ntk_Node_t * */ node /* node of network */ \ ) \ lsForEachItem(Ntk_NetworkReadCombOutputs(network), gen, node) /**Macro*********************************************************************** Synopsis [Iterates over the primary inputs of a network.] Description [This macro iterates over the primary inputs of a network. It is an error to modify the primary inputs of a network while iterating its primary inputs.] SideEffects [] SeeAlso [Ntk_NetworkForEachPrimaryOutput Ntk_NetworkForEachPseudoInput Ntk_NetworkForEachInput] ******************************************************************************/ #define Ntk_NetworkForEachPrimaryInput( \ /* Ntk_Network_t * */ network /* network to iterate primary inputs */, \ /* lsGen */ gen /* local variable for iterator */, \ /* Ntk_Node_t * */ input /* primary input of network */ \ ) \ lsForEachItem(Ntk_NetworkReadPrimaryInputs(network), gen, input) /**Macro*********************************************************************** Synopsis [Iterates over the pseudo inputs of a network.] Description [This macro iterates over the pseudo inputs of a network. It is an error to modify the pseudo inputs of a network while iterating its pseudo inputs.] SideEffects [] SeeAlso [Ntk_NetworkForEachPrimaryInput Ntk_NetworkForEachInput] ******************************************************************************/ #define Ntk_NetworkForEachPseudoInput( \ /* Ntk_Network_t * */ network /* network to iterate pseudo inputs */, \ /* lsGen */ gen /* local variable for iterator */, \ /* Ntk_Node_t * */ input /* pseudo input of network */ \ ) \ lsForEachItem(Ntk_NetworkReadPseudoInputs(network), gen, input) /**Macro*********************************************************************** Synopsis [Iterates over the inputs of a network.] Description [This macro iterates over the primary inputs and pseudo inputs of a network. It is an error to modify the inputs of a network while iterating its inputs.] SideEffects [] SeeAlso [Ntk_NetworkForEachPrimaryInput Ntk_NetworkForEachPseudoInput] ******************************************************************************/ #define Ntk_NetworkForEachInput( \ /* Ntk_Network_t * */ network /* network to iterate inputs */, \ /* lsGen */ gen /* local variable for iterator */, \ /* Ntk_Node_t * */ input /* input of network */ \ ) \ lsForEachItem(Ntk_NetworkReadInputs(network), gen, input) /**Macro*********************************************************************** Synopsis [Iterates over the primary outputs of a network.] Description [This macro iterates over the primary outputs of a network. It is an error to modify the primary outputs of a network while iterating its primary outputs.] SideEffects [] SeeAlso [Ntk_NetworkForEachPrimaryLatch Ntk_NetworkForEachLatch] ******************************************************************************/ #define Ntk_NetworkForEachPrimaryOutput( \ /* Ntk_Network_t * */ network /* network to iterate primary outputs */, \ /* lsGen */ gen /* local variable for iterator */, \ /* Ntk_Node_t * */ po /* primary output of network */ \ ) \ lsForEachItem(Ntk_NetworkReadPrimaryOutputs(network), gen, po) /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ EXTERN void Ntk_Init(void); EXTERN void Ntk_End(void); EXTERN Ntk_Network_t * Ntk_HrcManagerReadCurrentNetwork(Hrc_Manager_t *hmgr); EXTERN Ntk_Network_t * Ntk_HrcNodeConvertToNetwork(Hrc_Node_t *hrcNode, boolean buildMvfs, lsList abstractedNames); EXTERN array_t * Ntk_NodeComputeTransitiveFanoutNodes(array_t * nodeArray, int depth); EXTERN array_t * Ntk_NodeComputeTransitiveFanInputNodes(array_t * nodeArray, int depth); EXTERN array_t * Ntk_NodeComputeCombinationalSupport(Ntk_Network_t *network, array_t * nodeArray, boolean stopAtLatches); EXTERN array_t * Ntk_NodeComputeTransitiveFaninNodes(Ntk_Network_t *network, array_t * nodeArray, boolean stopAtLatches, boolean combInputsOnly); EXTERN st_table * Ntk_RegionFindNodes(array_t *roots, st_table *leaves); EXTERN st_table * Ntk_NetworkComputeLatchDependencies(Ntk_Network_t * network); EXTERN boolean Ntk_NetworkTestIsAcyclic(Ntk_Network_t * network); EXTERN boolean Ntk_NetworkTestLeavesCoverSupportOfRoots(Ntk_Network_t *network, array_t *roots, st_table *leaves); EXTERN lsList Ntk_NetworkComputeTopologicalOrder(Ntk_Network_t *network, array_t *rootNodesArray, st_table *leafNodesTable); EXTERN char * Ntk_NodeReadName(Ntk_Node_t * node); EXTERN Ntk_Network_t * Ntk_NodeReadNetwork(Ntk_Node_t * node); EXTERN Var_Variable_t * Ntk_NodeReadVariable(Ntk_Node_t * node); EXTERN int Ntk_NodeReadOutputIndex(Ntk_Node_t * node); EXTERN int Ntk_NodeReadMddId(Ntk_Node_t * node); EXTERN void Ntk_NodeSetMddId(Ntk_Node_t * node, int id); EXTERN void * Ntk_NodeReadUndef(Ntk_Node_t * node); EXTERN void Ntk_NodeSetUndef(Ntk_Node_t * node, void * value); EXTERN boolean Ntk_NodeTestIsPrimaryInput(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsPseudoInput(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsInput(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsUndefined(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsLatch(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsNextStateNode(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsShadow(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsCombInput(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsCombOutput(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsCombinational(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsPrimaryOutput(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsLatchDataInput(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsLatchInitialInput(Ntk_Node_t * node); EXTERN boolean Ntk_NodeTestIsConstant(Ntk_Node_t * node); EXTERN Ntk_Node_t * Ntk_NodeReadShadow(Ntk_Node_t * node); EXTERN Ntk_Node_t * Ntk_ShadowReadOrigin(Ntk_Node_t * shadow); EXTERN Ntk_Node_t * Ntk_LatchReadDataInput(Ntk_Node_t * node); EXTERN Ntk_Node_t * Ntk_LatchReadInitialInput(Ntk_Node_t * node); EXTERN int Ntk_NodeReadNumFanins(Ntk_Node_t * node); EXTERN int Ntk_NodeReadNumFanouts(Ntk_Node_t * node); EXTERN Ntk_Node_t * Ntk_NodeReadFaninNode(Ntk_Node_t * node, int faninIndex); EXTERN int Ntk_NodeReadFaninIndex(Ntk_Node_t * node, Ntk_Node_t * faninNode); EXTERN array_t * Ntk_NodeReadFanins(Ntk_Node_t * node); EXTERN array_t * Ntk_NodeReadFanouts(Ntk_Node_t * node); EXTERN void Ntk_NodeSetFanins(Ntk_Node_t * node, array_t *faninArray); EXTERN void Ntk_NodeSetFanouts(Ntk_Node_t * node, array_t *fanoutArray); EXTERN char * Ntk_NodeObtainTypeAsString(Ntk_Node_t * node); EXTERN void Ntk_NetworkWriteBlifMv(FILE *fp, Ntk_Network_t *network, boolean promotePseudo); EXTERN void Ntk_NodePrint(FILE * fp, Ntk_Node_t * node, boolean printIo, boolean printTableStats); EXTERN Ntk_Node_t * Ntk_NodeCreateInNetwork(Ntk_Network_t * network, char * name, Var_Variable_t *variable); EXTERN void Ntk_NodeDeclareAsLatch(Ntk_Node_t * latch, char * dataName, char * initName); EXTERN void Ntk_NodeDeclareAsPrimaryInput(Ntk_Node_t * node); EXTERN void Ntk_NodeDeclareAsPrimaryOutput(Ntk_Node_t * node); EXTERN void Ntk_NodeDeclareAsShadow(Ntk_Node_t * shadow, Ntk_Node_t * origin); EXTERN void Ntk_NodeFree(Ntk_Node_t * node); EXTERN char * Ntk_NetworkReadName(Ntk_Network_t * network); EXTERN mdd_manager * Ntk_NetworkReadMddManager(Ntk_Network_t * network); EXTERN void Ntk_NetworkSetMddManager(Ntk_Network_t * network, mdd_manager * mddManager); EXTERN mdd_manager * Ntk_NetworkInitializeMddManager(Ntk_Network_t * network); EXTERN bdd_reorder_type_t Ntk_NetworkReadDynamicVarOrderingMethod(Ntk_Network_t * network); EXTERN void Ntk_NetworkSetDynamicVarOrderingMethod(Ntk_Network_t * network, bdd_reorder_type_t dynVarOrdMethod, bdd_reorder_verbosity_t verbosity); EXTERN void * Ntk_NetworkReadUndef(Ntk_Network_t * network); EXTERN void Ntk_NetworkSetUndef(Ntk_Network_t * network, void * value); EXTERN Ntk_Node_t * Ntk_NetworkFindNodeByMddId(Ntk_Network_t * network, int mddId); EXTERN Ntk_Node_t * Ntk_NetworkFindNodeByActualName(Ntk_Network_t * network, char * name); EXTERN Ntk_Node_t * Ntk_NetworkFindNodeByName(Ntk_Network_t * network, char * name); EXTERN char * Ntk_NetworkReadActualNameFromFormalName(Ntk_Network_t * network, char * formalName); EXTERN void Ntk_NetworkInsertFormalNameToActualName(Ntk_Network_t * network, char * formalName, char * actualName); EXTERN int Ntk_NetworkReadNumNodes(Ntk_Network_t * network); EXTERN int Ntk_NetworkReadNumLatches(Ntk_Network_t * network); EXTERN int Ntk_NetworkReadNumCombInputs(Ntk_Network_t * network); EXTERN int Ntk_NetworkReadNumCombOutputs(Ntk_Network_t * network); EXTERN int Ntk_NetworkReadNumPrimaryInputs(Ntk_Network_t * network); EXTERN int Ntk_NetworkReadNumPseudoInputs(Ntk_Network_t * network); EXTERN int Ntk_NetworkReadNumInputs(Ntk_Network_t * network); EXTERN int Ntk_NetworkReadNumPrimaryOutputs(Ntk_Network_t * network); EXTERN lsList Ntk_NetworkReadNodes(Ntk_Network_t * network); EXTERN lsList Ntk_NetworkReadCombInputs(Ntk_Network_t * network); EXTERN lsList Ntk_NetworkReadCombOutputs(Ntk_Network_t * network); EXTERN lsList Ntk_NetworkReadLatches(Ntk_Network_t * network); EXTERN lsList Ntk_NetworkReadPrimaryInputs(Ntk_Network_t * network); EXTERN lsList Ntk_NetworkReadPseudoInputs(Ntk_Network_t * network); EXTERN lsList Ntk_NetworkReadInputs(Ntk_Network_t * network); EXTERN lsList Ntk_NetworkReadPrimaryOutputs(Ntk_Network_t * network); EXTERN boolean Ntk_NetworkAddApplInfo(Ntk_Network_t * network, char * key, Ntk_ApplInfoFreeFn freeFn, void * data); EXTERN boolean Ntk_NetworkSetApplInfo(Ntk_Network_t * network, char * key, Ntk_ApplInfoFreeFn freeFn, void * data); EXTERN void * Ntk_NetworkReadApplInfo(Ntk_Network_t * network, char * key); EXTERN boolean Ntk_NetworkFreeApplInfo(Ntk_Network_t * network, char * key); EXTERN Ntk_Network_t * Ntk_NetworkAlloc(char * name); EXTERN void Ntk_NetworkFree(Ntk_Network_t * network); EXTERN void Ntk_NetworkFreeCallback(void * data); EXTERN void Ntk_NetworkPrint(FILE * fp, Ntk_Network_t * network, boolean printIo, boolean printTableStats); EXTERN void Ntk_NetworkPrintStats(FILE * fp, Ntk_Network_t * network); EXTERN Ntk_Network_t * Ntk_NetworkDuplicate(Ntk_Network_t * oldNetwork); EXTERN void Ntk_NetworkAppendNetwork(Ntk_Network_t * network1, Ntk_Network_t * network2, st_table *name2ToName1); EXTERN int Ntk_NetworkPrintDot(FILE *fp, Ntk_Network_t *network); EXTERN void Ntk_NetworkSweep(Ntk_Network_t *network, int verbosity); EXTERN boolean Ntk_NodeRemoveFromNetwork(Ntk_Network_t *network, Ntk_Node_t *node, int force, boolean removeFromNodeList, int verbosity); EXTERN void Ntk_NetworkSetMAigManager(Ntk_Network_t * network, mAig_Manager_t * mAigManager); EXTERN mAigEdge_t Ntk_NodeReadMAigId(Ntk_Node_t * node); EXTERN mAig_Manager_t * Ntk_NetworkReadMAigManager(Ntk_Network_t * network); EXTERN void Ntk_NodeSetMAigId(Ntk_Node_t * node, mAigEdge_t mAigId); EXTERN void Ntk_NodeSetTable(Ntk_Node_t * node, Tbl_Table_t *table); EXTERN Tbl_Table_t * Ntk_NodeReadTable(Ntk_Node_t * node); EXTERN void Ntk_NodeDeclareAsPseudoInput(Ntk_Node_t * node, Tbl_Table_t * table, int outputIndex); EXTERN void Ntk_NodeDeclareAsCombinational(Ntk_Node_t * node, Tbl_Table_t * table, array_t * inputNames, int outputIndex); /**AutomaticEnd***************************************************************/ #endif /* _NTK */