Reveal swMATH ID: 801 Software Authors: Andraus, Zaher S.; Liffiton, Mark H.; Sakallah, Karem A. Description: 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. Homepage: http://www.springerlink.com/content/x5n182m473410w08/fulltext.pdf Related Software: MiniSat; MUSer2; HMQV; Paracooba; Kissat; CaDiCaL; Z3str3; Rosette; GitHub; COMiniSatPS; JViews; AsmL; Yices; Calysto; EUFORIA; CTIGAR; MOPS; z3; SMT-LIB; SLAM Cited in: 22 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Reveal: A formal verification tool for Verilog designs. Zbl 1182.68111Andraus, Zaher S.; Liffiton, Mark H.; Sakallah, Karem A. 2008 all top 5 Cited by 48 Authors 3 Marques-Silva, João P. 2 Choo, Kim-Kwang Raymond 2 Feuerstein, Steven 2 Grünewald, Stefan 2 Huber, Katharina T. 2 Liffiton, Mark H. 2 Sakallah, Karem A. 1 Andraus, Zaher S. 1 Arabie, Phipps 1 Bjørner, Nikolaj S. 1 Boyd, Colin A. 1 Bueno, Denis 1 Chow, Sherman S. M. 1 Du, Zhihua 1 Feldman, Jerome A. 1 Heras, Federico 1 Hitchcock, Yvonne 1 Hubert, Lawrence J. 1 Ignatyev, Alexey A. 1 Janota, Mikoláš 1 Levatich, Maxwell 1 Lin, Feng 1 Llabrés, Mercè 1 Lopes, Nuno P. 1 Madhusudan, Parthasarathy 1 Malik, Ammar 1 Mathur, Umang 1 Mirkin, Boris G. 1 Morgado, António 1 Moulton, Vincent L. 1 Pérez-Muñuzuri, Vicente 1 Pérez-Villar, Vicente 1 Previti, Alessandro 1 Pribyl, Bill 1 Raz, Ran 1 Reed, Lisa A. 1 Rocha, Jairo 1 Roshan, Usman W. 1 Rosselló, Francesc 1 Rybalchenko, Andrey 1 Semple, Charles 1 Silipo, Damiano B. 1 Stamper, Richard 1 Tauman Kalai, Yael 1 Todd, Bryan S. 1 Valiente, Gabriel 1 Viswanathan, Mahesh 1 Vuppalapati, Chandrasekar all top 5 Cited in 10 Serials 2 Journal of Mathematical Biology 2 Constraints 1 Bulletin of Mathematical Biology 1 Journal of Philosophical Logic 1 Journal of Classification 1 Journal of Economics 1 Formal Aspects of Computing 1 Artificial Intelligence Review 1 Computational Biology and Chemistry 1 World Scientific Series on Nonlinear Science. Series B: Special Theme Issues and Proceedings all top 5 Cited in 10 Fields 11 Computer science (68-XX) 5 Biology and other natural sciences (92-XX) 3 Combinatorics (05-XX) 3 Operations research, mathematical programming (90-XX) 2 Mathematical logic and foundations (03-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 2 Information and communication theory, circuits (94-XX) 1 General and overarching topics; collections (00-XX) 1 Statistics (62-XX) 1 Numerical analysis (65-XX) Citations by Year