next up previous
Next: Programming Environment Up: VIS : A System Previous: Capabilities of VIS


  This section briefly discusses the significant algorithms of VIS. The fundamental data structure for these algorithms is a multi-level 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 multi-valued, and logic functions over these variables are represented by multi-valued decision diagrams (MDDs) which are an extension of BDDs.

MDD variable ordering

The combinational input variables and next state variables must be ordered before MDDs can be constructed. The combinational input variables are ordered by doing a depth-first 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 network

Once 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/Pre-image computation

Our image/pre-image computation technique is based on an early quantification heuristic [6]. The initialization process consists of creating a bit-level relation for the next state function of each latch in the network. These bit-level 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 pre-image are calculated and stored. Also stored is the schedule of variables for early quantification.

Reachability analysis

Reachability 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):

  1. Selection of the frontier set for computing , given . The frontier set can be any set satisfying the following inequality: .
  2. Simplification of the transition relation , by taking the generalized cofactor with respect to (we care only about the transitions originating from the frontier states).
  3. Simplification of the transition relation , by taking the generalized cofactor with respect to (we care only about the transitions to the set of states not reached thus far).

Model checking and debugging

We 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 up previous
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 
©2002-2017 U.C. Regents