VIS-V: Verification

VIS-V provides analysis capabilities for designs. From any node in the hierarchy (the current node), executing the command flatten_hierarchy causes a flattened network to be created, representing everything from the current node down to the leaves of the hierarchy. Having a flattened representation in which all combinational ``gates'' and latches exist in a single network allows for the global analysis of that part of the design encompassed by the current node of the hierarchy. The packages of VIS-V are:

• ntk - A directed graph representation, where the vertices are ``gates,'' inputs and latches. Combinational cycles are not precluded by the network data structure, but many of the packages assume the absence of combinational cycles.
• ord - Routines to order the MDD variables of a network, based on the structure of the network. Also provides an interface to dynamic ordering of variables.
• ntm - A routine to build the Mvf_Function_ts of the roots of an arbitrary region of a network, in terms of the leaves of the region. The leaves can be treated as variables or as specific constants.
• part - Routines to build an MVF representation of a network. The MVFs are stored at the vertices of a DAG, where the sinks correspond to the combinational outputs of the network, and the sources to the combinational inputs. In general, intermediate vertices can be introduced to control the size of the MVFs.
• sim - A cycle-based network simulator. Simulation is performed by evaluating the MVFs provided by the part package. Simulation vectors can be provided by the application, or random simulation can be performed.
• img - Generic routines for performing forward and backward image computation. The routines work off the graph of MVFs provided by the part package, and have no direct knowledge of the ntk or fsm packages. Since this is an active area of research, a generic interface has been designed to easily allow the addition of new computation methods.
• fsm - An abstraction of a network. The FSM does not actually store the next state functions of the FSM - these are provided by part . It does store the vectors of present state and next state variables, reachability information, fairness constraints-related information, and image computation information.
• mc - A fair CTL model checker and debugger for FSMs.
• eqv - Routines for performing combinational equivalence between regions of two networks, and for performing sequential equivalence between two FSMs.
• ctlp - A CTL parser.

The nodes of a network have a single output. The function of a combinational node of a network is represented by a Tbl_Table_t. A k-output table in the hierarchy is represented by k combinational nodes in the corresponding network, where each of the k nodes points to the same table, but are distinguished by which output column they represent. This splitting is done by the flattening routine in the ntk package.

Throughout VIS-V, it is assumed that the combinational outputs are completely specified and deterministic. Non-determinism is introduced via pseudo-inputs . A pseudo-input is like a non-deterministic constant that can update its value on each clock cycle. See the documentation for the ntk package for more information on pseudo-inputs.

Because the emphasis of VIS-V is on analysis, the ability to modify the network data structure is not provided. It is assumed that once a network is created from the hierarchy, the network will be unchanged until it is destroyed.

Notice that the ntk package is independent of all other packages in VIS-V. This independence is maintained by allowing applications (e.g., fsm, part) to store information associated with a network in a lookup table. It is important to maintain this independence so that the ntk data structures do not become cluttered.