Experience with Applying Formal Methods to Protocol Specification and System Architecture Ching-Tsun Chou In the last three years or so we at Enterprise Platforms Group at Intel Corporation have been applying formal methods to various problems that arose during the process of defining platform architectures for Intel's processor families. The problems we have worked on include formal verification of directory-based cache coherence protocols, formal analysis of variations of sliding window protocols, and several novel applications of binary decision diagrams (rule-based checking of specification tables, search for minimal deadlock-free wormhole routing schemes, and search for fault-tolerant link initialization sequences). We also developed a verification methodology in which the models under verification are automatically generated from specification tables and both the ``syntax'' (via rule-based table checking) and ``semantics'' (via model checking) of the models are formally verified. We believe that architectural definition affords a rich and fruitful area for the application of formal methods, for several reasons. First, architectural definition is at the right level of abstraction for formal methods to be applied to system-level verification in a meaningful manner; any system description with more lower-level details would overwhelm the limited capacity of currently available formal techniques and tools. Second, applying formal techniques at the definition stage makes architects aware of the verification issues and challenges and encourages them to select from a plethora of possible schemes one that is most amenable to complete verification. Third, a close relationship between architects and FV experts developed through their interactions also encourages a more meaningful selection and abstraction of issues to be scrutinized by formal methods. Last but not least, since a typical implementation exercises only a subset of all allowed options in an architectural specification, applying formal methods to the specification enables the exploration of design spaces that are beyond the scope of any particular implementation. We learned several lessons from our experience. First, formal modeling steered us toward more precise and concrete protocol specifications than we would have written without it. Second, formal modeling also turned out to be an excellent way to help architects articulate their ideas. Third, Formal verification gave us much higher confidence in the correctness of our protocol specifications than we would have had without it. It is our view that certain protocols, such as directory-based cache coherence protocols and certain variations of sliding window protocols, are simply too complex for unaided human reasoning or simulation alone to get correct. Finally, formal verification also made it less risky for us to modify protocol specifications. Acknowledgements: Mani Azimi, Jay Jayasimha, Akhilesh Kumar, Victor W. Lee, Phanindra K. Mannava, Seungjoon Park, and Aniruddha Vaidya all contributed to the work described above.