In practice, formal specifications are often considered too costly for the benefits they promise. Specifically, interface
specifications such as standard bus protocol descriptions are still documented informally, and although many admit formal
versions would be useful, they are dissuaded by the time and effort needed for development.
We champion a formal specification methodology that attacks this cost-value problem from two angles. First, the framework
allows formal specifications to be feasible for signal-level bus protocols with minimal effort,lowering costs. And second,
a specification written in this style has many different uses, other than as a precise specification document, resulting in
increased value over cost. This methodology allows the specification to be easily transformed into an executable checker or
an simulation environment, for example.
In an earlier paper, we demonstrated the methodology on a widely-used bus protocol. Now, we show that the generalized methodology
can be applied to more advanced bus protocols, in particular, the Intel® Itanium™ Processor bus protocol. In addition, the
paper outlines how writing and checking such a specification revealed interesting issues, such as deadlock and missed data
phases, during the development of the protocol.