EBMC
About EBMC
EBMC is an open-source Model Checker for hardware designs. It can read netlists (given in ISCAS89 format), Verilog, System Verilog and SMV files. Properties can be given in LTL or a fragment of System Verilog Assertions. It includes both bounded and unbounded analysis, i.e., it can both discover bugs and is also able to prove the absence of bugs.
The unwound circuits can be exported as DIMACS CNF (bit-level) or in the SMT-LIB 2 format (word-level).
Features:
- System Verilog assertions for property specification
- Bounded Model Checking (BMC)
- unbounded proof with k-induction engine
- unbounded proof with BDD engine
Versions up to (including) 4.1 have also supported the following methods:
- Completeness threshold computation with structural analysis
- Cut-point abstraction with counterexample-guided refinement
- 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.
EBMC News
NEW: There is now a Google Group for annoucements related to EBMC.
EBMC 4.4 released on 3.7.2017!
Documentation
The EBMC Manual describes the command line options of EBMC.
We also provide papers that provide background on how EBMC works:
- Hardware Verification using Software Analyzers
- 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 (BSD 3-clause).
Download
We currently only distribute binaries for x86 Linux and Windows. The source code is available on github.
- Linux x86 binary: ebmc-4-1-linux-32.tgz
Linux x64 binary: ebmc-4-2-linux-64.tgz
Linux x64 binary: ebmc-4-4-linux-64.tgz
Command to extract the binary: tar xvfz ebmc-4-4-linux-64.tgz - Windows x86 binary: ebmc-4-1-win.zip
Windows x86 binary: ebmc-4-2-win.zip
Windows x64 binary: ebmc-4-4-win-64.zip
Double-click to unpack. This is a command-line utility.
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 was supported by the Semiconductor Research Corporation (SRC) under contracts no. 2006-TJ-1539, 2012-TJ-2269 and 2016-CT-2707.