A long, long time ago, in a laboratory far, far away, EDA researchers and developers used paper tape instead of Linux, rubylith instead of GDS II, yellow wires instead of ten levels of metal. Sitting around a potbellied stove, in their rocking chairs, practitioners of that era (and this) will offer insight into why some great ideas were immediately put into practice while others stayed on the drawing board or in the ivory tower. They will share remembrances of things past, of simpler days when foundries made steel, when options meant CMOS or bipolar, when real parts were measured instead of benchmarks touted. Their stories of what it was like, what has changed, and whether the "good old days" were then or now will be followed by questions and, possibly, answers.

In the film The Lost World released in the summer of 1997, based on the 1995 Michael Crichton novel, scientists speculate about whether remote areas exist, far from human view, where dinosaurs survived and prospered, in spite of their apparent extinction and replacement by other life forms. Is the same true in design and test today? Are there places unknown to us where practices are those of a bygone era? This paper examines the evolution of design and test, and the social as well as technical factors which lead to new design practices.

Systems which synthesize logic implementations from specifications have moved, under the pressure of production requirements, from Boolean minimizers to procedures attempting to satisfy a wider range of criteria. Gate or cell count, taken as a measure of area, continues to be a major factor in design acceptability, but timing constraints, testability, wirability, and efficient use of available primitives are important as well. Additional information, such as “don't care” conditions, can be used to improve the design quality. This paper describes how these requirements are specified to and enforced by the Logic Synthesis System (LSS), a tool which has been used in production on gate array chips. Trade-offs between varying requirements, and their effect on the logic produced, are discussed and illustrated with a standard set of examples.

This correspondence concerns applications of optimization techniques based on global flow analysis to the automated design of logic. Previous optimization work on logic design has relied primarily on either local transformations on the circuit graph or on the use of two-level Boolean minimization. Our methods involve linear time algorithms which extend the scope of local optimizations to the entire design. Their use, in some cases, has resulted in a reduction in gate count, in improved control over path length, and in better detection and elimination of redundancy.

A version of the standard high level data link control protocol has been verified as an experiment with an automated verification system. This paper tries to answer questions such as: How can HDLC and its properties be represented? To what extent can they be proved? What are the main obstacles in verifying protocols like HDLC?

Despite many attempts to generate hardware implementations automatically from functional specifications, the literature does not record any commercial success. Previous efforts have dealt primarily with technology-independent primitives and have emphasized circuit minimization. However, larger scales of integration have made other design requirements and technology restrictions as important as circuit count, and have increased the cost of making an engineering change. Thus it is becoming increasingly important to insure that initial chip designs are correct. This paper outlines an investigation into the feasibility of logic synthesis in this new context. A system is described which will produce a naive implementation automatically from a functional specification, and then will interact with the designer, allowing him to evaluate it with respect to these many factors, and to improve it incrementally by applying local transformations until it is acceptable for manufacture. The use of simple local transformations will insure correct implementations, will isolate technology-specific data, and will allow the total process to be applied to larger VLSI designs. This approach has been tested on the design of a single chip with encouraging results. A prototype synthesis system is now being used to perform further experiments.

The resolution principle, an automatic inference technique, is studied as a possible decision procedure for certain classes of first-order formulas. It is shown that most previous resolution strategies do not decide satisfiability even for “simple” solvable classes. Two new resolution procedures are described and are shown to be complete (i.e. semidecision procedures) in the general case and, in addition, to be decision procedures for successively wider classes of first-order formulas. These include many previously studied solvable classes. The proofs that a complete resolution procedure will always halt (without producing the empty clause) when applied to satisfiable formulas in certain classes provide new, and in some cases more enlightening, demonstrations of the solvability of these classes. A technique for constructing a model for a formula shown satisfiable in this way is also described.

System correctness often presents itself as the problem of showing that two programs, the "specification" and the "implementation," are in some sense equivalent. Such a concept of equivalence is supplied by Milner's definition of simulation between programs. This paper presents a problem-reduction approach to proving simulation, and describes an interactive system designed for this purpose.