EBMC

About EBMC

EBMC Logo 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:

Versions up to (including) 4.1 have also supported the following methods:

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:

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.

Benchmarks

Funding

This research was supported by the Semiconductor Research Corporation (SRC) under con­tracts no. 2006-TJ-1539, 2012-TJ-2269 and 2016-CT-2707.