IBM Logo
IBM Research Lab in Haifa
Hot Shots  
FV Research in HRL  

Download the presentation

Dave Reed



Formal Methods in Processor Developments at AMD

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.