EBMC – A Model Checker for Verilog Designs
Table of Contents
- Checking a combinational circuit
- Property specification on the command line
- Bounded verification of a sequential circuit
- Specifying the reset logic
- What are traces and what are they used for?
- Counterexample traces for safety properties
- Horizontal ("waveform") traces
- Using the VCD dump
- What is a Liveness Property?
- Writing Liveness Properties in SVA
- Refuting Liveness Properties with Bounded Model Checking
- Unbounded Proof with BDDs
- Unbounded Proof with k-induction