Abstract
Over the last decade BDD-based symbolic manipulations have been among the most widely used core technologies in the verification domain. To improve their efficiency within the framework of Unbounded Model Checking, we follow some of the most successful trends proposed in this field.
We present a very promising approach based on: Mixing forward and backward traversals, dovetailing approximate and exact methods, adopting guided and partitioned searches, efficiently using conjunctive decompositions and generalized cofactor based BDD simplifications. One of the main contributions of this paper is a backward verification procedure based on a prioritized traversal. We call the method “inbound-path-search”. Initially, an approximate forward traversal produces over-approximate onion-ring frontier sets. After that, these rings are used as distance estimators and guides to partition state sets in terms of the estimated distance from the “target” set of states. Finally, while the subsequent search is performed, the higher priority is given to the subset with the smallest estimated distance.
We experimentally compare our methodology with a state-of-the-art technique (approximate- reachability don’t cares model checking) implemented in the freely available VIS tool. Results show interesting improvements in terms of both efficiency and power.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic Model Checking using SAT procedures instead of BDDs. In Proc. 36th Design Automat. Conf., pages 317–320, New Orleans, Louisiana, June 1999.
F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Y. Vardi. Benefits of Bounded Model Checking at an Industrial Setting. In Gérard Berry, Hubert Comon, and Alan Finkel, editors, Proc. Computer Aided Verification, volume 2102 of LNCS, pages 435–453, Paris, France, July 2001. Springer-Verlag.
P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. In E. Allen Emerson and A. Prasad Sistla, editors, Proc. Computer Aided Verification, volume2102 of LNCS, pages 124–138, Chicago, Illinois, July 2000. Springer-Verlag.
A. Gupta, Z. Yang, P. Ashar, and A. Gupta. SAT-Based Image Computation with Application in Reachability Analysis. In Proc. Formal Methods in Computer-Aided Design, volume 1954 of LNCS, Austin, TX, USA, 2000.
H. Cho, G. D. Hatchel, E. Macii, B. Plessier, and F. Somenzi. Algorithms for Approximate FSM Traversal Based on State Space Decomposition. IEEE Transactions on CAD, 15(12):1465–1478, December 1996.
K. Ravi and F. Somenzi. Hints to Accelerate Symbolic Traversal. In Correct Hardware Design and Verification Methods (CHARME’99), pages 250–264, Berlin, September 1999. Springer-Verlag. LNCS 1703.
M. K. Ganai, A. Aziz, and A. Kuehlmann. Enhancing Simulation with BDDs and ATPG. In Proc. 36th Design Automat. Conf., pages 385–390, New Orleans, LA, November 1999.
G. Cabodi, P. Camurati, and S. Quer. Efficient State Space Pruning in Symbolic Backward Traversal. In Proc. Int’l Conf. on Computer Design, pages 230–235, Cambridge, Massachussetts, October 1994.
S. G. Govindaraju and D. L. Dill. Verification by Approximate Forward and Backward Reachability. In Proc. Int’l Conf. on Computer-Aided Design, pages366–370, San Jose, California, November 1998.
K. Ravi and F. Somenzi. High-Density Reachability Analysis. In Proc. Int’l Conf. on Computer-Aided Design, pages 154–158, San Jose, California, November 1995.
G. Cabodi, P. Camurati, and S. Quer. Improving the Efficiency of BDD—based Operators by means of Partitioning. IEEE Transactions on CAD, 18(5):545–556, May 1999.
G. Cabodi, P. Camurati, and S. Quer. Improving Symbolic Reachability Analisys by means of Activity Profiles. IEEE Transactions on CAD, 19(9):1065–1075, September 2000.
R. Fraer, G. Kamhi, B. Ziv, M. Y. Vardi, and L. Fix. Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification. In E. Allen Emerson and A. Prasad Sistla, editors, Proc. Computer Aided Verification, volume 1855 of LNCS, pages 389–402, Chicago, Illinois, July 2000. Springer-Verlag.
I. Moon, J. Jang, G. D. Hachtel, F. Somenzi, J. Yuan, and C. Pixley. Approximate Reachability Don’t Cares for CTL Model Checking. In Proc. Int’l Conf. on Computer-Aided Design, pages 351–358, San Jose, California, November 1998.
R. K. Brayton et al. VIS. In Mandayam Srivas and Albert Camilleri, editors, Proc. Formal Methods in Computer-Aided Design, volume 1166 of LNCS, pages 248–256, Palo Alto, California, November 1996. Springer-Verlag.
G. Cabodi, P. Camurati, and S. Quer. Can BDDs compete with SAT solvers on Bounded Model Checking? In Proc. 39th Design Automat. Conf., New Orleans, Louisiana, June 2002.
S. G. Govindaraju, D. L. Dill, A. Hu, and M. A. Horowitz. Approximate Reachability Analysis with BDDs using Overlapping Projections. In Proc. 35th Design Automat. Conf., pages 451–456, San Francisco, California, June 1998.
G. Cabodi. Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions. In Gérard Berry, Hubert Comon, and Alan Finkel, editors, Proc. Computer Aided Verification, volume 2102 of LNCS, pages118–130, Paris, France, July 2001. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cabodi, G., Nocco, S., Quer, S. (2002). Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_38
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive