| It is widely recognized that writing solid specifications for design interfaces is critical in this day of complex, multi-module hardware designs. However, many still resort to natural languages such as English to document interface protocols such as those of busses and IP (intellectual property) cores. Consequently, these protocols are often buggy and are frequently mis-communicated due to the inherent ambiguity of natural language specifications. Formal specifications, with precisely defined symbols and semantics, will resolve many of these problems, but in practice, they are seldom written. They are usually perceived as too difficult to develop and not very valuable beyond their role as documents.; A two-pronged approach to this problem will be presented. First, the thesis introduces a methodology that facilitates formal specification development for commonly used interface protocols. The popular PCI bus protocol and the Intel Itanium bus protocol (preliminary version) have been successfully specified with this method. Furthermore, the methodology's debugging techniques have uncovered previously unreported bugs and issues with these protocols.; Second, the thesis describes how formal specifications can be used to automate many procedures that are now done manually. For example, to verify a design using simulation, test inputs and checking properties must first be written, and this process require considerable expertise and effort. However, if there is a formal specification, the test inputs and the checking properties can be generated automatically from it. This technique was used to simulate and verify the I/O component from the Stanford FLASH project whereby new bugs were found in the design and manual work was kept to a minimum. |
