A Verification Manager for Adaptive Model Checking

由于验证约占开发周期的三分之二，形式方法很有希望提高电子设计师的生产率。为了克服现有形式化验证算法的局限性，本项目探索了自适应模型检测技术。模型检查是一种验证有限状态系统性质的技术。由于状态数随状态变量数呈指数增长，阻碍了模型检测在大型系统中的应用-这是一个称为状态爆炸的问题。该项目通过三种方法的组合来解决状态爆炸问题：验证管理、自动抽象/求精和二叉决策图(BDD)技术。这些方法结合在一起给出了自适应模型检查，其中验证管理组件识别适当的划分和抽象策略，并从设计中提取要被验证的信息，以指导基于BDD的算法进行有效的符号状态探索。

With verification taking about two thirds of the development cycle, formalmethods hold great promise of increasing the productivity of electronicdesigners. To overcome the limitations of current formal verificationalgorithms, this project explores adaptive model checking techniques. Modelchecking is a technique for the verification of properties of finite statesystems. Application of model checking to large systems is hindered by theexponential growth of the number of states with the number of statevariables---a problem known as state explosion. This project addresses thestate explosion problem by a combination of three approaches: verificationmanagement, automatic abstraction/refinement, and binary decision diagram(BDD) technology. These approaches combine to give adaptive model checking,in which the verification management component identifies the appropriatepartitioning and abstraction strategies and extracts from the design to beverified information that guides BDD-based algorithms to efficient symbolicstate exploration.