Timing exception verification has become a center of interest as incorrect constraints can lead to chip failures. Proving that a false path is valid or not is a difficult problem because of the inherent computational cost, and because in practice false paths are not specified one full path at a time. Instead designers use generalized false paths, which represent a set of paths. For instance the SDC format (Synopsys Design Constraint) specifies false path exceptions using a "--from --through --to" syntax that applies on sets of pins, often using wildcards to denote these sets. This represents many (usually hundreds to thousands) actual full paths. This paper proposes a method to verify generalized false paths in a very efficient manner. It is shown to be about 10x faster than the current state-of-the-art, making false path verification an overnight task or less for multi-million gate designs.

No abstract available.

This panel focuses on how new Web-based frameworks can enable academic research and development in VLSI CAD. Open-source initiatives, portals for research communities or for the EDA community at large, algorithm benchmarking support, etc. are a few of the possibilities. Each of the three panelists will describe the current status of efforts toward building new Web-based infrastructure for CAD research. The approaches and “mission statements” illustrate the literally unbounded potential for such frameworks to transform how CAD R&D is performed.

Comprehensive study of incremental algorithms and solutions in the context of CAD tool development is an open area of research with a great deal of potential. Incremental algorithms for synthesis and layout are needed when design undergoes local or incremental change. Often these local changes are made to react to local change in the design, correct local errors or to make local improvements in one or more of the design quality metrics. In this paper we outline fundamental problems in incremental logic synthesis and physical design. Preliminary solutions to a subset of these problems are outlined.

One essential step in sequential logic synthesis consists of finding a state encoding that meets some requirements, such as optimal implementation, or correctness in the case of asynchronous FSMs. Dichotomy-based constrained encoding is more general than other constrained encoding frameworks, but it is also more difficult to solve. This paper introduces a new formalization of this problem, which leads to original exact and heuristic algorithms. Experimental results show that the resulting exact solver outperforms the previous approaches.

Graph coloring has several important applications inVLSI CAD. Since graph coloring is NP-complete, heuristics are used to approximate the optimum solution. But heuristic solutions are typically 10% off, and as much as100% off, the minimum coloring. This paper shows thatsince real-life graphs appear to be 1-perfect, one can indeed solve them exactly for a small overhead.

Gate sizing has a significant impact on the delay, power dissipation, and area of the final circuit. It consists of choosing for each node of a mapped circuit a gate implementation in the library so that a cost function is optimized under some constraints. For instance, one wants to minimize the power consumption and/or the area of a circuit under some user-defined delay constraints, or to obtain the fastest circuit within a given power budget. Although this technology-dependent optimization has been investigated for years, the proposed approaches sometimes rely on assumptions, cost models, or algorithms that make them unrealistic or impossible to apply on real-life large circuits. We discussed here a gate sizing algorithm (GS), and show how it is used to achieve constrained optimization. It can be applied on large circuits within a reasonable CPU time, e.g., minimizing the power of a 10000 gates circuit under some delay constraint in 2 h.

The set covering problem and the minimum cost assignment problem (respectively known as unate and binate covering problem) arise throughout the logic synthesis ow.This paper investigates the complexity and approximation ratio of two l o w er bound computation algorithms from both a theoretical and practical point o f view.It also presents a new pruning technique that takes advantage of the partitioning.

Gate sizing consists of choosing for each n o d e o f a mapped network a gate implementation in the library so that some cost function is optimized under some constraints.It has a signi cant impact on the delay, power dissipation, and area of the nal circuit.This paper compares ve gate sizing algorithms targeting discrete, non-linear, non-unimodal, constrained optimization.The goal is to overcome the non-linearity and nonunimodality of the delay and the power to achieve good quality results within a reasonable CPU time, e.g., handling a 10000 node network in 2 hours.We compare the ve algorithms on constraint free delay optimization and delay constrained power optimization, and show that one method is superior to the others.

Constrained encoding has several applications in the synthesis of finite state machines (FSMs), e.g., it can be used to generate asynchronous FSM state assignment that guarantees a critical hazard-free implementation, or to generate synchronous FSM state assignment with minimum PLA implementation. This paper presents ZEDICHO, an original zero-suppressed binary decision diagram (ZBDD) based algorithm that solves exactly the dichotomy-based constrained encoding problem.

Research on synthesis for low power has been done in all three stages of logic synthesis: technology independent optimization, technology mapping, and technology dependent optimization. This paper presents an integrated method, using remapping and technology dependent optimizations, to minimize the power of a mapped circuit under the given delay constraints. It produces 24% savings in power.

Integrated circuit design has principally focused on achieving performance goals (e.g., speed) with minimal cost (e.g., area) using as little design time as possible. To help designers achieve these goals computer-aided design tools have traditionally focused on tools which improve performance, reduce area, and improve productivity. In the beginning of this decade, a new design concern began to surface. Motivated by the desire to differentiate products by longer battery life, designers of integrated circuits for portable products began to be worried about the power consumption of their electronics. Moreover, as the decade progressed and smaller processing geometries appeared on the horizon, the problem of packing millions of transistors into a cost-effective plastic package emerged. Finally, product reliability added a third motivation to address the issue of power dissipation. As we approach the end of the decade, it appears that power dissipation will eclipse area as a design concern for many integrated circuits. In response to this, the electronic-design automation industry is beginning to produce products which aid in the reduction of power dissipation of integrated circuits. This paper aims to review the state-of-the-art of commercial tools for reducing power dissipation.

Covering problems occur at several steps during logic synthesis including two-level minimization and DAG c o v ering.This paper presents a better lower bound computation algorithm and two new pruning techniques that signi cantly improve the eciency of covering problem solvers.We show that these techniques reduce by u p t o three orders of magnitude the time required to solve c o vering problems exactly.

This paper presents a new 2-level logic minimization procedure. It consists of computing in an implicit way the cyclic core of the Boolean function f to be minimized. This computation is done through original transformations of sets covering problems that take full advantage of the metaproduct based implicit set of products manipulations. The computational cost of this new procedure is independent of the number of minterms of the function f and of its number of prime implicants, which allows us to treat functions for which these numbers are so large that it has never been possible to perform a 2level minimization. This method is, as far as we know, the first one that is able to produce the cyclic cores of all the functions of the MCNC benchmark. 1 Introduction The metaproduct based implicit set of products manipulation techniques introduced in [4] have made possible to compute in an implicit way the sets of prime implicants of Boolean functions for which these sets are much too lar...

A unified framework for the verification of synchronous circuits is presented. Within this framework two verification tasks, verification by actual execution and by simulation, can be automatically performed using algorithms based on the same concepts. The first idea is to manipulate sets of states and sets of transitions instead of individual states and individual transitions. The second idea is to represent these sets by Boolean functions and to replace operations on sets with operations on Boolean functions. A definition is presented of the two problems addressed and then the authors present the verification algorithms. It is shown that these algorithms use the standard set operations in addition to two specific operations called 'Pre' and 'Img'. A brief explanation is presented as to why the basic set operations are very efficiently performed when sets are denoted by the typed decision graphs of their characteristic functions. The Boolean operators 'constrain' and 'restrict', and the function 'expand' that support efficiently the 'Img' and 'Pre' operations are presented. Experimental results are presented and discussed.>

Formal verification of finite state machines (FSM) using symbolic manipulations is addressed. It is shown that the use of symbolic manipulations algorithms for the traversal of a FSM can be sublinear in the number of state and input patterns for some classes of machines. A symbolic manipulation algorithm can be directly used as a method for the transformation of a FSM which preserves the observable behavior. It is also shown that a backward traversal of a FSM can also be performed using symbolic techniques.>

The authors present the original extensions brought to PRIAM to automate both the diagnosis and the rectification of the design errors detected by this tool. PRIAM is an industrial automated formal verifier used to check the functional correctness of digital circuits of up to 20000 transistors. These extensions implement a novel approach to diagnosis based on Boolean equation solving. In particular, no enumeration of the faulty patterns is necessary to find out the incorrect gates in the circuit. The diagnosis system can handle any circuit that can be verified by PRIAM.>