Skip navigation

In previous posts, I have tried to illustrate that writing complete, unambiguous specifications is hard, if not impossible. A solution that is proposed often, but never seems to take hold, is to write “executable” specifications. That is, rather than writing text-based specifications, write code that tools can then use to automate the process of producing the design. Today, specification is still done the same way it was twenty years ago, using (electronic) paper and pencil. Why is this? Why do we continue to write text-based specifications despite dramatic increases in complexity and the obvious need for more automation?

I gained some insight into this problem from research carried out by Kanna Shimizu, my colleague at Stanford. In bus protocols such as PCI, the protocol rules are spelled out in the spec. The traditional way of verifying PCI would be to design a PCI controller first, then verify that all the properties held for that controller. Kanna’s idea was to code the protocol rules into simple propositions that could be formally verified for consistency.  The advantage of this method is that you did not need a design in order to simply verify that the protocol itself had no problems. The types of errors that could be detected were things like conflicts between rules where, by one rule, a signal was supposed to be asserted at some time, while by another one, it was supposed to be deasserted. Suprisingly, a number of such inconsistencies were found in the PCI protocol using this approach.

When I first heard this result, my reaction was that it did not seem right. If there were that many bugs in the PCI protocol, it would not be possible to design any working hardware, yet PCI was a widely using protocol and there was no evidence that these inconsistencies had caused problems.

I didn’t think much about this until Kanna came to me one day with a case she had discovered while working on an Intel processor bus protocol, which happened to be the same one used on the HAL MCU design that I had worked on and, therefore, was familiar with. She had discovered a case where a bus agent could hang the bus forever under certain conditions. I was certain this could not happen, but after analyzing it, found that the protocol did indeed allow such a thing to happen. Again there was a disconnect between what I knew about the protocol and what the spec. actually was saying.

I didn’t think much about it until much later when I realized what the problem was. You would have to go out of your way to design an agent to do this. In fact, it would have to be malicious. Even though the spec. had holes, there is the intent to build a bus that communicates data. This intent was missing from the set of properties being verified. The intent is actually written in the spec., but not in a way that is easy to translate to code. It says, simply, “It’s a bus with the following rules.” The rules were what Kanna verified. While it was easy to code the rules into properties that could automatically verified, coding the requirement “it’s a bus” is consderably more difficult. That one sentence corresponds to potentially thousands of lines of code.

When claims are made about executable specs being better in some: either being more concise, easier to write, less ambiguous, proponents usually point to these easy to code protocol rules, while neglecting the difficulty of translating inherently concise specifications like “it’s a bus”. I believe this is one of the main reasons that executable specifications have not caught on as a better way of specifying complex designs. This will continue into the future, specifications will continue to be text-based because there is no solution on the horizon to this problem.


One Comment

  1. I agree that specifications will be written in human-readable language for a long time to come; probably not forever, but likely into the next century. This does not mean, however, that those specifications cannot be executed. I believe it is possible to write specifications in a human-readable manner that are also executable. Some form of pseudo-code. The specs are simply written as the logic (behavior) rules that they represent. IF-THEN-ELSE. Then a compiler is used to generate tests from these rules. If the specs are written as a compilation of IF-THEN-ELSE rules, then we have the makings of an executable specification.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: