Abstract
We describe the Reveal formal functional verification system and its application to four representative hardware test cases. Reveal employs counterexample-guided abstraction refinement, or CEGAR, and is suitable for verifying the complex control logic of designs with wide datapaths. Reveal performs automatic datapath abstraction yielding an approximation of the original design with a much smaller state space. This approximation is subsequently used to verify the correctness of control logic interactions. If the approximation proves to be too coarse, it is automatically refined based on the spurious counterexample it generates. Such refinement can be viewed as a form of on-demand “learning” similar in spirit to conflict-based learning in modern Boolean satisfiability solvers. The abstraction/refinement process is iterated until the design is shown to be correct or an actual design error is reported. The Reveal system allows some user control over the abstraction and refinement steps. This paper examines the effect on Reveal’s performance of the various available options for abstraction and refinement. Based on our initial experience with this system, we believe that automating the verification for a useful class of hardware designs is now quite feasible.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Andraus, Z., Liffiton, M., Sakallah, K.: Refinement strategies for verification methods based on datapath abstraction. In: Proc. of Asia and South Pacific Design Automation Conference, pp. 19–24 (2006)
Andraus, Z., Liffiton, M., Sakallah, K.: CEGAR-based formal hardware verification: a case study. Technical Report CSE-TR-531-07, University of Michigan (2007)
Andraus, Z., Sakallah, K.: Automatic abstraction and verification of Verilog models. In: Proc. of Design Automation Conference, pp. 218–223 (2004)
Bryant, R., Lahiri, S., Seshia, S.: Modeling and verifying systems using a logic of counter arithmetic with Lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78–92. Springer, Heidelberg (2002)
Burch, J., Dill, D.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems (TOPLAS) 16(5), 1512–1542 (1994)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Sixth Annual ACM SI PLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238–252 (2006)
Das, S., Dill, D.: Successive approximation of abstract transition relations. In: IEEE Symposium on Logic in Computer Science, pp. 51–58 (2001)
Dutertre, B., de Moura, L.: A fast linear arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Brayton, R., et al.: VIS: a system for verfication and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 428–432. Springer, Heidelberg (1996)
Hensessy, J., Patterson, D.: Computer Architecture: A Quantitative Approach, 2nd edn. Morgan Kaufmann, San Francisco (1996)
Jain, H., Kroening, D., Sharygina, N., Clarke, E.: Word-level predicate abstraction and refinement for verifying RTL Verilog. In: Proc. of Design Automation Conference, pp. 445–450 (2005)
Kurshan, R.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoritic Approach. Princeton University Press, Princeton (1999)
Manolios, P., Srinivasan, S., Vroon, D.: Automatic memory reductions for rtl model verification. In: Proc. of Int’l. Conference on Computer-Aided Design, pp. 786–793 (2006)
Wang, F., Li, B., Jin, H., Hachtel, G., Somenzi, F.: Improving Ariadne’s Bundle by following multiple threads in abstraction refinement. In: Proc. of Int’l. Conference on Computer-Aided Design, pp. 408–415 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andraus, Z.S., Liffiton, M.H., Sakallah, K.A. (2008). Reveal: A Formal Verification Tool for Verilog Designs. In: Cervesato, I., Veith, H., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2008. Lecture Notes in Computer Science(), vol 5330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89439-1_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-89439-1_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89438-4
Online ISBN: 978-3-540-89439-1
eBook Packages: Computer ScienceComputer Science (R0)