Industrial strength formal verification techniques for hardware designs
Industrial strength formal verification techniques for hardware designs
复制标题
用于硬件设计的工业强度形式验证技术
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
M. Srivas
中科院分区：
文献类型：
--
作者：
S. Rajan;Natarajan Shankar;M. Srivas
在过去的十年中，在用于硬件设计和验证的形式方法方面取得了巨大进展。虽然许多基于BDD的技术，符号模拟，特殊用途的决策程序，模型检查和定理已通过不同程度的成功应用，但没有一种技术本身就足够有效地验证复杂寄存器的有效性 - 转移级别的设计，例如最先进的微处理器。为了将正式验证扩展到工业规模的设计，有必要将这些免费技术结合在可以支持适当的抽象机制的一般逻辑环境中。原型验证系统（PVS）是支持探索这种验证方法的环境。 PVS旨在利用语言与扣除，自动化和互动之间的协同作用以及定理证明和模型检查。本文概述了PVS，并描述了PVS的一些主要应用。
The past decade has seen tremendous progress in the application of formal methods for hardware design and verification. While a number of different techniques based on BDDs, symbolic simulation, special-purpose decision procedures, model checking, and theorem proving have been applied with varying degrees of success, no one technique by itself has proven to be effective enough to verify a complex register-transfer level design, such as a state-of-the-art microprocessor. To scale up formal verification to industrial-scale designs it is necessary to combine these complimentary techniques within a general logical environment that can support appropriate abstraction mechanisms. The Prototype Verification System (PVS) is an environment to support the exploration of such a combined approach to verification. PVS is designed to exploit the synergies between language and deduction, automation and interaction, and theorem proving and model checking. This paper gives an overview of PVS and describes some of the major applications of PVS.