• 沒有找到結果。

高階合成中使用臆測編碼轉換技術之排程等效驗證

N/A
N/A
Protected

Academic year: 2021

Share "高階合成中使用臆測編碼轉換技術之排程等效驗證"

Copied!
67
0
0

加載中.... (立即查看全文)

全文

(1)

電機學院 IC 設計產業研發碩士班

高階合成中使用臆測編碼轉換技術之排程等效驗證

高階合成中使用臆測編碼轉換技術之排程等效驗證

高階合成中使用臆測編碼轉換技術之排程等效驗證

高階合成中使用臆測編碼轉換技術之排程等效驗證

Equivalence Checking of Scheduling with Speculative

Code Transformations in High-Level Synthesis

研 究 生:李季慧

指導教授:周景揚 教授

(2)

高階合成中使用臆測編碼轉換技術之排程等效驗證

Equivalence Checking of Scheduling with Speculative Code

Transformations in High-Level Synthesis

研 究 生:李季慧 Student:Chi-Hui Lee

指導教授:周景揚 教授 Advisor:Prof. Jing-Yang Jou

國 立 交 通 大 學

電機學院 IC 設計產業研發碩士班

碩 士 論 文

A Thesis

Submitted to College of Electrical and Computer Engineering National Chiao Tung University

in partial Fulfillment of the Requirements for the Degree of

Master in

Industrial Technology R & D Master Program on IC Design

January 2010

Hsinchu, Taiwan, Republic of China

(3)

高階合成中使用臆測編碼轉換技術之排程等效驗證

高階合成中使用臆測編碼轉換技術之排程等效驗證

高階合成中使用臆測編碼轉換技術之排程等效驗證

高階合成中使用臆測編碼轉換技術之排程等效驗證

學生:李季慧 指導教授:周景揚 教授

國立交通大學電機學院產業研發碩士班

摘 要

高階合成是一個將演算法層次的描述轉換成暫存器轉移層次設計的程序,它可以提 昇生產力。然而這轉換程序容易錯誤。排程,高階合成的子工作,是驗證高階合成中最 大的挑戰,因為排程會改變原來的執行順序。這篇論文的研究主題是排程驗證。我們提 出一個正規方法可用來驗證排程前後的描述是否相等。排程前後的描述由包含資料路徑 的有限狀態機所表示。它們一開始先被分解成有限條路徑;接著,在這些路徑中找到相 等的路徑。兩個包含資料路徑的有限狀態機的相等和兩條路徑的相等在這篇論文中被定 義。提出的方法不只適合驗證保留控制架構的排程,也適合驗證會改變控制架構的排 程。排程改變控制架構藉由合併連續的路徑或將某些程式碼在不同的基本塊中移動。由 驗證高階合成的測試程式的實驗結果顯示我們演算法可以有效地驗證排程。

(4)

Equivalence Checking of Scheduling with Speculative

Code Transformations in High-Level Synthesis

Student:Chi-Hui Lee Advisors:Prof. Jing-Yang Jou

Industrial Technology R & D Master Program of

Electrical and Computer Engineering College

National Chiao Tung University

ABSTRACT

High-level synthesis (HLS) is a process of generating a register-transfer level design from an algorithm level description. It can increase the design productivity. However, this translation process can be buggy. Scheduling, a sub-task of HLS, makes the major challenge of the HLS verification since it usually changes the original cycle-by-cycle behavior. This thesis focuses on the scheduling verification. A formal method for checking equivalence between the descriptions before and after scheduling is described. Finite state machine with datapaths (FSMDs) are used to represent both descriptions. Two FSMDs are both decomposed into finite paths, and the method finds equivalent paths between them. The equivalence of FSMDs and paths are also defined. The proposed method is suited to verify not only the scheduling preserving the control structure but also the scheduling changing the control structure by merging some consecutive paths or moving some codes across the boundaries of the basic blocks. The experimental results on several HLS benchmarks show the effectiveness of the proposed algorithm.

(5)

Acknowledgements

I greatly appreciate my advisors, Dr. Jing-Yang Jou and Dr. Juinn-Dar Huang, for their patient guidance, valuable suggestion, and encouragement during these years. I am also grateful to Che-Hua Shih and Wan-Hsien Len for their discussion and help on my research. Specially thank to all member of EDA Lab and Adar Lab for their friendship and company. Finally, I would like to express my sincerely acknowledgements to my family and my friends for their patient and support.

(6)

Contents

摘 要 ...i ABSTRACT ...ii Acknowledgements ...iii Contents ...iv List of Figures...vi

List of Tables ...vii

Chapter 1 Introduction...1

1.1 Scheduling in HLS ...2

1.2 Related Works...8

Chapter 2 Preliminaries ... 11

2.1 Finite State Machine with Data-path (FSMD) ... 11

2.1.1 Paths ...13

2.1.2 Characterization of a Path...15

2.1.3 Computational Equivalence of Paths...16

2.2 FSMD Equivalence ...17 2.2.1 Assumptions ...17 2.2.2 Computations of an FSMD...17 2.2.3 Path Covers of an FSMD...18 2.2.4 Verification Method...20 Chapter 3 Motivation...23 3.1 An Example of Speculation...23 3.2 An Example of CSE ...24

Chapter 4 Our Proposed Method ...26

(7)

4.1.1 Equivalence of Paths ...27

4.1.2 Notion ...30

4.1.3 CE Algorithm...31

4.2 Solution for CSE...33

4.2.1 Available Statement ...34

4.2.2 Notion ...36

4.2.3 Compute Available Statements ...37

4.2.4 FAS Algorithm...39

4.3 Our Algorithm ...43

Chapter 5 Experimental Results ...48

Chapter 6 Conclusion & Future Works ...53

(8)

List of Figures

Fig. 1 An Overview of HLS ...2

Fig. 2 An Example of BB-based Scheduling...4

Fig. 3 An Example of Path-based scheduling...5

Fig. 4 Code Motions ...7

Fig. 5 An Example of Common Subexpression Elimination ...8

Fig. 6 An FSMD ...12

Fig. 7 Paths ...13

Fig. 8 Compute Rβ and rβ...15

Fig. 9 Path Covers of M...19

Fig. 10 Verification Flow...22

Fig. 11 An Example of Speculation...24

Fig. 12 An Example of Safe-speculation & CSE ...25

Fig. 13 An Example of an Effective Variable ...28

Fig. 14 A Example of Speculation ...31

Fig. 15 An Example of an Available Statement ...34

Fig. 16 An Example of Lemma 1 ...36

Fig. 17 A Solution for CSE...37

Fig. 18 Compute Available Statements...39

Fig. 19 A Overview of Our Algorithm...45

Fig. 20 Our Proposed Algorithm ...46

Fig. 21 An Example of Loop Invariant...53

(9)

List of Tables

Table I Characteristics of Equivalent Cases 1 ...50

Table II Results of Equivalent Cases 1 ...50

Table III Characteristics of Equivalent Cases 2...51

Table IV Result of Equivalent Cases 2 ...51

Table V Characteristics of Not Equivalent Cases...52

(10)

Chapter 1

Introduction

High-level synthesis (HLS), also called behavioral synthesis, is a process that converts a behavior or algorithm description into an RTL (register-transfer level) circuit [1]-[3]. It is helpful to gain much higher productivity than RTL or logic synthesis. In Fig. 1, HLS consists of the following sub-tasks:

- Intermediate description generation

This task compiles a behavior description into an internal representation such as a control data flow graph (CDFG) which captures all the control and data-flow dependencies of the given behavioral description [1].

- Scheduling

Scheduling assigns operations of the behavior description to specific control steps or clock cycles under data-dependencies and constraints.

- Allocation and binding

Allocation and binding specify operations to functional units, and assign data to storage elements and interconnect units.

- Architecture generation

This task builds a controller (a finite state machine, FSM) to control the data-path, depending on the information of scheduling, allocation and binding.

(11)

Behavior Description

Intermediate Description Generation

Scheduling

Allocation & Binding

Architecture Generation RTL Description Algorithm Level Register-Transfer Level Physical Level Layout Synthesis Logic Level Logic Synthesis High-Level Synthesis System Synthesis System Level Fig. 1 An Overview of HLS

Obviously, the correctness of the HLS process is very important for the development of HLS. In HLS, scheduling usually changes the original cycle-by-cycle behavior. Moreover, many scheduling techniques may even change the control structure. Hence, most of scheduled results can not be one-to-one mapped to their original structures. Therefore, scheduling becomes the main challenge in the HLS verification. As a result, we focus on the scheduling verification. The following sections give an overview of the scheduling methodologies in HLS and a review of many previous researches of the scheduling verification.

1.1

Scheduling in HLS

Scheduling is an important task of HLS. It assigns operations of a behavior description to control steps or clock cycles under some given constraints on area or delay. Thus it impacts the tradeoff between the design cost and the performance. Scheduling algorithms, traditionally,

(12)

can be classified into two categories: data-flow-based and control-flow-based algorithms. Most of early scheduling algorithms are data-flow-based (DF-based) or basic-block-based (BB-based) algorithms. BB-based algorithms focus on taking advantage of parallelism among sequences of operations in a basic block (BB); a BB is a straight-line sequence of statements containing no branches or internal entrances or exit points. In other words, they do not change the control structure. That is, the branch states (the states have more than one outgoing edge) and the merge states (the states have more than one incoming edge) of the scheduled result can be one-to-one and onto mapped to those of the behavior description. A BB-based algorithm is either to minimize the total number of control steps under resource constraints or to minimize the resources requirement in a given number of control steps under timing constraints. List scheduling [4][5] and force-directed scheduling [6] are two well-known BB-based algorithms.

Fig. 2 shows two FSMDs, Mβ and Mα , representing the descriptions before and after BB-based scheduling. In an FSMD, a node is a state and an edge is a control step. Each edge of an FSMD consists of status and assignment statements; a status consists of predicates. A slash separates the statuses and assignment statements; “-” denotes that no status needs to be satisfied. A branch state or a merge state is depicted as a gray node. Obviously, the branch state and the merge state of Mβ have a bijective mapping to those of Mα . That is, Mβ and Mα have the same control structure.

(13)

Fig. 2 An Example of BB-based Scheduling

Control-flow-based (CF-based) algorithms focus on taking the advantage of the mutual exclusion of operations in the description by analyzing the conditional constructs. These algorithms may modify the control structure. The only goal of CF-based algorithms is to minimize the number of control steps in all sequences of operations under resource constraints. Path-based scheduling (PBS) is the main algorithm of CF-based scheduling [7]. Fig. 3 shows that PBS changes the control structure. The FSMD before PBS, Mβ , has two branch states and the FSMD after PBS, Mα , has only one.

(14)

Fig. 3 An Example of Path-based scheduling

In practice, designs tend to use significant amounts of the control flow as well as the data flow. To increase the performance and the resource utilization, many code transformation techniques such as speculation – derived from the compiler – have been employed by scheduling [8]-[15].

This thesis only discusses the global code transformation techniques. A transformation is local if it only looks at the statements in a BB; otherwise, it is global. Here, two kinds of the global code transformation techniques are introduced, code motions and common subexpression elimination (CSE).

Fig. 4 illustrates code motions. Code motions attempt to extract the inherent parallelism in designs and increase the resource utilization. They move operations across the boundaries of BBs. Each square block is a BB and the node having circular shape is a branch state or a merge state. A BB between the branch state and the merge state is called a branch BB. The solid lines represent the control flow and the dotted lines represent the direction of code motions. Fig. 4 contains following code motions:

(15)

- Duplicating down (DD): It moves operations from the BB preceding a branch state into all branch BBs. This is shown by arcs marked 1.

- Duplicating up (DU): It moves operations from the BB succeeding a merge state into all branch BBs. This is shown by arcs marked 2.

- Merging up (MU): If all branch BBs have the same operations, it moves these operations from all branch BBs to the BB preceding the branch state. This is shown by arcs marked 3.

- Merging down (MD): If all branch BBs have the same operations, it moves these operations from all branch BBs to the BB succeeding the merge state. This is shown by arcs marked 4.

- Useful move (UM): Move operations from the BB succeeding the merge state into the BB preceding the branch state as these operations are independent to all branch BBs; or vice versa. Arc 5 indicates this. It moves operations from BB3 to BB0 or from BB0 to BB3 if these operations are independent to BB1 and BB2.

- Speculation (Sp): Move operations from one of branch BBs into the BB preceding the branch state if the outputs of the system are the same. It is shown as arc 6.

- Reverse speculation (RSp): Move operations from the BB preceding a branch state into some of branch BBs if the outputs of the system are the same. It is shown as arc 7.

(16)

BB0 BB3 BB1 BB2 Control flow Code motion Branch state Merge state BB0 BB3 BB1 BB2 Branch state Merge state 1 1 3 3 5 2 2 4 4 6 7

Fig. 4 Code Motions

Fig. 5 gives an example of CSE. Gupta et al. [15] have shown that CSE can often expose opportunities for optimizations. The original FSMD is Mβ . Mα is the result of CSE. qβ0 and

qα0 are the initial states where the system starts from. In Mβ , the statements st2(e’⇐a+b) and

st3(e⇐a+b) compute the same expression “a+b”. Obviously, st2 always executes prior to st3

and no statement redefines a, b and e' between them. Therefore CSE replaces “a+b” of st3 with e' in Mα. Note that although statement st6(g⇐a+b) has “a+b”, “a+b” of st6 can not be replaced. st2 and st6 do not compute the same expression because statement st5(b⇐a+f) redefines b between st2 and st6.

(17)

Fig. 5 An Example of Common Subexpression Elimination

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

(18)

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

(19)

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.

(20)

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 = {xe | x∈O∪V and e is an arithmetic predicate or expression over I∪V} is a

(21)

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).

(a) An FSMD model M for E1 int yout; void E1(P0,P1){ int x = P0; int y = P1; int r = 1; while(x){ if(y) y = y/2; else{ x = x/2; r = r+1;} }//endwhile r = r * 2; yout = r; }//endofE1 (b) The behavior E1 in C M = <Q, q0, I, O, V, f, h> Q = {q0, q1, q2, q3}; I = {P0,P1}; O = {yout}; V = {x,y,r} f(q0,TRUE) = q1 , f(q1,!x) = q2 , f(q2,TRUE) = q0 , f(q1,x) = q3 , f(q3,y)=q1 , f(q3,!y) = q1 ; h(q0,TRUE) = {xP0, yP1, r1}, h(q1,!x) = {r r*2}, h(q2,TRUE) = {youtr},

h(q1,x) = Ø, h(q3,y) = {yy/2}, h(q3,!y) = {xx/2, r r +1}.

(c) The details of M Fig. 6 An FSMD

(22)

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, qiqj .

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.

(23)

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 yg(y), the predicate c(g(y)) is true before yg(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 “ca+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,

(24)

(a ≤ x) & (x < a+d)” and “rβ = <ϖβ, οβ> = <<a*b, b, a+d, d, a*b+a+d>, [o1a, 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 “xa+c” will not redefine the “x” of “x < c”. And only the

initial value “a + d ” substitutes for “c” of “x < c” in “qβ3→qβ4”.

q 3 q 2 q 1 a ≤ x / c ⇐ a + d x < c / x ⇐ a + c, o2 ⇐ a q 4 - / a ⇐ a * b, o1 ⇐ a R = (a ≤ x) & (x < a+d)

r = <s , O > = <<a*b, b, a+d, d, a*b+a+d>, [o1 ⇐ a, o2 ⇐ a * b]> R : a ≤ x

r : <<a, b, a+d, d, x>, - >

R : a ≤ x

r : <<a*b, b, a+d, d, x>, [o1 a]>

R : (a ≤ x) & (x < a+d)

r : <<a*b, b, a+d, d, a*b+a+d>, [o1⇐a, o2 a*b]> R : Ø

r : <<a, b, c, d, x>, - >

Fig. 8 Compute Rβ and rβ

2.1.2

Characterization of a Path

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 “β = qiqk” and

“α = qkqj” are paths of an FSDM M and β is a preceding path of α ; their characteristic

(25)

α 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α .

(26)

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

(27)

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.

(28)

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

(29)

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, 0in.

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

(30)

equivalent path in Mα . Because scheduling may change the control structure, a path “β =

qβiqβj” of Pβ in Mβ may not find a computationally equivalent path in Mα . The path

extension method, proposed by Karfa et al [26], is a solution to handle this situation. It extends a path to build a new path cover. The path extension method extends β with following steps:

1. Find the path sets ps and pe.

1) ps is the set of all paths of Pβ ending at qβj .

2) pe is the set of all paths of Pβ starting from qβj .

2. For each path βs of ps, concatenate βs and each path in pe. Bm is the set of all such

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β . Then, it starts from the reset states to find a computationally equivalent path from Mα for each path of Pβ . First, it finds “β = qβiqβj” from Pβ depending on the corresponding states

(qβi , qαm), and then it find a computationally equivalent path in Mα . If a computationally

equivalent path “α = qαmqαn” is found, it records the paths (β,α) as the computationally

equivalent paths and their end states (qβj , qαn) as the corresponding states. But if a

computationally equivalent path is not found, extend path β to build a new path cover, Pβ . 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α

(31)

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.

(32)

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 “bx+y” from “qβ1 → qβ3” to “qβ0 → qβ1” and generates Mα . The left computations are “µβl = qβ0 → qβ1 cqβ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> & [outx–y+1]” and “(x<y) & <x–y, x+y, x<y, x–y+1> & [outx–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

(33)

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(ea+b) from “qβ1cqβ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(ga+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 “ge' ”.

Karfa’s algorithm fails in this case. At first, it calculates that “qβ0 → qβ1 ≃

(34)

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 q - / g ⇐ a + b q 0 q - / c ⇐ a < b c / e a + b, d ⇐ a + d q q !c / d ⇐ a + f - / c ⇐ a < b, e' a + b c / e e', d ⇐ a + d !c / d ⇐ a + f - / g e'

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.

(35)

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:de” 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:xa+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.

(36)

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βiqβ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 “da+v” uses “v”. Others have no statement having “v” as a used variable. However,

“da+v” is always executed after the statement “va+1” redefining v. Therefore, there

(37)

q0 q2 q4 M q5 !t / v⇐ a + 1 t / d⇐ a + 1 - / a⇐ in1, b⇐ in2 - / d⇐ a + v - / out⇐ d q6 !b / d⇐ d + 1 b /

-Fig. 13 An Example of an Effective Variable

Definition 14 Equivalence of two paths (β ≈α) Two paths, β of Mβ and α of Mα , are equivalent if

1) Rβ =Rα, over Vβ∩Vα and

2) οβ =οα, over Vβ∩Vα and

3) ∀vi∈Vβ∩Vα and its final value in updated variable set are eβ∈ϖβ and eα∈ϖα ,  eβ = eα, over Vβ∩Vα or

 “vi” is NOT an effective variable of β in Mβ and of α in Mα.

Clearly, if β ≃α, β ≈α . The equivalence of two walks is defined in the similar way.

Definition 15 Equivalence of two walks (ω1≈ω2) Two walks, ω1 of Mβ and ω2 of Mα , are equivalent if

1) Rω1 = Rω2, over Vβ∩Vα and

2) οω1 = οω2, over Vβ∩Vα and

(38)

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 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, 0in.

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αjQα , is a CSP and there exists paths, β = qβiqβm and α = qαjqαn , such that β ≈α .

(39)

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 “bx+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 “bx+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 .

(40)

q

1

q

2

!c /

d

b

+ x

c / a

⇐ x - y

M

q

0

- / c

⇐ x < y,

b

x + y

q

3

- / d

⇐ a + 1

- / out

⇐ d

q

1

q

2

!c /

b

x + y

c / a

⇐ x - y

M

q

0

- / c ⇐ x < y

q

4

- / d

⇐ a + 1

q

3

- / d

b

+ x

- / out

⇐ d

Fig. 14 An Example of Speculation

4.1.3

CE Algorithm

CE Algorithm checks whether a variable v is an effective variable of a path β of a path cover P in an FSMD M. Note that, it searches paths in M by breadth-first search (BFS) 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 qs in M [31]. That is, BFS

can discover all paths in M from the end state qβ of β .

CE Algorithm

Input: A variable v of a path β in a path cover P

Output: TRUE (v is NOT an effective variable of β ) or FALSE

CheckEffect(v,β,P){ 1 qβ = EndState(β);

(41)

2 // qβ is the source state where BFS starts from 3 llp = all paths starting from qβ in P;

4 tp = llp;

5 p = Pop(llp);

6 while(p){

7 if (p uses v) return(FALSE); 8 else if(p defines v) p = Pop(llp); 9 else{

10 qp = EndState(p);

11 pset = all paths starting from qp in P but not contained in tp;

12 tp = tp∪pset; 13 llp = llp∪pset; 14 p = Pop(llp); 15 }//endelse 16 }//endwhile 17 return(TRUE); }//endCheckEffect Proof of CE Algorithm

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

1 (Termination)

CE Algorithm has only one loop, named p-while-loop. The termination of p-while-loop depends on the number of paths in tp. Since tp is a subset of P, CE Algorithm can always terminate.

(42)

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 pv . Since line 7 is not executed, pv is not in tp.

Therefore, we can let p0 p1pi 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 pi+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(e2*ko).

4.2

Solution for CSE

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

(43)

4.2.1

Available Statement

Definition 19 Available statement st of a state q

A statement st:ve 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. “q0 → q1 → q2 → q3 → q4 ” is the only one walk from q0 to q4 . Since “b” of

“s1:ab+c” is redefined in “q1 → q2 ”, s1 is NOT an available statement of the state q2. On the contrary, “s2:ab+c” is available at the state q4 since the walk from q0 to q4 has s2 and between s2 and q4 , all variables of s2 are not redefined.

Fig. 15 An Example of an Available Statement

(44)

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'.

(45)

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) = {“ca<b”, “e'a+b”} and in(qα1) = {“ca<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,

(46)

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βiqβ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(β).

(47)

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 from qβi should have the same in set. Therefore, in(qβi) = in(β) for each β starting at qβi.

Fig. 18 gives an example of how to compute available statements of cutpoints. Mα is a partial FSMD having three cupoints (qα0, qα2, qα3) and three initial paths (α0 = qα0→qα1,

α1 = qα1→c qα2→qα3, α2 = qα1→!c qα2→qα3). At first, our algorithm compute

gen(α0), gen(α1) and gen(α2). As computing gen(α1), there are two time steps (i.e. two transitions) needed to be computed. The first transition contains two statements, “e⇐e' ” and

“d⇐a+d ”. Since “da+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 “ge' ”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

(48)

equivalent statements in out(α2) in order, then in(qα3) = {“e'a+b”, “cd+e”, “ge' ”}. q 0 q q q - / c ⇐ a < b, e' a + b c / e e', d ⇐ a + d !c / d ⇐ a + f - / c ⇐ d + e, g e'

in(q ): Ø

in(q ):

1.c ⇐ a < b,

1.e' ⇐ a + b

in(q ):

1.e' ⇐ a + b,

2.c ⇐ d + e,

2.g ⇐ e'

gen(

):

1.d ⇐ a + f,

2.c ⇐ d + e,

2.g ⇐ e'

out(

):

1.e' ⇐ a + b,

2.d ⇐ a + f,

3.c ⇐ d + e,

3.g ⇐ e'

out(

) = gen(

):

1.c ⇐ a < b,

1.e' ⇐ a + b

gen(

):

1.e ⇐ e',

2.c ⇐ d + e,

2.g ⇐ e'

out(

):

1.e' ⇐ a + b,

2.e ⇐ e',

3.c ⇐ d + e,

3.g ⇐ e'

Fig. 18 Compute Available Statements

4.2.4

FAS Algorithm

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 q0 and initial path cover P0 gen(β) has been computed for each initial path

數據

Fig. 2 An Example of BB-based Scheduling
Fig. 3 An Example of Path-based scheduling
Fig. 4 Code Motions
Fig. 5 An Example of Common Subexpression Elimination
+7

參考文獻

相關文件

While in respect of vipa`syanā, the focus is the observation of aggregates, bases, dependent origination, nutriments, truths, elements and sensation. In the

during daytime. The barn owl is endangered because people are moving to barns and also because mice eat chemicals and the owls eat the mice and they die. 57). Stage 2:

(d) While essential learning is provided in the core subjects of Chinese Language, English Language, Mathematics and Liberal Studies, a wide spectrum of elective subjects and COS

The localization plays important role in supersymmetric (exact solvable) field theory. A special Wilson loop is also solvable by

In section29-8,we saw that if we put a closed conducting loop in a B and then send current through the loop, forces due to the magnetic field create a torque to turn the loopÆ

magnetic field lines that pass through the loop is

Midpoint break loops are useful for situations where the commands in the loop must be executed at least once, but where the decision to make an early termination is based on

` Sustainable tourism is tourism attempting to make a low impact on the environment and local culture, while helping to generate future employment for local people.. The