臺灣博碩士論文加值系統

基於數位電路中有限的輸出與輸入，大量的資料需要經過分割為較小的資料區塊，在多個不同的時脈訊號中加以處理，這產生了許多不同的狀態藉以處理相關的工作；更由於現今電路設計趨於複雜，為了分批處理資料造成的大量狀態，使得除錯與功能驗證造成困難。因此，使用統一塑模語言（UML）建立視覺化的模型，呈現較為直觀與簡易的概念以描述電路行為。統一塑模語言在商業市場及工業中已被廣泛的應用在系統化的實現或是軟體的設計當中。
在硬體描述語言（HDL）中可以使用多種不同的編寫方式作為電路的實現，而且通常使用結構化的行為描述方法加以實現時序電路。而以此方法製作時序電路時，經常遇到切割所要的工作進入不同的狀態中，將資料加以運算或輸出結及輸入。為了抽象化表示硬體描述語言對時序電路所做的描述，使用了統一塑模語言，並以其所提供的圖像與概念加以呈現電路設計所要達成的動作。
語意狀態機(SFSM)則是為了適當的表示硬體描述語言在實現數位時序電路中的狀態行為，用以取代過去以二進位表示的狀態轉換，以符合統一塑模語言抽象化的高階描述。最後，使用 SPIN加以驗證由統一塑模語言所建立的模型，得到驗證結果與圖形化的輸出。

Unified Modeling Language (UML) provides a simple and easy tool for the specification and requirement of systems. It is rapidly becoming an industrial standard for object-oriented modeling and analysis. According to its flexibility, this thesis adopts UML to build the model of finite state machine (FSM) structure in HDL. In addition, the model checker is SPIN that results from codes in description of PROMELA.
Semantic Finite State Machine (SFSM) presents complete definitions to explain circuits structured by hardware description language (HDL) in the abstract level. HDL depicts digital circuit in several methods, but structural behavior description is especially for sequential circuit. SFSM provides definitions for behavior description in HDL, and UML is used to build a model in abstract level and visualize the model to easily understand.
In addition to verification with binary deriving such as Karnaugh graph, binary decision diagram, this thesis proposes an abstract concept to portray the design that is based on states. Finally, the experimental result is produced after model checking with SPIN and model building with UML.

CHAPTER1 INTRODUCTION 1
1.1 MOTIVATION 1
1.2 DESIGN VERIFICATION 3
1.3 SPIN 4
CHAPTER2 MODELING PROCESS 7
2.1 DOMAIN MODEL 7
2.2 MODEL CHECKING 10
2.3 SEMANTIC FINITE STATE MACHINE 14
CHAPTER3 MODELS USING SPIN 16
3.1 IMPLICIT SPECIFICATION STYLE 16
3.2 EXPLICIT SPECIFICATION STYLE 23
CHAPTER4 IMPLEMENTATION WITH A CASE 34
4.1 A CASE WITH SUBSTATES 34
4.3 THE INTERCEPTIVE CONTROLLER IN SPIN 39
4.3 SUMMARY 43
CHAPTER5 CONCLUSIONS AND FUTURE WORKS 45
REFERENCE 47
APPENDIX A 49

[1] Prasanta Bose, “Automated Translation of UML Models of Architectures for Verification and Simulation Using SPIN”, 14th IEEE International Conference on Automated Software Engineering, October 12 - 15, 1999
[2] C.-N. Liu and J.-Y. Jou, “Efficient Coverage Analysis Metric for HDL Design Validation”, IEE Proceedings - Computers and Digital Techniques, vol. 148, no.1, pp. 1-6, January 2001.
[3] Charles H. and Jr. Roth, Fundamentals of Logic Design, Thomson Learning; 5th edtion, May 1, 2003
[4] David R. Smith and Paul Franzon, Verilog Styles for Synthesis of Digital System, Prentice Hall; 1st edition, January 15, 2001.
[5] Unified Modeling Language Specification, OMG; vesion 1.5, March 2003
[6] Thomas D. E., and Moorby P.R., The Verilog Hardware Description Language, Kluwer, Boston, MA, 1990
[7] IEEE standard Verilog hardware description language, IEEE Std. 1364-2001, New York: IEEE Press, Sep. 2001
[8] Gerard J. Holzmann, “The Model Checker SPIN”, IEEE Trans. on Software Engineering, Vol. 23, No. 5, pp. 279-295, May 1997
[9] Kuangnan Chang and David Kung, “An Efficient Way for specifying State-based System in Promela”, Proc. of 6th International Conf. on Software Engineering and Applications (SEA 2002), Cambridge, USA, Nov. 4 -- 6, 2002.
[10] Mikk E., Lakhnech Y., Siegel, M., and Holzmann G., “Implement Statecharts in PROMELA/SPIN”, In Proc. of the 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques, IEEE Computer Society, 1999
[11] Shige Wang and Shin, K.G., “ Formal Verification for Analysis and Design of Logic Controllers for Reconfigurable Machining Systems”, IEEE Transactions on Robotics and Automation, vol 18, no. 4, pp. 463-474, 2002
[12] Robert B. Jones, John W. O''Leary, Carl-Johan H. Seger, Mark D. Aagaard, and Thomas F. Melham., “Practical formal verification in microprocessor design”, IEEE Design and Test, vol.18, no.4, pp.16-25, July/August 2001.
[13] G.J. Holzmann, “An analysis of bitstate hashing. Formal Methods in Systems Desing”, vol.13, no.3, pp.287-305, 1998.
[14] G.J. Holzmann, D. Peled, and M. Yannakakis, “The nested depth first search algorithm used in Spin”, The Spin Verification System, pp. 23-32, American Mathematical Society, 1996. (Proc. of the 2nd Spin Workshop.)
[15] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, “Symbolic Model Checking: 1020 States and Beyon”, IEEE Information and Computation, vol. 98, no. 2, pp.142-170, June 1992.
[16] J. R. Burch, E. M. Clarke, D. Long, K. L. McMillan, D. L. Dill, “Symbolic Model Checking for Sequential Circuit Verification”, IEEE Transactions on CAD, vol. 13, no. 4, 1994.
[17] Fujita, M., “Model Checking: its basics and reality”, Proceedings of the ASP-DAC ''98. Asia and South Pacific, pp. 217 —222, 1998.
[18] Craig Larman, Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and the Unified Process, Prentice Hall PTR; 2nd edition, July 13, 2001.
[20] James Martin and James J., Odell Object-Oriented Methods: A Foundation, 2nd ed.
Prentice-Hall, 1998
[21] R.E. Bryant, “Graph-based algorithm for Boolean function manipulation”, IEEE Trans. Computers, vol. 35, no. 8, pp.677-691, 1986.
[22] Randal Bryant, “Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification”, IEEE International Conference on Computer-Aided Design, pp. 236-243, 1995.