Abstraction Refinement
ATVA(2004)
摘要
Formal property verification exhaustively verifies logic designs against some desired properties of the designs with respect
to all possible input sequences of any length. Without abstraction, state-of-the-art formal proof engines usually cannot verify
properties of designs with more than a couple of hundred registers. As a result, formal property verification relies on automatic
abstraction techniques to verify real-world logic designs.
Abstraction refinement, first introduced by Kurshan in the tool COSPAN, is one of the most practical automatic abstraction
methods. Abstraction refinement incrementally refines an abstract model of the design by including more and more detail from
the original design until the underlying formal property verification engine verifies or falsifies the property.
In this talk we give an overview to some of the most interesting abstraction refinement techniques that have enabled the formal
verification of VLSI logic designs with millions of logic gates.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络