Skip to main content

Über dieses Buch

This book grew out of material which was taught at the International Summer School on Architecture Design and Validation Methods, held June 23-July 5, 1997, on the Island of Lipari and directed to graduate students and young researchers. Since then the course notes have been completely elaborated and extended and additional chapters have been added so that this book offers a comprehensive presentation of the state of the art which leads the reader to the forefront of the current research in the area. The chapters, each of which was written by a group of eminent special­ ists in the field, are self-contained and can be read independently of each other. They cover the wide range of theoretical and practical methods which currently used for the specification, design, validation and verification of are hardware/software architectures. Synthesis methods are the subject of the first three chapters. The chapter on Modeling and Synthesis of Behavior, Control and Data Flow focusses on techniques above the register-transfer level. The chapter on Cell-Based Logic Optimizations concentrates on methods that interface logic design with phys­ ical design, in particular on techniques for cell-library binding, the back-end of logic synthesis. The chapter on A Design Flow for Performance Planning presents new paradigms for iteration-free synthesis where global wire plans for meeting timing constraints already appear at the conceptual design stage, even before fixing the functionality of the blocks in the plan.



Modeling and Synthesis of Behavior, Control and Data Flow

To tackle the exponential growth in the complexity of digital circuits, designers are moving to higher levels of abstraction in the design process. This chapter surveys the state of the art in modeling and synthesis techniques above RTL. The chapter focuses in three areas: Behavioral Synthesis, High-Level Control, and Data Flow.
Raul Camposano, Andrew Seawright, Joseph Buck

Cell-based Logic Optimization

This chapter surveys techniques for library binding in semicustom technologies. Library binding is the back-end of logic synthesis, and constructs an interconnection of cell instances from a given library, starting from a multi-level logic network. Emphasis is placed on the algorithmic approach to library binding, with particular reference to covering and matching techniques.
Giovanni De Micheli

A Design Flow for Performance Planning: New Paradigms for Iteration Free Synthesis

In conventional design, higher levels of synthesis produce a netlist, from which layout synthesis builds a mask specification for manufacturing. Timing analysis is built into a feedback loop to detect timing violations which are then used to update specifications to synthesis. Such iteration is undesirable, and for very high performance designs, infeasible. The problem is likely to become much worse with future generations of technology. To achieve a non-iterative design flow, early synthesis stages should use wire planning to distribute delays over the functional elements and interconnect, and layout synthesis should use its degrees of freedom to realize those delays.
Ralph H. J. M. Otten

Test and Testable Design

Defects may occur during the fabrication process and during the lifetime of integrated circuits. Integrating a faulty device into systems will result in expensive repairs or even in unsafe situations and should be avoided by testing the chips
This section explains defect mechanisms and their consequences for the product quality. Methods for test pattern generation are discussed, and it is shown how these methods can already be supported in the design phase. Modern systems-on-chip often have the capabilities of testing themselves, and recent built-in self-test techniques (BIST) are presented.
Hans-Joachim Wunderlich

Machine Assisted Verification

An introduction to a number of fully mechanized methods of formal hardware verification is given. Decision-diagram based procedures for the verification of combinational circuits at the gate- and word-level are surveyed. Fixed-point calculation techniques for equivalence and property verification of sequential machines are studied. The verification of processor architectures at the instruction-set and algorithmic register-transfer level is discussed. A method of formally correct synthesis of pipelined architectures is presented.
Hans Eveking

Models of Computation for System Design

In the near future, most objects of common use will contain electronics to augment their functionality, performance, and safety. Hence, time-to-market, safety, low-cost, and reliability will have to be addressed by any system design methodology. A fundamental aspect of system design is the specification process. We advocate using an unambiguous formalism to represent design specifications and design choices. This facilitates tremendously efficiency of specification, formal verification, and correct design refinement, optimization, and implementation. This formalism is often called model of computation. There are several models of computation that have been used, but there is a lack of consensus among researchers and practitioners on the “right” models to use. To the best of our knowledge, there has also been little effort in trying to compare rigorously these models of computation. In this paper, we review current models of computation and compare them within a framework that has been recently proposed. This analysis demonstrates both the need for heterogeneity to capture the richness of the application domains, and the need for unification for optimization and verification purposes. We describe in detail our CFSM model of computation, illustrating its suitability for design of reactive embedded systems and we conclude with some general considerations about the use of models of computations in future design systems.
Luciano Lavagno, Alberto Sangiovanni-Vincentelli, Ellen M. Sentovich

Modular Design for the Java Virtual Machine Architecture

We provide a modular high-level definition of the Java Virtual Machine (JVM) architecture. We decompose the machine into three components — the loader, the bytecode verifier and the interpreter — each for a hierarchy of four stepwise refined JVM program layers. These layers naturally correspond to the structuring of Java into sub languages with imperative, procedural, object-oriented and exception handling features. We give our definitions in terms of Abstract State Machines, which have a simple but precise semantic foundation. As a consequence our JVM models can be verified and validated by machine supported mathematical analysis and standard simulation techniques. Furthermore, due to their abstract nature, the models can serve as a platform independent basis for the evaluation and comparison of different JVM implementations.
Egon Börger, Wolfram Schulte
Weitere Informationen