Monitor-Based Formal Specification of PCI

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 severa...

• Type: Conference
• Year: 2000
• Where: FMCAD
• Authors: Kanna Shimizu, David L. Dill, Alan J. Hu
• Keywords: FMCAD 2000, Formal Methods, Formal Specification, Monitor Specification, Specification