模拟与混合信号电路的形式化验证.PDFVIP

第 42 卷 第 8 期 Vol． 42 No． 8 计 算 机 工 程 Computer Engineering 2016 年 8 月 August 2016 ·体系结构与软件技术· 文章编号: 1000-3428( 2016) 08-0034-05 文献标志码: A 中图分类号: TP302． 7 基金项目: 国家自然科学基金资助项目(11461006) ; 广西自然科学基金资助项目 ( 2014GXNSFAA118359，2014G XNSFAA118358) 。 作者简介: 杨世瀚( 1972 － ) ，男，副教授、博士，主研方向为集成电路形式化验证、混杂系统、符号计算; 吴尽昭，教授、博士生导师; 丁广泓，硕士; 秦董洪，副教授、博士。 收稿日期: 2015-06-02 修回日期: 2015-08-25 E-mail: mryangsh@ 163． com 模拟与混合信号电路的形式化验证 杨世瀚1，2，吴尽昭1，2，丁广泓2，秦董洪2 ( 1． 广西混杂计算与集成电路设计分析重点实验室，南宁 530006; 2． 广西民族大学 信息科学与工程学院，南宁 530006) 摘 要: 针对模拟与混合信号( AMS) 电路形式化建模逼真度低和描述不规范的问题，提出一种基于基尔霍夫电流 定律节点分析的形式化建模方法。通过扩展计算树逻辑公式，在保留电路更多物理特性的前提下综合描述和验证 AMS 电路的离散事件和动态行为，保证性质验证的精确性和可信性。以环形振荡器为例，给出该方法的实现过程， 并通过 Coho 工具对振荡器电路进行验证。实验结果表明该方法正确、有效。 关键词: 形式化验证; 模拟与混合信号电路; 混杂系统; 基尔霍夫电流定律; 计算树逻辑 中文引用格式: 杨世瀚，吴尽昭，丁广泓，等． 模拟与混合信号电路的形式化验证［J］． 计算机工程，2016，42( 8) : 34- 38，45． 英文引用格式: Yang Shihan，Wu Jinzhao，Ding Guanghong，et al． Formal Verification of Analog and Mixed Signal Circuit ［J］． Computer Engineering，2016，42( 8) : 34-38，45． Formal Verification of Analog and Mixed Signal Circuit YANG Shihan 1，2，WU Jinzhao1，2，DING Guanghong2，QIN Donghong2 ( 1． Guangxi Key Laboratory of Hybrid Computation and IC Design Analysis，Nanning 530006，China; 2． College of Information Science and Engineering，Guangxi University for Nationalities，Nanning 530006，China) 【Abstract】For the low fidelity and non-normative description of formal modeling in Analog and Mixed Signal( AMS ) circuit，a formal modeling method is proposed based on nodal analysis of Kirchhoff’s Current Law ( KCL ) ． An extension to Computation Tree Logic( CTL ) formula is developed to describe the discrete events and dynamic behavior of AMS circuit and reserves many physical characteristics of the circuit，which guarantee the accuracy and credibility of the properties’verification． Taking the ring oscillator as an example，it illustrates specific implementation processes of the proposed method and verifies the oscillator circuit by Coho． Experimental result shows that the proposed