Formal Verification of Complex Data Paths: An Industrial Experience

After caches, most transistors in a modern microprocessor are devoted to wide data-paths. Due to performance and power requirements, these data-paths often use complex implementations of sophisticated algorithms. As Intel experienced in 1994, a bug in a data-path can be extremely expensive and thus needs to be avoided at almost any cost. At the same time, simulation based verification is extremely poor at verifying data-paths due to the vast data space and thus formal verification is almost a requirement. In this paper a retrospective is given of the formal verification of complex data-paths that took place at Intel from the mid 1990\ua0s until very recently. The technology that made the effort possible, the tools developed that made it feasible, and the methodology created that made it practical will all be discussed. Finally, a few examples that illustrates the approach will be presented as well as a concluding discussion on what the goal of using formal verification should be