The PCI Specification Project

Goals

• Eliminate ambiguity

  An interface specification is an agreement between two parties. Ideally, based on this agreement, different parties can implement a machine respectively without any further communications . However, there are usually ambiguities in non-formal specifications which may result in the two parties creating machines which are not compatible due to differing interpretations of the ambiguous specification. Or, after agreeing on a specification, the two parties must constantly communicate with each other, to implement compatible systems. This may become a headache if there are numerous parties using the interface protocol (which is the case for most protocols).

  A formal specification is precise and concise and does not cause these problems.

• Eliminate contradictions

  With a non-formal, lengthy specification, it is very easy to specify a rule in one part of the specification and then specify a contradicting requirement somewhere else in the specification. With a formal, logical specification, this problem can be avoided entirely by doing an automatic logical analysis on the specification and have a program point out contradictions in the specification.

• Check correctness for all cases

  Protocols usually work as intended for majority of the cases. However, often there are chicoryer cases where a protocol acts in a non-intended, "bad" way. By having a logical specification which a program can analyze for every possible scenario, this problem is avoided.

PCI

And as a specification style which can easily be analyzed, we chose the monitor style.

Results

In addition, we have found several problems with the PCI protocol.

• Never giving up the bus

  The protocol is intended to never allow any one agent to "hog" the bus and not let other agents use the bus. However, if an agent asserts "IRDY#" from an idle state of ths bus, there is no rule forcing that agent to deassert "IRDY#" so that another agent can start a transaction on ths bus; the agent can forever stay in this state blocking out other agents.

• Changing its mind when it's not supposed to

  The current PCI protocol allows the target to change from signaling "target abort" to "disconnect with data" within the same transaction. Other combinations of signaling "change of mind"s exist. This leaves open the question of how a master should react to such confusing singaling from the target.

There were also other problems such as minor inconsistencies and confusing ambiguities in the PCI protocol. For example, in section 3.2.4, it is stated that TRDY# should use the address phase as a turnaround cycle (i.e. no agent is driving TRDY#), but for a back-to-back transaction, TRDY# will need to be driven (deasserted) during the address phase! ( more details).

Publications

Presentation Slides

Tutorial

1. A brief overview of the monitor-style specification including applications of such a specification.
2. How to write the monitor-style specification.

Download

1. Please read the Documentation first.
2. Here are the Instructions .

For Advanced Users

Investigators

We would very much like feedback on this project. Please send any thoughts, comments, suggestions to kannas@ofb.net. If you know of any protocols which will challenge our method, we really want to know about them! Thank you.