Monitor-Based Formal Specification of PCI

Kanna Shimizu, David L. Dill, Alan J. Hu

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


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.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:39
Start Conference Manager
Conference Systems