Applications of Hierarchical Verification in Model Checking.

Robert Beers,Rajnish Ghughal,Mark D. Aagaard

CHARME '01: Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods（2000）

引用 3|浏览8

暂无评分

摘要

The LTL model checker that we use provides sound decomposition mechanisms within a purely model checking environment.We have exploited these mechanisms to successfully verify a wide spectrum of large and complex circuits. This paper describes a variety of the decomposition techniques that we have used as part of a large industrial formal verification effort on the Intel Pentium® 4 (Willamette) processor.

查看译文

关键词

LTL model checker,decomposition technique,large industrial formal verification,model checking environment,sound decomposition mechanism,Intel Pentium,complex circuit,wide spectrum,Hierarchical Verification,Model Checking

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要