Chapter 10: Dealing with complexity

Abstract

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 ...

Get Formal Verification, 2nd Edition now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.