About EBMC

EBMC is a complete Bounded Model Checker for hardware designs, i.e., not only discovers bugs, but is also able to prove the absence of bugs. It can read Netlists (ISCAS89 format), Verilog, and SMV files.

The unwound circuits can be exported as DIMACS CNF (bit-level) or in the SMT-LIB format (word-level).

Features:

• Bounded Model Checking (BMC)
• Completeness threshold computation with structural analysis
• Cut-point abstraction with counterexample guided refinement
• Supports fragment of System Verilog assertions for property specification
• k-induction
• Model Checking using bit-level interpolation for approximate image computation
• Model Checking using word-level interpolation for approximate image computation

Authors: Daniel Kroening and Mitra Purandare.

Documentation

The EBMC Manual describes the command line options of EBMC. We also provide papers that provide background on how EBMC works:

• Approximation Refinement for Interpolation-Based Model Checking
• Computational Challenges in Bounded Model Checking
• Computing Over-Approximations with Bounded Model Checking
• Efficient Computation of Recurrence Diameters

You should also read the license.

 

Benchmarks

• AIG_SMV_08.tar.gz (bit-level SMV files)
  

  EBMC can check the benchmarks used at the hardware model checking competition 2008. A PERL script is provided to run EBMC on these benchmarks. The PATH variable must include the location where the ebmc binary is located before you run the script.

• vcegar-benchmarks.tgz

Funding

This research is supported by the Semiconductor Research Corporation (SRC) under con­tract no. 2006-TJ-1539.