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.