什么是形式化验证.doc

设计正确性的验证问题是目前学术界和工业界均予以关注的重要研究课题。在学术界，对相关课题的研究集中了世界上最优秀的数学家和计算机科学家，他们广泛分布于世界上最著名的高校、科研机构和公司；在工业界，几乎所有的世界顶尖IT公司都投入大量的人力和物力来开发它们的验证和测试工具。而且，学术界和产业界的密切结合也是该领域的一个突出现象。 设计正确性验证的重要性 我们可从以下两个事件切实感受到设计正确性验证的重要性。 1994年，奔腾处理器被发现在执行某个特定的浮点运算时出现错误，这种错误27000年才可能出现一次。对此，Intel付出4.75亿美元的巨额代价回收有缺陷的奔腾处理器。 1996年6月4日，欧洲航天局研制的阿里亚娜五型火箭在发射后不到40秒爆炸。事后调查发现，错误发生于当一个很大的64位浮点数转换为16位带符号整数时出现异常。细微错误，使得十年的努力毁于一旦。 从以上事件可以看出，无论是在高危险性领域中使用的还是普通家用的数字系统，保证设计正确性都是至关重要的。软件、硬件和协议是目前数字系统设计所包含的三种最基本的形式，任何复杂的数字系统大致都由这三个部分组成。如果说在复杂系统设计过程中错误是难免的，那么出现事故的惟一原因就是：没有在产品使用前对其进行完备的置信(validation)工作，即确认系统已经完全实现了设计者的意图。 验证技术的方法和困难 为什么验证一个系统的正确性会如此困难呢？让我们首先来了解一下主要的验证方法。 迄今的验证方法可分为模拟、仿真和形式验证三种。模拟验证是传统的验证方法，而且目前仍然是主流的验证方法。模拟验证是将激励信号施加于设计，进行计算并观察输出结果，并判断该结果是否与预期一致。模拟验证的主要缺点是非完备性，即只能证明有错而不能证明无错。因此，模拟一般适用于在验证初期发现大量和明显的设计错误，而难以胜任复杂和微妙的错误。模拟验证还严重依赖于测试向量的选取，而合理而充分地选取测试向量，达到高覆盖率是一个十分艰巨的课题。由于设计者不能预测所有错误的可能模式，所以尚未发现某个最好的覆盖率度量。即使选定了某个覆盖率度量，验证时间也是一个瓶径。 仿真验证在原理上与模拟验证类似，只是将模拟验证的三个主要部分即激励生成、监视器和覆盖率度量集成起来，构成测试基准(testbench)，用FPGA实现。仿真比模拟的验证速度快得多，其缺点是代价昂贵，灵活性差。 既然模拟/仿真验证有如此大的局限性，自然就促使人们去研究更完善的验证方法，即形式验证。形式验证就是从数学上完备地证明系统是否实现了设计者的意图。这意味着首先要用某种语言和逻辑构造系统的数学模型，然后运用严格的数学推理来证明设计的正确性。形式验证的主要优点是完备性，能够完全断定设计的正确性。其缺点是首先要对原始设计进行模型抽取，这对使用者有数学技能和经验上的要求。而且，有的工具需要人工引导(如定理证明)，有的工具存在状态空间爆炸问题(如模型检验)。 到此回答为什么验证问题如此之难就比较容易理解了。困难来自于以下两个方面： 系统复杂度的不断增大。一直在遵循Moore定律的IC制造技术使得设计者在单个芯片上集成了更多的IP核、内存、总线等，构成非常复杂的系统。与此鲜明对照，验证技术的发展落后于IC制造能力。这使现有的验证工具越来越不能胜任验证需求。对于模拟验证，发现隐含错误本来就是它的弱项，而系统越复杂，隐含错误就越多。 上市时间的不断缩短。目前电子产品的更新换代之快反映了对设计周期不断缩短的市场竞争要求。验证过程所耗费的时间一般占总设计周期的三分之二，甚至达到80%以上。因此，对验证的合理要求就是：尽量提高速度以溶入设计流程中。尤其在设计早期，在高层次发现设计错误，可以极大地降低设计返工的成本。目前，形式验证方法只能在较小规模的设计上才能达到速度要求。对于大规模设计，则需要多种验证工具的协作。 虽然形式验证目前还不能成为验证的主流工具，但业界的研究人员仍在继续努力，并不断取得进展。 形式验证技术 对形式验证技术的关注起源于20世纪60年代的软件危机。直至整个70年代，形式验证技术所针对的一般是转换型程序，即单纯进行科学计算、计数等功能的软件。所采用的主要是定理证明(theorem proving)技术。80年代初，最大的进展是Pnueli将时态逻辑引入到反应式程序的验证中。1981年，Clarke等提出了模型检验(Model Checking)方法，实现了对于并发系统的自动验证问题。然而，模型检验因状态空间爆炸问题而很难达到实用化。 形式验证的巨大成功首先来自于80年代后期符号模型检验(Symbolic Model Checking)方法的提出和在硬件验证中实现。1987年，McMillan在博士论文中，首次将发表于前一年的BD