全定制存储电路的FPGA验证方法研究
|
摘要
X微处理器是一款采用全定制方法设计的处理器,内部结构复杂,规模宏大,含有大量的存储电路,因此对其进行验证具有很大的难度。
本文研究了X高性能微处理器体系结构与设计特点,并深入研究X微处理器中存储电路的特性与功能,对验证模型建立过程中存储电路映射模型的建立提出了具体的逻辑映射方法。同时,考虑到验证模型的建立是以映射后面积为首要考虑因素,因此通过深入研究FPGA的资源利用、综合工具的综合特性以及Verilog语言的描述风格,对存储电路的逻辑映射方法进行了基于优化面积的改善。
本文通过深入研究了模拟验证与形式化验证的理、论以及优缺点,对存储电路映射模型的功能一致性提出了模拟验证与等价性验证相结合的验证方法。这种验证方法相比于单独使用模拟验证或等价性验证,极大的提高了验证效率、缩短了验证时间、保证了功能一致性。
本文提出的逻辑映射方法与验证方法在对X微处理器存储电路进行映射模型建立的工作中起到了关键的作用,并对于其它模块的逻辑映射与验证也具有一定的参考意义。本文还通过在具体工程中对辅助工具的使用,提出了一些能够有效提升验证模型建立的速度以及提高验证效率的方法,使得工作效率比传统的工作效率提高了5倍。
X microprocessor is a complex one which uses full-custom design method,and its scale is very large,including many memory circuits.In order to validate the design,we must apply function verification.
This paper is mainly about the logic mapping of memory circuits in the X microprocessor,and verifying the mapping module.Based on the study of the architecture and the design method of X microprocessor,also based on the lucubrating of characteristic and function of the memory circuits,this paper raises a logic mapping method for the memory circuits.And considering the mapped area of the verification model,this paper improves the logic mapping method for optimizing the area through the study of the source of FPGA,the character of synthetic tools and the coding style of Verilog.
Based on the study of the theory of the function verification,this paper raises a verification method for the memory circuits.This method is combined the advantage of formal verification and verification through simulation,and it improves the efficiency and makes the verification easier than either of them.
Under the instructing of these methods,it's much easier to build mapping model of memory circuits,and can make sure the design model and mapping model is consistent. And through using the assistant tools in the work,this paper also raise some other mehods to improve the efficiency of verification.
本文研究了X高性能微处理器体系结构与设计特点,并深入研究X微处理器中存储电路的特性与功能,对验证模型建立过程中存储电路映射模型的建立提出了具体的逻辑映射方法。同时,考虑到验证模型的建立是以映射后面积为首要考虑因素,因此通过深入研究FPGA的资源利用、综合工具的综合特性以及Verilog语言的描述风格,对存储电路的逻辑映射方法进行了基于优化面积的改善。
本文通过深入研究了模拟验证与形式化验证的理、论以及优缺点,对存储电路映射模型的功能一致性提出了模拟验证与等价性验证相结合的验证方法。这种验证方法相比于单独使用模拟验证或等价性验证,极大的提高了验证效率、缩短了验证时间、保证了功能一致性。
本文提出的逻辑映射方法与验证方法在对X微处理器存储电路进行映射模型建立的工作中起到了关键的作用,并对于其它模块的逻辑映射与验证也具有一定的参考意义。本文还通过在具体工程中对辅助工具的使用,提出了一些能够有效提升验证模型建立的速度以及提高验证效率的方法,使得工作效率比传统的工作效率提高了5倍。
X microprocessor is a complex one which uses full-custom design method,and its scale is very large,including many memory circuits.In order to validate the design,we must apply function verification.
This paper is mainly about the logic mapping of memory circuits in the X microprocessor,and verifying the mapping module.Based on the study of the architecture and the design method of X microprocessor,also based on the lucubrating of characteristic and function of the memory circuits,this paper raises a logic mapping method for the memory circuits.And considering the mapped area of the verification model,this paper improves the logic mapping method for optimizing the area through the study of the source of FPGA,the character of synthetic tools and the coding style of Verilog.
Based on the study of the theory of the function verification,this paper raises a verification method for the memory circuits.This method is combined the advantage of formal verification and verification through simulation,and it improves the efficiency and makes the verification easier than either of them.
Under the instructing of these methods,it's much easier to build mapping model of memory circuits,and can make sure the design model and mapping model is consistent. And through using the assistant tools in the work,this paper also raise some other mehods to improve the efficiency of verification.
引文
[1]Anantha Chandrakasan,William J Bowhill,Frank Fox,editors.Design of high-performance microprocessor circuits.IEEE Press.ISBN:0-7803-6001-X.469-470
[2]Jan M Rebaey,Anantha Chandrakasan,Borivoje Nikolic.数字集成电路--设计透视(影印版),清华大学出版社.2004
[3]戴态初,阙沛文.基于FPGA的数字逻辑器件开发及优化设计.微电子学.2002
[4]Xilinx Corp."Virtex-ll Complete Data Sheet.",2005.3,from http:lldirect.xilinx.com/bvdocs/publications/ds031.pdf
[5]马群刚,杨银堂,李跃进,高海霞.基于LUT的SRAM-FPGA结构研究.电子器件.2003
[6]Sabin H.Gerez,Algorithms for VLSI Design Automation,University of Twente,Department of Electrical Engineering,The Netherlands.ISBN 0-471-98489-2
[7]李晓维,吕涛,李光辉,邵明.集成电路设计验证.信息技术快报.2004.
[8]IEEE Std 1364-2001,IEEE Standard Verilog Hardware Description Language.New York:The Institute of Electrical and Electronics Engineers,Inc,2001.
[9]Verisity."Axis Systems description.",2004.11,from http://www.cadence.com
[10]徐欣,李宗华,卢启中,周一宇.基于FPGA的内容可寻址存储器研究设计与应用.国防科技大学学报.2001
[11]彭保,吴坚,于春梅,马建国.Verilog HDL语言在FPGA/CPLD开发中的应用.可编程技术专题.2004
[12]Lionel Bening,Harry Foster.Principles of Verifiable RTL Design Second Edition.2002.http://ebooks.kluweronline.com
[13]Janick Bergeron.Writing Testbenches:Functional Verification of HDL Models.Boston:KluwerAcademic Publishers,2000
[14]陈迅,梁斌,陈跃跃,张民选.全定制微处理器的FPGA原型验证方法,第九届计算机工程与工艺全国学术年会,2005,山东济南,中国计算机学会计算机工程与工艺专业委员会
[15]梁斌.X微处理器系统级验证平台的研究与实现,2004,工学硕士学位论文.
[16]DiniGroup."DN3000k10S user's Manual." Version 1.1.2003.11
[17]Paul Wilcox.Professional Verification.Kluwer Academic Publishers.2004
[18]Cadence design system Inc.Encounter Conformal Equivalence Checking User Guide,2004,http://www.cadence.com/datasheets
[19]Mike Benjamin,Daniel Geist,Alan Hartman,et al.A Study in Coverage-Driven Test Generation.Proceedings of the 36th ACM/IEEE conference on Design automation conference,New York,ACM press.1999,:970-975
[20]刘丽霞,陈书明,梁斌.“夜鹰”仿真验证辅助程序的设计,2005,第九届计算机工程与工艺全国学术年会,山东济南,中国计算机学会计算机工程与工艺专业委员会
[21]Cadence design system Inc.Cadence NC-Verilog Simulator Help,2003, http://www.cadence.com/datasheets
[22]陶俊,邢座程,梁斌.FPGA仿真验证中逻辑综合工具的选择,第九届计算机工程与工艺全国学术年会,2005,山东济南,中国计算机学会计算机工程与工艺专业委员会
[23]Dean Drako,Paul Cohen."HDL Verification Coverage.",2003.7,from http://www.eedesign.com/editorial/1998/codecoverage9806.html
[24]Eric Hennenhoefer,Melanie Typaldos.The Evolution of Processor Test Generation Technology,2003,from http://www.obsidiansoft.com
[25]Lavi Lev,Rahul Razdan,Christopher Tice,It's about time-requirements for the functional verification of nanometer-scale ics,Cadence design system Inc wite paper,2005.from http://www.cadence.com
[26]MentorGraphics design system Inc."Scalable Verification.",2005,from http://www.mentor.com/products/fv/
[27]Synopsys."Discovery Verification Platform.",2004,from http://www.synopsys.com/products/solutions/discovery_platform.html
[28]Zhengyu Gu,Zhiyi Yu,Bo Shen,Qianliang Zhang.Functional Verification Methodology Of a 32-bit RISC Microprocessor.Fudan Unversity.IEEE press.2002
[29]David Dempster,Michael Stuart.Verification Methodology Manual Techniques for Verifying HDL Design.Teamwork International.2002
[30]Janick Bergeron.Writing Testbenches;Functional Verification of HDL Models
[31]Samir Palnitkar.Design Verification with e.Prentice PTR.2003-09-25
[32]William K.Lam,Sun Microsystems.Hardware Design Verification:Simulation and Formal Method-Based Approaches.Prentice PTR.2003-05-03
[33]朱英.微处理器功能验证及相关技术浅析.高性能计算技术.总第160期.2003-02
[34]Verisity Design Inc.User Guide for Verilog-Based Designs:Xcite and Xtreme.2005-01-01
[35]Cadence Design Systems Inc.Connectivity to Schematic User Guide.Product Version 5.1.41.2004-06
[36]Cadence Design Systems Inc.Design Data Translator's Reference.Product Version 5.1.41.2004-06:170-187
[37]Richard Ho.在以覆盖率为导向的验证理论中如何有效结合断言和覆盖点.http://www.fpgatech.net.2005-10
[38]尤永康,刘乃琦.自动化回归测试在Java项目中的实现.计算机应用,第25卷第一期.2005-01
[39]马凤翔,孙义和.SoC原型验证技术的研究.2006-02.http://www.ednchina.com
[40]李暾,李思昆,郭阳.功能验证模拟矢量自动生成技术研究综述.计算机工程与科学,2003年第25卷第6期
[41]Gorschwin Fey,Rolf Drechsler.lmproving Simulation-Based Verification by Means of Formal Methods
[2]Jan M Rebaey,Anantha Chandrakasan,Borivoje Nikolic.数字集成电路--设计透视(影印版),清华大学出版社.2004
[3]戴态初,阙沛文.基于FPGA的数字逻辑器件开发及优化设计.微电子学.2002
[4]Xilinx Corp."Virtex-ll Complete Data Sheet.",2005.3,from http:lldirect.xilinx.com/bvdocs/publications/ds031.pdf
[5]马群刚,杨银堂,李跃进,高海霞.基于LUT的SRAM-FPGA结构研究.电子器件.2003
[6]Sabin H.Gerez,Algorithms for VLSI Design Automation,University of Twente,Department of Electrical Engineering,The Netherlands.ISBN 0-471-98489-2
[7]李晓维,吕涛,李光辉,邵明.集成电路设计验证.信息技术快报.2004.
[8]IEEE Std 1364-2001,IEEE Standard Verilog Hardware Description Language.New York:The Institute of Electrical and Electronics Engineers,Inc,2001.
[9]Verisity."Axis Systems description.",2004.11,from http://www.cadence.com
[10]徐欣,李宗华,卢启中,周一宇.基于FPGA的内容可寻址存储器研究设计与应用.国防科技大学学报.2001
[11]彭保,吴坚,于春梅,马建国.Verilog HDL语言在FPGA/CPLD开发中的应用.可编程技术专题.2004
[12]Lionel Bening,Harry Foster.Principles of Verifiable RTL Design Second Edition.2002.http://ebooks.kluweronline.com
[13]Janick Bergeron.Writing Testbenches:Functional Verification of HDL Models.Boston:KluwerAcademic Publishers,2000
[14]陈迅,梁斌,陈跃跃,张民选.全定制微处理器的FPGA原型验证方法,第九届计算机工程与工艺全国学术年会,2005,山东济南,中国计算机学会计算机工程与工艺专业委员会
[15]梁斌.X微处理器系统级验证平台的研究与实现,2004,工学硕士学位论文.
[16]DiniGroup."DN3000k10S user's Manual." Version 1.1.2003.11
[17]Paul Wilcox.Professional Verification.Kluwer Academic Publishers.2004
[18]Cadence design system Inc.Encounter Conformal Equivalence Checking User Guide,2004,http://www.cadence.com/datasheets
[19]Mike Benjamin,Daniel Geist,Alan Hartman,et al.A Study in Coverage-Driven Test Generation.Proceedings of the 36th ACM/IEEE conference on Design automation conference,New York,ACM press.1999,:970-975
[20]刘丽霞,陈书明,梁斌.“夜鹰”仿真验证辅助程序的设计,2005,第九届计算机工程与工艺全国学术年会,山东济南,中国计算机学会计算机工程与工艺专业委员会
[21]Cadence design system Inc.Cadence NC-Verilog Simulator Help,2003, http://www.cadence.com/datasheets
[22]陶俊,邢座程,梁斌.FPGA仿真验证中逻辑综合工具的选择,第九届计算机工程与工艺全国学术年会,2005,山东济南,中国计算机学会计算机工程与工艺专业委员会
[23]Dean Drako,Paul Cohen."HDL Verification Coverage.",2003.7,from http://www.eedesign.com/editorial/1998/codecoverage9806.html
[24]Eric Hennenhoefer,Melanie Typaldos.The Evolution of Processor Test Generation Technology,2003,from http://www.obsidiansoft.com
[25]Lavi Lev,Rahul Razdan,Christopher Tice,It's about time-requirements for the functional verification of nanometer-scale ics,Cadence design system Inc wite paper,2005.from http://www.cadence.com
[26]MentorGraphics design system Inc."Scalable Verification.",2005,from http://www.mentor.com/products/fv/
[27]Synopsys."Discovery Verification Platform.",2004,from http://www.synopsys.com/products/solutions/discovery_platform.html
[28]Zhengyu Gu,Zhiyi Yu,Bo Shen,Qianliang Zhang.Functional Verification Methodology Of a 32-bit RISC Microprocessor.Fudan Unversity.IEEE press.2002
[29]David Dempster,Michael Stuart.Verification Methodology Manual Techniques for Verifying HDL Design.Teamwork International.2002
[30]Janick Bergeron.Writing Testbenches;Functional Verification of HDL Models
[31]Samir Palnitkar.Design Verification with e.Prentice PTR.2003-09-25
[32]William K.Lam,Sun Microsystems.Hardware Design Verification:Simulation and Formal Method-Based Approaches.Prentice PTR.2003-05-03
[33]朱英.微处理器功能验证及相关技术浅析.高性能计算技术.总第160期.2003-02
[34]Verisity Design Inc.User Guide for Verilog-Based Designs:Xcite and Xtreme.2005-01-01
[35]Cadence Design Systems Inc.Connectivity to Schematic User Guide.Product Version 5.1.41.2004-06
[36]Cadence Design Systems Inc.Design Data Translator's Reference.Product Version 5.1.41.2004-06:170-187
[37]Richard Ho.在以覆盖率为导向的验证理论中如何有效结合断言和覆盖点.http://www.fpgatech.net.2005-10
[38]尤永康,刘乃琦.自动化回归测试在Java项目中的实现.计算机应用,第25卷第一期.2005-01
[39]马凤翔,孙义和.SoC原型验证技术的研究.2006-02.http://www.ednchina.com
[40]李暾,李思昆,郭阳.功能验证模拟矢量自动生成技术研究综述.计算机工程与科学,2003年第25卷第6期
[41]Gorschwin Fey,Rolf Drechsler.lmproving Simulation-Based Verification by Means of Formal Methods