模拟电路验证技术发展现状及挑战

理论计算机科学电子笔记153（2006）3-7www.elsevier.com/locate/entcs模拟电路验证技术的发展现状Oded Maler1，2CNRS-VERIMAG中心方程，2平均值。deVignate38610Gi`eres，France摘要将形式验证方法扩展到模拟电路是一项非常具有挑战性的任务，将占用研究人员一段时间。为了应对这一挑战，我们概述了数字电路验证的一些历史，以及最近将其应用于连续和混合系统的尝试。保留字： 模拟电路验证、硬件验证1引言我们首先定位形式验证在电路设计过程中的作用。基于属性的系统设计意味着系统由它应该满足的一组属性来表征。这些属性指定，在一个正式的语言，哪些痕迹的I/O行为的系统可能会表现出，而与其外部环境进行交互。基本上有两种方法来验证系统的给定属性。它们都基于将属性转换为属性监视器，这是一种检查给定行为（I/O事件序列）是否满足属性的机制。这个监视器可以被看作是一个自动机接受完全满足的行为集，或作为一个程序工作递归的长度上的序列和语法结构的属性。1这项工作得到了欧洲共同体项目IST-2003-507219 PROSYD（基于属性的系统设计）的部分支持2电子邮件：Oded. imag.fr1571-0661 © 2006由Elsevier B. V.出版在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.02.0204O. Maler/Electronic Notes in Theoretical Computer Science 153（2006）3在仿真/测试（也称为电路术语中的如果其中一个跟踪违反了该属性，则系统不正确。然而，由于系统将暴露于潜在的无限（或非常大）数量的输入，因此不可能对所有可能的输入完成此过程。 这个领域的一个大问题是系统地生成测试用例，以某种方式算法验证的目标更加雄心勃勃。探索系统的转换图，以表明它可以生成的所有序列都被属性监视器接受。这里的一个主要问题是状态爆炸，因为系统的状态数是状态变量（在数字电路的情况下，存储器保持元件）的指数。当前验证领域的大部分研究都是关于找到应对这种情况的巧妙方法，以及关于开发基于属性的系统设计的方法论方面。本次研讨会关注的是将这种方法扩展到模拟和混合信号系统。2历史背景为了评估数字和模拟领域各自情况之间的对比，有必要回顾一下（数字）形式验证迄今为止的演变：• 程序验证的早期工作（1965-1977）。• 引入时态逻辑作为描述反应系统属性的形式主义（Pnueli 1977）。• 为TL进行演绎（部分手工）验证（1977年至今）。• 第一个用于全自动验证的模型检查算法（Queille和Sifakis 1981，Clarke和Emerson 1981）。• 第一次计算机辅助核查讲习班（格勒诺布尔，1989年）。• 第一个符号模型检查器，可以处理状态空间太大而无法枚举的系统（McMillan 1992）。• 工业强度验证工具的开发• 英特尔的缺陷和正式验证在半导体工业中的扩散（1995）.• 时态逻辑的“工业”版本的开发，• 在PSL标准（1998-2004）中达到高潮的讨论O. Maler/Electronic Notes in Theoretical Computer Science 153（2006）35正如我们所看到的，将理论思想转化为工业工具花了将近30年的时间，在此过程中，除了令人印象深刻的算法发展之外，理论家和实践者之间的文化鸿沟也必须弥合。验证是建立在逻辑，自动机和语义，这是理论计算机科学的一部分在一定程度上，这些主题的一些知识是数字设计师通过布尔逻辑和顺序有限状态机的背景的一部分在另一个方向上，大多数理论计算机科学家对数字电路有基本的了解，至少在门级和门级的抽象层次像CAV这样的会议：计算机辅助验证，以及研究人员和行业之间的合作为创建共同的验证文化做出了很大贡献。模拟领域的情况完全不同。数字电路中晶体管的电学行为只是实现逻辑门的一种手段。这意味着电路的功能正确性可以使用与时序机相对应的抽象模型来验证，而无需过多担心物理实现。这样的物理细节可能会影响电路的“非功能”属性，例如时序或功耗，但是逻辑抽象相对于这样的变化是鲁棒的。相比之下，模拟电路的功能直接根据连续的电量来定义。因此，它们对来自整体操作环境的不可避免的（有时是随机的）扰动更加敏感，例如来自电源的电压、温度、来自附近电子设备的噪声或来自基本源（例如基本晶体管内部的物理特性）的噪声。这种情况的一个令人不快的后果是，电路动态的重要参数只有在物理布局甚至制造之后才能确定。模拟电路的行为是模拟和分析使用模型的连续动态系统，具体由微分方程和代数方程。对这些活动的系统数学支持通常只存在于线性系统中。设计师的文化可能包括电气工程的许多非数字部分，包括信号处理及其数学基础（傅立叶分析，信息论），线性代数和线性系统理论，数值计算，当然还有对实际晶体管行为和电路使用的特定应用领域的物理学的深入了解。这些领域中的大多数都不属于计算机科学家的背景。尝试将误差验证方法导出到允许实值变量和密集时间的模型的历史要短得多，概述如下：• 首次尝试为实时系统定义规范形式和计算模型（1985-1995）。6O. Maler/Electronic Notes in Theoretical Computer Science 153（2006）3• 关于时间自动机的验证的肯定结果（Bennett和Dill 1990）。• 验证混合系统的第一个建议（Maler，Manna和Pnueli 1991）。• 开发用于分析时间和“线性”混合自动机的算法方法• 开发第一个工具，用于近似验证具有非平凡连续动态和少量状态变量的 连 续 和 混 合 系 统 （ Checkmate ， CMU 1999;d/dt ， Verimag 2000;Hysdel，ETH 2000）;控制系统分析是主要的应用领域。• 首次尝试将形式验证应用于模拟电路（2002年至今）。正如我们所看到的，具有连续变量的系统的验证，可以证明，比有限状态系统的验证要困难得多，而且这种系统的验证工具仍处于起步阶段。在尝试将验证方法导出到模拟电路之前，我们应该首先澄清这样做的动机。众所周知，带有模拟或RF功能的芯片很难在第一次尝试时就获得正确的结果，因此我们所做的任何有助于在性能空间的微妙角落发现更多功能缺陷或这种电路的设计者确实使用了数学模型进行分析和数值计算，但这些模型的处理更多地是在工程和应用数学传统中，没有为建模数字并行系统而开发的仔细的语义和方法概念。由于模拟元件的重要性随着系统越来越多地集成在芯片上并更多地嵌入物理世界而增长，因此任何加速其开发的贡献都将产生重大的经济后果。人们相信，正式的方法将在目前使用的模拟系统设计方法中占据一些互补的位置，就像它们已经在数字系统中所做的那样3研讨会概述本期由第一次研讨会上提出的论文组成。这些贡献反映了模拟电路验证的多样性，从形式模型检查到小信号灵敏度分析。它们还说明了基本的挑战：对抗状态爆炸问题，在抽象中以速度换取准确性，以及在适合验证的形式主义中描述实际利益各种O. Maler/Electronic Notes in Theoretical Computer Science 153（2006）37电路被认为：振荡器电路，如隧道二极管振荡器和压控振荡器，顺序混合信号电路，施密特触发器，开关电容积分器和基于自复位多米诺异或门的冲浪流水线。在Frehse等人的论文中，通过线性边界和连续时间动态定义的模型在无限时间范围内以形式合理的方式进行分析。监控自动机用于验证电路特性，如使用传统的可达性技术的抖动。Freibothe等人在论文中提出了一个稍微抽象的观点，其中类似的模型，但具有离散时间动态，在有限的时间范围内进行分析，这也被称为有界模型检查。这种方法允许考虑更复杂的电路架构。在Grabowski等人的方法中，通过建立系统的非保守有限状态抽象，准确性与速度相权衡，然后可以通过有效的模型检查技术进行分析。电路属性，erties描述使用一个特殊的时序逻辑，允许一个包括定时信息。Myers等人在论文中使用混合赋时Petri网作为建模范例，这证明了验证与模拟与说明性的例子。它表明，标准的模拟技术，如随机或极端点模拟，可能无法检测到不必要的行为，可以发现使用正式验证。在Yang和Greenstreet的论文中，将小信号灵敏度分析应用于冲浪电路的非线性模型，以保证其鲁棒性。研究结果可用于改进基于优化的大干扰稳定性分析。