X86 processors are evolving to be composed of multiple execution units involving out of
order execution, employing ever increasing complexity of instruction set architecture.
The resulting problems of functional verification are seen to increase beyond the scope
of traditional verification methods such as simulation. This same complexity has made bugs
harder to find and more prevalent, while market pressures increase the cost of residual bugs.
This problem is further complicated by continuously decreasing product life cycles with
increasingly aggressive development schedules.
In this presentation, we will give an overview of the AMD processor design group's
experience with formal methods in dealing with functional verification. We will review the
factors and experiences that haveled to the successful use of theorem proving, and ACL2 in
particular, as a major player in functional verification. Our design flow imposes constraints,
for example restricting us to an AMD-specific language for the rtl. We will discuss how
such constraints, together with methodological concerns such as level of abstraction,
continue to direct our formal methods interests.