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

• Model checking
• Hardware design

Type of tool

Model checker

Expected input

• Synthesizable hardware design at register transfer level (RTL)
• Safety or liveness property

Format:

• Hardware design: Verilog, Netlists (ISCA89 format), System Verilog or SMV file
• https://www.cprover.org/ebmc/manual/verilog_language_features/ (describes the synthesizable subset of Verilog)
• Property: SystemVerilog assertions or LTL

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).

Internals

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.