Chapter 1 Introduction
1.2 Related Works
Ernst et al [16] and Bergamaschi et al [17] propose a simulation-based verification method of HLS verification. Unfortunately, simulation is becoming inadequate with the increasing in system complexity.
Chiang et al [18] propose a model checking technique by using Petri Net model as the formal description to check the correctness of BB-based algorithms. Narasimhan et al [19]
prove the correctness of the force-directed list scheduler (FDLS) [28] algorithm in PVS [27]
and insert invariant properties as program assertions in the implementation of the FDLS algorithm. Radhakrishnan et al [20][21] propose a method based on the precondition-based correctness of register transfer split (RTS) [29] and on the completeness of RTS transformations to perform the scheduling task with the schedule table generated by the scheduling algorithm. However, those methodologies are difficult to identify properties or
complete transformations in a large and complex scheduling task.
Recently, equivalence checking technique is used to prove the functional equivalence of two designs. Equivalence checking can be directly applied to the scheduling verification. It reads descriptions before and after scheduling as inputs. If two descriptions are functionally equivalent, it works successfully; otherwise, it gives a counter example for diagnosis. Neither the knowledge of scheduling nor the creation of properties or transformations is needed.
Mansouri et al [22] introduce the critical states to define the critical path. The equivalence between critical paths of behavior description and those of scheduled description was proved using the PVS theorem prover. Kim et al [23] define the functional equivalence between two FSMDs representing the descriptions before and after scheduling and proved the equivalence with PVS. The break-points are introduced to decompose an FSMD into a set of path predicates. Both [22] and [23] assume that the control structure is not modified during scheduling. The aforementioned methodologies, [18]-[23], are only well suited to BB-based scheduling.
Eveking et al [24] represent the behavioral description and the scheduled description in LLS (language of labeled segments) language and give basic transformations to prove the computational equivalence of LLS. If the behavioral description can be transformed to the scheduled result according to the basic transformations, they are computationally equivalent.
However, the completeness of basic transformations is hard to define and the transformation from the behavioral LLS to the scheduled LLS is tough and tedious. Kim et al [25] extend the equivalence checking method of [23] to handle the scheduling employing MU and DD by concatenating the critical paths. However, the paths affected by the code motions need to be identified. Karfa et al [26] propose an equivalence checking method suited to PBS as well as BB-based scheduling. FSMDs are used to represent the descriptions before and after scheduling and they are characterized by a finite set of paths. The equivalence of FSMDs is transformed into the equivalence of paths. However, it does not support some code
transformation techniques, such as Sp and CSE.
The rest of this thesis is organized as follows. In Chapter 2, the theoretical concepts of the equivalent checking method proposed by Karfa et al [26] are discussed. Chapter 3 presents two motivational examples, and Chapter 4 describes our proposed method in details. The experimental results and analyses are provided in Chapter 5. Followed Chapter 6 gives a conclusion and identifies some directions for future works.
Chapter 2
Preliminaries
Here, we discuss a verification method and its theoretic conceptions proposed by Karfa et al [26]. Our approach is based on those conceptions and their verification method. The notion of computations, paths, and a path cover of an FSMD and the transformations between them are defined. The equivalence of two FSMDs is also derived.
2.1 Finite State Machine with Data-path (FSMD)
An FSMD was proposed by Gajski et al. in [1]. It can trivially implement the descriptions of algorithm level (or behavior level) and RT-level. FSMDs are used to represent the descriptions before and after scheduling with an additional initial state. An initial state is also called a reset state. The FSMD was defined as a 7-tuple, M = <Q, q0, I, O, V, f, h>, where 1) Q is the finite set of states,
2) q0 is the reset state, 3) I is the finite set of inputs, 4) O is the finite set of outputs, 5) V is the finite set of variables,
6) f: Q × S → Q is the state transition function,
S is the set of status expressions consisting of arithmetic predicates over I∪V, 7) h: Q × S → U is the update function of the outputs and variables, where
U = {x⇐e | x∈O∪V and e is an arithmetic predicate or expression over I∪V} is a set of variables or output assignment statements.
An FSMD is inherently deterministic. For any state q, if the status expressions s1 = s2, it implies that f(q,s1) = f(q,s2) and h(q,s1) = h(q,s2). In an FSMD, the concept of time can be thought of as the order in which the statements are executed. An example of a behavioral description and its FSMD are shown in Fig. 6. A behavior description E1 using C language is described in (b). An FSMD M in (a) represents E1 and the detail of M is shown in (c).
In an FSMD, a walk represents a sequence of transitions.
Definition 1 [26] Walk ω of M from qi to qj
A walk ω from a start state qi to an end state qj is a transition sequence of the states. It is formulated as
1 1
1 ...
i i i n
i C i C C i n j
q q q q
+ + −
+ +
→ → → = where qk∈Q for all k, i≤k≤i+n and there exits ck∈S and transition functions fk such that fk(qk, ck) = qk+1 for all k, i≤k≤i+n-1. For short, qi⇒qj .
A state of a walk is called an internal state if it is neither the start state nor the end state.
2.1.1 Paths
A path is a finite walk. Its definition and characteristic formula are described here.
Definition 2 [26] Path β of M from qi to qj
A path β from qi to qj is a finite walk where all the states are distinct or the end state is only identical to the start state of β.
Fig. 7 illustrates paths that p1 and p2 are paths and p3 is NOT a path.
Fig. 7 Paths
Definition 3 [26] Condition Rβ of a path β
The condition Rβ of β is a logical expression over I∪V which should be satisfied before executing β.
Definition 4 [26] Result rβ of a path β
The result rβ of β is an ordered pair consisting of an updated variable set ϖ and an updated output list ο after executing β and is denoted as <ϖβ,οβ>.
1) Updated variable set ϖβ is an ordered tuple <ei> of arithmetic predicates or expressions over I∪V for all variables in V and each ei represents the final value of the variable vi∈V at the end state qj.
2) Updated output list οβ is a list of the output assignment statements with the order in which the outputs occur in β.
For a path β, its condition Rβ and its result rβ can be computed by substitution.
Substitution is a symbolic execution and based on the rule: If a predicate c(y) is true after assignment statement y⇐g(y), the predicate c(g(y)) is true before y⇐g(y) [30].
Fig. 8 describes an example of how to compute Rβ and rβ of β in M by substitution. Let V
= {a, b, c, d, x}, I = {i1, i2}, and O = {o1, o2} of M. At first, the initial values are {a, b, c, d, x}
for each variable of V. Hence, at the start state qβ1 , Rβ = Ø, ϖβ = <a, b, c, d, x> and οβ = Ø.
The first transition from qβ1 to qβ2 has only one status, thus, the condition becomes “Rβ = a ≤ x”; it also has only one assignment statement “c⇐a+d ”, thus, “a+d ” substitutes for “c” and ϖβ becomes “<a, b, a+d, d, x>”. Then, the initial values for the next transition, “qβ2→qβ3”,
become {a, b, a+d, d, x}. Similarly, after executing “qβ2→qβ3 ”, the updated variable set becomes “ϖβ = <a*b, b, a+d, d, x>” and the updated output list becomes “[o1⇐⇐⇐⇐a]”. Therefore, the initial values of “qβ3→qβ4” are {a*b, b, a+d, d, x}. Finally, after “qβ3→qβ4”, “Rβ =
(a ≤ x) & (x < a+d)” and “rβ = <ϖβ, οβ> = <<a*b, b, a+d, d, a*b+a+d>, [o1⇐a, o2⇐⇐⇐⇐a*b]>”
at qβ4 are computed. Note that since the status is always prior to the assignment statements of a transition, the execution of “x⇐a+c” will not redefine the “x” of “x < c”. And only the
Depending on the aforementioned definitions and the substitution method, a path can be characterized as “Rβ (v) & rβ (v)” or “Rβ (v) & (vf =ϖβ (v)) & οβ (v)” where v∈I∪Vβ and vf ∈ Vβ .
A concatenation of a sequence of paths can also be characterized. Let “β = qi⇒qk” and
“α = qk⇒qj” are paths of an FSDM M and β is a preceding path of α ; their characteristic formulas are “Rβ(v)&(vf=ϖβ(v))&οβ(v)” and “Rα(v)&ϖα(v)&οα(v)”, respectively. Then β and
α can be concatenated, denoted as βα , and the characteristic formula of βα is “Rβ (v) & Rα (vf)
& ϖα (vf) & (οβ (v)οα (vf))”.
2.1.3 Computational Equivalence of Paths
Mβ = <Qβ , qβ0 , Iβ , Oβ , Vβ , fβ , hβ > and Mα = <Qα , qα0 , Iα , Oα , Vα , fα , hα > are two FSMDs.
Definition 5 [26] Computational equivalence of paths (β ≃α)
Let β and α be paths of Mβ and Mα , respectively. β and α are computationally equivalent, denoted as β≃α , if Rβ = Rα and rβ = rα over Vβ∩Vα .
Notice that the equivalence of paths is restricted to Vβ∩Vα . That is, it is not allowed if R and r have some variables not in the intersection and the final values of variables which are not in the intersection are ignored. An example of equivalent paths is given below.
Example 1: Let Vβ = {a, b} and Vα = {a, b, x}, then Vβ∩Vα = {a, b}. Let β and α be two paths of Mβ and Mα , respectively. Assume Rβ = Rα and both have no output assignment statements.
1. If rβ = <<a*b, b>, - > and rα = <<a*b, b, a*b + a >, - >, ignore the value of x∉Vβ∩ Vα .
⇒β ≃α .
2. If rβ = <<a*b, b>, - > and rα = <<a*x, b, a*b+a >, - >, clearly, the final value of a uses x∉Vβ∩Vα in rα .
⇒β ≄α .
2.2 FSMD Equivalence
Let Mβ = <Qβ , qβ0 , Iβ , Oβ , Vβ , fβ , hβ > and Mα = <Qα , qα0 , Iα , Oα , Vα , fα , hα > be two FSMDs representing the descriptions before and after scheduling, respectively. The objective is to verify whether Mβ behaves exactly as Mα . That is, whether they produce the same output sequences for all possible input sequences.
2.2.1 Assumptions
Since the design synthesized by HLS is usually applied to a component of a system, the interface should be unchanged after scheduling. Therefore, we have the Assumption 1.
Assumption 1:
The input set and output set of two FSMDs are identical. That is, Iβ = Iα and Oβ = Oα.
Assumption 2:
The system works in an infinite outer loop. That is, an FSMD represents a system, and every walk of an FSMD starting from the reset state can always go back to the reset state.
More specifically, every inner loop of an FSMD must have at least one exit point.
Assumption 2 is reasonable since a hardware design is usually designed to have a reset state to prevent the dead lock. According to Assumption 2, all inner loops of an FSMD can be cut by a cutpoint introduced in a latter section.
2.2.2 Computations of an FSMD
Based on Assumption 2, a walk of an FSMD from the reset state to the reset state can be seen as a complete computation. In other words, revisiting the reset state implies a termination of a computation and a beginning of a new computation. Hence, an FSMD can be thought of
as a set of computations. Then the equivalence of FSMDs can transform to the equivalence of computations.
Definition 6 [26] Computation µ
A computation µ is a finite walk from the reset state q0 to q0 and it has no intermediary occurrence of q0 .
Definition 7 [26] Computational equivalence of walks
Two walks ωβ of Mβ and ωα of Mα are computationally equivalent, denoted as ωβ ≃ωα , if R ωβ= R ωα and r ωβ= r ωα over Vβ∩Vα .
Definition 8 [26] Mβ is computationally contained in Mα (Mβ⊆Mα)
Mβ is computationally contained in Mα , denoted as Mβ⊆Mα , if, for each computation µβ
of Mβ , there exists a computation µα of Mα such that µβ ≃µα .
Definition 9 [26] Computational equivalence of FSMDs (Mβ≅ Mα)
Mβ and Mα are computationally equivalent, denote as Mβ≅ Mα , if Mβ⊆Mα and Mα⊆Mβ .
2.2.3 Path Covers of an FSMD
Since an FMSD may have inner loops, there may be infinite computations of an FSMD.
According to Section 2.1.2, a walk is a concatenation of a sequence of paths; a computation can be a concatenation of a set of paths.
Definition 10 [26] A path cover P of an FSMD M
A path cover P of M is a finite set of paths, if, for each computation of M, it can be composed of the paths of P.
Notice that a path cover of an FSMD is not unique. Fig. 9 illustrates path covers of an FSMD M. M has only two computations, one is “µ1= q0 → q1 → q2 → q3 → q4 → q6 → q0 ” and another is “µ2 = q0 → q1 → q2 → q5 →
q6 → q0 ”. P1 = {p1, p2, p3} is a path cover of M since µ1 can be composed of p1 and p2 by concatenating them and µ2 can be composed of p1 and p3. P2 = {µ1, µ2} is also a path cover of M.
Fig. 9 Path Covers of M
Therefore, following Theorem 1 is derived and it has been proved by Karfa et al [26].
Theorem 1 [26] Mβ⊆Mα if there exists a path cover Pβ = {pβ0 , ... , pβn} of Mβ and a set of path Pα = {pα0 , ... , pαn} of Mα such that pβi ≃ pαi for all i, 0≤i≤n.
Theorem 1 transforms the problem of equivalent FSMDs to the problem of equivalent paths. To find an equivalent path pαi in Mα for each pβi of Mβ , we define the corresponding states where the comparison of two paths starting from.
Definition 11 [26] Corresponding state (CS)
1) The reset states qβ0∈Qβ and qα0∈Qα are native corresponding states and
2) qβm∈Qβ and qαn∈Qα are corresponding states if qβi∈Qβ and qαj∈Qα are corresponding states and there exist paths β = qβi ⇒ qβm and α = qαj ⇒ qαn , such that β ≃α .
It is hard to find a path cover constituting all possible computations of an FSMD because of the loops of an FSMD. Therefore, Karfa et al [26] introduce the cutpoints. Each loop of an FSMD can be cut by at least one cutpoint and the set of paths between cutpoints without any intermediary occurrence of cutpoint is a path cover. According to Assumption 2, each inner loop of an FSMD must have an exit point, i.e. a branch state; hence, the reset state and the branch states are selected to be the initial cutpoints. The set of paths between the initial cutpoints without any intermediary occurrence of initial cutpoint is named an initial path cover and a path of the initial path cover is named an initial path.
2.2.4 Verification Method
Based on Theorem 1, for each path of the initial path cover P of M , we want to find an
equivalent path in Mα . Because scheduling may change the control structure, a path “β = concatenated paths and qβj is not a cutpoint now.
3. Remove each path, which is a path of ps or a path of pe, from Pβ . 4. Add all paths of Bm into Pβ .
After the process, Pβ becomes a new path cover of Mβ . A path extension is invalid if it becomes a loop or it needs to extend via the reset state.
Fig. 10 illustrates the verification flow of [26]. Two FSMDs, which are Mβ and Mα representing the descriptions before and after the scheduling, are the inputs of the algorithm.
At first, the algorithm inserts the cutpoints only into Mβ and finds initial path cover Pβ of Mβ . Note that, if β is not extensible, the algorithm fails; otherwise, it repeats the process until all paths of Pβ finding their computationally equivalent paths in Mα . Hence, Mβ⊆Mα is proved.
Then, it interchanges Mβ and Mα and repeats the process to prove Mα⊆Mβ . As both Mβ⊆Mα
and Mα⊆Mβ have been proved, Mβ≅ Mα .
<M , M > <M , M >
InsertCutpoint in M GetEquivalentPath
Fail ExtendPath
InsertCutpoint in M GetEquivalentPath
ExtendPath
Pass Fail
CheckEquivalence CheckEquivalence
Fig. 10 Verification Flow
Obviously, Karfa’s algorithm has the ability to cope with BB-based scheduling. Since BB-based scheduling does not change the control structure, the bijective mapping of cutpoints are preserved. It means that for each path of one FSMD, the algorithm can straightly find the computationally equivalent path of another one without any extension.
Karfa’s algorithm is also capable of verifying PBS. PBS only merges some consecutive paths; it doesn’t move the operations across the BB boundaries after merging the paths.
Therefore, the algorithm with path extension method is strong enough to handle PBS.
Karfa’s algorithm obviously supports some code motions: DD, DU, MU, MD, and UM through path extension; since moving the operations from one path to another path can be thought of as merging these consecutive paths. Note that a merge state is not a cutpoint, the algorithm without path extension inherently handles DD and MU.
Chapter 3 Motivation
Although Karfa’s algorithm discussed in Chapter 2 can verify the BB-based and PBS, it is still weak in handling some code transformation techniques, such as Sp, RSp, and CSE.
Following sections give two such examples and we proposed the solutions for these cases in the next chapter.
3.1 An Example of Speculation
The equivalence of two paths defined by Karfa et al can not handle the result of scheduling employing Sp or RSp. An example of Sp is shown in Fig. 11. Mβ is the original FSMD, and it is functionally equivalent to Mα . Two systems are functionally equivalent if they produce the same output sequences for all possible input sequences. Let Vβ∩Vα = {a, b, c, d}, I = {x, y} and O = {out}. The scheduler moves “b⇐x+y” from “qβ1 → qβ3” to
“qβ0 → qβ1” and generates Mα . The left computations are “µβl = qβ0 → qβ1 c→
qβ2 → qβ4 → qβ0 ” of Mβ and “µαl = qα0 → qα1 c→ qα2 → qα3 → qα0 ” of Mα shown in bold lines. Their characteristic formulas are “(x<y) & <x–y, b, x<y, x–y+1> &
[out⇐x–y+1]” and “(x<y) & <x–y, x+y, x<y, x–y+1> & [out⇐x–y+1]”, respectively.
Obviously, µβl and µαl are not computationally equivalent because <x–y, b, x<y, x–y+1> ≠
<x–y, x+y, x<y, x–y+1>; µβl is not extensible. Therefore, Mβ and Mα are not computationally equivalent. However, the conditions and outputs of µβl and µαl are equivalent; the different values won’t affect the outputs of all computations of Mβ and Mα . That is, µβl and µαl produce the same output values for any input. Thus, µβl and µαl should be equivalent. Therefore, a
definition of equivalence between paths that captures the notion of functional equivalence is needed.
Fig. 11 An Example of Speculation
3.2 An Example of CSE
Fig. 12 illustrates an example of safe-speculation (SSp) and CSE. SSp is a method to realize Sp [15]. It attempts to move se(e⇐a+b) from “qβ1c→qβ2” to “qβ0→qβ1”. Unlike Sp, it introduces a new variable “e' ” to store the value of “a+b”, and then assigns “e' ” to “e”.
After SSp, all walks starting from the reset state qα0 to sg(g⇐a+b) have se'(e'⇐ a+b) and there is no statement redefining “a”, “b” or “e' ” between se' and sg ; therefore, CSE replaces sg with “g⇐e' ”.
Karfa’s algorithm fails in this case. At first, it calculates that “qβ0 → qβ1 ≃ qα0→qα1”. Then it compares the paths, denoted in bold lines, starting from qβ1 and qα1 .
Because the expression of se is replaced in Mα , the final values of “e” are not equivalent;
therefore, the bold paths are not equivalent. However, if se'(e'⇐ a+b) is recorded in this case, both paths have the same final value “a+b” of “e”.
q 0
Fig. 12 An Example of Safe-speculation & CSE
Sp, Rsp, SSp, and CSE are common techniques in scheduling. None of the formal verification methods proposed in Section 1.2 can handle all of them. This thesis proposes an equivalence checking method for scheduling to support them, and our method is extended from Karfa’s method [26]. Following chapter describes the detail of our method.
Chapter 4
Our Proposed Method
This chapter has three sections; first one defines equivalence of paths to cope with Sp and RSp; second one gives a solution to handle CSE; the last one is the detail of our proposed algorithm. The purpose of this thesis is to check whether two FSMDs, which are used to represent the descriptions before and after scheduling, produce the same output sequences for all possible input sequences. Our assumptions and the basic theoretical conceptions, which are proposed by Karfa et al [26], are described in Chapter 2.
In the rest of this thesis, Mβ = <Qβ , qβ0 , Iβ , Oβ , Vβ , fβ , hβ > and Mα = <Qα , qα0 , Iα , Oα , Vα , fα , hα > are the behavior FSMD and the scheduled FSMD, respectively. A gray node depicted in a figure represents an initial cutpoint.
4.1 Solution for Speculation
The rest thesis will use the terminologies: a statement, a used variable, and a defined variable; therefore, we give their definitions below.
Definition 12 Statement, Use, and Define
A statement “st:d⇐e” assigns an arithmetic predicate or expression (e) to a variable (d).
Then st is said to use all variables occurring in e and to define “d ”.
Example 2: A statement “s:x⇐a+b” is said to define “x” and to use “a” and “b”. In this example, “a”, “b” and “x” are the variables of s where “a” and “b” are called used variables and “x” is called defined variable.
4.1.1 Equivalence of Paths
Assume two paths which are β of Mβ and α of Mα have the same condition and the same outputs, but their final values of some variables are not equivalent. If these final values will not be used in both Mβ and Mα , the outputs will not be affected; hence, β and α can be thought of as two equivalent paths.
Definition 13 Effective variable v of a path β
A variable v∈Vβ is an effective variable of a path β = qβi⇒qβj of an FSMD Mβ if there exists a walk which starts from qβj and uses “v” before any defined “v”.
In Fig. 13, β = q2→ q4 →q5 is a path of an FSMD M, depicted in bold line. “d ”
is an effective variable of β because “d ” is used by the walk “q5→!b q6” starting from the end state q5 of β . On the contrary, “v” is NOT an effective variable of β . Since for all possible walks starting from q5 , only the walks containing the path β have a statement
“d⇐a+v” uses “v”. Others have no statement having “v” as a used variable. However,
“d⇐a+v” is always executed after the statement “v⇐a+1” redefining v. Therefore, there exists no walk starting from q5 and using “v” before any defined “v”.
q0
-Fig. 13 An Example of an Effective Variable
Definition 14 Equivalence of two paths (β ≈α)
respectively,
eω1i = eω2i, over Vβ∩Vα or
“vi” is NOT an effective variable of ω1 in Mβ and of ω2 in Mα.
The equivalence of FSMDs is similar to the computational equivalence of FSMDs defined
The equivalence of FSMDs is similar to the computational equivalence of FSMDs defined