Fitting Formal Methods into the Design Cycle

This tutorial introduces several methods of formal hardware verification that could potentially have a practical impact on the design process. The measure of success in integrating these methods into a design methodology is arguably not the ability to provide formal guarantees of correctness, but rather to detect design errors in a timely manner, as the design evolves. Based on this criterion, and some limited practical experience, we consider where the various methods might fit into the life cycle of a design, what their capabilities and shortcomings are, and how the design process might change in order to accommodate formal methods.