Monitor-Based Formal Specification of PCI
Kanna Shimizu, David L. Dill, Alan J. Hu
Bus protocols are hard to specify correctly, and yet it is often critical and
highly beneficial that their specifications are correct, complete, and
unambiguous. The informal specifications currently in use are not adequate
because they are difficult to read and write, and cannot be functionally
verfied by automated tools. Formal specifications, promise to eliminate
these problems, but in practice, the difficulty of writing them limits their
widespread acceptance. This paper presents a new style of
specification based on writing the interface specification as a formal
monitor, which enables the formal specification to be simple to write, and
even allows the description to be written in existing HDLs. Despite the
simplicity, monitor specifications can be used to specify industry-grade
protocols. Furthermore, they can be checked automatically for internal
consistency using standard model checker tools, without any protocol
implementations. They can be used without modification for several other
purposes, such as formal verification and system simulation of
implementations. Additionally, it is proved that specifications written in this
style are receptive, guaranteeing that implementations are possible.
The effectiveness of the monitor specification is demonstrated by formally
specifying a large subset of the PCI 2.2 standard and finding several bugs in
the standard.