7 - Decision diagrams for verification

Summary

Introduction

Having matured over the years, formal design verification methods, such as theorem proving, property and model checking, and equivalence checking, have found increasing application in industry. Canonical graph-based representations, such as binary decision diagrams (BDDs), [1] binary moment diagrams (BMDs), [2] and their variants, play an important role in the development of software tools for verification. While these techniques are quite mature at the structural level, the high-level verification models are only now being developed. The main difficulty is that such verification must span several levels of design abstraction. Verification of arithmetic designs is particularly difficult because of the disparity in the representations on the different design levels and the complexity of logic involved.

This chapter addresses verification based on canonical data structures. It presents several canonical, graph-based representations that are used in formal verification, and, in particular, in equivalence checking of combinational designs specified at different levels of abstraction. These representations are commonly known as decision diagrams, even though not all of them are actually decision-based forms. They are graph based structures whose nodes represent the variables and whose directed edges represent the result of the decomposition of the function with respect to the individual variables. Particular attention is given to arithmetic and word-level representations.

An important common feature of all these representations is canonicity, which is essential in combinational equivalence checking. A form is canonical if the representation of a function in that form is unique. Canonical graph-based representations make it possible to check whether two combinational functions are equivalent by checking whether their graph-based representations are isomorphic.