形式化验证技术eda软件开发中的应用.pdf

摘要 摘要 形式化验证技术起源于20世纪60年代软件危机。直至整个70年代，形式化 验证技术所针对的一般是转换型程序，即单纯进行科学计算、计数等功能的软件。 Model 形式化验证的巨大成功首先来自于80年代后期符号模型检验(Symbolic 首次将发表于前一年的二分决策图(Binar)，DecisionDia酎am)技术应用于模型检验 中，从而大大地缓解了空问爆炸问题。其后的一系列改进更增强了对符号模型检 验技术的信心。然而，人们很快就发现，对于复杂系统，空间爆炸问题仍是符号 模型检验技术难以克服的障碍，这导致了在1999年定界模型检验技术的提出。总 的来说，模型检验方法在硬件验证上是成功的，其根本原因是硬件通常有层次性 且比较规整，相比于软件的复杂程序结构，更易于描述和验证。 本文主要介绍形式化验证技术在集成电路自动化设计中的应用。首先介绍了 形式化验证技术的发展现状和集成电路自动化设计流程，然后介绍了框架时序逻 辑程序设计语言，本文利用这种语言实现了简单时序电路的描述。随后本文介绍 了模型检验工具的设计原理和移植框架，并使用移植后的模型检验工具对采用框 架时序逻辑程序设计语言描述的电路进行模拟验证。 最后本文介绍了可满足性验证和等价性验证。本文详细阐述了集成电路自动 化设计中的逻辑综合过程，设计原则，综合工具，并在此基础上完成了组合电路 逻辑综合前后的等价性验证。 关键词：形式化验证等价性验证 可满足性验证逻辑综合 ABSTRACT AB STRACT FomalVerification inthe20tll so腑are嘶sisin tecllll0109yor蜮nated centu吼me 60 me Verification istmsfonnationalforthe 70’s，fomal years．Until technology iIl a scientific arld omer凡nctionsof programgeneral，thatsimple caLlculation，co戚ing the success the so胁are．The comes舶mlate Model great 80’s，S舯bolicChecbng Model are and inhardware (SymbolicChec玉【ing)methodsproposedimplemented 1 Verification．In PhD 987，McMillaJlthesis，used BDD(Binar)，DecisionDia蓼anl) inmodel forthefirst tlle time，thus tecllllologycheckiIlg greatlyeaSingspaceexplosion