PV3 VCEGARchecks user-specified safety properties for Verilog programs

VCEGAR is a tool for checking safety properties (assertions) of Verilog programs

Application domain/field

Type of tool

Model checker

Expected input

Format:

Expected output

Property holds or a counterexample showing how the property is violated.

Internals

Uses predicate abstraction and a refinement loop (CEGAR).
Hardware Model checking

Links

Project page: https://www.cs.cmu.edu/~modelcheck/vcegar/

Last commit date

11 April 2008 (last release date)

Related papers

Last publication date

2007

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.