file.pdf (215.14 kB)
Download fileAbstract BDDs: A Technique for Using Abstraction in Model Checking
journal contribution
posted on 2003-01-01, 00:00 authored by Edmund M Clarke, Somesh Jha, Yuan Lu, Dong WangWe 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 oft he PCI local bus protocol.
Our verification oft he PCI bus revealed a subtle inconsistency in the
PCI standard. We believe this is an interesting result by itself.