Protocol Verification as a Hardware Design Aid \Lambda

The role of automatic formal protocol verifica- tion in hardware design is considered. Principles are identified that maximize the benefits of pro- tocol verification while minimizing the labor and computation required. A new protocol description language and verifier (both called Mur') are de- scribed, along with experiences in applying them to two industrial protocols that were developed as part of hardware designs. 1 Introduction Most complex digital designs must be regarded as concur- rent systems: individual modules run in parallel and must coordinate by explicit synchronization and communication. Complexity will continue to increase, portending a shift in total design effort from, for instance, faster arithmetic cir- cuits, to mechanisms for coordination. Those mechanisms usually involve protocols: rules that, if followed by each party in a coordinated action, assure a desired outcome. Unfortunately, protocol design is a subtle art. Even when a designer exercises the utmost care, there is a strong possibility that he or she will fail to anticipate some possi- ble interaction among rules, resulting in errors and dead- locks. Even worse, the nondeterminism resulting from dif- fering internal states or delays means that resulting errors are often not reliably repeatable, making testing and de- bugging extremely difficult