The speed-independent circuits of the title are circuits without clocks that satisfy specifications without assumptions about the relative speed of components. Some general claims are made (on the back cover) that such circuits “have gained renewed interest in the VLSI community” and can “expedite circuit design.” No significant evidence in support of these claims is given. In addition to its possible value for VLSI design, this work will interest researchers in formal models of concurrency.
This monograph is Dill’s 1988 PhD dissertation, written under Edmund Clark at CMU. The research falls into two parts, depending on the power of the specification language. For safety properties, Dill defines the notion of a prefix-closed trace structure, and for liveness properties, he defines the notion of a complete trace structure. In the safety case, the specification is based on prefix-closed sets of finite traces, with each trace representing a partial execution of the system. Finite automata are used as a crucial tool in representing sets of traces. The verification problem for safety properties is feasibly computable, and Dill has implemented an automated verifier. He discovered an error in a previously published circuit design using the automated verifier. He discusses the limitations of verifying safety properties: for instance, the trivial circuit (which can be “manufactured out of wood”) satisfies all safety specifications.
To handle liveness assertions, complete trace structures are based on infinite traces. The theory of specification and verification using complete trace structures is developed in analogy to the prefix-closed theory. Büchi automata take the place of finite automata in the representation of sets of traces. The verification problem is not automated because of computational difficulties, but prospects for future progress are suggested.
One of the interesting differences between the two theories is the modeling of receptiveness, which is the requirement that trace structures cannot constrain circuit input values. In the prefix-closed theory, where traces represent partial executions, receptiveness is easily handled by requiring that whenever a trace is extended by an input event, the result is again a trace. In the complete trace theory, partial executions are not directly represented. Receptiveness is modeled by considering infinite two-player games between the circuit and the environment, which specifies input events. The receptiveness requirement states that the circuit must have a strategy that generates a valid trace when played against any sequence of input events. This requirement adds substantial complexity to the verification problem. Dill proves a new result on the decidability of the existence of winning strategies in order to establish the decidability of the verification problem for complete trace structures.
Circuit algebras are a central theme of Dill’s approach. In chapter 2, circuit algebras are defined using operations and axioms. The elements of a circuit algebra are called circuits, and every circuit contains a finite set of wires, with some wires designated as inputs and others designated as outputs. Three operations are defined. The composition operation combines two circuits that have disjoint output wires, forming a new circuit in which wires with the same name are identified. The rename operation renames wires in a circuit. The hide operation changes output wires to internal (neither input nor output) wires. The free circuit algebras are constructed explicitly and are named circuit structures. The generators in a free circuit algebra are called basic circuits; they normally represent AND-gates and the like.
Chapter 3 covers the prefix-closed trace structures and proves that they form a circuit algebra. Chapter 4 describes the approach to specification. A trace structure T1 is said to implement T2 if T1 can safely be substituted for T2 in all environments. Chapter 5 discusses the automatic verifier and the error it discovered in an existing design. Chapter 6 provides background on Büchi automata, infinite games, and the new result on decidability in games. Chapter 7 provides the results on complete trace structures. Chapter 8 provides conclusions and future prospects.
The book is well written, with few typographical errors, numerous references, and sufficient motivation for definitions and detail in mathematical arguments. The introduction provides a good survey of related work in circuit verification and synthesis and in models of concurrency. The disappointment in this work, if any, comes from the fact that only simple specifications can be handled in an automated way.
One interesting technical issue that the book does not raise is whether the receptiveness problem for complete trace structures can be resolved more simply. One possibility is to consider a structure that maintains both partial and complete traces, with each complete trace a limit of partial traces. It might be sufficient to require receptiveness for just the finite traces. The idea of maintaining both types of traces has been used in concurrency theory.
