
Next: Programming Environment Up: VIS : A System Previous: Capabilities of VIS
AlgorithmsThis section briefly discusses the significant algorithms of VIS. The fundamental data structure for these algorithms is a multilevel network of latches and combinational gates that is created by flattening the hierarchy. It is assumed that there are no combinational cycles in the network. The primary inputs and latch outputs are referred to as combinational inputs and the primary outputs and latch inputs are referred to as combinational outputs. The variables of a network are multivalued, and logic functions over these variables are represented by multivalued decision diagrams (MDDs) which are an extension of BDDs.
MDD variable orderingThe combinational input variables and next state variables must be ordered before MDDs can be constructed. The combinational input variables are ordered by doing a depthfirst traversal of the logic that generates the combinational outputs. The order in which the output logic cones are visited is determined using the algorithm of Aziz et al. [1]. This algorithm orders the latches to decrease a communication complexity bound (where backward edges are more expensive than forward edges) on the latch communication graph. The traversal of an output logic cone is done in such a way that the combinational inputs farthest from the outputs appear earlier in the ordering. We use the merging technique of Fujii et al. to handle those variables that appear in multiple cones of logic [5]. Finally, each next state variable is inserted into the variable ordering immediately after the corresponding present state variable. If the user has some knowledge of a good ordering, then a partial or total ordering on the variables can be read in. In addition, dynamic variable ordering is supported. We have found that forcing corresponding present state and next state variables to remain adjacent to each other is usually beneficial. Generally, a good initial ordering followed by one or two forced dynamic reorderings gives good results.
Partitioning the networkOnce the description of a system has been read in and the ordering of the variables assigned, an abstracted view of the system is created in which the functions of the network are stored as MDDs. This abstracted view, called a ``partition'', is the input to model checking and reachability. It can be created in several ways. At one extreme, combinational output functions are defined directly in terms of combinational inputs. On the other extreme, there is an MDD corresponding to each node in the network representing the functionality of the node in terms of its fanins, i.e., a variable is introduced for each node in the network. In general, intermediate variables can be introduced to represent the functionality of a cluster of nodes in the original network. This flexibility allows very large designs to be represented and manipulated.
Image/Preimage computationOur image/preimage computation technique is based on an early quantification heuristic [6]. The initialization process consists of creating a bitlevel relation for the next state function of each latch in the network. These bitlevel relations are then ordered to optimally exploit early quantification. Next, the relations of several bits are grouped together, making a cluster whenever the MDD size of the group reaches a threshold. Next, each cluster is simplified by quantifying out the primary inputs local to that cluster. Finally, the orders of the clusters for image and preimage are calculated and stored. Also stored is the schedule of variables for early quantification.
Reachability analysisReachability analysis makes iterative use of image computation. The performance of reachability analysis is improved by exploiting three sets of don't cares (in the following represents the set of states reached from the initial states in or fewer steps):
Model checking and debuggingWe use the algorithms presented in [3] as the basis for fair CTL model checking and debugging. In addition, a special algorithm has been implemented to improve the efficiency of checking invariants. Also, a structural pruning technique is used to eliminate those parts of the network that cannot affect the formula being checked. This is particularly useful in conjunction with the abstraction mechanism mentioned in Section 2. Finally, don't cares arising from the unreachable states, and from the fixed point computations, are used to simplify intermediate MDDs.
Next: Programming Environment Up: VIS : A System Previous: Capabilities of VIS
Tom Shiple Thu Feb 8 16:55:08 PST 1996 
You are not logged in 
Contact 
©20022017 U.C. Regents 