高階有限狀態機為一種硬體系統設計所採用之行為層級的設計描述方法，其狀態轉移上附有狀態轉移時執行的陳述式敘述。為了進行其與所衍生之低階有限狀態機之間的等效驗證需求，我們將在低階有限狀態機上萃取出對應高階狀態機上之狀態轉移的陳述式，再進行相對應之配對陳述式間的等效驗證。

　　過去的研究採取模擬的方式實證檢查對應陳述式的等效性，由於其組合複雜度此方法無法保証通過檢查之陳述式的完全等效，在此研究中，我們將針對已萃取出的配對陳述式間的等效驗證，提出可實行之方法與軟體設計，其中將包含下列三項系統功態的軟體設計工作：

１. 運用融合交換律、結合律與分配律之正規化做法，將各個轉換代表為等效之精簡型陳述式圖的代表法，以減少需探尋的陳述式等效空間，而降低搜尋比對時間與所衍生等效陳述式所需記憶容量。

２. 針對各衍生之等效陳述式共享其相同的同構陳述子圖結構，形成一個正規之共享陳述圖，以進一步節省記憶空間，並便利衍生陳述式間之同構比對，以改進效能。

３. 在共享陳述圖中尋找代表之陳述式與公理模式的匹配及變數的一致化，將符合公理模式的陳述式結構取代為代入一致化的變數值之對應的公理樣本，建立出公理轉換所產生的新陳述式子圖。

　　我們針對此陳述式等效驗證軟體進行實作測試。實驗結果顯示，此方法具備有應用於硬體系統設計與低階設計間之等效驗證的能力。

High-level finite-state-machine is a behavioral level hardware system design specification method. Each of its state transitions is tagged with a description of an expression executed during the corresponding state transition. In order to verify the equivalence between a high-level finite-state-machine and its deriving low-level finite-state-machine, we can extract expressions executed in state transition sequences from an annotated state to another. Then, the extracted expression can be checked against the corresponding expression in the high-level finite-state-machine for their equivalence.

Past research adopted a simulation-based validation technique to examine expression equivalence. Due to its combinatorial complexity, it can not guarantee hundred percent equivalence for expression passing the test. In this research, we designed software of our expression equivalence verification method applied on the extracted expressions. It consists of software design tasks of tree system functionalities :

1. By applying a normalization method on commutative, associative, and distributive laws, we can transform each expression into an equivalent reduced expression graph. It can reduce the size of the equivalence space to be explored in the equivalence verification process and thus reduce computation time and storage size of explored equivalent expressions.

2. For equivalent expression s explored during the verification process, we can share the common sub-expression structures and form a formal shared expression graph. We can furthermore reduce the storage size of the evolved expressions and facilitate isomorphism checking between them to improve performance.

3. In the shared expression graph, we can match its sub-expressions against axiom patterns and derive corresponding unification. Then, substitute the matched sub-expression with the corresponding axiom template with unified variable values and form a new equivalent expression graph from axiom transformation.

We carried out experiments of this expression equivalence verification method. Experimental results shows that this method obtains the equivalence verification capability to be applied between a hardware system design and its low level design.

致 謝............................................................... i
摘 要............................................................... ii
英 文 摘 要.......................................................... iii
目　錄............................................................... v
第一章 導　論....................................................... 1
1.1 研究動機..................................................... 1
1.2 研究背景..................................................... 3
1.3 研究目的..................................................... 3
1.4 論文架構..................................................... 6
第二章 基於公理之等效檢查器......................................... 7
2.1 等效檢查原理................................................. 7
2.1.1 陳述式....................................................... 7
2.1.2 公理......................................................... 8
2.2 等效陳述式圖................................................. 8
2.2.1 陳述式的等效轉換............................................. 8
2.2.2 精簡型等效陳述式圖........................................... 10
2.3 基於公理之等效檢查程序....................................... 12
2.3.1 陳述式的轉換程序............................................. 12
2.3.2 等效驗證的程序............................................... 13
第三章 共享陳述圖................................................... 15
3.1 陳述樹....................................................... 15
3.1.1 陳述樹的架構................................................. 15
3.1.2 陳述樹的正規化處理........................................... 16
3.2 共享陳述圖................................................... 18
3.2.1 共享陳述圖的建立............................................. 18
3.2.2 共享陳述圖的走訪............................................. 20
3.3 常數葉頂點................................................... 24
3.3.1 常數型態類別................................................. 24
3.3.2 常數型態階層圖............................................... 25
3.3.3 常數函數操作表............................................... 25
第四章 共享公理轉換法則代表法....................................... 27
4.1 公理轉換的代表法............................................. 27
4.2 公理模式的代表法............................................. 28
4.2.1 非交換結合律的公理模式....................................... 29
4.2.2 模式序列..................................................... 29
4.2.3 共享模式序列................................................. 32
4.2.4 交換結合律子模式............................................. 33
4.3 公理樣本的代表法與轉換程..................................... 34
第五章 匹　配....................................................... 37
5.1 匹配概述..................................................... 37
5.1.1 同步比對..................................................... 37
5.1.2 交換結合律運算頂點的匹配..................................... 38
5.2 匹配的程序................................................... 39
5.2.1 同步比對的匹配程序........................................... 39
5.2.2 交換結合律子模式的匹配程..................................... 41
5.3 變數的一致性................................................. 42
5.3.1 限定變數表................................................... 43
5.3.2 變數池....................................................... 43
第六章 實驗規劃與結果............................................... 46
6.1 實驗規劃..................................................... 46
6.2 實驗結果..................................................... 47
6.2.1 陳述式等效驗證比對類型分..................................... 47
6.2.2 陳述式等效驗證計算時間與記憶容量............................. 53
第七章 結　論....................................................... 55
參 考 文 獻.......................................................... 56

[1] T. Lee & P. H. Yu, The Design of an Axiom-Based Equivalence Verification Method, Tech. Rep. No. CAD-04-01, CAD. Lab., Dept. of Electrical Engineering, National Sun Yat-Sen University, Kao-Hsiung, Taiwan, 2004
[2] T. Lee, An Axiom-Based Equivalence Verification Method, Internal Discussion Memo, CAD. Lab., Dept. of Electrical Engineering, National Sun Yat-Sen University, Kao Hsiung, Taiwan, 2003
[3] D. Gajski,N. Dutt, A. Wu, S. Lin, High-level Synthesis : Introduction to chip and system design, Kluwer Academic Publishers, 1992
[4] A. Jerraya, H, Ding, P. Kission, M. Tahmouni, Behavioral Synthesis and Component Reuse with VHDL, Kluwer Academic Publishers, 1997
[5] D. Gajski, L. Ramachandren, “Introduction to High-level Synthesis,” IEEE Design & Test of Computers, Vol.11, No. 4, pp. 44-54, Winter, 1994
[6] D. Borrione, J. Duchina, L. Pierre, “Formalization of Finite State Machines with Data Path for the Verification of High-Level Synthesis,” Proc. IX Brazilian Symposium on Integrated Circuit Design, pp. 99-102, IEEE Computer Society Press., October 1998
[7] S. Y. Huang, K. T. Cheng, Formal Equivalence Checking and Design Debugging, Kluwer Academic Publishers, 1998
[8] S. B. Akers, “Binary decision diagram,” IEEE Trans. On computers, Vol. C-27, No. 6, pp.509-516, June 1978
[9] R. E. Bryant, “Graph-based algorithms for Boolean function manipulation,” IEEE Trans. on Computers, Vol. C-35, No. 8, pp. 677-691, August 1986
[10] S. Minato, “Implicit manipulation of polynomials using zero-suppressed BDDs,” Proc. of the European Design and Test Conference (ED&TC’95), pp. 449-454, March 1995
[11] S. Minato, “Calculation of unite cube set algebra using zero-suppressed BDDs,” Proc. of 31st ACM/IEEE Dsign Automation Conference(DAC’94), pp. 420-424, June 1994
[12] A. V. Aho, R. Sethi, and J. D. Ullman, Compilers: Principles, Techniques, and Tools, Addison-Wesley, 1986
[13] H. Samet, “Distance transform for images represented by quadtrees,” IEEE Trans. Pattern Anal. Machine Intell., Vol. 4, No. 3, pp. 298-303, 1982
[14] C. M. Hoffmann and M. J. O’Donnell, “Pattern matching in trees,” J. ACM, Vol. 29, No. 1, pp. 68-95, 1982
[15] A. V. Aho, M. Ganapathi, and S.W. K. Tjiang, “Code generation using tree matching and dynamic programming,” ACM Trans. on Programming Languages and Systems, Vol. 11, pp. 491-516, 1989
[16] Cedric Chauve, “Tree pattern matching with a more general notion of occurrence of the pattern,” Information Processing Letters, Vol. 82, No. 4, pp. 197-201, 2002
[17] D. Kuck, The Structure of Computers and Computation, Wiley, New York, 1978
[18] D. Watson, High-level Languages and their Compilers, Addison-Wesley, 1989
[19] D. A. Plaisted, “Equational reasoning and term rewriting systems,” Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 1, pp. 273-364, D. Gabbay and J. Siekmann, eds., New York, Oxford University Press., 1993
[20] G.. Valiente, Simple and Efficient Tree Pattern Matching, Research Report LSI-00-72-R, Technical University of Catalonia, Department of Software, Barcelona, December. 2000