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

《模拟与混合信号电路的形式化验证》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、第42卷第8期计算机工程2016年8月Vol．42No．8ComputerEngineeringAugust2016·体系结构与软件技术·文章编号:1000-3428(2016)08-0034-05文献标志码:A中图分类号:TP302．7模拟与混合信号电路的形式化验证1，21，222杨世瀚，吴尽昭，丁广泓，秦董洪(1．广西混杂计算与集成电路设计分析重点实验室，南宁530006;2．广西民族大学信息科学与工程学院，南宁530006)摘要:针对模拟与混合信号(AMS)电路形式化建模逼真度低和描述不规范

2、的问题，提出一种基于基尔霍夫电流定律节点分析的形式化建模方法。通过扩展计算树逻辑公式，在保留电路更多物理特性的前提下综合描述和验证AMS电路的离散事件和动态行为，保证性质验证的精确性和可信性。以环形振荡器为例，给出该方法的实现过程，并通过Coho工具对振荡器电路进行验证。实验结果表明该方法正确、有效。关键词:形式化验证;模拟与混合信号电路;混杂系统;基尔霍夫电流定律;计算树逻辑中文引用格式:杨世瀚，吴尽昭，丁广泓，等．模拟与混合信号电路的形式化验证［J］．计算机工程，2016，42(8):34-3

3、8，45．英文引用格式:YangShihan，WuJinzhao，DingGuanghong，etal．FormalVerificationofAnalogandMixedSignalCircuit［J］．ComputerEngineering，2016，42(8):34-38，45．FormalVerificationofAnalogandMixedSignalCircuit1，21，222YANGShihan，WUJinzhao，DINGGuanghong，QINDonghong(1．Guan

4、gxiKeyLaboratoryofHybridComputationandICDesignAnalysis，Nanning530006，China;2．CollegeofInformationScienceandEngineering，GuangxiUniversityforNationalities，Nanning530006，China)【Abstract】Forthelowfidelityandnon-normativedescriptionofformalmodelinginAnalog

5、andMixedSignal(AMS)circuit，aformalmodelingmethodisproposedbasedonnodalanalysisofKirchhoff’sCurrentLaw(KCL)．AnextensiontoComputationTreeLogic(CTL)formulaisdevelopedtodescribethediscreteeventsanddynamicbehaviorofAMScircuitandreservesmanyphysicalcharacte

6、risticsofthecircuit，whichguaranteetheaccuracyandcredibilityoftheproperties’verification．Takingtheringoscillatorasanexample，itillustratesspecificimplementationprocessesoftheproposedmethodandverifiestheoscillatorcircuitbyCoho．Experimentalresultshowsthat

7、theproposedmethodisvaild．【Keywords】formalverification;AnalogandMixedSignal(AMS)circuit;hybridsystem;Kirchhoff’sCurrentLaw(KCL);ComputationTreeLogic(CTL)DOI:10．3969/j．issn．1000-3428．2016．08．007［3］Synopsys公司的AMS测试平台，它是基于抽样的1概述模拟仿真方法，是一种不完全的方法。该方法虽然目前基于形

8、式化技术的验证方法已经在数字系能够通过更精细的抽样来不断提高验证的覆盖率，［1］统设计的诸多领域取得了成功，如控制器、接口协但在理论上的不完全性和模拟信号的状态无限性，议、可测性设计等，但无法验证模拟与混合信号也导致这种方法的可信度下降。［2］(AnalogandMixedSignal，AMS)电路的设计。基于混杂系统的形式化验证理论对于验证AMSAMS电路具有功耗低、微型化、可嵌入性、实时性的电路设计的正确性和有效性是一种新的尝试。AMS优点，AMS电路的模拟部分抗干扰能力差，受