Formal verification in hardware design: a survey
Formal verification in hardware design: a survey
复制标题
DOI：
10.1145/307988.307989
复制
发表时间：
1999-04
期刊：
影响因子：
--
通讯作者：
Christoph Kern;M. Greenstreet
中科院分区：
文献类型：
--
作者：
Christoph Kern;M. Greenstreet
近年来，形式化方法作为一种确保硬件设计质量和正确性的替代方法出现，克服了模拟和测试等传统验证技术的一些局限性。形式化方法在设计过程中的应用有两个主要方面：用于指定设计所需属性的形式化框架和用于推理规范和相应实现之间的关系的验证技术和工具。我们考察了文献中提出并应用于实际设计的各种框架和技术。我们描述的规范框架包括时序逻辑、谓词逻辑、抽象和精化，以及ω规则语言之间的包容。所提出的验证技术包括模型检测、自动机理论技术、自动定理证明以及综合上述方法的方法。为了深入了解当前可用技术的范围和局限性，我们提供了一些案例研究，其中正式方法被应用于工业规模的设计，如微处理器、浮点硬件、协议、存储子系统和通信硬件。
In recent years, formal methods have emerged as an alternative approach to ensuring the quality and correctness of hardware designs, overcoming some of the limitations of traditional validation techniques such as simulation and testing. There are two main aspects to the application of formal methods in a design process: the formal framework used to specify desired properties of a design and the verification techniques and tools used to reason about the relationship between a specification and a corresponding implementation. We survey a variety of frameworks and techniques proposed in the literature and applied to actual designs. The specification frameworks we describe include temporal logics, predicate logic, abstraction and refinement, as well as containment between ω-regular languages. The verification techniques presented include model checking, automata-theoretic techniques, automated theorem proving, and approaches that integrate the above methods. In order to provide insight into the scope and limitations of currently available techniques, we present a selection of case studies where formal methods were applied to industrial-scale designs, such as microprocessors, floating-point hardware, protocols, memory subsystems, and communications hardware.