驗證一個接上匯流排硬體模組的協定有沒有正確對於一個系統晶片(SoC)的發展是很重要的。在傳統以模擬為主的檢測器可以檢測匯流排上的訊號是否有遵守協定，但是這個檢測器是沒有辦法合成而且也沒有辦法及時的找出在實際硬體上發生的錯誤，所以我們提出了以規則為主以及可合成的AHB協定檢測器(HPChecker)，在這個檢測器中共包含了七十三條規則，而且用這些規則去檢查在系統匯流排上的訊號是否有遵守協定。而且為了可以讓設計者快速的找出錯誤的所在，HPChecker還有兩個機制可以加快找出錯誤的速度：一個是錯誤參考表，這個表記錄了所有被測試模組的錯誤情況、另外一個就是歷史資料記憶體，有了這兩個機制可以讓設計者可以更快的找出錯誤的所在。而HPChecker的大小共是43,432個邏輯閘，而速度再0.18Mm 的製程當中可以執行
203MHz。最後HPChecker 已經被整合進去了一個三維圖形加速器而且也成功的找出了在FPGA 環境下驗證時所發生的協定錯誤。HPChecker 也成功的技術轉移給法國與台灣的工業界，因而幫助系統晶片的發展。

Verifying that a hardware module connected to a bus follows the bus protocol correctly is a necessity in a bus-based System-on-Chip (SoC) development. Traditional simulation-based bus protocol monitors can check whether bus signals obey bus protocol or not, but they are non-synthesizable and thus could not identify bugs occurring at run time in real physical environment. We propose a rule-based and synthesizable protocol checker (HPChecker) for AMBA AHB Bus. It contains 73 related bus protocol rules to check bus signal behavior, and two corresponding debugging mechanisms to shorten debugging time. Error reference table can summarize the violation condition of a design under test (DUT); History Memory contains the content of violation signals. These two mechanisms can help designer debugging efficiently. The gate counts of the HPChecker are 43,432 gates and the speed of it is 203 MHz at 0.18Mm technology. Finally, the HPChecker has been integrated into a 3D graphics accelerator and successfully identifies protocol violation in the FPGA prototype. . HPChecker has been successfully licensed to industries in France and Taiwan to assist SoC development.

CHAPTER 1. INTRODUCTION 1-1
1.1 BACKGROUND 1-1
1.2 MOTIVATION 1-3
1.3 RESEARCH METHOD 1-4
1.4 CONTRIBUTION 1-5
CHAPTER 2. RELATED WORK 2-6
2.1 FORMAL MODELING AND SYMBOLIC VERIFICATION 2-6
2.2 MONITOR-BASED CHECKER 2-8
2.3 RULES COMPARISON 2-10
CHAPTER 3. AMBA AHB INTRODUCTION 3-12
3.1 AHB MASTER MODULE 3-14
3.1.1 AHB master interface 3-14
3.1.2 AHB master output signal list 3-15
3.1.3 Transfer type 3-16
3.1.4 AHB master related rules 3-17
3.2 AHB SLAVE MODULE 3-20
3.2.1 AHB slave interface 3-20
3.2.2 AHB slave output signal list 3-21
3.2.3 AHB slave response type 3-21
3.2.4 Slave’s two-cycle response 3-21
3.2.4.1. Slave RETRY response 3-22
3.2.4.2. Slave SPLIT response 3-23
3.2.5 AHB slave related rules 3-24
3.3 AHB ARBITER 3-26
3.3.1 Arbiter interface 3-26
3.3.2 Arbitration process 3-27
3.3.3 Split transfers 3-29
3.3.4 Dummy master 3-29
3.3.5 Default master 3-29
3.3.6 AHB arbiter related rules 3-30
3.4 AHB DECODER 3-31
3.4.1 AHB decoder interface 3-31
3.4.2 AHB decoder related rules 3-31
3.5 INTRODUCTION OF THE BASIC AMBA AHB TRANSFER 3-32
3.5.1 Basic master transfer 3-32
3.5.2 Basic slave transfer response 3-34
CHAPTER 4. AMBA AHB PROTOCOL CHECKER 4-35
4.1 HPCHECKER ARCHITECTURE 4-35
4.2 PROTOCOL CHECKING MODULE 4-37
4.2.1 Protocol Checking Module 4-38
4.2.2 Basic Idea of Checking Method 4-43
4.3 HISTORY MEMORY 4-45
4.4 REFERENCE TABLE 4-46
4.5 RULE EXTENSION 4-48
CHAPTER 5. VERIFICATION STRATEGY FOR HPCHECKER 5-52
5.1 VERIFICATION ENVIRONMENT INTRODUCTION 5-53
5.1.1 EASY AHB major modules 5-53
5.1.2 AMBA EASY components 5-53
5.2 USING AN AHB BUS EVENT GENERATOR TO VERIFY HPCHECKER 5-55
5.2.1 RTL Triggers to Generate Bus signals 5-55
5.2.2 Pre-compiled Cycle-level Simulation Patterns 5-61
5.2.2.1. Pre-compiled Cycle-level Simulation flow introduction 5-62
5.3 USING A SYNOPSYS’ VIP (VERIFICATION INTELLECTUAL PROPERTY) TO VERIFY HPCHECKER 5-63
5.3.1 VIP Simulation Result 5-64
CHAPTER 6. CASE STUDY 6-66
6.1 CASE STUDY 1: 3D GRAPHICS SOC ENVIRONMENT 6-67
6.1.1 3D graphics SoC case study result1 6-68
6.1.2 3D graphics SoC case study result2 6-68
6.1.3 3D graphics SoC case study result3 6-69
6.1.4 3D graphics SoC case study result4 6-70
6.2 CASE STUDY 2: LEON2 SOC 6-72
6.2.1 LEON2 Environment Overview 6-72
6.2.2 Generic test bench 6-74
6.2.3 Environment Result 6-74
6.3 SYNTHESIS RESULT 6-75
CHAPTER 7. CONCLUSION AND FUTURE WORK 7-76
7.1 CONCLUSION 7-76
7.2 FUTURE WORK 7-76
APPENDIX A HPCHECKER RULE DETAIL INTRODUCTION 7-80

[1]. WISHBONE Specification, Rev. B.2, Silicore Inc., Oct. 2001.
http://www.opencores.org/projects.cgi/web/wishbone/wbspec_b3.pdf
[2]. AMBA Specification, Rev. 2.0, ARM Inc, 1999.
http://www.arm.com/products/solutions/AMBA_Spec.html
[3]. CoreConnect Bus Architecture, White Paper, IBM Inc., 1999.
http://www-1.ibm.com/chips/techlib/techlib.nsf/productfamilies/CoreConnect_Bus_Architecture
[4]. Overview of the CoreFrame Architecture, Rev. 1.01, Palmchip Inc., Jan. 2002.
http://www.palmchip.com/press_Rel_Details.asp?id=23
[5]. EC™ interface, v1.05, MIPS TECHNOLOGIES, 2002.
http://www.mips.com/content/Documentation/MIPSDocumentation/ProcessorCores/BusSpecification/MD00052-2B-EC-SPC-01.05.pdf
[6]. Atlantic Interface, Altera Corporation,
http://www.altera.com/products/ip/altera/t-alt-atlantic.html
[7]. Avalon Bus Specification, Altera Corporation,
http://www.altera.com.cn/literature/manual/mnl_avalon_bus.pdf
[8]. WISHBONE Specification, Rev. B.2, Silicore Inc., Oct. 2001.
http://www.opencores.org/projects.cgi/web/wishbone/wbspec_b3.pdf
[9]. OCP Specification, OCP International Partnership, Release 1.0,
http://www.ocpip.org/socket/ocpspec/
[10]. K. L. McMillan, “Symbolic Model Checking”, Kluwer Academic Publishers, 1993
[11]. Seger, C.-J.H.; Jones, R.B.; O'Leary, J.W.; Melham, T.; Aagaard, M.D.; Barrett, C.; Syme, D., “Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on”; Volume 24, Issue 9, Sept. 2005,
[12]. E. M. Clarke, E. A. Emerson, A. P. Sistla. “Automatic verification of finite-state concurrent systems using temporal logic specifications”, ACM Transactions on Programming Languages and Systems (TOPLAS). 244-263, 1986
[13]. S. Campos, E. Clarke, W. Marrero, M. Minea. “Verifying the performance of PCI Local Bus using Symbolic Techniques”, IEEE International Conference in Computer Design. Oct. 1995.
[14]. F. Aloul and K. Sakallah. “Efficient verification of the PCI local bus using boolean satisfiability.” In International Workshop on Logic Synthesis (IWLS), 2000.
[15]. A. Mokkedem, R. Hosabettu, M. Jones, and G. Gopalakrishnan. “Formalization and analysis of a solution to the PCI 2.1 bus transaction ordering problem.” Formal Methods in System Design, 16, 2000.
[16]. L. Ivanov, R. Nunna. “Specification and formal verification of interconnect bus protocols”, . 43rd IEEE Midwest Symposium on Circuits and Systems, Aug. 2000.
[17]. Roychoudhury, A.; Mitra, T.; Karri, S.R.;” Using formal techniques to debug the AMBA system-on-chip bus protocol”, Design, Automation and Test in Europe Conference and Exhibition, 2003
[18]. K. Shimizu, D. L. Dill, C.-T. Chou. “A specification methodology by a collection of compact properties as applied to the Intel Itanium Processor Bus protocol.” Correct Hardware Design and Verification Methods: 11th IFIP WG 10.5 Adv Research Working Conf, pp. 340–354. LNCS 2144. Springer, 2001.
[19]. Borriello, G., Lavagno, L., and Ortega, R.B.: “Interface synthesis: a vertical slice from digital logic to software components”. Proceeding of International Conference on Computer-Aided Design, November 1998
[20]. Rajawat, A., Balakrishnan, M., and Kumar, A.: “Interface synthesis: Issues and approaches”. Proceeding of 13th International Conference on VLSI Design, January 2000
[21]. V. D'silva, S. Ramesh, A. Sowmya, “Synchronous protocol automata: a framework for modelling and verification of SoC communication architectures”. Design, Automation and Test in Europe Conference and Exhibition, 2004.
[22]. Kanna Shimizu, David L. Dill and Alan J. Hu.” A monitor-based formal specification of PCI”. Proceeding of the 3rd International Conference of Formal Methods in Computer-Aided Design, Nov. 2000.
[23]. Marcio T. Oliveira, Alan J. Hu. “High level specification and design: High-Level specification and automatic generation of IP interface monitors”. Proceedings of the 39th conference on Design automation, June 2002
[24]. M. S. Jahanpour, E. Cerny. “Compositional verification of an ATM switch module using interface recognizer/suppliers (IRS)”. International High-Level Design, Validation, and Test Workshop, pp. 71–76. 2000.
[25]. M. Kaufmann, A. Martin, C. Pixley. “Design constraints in symbolic model checking.“10th International Conference on Computer-Aided Verification, pp. 477–487. LNCS 1427. Springer, 1998.
[26]. Kanna Shimizu and David L. Dill. "Deriving a Simulation Input Generator and a Coverage Metric From a Formal Specification". Proceedings of the Design Automation Conference, June, 2002.
[27]. Prakash Rashinkar, Peter Paterson, and Leena Signh, System-on-a-chip Verification:
Methodology and Techniques, Kluwer Academic Publishers, 2001.