PV3 EBMCchecks assertions/properties against a Verilog/Netlists/… spec

EBMC is a model checker for hardware designs. It includes both bounded and unbounded analysis, i.e., it can both discover bugs and is also able to prove the absence of bugs.

Application domain/field

Type of tool

Model checker

Expected input


Expected output

Per failure it will report whether it could prove it (SUCCESS) or not (FAILURE). When EBMC refutres a property, it will compute a counterexample (path from initial state to an error state).


EBMC supports bounded and unbounded analysis. It uses k-induction, bounded model checking (BMC) and a BDD engine. The BDD engine and k-induction are used for unbounded safety verification. BMC is used to check liveness properties.
Hardware LTL Model checking


Related papers

Last publication date


ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.