EBMC – A Model Checker for Verilog Designs

Table of Contents

1. A Short Tutorial

• Checking a combinational circuit
• Bounded verification of a sequential circuit
• Specifying the reset logic

2. Working with EBMC Traces

• What are traces and what are they used for?
• Counterexample traces for safety properties
• Horizontal ("waveform") traces
• Using the VCD dump

3. Checking Liveness Properties Using EBMC

• What is a Liveness Property?
• Writing Liveness Properties in SVA
• Refuting Liveness Properties with Bounded Model Checking

4. Unbounded Proof Using EBMC

• Unbounded Proof with BDDs
• Unbounded Proof with k-induction

5. Verilog Language Features