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_β1_c→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 “q₅→_!b q₆” starting from the end state q₅ of β . On the contrary, “v” is NOT an effective variable of β . Since for all possible walks starting from q₅ , 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 q₅ 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

 “v_i” 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 in Chapter 2.

Definition 16 M_β is contained in M_α

M_β is contained in M_α , if for each computation µβ of M_β , there exist a computation µα of M_α , such that µβ≈µα .

Definition 17 Equivalence of two FSMDs (M_β≊ Mα)

Two FSMDs M_β and M_α are equivalent, denote as M_β≊ Mα , if M_β is contained in M_α and M_α is contained in M_β .

Theorem 2 M_β is contained in 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.

The proof of Theorem 2 is similar to it of Theorem 1.

Definition 18 Corresponding state pair (CSP)

1) The pair of the reset states, q_β0∈Q_β and q_α0∈Q_α , is a native CSP.

2) The pair of states, q_βm∈Q_β and q_αn∈Q_α , is a CSP if the states, q_βi∈Q_β and q_αj∈ Q_α , is a CSP and there exists paths, β ^{= q}βi⇒q_βm and α ^{= q}αj⇒q_αn , such that β ≈α ^.

4.1.2 Notion

An example of two equivalent FSMDs, M_β and M_α , before and after scheduling employing Sp is shown in Fig. 14. Sp transforms M_β to M_α by moving “b⇐x+y” from

“q_β1→ q_β3” to “q_β0 → q_β1”. The reset states are q_β0 and q_α0 and the initial path covers are {“β0 ^{= q}β0 → q_β1 ”, “β1 ^{= q}β1 c→ q_β2 → q_β4 → q_β0 ”, “β2 ^{= q}β1 →!c

q_β3 → q_β4 → q_β0 ”} and {“α0 ^{= q}α0 → q_α1 ”, “α1 ^{= q}α1 c→ q_α2 →

q_α3 → q_α0 ”, “α2 ^{= q}α1 →!c q_α3 → q_α0 ”}. Our algorithm first compares β0 ^and α0^, and then computes “ϖβ0 = < a, x+y, x<y, d >” ≠ “ϖα0 = < a, b, x<y, d >”. It is obvious that only the final values of variable “b” are not equivalent. Since “b” is immediately used in β2 succeeding β0, it is an effective variable of β0 ^{; thus,} β0 ≉ α0 . Therefore, our algorithm extends β0 ^to β0β1 ^and β0β2, and then compares β0β1 ^and α0α1 . It results that “ϖβ0β1 = <

x–y, x+y, x<y, x–y+1 > ≠ ϖα0α1 = < x–y, b, x<y, x–y+1 >”. Similarly, our algorithm checks if

“b” is an effective variable of β0β1 ^and α0α1 ^{. In M}β , “b” is immediately redefined by

“b⇐x+y” in β0β2 . Therefore, “b” is NOT an effective variable of β0β1 ^{. In M}α , there are only two computations: α0α1 ^and α0α2 ^{. Since} α0α1 is not used or defined “b” and α0α2 always redefined “b” before using it, therefore, “b” is NOT an effective variable. As a result, we can conclude that β0β1≈α0α1 ^.

q 1 method. A state q is reachable from a state qs means that there exists a walk starting from qs

and ending at q. Then BFS can discover all reachable states from q_s in M [31]. That is, BFS can discover all paths in M from the end state q_β of β ^.

2 // q_β is the source state where BFS starts from

We prove CE Algorithm in two parts. The first part is for the termination and the second part is for the correctness.

As line 7 returns FALSE, there exists a walk starting from q_β and using “v” before any defined “v”. Therefore, “v” is an effective variable of β^.

Assume, for the purpose of contradiction, that there exists a walk ω starting from q_β and using “v” before any defined “v” as CE Algorithm returns TRUE. Without loss of generality, let ω has only one path using “v”, say p_v . Since line 7 is not executed, p_v is not in tp.

Therefore, we can let p0 p1…pi be the first part of ω where each pk is contained in tp for all k from 0 to i and let the succeeding path pi+1 of pi is not in tp. According to line 8, pi must define “v”; otherwise p_i+1 should be in tp. Then we can conclude that “v” is not an effective variable as return TRUE.

Complexity of CE Algorithm

n = the number of states of M e = the number of edges of M

ko = the number of outgoing edges of a state of M

In the worst case, p travels all edges; therefore, p-while-loop iterates at most e times. Line 11 scans all outgoing paths of a state and checks whether each path is contained in tp, it devotes O(ko*e). Therefore, the complexity of CE Algorithm is O(e²*ko).

4.2 Solution for CSE

The equivalent problem introduced by CSE can be solved if we can record all possible available statements.

4.2.1 Available Statement

Definition 19 Available statement st of a state q A statement st:v⇐e is available at a state q if

1) all possible walks from the reset state to q has st and

2) “v” and all used variables in e are not defined between the last st and q.

Fig. 15 illustrates an available statement of a state. q0 is the reset state. “q₀ →

q₁ → q_{2 →} q_{3 →} q₄ ” is the only one walk from q0 to q4 . Since “b” of

“s1:a⇐b+c” is redefined in “q1 → q₂ ”, s1 is NOT an available statement of the state q₂. On the contrary, “s2:a⇐b+c” is available at the state q₄ since the walk from q₀ to q₄ has s2 and between s2 and q₄ , all variables of s2 are not redefined.

Fig. 15 An Example of an Available Statement

An available statement st of a state q holds a main property: all variables of st are

preserved the values from the last occurrence of st to q. Therefore, a system produces the same outputs as it re-computes st again between the last occurrence of st and q. The following lemma is derived.

Lemma 1

Let statement st be available at a state q in M. M' is transformed from M by two steps:

1. Add a new paths “q _→ q' ” in M where “q _→ q' ” has only a copy st' of st.

2. Change the start states of all path starting at q to q'.

Then M ≊ M'.

We give a brief proof of Lemma 1. Since st is available at the state q, the values of all variables of st are preserved from the last occurrence of st to q for each possible computation µ having q. Therefore, let µ' of M' be the corresponding computation of µ . Clearly, they compute the same condition and the same result. Therefore, ∀computation µ ^{∈M, ∃}µ^'∈

M' such that µ ≈µ', and vice versa. As the result, M ≊ M'.

Fig. 16 gives an example of Lemma 1. M' is generated from M having an available statements “e'⇐a+b”. Then, M ≊ M'.

Fig. 16 An example of Lemma 1

Let M_β' and M_α' be transformed by Lemma 1 from M_β and M_α , respectively; then, M_β ≊ M_β' and M_α ≊ Mα'. Therefore, if M_β' ≊ Mα', M_β ≊ Mα .

4.2.2 Notion

Fig. 17 shows a solution for CSE. M_β and M_α are partial FSMDs. V_β∩V_α={c, d, e, e', f }, I={a, b}. q_β0 and q_α0 are the reset states of M_β and M_α , respectively. Before finding all equivalent paths, our algorithm computes all available statements of each cutpoint of M_β and M_α . in(q_β1) = {“c⇐a<b”, “e'⇐a+b”} and in(q_α1) = {“c⇐a<b”, “e'⇐a+b”} are the set of statements available at q_β1 and q_α1 , respectively. After computing all available statements, our algorithm compares β0 ^and α0 and computes that “ϖβ0 = < a<b, d, e, a+b, f > = ϖα0”. Then it compares paths β1 ^and α1 and computes that “ϖβ1 = < c, a+d, a+b, a+b >”≠ “ϖα1 = < c, a+d, e', e' >”. According to Lemma 1, in(q_β1) and in(q_α1) are thought of as paths; we concatenate

in(q_β1) and β1 and concatenate in(q_α1) and α1. As the result, ϖβ1 = < c<b, a+d, a+b , a+b > = ϖα1 and β1 ≃α1^.

Fig. 17 A Solution for CSE

4.2.3 Compute Available Statements

For each path β ^{= q}βi⇒q_βj of an FSMD M, gen(β^{), in(}β^{), kill(}β) and out(β) are defined.

gen(β) is the set of statements of β which are available at the end state of β. At first, gen(β^{) is} computed for each path β of M. Therefore, three groups of equations can be created, shown in (3.1). in(β) is the set of statements which are available at the start state q_βi of β taking into account all the available statements of all possible walks starting from reset state to q_βi. It is the intersection of the sets consisting of possible available statements of all preceding paths of β. Oppositely, kill(β) is a subset of in(β) and contains all statements having some variables being redefined in β^{. out(}β) is the set of statements which are available at the end state of β^{. It} is the union of gen(β) and the statements in in(β) but not in kill(β^).

1. out(β^{) = gen(}β^)∪(in(β^{) - kill(}β⁾⁾

2. in(β^{) =∩}p is a preceding paths of βout(p) (3.1)

3. in(β0) = Ø where β0 is the path starting from the reset state

Note that, in(β) for the reset state is handled as a special case because nothing is available if the FSMD has just begun at the reset state. And more important, in(β) uses intersection because an statement is available at the start state of β only if it is available at the end state of all preceding paths according to the definition of an available statement. All paths starting transitions) needed to be computed. The first transition contains two statements, “e⇐e' ” and

“d⇐a+d ”. Since “d⇐a+d ” redefines “d ” by itself, it is not available at q_α3 and can not be contained in gen(α1). And in the second transition, all its statements are available at q_α3 . Our algorithm cascades statements with their order, and then gen(α1) consists of “e⇐e' ” having order 1, “c⇐d+e” having order 2, and “g⇐e' ”having same order 2. It is worth to notice that the time is preserved by recording the order of statements and the statements with the same order are executed simultaneously. Next, our algorithm computes in and out of each path.

Since α0 starts from reset state, in(q_α0) = in(α0) = Ø and out(α0^{) = gen(}α0). Because α0 ^is the only preceding path of α1 ^and α2, this derives that in(q_α1) = in(α1^{) = in(}α2^{) = out(}α0^{). As} calculating out(α1), “c” of statement “c⇐a<b” in in(α1) is redefined in α1; thus, out(α1^{) is} the union of gen(α1) and the rest statements of in(α1^{), “e'}⇐a+d ”. out(α2) is computed in the similar way. Finally, our algorithm computes in(q_α3). Since there are only two preceding paths α1 ^and α2 ^{of q}α3, in(q_α3) is the intersection of out(α1^{) and out(}α2). From out(α1), we find all

equivalent statements in out(α2) in order, then in(q_α3) = {“e'⇐a+b”, “c⇐d+e”, “g⇐e' ”}.

The algorithm of computing all available statements in an FSMD M is shown below. Note that the initial paths have been sorted by BFS and the gen set of each path has been calculated.

FAS Algorithm

Input: An FSMD M with reset state q₀ and initial path cover P₀ gen(β) has been computed for each initial path

Output: in(β) set for each initial path

FindAvailableStatement(M){

26 }//endwhile(pp)

FAS Algorithm has only two loops, change-while-loop and pp-while-loop. Pp-while-loop depends on the number of paths in llp. Since llp is the initial path cover, llp is finite and pp-while-loop can terminate for each iteration of change-while loop.

Then prove change-while-loop can terminate. A walk starting from the reset set is called an r-walk. Change-while-loop depends on the number of all possible r-walks. The paths starting from the reset state have the constant out set, and then each other path can compute the constant in set from an intersection of the constant out sets of all possible preceding r-walks. Let Wp be the set consisting of those possible preceding r-walks for a path.

Let l1 be a loop and let B be an in set of l1. Let’s pass B through l1 and compute the out set B' of l1 with the rule (3.1). Clearly, as passing B∩B' through l1 for any number of runs, even infinite, we always compute the same constant B'. In other words, let Wf be a subset of Wp and each walk, called rf-walk, of Wf has either no loop or only one. The intersection of the out set of all walks in Wp is same as it in Wf. Therefore, the constant in set of each path is an intersection of the constant out sets of finite walks.

Since llp is the initial path cover sorted by BFS, after the first run of pp-while-loop, each path has an initial in set of an r-walk or an intersection of some r-walks. After a finite runs of change-while loop, the constant out sets of all preceding r-walks containing no loop for a path are computed. (An r-walk containing no loop may have reverse order because of BFS; for example, let an r-walk be p1p2p3, and after BFS, the order of p3 is prior to p2 in llp.

Therefore, the r-walk needs at most 2 runs of change-while loop to compute the constant out set.) Similarly, all preceding r-walks of a path containing only one loop can compute the constant out sets after finite runs of change-while loop. Since there are finite r-walks, change-while-loop can terminate.

2 (Correctness)

Since a path has only finite preceding rf-walks and each rf-walk can compute the constant out set after finite runs of change-while loop, all available statements of a state can be computed. Assume, for the purpose of contradiction, that there is a statement st which is not available at the start state of a path p, but is in the in set of p. It means that some preceding rf-walks don’t have st or a variable of st is redefined in a preceding rf-walk. In the former case, the out sets of some rf-walks don’t contain st and the process in line 19 or line 21 will remove it. In the latter case, st will be killed by line 22 as compute the out sets of the paths defining st.

If their original out sets has st, change will be set to TRUE. As a result, all statements in the in set of p are available at the start state of p.

Complexity of FAS Algorithm

n = the number of states of M e = the number of edges of M

ki = the largest indegree of all states of M

An iteration of pp-while-loop takes O(ki) and pp-while-loop has at most e iterations.

Change-while-loop depends on the largest number of the reverse order of all r-walks and the longest loop; it has O(e) runs. Therefore, the complexity of FAS Algorithm is O(e²*ki).

4.3 Our Algorithm

According to the Theorem 2 and Definition 17, M_β is contained 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. If a set of path P_α of M_α is also a path cover of M_α, it implies that M_β ≊ M_α .

Lemma 2 M_β ≊ Mα if there exists a path cover P_β = { p_β0 , ... , p_βn } of M_β and a path cover P_α = { p_α0 , ... , p_αn } of M_α such that p_βi ≈ pαi for all i, 0 ≤ i ≤ n.

Since extending a path means to find a new path cover, we insert the cutpoints into not

Since extending a path means to find a new path cover, we insert the cutpoints into not

在文檔中 高階合成中使用臆測編碼轉換技術之排程等效驗證 (頁 29-0)