We describe a new extraction tool, EMX (Electro-Magnetic eXtractor), for the analysis of RF, analog and high-speed digital circuits. EMX is a fast full-wave field solver. It incorporates two new techniques which make it significantly faster and more memory-efficient than previous solvers. First, it takes advantage of layout regularity in typical designs. Second, EMX uses a new method for computing the vector-potential component in the mixed potential integral equation. These techniques give a speed-up of more than a factor of ten, together with a corresponding reduction in memory.

Wireless transceivers for digital telecommunications are heterogeneous systems that combine digital hardware, software and analog circuitry. The pressure to miniaturization and lower power consumption for these transceivers imposes tight specifications on their analog RF parts. Many aspects of RF circuits cannot be simulated accurately and efficiently with a classical circuit-level SPICE approach. In this paper three important simulation problems for RF circuits are addressed: 1. High-level simulation of analog and RF blocks for the determination of the specifications of the circuits. 2. Accurate circuit-level simulation of nonlinear circuits with time constants that differ largely. 3. Efficient and accurate computation of phase noise in RF oscillators. For each of these problems, solutions are proposed. These solutions illustrate that accurate and efficient simulations of RF communication circuits need a heterogeneous variety of advanced algorithms.

We describe a new method for accurate large-scale capacitance calculations. The algorithm uses an integral equation formulation, but with a new representation for charge distributions that decouples charge variation from conductor geometry. This separation significantly reduces the problem size compared to a traditional discretization, resulting in a large speed increase. The full capacitance matrix of typical interconnect problems with thousands of nets can be computed in a few hours.

The main effort in oscillator phase noise calculation lies in computing a vector function called the Perturbation Projection Vector (PPV). Current techniques for PAVE calculation use time domain numerics to generate the system's monodromy matrix, followed by full or partial eigenanalysis. We present a superior method that finds the PPV using only a single linear solution of the oscillator's time- or frequency-domain steady-state Jacobian matrix. The new method is better suited for existing tools with fast harmonic balance or shooting capabilities, and also more accurate than explicit eigenanalysis. A key advantage is that it dispenses with the need to select the correct one-eigenfunction from amongst a potentially large set of choices, an issue that explicit eigencalculation based methods have to face.

In this paper, we first present an algorithm (FILL) to efficiently identify a large subset of illegal states in synchronous sequential circuits, without assuming a global reset mechanism. A second algorithm, FUNI, finds sequentially untestable faults whose detection requires some of the illegal states computed by FILL. Although based on binary decision diagrams (BDDs), FILL is able to process large circuits by using a new functional partitioning procedure. The incremental building of the set of illegal states guarantees that FILL will always obtain at least a partial solution. FUNI is a direct method that identifies untestable faults without using the exhaustive search involved in automatic test generation (ATG). Experimental results show that FUNI finds a large number of untestable faults up to several orders of magnitude faster than an ATG algorithm that targeted the faults identified by FUNI. Also, many untestable faults identified by FUNI were aborted by the test generator.

Modern IC design requires accurate analysis and modeling of chip-level interconnect, the substrate and package parasitics. Traditional approaches for such analyses are computationally expensive. In this paper we discuss some recent novel schemes for extraction and reduced order modeling that help overcome this computational bottleneck.

We describe powerful new techniques for the analysis of RF circuits. Next-generation CAD tools based on such techniques should enable RF designers to obtain a more accurate picture of how their circuits will operate. These new simulation capabilities will be essential in order to reduce the number of design iterations needed to produce complex RF ICs. 1 Introduction Design methodology and superior computer-aided design tools are key to success in the integrated circuit (IC) business. They are particularly important in the case of radio-frequency (RF) IC applications, where the digital IC divide-and-conquerdesign style, based on partitioning by functional blocks and abstraction levels, does not apply. The goal of an RF designer is to get a manufacturable design that meets the specifications with minimum cost, under severe time-to-market constraints. Unlike traditional discretecomponent RF design, prototyping is practically impossible, and the validation of a design can only be done b...

In tegral equation approaches based on layered media Green's functions are often used to extract models of integrated circuit structures. The primary advan tage of these approaches over equiv alen t-sourcebased schemes is the dramatic reduction in problem size. When combined with an SVD-accelerated sc heme for the solution of the associated dense linear system, this leads to a substantial speedup.

Integral equation based approaches are popular for extracting the capacitance of integrated circuit structures. Typically, first-order collocation or Galerkin methods are used. The resulting dense system of equations is e#ciently solved by combining matrix sparsification with an iterative solver. While the speed-up over direct factorization is substantial, the first-order methods still lead to large systems even for simple problems. In this paper we introduce a high-order Nystrom scheme. For the same level of discretization, the high-order schemes can be an order of magnitude more accurate than the first-order approaches at the same computational cost. As a consequence, we obtain the same level of accuracy with a much smaller matrix. 1 Introduction With decreasing feature sizes and increasing frequencies, accurate and e#cient capacitance extraction has become critical for design. In recent years, capacitance extractors based on integral equations [3, 7] have become popular. Integral ...

We describe the architecture for a new BDD library that is designed to be cache-friendly. The library in-corporates a novel technique for terminating searches early during nd operations together with a regroup-ing garbage collector. These features lead to a fac-tor of two improvement in speed on typical examples compared to existing libraries. 1

Integral equation techniques are often used to extract models of integrated circuit structures. This extraction involves solving a dense system of linear equations, and using direct solution methods is prohibitive for large problems. In this paper, we present IES/sup 3/ (pronounced "ice cube"), a fast Integral Equation Solver for three-dimensional problems with arbitrary kernels. Extraction methods based on IES/sup 3/ are substantially more efficient than existing multipole-based approaches.

personal or class-room use is granted without fee provided that copies are not made or distributed for profit or commercial advantage, the copyright notice, the title of the publication and its date appear, and notice is given that copying is

We describe an efficient algorithm for time-domain simulation of elements described by causal impulse responses. The computational bottleneck in the simulation of such elements is the need to compute convolutions at each time point. Hence, direct approaches for the simulation of such elements require time O(N/sup 2/), where N is the length of the simulation. We apply ideas from approximation theory to reduce this complexity to O(N log N) while maintaining double-precision accuracy. The only restriction imposed by our method is that the impulse response h(t) gets "smoother" as t goes to infinity. Essentially all physically reasonable impulse responses have this characteristic. The ideas presented can also be applied to time-domain simulation of elements described in the frequency domain, including those characterized by measured data. In this paper, we demonstrate the efficiency of the algorithm by applying it to the simulation of lossy transmission lines.

Symbolic verification based on Binary Decision Diagrams (BDDs) has proven to be a powerful technique for ensuring the correctness of digital hardware. In contrast, BDDs have not caught on as widely for software verification, partly because the data types used in software are more complicated than those used in hardware. In this work, we propose an extension of BDDs for dealing with dynamic data structures. Specifically, we focus on queues, since they are commonly used in modeling communication protocols. We introduce Queue BDDs (QBDDs) which include all the power of BDDs while also providing an efficient representation of queue contents. Experimental results show that QBDDs are well-suited for the verification of communication protocols.

We provide a new answer to the fundamental question "Why is sequential test generation so difficult?" the presence of darn (Difficult And Really Needed) states. A darn state is both difficult to reach and required to detect some faults. We introduce a method for identifying darn stares, along with a technique to measure their detrimental effect on the fault coverage. Darn states are the result of detrimental correlation between flip-flops (FFs) sharing the same clock. We propose a novel DFT technique in which FFs are partitioned into different groups having independent clocks during resting. The goal of partitioning is to increase the fault coverage by transforming darn states into easy-to-reach states. The proposed DFT has small area overhead and no performance penalty.

In this paper, we first present an algorithm (FILL) which efficiently identifies a large subset of the illegal states in a synchronous sequential circuit, without assuming a global reset mechanism. A second algorithm, FUNI, finds sequentially untestable faults whose detection requires some of the illegal states computed by FlLL. Although based on binary decision diagrams (BDDs), FILL is able to process large circuits by using a new functional partitioning procedure. The incremental building of the set of illegal states guarantees that FILL mill always obtain at least a partial solution. FUNI is a direct method that identifies untestable faults without using the exhaustive search involved in automatic test generation (ATG). Experimental results show that FUNI finds a large number of untestable faults up to several orders of magnitude faster than an ATG algorithm that targeted the faults identified by FUNI, Also, many untestable faults identified by FUNI were aborted by the test generator.

The temporal logic model checking algorithm of Clarke, Emerson, and Sistla (1986) is modified to represent state graphs using binary decision diagrams (BDD's) and partitioned transition relations. Because this representation captures some of the regularity in the state space of circuits with data path logic, we are able to verify circuits with an extremely large number of states. We demonstrate this new technique on a synchronous pipelined design with approximately 5/spl times/10/sup 120/ states. Our model checking algorithm handles full CTL with fairness constraints. Consequently, we are able to express a number of important liveness and fairness properties, which would otherwise not be expressible in CTL. We give empirical results on the performance of the algorithm applied to both synchronous and asynchronous circuits with data path logic.>

We describe a method for using abstraction to reduce the complexity of temporal-logic model checking. Using techniques similar to those involved in abstract interpretation, we construct an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a program representing a pipelined ALU circuit with over 10 1300 states.

We describe a framework for compositional verification of finite-state processes. The framework is based on two ideas: a subset of the logic CTL for which satisfaction is preserved under composition, and a preorder on structures which captures the relation between a component and a system containing the component. Satisfaction of a formula in the logic corresponds to being below a particular structure (a tableau for the formula) in the preorder. We show how to do assume-guarantee-style reasoning within this framework. Additionally, we demonstrate efficient methods for model checking in the logic and for checking the preorder in several special cases. We have implemented a system based on these methods, and we use it to give a compositional verification of a CPU controller.

Efficient algorithms for performing the matching step in technology mapping are proposed. The main result is an algorithm for matching under input negations that takes time polynomial in the size of the BDDs representing the functions to be matched. This algorithm is the basis for efficient methods for matching under permutations, bridging and constant inputs. A simple mapper based on the algorithms was implemented and tested on a suite of combinational circuits. Using the Actel type 1 mother cell, the mapper required an average of 8.5% fewer cells than mispga. When integrated into a more sophisticated technology mapper, the matching algorithms could provide even better performance.>

We describe a method for using abstraction to reduce the complexity of temporal logic model checking. The basis of this method is a way of constructing an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a pipelined ALU circuit with over 101300 states.

Article Representing circuits more efficiently in symbolic model checking Share on Authors: J. R. Burch School of Computer Science, Carnegie Mellon University School of Computer Science, Carnegie Mellon UniversityView Profile , E. M. Clarke School of Computer Science, Carnegie Mellon University School of Computer Science, Carnegie Mellon UniversityView Profile , D. E. Long School of Computer Science, Carnegie Mellon University School of Computer Science, Carnegie Mellon UniversityView Profile Authors Info & Claims DAC '91: Proceedings of the 28th ACM/IEEE Design Automation ConferenceJune 1991 Pages 403–407https://doi.org/10.1145/127601.127702Online:01 June 1991Publication History 134citation365DownloadsMetricsTotal Citations134Total Downloads365Last 12 Months6Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

The authors consider the state machine language (SML) for describing complex finite state hardware controllers. It provides many of the standard control structures found in modern programming languages. The state tables produced by the SML compiler can be used as input to a temporal logic model checker that can automatically determine whether a specification in the logic CTL is satisfied. The authors describe extensions to SML for the design of modular controllers. These extensions allow a compositional approach to model checking which can substantially reduce its complexity. To demonstrate these methods, the authors discuss the specification and verification of a simple central-processing-unit (CPU) controller.>

A parallel resolution theorem prover, called Parthenon, that handles first-order logic is described. Parthenon is apparently the first general-purpose theorem prover to be developed for a multiprocessor. The system is based on a modification of D.H.D. Warren's SRI model (Int. Symp. on Logic Prog., pp.92-101, 1987) for OR-parallelism and implements a variant of D.W. Loveland's (J. ACM, vol.15, pp.236-51, 1968) model elimination procedure. It has been evaluated on various shared memory multiprocessors, including a 16-processor Encore Multimax. The authors have found that typical theorem-proving problems exhibit a great deal of potential parallelism. Parthenon has been able to exploit much of this parallelism, producing both impressive absolute run times and near-linear speed-up curves.>

A method is described for reducing the complexity of temporal logic model checking in systems composed of many parallel processes. The goal is to check properties of the components of a system and then deduce global properties from these local properties. The main difficulty with this type of approach is that local properties are often not preserved at the global level. The authors present a general framework for using additional interface processes to model the environment for a component. These interface processes are typically much simpler than the full environment of the component. By composing a component with its interface processes and then checking properties of this composition, the authors can guarantee that these properties will be preserved at the global level. They give two example compositional systems based on the logic CTL.>