## Equivalence Checking of Digital Circuits: Fundamentals, Principles, MethodsHardware verification is the process of checking whether a design conforms to its specification of functionality. In today's design processes it becomes more and more important. Very large scale integrated (VLSI) circuits and the resulting digital systems have conquered a place in almost all areas of our life, even in security sensitive applications. Complex digital systems control airplanes, have been used in banks and on intensive-care units. Hence, the demand for error-free designs is more important than ever. In addition, economic reasons underline this demand as well. The design and production process of present day VLSI-circuits is highly time- and cost-intensive. Moreover, it is nearly impossible to repair integrated circuits. Thus, it is desirable to detect design errors early in the design process and not just after producing the prototype chip. All these facts are reflected by developing and production statistics of present day companies. For example, nowadays about 60% to 80% of the overall design time is spent for verification. This shows that verifying logical correctness of the design of hardware systems is a major gate to the problem of time-to-market. With the chip complexity constantly increasing, the difficulty as well as the importance of functional verification of new product designs has been increased. It is not only more important to get error-free designs. Moreover, it becomes an increasingly difficult task for a team of human designers to carry out a full design without errors. The traditional training of new verification engineers has to be adapted to the new situation. New skills are necessary. For these reasons, nearly all major universities offer lectures on basic verification techniques such as propositional temporal logic, model checking, equivalence checking, and simulation coverage measures. The present book is designed as a textbook covering one of the most important aspects in the verification process – equivalence checking of Boolean circuits. Equivalence Checking of Digital Circuits is a textbook for advanced students in electrical and computer engineering, but is also intended for researchers who will find it useful as a reference text. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

PRELIMINARIES | 11 |

PseudoBoolean functions | 23 |

4 | 30 |

Truth tables | 71 |

Boolean formulae | 83 |

SAT AND ATPG BASED EQUIVALENCE CHECKING | 99 |

EXPLOITING SIMILARITIES | 131 |

PARTIAL IMPLEMENTATIONS | 145 |

PERMUTATION INDEPENDENT BOOLEAN COMPARISON | 169 |

BASIC DEFINITIONS AND ALGORITHMS | 209 |

11 | 213 |

LATCH CORRESPONDENCE PROBLEM | 227 |

References | 243 |

12 | 244 |

253 | |

About the Athors | 263 |

### Other editions - View all

Equivalence Checking of Digital Circuits: Fundamentals, Principles, Methods Paul Molitor,Janett Mohnke No preview available - 2004 |

### Common terms and phrases

algorithm aliasing groups applied approach assigned value automatic test pattern backward construction binary decision diagrams black box black box BB1 Bn,m Boolean formula Boolean network canonical Chapter cofactor computed conjunctive normal form cutpoints cutset variables defined Definition denote encoding equivalence checking error-free example EXOR EXOR EXOR-gate F and G false negative fanout fault finite state machines formal verification FSMs function f function signature functionally equivalent G–symmetry implication graph input permutation input signature function integer multiplier internal node iteration J-frontier Lemma logic m-ary Boolean function miter NAND NAND NAND one-literal clause operator node output signature partial implementation partition primary output problem pseudo–Boolean function representation respect ROBDD Section sequential circuits shown in Figure single-output Boolean functions space traversal subsets symbolic symbolic simulation symmetric variables symmetry terminal node Theorem unate uniquely identified variable assignments variable order variable xi verification word-level