# Application of high-level decision diagrams for simulation-based verification tasks/Korgtaseme otsustusdiagrammide kasutamine simuleerimisel pohinevas riistvara verifitseerimisel.

1. INTRODUCTIONTraditional design representation models are based on HDLs (e.g. VHDL or Verilog). However, a number of drawbacks are related to the application of HDLs-based models in verification.

The awkwardness and usually even inability of HDLs to represent complex temporal assertions has caused introduction of languages, especially dedicated for this purpose, such as the Property Specification Language (PSL). The latter one in turn is not always supported by design simulation tools or this support may be expensive. The attempts to unify design implementation and its properties' representations normally result in creation of large hardware checkers that assume significant restrictions on the initial assertion functionality. At the same time a comprehensive verification coverage measurement, based on the HDL model, may require complicated HDL code manipulations, resulting in inefficient resource consumption.

In this paper we address the main simulation-based hardware verification issues that are speed and accuracy of the verification process. We target these issues by exploiting the advantages of the HLDD-based modelling formalism. The main contribution of this paper is the combination of assertion checking and coverage analysis approaches into a single homogeneous HLDD-based dynamic functional verification flow. Previous research, including [1], has shown that HLDDs are an efficient model for design simulation and convenient for diagnosis and debug.

The paper is organized as follows. Section 2 defines the HLDD graph model, discusses its compactness types and describes the HLDD-based simulation process. HLDD-based structural coverage analysis is discussed in Section 3. Here the most popular coverage metrics such as statement, branch and condition are considered. Section 4 discusses application of the HLDD for assertion checking. For this purpose a brief description of IEEE std PSL as a language for assertions entry is provided. Further, the main issues of the approach itself, such as temporal extension for HLDD (THLDD), hierarchical creation of THLDDs and the THLDD assertion checking process, are discussed. Section 5 provides the experimental results, and finally conclusions are drawn.

2. HIGH-LEVEL DECISION DIAGRAMS

Various kinds of Decision Diagrams (DD) have been applied for design verification and test for about two decades. Reduced Ordered Binary Decision Diagrams (BDD) [2] as canonical forms of Boolean functions have their application in equivalence checking and in symbolic model checking.

In this paper we consider a decision diagram representation called High-Level Decision Diagrams (HLDDs) that can be considered as a generalization of BDD. There exist a number of other word-level decision diagrams such as multi-terminal DDs (MTDDs) [3], K*BMDs [4] and ADDs [5]. However, in MTDDs the non-terminal nodes hold Boolean variables only. The K*BMDs, where additive and multiplicative weights label the edges, are useful for compact canonical representation of functions on integers (especially wide integers). The main goal of HLDD representations, described in this paper, is not canonicity, but ease of simulation. The principal difference between HLDDs and ADDs lies in the fact that ADDs edges are not labelled with activating values. In HLDDs the selection of a node activates a path through the diagram, which derives the needed value assignments for variables.

The HLDDs can be used for representing different abstraction levels from RTL (Register-Transfer Level) to TLM (Transaction Level Modelling) and the behavioural level. HLDDs have proven to be an efficient model for simulation and diagnosis since they provide for a fast evaluation by graph traversal and for easy identification of cause-effect relationships [1]. The HLDD model itself is not a contribution of this paper.

2.1. Definition of the HLDD modelling formalism

In the following we give a formal definition of High-Level Decision Diagrams. Let us denote a discrete function y = f(x), where y= ([y.sub.1], ..., [y.sub.n]) and X = ([x.sub.1], ..., [x.sub.m]) are vectors defined on X = [X.sub.1] x ... x [X.sub.m] with values y [member of] Y = [Y.sub.1] x ... x [Y.sub.m] and both, the domain X and the range Y are finite sets of values. The values of variables may be Boolean, Boolean vectors or integers.

Definition 1. A HLDD, representing a discrete function y = f(x), is a directed acyclic labelled graph that can be defined as a quadruple [G.sub.y](M, E, Z, [LAMBDA]), where M is a finite set of vertices (referred to as nodes), E is a finite set of edges, Z is a function, which defines the variables labelling the nodes, and [LAMBDA] is a function on E.

The function Z([m.sub.i]) returns the variable [x.sub.k], which is labelling node [m.sub.i]. Each node of a HLDD is labelled with a variable. In special cases, nodes can be labelled with constants or algebraic expressions. An edge e [member of] E of a HLDD is an ordered pair e = ([m.sub.1], [m.sub.2]) [member of] [E.sup.2], where [E.sup.2] is the set of all the possible ordered pairs in set E. [LAMBDA] is a function on E, representing the activating conditions of the edges for the simulating procedures. The value of [LAMBA](e) is a subset of the domain [X.sub.k] of the variable [x.sub.k], where e = ([m.sub.i], [m.sub.j]) and Z([m.sub.i]) = [x.sub.k]. It is required that [Pm.sub.j] = {[LAMBDA](e)|e = ([m.sub.i], [m.sub.j]) [member of] E} is a partition of the set [X.sub.k] Figure 1 presents a HLDD for a discrete function y = f([x.sub.1], [x.sub.2], [x.sub.3], [x.sub.4]). HLDD has only one starting node (root node) [m.sub.0], for which there are no preceding nodes. The nodes that have no successor nodes are referred to as terminal nodes [M.sup.term] [member of] M.

HLDD models can be used for representing digital systems. In such models, the non-terminal nodes correspond to conditions or to control signals, and the terminal nodes represent data operations (functional units). Register transfers and constant assignments are treated as special cases of operations. When representing systems by decision diagram models, in the general case, a network of HLDDs rather than a single HLDD is required. During the simulation in HLDD systems, the values of some variables, labelling the nodes of a HLDD, are calculated by other HLDDs of the system.

[FIGURE 1 OMITTED]

[FIGURE 2 OMITTED]

Consider the example of HLDD representation of a VHDL design, containing feedback loops shown in Fig. 2. Figure 2a presents a behavioural description of the greatest common divisor algorithm, which contains variable assignments, a loop construct (WHILE) and an if-statement. Figure 2b provides an RTL implementation of the algorithm. Figure 2c shows the HLDD representation of the RTL, given in Fig. 2b. It is a system of HLDDs, where for each HDL variable a separate diagram corresponds.

Different from the well-known Reduced Ordered BDD models, which have worst-case exponential space requirements, HLDD size scales well with respect to the size of the RTL code. Let n be the number of processes in the RTL code, v be the average number of variables/signals inside a process and c be the average number of conditional branches in a process. In the worst case, the number of nodes in the HLDD model will be equal to nvc. Note, that the complexity of HLDDs is just O(n) with respect to the number of processes in the code.

Figure 3 presents a functional segment of VHDL description of an example design CovEx2 and its corresponding HLDD representation. There are three columns with numerical values to the left from the VHDL code. The first column Ln. is basically the line number, while the other two are explained further. The variables' names in CovEx2 follow the following unification rules: {V--an output variable; cS--a conditional statement; D--a decision; T--a terminal node; C--a condition}. The nodes and edges in HLDD representation are also enumerated. This enumeration is used for explanatory purposes and will be discussed in Section 3.

[FIGURE 3 OMITTED]

2.2. Representation types of the HLDD model

We distinguish three types of HLDD representations according to their compactness and with consideration of the HLDD reduction rules. These rules are similar to the reduction rules for BDDs, presented in [2] and can be generalized as follows:

HLDD reduction rule 1: Eliminate all the redundant nodes whose all edges point to an equivalent sub-graph.

HLDD reduction rule 2: Share all the equivalent sub-graphs.

The three representation types in the increasing order of compactness are:

* Full tree HLDD contains all control flow branches of the design. This type of representation includes a lot of redundancy. They introduce large space requirements and relatively slow simulation times.

* Reduced HLDD is obtained by application of the HLDD reduction rule 1 to the full tree representation. This HLDD representation is still a tree-graph. This type of representation combines the advantages of full-tree representation and minimized representation.

* Minimized HLDD is obtained by application of both HLDD reduction rules 1 and 2 to the full tree representation. This representation is the most compact of the three.

Different design verification tasks may require different HLDD representation types. For example, as it will be shown in Section 3, the compactness of HLDD representation has significant impact on the accuracy of the verification coverage analysis.

The HLDD representation, used in Fig. 3, was of the reduced type. Figures 4 and 5 represent CovEx2 design by full tree and minimized HLDDs, respectively.

2.3. Simulation using HLDDs

In [1], we have implemented an algorithm, supporting both RTL and behavioural design abstraction levels. Algorithm 1 presents the HLDD-based simulation engine for RTL, behavioural and mixed HDL description styles.

Simulation on decision diagrams takes place as follows. Consider a situation, where all the node variables are fixed to some value. For each non-terminal node [m.sub.i] [??] [M.sup.term], according to the value [v.sub.k] of the variable [x.sub.k] = Z([m.sub.i]), certain output edge e = ([m.sub.i], [m.sub.j]), [v.sub.k] [member of] [LAMDA](e) will be chosen, which enters into its corresponding successor node [m.sub.j]. Let us call such connections activated edges under the given values and denote them by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]. Succeeding each other, activated edges form in turn activated paths. For each combination of values of all the node variables there always exists a corresponding activated path from the root node to some terminal node. We refer to this path as the main activated path. The simulated value of variable, represented by the HLDD, will be the value of the variable labelling the terminal node of the main activated path.

[FIGURE 4 OMITTED]

[FIGURE 5 OMITTED]

Algorithm 1. SimulateHLDD() For each diagram G in the model [m.sub.Current] = [m.sub.0] Let [x.sub.Current] be the variable labeling [m.sub.Current] While [m.sub.Current] is not a terminal node If [x.sub.Current] is clocked or its DD is ranked after G then Value = previous time-step value of [x.sub.Current] Else Value = present time-step value of [x.sub.Current] End if [m.sub.Current] = [m.sub.Current.sup.Value] End while Assign [x.sub.G] = [x.sub.Current] End for End SimulateHLDD

In the RTL style, the algorithm takes the previous time step value of variable [x.sub.j], labelling a node [m.sub.i], if [x.sub.j] represents a clocked variable in the corresponding HDL. Otherwise, the present value of [x.sub.j] will be used. In the case of behavioural HDL coding style, HLDDs are generated and ranked in a specific order to ensure causality. For variables [x.sub.j], labelling HLDD nodes the previous time step value is used if the HLDD calculating [x.sub.j] is ranked after the current decision diagram. Otherwise, the present time step value will be used.

Let us explain the HLDD simulation process on the decision diagram example, presented in Fig. 1. Assuming that variable [x.sub.2] is equal to 2, a path is activated from node [m.sub.0] (the root node) to a terminal node [m.sub.3], labelled with [x.sub.1]. Let the value of variable [x.sub.1] be 4, thus, y = [x.sub.1] = 4. Note, that this type of simulation is event-driven since we have to simulate only those nodes that are traversed by the main activated path.

3. HLDD-BASED COVERAGE ANALYSIS

Hardware verification coverage analysis is aimed to estimate quality and completeness of the performed verification. It plays a key role in simulation-based verification and helps to find an answer to the important yet sophisticated question of when the design is verified enough. The main focus in this paper is on the structural coverage (code coverage) for simulation-based verification as the most widely used in practice. This section describes how a number of traditional code coverage metrics [6,7] can be analysed, based on the HLDD model.

3.1. Statement coverage analysis

The statement coverage is the ratio of statements, executed during simulation, to the total number of statements under the given set of stimuli.

The idea of statement coverage representation on HLDDs was proposed in [8] and developed further in [9]. The statement coverage metric has a straightforward mapping to HLDD-based coverage. It maps directly to the ratio of nodes [m.sub.Current], traversed during the HLDD simulation presented in Algorithm 1 (Subsection 2.3), to the total number of the HLDD nodes in the DUV's (Design Under Verification) representation. The appropriate type of HLDD representation for the analysis of both, statement and branch coverage metrics, is the reduced one. The variations in the analysis, caused by different HLDD representation types, are discussed further.

Let us consider the VHDL description of the CovEx2 design, provided in Fig. 3. The numbers in the second column (Stm.) correspond to the lines with statements (both conditional and assignment). The 20 HLDD nodes of the two graphs in the same figure correspond to the 18 statements of the VHDL segment. Covering all nodes in the HLDD model (i.e. full HLDD node coverage) corresponds to covering all statements in the respective HDL (100% statement coverage). However, the opposite is not true. HLDD node coverage is slightly more stringent than HDL statement coverage. Please note that some of the HDL statements have duplicated representation by the HLDD nodes. This is due to the fact that HLDD diagrams are normally generated for each data variable separately. Please consider statements 1 and 2 with asterisk '*' in VHDL representation and additional indexes in HLDD (Fig. 3). They are represented twice by the nodes of both variables V1 and V2 graphs, and therefore there are 20 HLDD nodes in total.

The fact that HLDD node coverage is slightly more stringent than HDL statement coverage is caused by their property to better represent the actual structure of the design. For example, if one statement in a design description by VHDL can be accessed by several execution paths, it will be represented by a number of nodes (or sub-graphs) in the corresponding graph when reduced, or full-tree HLDD representations are used.

3.2. Branch coverage analysis

The branch coverage metric shows the ratio of branches in the control flow graph of the code that are traversed under the given set of stimuli. This metric is also known as decision coverage, especially in software testing [7], and arc coverage. In a typical application of branch coverage measurement, the number of every decision's hits is counted. Note, that the full branch coverage comprises full statement coverage.

Similar to the statement coverage, branch coverage also has very clear representation in the HLDD model (also initially proposed in [8] and developed further in [9]). It is the ratio of every edge [e.sub.active], activated in the simulation process, presented by Algorithm 1 (Subsection 2.3) to the total number of edges in the corresponding HLDD representation of the DUV.

Let us consider the VHDL segment in Fig. 3. Here, the third column (Dcn.) numbers all 13 branches (aka decisions) of the code. The edges in the HLDD graphs, provided in Fig. 3, represent these branches and are marked by the corresponding numbers (underlined). Covering all the edges in a HLDD model (i.e. full HLDD edge coverage) corresponds to covering all branches in the respective HDL. However, similarly to the previously discussed statement on coverage mapping, here the opposite is also not true and HLDD edge coverage is slightly more stringent than HDL branch coverage.

Please note that some of the HDL branches also have duplicated representation by the HLDD edges. This is due to the same reason as with HLDD nodes. In Fig. 3 they are marked by '*' and by additional subscript indexes.

The HLDD-based approaches for statement and branch coverage metrics can further be extended for other metrics of structural verification coverage such as state coverage (aka FSM coverage), data flow coverage and others. In the first case the graph or graphs for the state variable should be analysed. The second one would require strict HLDD model partitioning by the variables sub-graphs and would map to the coverage of all single paths from terminal nodes to the root nodes separately in all variables' HLDD sub-graphs.

3.3. Condition coverage analysis

Condition coverage metric reports all cases of each Boolean sub-expression, separated by logical operators or and and; in a conditional statement it causes the complete conditional statement to evaluate the decisions (e.g. 'true' or 'false' values) under the given set of stimuli. It differs from the branch coverage by the fact that in the branch coverage only the final decision, determining the branch, is taken into account. If we have n conditions, joined by logical and operators in a logical expression of a conditional statement, it means that the probability of evaluating the statement to the decision 'true' is [1/2.sup.n] (considering pure random stimuli for the condition values). Calculation of the condition coverage, based on HDL representation, is a sophisticated multi-step process. However, the condition coverage metric allows discovering information about many corner cases of the DUV.

In this section we discuss an approach for condition coverage metric analysis, based on the HLDD model. The approach is based on a hierarchical DUV representation, where the conditional statements with complex logical expressions (normally represented by single nodes in HLDD graphs) are expanded into separate HLDD graphs.

Let us consider the example design CovEx2, provided in Fig. 3. It contains the following 6 conditional statements:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

The HLDD expansion graphs for these conditional statements are provided in Fig. 6. Here the terminal nodes are marked by background colors according to different decisions for better readability.

These 6 expansion graphs can be considered as sub-graphs, representing "virtual" variables (because they are not real variables of the CovEx2 VHDL representation) cS1-cS6. Thus together with the two HLDD graphs for variables V1 and V2 (Fig. 3) these sub-graphs compose hierarchical HLDD representation of the design (altogether 8 graphs). Here we choose graphs from Fig. 3, because accurate condition coverage analysis requires reduced type of HLDDs.

The full condition coverage metric maps to the full coverage of terminal nodes of the conditional statements expansion graphs during the complete hierarchical DD system simulation with the given stimuli. The size of the items' list C I for this coverage metric is:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

[FIGURE 6 OMITTED]

Here [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] is the number of if-type conditional statements, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] is the number of conditions in the ith conditional statement, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] is the number of case-type conditional statements and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] is the number of conditions in the kth conditional statement. E.g., list of the condition coverage items for CovEx2 is

[I.sub.C] = (2 * [2.sup.1] + 2 * [2.sup.2] + [2.sup.3]) + (3) = 23.

The main advantage of the proposed approach is low computational overhead. Once the hierarchical HLDD is constructed, the analysis for every given stimuli set is evaluated in a straightforward manner during HLDD simulation (Algorithm 1, Subsection 2.3).

The size of the hierarchical HLDDs with the expanded conditional statements grows with respect to [I.sub.C] and therefore there is a significant increase of the memory consumption. However, the length of the average sub-path from the root to terminal nodes grows linearly with the number of conditions. Therefore, since the simulation time of a HLDD has a linear dependence on the average sub-path from the root to terminal nodes, it will grow only linearly with respect to the number of conditions.

A less compact HLDD representation contains more items, i.e. nodes and edges. It means it requires more memory for the data structure storage and possibly longer simulation time, if the average sub-path from the root to terminal nodes becomes longer. However, it is potentially capable to represent the design's structure more accurately and therefore the coverage measurement may be more accurate as well.

It has been shown in [10] that the results of the analysis of the discussed coverage metrics, performed on reduced HLDDs, are more stringent that the ones with the minimized HLDDs. Moreover, compared to HDL-based analysis, the reduced HLDD-based results are always more stringent, while minimized HLDD-based ones are often less.

At the same time, the performance of the base coverage metrics analyses, based on the reduced and minimized HLDD model, is equivalent due to the fact that both models have the same average length of sub-paths from the root to terminal nodes. Compared to the full tree HLDD representation, the reduced HLDD model usually has significant performance improvement while the accuracy of the design's structure representation remains the same for the discussed coverage metrics.

4. HLDD-BASED ASSERTION CHECKING

Application of assertions checking has been recognized to be an efficient technique in many steps of the state-of-the-art digital systems design [11]. In simulation-based verification, which is the main focus of this paper, assertions play the role of monitors for a particular system behaviour during simulation and signal about satisfaction or violation of the property of interest [12].

The popularity of assertion-based verification has encouraged cooperative development of a language, specially dedicated for assertions expression. As a result, a Property Specification Language (PSL), which is based on IBM's language Sugar, has been introduced [13]. Later it has become an IEEE 1850 Standard [14]. PSL has been specifically designed to fulfill several general functional specification requirements for hardware, such as ease of use, concise syntax, well-defined formal semantics, expressive power and known efficient underlying algorithms in simulation-based verification. Research on the topic of converting PSL assertions to various design representations, such as finite state machines and hardware description languages, is gaining popularity [15-18]. Probably the most well-known commercial tool for this task is FoCs [19] by IBM. The above-mentioned solutions and the approach proposed in [20] mainly address synthesis of checkers from PSL properties that are to be used in hardware emulation. The application of the same checker constructs for simulation in software may lack efficiency due to target language concurrency and poor means for temporal expressions. Current approach allows avoiding the above limitations. The structure of an HLDD design representation with the temporal extension, proposed in this paper, allows straightforward and lossless translation of PSL properties. Traditionally the process of checking complex temporal assertions in HDL environment causes significant time and resources overhead. In this section, we discuss an approach to checking PSL assertions using HLDDs that is aimed to overcome these drawbacks.

4.1. PSL for assertion expression

The PSL [13,21] is a multi-flavored language. In this paper we consider only its VHDL flavour. PSL is also a multi-layered language. The layers include:

* Boolean layer--the lowest one, consists of Boolean expressions in HDL (e.g. a &&(b\\c))

* Temporal layer--sequences of Boolean expressions over multiple clock cycles, also supports Sequential Extended Regular Expressions (SERE) (e.g. {A[*3];B} |-> {C})

* Verification layer--it provides directives that tell a verification tool what to do with the specified sequences and properties.

* Modelling layer--additional helper code to model auxiliary combinational signals, state machines etc that are not part of the actual design but are required to express the property.

The temporal layer of the PSL language has two constituents:

* Foundation Language (FL) that is Linear time Temporal Logic (LTL) with embedded SERE

* Optional Branching Extension (OBE) that is Computational Tree Logic (CTL)

The latter considers multiple execution paths and models design behaviour as execution trees. The OBE part of PSL is normally applied for formal verification. Therefore, in this paper we shall consider only the FL part of PSL. In fact, only FL, or more precisely, its subset known as PSL Simple Subset, is suitable for dynamic assertion checking. This subset is explicitly defined in [139] and loosely speaking it has two requirements for time: to advance monotonically and to be finite, which leads to restrictions on types of operands for several operators. Currently in the discussed HLDD-based approach only several LTL operators without SERE support are implemented. However, as it will be shown later, the support for SERE as well as for any other language constructs can be easily added by an appropriate library extension.

Let us consider a simple example assertion, expressed in PSL:

reqack: assert always (req -> next ack).

Here reqack followed by semicolon is a label that provides a name for the assertion. assert is a verification directive from the Verification layer, always and next are temporal operators, ->is an operator from Boolean layer, while req and ack are Boolean operands that are also 2 signals in the DUV.

In the following the reqack assertion checking results are shown for 3 example stimuli sequences for signals {req, ack}:

* stimuli 1: ({0,0};{1,0};{0,1} {0,0}) - PASS (satisfied)

* stimuli 2: ({0,0};{1,0};{0,0} {0,0}) - FAIL (violated)

* stimuli 3: ({0,0};{0,0};{0,1} {0,0}) - not activated (vacuous pass)

Vacuous pass occurs if a passing property contains Boolean expression that, in frames of the given simulation trace, has no effect on the property evaluation. The property has passed not because of meeting all the specified behaviour but only because of non-fulfillment of logical implication activation conditions. The decision whether to treat vacuous passes as actual satisfactions of properties or not depends on particular verification tool. The approaches presented in this paper separate vacuous passes from normal passes of a property.

4.2. Temporally extended HLDDs

In order to support complex temporal constructs of PSL assertion, an extension for the HLDD modelling formalism has been proposed [22]. The extension is referred to as temporally extended high-level decision diagrams (THLDDs).

Unlike the traditional HLDD, the temporally extended high-level decision diagrams are aimed at representing temporal logic properties. A temporal logic property P at the time-step , [t.sub.h] [member of] T, denoted by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] where x = ([x.sub.1], ..., [x.sub.m]), is a Boolean vector and T = {[t.sub.1], ... , [t.sub.5]) is a finite set of time-steps. In order to represent the temporal logic assertion [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] a temporally extended high-level decision diagram [G.sub.P] can be used.

Definition 2. A temporally extended high-level decision diagram (THLDD) is a non-cyclic directed labelled graph that can be defined as a sixtuple [G.sub.P] = (M, E, T, Z, [LAMBDA], [PHI]), where M is a finite set of nodes, E is a finite set of edges, T is a finite set of time-steps, Z is a function, which defines the variables, labelling the nodes and their domains, [LAMBDA] is a function on E, representing the activating conditions for the edges, and [PHI] is a function on M and T, defining temporal relationships for the labelling variables.

The graph P G has exactly three terminal nodes [M.sup.term] [member of] M, labelled with constants, whose semantics is explained below:

* FAIL--the assertion P has been simulated and does not hold;

* PASS--the assertion P has been simulated and holds;

* CHK. (from CHECKING)--the assertion P has been simulated and it does not fail, nor does it pass non-vacuously.

The function [PHI]([m.sub.i], t) represents the relationship, indicating at which time-steps t [member of] T the node labelling variable [x.sub.l] = Z([m.sub.i]) should be evaluated. More exactly, the function returns the range of time-steps relative to current time [t.sub.curr], where the value of variable [x.sub.k] must be read. We denote the relative time range by [DELTA]t and calculation of variable [x.sub.l] using the time-range [PHI]([m.sub.i], t) = [DELTA]t by [x.sup.[DELTA]t.sub.l]. We distinguish three cases:

* [DELTA]t = [for all] {j, ... , k}, meaning that [x.sup.[DELTA]ij.sub.l] ^ ... ^ [x.sup.[DELTA]tk.sub.j] is true, i.e. variable [x.sub.l] is true at every time-step between [t.sub.curr+j] and [t.sub.curr+k].

* [DELTA]t = [there exists]{j, ..., k}, meaning that [x.sup.[DELTA]tj.sub.l] v ... v [x.sup.[DELTA]tk.sub.l] is true, i.e. variable [x.sub.l] is true at least at one of the time-steps between [t.sub.curr+j] and [t.sub.curr+k].

* [DELTA]t = k, where k is a constant. In other words, the variable [x.sub.l] has to be true k time-steps from current time-step [t.sub.curr]. In fact, [DELTA]t = k is equivalent to and may be represented by [DELTA]t = [for all]{k, ..., k}, or alternatively by [DELTA]t = [for exists]{k, ..., k}.

Notation event([x.sub.c]) is a special case of the upper bound of the time range, denoted above by k and means the first time-step when [x.sub.c] becomes true. This notation can be used in the three listed above THLDD temporal relationship functions [PHI]([m.sub.i], t), which creates the listed below variations of them. For [x.sup.[DELTA]t.sub.l]. where [x.sub.l] and [x.sub.c] are node labelling variables:

* [DELTA]t = [for all]{0, ..., event([x.sub.c])}, which means that variable [x.sub.l] is true at every time-step between [t.sub.curr] and the first time-step from [t.sub.curr] when variable [x.sub.c] becomes true, inclusively. This is equivalent to the PSL expression [x.sub.l] until_[x.sub.c]. The PSL expression [x.sub.l] until_[x.sub.c] can be represented by [DELTA]t = [for all]{0, ..., event([x.sub.c]) - 1}.

* [DELTA]t = [there exists]{0, ..., event([x.sub.c])} which means that variable [x.sub.l] is true at least at one of the time-steps between [t.sub.curr] and the first time-step from [t.sub.curr] when variable [x.sub.c] becomes true, inclusive. This is equivalent to the PSL expression [x.sub.l] before_[x.sub.c]. The PSL expression [x.sub.l] before_[x.sub.c] can be represented by [DELTA]t = [there exists]{0, ..., event([x.sub.c]) - 1}.

* [DELTA]t = event([x.sub.c]), which means that variable [x.sub.l] has to be true at the first time-step when [x.sub.c] becomes true. This is equivalent to the PSL expression next_next([x.sub.c])[x.sub.l].

For Boolean, i.e. non-temporal, variables [DELTA]t = 0.

Table 1 shows examples on how temporal relationships in THLDDs map to PSL expressions.

In addition, we use the notion of [t.sub.end] as a special value for the upper bound of the time range, denoted above by k; [t.sub.end] is the final time-step that occurs at the end of simulation and is determined by one of the following cases:

* number of test vectors

* the amount of time provided for simulation

* simulation interruption

The special values for the time range bounds (i.e. event([x.sub.c]) and [t.sub.end]) are supported by the HLDD-based assertion checking process. In the proposed approach the design simulation, which calculates simulation trace, precedes assertion checking process. In practice, [t.sub.end] is the final time-step of the pre-stored simulation trace.

Note, that THLDD is an extension of HLDD, defined in Section 2, as it includes temporal relationships functions. The main purpose of the proposed temporal extension is transferring additional information and giving directives to the HLDD simulator that will be used for assertions checking.

4.3. PSL assertions conversion to THLDDs

The first step in the conversion process is parsing a PSL assertion of interest into elementary entities, containing one operator only. The hierarchy of operators is determined by the PSL operators precedence specified by the IEEE1850 Standard. The second step is generation of a THLDD representation for the assertion. This process in turn consists of two stages. The first stage is preparatory and consists of a PPG (Primitive Property Graphs) library creation for elementary operators. The second stage is recursive hierarchical construction of a THLDD graph for a complex property using the PPG library elements.

A PPG should be created for every PSL operator supported by the proposed approach. All the created PPGs are combined into one PPG Library. The library is extensible and should be created only once. It implicitly determines the supported PSL subset. The method currently supports only weak versions of PSL FL LTL-style operators. However, by means of the supported operators a large set of properties, expressed in PSL, can be derived. Primitive property graph is always a THLDD graph. That means it uses HLDD model with the proposed above temporal extension and has a standard interface.

Figure 7 shows examples of primitive property graphs for two PSL operators next_e and logical implication ->.

The construction of complex THLDD properties is performed in the top-down manner. The process starts from the operators with the lowest precedence, forming the top level. Then their operands that are sub-operators with higher precedence recursively form lower levels of the complex property. For example, always and never operators have the lowest level of precedence and consequently their corresponding PPGs are put to the highest level in the hierarchy. The sub-properties (operands) are step-by-step substituted by lower level PPGs until the lowest level, where sub-properties are pure signals or HDL operations.

Let us consider a sample PSL property:

gcd_ready: assert always((not ready) and (a=b) -> next_e[1 to 3](ready)).

The resulting THLDD graph, describing this property, is shown in Fig. 8.

[FIGURE 7 OMITTED]

[FIGURE 8 OMITTED]

The construction of the property gcd_ready implies usage of the four PPGs. The nodes in the final THLDD contain signal variables and an HDL expression (a = b).

4.4. HLDD-based assertion checking

The process of HLDD-based assertion checking implies the existing HLDD simulator functionality (Algorithm 1) and its extension for assertion checking presented by Algorithm 2.

In the current implementation, HLDD-based assertion checking is a two-step process. First the DUV has to be simulated (Algorithm 1, Section 2.3), which calculates the simulation trace. This trace is a starting point for assertion checking that is performed in accordance with Algorithm 2 shown bellow. The process of checking takes into account temporal relationships information at the THLD nodes that represent an assertion.

Algorithm 2. AssertionCheck() For each diagram G in the model For t=[t.sub.min] ... [t.sub.max] [m.sub.Current] = [m.sub.0]; [t.sub.now] = t [x.sub.Current] = Z([m.sub.Current]) Repeat If [t.sub.now] > [t.sub.max] then Exit End if Value = [x.sub.Current] at F([m.sub.Current],[t.sub.now]) [m.sub.Current] = [m.sub.Current.sup.Value] [t.sub.now] = [t.sub.now+[DELTA]t] Until [m.sub.Current] [??] [M.sup.term] Assign [x.sub.G] = [x.sub.Current] at time-step [t.sub.now] End for /* t= [t.sub.min] ... [t.sub.max] */ End for End AssertionCheck

A general flow of the HLDD-based assertion checking process can be described as follows. The input data for the first step (simulation) are HLDD model representation of the design under verification and stimuli. This step results in a simulation trace, stored in a text file. The second step (checking) uses this data as well as the set of THLDD assertions as input. The output of the second step is the assertions checking results that include information about both the assertions coverage and their validity.

The stored assertion validity data allows further analysis and reasoning of which combinations of stimuli and design states have caused fails and passes of the assertions. This data also implicitly contains information about the monitored assertions coverage (i.e. assertion activity: "active" or "inactive") by the given stimuli.

5. EXPERIMENTAL RESULTS

This section demonstrates experimental results for the discussed HLDD model applications for verification coverage analysis and assertion checking. The experiment benchmarks several designs from ITC'99 benchmarks family [23] and a design gcd which is an implementation of the greatest common devisor.

Figure 9 shows comparison results obtained in [10] with the proposed methodology, based on different HLDD representations and coverage analysis, achieved by a commercial state-of-the-art HDL simulation tool from a major CAD vendor using the same sets of stimuli.

As it can be seen, the reduced HLDDs with expanded conditional nodes allow equal or more stringent coverage evaluation in comparison to the commercial coverage analysis software. For three designs (b01, b06 and b09) more stringent analysis is achieved using HLDDs. The HLDD model allows increasing the coverage accuracy up to 13% more exact statement measurement and 14% branch measurement (b09 design). While minimized HLDD require less memory compared to the reduced type, they do not suit accurate coverage analysis. Please note, that a higher coverage percentage, reported by a coverage metric for the given stimuli, means the metric is less stringent compared to another showing more potential for stimuli improvement and thus being more accurate.

Figure 10 demonstrates experimental results obtained in [8], where it was shown that HLDD-based coverage analysis has significantly lower (tens of times) computation (i.e. measurement) time overhead compared to the same commercial simulator.

[FIGURE 9 OMITTED]

The evaluation of HLDD-based assertion checking is demonstrated in Fig. 11. For the experimental results, performed in [22], a set of 5 realistic assertions has been created for each benchmark. The assertions were selected on the following basis:

* Different types of operators should be included (e.g. Boolean operators, implication, temporal operators including until);

* Different outcomes should result (fail, pass, both);

* The failure/pass frequency should vary (frequent, infrequent).

For example the assertions selected for gcd design were the following:

p1: assert always(((not ready) and (a = b)) -> next_e[1 to 3](ready)); p2: assert always (reset -> next next((not ready) until (a = b))); p3: assert never ((a /= b) and ready); p4: assert never ((a /= b) and (not ready)); p5: assert always(reset -> next_a[2 to 5](not ready)).

The assertions used for the b00, b04, b09 benchmarks had the same temporal complexity as the ones listed for the gcd design. Each assertion has been checking 2-5 signals and besides an invariance operator (always or never) contained from 1 to 3 LTL temporal operators from Table 1. SERE have not been used as they are not currently supported. Both simulators were supplied with the same sequences of realistic stimuli providing a good coverage for the assertions.

Figure 11 shows comparison of the assertion checking execution times between HLDD simulator and the commercial tool. The execution time values in the table are presented in seconds for 106 clock cycles of stimuli. Both tools have shown identical responses to the assertion satisfactions and violations occurrences. The conversion of the benchmarks representation from VHDL to HLDD has taken from 219 to 260 ms and conversion of the set of 5 assertions for each of the benchmarks from 14 to 19 ms, respectively. Please note, that these conversions should be performed only once for each set of DUV and assertions and they are comparable to the commercial CAD tools VHDL compilation times. During the experiments we have tried to use different number of time intervals with various sizes and have not observed any issues with scalability, however, proper experiments to evaluate the scalability issue are scheduled for the future.

The presented experimental results show the feasibility of the proposed approach and a significant speed-up (2 times) in the execution time, required for design simulation with assertion checking by the proposed approach compared to the state-of-the-art commercial tool.

6. CONCLUSIONS

This paper has demonstrated several advantages of the application of high-level decision diagrams for simulation-based verification.

The paper has discussed an approach to the structural coverage analysis using HLDDs. In particular, statement, branch and condition coverage metrics have been considered in details. It is important to emphasize that all coverage metrics (i.e. statement, branch, condition or a combination of them) in the proposed methodology are analysed by a single HLDD simulation tool which relies on HLDD design representation model. Different levels of coverages are distinguished by simply generating a different level of HLDD (i.e. minimized, reduced, or hierarchical with expanded conditional nodes).

An HLDD-based approach for assertion checking has also been demonstrated. The approach implies a temporal extension of HLDD model (THLDD) to support temporal operations inherent in IEEE standard PSL properties and also to directly support assertion checking. A hierarchical approach to generate THLDDs and basic algorithms for THLDD-based assertion checking were discussed.

As a future work we see integration of these HLDD-based assertion checking and coverage measurement methods for the design error diagnosis and debug solutions.

doi: 10.3176/eng.2010.1.07

ACKNOWLEDGEMENTS

This work has been supported by European Commission Framework Program 7 projects DIAMOND and CREDES, by European Union through the European Regional Development Fund, by Estonian Science Foundation (grants Nos. 8478, 7068 and 7483), Enterprise Estonia funded ELIKO Development Centre and Estonian Information Technology Foundation (EITSA).

Received 28 October 2009, in revised form 20 January 2010

REFERENCES

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

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

[3.] Clarke, E., Fujita, M., McGeer, P., McMillan, K. L., Yang, J. and Zhao, X. Multi terminal BDDs: an efficient data structure for matrix representation. In Proc. International Workshop on Logic Synthesis, Louvain, Belgium, 1993, 1-15.

[4.] Drechsler, R., Becker, B. and Ruppertz, S. K *BMDs: a new data structure for verification. In Proc. European Design & Test Conference, Paris, 1996, 2-8.

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

[6.] Piziali, A. Functional Verification Coverage Measurement and Analysis. Springer Science, New York, 2008.

[7.] Bullseye testing technology. Code coverage analysis. Minimum acceptable code coverage. URL: http://www.bullseye.com (September 28, 2009).

[8.] Raik, J., Reinsalu, U., Ubar, R., Jenihhin, M. and Ellervee, P. Code coverage analysis using high-level decision diagrams. In Proc. IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems. Bratislava, Slovakia, 2008, 201-206.

[9.] Jenihhin, M., Raik, J., Chepurov, A. and Ubar, R. PSL assertion checking with temporally extended high-level decision diagrams. In Proc. IEEE Latin-American Test Workshop. Puebla, Mexico, 2008, 49-54.

[10.] Minakova, K., Reinsalu, U., Chepurov, A., Raik, J., Jenihhin, M., Ubar, R. and Ellervee, P. High-level decision diagram manipulations for code coverage analysis. In Proc. IEEE International Biennal Baltic Electronics Conference. Tallinn, Estonia, 2008, 207-210.

[11.] International technology roadmap for semiconductors. URL: http://www.itrs.net (September 28, 2009).

[12.] Yuan, J., Pixley, C. and Aziz, A. Constraint-Based Verification. Springer Science, New York, 2006.

[13.] Accellera. Property Specification Language Reference Manual, v1.1. Accellera Organization, Napa, USA, 2004.

[14.] IEEE-Commission. IEEE standard for Property Specification Language (PSL). IEEE Std 1850-2005, 2005.

[15.] Gheorghita, S. and Grigore, R. Constructing checkers from PSL properties. In Proc. 15th International Conference on Control Systems and Computer Science (CSCS). Bucharest, Roumania, 2005, 757-762.

[16.] Bustan, D., Fisman, D. and Havlicek, J. Automata construction for PSL. Technical Report MCS05-04, The Weizmann Institute of Science, 2005.

[17.] Boule, M. and Zilic, Z. Efficient automata-based assertion-checker synthesis of PSL properties. In Proc. IEEE International High Level Design Validation and Test Workshop. Monterey, CA, 2006, 1-6.

[18.] Morin-Allory, K. and Borrione, D. Proven correct monitors from PSL specifications. In Proc. Design, Automation and Test in Europe Conference. Munich, Germany, 2006, 1-6.

[19.] IBM AlphaWorks. FoCs property checkers generator ver. 2.04. URL: http://www.alphaworks.ibm.com/tech/FoCs, (September 28, 2009).

[20.] Jenihhin, M., Raik, J., Chepurov, A. and Ubar, R. Assertion checking with PSL and high-level decision diagrams. In Proc. IEEE Workshop on RTL and High Level Testing. Beijing, China, 2007, 1-6.

[21.] Eisner, C. and Fisman, D. A Practical Introduction to PSL. Springer Science, New York, 2006.

[22.] Jenihhin, M., Raik, J., Chepurov, A. and Ubar, R. Temporally extended high-level decision diagrams for PSL assertions simulation. In Proc. IEEE European Test Symposium. Verbania, Italy, 2008, 61-68.

[23.] Corno, F., Reorda, M. S. and Squillero, G. RT-level ITC'99 benchmarks and first ATPG results. IEEE Journal Design & Test of Computers, 2000, 17, 44-53.

Maksim Jenihhin, Jaan Raik, Anton Chepurov and Raimund Ubar

Department of Computer Engineering, Tallinn University of Technology, Raja 15, 12618 Tallinn, Estonia; {maksim, jaan, anchep, raiub}@pld.ttu.ee

Table 1. Temporal relationships in THLDDs PSL expression Formal semantics THLDD construct [PHI] next_a[j to k] x x holds at all [x.sup.[DELTA]t= time-steps [for all](j, ... ,k)] between [t.sub.j] and [t.sub.k] next_e[j to k] x x holds at least [x.sup.[DELTA]t= once between [there exist]](j, ... ,k)] [t.sub.j]and [t.sub.k] next[k] x x holds at k [x.sup.[DELTA]t=k] time-steps from [t.sub.curr] x until_[x.sub.c] x holds at all [x.sup.[DELTA]T=[for all] time-steps between {0, ... ,event [t.sub.curr] and ([x.sub.c])}] the first time-step from [t.sub.curr] where [x.sub.c] holds x before_[x.sub.c] x holds at least [x.sup.[DELTA]t= once between event([x.sub.c])] [t.sub.curr] and the first time-step from [t.sub.curr] where [x.sub.c] holds next_event x holds at the first [sup.[DELTA]t= ([x.sub.c]) x time-step from event([x.sub.c]) [t.sub.curr] where [x.sub.c] holds Fig. 10. HLDD-based coverage analysis time overhead evaluation. HLDD-based analysis VHDL-based analysis time overhead time overhead b00 1 28 b04 0.9 32.2 b09 4.3 78.9 gcd 3.2 31.7 Note: Table made from bar graph. Fig. 11. HLDD-based assertion checking evaluation. HLDD-based analysis HLDD-based analysis VEDI-based analysis simulation checking total time gcd 4.87 2.07 13.52 b00 2.95 3.43 13.84 b04 3.61 5.47 19.23 b09 4.55 2.21 12.41 Note: Table made from bar graph.

Printer friendly Cite/link Email Feedback | |

Author: | Jenihhin, Maksim; Raik, Jaan; Chepurov, Anton; Ubar, Raimund |
---|---|

Publication: | Estonian Journal of Engineering |

Article Type: | Report |

Geographic Code: | 4EXES |

Date: | Mar 1, 2010 |

Words: | 7845 |

Previous Article: | 11th Baltic Electronics Conference BEC2008. |

Next Article: | Centre for Integrated Electronic Systems and Biomedical Engineering--CEBE. |

Topics: |