Canonical representations of high-level decision diagrams/Korgtaseme otsustusdiagrammide kanooniline esitus.

Karputkin, Anton ; Ubar, Raimund ; Raik, Jaan 等

1. INTRODUCTION

As the complexity of digital systems continues to increase, the traditional gate level modelling of systems, especially for verification and test generation purposes, has become obsolete. Economical and practical reasons have pushed the designers to apply automatic test pattern generation at higher abstraction levels to implement functional or hierarchical test strategies, or to approach design validation with the goal to early identify and remove design errors at higher functional levels, saving time and money. Thus many functional automated test pattern generators (ATPG) have been proposed in the literature to generate effective test sequences at the higher [1-3], behaviour [4,5] or functional register-transfer levels [6,7]. A special case of functional techniques are ATPGs, based on perturbation of statements in the digital circuit model using VHDL or RTL [8,9]. Hierarchical approach [10,11], compared to pure functional approach, lies in the possibility of constructing test plans on higher levels and modelling faults on more detailed lower levels, which results in better test quality.

The efficiency of high-level test generation for complex digital systems depends essentially on selecting the diagnostic model of the system and the way how to represent and handle the faults of the system. High-level functional ATPGs can be divided into two main categories: random-based and deterministic. The first set adopts simulation-based strategies, guided by genetic algorithms or other probabilistic techniques [2,3]. They rely on functional fault models and simulation of HDL descriptions (e.g. SystemC, VHDL, Verilog, etc.) of the design. These ATPGs are fast, but they cannot guarantee high fault coverage and they tend to generate very long test sequences. Deterministic ATPGs are based on mathematical strategies to allow a complete exploration of the system's state space [4,6,7,10,11], thus covering corner cases, but they require a larger amount of timing and memory resources.

In search for efficient high-level models, recently a number of papers has been published on implementing assignment decision diagram (ADD) models [12] combined with SAT methods to address register-transfer level (RTL) test pattern generation [6,7]. A promising approach is to use high-level decision diagrams (HLDD) [13] that, unlike ADDs, can be viewed as a generalization of binary decision diagrams (BDDs). HLDDs allow modelling of different abstraction levels from RTL to behavioural while ADDs are limited to RTL only. HLDDs have proven to be an efficient model for simulation [14], fault modelling [15] and test generation [10,11] as they provide for fast evaluation by graph traversal and for easy identification of cause-effect relationships. Further improvements in using HLDDs for high-level functional test generation were reached by combining HLDDs with extended finite state machines (EFSM) [16,17].

Within the last two decades binary decision diagrams (BDD) have become the state-of-the-art data structure in VLSI CAD for representation and manipulation of Boolean functions [18-25]. They were introduced first in 1959 by C. Y. Lee in the form of binary decision programs for representing digital circuits [18]. In 1976 the same model, called alternative graphs [19,20], was introduced for test generation purposes. Independently the same model was introduced into the field of test generation by Akers [21] under the name of BDDs. Today the theory of BDDs is developing quickly with the main purpose of efficient manipulation of logic expressions. The subset of BBDs, called structurally synthesized binary decision diagrams (SSBDDs), represent directly in the graph the structural features of circuits [19,20,26,27]. While traditionally BDDs are generated by Shannon's expansions, which allow to extract only the Boolean function of the logic circuit, the SSBDDs are generated by a superposition procedure that extracts both, function and data about structural paths of the circuit. This feature makes them preferable for diagnosis related tasks like fault modelling, simulation, test generation and fault location. 40

HLDDs represent a generalization of SSBDDs for modelling the functions and structure of digital systems on higher behaviour, functional or RTL abstraction levels. HLDDs are an excellent way to represent cause-effect and effect-cause relationships at higher levels of system abstraction as a basis for fault diagnosis in technical systems. They allow to skip dedicated low-level technical problems, related to semiconductor technology and to concentrate only on the high-level logic abstractions to carry out diagnostic reasoning. This is the only way how to handle today's complex systems. Moreover, the test related procedures, developed for SSBDDs, can be easily generalized for HLDDs to handle digital systems, represented at higher levels. In [28] two methods for synthesis of HLDDs were proposed. The first method is based on symbolic execution of procedural descriptions, which corresponds to functional representation of the system, e.g. on the behavioural level. The second one is based on iterative superposition of HLDDs, and the created model corresponds to the high-level structural representation of the system. The second method can be regarded as the generalization of the superposition of SSBDDs [29].

An example of a structurally synthesized HLDD, which represents a RTL data path of a digital system shown in Fig. 1 with functions of the components in Table 1, is depicted in Fig. 2. Variables [R.sub.1] and [R.sub.2] represent registers, IN represents the input bus, integer variables [y.sub.1], [y.sub.2], [y.sub.3], [y.sub.4] represent control signals, [M.sub.1],[M.sub.2],[M.sub.3] are multiplexers, and the functions [R.sub.1] + [R.sub.2] and [R.sub.1] * [R.sub.2] represent adder and multiplier, respectively. Each node in the HLDD represents a subcircuit of the system (e.g. the nodes [y.sub.1], [y.sub.2], [y.sub.3], [y.sub.4] represent multiplexers and decoders). The whole DD describes the behaviour of the input logic of the register [R.sub.2]. The bold path in Fig. [member of] shows the active mode of the system in the case of input control vector ([y.sub.1], [y.sub.2], [y.sub.3], [y.sub.4]) = (1, 0, 3, 2), which means that during this clock cycle the system calculates the multiplication [R.sub.2] = [R.sub.1] * [R.sub.2]. The structural relationships between the HLDD and the original system are highlighted by dotted lines in Fig. 2. The area in Fig. [member of] denoted by [R.sub.2] corresponds to the DD for the subcircuit [R.sub.2], consisting of register [R.sub.2] with its input logic in Fig. 1; the area denoted by [R.sub.2]+[M.sub.3] corresponds to the composite DD for the subcircuit, consisting of components [M.sub.2], multiplier, [M.sub.3] and [R.sub.2], highlighted by dark colour in Fig. 1; the area, denoted by c([M.sub.1]), corresponds to the DD for the subcircuit consisting of the components [M.sub.1] and adder; finally, the area denoted by d([M.sub.2]) corresponds to the DDs for the subcircuit, consisting of the components [M.sub.2] and multiplier.

[FIGURE 1 OMITTED]

[FIGURE 2 OMITTED]

In the HLDDs the internal nodes represent the control part of a system and the terminal nodes represent the data manipulation part of the latter. In the general case a system is described by a set of HLDDs, where each HLDD represents a controlled input logic of a register.

In this paper we will show how the HLDDs can be used for high-level verification purposes (more precisely, for probabilistic equivalence checking), for example in the cases when we have got two HLDD representations of a system: (1) high level specification, and (2) high level implementation. We will describe the diagrams by sets of characteristic polynomials and show how to use them in practice. The idea to represent digital systems as polynomials is not new, one can find similar ideas adapted for gate level models in papers [30,31]. An attempt to move up to the higher levels was made in [32]. However, at these levels we do not have such convenient and well-known formal representation of the system as boolean expressions are for the gate level. Before strarting to compute a polynomial we need an initial definition of the function it describes. The multivalued decision diagrams proposed for this purpose in [32] is not the best choice: computing them is the problem itself. This work combined with our previous paper [28] gives a way to get the canonical form of the digital system at higher levels directly from its description.

The paper is organized as follows. In Section [member of] we give the formal definition of HLDDs, in Section 3 we show the possibility of representing the HLDDs by characteristic polynomials, which can be used as a canonical form of HLDDs. In Section 4 we show how the characteristic polynomials can be used for proving the equivalence between two HLDDs, which may have different internal structures. Section 5 concludes the paper.

2. DEFINITION OF HLDD

In this section we define the objects being studied in the current article: HLDDs and functions represented by them, further called HLDD functions.

Consider a digital system (Z, F) as a network of subsystems or components where Z is the set of variables (Boolean, Boolean vectors or integers), which represent connections between components, inputs and outputs of the network. Let Z = X [union] Y , where X is the set of function arguments and Y is the set of function values where Q = X [intersection] Y is the set of state variables. D(z) denotes the finite set of all possible values for z [member of] Z and D(U) is the set of all possible vectors in U [subset or equal to] Z. Obviously, if U = {[u.sub.1], ... , [u.sub.n]} then D(U) = D([u.sub.1]) x ... x D([u.sub.n]). Let F be a set of digital functions: [z.sub.k] = [f.sub.k]([Z.sub.k]) where [z.sub.k] [member of] Z, [f.sub.k] [member of] F, and [Z.sub.k] [subset] Z (k iterates over all elements in F).

Definition 1. The high-level decision diagram representing the function [f.sub.k] : D([Z.sub.k]) [right arrow] D([z.sub.k]) is a directed acyclic graph G = (V,E) with one root node and a set of terminal nodes, where:

--Each non-terminal node is labelled by some input or control variable x [member of] X [union] Q. We shall denote the variable of node v by [x.sub.v].

--Each terminal node w is labelled by some function [g.sub.w] : D([Z.sub.w]) [right arrow] D([z.sub.k]) (possibly a constant or a single variable), where [Z.sub.w] [subset or equal to] [Z.sub.k].

--Each edge e = (v, u) is labelled by some constant [c.sub.e] [member of] D([x.sub.v]).

--Each two edges [e.sub.1] = (v, [u.sub.1]) and [e.sub.2] = (v, [u.sub.2]) going from the same source node are labelled by different constants c[e.sub.1] [not equal to] c[e.sub.2].

--If the node v is labelled by [x.sub.v] then the number of edges going from this node is |D([x.sub.v])|.

Remark 1. Each BDD is HLDD as well, with two terminal vertices labelled by constant functions 0 and 1, and D(x) = {0, 1} for every variable x.

We shall denote the set of terminal nodes by [V.sup.T], the set of non-terminal nodes by [V.sup.N] and the set of all successors of the node v by [LAMBDA](v). For non-terminal nodes v [member of] [V.sup.N] an onto function exists between the values c [member of] D([x.sub.v]) of labels [x.sub.v] and the successors [v.sup.c] [member of] [LAMBDA](v) of v. By [v.sup.c] we denote the successor of v for the value [x.sub.v] = c. The edge (v, [v.sup.c]), which connects nodes v and [v.sup.c], is called activated iff there exists an assignment [x.sub.v] = c. Activated edges, which connect [v.sub.i] and [v.sub.j] , make up an activated path l([v.sub.i], [v.sub.j]) [subset or equal to] V . An activated path l([v.sub.0], [V.sup.T]) from the root node v0 to a terminal node [V.sup.T] is called full activated path and [V.sup.T] itself is activated terminal node. Without loss of generality we assume further that each variable has at least two values, i.e. [for all]z [member of] Z, D(z) > 1.

Let S = X [union] Q and let [D.sub.i] designate a subset of D(S), such that assignments from it will activate the terminal node [V.sup.T].sub.i]. Thus D(S) is being split to non-intersecting sets [D.sub.1], ...,[D.sub.t], where t = |[V.sup.T]|. More formally,

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

Now it is easy to get an algebraic expression for the HLDD function [f.sub.k]. Let [alpha] [member of] D(S) be some assignment to input and control variables and [X.sub.i]: D(S) [right arrow] {0, 1} be the characteristic function of the set [D.sub.i], i.e. [X.sub.i]([[alpha].sub.1], ... , [[alpha].sub.n]) = 1 [left and right arrow] ([[alpha].sub.1], ... , [[alpha].sub.n]) [member of] [D.sub.i]. We will use a formula

[f.sub.k]([Z.sub.k]) = [case.sup.t.sub.i=1] [X.sub.i](S) [right arrow] gi(Zi) (1)

as a shorthand for the algorithm:

begin

if [alpha] [member of] [D.sub.1] then [f.sub.k]([Z.sub.k]) = g1([Z.sub.1]) endif ... if [alpha] [member of] [D.sub.t] then [f.sub.k]([Z.sub.k]) = gt([Z.sub.t]) endif

end

Let us continue with some examples:

Example 1. An HLDD in Fig. 3 evaluates the next state of the variable C. In this example Z = {C',A',B', q, [x.sub.A], [x.sub.B], [x.sub.C]}. The apostrophe means the previous value of the variable. Depending on the values of q, [x.sub.A], [x.sub.B] and [x.sub.C], the next value of C is its previous value C', negation [bar.C'] or A' + B'.

[FIGURE 3 OMITTED]

3. CHARACTERISTIC POLYNOMIALS

There are two ways to generate an HLDD for some digital system: one based on procedural description and another based on iterative superposition. These methods are described in [28]. Further research on HLDD properties requires us to make the following important assumption: each path in the diagram does not contain any of the control variables twice. Diagrams generated by the first algorithm really have such property. The second method can theoretically produce such paths. If we encounter the same variable two times in a path, we can duplicate all variables between the occurrencies of this variable and make an equivalent diagram without such redundancies. Let a path contain nodes, labelled by variables [x.sub.0], [x.sub.1], ..., [x.sub.k], [x.sub.0]. We should produce a new diagram, where this chain would be replaced by two new chains, [x.sub.0], [x.sub.1], ..., [x.sub.k] and [x.sub.1], ..., [x.sub.k], [x.sub.0]. The following theorem will help us.

Theorem 1. Suppose an HLDD, containing a chain of non-terminal nodes labelled by variables [x.sub.0], [x.sub.1], ..., [x.sub.k], [x.sub.0], was transformed in the following way:

--Remove nodes labelled [x.sub.0], [x.sub.1], ..., [x.sub.k], [x.sub.0]:

--Add 2(k + 1) nodes labelled [x.sub.1], ..., [x.sub.k], [x.sub.0] (the first chain) and [x.sub.0], [x.sub.1], ..., [x.sub.k] (the second chain).

--All connections from and to the nodes of the first chain will remain the same.

--All connections from and to [x.sub.0] occurence in the second chain will remain the same.

--Connections from other nodes to [x.sub.1], ..., [x.sub.k] in the second chain will be removed.

Then the result is equivalent to the original diagram.

Proof. We shall prove that the second diagram contains all paths from the first one that could be activated and vice versa. [right arrow]:

--Obviously, all paths not containing mentioned nodes remain unchanged.

--All paths containing the first occurrence of the [x.sub.0] can be activated in the second chain.

--All paths containing the second occurrence of the [x.sub.0] or only intermediate nodes [x.sub.1], ..., [x.sub.k] can be found in the first chain.

[left arrow]: The similar check for all possible paths in our two chains shows that they can be activated in the first diagram.

Example 2. Figure 4 illustrates the transformation described above. Some vertex and all edge labels are not shown because they are not important. We have a path x [right arrow] y [right arrow] z [right arrow] x that is being split in two chains x [right arrow] y [right arrow] z and y [right arrow] z [right arrow] x.

Suppose now that we have two HLDDs, representing the same functionality. They can look very different as the next examples illustrate.

Example 3. Figure 5 shows two HLDDs of the same function. The only difference is how we evaluate this function. The first diagram represents the situation when we first check the value of the variable X, then, if X equals 2, we check the Y value. The second diagram displays the process of evaluation starting with checking Y .

Example 4. Figure 6, left side, shows the diagram with 4 non-terminal nodes labelled by variables X, Y,Z. However, it is easy to see that the variable Y is redundant in this case and the diagram from the right side without this variable is the equivalent one.

[FIGURE 4 OMITTED]

[FIGURE 5 OMITTED]

[FIGURE 6 OMITTED]

Let us suppose we have two diagrams [G.sub.1] and [G.sub.2], with the same sets of control variables and terminal nodes and wish to prove that they are equivalent. Actually it means that the function (1) for both diagrams is the same. As the functions [g.sub.i] are the same, we should compare the corresponding characteristic functions. Without loss of generality we may assume that D([x.sub.i]) = {1, ... , |D([x.sub.i])|}. If not we may define a bijective mapping h : D([z.sub.i]) [right arrow] {1, ... , |D([x.sub.i])|} and use the values of this function instead of their originals. Then the following theorem takes place.

Theorem 2. The characteristic function of the set [D.sub.i], [X.sub.i](S), can be represented by a unique polynomial [P.sub.i] : [Q.sup.n] [right arrow] Q of degree at most [[SIGMA.sup.P.sub.i=1] (|D([x.sub.i])| - 1) where we have for each vector [alpha] = ([[alpha].sub.1], ..., [[alpha].sub.n]) [member of] D(S)

[X.sub.i]([[alpha].sub.1], ..., [[alpha].sub.n]) = [P.sub.i]([[alpha].sub.1], ..., [[alpha].sub.n]):

Proof. We have D(S) different vectors in [Q.sup.n]. The sought-for polynomial should be equal to 1 for vectors from [D.sub.i] and to 0 for vectors from D(S)\[D.sub.i]. In numerical analysis the Lagrange interpolation polynomial is well-known [33]: consider we have measured the values for a function f : [a, b] [right arrow] R at points [x.sub.0], ..., [x.sub.n], and obtained results are [y.sub.0], ..., [y.sub.n], then we can interpolate them to the whole segment [a, b] by a polynomial of degree at most n:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

If f is a polynomial of such degree then we get the exact result, otherwise there will be some error. Note that for x = [x.sub.0], ..., [x.sub.n] we will always get the exact result: P([x.sub.i]) = [y.sub.i] = f([x.sub.i]) and it is a polynomial of lowest degree that gives such result. This is the property we are interested in the current paper. Although in numerical analysis textbooks only the case of one-variable function is usually studied, these results can be easily transferred to the multiple-variable case. So, our sought-for polynomial [P.sub.i] is the Lagrange polynomial that evaluates to 1 for each vector from [D.sub.i] and to 0 for each vector from D(S)\[D.sub.i]:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] (2)

The degree of this polynomial is at most [[SIGMA].sup.n.sub.i=1] (|D([x.sub.i])| - 1). Let us prove that this is the only polynomial of such degree.

--The basis. Let n = 1. Assume we have [member of] polynomials, P([x.sub.1]) and Q([x.sub.1]), deg P = degQ = |D([x.sub.1])| - 1 and [for all](i [member of] 1..|D([x.sub.1])|) P(i) = Q(i). Then the polynomial P - Q has |D([x.sub.1])| roots, from 1 to |D([x.sub.1])|, which could be only in case P [equivalent to] Q.

--The induction step. The proof is similar to the basis case one: assume we have [member of] polynomials, P([x.sub.1], ..., [x.sub.n]) and Q([x.sub.1], ..., [x.sub.n]), deg P = deg Q = [[SIGMA].sup.n.sub.i=1] (|D([x.sub.i])| - 1). After assigning values to [x.sub.1] we get |D([x.sub.1])| pairs of (n - 1)-variable polynomials. They are pairwise equal by induction hypothesis. Thus, the polynomial function P - Q : Q [right arrow] Q[[x.sub.2], ..., [x.sub.n]] of degree at most |D([x.sub.1])|-1 has |D([x.sub.1])| roots in Q[[x.sub.2], ..., [x.sub.n]]. Thus, P [equivalent to] Q.

Corollary 1. Two diagrams [G.sub.1] and [G.sub.2] are equivalent iff they have equal sets of control variables, terminal nodes and the polynomial representations (2) of characteristic functions for any two corresponding terminal nodes are the same.

We shall call the right side of formula [member of] the characteristic polynomial of the node [V.sup.T.sub.i]. The Algorithm 1 shows how to get such polynomials for a certain diagram. Here we shall prove that it is correct.

Theorem 3. The Algorithm 1 produces the set of characteristic polynomials for the diagram G.

Algorithm 1. Evaluation of characteristic polynomials.

Input: HLDD G
Output: The set of characteristic polynomials for G
we shall evaluate polynomials node by node. A polynomial
for node v will be denoted by [P.sub.v],
order all nodes in G topologically. Let T be an array of ordered nodes,
[P.sub.T[0]] = 1,
for v [member of] T do
   [P.sub.v] = 0,
end
for v [member of] T do
   for parentnode w of v do
      i = [c.sub.(w,v)];
      [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]
   end
end
return {[P.sub.v]|v [member of] [V.sup.T]}

Proof. Let W be a set of all paths from the root node to some terminal node [V.sup.T] . Each path w [member of] W activated by the assignment ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]) will be represented in the resulting polynomial by the following summand:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] (3)

(This can be easily proved by induction). The resulting polynomial will be the sum of these summands over all paths from W. As we have assumed in the beginning of the chapter, all variables in w are different. So, l [less than or equal to] n. The only difference between summands in (2) and (3) is the bound of the first product sign: generally, the path w should not contain all variables; some of them may be missing. This means that one path actually represents |D([r.sub.1]) x ... x D([r.sub.n-l])| assignments [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] where [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]. But we have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] (4)

This is the Lagrange polynomial that evaluates to 1 for all possible values from D([r.sub.1]) x ... x D([r.sub.n-l]). The simplest polynomial with such property is the constant 1, so they should coincide. Multiplying this polynomial with our summand gives the sum of D([r.sub.1]) x ... x D([r.sub.n-l]) summands, each representing certain assignment for the whole set of variables. Finally, adding them together results in the formula (2) (none of the summands will appear twice, because all paths have the same source node and thus assignments of corresponding paths will differ for at least one variable; otherwise they would never branch off).

Example 5. Let us now find the characteristic polynomials for HLDD from Example 1. First of all we change the labels of edges labelled by 0 to 5 for the one going from node q and to [member of] for others. We have 4 paths to the first terminal node: (q = 5), (q = 1), (q = 3, xC = 1), (q = 4, xA = 2). Thus,

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

For the second node we have two paths (q = 2, [x.sub.B] = 2) and (q = 3, [x.sub.C] = 2), so the second polynomial will be

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

Finally, paths (q = 2, [x.sub.B] = 2) and (q = 4, [x.sub.A] = 1) give us the third polynomial:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

4. PRACTICAL USAGE OF CHARACTERISTIC POLYNOMIALS

A skeptically minded reader, after looking at Eq. (2), may notice that the evaluation of such polynomial for a large modern digital system would take huge amount of time. This is true. However, we can get a lot of useful information about the function without evaluating it directly in analytical form. Here we are giving an algorithm that can be used in HLDD verification and is residing in complexity class P. It evaluates the coefficients of lower degrees. Before we provide it we should agree on mapping from D(z) to Z. Generally, each mapping is good except the ones containing zeroes. Multiplication by zero will lose information about some paths. Thus, for example in case of D(z) = 0, 1, ..., |D(z)| - 1 it is better to use mapping h(z) = z + 1. Indeed, assume 0 [member of] D(z) and we need to evaluate the constant term. In this case all assingnments with z [nit equal to] 0 will produce summands containing factor z in Eq. (2). The constant terms of these summands are equal to 0, so they are not taken into account when we evaluate the last coefficient of the whole polynomial.

Algorithm 2. Evaluating polynomial coefficients of degrees
[less than or equal to] k.

Input: HLDD G, maximal degree k
Output: Set of polynomials, one per each terminal node, that contain
   members of the
   characteristic polynomials with degree [less than or equal to] k
order all nodes in G topologically. Let T be an array of ordered
   nodes;
[P.sub.T][0] = 1;
for v [member of] T do
   [P.sub.v] = 0;
end
for v [member of] T do
   for parentnode w of v do
      i = [c.sub.(w,v)];
      [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]
      if [P.sub.v] contains coefficiens of degree > k delete them;
   end
end
return {[P.sub.v]|v [member of] [V.sup.T]}

Once we have chosen the proper mapping we can use Algorithm [member of] to calculate all coefficients of degrees [less than or equal to] n. This method cannot allow us to be 100% confident that our two diagrams are equivalent but if they are not then it can be found very quickly. We continue with an example.

Example 6. Let us introduce an error to the diagram in Fig. 3. For instance, let the edge ([x.sub.B],A'+B') now point to the first terminal node, C', as it is shown in Fig. 7. The characteristic polynomial of the third terminal node remains the same, while [member of] others will change:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

As we see, even only the check for constant terms would detect the error.

[FIGURE 7 OMITTED]

5. CONCLUSIONS

A novel method for probabilistic equivalence checking of digital systems was proposed. It is based on representing the high-level decision diagrams as the model of digital systems by the sets of characteristic polynomials. It was shown that this representation is canonical, i.e. the sets of polynomials for equivalent diagrams are the same up to the names of the variables. Computing the full set of polynomials is unfeasible for large diagrams as it demands checking all assignments to the control variables. To cope with this problem we have developed a polynomial algorithm for probabilistic checking.

The algorithm calculates coeficients of low-degree summands up to the given fixed degree k. If the coeficients do not coincide, then the HLDDs are definitely different; if the coefficients coincide, then the HLDDs are with high probability equivalent whereas the probability depends on the chosen degree of k. To prove that the HLDDs are not equivalent is possible also by only comparing constant terms of the polynomial. For instance, in Example 6, we can see, that even a small erroneous change in the diagram is detectable by comparing constant terms.

The technique itself does not have limitations. However, for some classes of digital systems, optimization techniques may be needed to create efficient HLDD models, but this topic does not belong to the scope of the paper. Also, the equivalence checking of the terminal node functions was left uncovered. The general idea is that those functions are usually simple ones and can be verified using gate level methods. Nevertheless we plan to look at those functions more intently in our future research.

doi: 10.3176/eng.2010.1.06

ACKNOWLEDGEMENTS

The work has been supported by the European Commission Framework Program FP7 CREDES, by the European Union through the European Regional Development Fund, by the Estonian Science Foundation (grants Nos. 7068 and 7483), and Enterprise Estonia funded ELIKO Development Centre. 53

REFERENCES

[1.] Kapuer, R. High Level ATPG is important and is on its way! In Proc. IEEE International Test Conference. Atlantic City, NJ, 1999, 1115-1116.

[2.] Corno, F., Cumani, G., Sonza Reorda, M. and Squillero, G. Effective techniques for high-level ATPG. In Proc. IEEE Asian Test Symposium. Kyoto, Japan, 2001, 225-230.

[3.] Fin, A. and Fummi, F. Genetic algorithms: the philosopher's stone or an effective solution for high-level TPG? In Proc. IEEE High-Level Design Validation and Test Workshop. San Francisco, CA, 2003, 163-168.

[4.] Ferrandi, F., Fummi, F. and Sciuto, D. Implicit test generation for behavioral VHDL models. In Proc. IEEE International Test Conference. Washington, D.C., 1998, 436-441.

[5.] Xin, F., Ciesielski, M. and Harris, I. Design validation of behavioral VHDL descriptions for arbitrary fault models. In Proc. IEEE European Test Symposium. Tallinn, Estonia, 2005, 156-161.

[6.] Ghosh, I. and Fujita, M. Automatic test pattern generation for functional register-transfer level circuits using assignment decision diagrams. IEEE Trans. Comput.-Aided Des. Integrated Circuits Systems, 2001, 20, 402-415.

[7.] Zhang, L., Ghosh, I. and Hsiao, M. Efficient sequential ATPG for functional RTL circuits. In Proc. International Test Conference. Charlotte, NC, 2003, 290-298.

[8.] Armstrong, J. A., Lam, F. S. and Ward, P. C. Test generation and fault simulation for behavioural models. In Performance and Fault Modelling with VHDL (Shoen, J. M., ed.). Prentice Hall, Englewood Cliffs, NY, 1992, 240-303.

[9.] Cho, H. Ch. and Armstrong, J. A. B-algorithm--a behavioural test generation algorithm. In Proc. International Test Conference. Washington, D.C., 1994, 968-979.

[10.] Raik, J. and Ubar, R. Fast test pattern generation for sequential circuits using decision diagram representations. J. Electronic Testing: Theory and Applications, 2000, 16, 213-226.

[11.] Jervan, G., Ubar, R., Peng, Z. and Eles, P. Test generation: a hierarchical approach. In System-level Test and Validation of Hardware/Software Systems (Sonza Reorda, M., Peng, Z. and Violante, M., eds.), Springer, London, 2005, 63-77.

[12.] Chayakul, V., Gajski, D. D. and Ramachandran, L. High-level transformations for minimizing syntactic variances. In Proc. ACM/IEEE Design Automation Conference. Dallas, TX, 1993, 413-418.

[13.] Ubar, R. Test synthesis with alternative graphs. IEEE Des. Test Comput., 1996, 13, 48-57.

[14.] Ubar, R., Morawiec, A. and Raik, J. Back-tracing and event-driven techniques in high-level simulation with decision diagrams. In Proc. IEEE International Symposium on Circuits and Systems '00. Geneva, 2000, 208-211.

[15.] Ubar, R., Raik, J., Jutman, A., Instenberg, M. and Wuttke, H.-D. Modeling microprocessor faults on high-level decision diagrams. In Proc. International Conference on Dependable Systems & Networks. Anchorage, AL, 2008, C-17-C-22.

[16.] Di Guglielmo, G., Fummi, F., Marconcini, C. and Pravadelli, G. Improving gate-level ATPG by traversing concurrent EFSMs. In Proc. IEEE VLSI Test Symposium. Berkeley, CA, 2006, 172-179.

[17.] Guglielmo, G., Fummi, F., Jenihhin, M., Pravadelli, G., Raik, J. and Ubar, R. On the combined use of HLDDs and EFSMs for functional ATPG. In Proc. 5th IEEE East- West Design and Test International Symposium. Jerevan, Armenia, 2007, 503-508.

[18.] Lee, C. Y. Representation of switching circuits by binary decision programs. Bell Syst. Techn. J., 1959, 38, 985-999.

[19.] Ubar, R. Test generation for digital circuits with alternative graphs. Proc. Tallinn Technical University, 1976, No. 409, 75-81 (in Russian).

[20.] Plakk, M. and Ubar, R. Digital circuit test design using the alternative graph model. In Automation and Remote Control. Plenum Publishing Corporation, New York, 1980, 41, 714-722.

[21.] Akers, S. B. Functional testing with binary decision diagrams. J. Design Automat. Fault-Tolerant Comput., 1978, 2, 311-331.

[22.] Bryant, R. E. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Computers, 1986, C-35, 677-691.

[23.] Minato, S. Binary Decision Diagrams and Applications for VLSI CAD. Kluwer, Norwell, MA, 1996.

[24.] Sasao, T. and Fujita, M. (eds.). Representations of Discrete Functions. Kluwer, Norwell, MA, 1996.

[25.] Drechsler, R. and Becker, B. Binary Decision Diagrams. Kluwer, Boston, Dordrecht, London, 1998.

[26.] Ubar, R. Multi-valued simulation of digital circuits with structurally synthesized binary decision diagrams. In Multiple Valued Logic. Gordon and Breach Publishers, 1998, vol. 4, 141-157.

[27.] Jutman, A., Raik, J. and Ubar, R. SSBDDs: Advantageous model and efficient algorithms for digital circuit modeling, simulation & test. In Proc. 5th International Workshop on Boolean Problems. Freiberg, Germany, 2002, 157-166.

[28.] Ubar, R., Raik, J., Karputkin, A. and Tombak, M. Synthesis of high-level decision diagrams for functional test pattern generation. In Proc. 16th International Conference on Mixed Design of Integrated Circuits and Systems. Lodz, Poland, 2009, 519-524.

[29.] Ubar, R., Vassiljeva, T., Raik, J., Jutman, A., Tombak, M. and Peder, A. Optimization of structurally synthesized BDDs. In Proc. 4th IASTED International Conference on Modelling, Simulation and Optimization. Kauai, HI, 2004, 234-240.

[30.] Agrawal, V. D. and Lee, D. Characteristic polynomial method for verification and test of combinational circuits. In Proc. 9th International Conference on VLSI Design: VLSI in Mobile Communication. Bangalore, India, 1996, 341-342.

[31.] Jain, J., Bitner, J., Fussell, D. S. and Abraham, J. A. Probabilistic design verification. ICCAD-91. In Digest of Technical Papers., 1991 IEEE International Conference on Computer-Aided Design. Santa Clara, CA, 1991, 468-471.

[32.] Dubrova, E. and Sack, H. Probabilistic verification of multiple-valued functions. In Proc. 30th IEEE International Symposium on Multiple-Valued Logic. Portland, OR, 2000, 460-466.

[33.] Atkinson, K. A. An Introduction to Numerical Analysis, 2nd ed. J.Wiley, New York, 1989.

Anton Karputkin (a), Raimund Ubar (a), Jaan Raik (a) and Mati Tombak (b)

(a) Department of Computer Engineering, Tallinn University of Technology, Raja 15, 12618 Tallinn, Estonia, {kanton, raiub, jaan}@pld.ttu.ee

(b) Department of Informatics, Tallinn University of Technology, Raja 15, 12618 Tallinn, Estonia, mati@ut.ee

Received 28 October 2009, in revised form 26 January 2010

Table 1. Functions of the blocks of system in Fig. 1

[y.sub.1]   [M.sub.1]/a   [y.sub.2]   [M.sub.2]/b   [y.sub.3]

            [R.sub.1]     0           [R.sub.1]     0
0           IN            1           IN            1
1                                                   2
                                                    3
[y.sub.1]   [M.sub.3]/e   [y.sub.4]   [R.sub.2]

0           [M.sub.1] +   0           0
            [R.sub.2]
1           IN            1           [R.sub.2]
            [R.sub.1]     2           [M.sub.3]
            [M.sub.2] *
            [R.sub.2]