臺灣博碩士論文加值系統

本篇論文提出一個功能驗證(functional verification)方法來協助驗證我們所設計的一顆和ARM7TDMI相容的微處理器，稱之為C-ARM。為了協助功能測試的實現，我們建構了一個稱作CAVE的C-ARM驗證環境。在這個CAVE驗證環境上，我們將驗證的流程分為兩個階段：首先是驗證每個時脈週期所送出的結果、再來是驗證每個指令的執行結果，這兩種驗證方法都能夠非常有效地找出錯誤。然而，沒有功能測試向量(test patterns)，功能驗證也將無法實現，為了產生那些測試向量，我們首先根據ARM7TDMI的指令集架構及C-ARM微架構來建立系統圖(system graph)，則在功能模型之上我們對於每一個功能單元找出其可能的功能錯誤模型(functional fault model)。根據系統圖以及功能錯誤模型，可以針對每一個功能單元來產生測試向量。我們再把這些針對個別功能單元所產生的測試向量組合成一組測試程式，利用此測試程式來驗證C-ARM於設計及實作階段的功能是否符合ARM7TDMI的規格要求。因C-ARM正在整合測試中，這些測試向量之效能則有待進一步的評估。

This thesis proposes a methodology to perform functional verification of a compatible ARM7TDMI microprocessor C-ARM designed by a colleague in our laboratory. To facilitate carrying out the functional test, a C-ARM verification Environment (CAVE) is created. Based on CAVE, the verification process goes through two stages: cycle-by-cycle and instruction-by-instruction verification. We find out that these two verification techniques are quite effective in uncovering bugs. Functional verification can not be performed without functional test patterns. To generate these patterns, the functional fault models for each functional unit are first identified based on its corresponding functional model. Then, system graphs are created based on the ARM7TDMI instruction set architecture and C-ARM micro-architecture. Test patterns are generated for each functional unit based on the system graphs and its functional fault models. The test patterns for each individual functional units are assembled into a testfixture to verify the functionality of C-ARM during design and implementation. Since C-ARM is under integration and testing, the effectiveness of these test patterns is yet to be found out.

List of Figures III
List of Tables IV
Chapter 1 Introduction 1
1.1 Background 1
1.2 Related Work 2
1.3 Scope of the Work 4
1.4 Thesis Organization 6
Chapter 2 Overview of ARM7TDMI Microprocessor 7
2.1 ARM7TDMI Programming Model 8
2.1.1 Operating Modes 8
2.1.2 Processor Operating States 8
2.1.3 State Switching 9
2.1.4 Memory Formats 9
2.1.5 Data Types 10
2.1.6 Registers 11
2.1.7 Program Status Registers 13
2.1.8 Exceptions 14
2.2 Instruction Set 16
2.2.1 ARM Instruction 17
2.2.2 THUMB Instruction 19
2.3 Memory Interface 20
2.3.1 Memory Cycle Types 24
2.3.2 Memory Address Timing 25
2.3.3 Stretching Access Timing 26
2.3.4 Memory Management 27
2.3.5 Instruction Fetch 27
2.3.6 Data Transfer Size 28
Chapter 3 Functional Verification Strategy 29
3.1 Coupling of Design and Verification 29
3.2 Verification Environment 30
3.2.1 V-ARM 32
3.2.2 Memory 33
3.2.3 Virtual Disk Controller 34
3.2.4 Monitor 34
3.2.5 Test Controller 37
3.3 Verification Flow 37
Chapter 4 Test Generation 39
4.1 Functional Blocks and Associated Fault Models 41
4.1.1 Fault Models for Register File 42
4.1.2 Fault Models for WD Block: 44
4.1.3 Fault Models for RD Block: 45
4.1.4 Fault Models for PSR Block: 45
4.1.5 Fault Models for Execution Blocks: 46
4.1.6 Fault Models for INC Block: 47
4.2 Creation of System Graph 47
4.3 Test Program Generation 52
4.3.1 Test Patterns for Stuck-at and Coupling Faults 53
4.3.2 Test Program for Register File 53
4.3.3 Test Program for PSR Block 55
4.3.4 Test Program for RD Block 56
4.3.5 Test Program for WD Block 56
4.3.6 Test Program for Execution Blocks 57
4.3.7 Test Program for INC Block 57
4.4 Test Program Application 58
Chapter 5 Conclusions 60
References 62
Appendix 65

[1] "ARM7TDMI Data Sheet," Document Number: ARM DDI 0029E, Copyright Advanced RISC Machines Ltd. (ARM), August 1995.
[2] Chyi-Bin Lin, "Design and Implementation of a Compatible ARM7TDMI Microprocessor," Master Thesis, Department of Computer Engineering and Science, Yuan-Ze University, July 1999.
[3] E. A. Talkhan, A. M. H. Ahmed, E. Aly and A. E. Salama, "Microprocessors Functional Testing Techniques," IEEE Trans. on Computer-Aided Design, CAD-8 (3), pp. 316-318, 1989.
[4] S. M. Thatte, and J. A. Abraham, "Test Generation for Microprocessors," IEEE Transactions on Computers, C-29 (6), pp. 429-441, 1980.
[5] D. Brahme and J. A. Abraham, "Functional Testing of Microprocessors," IEEE Transactions on Computers, C-33 (6), pp. 475-485, 1984.
[6] L. Shen and S. Y. H. Su, "A Functional Testing Method for Microprocessors," IEEE Trans. on Computers, C-37 (10), pp. 1288-1293, 1988.
[7] A. J. van de Goor and Th.J.W. Verhallen, "Functional Testing of Modern Microprocessors," In 3rd Proc. of IEEE European Conference Design Automation, pp. 350-354, 1992.
[8] A. J. van de Goor and Th.J.W. Verhallen, "Functional Testing of Current Microprocessors (applied to the Intel i860TM)," IEEE International Test Conference, pp. 684-695, 1992.
[9] T. R. Burch and D. L. Dill, "Automatic Verification of Pipelined Microprocessor Control," In 6th Int. Conf. Computer-Aided Verification, Lect. Notes on Comput. Sci. no. 818, pp. 68-80, June 1994.
[10] A. E. Salama, A. K. Ali, and E. A. Talkhan, "Functional Testing of Pipelined Processors," Proc. of IEE Comput. Digit. Tech., vol. I43, no. 5, pp. 318-324, September 1996.
[11] P. Thevenod-Fosse and R. David, "Random Testing of the Control Section of Microprocessor," Proc. of Fault-Tolerant Computing Symp. Milan, Italy, pp. 366-373, June 1983.
[12] J. Miyake, G. Brown, M. Ueda, "Automatic Test Generation for Functional Verification of Microprocessors," Proc. of the Third Asian Test Symposium, pp. 292-297, 1994.
[13] Christoph Kern and Mark R. Greenstreet, "Formal Verification in Hardware Design: A Survey," ACM Computing Surveys, 1997.
[14] D. P. Appenzeller and A. Kuehlmann, "Formal Verification of the PowerPC? Microprocessor," the proceedings of ICCD, pp. 79-84, 1995.
[15] D. L. Beatty and R. E. Bryant, "Formal Verifying a Microprocessor Using a Simulation Methodology," the proceedings of 31st IEEE/ACM Design Automation Conference, pp. 596-602, June 1994.
[16] J. R. Burch, "Techniques for Verifying Superscalar Microprocessors," the proceedings of 33rd IEEE/ACM Design Automation Conference, pp. 552-557, June 1996.
[17] W. A. Hunt, " Microprocessor Design Verification," Journal of Automated Reasoning 5, pp.411-428, April 1989.
[18] Joon-Seo Yim and Chang-Jae Park, "Verification Methodology of Compatible Microprocessors," Proceedings of the ASP-DAC, pp. 173-180, 1997.
[19] M. Abrahams and J. Barkley, "RTL Verification Strategies," Wescon/98, pp. 130-34, 1998.
[20] C. M. Kyung, I. C. Park and S. K. Hong, "HK386: an x86-compatible 32-bit CISC Microprocessor," Proceedings of the ASP-DAC, pp. 661-662, 1997.