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.

References in zbMATH (referenced in 19 articles , 1 standard article )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Ignatiev, Alexey; Janota, Mikoláš; Marques-Silva, Joao: Quantified maximum satisfiability (2016)
  2. Liffiton, Mark H.; Previti, Alessandro; Malik, Ammar; Marques-Silva, Joao: Fast, flexible MUS enumeration (2016)
  3. Morgado, Antonio; Heras, Federico; Marques-Silva, Joao: Improvements to core-guided binary search for MaxSAT (2012)
  4. Andraus, Zaher S.; Liffiton, Mark H.; Sakallah, Karem A.: Reveal: A formal verification tool for Verilog designs (2008)
  5. Grünewald, S.; Huber, K.T.; Wu, Q.: Two novel closure rules for constructing phylogenetic super-networks (2008)
  6. Grünewald, Stefan; Huber, Katharina T.; Moulton, Vincent; Semple, Charles: Encoding phylogenetic trees in terms of weighted quartets (2008)
  7. Kalai, Yael Tauman; Raz, Ran: Interactive PCP (2008)
  8. Chow, Sherman S.M.; Choo, Kim-Kwang Raymond: Strongly-secure identity-based key agreement and anonymous extension (2007)
  9. Llabrés, Mercè; Rocha, Jairo; Rosselló, Francesc; Valiente, Gabriel: On the ancestral compatibility of two phylogenetic trees with nested taxa (2006)
  10. Choo, Kim-Kwang Raymond; Boyd, Colin; Hitchcock, Yvonne: On session key construction in provably-secure key establishment protocols (2005)
  11. Du, Zhihua; Lin, Feng; Roshan, Usman W.: Reconstruction of large phylogenetic trees: a parallel approach (2005)
  12. Silipo, Damiano B.: The evolution of cooperation in patent races:Theory and experimental evidence (2005)
  13. Feuerstein, Steven: Oracle PL/SQL programming. Guide to Oracle8i features. Translated from the English by Wolfgang Gabriel. Incl. 1 disc (2000)
  14. Feuerstein, Steven; Pribyl, Bill: Oracle PL/SQL programming (1999)
  15. Reed, Lisa A.: Necessary versus probable cause (1999)
  16. Pérez-Muñuzuri, Vicente (ed.); Pérez-Villar, Vicente (ed.): Discretely-coupled dynamical systems. Proceedings of the workshop, Univ. of Santiago de Compostela, Spain, June 24--28, 1995 (1997)
  17. Mirkin, Boris; Arabie, Phipps; Hubert, Lawrence J.: Additive two-mode clustering: The error-variance approach revisited (1995)
  18. Todd, Bryan S.; Stamper, Richard: A formal model of explanation (1995)
  19. Feldman, Jerome A.: Structured connectionist models and language learning (1993)