CEGAR+SMT: Formal Verification of Control Logic in the Reveal System
The paradigm of iterative abstraction and refinement has gained momentum in recent years as a particularly effective approach for the scalable verification of complex hardware and software systems. Dubbed CounterExample-Guided Abstraction Refinement (CEGAR), its power stems from the elimination (i.e., abstraction) of details that are irrelevant to the property being checked and from analyzing any spurious counterexamples to pinpoint and add just those details that are needed to refine the abstraction, i.e., to make it more precise. Originally pioneered by Kurshan \cite
, it has since been adopted by several researchers as a powerful means for coping with verification complexity. In particular, the use of abstraction-based verification has been thoroughly studied in the context of model checking by Clarke
\cite
and Cousot and Cousot \cite
for over two decades. Later methods by Clarke
\cite
, Das
\cite
and Jain
\cite
have successfully demonstrated the automation of abstraction and refinement in the context of model checking for safety properties._
Whereas such a verification paradigm is appealing at a conceptual level, its success in practice hinges on effective automation of the abstraction and refinement steps, as well as the various checking steps requiring sophisticated reasoning. In this talk, I will describe how these issues are addressed by Reveal, an automatic CEGAR-based verification system. Reveal is used to formally verify complex hardware designs, including pipelined microprocessors whose Register-Transfer Level (RTL) descriptions have tens of thousands of Hardware Description Language (HDL) source lines, thousands of signals, and hundreds of thousands of state bits.
Specifically, I will describe Reveal's overall CEGAR flow and its abstraction and refinement algorithms. I will also analyze its behavior and compare its performance on several representative test cases against several existing automatic tools that perform formal verification of hardware, such as VCEGAR \cite
, BAT \cite
, UCLID \cite
, and VIS \cite
. For each test case, I will compare a number of methods to model and check the desired properties on the abstract design, including the use of a
(SMT) solver \cite
. I will also demonstrate the trade-offs between various refinement options, highlight the types of lemmas generated in the refinement stage, and analyze the idiosyncrasies leading to them. I will conclude with a brief update on the commercialization of Reveal technology and its use in an industrial verification setting.
The paradigm of iterative abstraction and refinement has gained momentum in recent years as a particularly effective approach for the scalable verification of complex hardware and software systems. Dubbed CounterExample-Guided Abstraction Refinement (CEGAR), its power stems from the elimination (i.e., abstraction) of details that are irrelevant to the property being checked and from analyzing any spurious counterexamples to pinpoint and add just those details that are needed to refine the abstraction, i.e., to make it more precise. Originally pioneered by Kurshan \cite
, it has since been adopted by several researchers as a powerful means for coping with verification complexity. In particular, the use of abstraction-based verification has been thoroughly studied in the context of model checking by Clarke et al. \cite
and Cousot and Cousot \cite
for over two decades. Later methods by Clarke et al. \cite
, Das et al} \cite
and Jain et al. \cite
have successfully demonstrated the automation of abstraction and refinement in the context of model checking for safety properties.
Whereas such a verification paradigm is appealing at a conceptual level, its success in practice hinges on effective automation of the abstraction and refinement steps, as well as the various checking steps requiring sophisticated reasoning. In this talk, I will describe how these issues are addressed by Reveal, an automatic CEGAR-based verification system. Reveal is used to formally verify complex hardware designs, including pipelined microprocessors whose Register-Transfer Level (RTL) descriptions have tens of thousands of Hardware Description Language (HDL) source lines, thousands of signals, and hundreds of thousands of state bits.
Specifically, I will describe Reveal's overall CEGAR flow and its abstraction and refinement algorithms. I will also analyze its behavior and compare its performance on several representative test cases against several existing automatic tools that perform formal verification of hardware, such as VCEGAR \cite
, BAT \cite
, UCLID \cite
, and VIS \cite
. For each test case, I will compare a number of methods to model and check the desired properties on the abstract design, including the use of a Satisfiability Modulo Theories (SMT) solver \cite
. I will also demonstrate the trade-offs between various refinement options, highlight the types of lemmas generated in the refinement stage, and analyze the idiosyncrasies leading to them. I will conclude with a brief update on the commercialization of Reveal technology and its use in an industrial verification setting.
Karem Sakallah
, University of Michigan, Ann Arbor, USA
put your bio here