Abstract
Abstraction-guided simulation is a general framework for automatically harnessing, during simulation, information from abstraction and model checking. EverLost is our platform for industrial-strength abstraction-guided simulation. EverLost takes an RTL Verilog design and preimage/abstraction information from any BDD-based abstraction/model-checking tool, and automatically generates code that implements abstraction-guided simulation and directly compiles with the design under the widely-used Synopsys VCS simulator. The platform enables flexible exploration of abstraction-guided simulation — different formal tools and guidance heuristics are easily inserted — while providing the capacity, speed, and Verilog compatibility of a leading industry-standard tool.
Supported by an NSERC Discovery Grant. We would also like to thank Daniel Kroening and Himanshu Jain for their help with the vcegar tool.
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
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Boppana, V., Rajan, S.P., Takayama, K., Fujita, M.: Model checking based on sequential ATPG. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 418–430. Springer, Heidelberg (1999)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Conf. on Logic in Computer Science, pp. 428–439 (1990)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Edelkamp, S., Lluch-Lafuente, A.: Abstraction in directed model checking. In: Workshop on Connecting Planning Theory and Practice, pp. 7–13 (2004)
Jain, H., Kroening, D., Sharygina, N., Clarke, E.: Word level predicate abstraction and refinement for verifying RTL verilog. In: 42nd Design Automation Conf., pp. 445–450 (2005)
Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
Shyam, S., Bertacco, V.: Distance-guided hybrid verification with GUIDO. In: Design Automation and Test in Europe, pp. 1211–1216 (2006)
Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: 35th Design Automation Conf., pp. 599–604 (1998)
USB 1.1 PHY., http://www.opencores.org/projects.cgi/web/usb_phy/overview
USB 2.0 Function Core, http://www.opencores.org/projects.cgi/web/usb/overview
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Paula, F.M., Hu, A.J. (2006). EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_27
Download citation
DOI: https://doi.org/10.1007/11817963_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)