Chapter 1 Introduction
1.4 Organization of This Thesis
The remainder of this thesis is organized as follows. Chapter 2 introduces the basis of symbolic model checking, which is used as the verifier in our approach. We explain the detail of our approach to assertion checking in Chapter2. A case study and experimental result are illustrated in Chapter 4. The conclusions and future works are touched upon in Chapter 5.
Chapter 2 Preliminary
Our approach uses Symbolic Model Verifier (SMV) as a tool to check converted assertions. In this section, we introduce preliminary knowledge about Symbolic Model Checking.
2.1 Symbolic Model Checking
Symbolic Model Checking [10,11,14-16] is an automatic technique for verifying properties of a finite state model of a system. Its flow is illustrated in Figure 2.1.
Figure 2.1 Symbolic Model Checking
The general approach of symbolic model checking is to describe the finite model for the behavior of the system by giving as Kripke structure, and to define the expected property of the system as Temporal Logic. It checks whether finite model satisfies the property. If not, the counterexample is generated.
2.2 Kripke Model
Kripke Model is used to model the finite state model of the system [10]. Let AP be a set of atomic
proposition. A Kripke structure M over AP is a four touple M=(S, S0, R, L), where:
S
is a finite set of statesS
0⊆ S
is the set of initial statesR ⊆ S × S
is transition relation that must be totalL : S → 2AP is a function that labels each state with the set of atomic proposition being true in that state
2.3 State in Kripke Model
Let V = {v1, v2, … vn} be the set of system variables, the variables in V range over a finite set D.
A state of a system can be described by giving values for all of the elements in V. A state is just a
valuation s : V → D for the set of variables in V. For example,
V = {v1, v2, v3}, D = {0,1} , then
a state si is a valuation: <v1←1, v2←0, v3←1>, and thus we
derive the formula: (v1=1) ^ (v2=0) ^ (v3=1)
Figure 2.2 illustrates an example of that state in Kripke model.
[v1, ¬v2, v3]
Fig. 2.2 A State of Kripke Model
2.4 Computation Tree
Computation tree, as illustrated in Figure 2.3, is formed by designating the initial state in Kripke
structure, and then unwinding (unrolling) the structure into an infinite tree. The computation tree shows all of the possible executions starting from the initial state.
bc
ab
c
c ab c
c bc
ab
unwinding
Figure 2.3 Unwinding Computation Tree
2.5 Computation Tree Logics
The formulae of computation tree logics are constructed from path quantifiers and temporal
operators:
1. Path quantifier:
A—“for every path”
E—“there exists a path”
2. Temporal modality:
Xp—p holds next time
Fp—p holds sometime in the future Gp—p holds globally in the future pUq—p holds until q holds
Chapter 3
Proposed Approach
In this chapter, we will describe our overall approach. It is organized as the following sections.
Section 3.1 defines the problem. Section 3.2 gives an input example. Section 3.3 introduces the framework. Section 3.4 determines the input language. Section 3.5 describes partitioning. Section 3.6 explains conversion techniques. Section 3.7 depicts some conversion examples. Section 3.8 elucidates verifying process. And then finally, section 3.9 demonstrates a complete example.
3.1 Problem Formulation
In our approach, the input is design assertions written in assertion language. The goal is to find out whether there are conflicts among input assertions. If yes, the approach will report which assertions are
conflict and generate the counterexamples. The brief flow of our approach is illustrated in Figure 3.1.
Figure.3.1 The Brief Flow
3.2 Input Example
Here is a simple example of input assertions:
Assertion-i:
assert Ai always {@a; @b; @c} => eventually {@x; @y};
Assertion-j:
assert Aj never {@b; [2:5]; @x};
Assertion-k:
assert Ak always {@a; @b; @c} before {@x; @y; @z};
Our approach will check whether there are conflicts among these assertions.
3.3 Framework
Figure 3.2 illustrates the framework of our approach to assertion checking. The proposed approach contains three portions. The first one is to partition input assertions into assertion groups. In the second portion, for each assertion group, we convert each assertion into deterministic finite automata (DFA) and their respective properties. Finally, we take those DFA and properties to run symbolic model checking. It will report contradiction and its counterexample if there is any conflict among input assertions. We will describe each portion in details in the following sections.
Checking Report Verify DFA and Properties with SMV Convert Assertions into
DFA and Properties Partition Assertions into
Assertion Groups Assertions
Figure 3.2 The Framework
3.4 Input Language
Assertion languages for design verification such as Property Specification Language (PSL)/(Sugar) [17], OpenVera [18], and e [19,20] have been gaining in popularity and applied in industry. In order to implement our approach, we formally define an assertion language as our input assertion language. For
simplicity, we choose the common set of above three popular assertion languages (PSL, OpenVera and
e) as our input assertion language and call it a PSL-like language. The common set of above languages
are the most frequently used common part of general design assertion languages, which is capable of
modeling most of real world design properties. Our simplified PSL-like assertion language has following characteristics and assumptions:
It consists of common basic parts of popular assertion languages.
It has rigorously well-defined formal semantics and concise syntax.
It cover all major temporal layer expressions and Boolean layer expressions.
All primitive events are assumed clocked and synchronized.
Properties are restricted to time move forward from left to right sequentially.
The assumption we made is only for the purpose of simplicity on implementation. It does not lose the generality of common assertion languages. The major constructs of our language are described
Figure 3.3. For the syntax detail, please refer to "BNF Grammar of PSL-like Assertion Language in
Appendix A.
Assertion := assert Id once TE
Figure 3.3 Constructs of our Language
In this thesis, we focus on the temporal layer expressions of general assertion languages, since this
is the heart of the language. The temporal layer expressions are used to define properties, which
describe Boolean expressions related over time. Temporal layer expression is sophisticated enough to
describe the complex behavior of specification.
3.5 Partitioning Assertions
To alleviate the state explosion problem in formal model checking, we come up with a reduction solution. That is, we put together the assertions which share common event variables to run model checking. That is because only the assertions which have common event variables are possible to have conflict. Hence we define an assertion group for our approach. An assertion group contains some
assertion members, such that assertion members may have some common event variables. Therefore, the assertions belonging to different groups must not have any common variable.
Based on this idea, all input assertions will be partitioned into several assertion groups. An example of assertion groups is illustrated in Figure 3.4, where EV are event variables.
Input assertions:
A1: (EV1, EV2, EV4) A2: (EV3, EV6, EV8) A3: (EV2, EV4, EV7) A4: (EV5, EV7) A5: (EV6, EV9)
Output assertion groups:
The group-1:
A1: (EV1, EV2, EV4) A3: (EV2, EV4, EV7) A4: (EV5, EV7) The group-2:
A2: (EV3, EV6, EV8) A5: (EV6, EV9)
Partitioning
Figure 3.4 Partition Assertions into Assertion Groups
We apply the techniques in [21-23] to parse all input assertions and collect all event variables for building event variable table in the first pass. Then we partition all assertions by applying the algorithm illustrated in Figure 3.5.
Figure 3.5 The Partition Algorithm function partition (all_assertions):
for i=1 to i=N do { for j=i+1 to j=N do {
if (Assertion j is not empty) do {
if (Assertion i and Assertion j have common event variables) do { Assertion i := Assertion j ∪ Assertion j;
Assertion j := ∅;
};
};
};
if (any_merger_happened) do {
swap(Assertion i, Assertion last_merged );
Assertion i := ∅;
};
};
};
As the shown pseudo code in the Figure 3.5, the assertions which have common variables will be put together.
By partitioning the assertions, the runtime of symbolic model checking is greatly reduced.
Furthermore , the time complexity of this algorithm is O(N2). In most real cases, the assertions may be partitioned to tens or hundreds of groups.
3.6 Assertion Conversion Techniques
The essential part of our approach is assertion conversion. After partitioning assertions, each assertion is converted into a deterministic finite automata (DFA) and its corresponding CTL property.
The process is illustrated in Figure 3.6.
(4) Build
Figure 3.6 The Conversion Process
Before the conversion routines work, we derive the conversion templates for various assertion types and temporal operators. These templates facilitate the conversion work in the later processes. In the conversion process, the first step is to decompose the assertions into primitive sequences and to extract temporal operators. We also determine the assertion types by those decomposition and extraction.
Then the second step is to build primitive DFA. Since the assertion type and temporal operator have been known from the first step, we may decide which type to apply. In this step, the primitive sequence is also decomposed further into the passive part and/or active part.
For example, consider a part of an assertion, {@a; @b} => {@x; @y}. We define the left hand side ({@a; @b}) of the temporal operator as the passive part; the right hand side ({@x; @y}) as the active part. Once the premise condition is matched, the consequence sequence will be forced to hold. The events with active attribute in that sequence will be forced to occur. So those events should be actively driven. In terms of event correlation and contribution of stimulation for asserted argument, the event attribute of an assertion is also determined by both assertion type and temporal operator. The attribute categories are listed in Table 3.1.
Active
eventually Seq.Table. 3.1 Event Attributes
The third step is to assemble the whole composite DFA. The composite DFA is a structural DFA which is constructed by combining DFA according to assertion type and temporal operators.
The fourth step is to build Computation Tree Logic (CTL) formula. The primitive CTL formula are constructed from path quantifiers and CTL temporal modalities. The atomic proposition is directly extracted and converted from the events of original assertion. The proposition whose events have passive attribute will be specified with the "E" path quantifier because they are free event variables in that property. That means the event value depends on the path in the computation tree. On the contrary, the proposition whose events have active attribute will be specified with "A" path quantifier because their value is constrained to specific ones for the all paths. Temporal modalities in CTL are also determined by original temporal operator and assertion types. For example, if it is an atomic event of a sequence holding at the next time, just specify its temporal modality as "X".
The final step is to assemble the whole property by combining the CTL formula which were converted at previous steps and the logical connectives which are determined according to the assertion type. At the end, we get the DFA and the corresponding property by above conversion steps.
We explain the correctness of assertion conversion in our approach in Appendix B.
3.7 Conversion of Common Types of Assertions
According to assertion type and temporal operator, we pre-build the conversion templates which are used in conversion steps. In this section, we depict how to build such conversion templates for some most common used temporal operator or the assertions which use these operators.
3.7.1 Conversion Template of "sequence" Operator
Definition: A sequence is a finite series of events that represent a set of sequential behaviors, which is enclosed in curly braces.
Example: {@a; @b; not@c; @d};
Converted DFA in SMV:
As in Figure 3.7 (a), we create the leave DFA of each event variable for current state and
previous states, which keep the current event states and the previous states.
a=T
Figure 3.7 (a) The Converted Primitive DFA
Then, we construct the composite DFA by combining those leave DFA. It is illustrated in
Figure 3.7 (b) The Converted Composite DFA
Converted Property in SMV:
According to the Computation Tree Logic (CTL), the sequence could be represented as the unwinding computation tree in Figure 3.8.
d=T c=F b=T
a=T
Figure 3.8 The Computation Tree Logic
Therefore, we can describe its property with CTL formula the following:
EF(a=T & EX(b=T & EX(c=F & EX(d=T))))
3.7.2 Conversion Example of "sequence-imply-sequence" Operator
We demonstrate an example of conversion template of sequence-imply-sequence. The conversion steps are depicted in following respective figures.
Assertion example: always {@a; @b; @c} => {@x; @y}
Converted DFA in SMV:
Step 1 is to decompose the assertion into primitive sequences, they are {@a; @b; @c} and
{@x; @y}, and temporal operator "=>".
always {@a; @b; @c} => {@x; @y} Determine the assertion type by
the assertion keyword "always"
and the main temporal operator
Primitive sequence with active attribute
Figure 3.9 Decomposing The Assertion
The step 2 is to build primitive DFA. In Figure 3.10 (a), the primitive sequence {@a; @b;
@c} with passive attribute is converted into a leave DFA.
b
-1Figure 3.10 (a) The Converted DFA for the Primitive Sequence
is shown in Figure 3.10 (a). The composite DFA is shown in Figure 3.10 (b).
{@a;@b;@c}
not{@a;@b;@c}
not{@a;@b;@c}
i
{@a;@b;@c}abc
Figure 3.10 (b) The Converted Composite DFA
On the other side, the primitive sequence {@x; @y} with active attribute is converted into a leave DFA, which is shown in Figure 3.10 (c)
x y
x ← 1 y ← 1
Figure 3.10 (c) The Converted DFA
In step 3, we assemble the whole composite DFA. The composite DFA is assembled by
composing some leave DFA. The assembled DFA is illustrated in Figure 3.11.
The passive part The active part
y ← 1
Converted Property in SMV:In step 4, we build CTL formula for each decomposed primitives.
The respective converted CTL is shown in below.
always {@a; @b; @c} => {@a; @y};
EX(a=T & EX(b=T & EX(c=T -> AX(x=T & AX(y=T)) )));
In this case, we apply the CTL temporal modality "X" for each events of sequences, because they are the continuous next events in a sequence. For the passive sequence, the "E"
quantifier is specified due to there is some path for which the sequence matching codition
(@a; @b; @c) holds. On the contrary, for the active sequence, the "A" quantifier is specified
since it holds for every paths once the condition matched.
In step 5, we assemble the whole CTL property by combining the primitive CTL formula which are converted in step 4. The converted CTL property is illustrated in Figure 3.12.
SPEC EG (a=T & EX(b=T & EX(c=T -> AX(x=T & AX(y=T)) ))) ; Figure 3.12 Assemble CTL Property
The final converted CTL property for this example is:
SPEC EG (a=T & EX(b=T & EX(c=T -> AX(x=T & AX(y=T)))));
3.7.3 Conversion Example of "and" Operator
In the following section, we demonstrate the conversion results, but omit the conversion details.
Definition: An expression with length-matching "and" operator succeeds when both compound TE hold at the current cycle, and furthermore both complete in the same cycle.
Example: {@a; @b; @c} and {@p; @q; @r}
Figure 3.13 Converted DFA
Converted property in SMV:
SPEC EF((a=T & p=T) & EX((b=T & q=T) & EX(c=T & r=T)));
3.7.4 Conversion Example of "or" Operator
Definition: An expression holds on a path iff at least one of events/sequences holds on the path.
Example: {@a; @b; @c; @d} or {@p; @q}
Converted DFA in SMV:
{@a; @b; @c; @d}
{@a; @b; @c; @d} or {@p; @q}
{@p; @q}
Figure 3.14 Converted DFA Converted properties in SMV:
SPEC EF(a=T & EX(b=T & EX(c=T & EX(d=T))) | (p=T & EX(q=T)));
3.7.5 Conversion Example of "until" Operator
Definition of “@a until @b”: It holds in the current cycle iff: 1) @b holds at the current cycle or at some future cycle and 2) @a holds at all cycles up to and including the earliest cycle at which @b holds.
Example: once @a until @b
We add an additional state named as "Fail" in the converted DFA. When it enters the "Fail"
state, it means it violates the assertion.
Figure 3.15 Converted DFA Converted properties in SMV
SPEC A[a=T U b=T]
or
SPEC !EF state=Fail;
3.7.6 Conversion Example of "before" Operator
Example: always @a before @b;
Converted DFA in SMV:
Figure 3.16 Converted DFA
Converted properties in SMV:
3.7.7 Conversion Example of "repetition" Operator
repetitions of the repeat-expression such that the number falls
Example: {@a; [2:4]; @c}
Converted DFA in SMV
igure 3.17 Converted DFA
V:
Definition: any number of within the specified range.
t
4SPEC !EF state=Fail;
or
3.7.8 Conversion Example of "eventually" Operator
@c} => eventually {@x; @y}
C
Converted Property in SMV
The operator, "eventually" means that the property holds at the current cycle or at some future cycle. That is it must hold at some time in the indefinite future. To implement the checking for this assertion, we have SMV to assign value non-deterministically until it reaches the specified time upper bound. That means the assertion will hold at most of upper limit time. According to the analysis, this upper bound should be greater than the maximum depth of time step of all input assertions. That ensures the assertion will be held in finite time.
Figure 3.18 Converted DFA
SPEC EF(EG(a=T & EX(b=T & EX(c=T & AF(x=T & AX(y=T))))));
Example: always {@a; @b;
onverted DFA in SMV:
a
3.8 Verifying Assertions with SMV
After assertion conversion finishes, we apply symbol model verifier (SMV) to verify converted asse s the converted set of DFA and set of properties are fed to SMV. If
ny conflict exists, the verifier will report the counterexample. Figure 3.19 illustrates the process.
3.9 A More Complete Example of Assertion Checking
In this section, we use a complete example to demonstrate our approach, and explain its process step by step. First at all, as shown in Figure 3.20, there are six assertions in the input.
rtion . For each assertion group, a
Figure 3.19 Verify Assertions with SMV
assert A1 always {@a; @b; @c} => ev
In our approach, we partition the input assertions into assertion groups. According to the partitioning algorithm, the six are assertions are partitioned into two groups, Assertion Group 1 and Assertion Group 2, as Figure 3.21 shows.
mposed into primitive
Figure 3.21 Partitioning Result Figure 3.20 Input of the Example
We take Assertion Group 1 to demonstrate the process. In the step 1, it is deco
quences and temporal operators, and the conversion template is applied according to the decomposed result. It is illustrated in Figure 3.22.
Then at step 2, the primitive DFA are built according to decomposed primitive sequence . At step3, composite DFA is assembled by each primitive DFA and temporal operators. The converted DFA of Assertion Group 1 is depicted in Figure 3.23.
Similarly, assertion A3, assertion A5 and assertion A6 are shown in the Figure 3.24, 3.25 and 3.26 respectively.
Figure 3.23 Converted DFA from Assertion A1
A1: always {@a; @b; @c} => eventually {@x; @y; @z};
Figure 3.22 Decomposed Assertions of Assertion Group 1 y; @z};
Figure 3.24 Converted DFA from Assertion A3
Figure 3.25 Converted DFA from Assertion A5
Figure 3.26 Converted DFA from Assertion A6 A3: never {@b; [2:5]; @x};
At the step 4 and step 5, CTL formula are built and then properties are assembled with them. The onverted properties are illustrated in the following.
After the conversion is done, the converted DFA and properties are fed into SMV for checking. The port is shown in Figure 3.27.
As the Figure 3.27 shows, there are four conflicts found in this assertion group. They are DFA1
gainst Property3, DFA1 against Property5, DFA3 against Property6, and DFA6 against Property3.
ccording to our analysis from the checking results of SMV, where (DFA1,Property3) and
(DFA Property) are unilateral conflict, so they are suspected conflicts alert. That means it could be Property of assertion A1:
SPEC !EF(EG(a=T & EX(b=T & EX(c=T & !AF(x=T & AX(y=T & AX(z=T))))));
Property of assertion A3:
SPEC !EF(b=T & EX(EX(EX(x=T | EX(x=T | EX(x=T | EX(x=T)))))));
Property of assertion A5:SPEC !EF state=Fail;
Property of assertion A6:
SPEC EG((a=T | q=T) -> AX(w=T & AX(w=T & AX(w=T & AX(x=T)))));
Unilateral conflicts, suspected conflicts alerted
Mutual conflicts, definite conflicts reported
Figure 3.27 Checking Result
a A
ind
rtions. The other two, (DFA3, Property6), are m lict. That means they are definite conflicts.
eed conflict or either one of two is redundant. Therefore, users who perform our approach can inspect the result to identify the errors among the asse
utual conf
Chapter 4 Case Study
4.1 Case Description
We choose the assertions for the Bus Transaction Protocol of PCI Local Bus Specification as our case. The assertions cover Bus Transfer Control, Addressing, Byte Lane and Byte Enable, Bus Driving and Turnaround, as well as Transaction Ordering and Posting [26].
In general, the assertions consist of two parts: PCI master and PCI target. There are 41 assertions in this case study.
4.2 Experimental Environment
We implement our approach in C program and some shell scripts. They are executed on Sun Sparc Workstation with 1 GB memory on 400MHz speed.
4.3 Experimental Result
We partition the input assertions into 5 and 4 assertion groups for PCI master and PCI target pectively.
ected conflicts alerted), 1 mutual conflicts, (definite conflicts reported).
The experimental result is depicted on Table. 4.1.
Case No. of
After execution, it found:
4 unilateral conflicts (susp
PCI Master 25 5 2 1 92
PCI Target 16 4 1 0 41
Table 4.1 Experimental Result of Case Study
Chapter 5
Conclusions and Future Works
5.1 ions
We check esign assert by means of converting assertion into
corresponding DFA and pr the others using SMV.
The major features of our approach are:
Without referring the design, only the assertions required, Without need of simulation and test patterns,
Stand-alone, off-line processing, may check assertions prior to design verification, Greatly alleviating the state explosion problem of SMV.
operties and then checking each of them against
Conclus
propose a technique to d ions
5.2 Discussion
Ensuring a set of assertions without any conflict can increase our confidence in the correctness of
Ensuring a set of assertions without any conflict can increase our confidence in the correctness of