Formal Verification of Arithmetic Circuits

Abstract

As designs are becoming more complex while the time-to-market window is getting shorter, it is important that designers can locate pre-silicon errors at an early stage. Beside logic simulation and timing verification, formal verification is becoming a viable solution to improve design quality. This seminar will first motivate the topic by presenting microprocessor design trends regarding performance, area and productivity. Traditionally formal verification has been applied to control circuits and various protocols successfully. We found that formal verification of arithmetic circuits is both important and feasible, which will be the focus of this seminar. An industrial strength FV tool called word-level model checking will be presented which uses HDDs (BDDs+BMDs) to compactly represent mixed arithmetic/control functions. A suite of enabling FV techniques will also be presented, with which a large class of floating-point arithmetic circuits can be automatically verified and debugged using word-level model checking.