Formal hardware verification with BDDs: an introduction

This paper is a brief introduction to the main paradigms for using BDDs (binary decision diagrams) in formal hardware verification. The paper addresses two audiences: for people doing theoretical BDD research, the paper gives a glimpse of the problems in the main application area; and for people building hardware, the paper gives a peek under the hood of the formal verification technologies that are rapidly gaining industrial importance. Topics described include combinational equivalence checking, symbolic simulation, sequential equivalence checking, model checking and symbolic trajectory evaluation.