Formal Verification

Chapter 10

Dealing with complexity

In Chapter 10, we describe ways to address complexity issues, enabling formal verification on designs that initially might seem too large or logically complicated for tools to handle. After reviewing the general concepts of state space and complexity, we describe several complexity reduction techniques on a memory controller example. Simple techniques include black boxing, case splitting, property simplification, and cut points. Generalizing analysis with free variables is also often useful. We then describe several types of abstraction models: datapath abstraction, symmetry exploitation, counter abstraction, sequence abstraction, and memory abstraction. We conclude with descriptions of creating partial “shadow” ...