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