How to Write a Monitor-Style Specification

1. Write the Specification

How to write such a monitor? The basic idea is to avoid complicated state machines and to keep the specification as simple as possible (to avoid adding bugs of your own!). Keeping code which records a history of what the observed machines have done, and code which specifies what the machine should be doing now, separate is very important and extremely helpful in keeping the specification flat and uncomplicated. A good specification will have the observational functionality and the specification functionality separate.

1.1 Three Types of State Machines

With PCI, for the history-recording observational part, only three types of state machines, were needed.

The previous state
These are variables which have the value of some variable in the previous state. For example, p_foo is the value of foo one clock cycle priot to the current clock cycle. For such a state machine, the assignment "p_foo = foo" happens on every clock.
The counter
In PCI, there are some rules which are time-binding; some actions must happen within a constant number of clock cycles. Thus, a counter-type state machine will start couting due to some "trigger" event and stop counting and clear due to a "clear" event. Based on a counter value, rules can be stated. For example, there is a counter for counting clock cycles since FRAME# has been asserted and this is used to state a rule about FRAME# and timeouts.
The boolean history flag
The boolean history flag becomes true when a "trigger" condition becomes true, and remains true until a "clear" condition becomes true, wherein it becomes false. For example, there is a history flag for whether a write transaction was requested in the address phase. This is needed because the monitor needs to "remember" what the current transaction type is.

1.2 The Rules

Now, using the state machines described above, the rules must be written out. We have found that all PCI rules fall in two categories.

current signal condition IMPLIES current signals to be in a certain state
past history condition IMPLIES current signals to be in a certain state

The past history condition will be an expression comprised of the state machines described above. Please spend some time looking at examples of PCI rules to get a better idea of what these rules are like.

1.3 Putting it Together

Now, the monitor is simply a clocked machine observing the different agents using the protocol, and at each clock, checking whether all the rules are being upheld by the agents. It also updates the state machines based on its oberservation of the agents.

2. Check the Specification

Now that the specification is written, how can one be confident that the rules are reasonable? Perhaps, there is a bug in the specification; there may be an unintended contradiction in the specification. This section describes the methods how these problems can be found.

2.1 Check for Contradictions

The question to ask is "at all times where no rules have been broken so far, is there a next state which does not break any rule?" The way to check for this depends on the model checker being used and the details of how the monitor is coded. Please contact the author for further information.

2.2 Check for certain properties

One usually wants the specification to have certain characteristics. Do the rules work together as a whole to imply desired properties? Do the micro-rules together imply the desired marco-properties? A model checker can directly check for this.

The macro properties can be written in, for example, CTL and a model checker like SMV can check whether the CTL properties hold for the specification.

Note that the specification itself is *not written* in CTL. It is written in the rule style described above. The CTL expressions are only used to verify the specification.

Here is a list of properties (CTL formulas) that I used to check our formal specification.

Go back to the main page
Site Index

kannas@stanford.edu

Last modified : February 2, 2000