1999 | OriginalPaper | Buchkapitel
Abstract BDDs: A Technique for Using Abstraction in Model Checking
verfasst von : Edmund Clarke, Somesh Jha, Yuan Lu, Dong Wang
Erschienen in: Correct Hardware Design and Verification Methods
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We propose a new methodology for exploiting abstraction in the context of model-checking. Our new technique uses abstract BDDs as its underlying data structure. We show that this technique builds a more refined model than traditional compiler-based methods proposed by Clarke, Grumberg and Long. We also provide experimental results to demonstrate the usefulness of our method. We have verified a pipelined carry-save multiplier and a simple version of the PCI local bus protocol. Our verification of the PCI bus revealed a subtle inconsistency in the PCI standard. We believe this is an interesting result by itself.