Bus protocols are hard to specify correctly, and yet it is often critical and
highly beneficial that their specifications are correct and unambiguous. The
informal specifications currently in use are not adequate because they are
difficult to read and write, and cannot be checked for correctness 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 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 bus interface designs. 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.
