Counterexample Guided Abstraction and Refinement
VCGEAR is a tool for
checking safety properties (assertions) of Verilog programs. The
input to the tool is a Verilog description and a property. The
output is either the property holds or a real counterexample showing
how the property is violated.
VCEGAR uses word level predicate
abstraction and refinement for checking properties of RTL
VCGEAR, contact Himanshu Jain or Daniel Kroening.
03/24/2005: The x86 Linux binary of
VCEGAR 0.9 released.
07/15/2006: The x86 Linux binary of
VCEGAR 1.0 released.
01/22/2007: The x86 Linux binary of
VCEGAR 1.1 released.
03/20/2007: The Cygwin binary of
VCEGAR 1.1 released.
07/31/2007: The x86 Linux binary of
VCEGAR 1.3 released.
11/04/2008: The x86 Linux binary of
VCEGAR 1.5 released.
Following papers describe
the technical details about the working of the tool.
- Word Level Predicate Abstraction and Refinement for Verifying RTL
Verilog. (available online)
In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems.
Revised and expanded version of DAC 2005 paper.
- VCEGAR: Verilog CounterExample Guided Abstraction Refinement. (tool description ) (ps)
In 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007).
- Word Level Predicate Abstraction and Refinement for
Verifying RTL Verilog. (ps)
In 42nd Design Automation Conference (DAC 2005).
Nominated for DAC 2005 best paper award.
- Technical report (ps)
- Conference presentation (ppt)
We currently distribute binaries for
x86 Linux and Cygwin under Windows.
If you wish to perform
experimental comparison with VCEGAR, please let us know in
advance so that we can provide you with the latest version of the
| This research was sponsored by the Gigascale Systems
Research Center (GSRC), the National Science Foundation (NSF) under
grant no. CCR-9803774, the Office of Naval Research (ONR), the Naval
Research Laboratory (NRL) under contract no. N00014-01-1-0796, and by
the Defense Advanced Research Projects Agency, and the Army Research
Office (ARO) under contract no. DAAD19-01-1-0485. The views and
conclusions contained in this document are those of the author and
should not be interpreted as representing the official policies, either
expressed or implied, of GSRC, NSF, ONR, NRL, DOD, ARO, or the U.S.