超大规模集成电路设计流程中的验证技术及实践
|
摘要
随着芯片规模的指数上涨，验证能力已经远远落后于设计能力，并且正在成为制造功能更复杂、规模更庞大的芯片的瓶颈。为了解决这一问题，验证领域得到了极大的发展。在文中，通过对验证活动的作用、验证流程的分析，提出芯片的验证已经不仅仅是硬件测试，而且是结合有软件测试特点的硬件测试。在此思想的指导下，对测试平台提出的要求也超出了早期仅局限于效率和功能的局限。扩展性、代码覆盖率和回归测试等也在测试中占有很重要的地位。
更高的验证目标要求有更有效的支持。其中，Synopsys公司的Vera语言是专用于设计测试平台的现代语言之一。主要的特点是：面向对象的语言内核；通过界面定义和端口变量等实现了Vera语言内核和硬件描述语言的接口；通过编程结构fork／join和数据结构(事件、邮箱和旗语)来实现复杂的并行控制，实现对硬件特点的模拟。
本文以视频后处理芯片的测试实践为基础，分析了视频输出模块和算法实现模块的测试过程，强调模块级和系统级测试的不同重点，并总结了这块芯片的验证工作中的成功和不足。
静态验证也对上述动态验证起到很大的补充。其中形式验证是静态验证的一种。本文通过对形式验证中部分顺序理论的分析，阐述了通过串并行部序集描述复杂系统的原理。在简单评价了Synopsys公司的商用软件Formality之后，重点分析了在视频后处理芯片项目中Formality的应用流程和实际工作经验，证明形式验证的重要作用。
这篇论文分成四个部分，第一部分主要是对验证策略的介绍，第二部分是介绍Vera语言的特性，第三部分是视频后处理第二版芯片中的验证工作的分析和总结，第四部分是对形式验证理论的探讨和视频后处理芯片中形式验证工具的使用以及经验的总结。
As the scale of chips increase exponentially, verification trails far from design, and verification is becoming the bottleneck of designing and producing much greater and more complex chips. In order to solve the problem, the field of verification has been developed greatly. This paper points that the activity of chip's verification is no longer hardware testing, but a hardware testing with basic rules of software testing. Directed by this idea, more requires are promoted of testbenches than efficiency and functionality. Expansibility, code coverage and regression test also possesses great importance.
Higher goals demand for more powerful tools. Synopsys's Vera is one of the most modern languages designed specially for making testbenches. Main characteristics include object-oriented language core, interfaces between Vera core and HDL implemented by interface definition and port variables, complex concurrency control implemented by programming construction (fork/join) and data structures (event, mailbox and semaphore, etc). All these help Vera successfully model hardware properties.
In this paper, we take the verification experiences of video post-process chip as example, analyze the testing course of video display module and algorithm module, emphasize different sides of between module level and system level, and summarize the gains and fails of the chip's verification.
Static verification also provides great help to dynamic verification mentioned above. And formal verification is one form of static verification. This paper analyses patial sequential theory of formal verification, states the principle of modeling complex systems. After evaluating Synopsys's Formality, the paper construes the flow and practical experiences in Video Post-process Chip, and comes to the conclusion that static verification really works.
This paper is composed of four parts. The first part discusses about the strategy of verification; the second one analyzes Vera; the third focuses on the anatomy of verification work in Video Post-process Chip Version 2, the last one probes into the formal verification theory, and summarizes the flow according to practical experiences.
更高的验证目标要求有更有效的支持。其中，Synopsys公司的Vera语言是专用于设计测试平台的现代语言之一。主要的特点是：面向对象的语言内核；通过界面定义和端口变量等实现了Vera语言内核和硬件描述语言的接口；通过编程结构fork／join和数据结构(事件、邮箱和旗语)来实现复杂的并行控制，实现对硬件特点的模拟。
本文以视频后处理芯片的测试实践为基础，分析了视频输出模块和算法实现模块的测试过程，强调模块级和系统级测试的不同重点，并总结了这块芯片的验证工作中的成功和不足。
静态验证也对上述动态验证起到很大的补充。其中形式验证是静态验证的一种。本文通过对形式验证中部分顺序理论的分析，阐述了通过串并行部序集描述复杂系统的原理。在简单评价了Synopsys公司的商用软件Formality之后，重点分析了在视频后处理芯片项目中Formality的应用流程和实际工作经验，证明形式验证的重要作用。
这篇论文分成四个部分，第一部分主要是对验证策略的介绍，第二部分是介绍Vera语言的特性，第三部分是视频后处理第二版芯片中的验证工作的分析和总结，第四部分是对形式验证理论的探讨和视频后处理芯片中形式验证工具的使用以及经验的总结。
As the scale of chips increase exponentially, verification trails far from design, and verification is becoming the bottleneck of designing and producing much greater and more complex chips. In order to solve the problem, the field of verification has been developed greatly. This paper points that the activity of chip's verification is no longer hardware testing, but a hardware testing with basic rules of software testing. Directed by this idea, more requires are promoted of testbenches than efficiency and functionality. Expansibility, code coverage and regression test also possesses great importance.
Higher goals demand for more powerful tools. Synopsys's Vera is one of the most modern languages designed specially for making testbenches. Main characteristics include object-oriented language core, interfaces between Vera core and HDL implemented by interface definition and port variables, complex concurrency control implemented by programming construction (fork/join) and data structures (event, mailbox and semaphore, etc). All these help Vera successfully model hardware properties.
In this paper, we take the verification experiences of video post-process chip as example, analyze the testing course of video display module and algorithm module, emphasize different sides of between module level and system level, and summarize the gains and fails of the chip's verification.
Static verification also provides great help to dynamic verification mentioned above. And formal verification is one form of static verification. This paper analyses patial sequential theory of formal verification, states the principle of modeling complex systems. After evaluating Synopsys's Formality, the paper construes the flow and practical experiences in Video Post-process Chip, and comes to the conclusion that static verification really works.
This paper is composed of four parts. The first part discusses about the strategy of verification; the second one analyzes Vera; the third focuses on the anatomy of verification work in Video Post-process Chip Version 2, the last one probes into the formal verification theory, and summarizes the flow according to practical experiences.
引文
[1] IEEE Standard Verilog Language Reference Manual, IEEE Std 1364-1995. IEEE Press, New York, NY, 1995.
[2] A. Hosseino, D. Mavroidis, P. Knas, "Code Generation and Analysis for the Functional Verification of Microprocessors", DAC96
[3] J. Monaco, D. Holloway, R. Raina, "Functional Verification Methodology for the PowerPC 604TM Microprocessor', DAC96
[4] M. Kantrowitz, L. Moack, "I'm Done Simulating; Now What? Verification Coverage Analysis and Correctness Checking of the DEC chip 21164 Alpha Microprocessor", DAC96
[5] Vera User Guide, Version 5.1.0, June, 2002
[6] R. M. Sedmak, "Implementation Techniques for Self-Verification", Proc, IEEE International Test Conf., pp. 267-278, November 1980
[7] Writing Testbenches: Functional Verification of HDL Models, Janick Bergeron, Qualis Design Corporation
[8] Francoise Casaubieith, et al, "Functional Verification Methodology of Chameleon Processor', Proceedings of the 33rd Design Automation Conference, Las Vegas, June 1996
[9] J. Freeman et al, "The 68060 Microprocessor Functional Design and Verification Methodology", Proceedings of the Design SuperCon '95 On-Chip Design Conference, Santa Clara, March 1995
[10] lan Gibson et al, "Practical Industrial Use of HDLs for the Development of Large High Speed ASICs", Proceedings of the Asia Pacific Conference on Hardware Description Languages, Standards and Applications, Brisbane, December 1993
[11] "Automatic generation of simulation monitors from quantitative constraint formula [system-level verificationS', Xi Chen; Hsieh, H.; Balarin, F.; Watanabe, Y.; Design, Automation and Test in Europe Conference and Exhibition, 2003, 2003 Page(s): 1174-1175
[12] Alberto L. Sangiovanni Vincentelli et al, "Verificaiton of Electronic Systems", Proceedings of the 33rd Design Automation Conference, Las Vegas, June 1996
[13] S. Hunt, A. Mehta, D. Patterson and S. Sah, "A Behavioral VHDL Bus Functional Model for the Pentitum TM Processor", Proceedings of the Spring 1993 VHDL International Users Conference, pp 163-173
[14] Michael J. Knieser, Francis G. Wolff, Chris A. Papachristou, "Developing VHDL Testbenches from C/UNIX Functions" SNUG Europe 2001
[15] Venkat Rajaraman, Naryanan Vydianathan, Khosrow Hajikhani "A Scalable Verification Methodology using VERA", SNUG San Jose2002
[16] Mike Bartley, "Why is Functional Verification So Hard To Plan" SNUG SNUG Europe 2002
[17] Tayal. S.; Moezzi, A.; Magnusson, E., "System level verification of ASIC chip-sets"; ASIC Conference and Exhibit, 1993. Proceedings., Sixth Annual IEEE International, 27 Sept.-1 Oct. 1993 Page(s): 283-287
[18] "System-level verification-a comparison of approaches", Turner, R. ; Rapid System Prototyping, 1999. IEEE International Workshop on, 16-18 June 1999 Page(s): 154-159
[19] "Efficient system-level functional verification methodology for multimedia applications", Cupak, M.; Catthoor, F.; De Man, H. J.; Design & Test of Computers, IEEE, Volume: 20 Issue: 2, March-April 2003 Page(s): 56 -64
[20] Val Popescu and Bill McNamara, "Innovative Verification Strategy redues design cycle for high end sparc processor", Proceedings of the 33rd Design Automation Conference, Las Vegas, June 1996
[21] 数据结构C++语言描述，William Ford、William Topp著，刘卫东、沈关林翻译，清华大学出版社，1998年11月第一版
[22] Perl参考大全(第二版)，Martin C．Brown著，顾凯译，人民邮电出版社，2002年2月第一版
[23] C++ Primer, Stanley B. Lippman, Josee Lajoie 著
[24] Synopsys 公司 Fomality 用户手册 Version U-2003.06, June 2003
[25] Formal Verification: A New Partial Order Approach, Lubomir Ivanov , Ramakrishna Nunna, 1999。
[26] Formal Verification of an Industrial System-on-a-chip , Hoom Choi, Myung-Kyoon Yim, Jae-Young Lee, 20000
[27] Verification of a Combinational Loop Based Arbitration Scheme in a System-on-a-chip Integration Arichitecture, Yang Xia, Pranav Ashar, 20000
[2] A. Hosseino, D. Mavroidis, P. Knas, "Code Generation and Analysis for the Functional Verification of Microprocessors", DAC96
[3] J. Monaco, D. Holloway, R. Raina, "Functional Verification Methodology for the PowerPC 604TM Microprocessor', DAC96
[4] M. Kantrowitz, L. Moack, "I'm Done Simulating; Now What? Verification Coverage Analysis and Correctness Checking of the DEC chip 21164 Alpha Microprocessor", DAC96
[5] Vera User Guide, Version 5.1.0, June, 2002
[6] R. M. Sedmak, "Implementation Techniques for Self-Verification", Proc, IEEE International Test Conf., pp. 267-278, November 1980
[7] Writing Testbenches: Functional Verification of HDL Models, Janick Bergeron, Qualis Design Corporation
[8] Francoise Casaubieith, et al, "Functional Verification Methodology of Chameleon Processor', Proceedings of the 33rd Design Automation Conference, Las Vegas, June 1996
[9] J. Freeman et al, "The 68060 Microprocessor Functional Design and Verification Methodology", Proceedings of the Design SuperCon '95 On-Chip Design Conference, Santa Clara, March 1995
[10] lan Gibson et al, "Practical Industrial Use of HDLs for the Development of Large High Speed ASICs", Proceedings of the Asia Pacific Conference on Hardware Description Languages, Standards and Applications, Brisbane, December 1993
[11] "Automatic generation of simulation monitors from quantitative constraint formula [system-level verificationS', Xi Chen; Hsieh, H.; Balarin, F.; Watanabe, Y.; Design, Automation and Test in Europe Conference and Exhibition, 2003, 2003 Page(s): 1174-1175
[12] Alberto L. Sangiovanni Vincentelli et al, "Verificaiton of Electronic Systems", Proceedings of the 33rd Design Automation Conference, Las Vegas, June 1996
[13] S. Hunt, A. Mehta, D. Patterson and S. Sah, "A Behavioral VHDL Bus Functional Model for the Pentitum TM Processor", Proceedings of the Spring 1993 VHDL International Users Conference, pp 163-173
[14] Michael J. Knieser, Francis G. Wolff, Chris A. Papachristou, "Developing VHDL Testbenches from C/UNIX Functions" SNUG Europe 2001
[15] Venkat Rajaraman, Naryanan Vydianathan, Khosrow Hajikhani "A Scalable Verification Methodology using VERA", SNUG San Jose2002
[16] Mike Bartley, "Why is Functional Verification So Hard To Plan" SNUG SNUG Europe 2002
[17] Tayal. S.; Moezzi, A.; Magnusson, E., "System level verification of ASIC chip-sets"; ASIC Conference and Exhibit, 1993. Proceedings., Sixth Annual IEEE International, 27 Sept.-1 Oct. 1993 Page(s): 283-287
[18] "System-level verification-a comparison of approaches", Turner, R. ; Rapid System Prototyping, 1999. IEEE International Workshop on, 16-18 June 1999 Page(s): 154-159
[19] "Efficient system-level functional verification methodology for multimedia applications", Cupak, M.; Catthoor, F.; De Man, H. J.; Design & Test of Computers, IEEE, Volume: 20 Issue: 2, March-April 2003 Page(s): 56 -64
[20] Val Popescu and Bill McNamara, "Innovative Verification Strategy redues design cycle for high end sparc processor", Proceedings of the 33rd Design Automation Conference, Las Vegas, June 1996
[21] 数据结构C++语言描述，William Ford、William Topp著，刘卫东、沈关林翻译，清华大学出版社，1998年11月第一版
[22] Perl参考大全(第二版)，Martin C．Brown著，顾凯译，人民邮电出版社，2002年2月第一版
[23] C++ Primer, Stanley B. Lippman, Josee Lajoie 著
[24] Synopsys 公司 Fomality 用户手册 Version U-2003.06, June 2003
[25] Formal Verification: A New Partial Order Approach, Lubomir Ivanov , Ramakrishna Nunna, 1999。
[26] Formal Verification of an Industrial System-on-a-chip , Hoom Choi, Myung-Kyoon Yim, Jae-Young Lee, 20000
[27] Verification of a Combinational Loop Based Arbitration Scheme in a System-on-a-chip Integration Arichitecture, Yang Xia, Pranav Ashar, 20000