针对GSTE的电路模型抽取

【作者】 祝睿；

【导师】 杨国武；

【作者基本信息】 电子科技大学 ， 计算机应用技术， 2010， 硕士

【摘要】 集成电路产业已经成为国民经济的朝阳产业,每年在全球产生数千亿美元的生产价值。从世界上第一个块集成电路芯片诞生至今,集成电路芯片的面积越来越小,单位面积集成的电路元器件数越来越多,如今一块芯片上已集成了数亿个门。随成电路集成度的增高,人们发现制约集成电路发展的一个重要因素是芯片设计与芯片制造的严重脱节。阻碍芯片设计发展的一个重要因素便是如何验证芯片设计的正确性。传统的模拟验证已经难以满足芯片设计的要求。而形式化验证方法因其是基于严格的数学方法来确保芯片设计的正确性,因此已经在芯片设计领域受到越来越多的重视。实现形式化验证的理论并形成相关验证工具软件的一个关键点就是电路模型的抽取和仿真。本论文首先研究和学习了形式化验证的相关理论知识,包括该理论的主要分支,发展情况。并对目前形式化验证领域的主流算法GSTE进行了深入学习和研究,并对比了该算法与传统算法的不同。其次对当前学术界以及工业界的一些常用工具SMV,VIS,FORTE等进行研究和源码剖析。并对当前电路设计语言VERILOG进行学习研究后,在基于以上工具所提供的电路描述语言的基础上简化VERILOG。设计了一套针对GSTE算法的验证工具的电路描述语言的语法和语义。然后让软件能够方便的对电路进行描述并对电路模型进行抽取。最后设计了系统的框架以及技术路线。然后,研究了电路设计前端语言描述与数字电路形式化验证算法的结合点。分析了电路模型在计算机内存中表示的相关数据结构。研究了如何将一个用语言描述的电路抽取为适合采用GSTE算法来进行验证的电路模型,使得GSTE算法能够应用在实际的电路设计领域。使用编译工具LEX,YACC实现了本软件的电路输入前端,在对语法树进行语义推理后产生了电路模型的二叉判定图数据结构后,交由后端GSTE验证算法进行电路模型的形式化验证。本论文在对数字电路仿真进行了相关研究后,基于抽取的电路模型,实现对该电路模型的仿真,能够得到相应的波形图,从来能方便的对GSTE算法进行演示。最后对全文进行了系统全面的概括总结,并指出了本文所设计工具的不足以及下一步的改进方向,并展望了形式化验证算法在电路设计领域的良好应用前景。更多还原

【Abstract】 IC industry has become a sunrise industry of the national economy annually. It produce several hundred billion dollars in the global value of production. A block from the world’s first integrated circuit chip, since its inception, the area of integrated circuit chips getting smaller and smaller. Integrated circuits has per unit area of increasing number of components, and now a chip has been integrated with hundreds of millions of gates. With the increased integration into the circuit, it was discovered that constrained the development of an important factor in IC chip design and chip manufacturing is a serious disconnect. Hinder the development of chip design is an important factor in how to verify the correctness of chip design. Traditional analog chip design verification has been difficult to meet the requirements of the formal verification method is based on its rigorous mathematical methods to ensure the correctness of chip design, so the field of chip design has been more and more attention. To achieve the formation of formal verification of the theory and tools related to validation is a key point is the circuit model extraction and simulation.In this paper, first of all research and study of the formal verification of the relevant theoretical knowledge, including the theory of the main branch of development. And is currently the mainstream of the field of formal verification algorithms GSTE conducted in-depth study and research, and compared the algorithm with the traditional algorithms different.Second, pairs of digital circuits and digital circuit design method related to a summary study of digital circuit design front-end circuit description and digital circuits formal verification algorithm point. Analysis of how the circuit model expressed in the computer memory, data structure, and studied how to use language to describe a circuit extraction algorithm suitable for use GSTE to verify the circuit model, allowing GSTE algorithm can be applied to practical circuit design zoneThirdly, in the current academic and industrial circles some common tools SMV, VIS, FORTE and other research and source analysis, and the current circuit design language VERILOG learning studies, in view of the above tools offered by the circuit description language summarized on the basis of grammatical simplification VERILOG produced a set of algorithms for verification tools GSTE circuit description language syntax and semantics, so that it could easily describe the circuit and the circuit model extraction. Using the compilation tools LEX, YACC implements the circuit of this software enter the front end, in the syntax tree generated from semantic reasoning, the circuit model of the data structure binary decision diagram by the back-end authentication algorithm GSTE Formal Verification of the circuit model. In order to visual observations of the circuit description language describes the circuit behavior, this paper in the digital circuit simulation carried out relevant studies, based on the extraction of the circuit model, realization of the circuit model of the simulation, the corresponding waveforms can be, never be able to convenient presentation of the GSTE algorithm.Finally, the paper conducted a systematic and comprehensive summary of conclusion and pointed out the lack of design tools in this article, as well as the next step to improve the direction and looks forward to the formal verification algorithm in the field of circuit design a good application prospects.更多还原