vcegar logo  
 Verilog Counterexample Guided Abstraction and Refinement 
About
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 Verilog programs.   

For questions about VCGEAR, contact Himanshu Jain or Daniel Kroening.

News
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.  

 


Documentation

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) (pdf)
    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) (pdf)
    In 42nd Design Automation Conference (DAC 2005).
    Nominated for DAC 2005 best paper award.

    • Technical report  (ps) (pdf). 
    • Conference presentation (ppt)

 

Download

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 tool.

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. government.