Reveal: A Formal Verification Tool for Verilog Designs

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 all 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 relined 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 process is iterated until the design is shown to be correct or all 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 oil our initial experience with this system, we believe that automating the verification for a useful class of hardware designs is now quite feasible.