Fitting Formal Methods into the Design Cycle

This tutorial introduces several methods of formal hardware verication 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 t 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.

• Type: Conference
• Year: 1994
• Where: DAC
• Authors: Kenneth L. McMillan
• Keywords: Computer Architecture, DAC 1994, Design Process, Formal Guarantees, Formal Hardware Veri