A Specification Methodology by a Collection of Compact Properties as
Applied to the Intel Itanium Processor Bus Protocol
Kanna Shimizu, David L. Dill, Ching-Tsun Chou
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.