Sciweavers

DAC
1994
ACM

New Techniques for Efficient Verification with Implicitly Conjoined BDDs

13 years 7 months ago
New Techniques for Efficient Verification with Implicitly Conjoined BDDs
-- In previous work, Hu and Dill identified a common cause of BDD-size blowup in high-level design verification and proposed the method of implicitly conjoined invariants to address the problem. That work, however, had some limitations: the user had to supply the property being verified as an implicit conjunction of BDDs, the heuristic used to decide which conjunctions to evaluate was rather simple, and the termination test, though fast and effective on a set of examples, was not proven to be always correct. In this work, we address those problems by proposing a new, more sophisticated heuristic to simplify and evaluate lists of implicitly conjoined BDDs and an exact termination test. We demonstrate on examples that these more complex heuristics are reasonably efficient as well as allowing verification of examples that were previously intractable.
Alan J. Hu, Gary York, David L. Dill
Added 27 Aug 2010
Updated 27 Aug 2010
Type Conference
Year 1994
Where DAC
Authors Alan J. Hu, Gary York, David L. Dill
Comments (0)