No abstract available.

Various formal verification techniques and how they can be applied to sequential hardware, especially at the register-transfer level, are examined. The basic elements of a verification system, as illustrated on the relatively simple problem of verifying combinational circuits, are presented. The more complex problems involved in analyzing sequential systems and the techniques that have been developed to solve them are then considered. Throughout, the focus is on those techniques whose utility has been demonstrated on real systems, including higher order logic, temporal logic, predicate transformers, state-machine models, and model checkers.>

CPA (conditions, precedence relations and assertions), a framework for specifying the behavior of control-oriented digital systems, is described. CPA allows the expression of sequential behavior, data transformations and timing constraints in an integrated representation. It supports the abstract, declarative specification of behavior independent of any particular implementation. Thus it is especially useful for verifying a design against a set of externally-defined requirements.>

High-level synthesis systems start with an abstract behavioral specification of a digital system and find a register-transfer level structure that realizes the given behavior. The various tasks involved in developing a register-transfer level structure from an algorithmic level specification are described. In particular, it is shown how the high-level synthesis task can be decomposed into a number of distinct but not independent subtasks. The techniques that have been developed for solving those subtasks are presented. Areas related to high-level synthesis that are still open problems are examined.>

A novel method for using bottom-up design information in the synthesis of integrated circuits from abstract behavioral description is reported. There are two important ways in which this method differs from traditional top-down synthesis techniques. First, it draws on a newly developed procedural database to collect detailed information on the physical and logical properties of the primitives available for building the design. Second, it partitions each design it considers into clusters that have physical as well as logical significance. This method for representing and organizing knowledge about candidate designs makes it possible to estimate physical placement and wiring, even at the abstract register-transfer (RT) level. This allows a more accurate evaluation of RT designs without doing a full logic-level or transistor-level layout. Partitioning also leads to a simple method for systematically exploring the space of possible designs to find the one that best meets the designer's objectives and constraints.>

No abstract available.

A method for producing a chip floor plan from a list of blocks and their interconnections is presented. The blocks can be of different sizes, and each block can have several possible aspect ratios. The algorithm places the blocks and chooses the orientation and aspect ratio of each to produce a near-minimum area floor plan. The preliminary placement of the blocks is done using a standard min-cut placement algorithm, modified so that it can handle blocks of different sizes. The choice of aspect ratio and orientation is done using a dynamic programming algorithm, along with a heuristic that limits the number of possible configurations explored. The algorithm is shown to give near-optimal results, yet it is faster than comparable placement algorithms, fast enough to be used in the inner loop of a program that generates and evaluates many alternative designs for a given high-level behavioral specification.>

This paper reports on a new method for using bottom-up design information in the synthesis of integrated circuits from abstract behavioral descriptions. There are two important ways in which this method differs from traditional top-down synthesis techniques. First, it draws on a newly developed procedural database to collect detailed information on the physical and logical properties of the primitives available for building the design. Second, it uses a different method for representing and organizing knowledge about a design that makes possible estimates of physical placement and wiring in the analysis of that design, even at the abstract register-transfer level. This allows a more accurate evaluation of candidate register-transfer designs without doing a full logic-level or transistor-level layout. It also leads to a simple method for systematically exploring the space of possible designs in order to find the one that best meets the designer's objectives and constraints.

As part of our research on the Carnegie-Mellon University Design Automation System, we have been investigating methods for proving that the system produces correct designs from correct specifications. We have developed a mathematical model for the behavior of hardware descriptions, which we have used to prove that some of the optimizing transformations used in the design system preserve behavioral equivalence. The model, which is based on regular expressions modified by predicates to show data dependence, goes beyond the usual computational models used in program verification, in that it takes into account the proper sequencing of those "events" which represent interactions with the environment. This paper presents the model, shows how it can be used to represent the behavior of descriptions in an ISP-like hardware description language, and gives an example proof of a transformation.