Abstract BDDs: A Technique for Using Abstraction in Model Checking
journal contributionposted on 01.01.2003, 00:00 by Edmund M Clarke, Somesh Jha, Yuan Lu, Dong Wang
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 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.