This paper applies interval-arithmetic based verification algorithms to circuit verification problems. In particular, we use Krawczyk's operator to find all DC operating points of CMOS circuits. We present what we believe to be the first, completely automatic verification of the Rambus ring-oscillator start-up problem. Comparisons with the dReal and Z3 SMT shows large performance and scalability advantages to the interval verification approach. We provide an open-source implementation that supports state-of-the-art short-channel device models.

The complementary strengths of interactive theorem proving and SMT solvers have motivated several efforts at integration including Sledgehammer for Isabelle/HOL, CoqSMT. The goal of these efforts is to combine the generality of interactive theorem provers, especially support for inductive proofs, with the automation of SMT solvers for discharging tedious subgoals. In practice, such efforts have been hindered by the gaps between the logic of the theorem prover and the SMT solver. Typically, goals in the theorem prover are expressed in an untyped logic, making often making extensive use of recursive functions and quantifiers. In contrast, the logic of SMT solvers is first-order, many-sorted, and lacks recursive functions. In practice, the effort to transform proof goals into formulations that are amenable to SMT techniques can dominate the proof effort. This tutorial describes Smtlink, our integration of Z3 into ACL2, and presents examples demonstrating the effectiveness of the approach. Smtlink makes extensive use of reflection. By inspecting proof goals and extracting already proven facts, Smtlink automates much of the translation of goals from the untyped logic of ACL2 to the many-sorted logic of Z3. From the users perspective, Smtlink can discharge goals that include user-defined data types, recursive functions, and whose proofs build on previously established theorems. We present several examples from analog and mixed-signal circuits. We also present a simple proof of the Cauchy-Schwartz inequality. In our experience, these proofs were surprisingly straightforward: we identified the obvious, inductive lemmas, and these lemmas were discharged without further effort by the user. As we will show with these examples, the SMT integration makes the theorem proving process productive and fun.This tutorial is based on joint work with Carl Kwan and Yan Peng.

A response property is a simple liveness property that, given state predicates p and q, asserts "whenever a p-state is visited, a g-state will be visited in the future". This paper presents an efficient and scalable implementation for explicit-state model of checking response properties on systems with strongly- and weakly-fair actions, using a network of machines. Our approach is a novel twist on the One-Way-Catch-Them-Young (OWCTY) algorithm. Although OWCTY has a worst-case time complexity of O(n2m) where n is the number of states of the model, and m is the number of fair actions, we show that in practice, the run-time is a very small multiple of n. This allows our approach to handle large models with a large number of fairness constraints. Our implementation builds upon PREACH, a distributed, explicit-state model checking tool. We demonstrate the effectiveness of our approach by applying it to several standard benchmarks on some real-world, proprietary, architectural models.

The performance of today's computers is limited primarily by power consumption rather than the number of instructions executed. Because the energy required to perform an operation using VLSI circuits drops rapidly with the time allowed for the operation, many slow processors can complete a parallel computation using less time and less energy than a fast uniprocessor that can execute the best sequential algorithm. This motivates designing algorithms for minimum execution time subject to energy constraints. We propose a simple model for analyzing algorithms that reflects the energy-time trade-offs of CMOS circuits. Using this model, we derive lower bounds for the energy-constrained execution time of sorting, addition, and multiplication, each with bitwise inputs, and we present algorithms that meet these bounds. These lower bounds are based on the energy-time costs of communication distance, rather than bisectional bandwidth arguments typical of area-time lower bounds. We show that minimizing time under energy constraints is not the same as minimizing operation count or computation depth. This work establishes a tractable method for the evaluation of parallel computations in a power-constrained environment.

For a given algorithm, the energy consumed in executing the algorithm has a nonlinear relationship with performance. In case of parallel algorithms, energy use and performance are functions of the structure of the algorithm. We define the asymptotic energy complexity of algorithms which models the minimum energy required to execute a parallel algorithm for a given execution time as a function of input size. Our methodology provides us with a way of comparing the orders of (minimal) energy required for different algorithms and can be used to define energy complexity classes of parallel algorithms.

FPGA user clocks are slow enough that only a fraction of the interconnect's bandwidth is actually used. There may be an opportunity to use throughput-oriented interconnect to decrease routing congestion and wire area using on-chip serial signaling, especially for datapath designs which operate on words instead of bits. To do so, these links must operate reliably at very high bit rates. We compare wave pipelining and surfing source-synchronous schemes in the presence of power supply and crosstalk noise. In particular, supply noise is a critical modeling challenge; better models are needed for FPGA power grids. Our results show that wave pipelining can operate at rates as high as 5Gbps for short links, but it is very sensitive to noise in longer links and must run much slower to be reliable. In contrast, surfing achieves a stable operating bit rate of 3Gbps and is relatively insensitive to noise.

Systems-on-chip designs often use functional blocks operating at different clock frequencies. This motivates the use of an asynchronous network-on-chip (NoC) with synchronizing FIFOs interfacing between the NoC and the functional blocks. To minimize design time, these FIFOs should be constructed from cells available in a standard cell library and configurable to work in a wide range of applications. We present a modular synchronizing FIFO design that can be implemented using logic gates from a typical standard-cell library. The FIFO has interchangeable input and output interfaces for edge-triggered synchronous communication and for two asynchronous handshake protocols: asP* and LEDR. The FIFO capacity, synchronizer latency and interface protocols are independent parameters, allowing the FIFO to be easily configured for different NoC requirements. We evaluate performance using post-layout simulation results and analyze the metastability induced failure rate for synchronization latencies from half a clock cycle up to three clock cycles.

Wave pipelining has gained attention for NoC interconnect by its promise of high bandwidth using simple circuits. Reliability issues must be addressed before wave pipelining can be used in practice; so, we develop a statistical model of dynamic timing uncertainty. We show that it is important to distinguish between static and dynamic sources of timing uncertainty, because source-synchronous wave pipelining is much more sensitive to the latter. We use HSPICE simulations to develop a model for a wave pipelined link in a 65 nm CMOS process and apply a statistical approach to determine the achievable throughput at acceptable bit-error rates. Reliability estimates show that a modest amount of dynamic noise can cut achievable throughput in half for a ten-stage wave-pipelined link, and will further degrade longer links. After accounting for noise, traditional globally synchronous design is shown to offer higher throughput than the wave-pipelined design.

As VLSI fabrication technology progresses to 65 nm feature sizes and smaller, transistors no longer operate as ideal switches. This motivates the verification of digital circuits using continuous models. Recently, we showed how such verification can be performed using projection based methods.However, the verification was slow, requiring nearly four CPU days to verify a nine-transistor toggle flip-flop. Here, we describe improvements to the reachability algorithms and optimizations of the software architecture. These produce a 15 x reduction in computation time and significant reductions in the overapproximation errors. With these changes, the same toggle flip-flop can be verified in a few hours, making formal verification a viable alternative to circuit simulation.

This paper presents the verification of an asynchronous arbiter modeled at the circuit level with non-linear ordinary differential equations. We use Brockett's annulus to represent the allowed families of continuous waveforms for input and output signals and show that the metastability filter of the arbiter can be understood as a "Brockett annulus transformer." Improvements to the Coho verification tool are described that reduce the over approximation errors when working with non- convex reachable regions. The verification shows that the arbiter observes a four-phase handshake protocol with its clients and maintains mutual exclusion. We also show several liveness properties including bounded time response to uncontested requests and that grants are issued fairly.

Recently, researchers at Rambus proposed a ring-oscillator example as a challenge problem for analog verification: they asked researchers to identify conditions that will ensure that the oscillator is free from lock-up. We present a solution to this challenge problem. Our approach is primarily pencil-and-paper analysis. We prove properties of the oscillator circuit, and then use numerical computation to determine parameter values for which correct operation is guaranteed. In addition to answering the challenge question, our approach uncovered anomalous behaviors that could cause the circuit to fail to oscillate but that would be hard to detect by standard, simulation-based, design practices.

Power consumption has become one of the most critical concerns for processor design. This motivates designing algorithms for minimum execution time subject to energy constraints. We propose simple models for analysing algorithms that reflect the energy-time trade-offs of CMOS circuits. Using these models, we derive lower bounds for the energy-constrained execution time of sorting, addition and multiplication, and we present algorithms that meet these bounds. We show that minimizing time under energy constraints is not the same as minimizing operation count or computation depth.

We show that the problem of finding an energy minimal schedule for execution of a collection of jobs on a multiprocessor with job migration allowed has polynomial complexity. Each job is specified by a release time, a deadline, and an amount of work to be performed. All of the processors have the same, convex power-speed trade-off of the form P = phi(s), where P is power, s is speed, and phi is convex. Unlike previous work on multiprocessor scheduling, we place no restriction on the release times, deadlines, or amount of work to be done. We show that the scheduling problem is convex, and give an algorithm based on linear programming. We show that the optimal schedule is the same for any convex power-speed trade-off function.

The implementation of interconnect is becoming a significant challenge in modern integrated circuit (IC) design. Both synchronous and asynchronous strategies have been suggested to manage this problem. Creating a low skew clock tree for synchronous inter-block pipeline stages is a significant challenge. Asynchronous interconnect does not require a global clock, and therefore, it has a potential advantage in terms of design effort. This paper presents an asynchronous interconnect design that can be implemented using a standard application-specific IC flow. This design is considered across a range of IC interconnect scenarios. The results demonstrate that there is a region of the design space where the implementation provides an advantage over a synchronous interconnect by removing the need for clocked inter-block pipeline stages, while maintaining high throughput. Further results demonstrate a computer-aided design tool enhancement that would significantly increase this space. A detailed comparison of power, area, and latency of the two strategies is also provided for a range of IC scenarios.

Circuits such as flip-flops, sense amplifiers and synchronizers can exhibit metastability failures that are undetectable given the numerical accuracy limitations of simulators such as HSPICE. We present a novel simulation technique that allows us to generate accurate waveforms for the metastability failures and similar events. We apply our method to two latches and a self-resetting circuit for clock-phase generation.

As VLSI fabrication technology progresses to 65nm feature sizes and smaller, transistors no longer operate as ideal switches. This motivates verifying digital circuits using continuous models. This paper presents the verification of the high-speed, toggle flip-flop proposed by Yuan and Svensson [1]. Our approach builds on the projection based methods originally proposed by Greenstreet and Mitchell [2], [3]. While they were only able to demonstrate their approach with two- and threedimensional systems, we apply projection based analysis to a seven-dimensional model for the flip-flop. We believe that this is the largest verification to date of a digital circuit using non-linear circuit-level models. In this paper, we describe how we overcame problems of numerical errors and instability associated with the original projection based methods. In particular, we present a novel linear-program solver and new methods for constructing accurate linear approximations of non-linear dynamics. We use the toggle flip-flop as an example and consider how these methods could be extended to verify a standard cell library for digital design.

Over the past ten years, as integrated circuits became increasingly more complex and expensive, the industry began to embrace new design and reuse methodologies that are collectively referred to as system-on-chip (SoC) design. In this paper, we focus on the reuse and integration issues encountered in this paradigm shift. The reusable components, called intellectual property (IP) blocks or cores, are typically synthesizable register-transfer level (RTL) designs (often called soft cores) or layout level designs (often called hard cores). The concept of reuse can be carried out at the block, platform, or chip levels, and involves making the IP sufficiently general, configurable, or programmable, for use in a wide range of applications. The IP integration issues include connecting the computational units to the communication medium, which is moving from ad hoc bus-based approaches toward structured network-on-chip (NoC) architectures. Design-for-test methodologies are also described, along with verification issues that must be addressed when integrating reusable components.

We present a novel method for jointly optimizing FIR filters for pre-equalization, decision feedback equalization, and near-end crosstalk cancellation. The unified optimization problem is a linear program, and we describe sparse matrix techniques for its efficient solution. We illustrate our approach with uni- and bi-directional buses using differential signaling in both intra-board and cross-backplane scenarios.

We consider the problem of noise margin analysis for dynamic logic circuits. Because such circuits operate in multiple phases, their noise immunity is also time varying. We formulate noise margin analysis as a non-linear optimization problem where we find the smallest disturbance waveform that results in a qualitative change in the behavior of the circuit. We present a practical method for solving these optimization problems based on deriving a sensitivity matrix for the small-signal response of the circuit. We use our approach to compare the robustness of static CMOS gates, self-resetting domino, and output prediction logic.

The implementation of interconnect is becoming a significant challenge in modern IC design. Both synchronous and asynchronous strategies have been suggested to manage this problem. Creating a low skew clock tree for synchronous inter-block pipeline stages is a significant challenge. Asynchronous interconnect does not require a global clock, and therefore, it has a potential advantage in terms of design effort. This paper presents an asynchronous interconnect design that can be implemented using a standard ASIC flow. This design is considered in the context of a simple interconnect network. The results demonstrate that there is a region of the design space where the implementation provides an advantage over a synchronous interconnect. A detailed comparison of power, area and latency of the two strategies is also provided for a range of IC scenarios.

Research in high-speed interconnect requires physical test to validate circuit models and design assumptions. At multi-Gbit/sec rates, physical implementations require custom circuit design, teams with many designers, long design cycles, and expensive test equipment. By building a "scale model" that operates at bit rates of 50-100 Mbits/sec, we obtain order of magnitude reductions in cost and design time. We present a simple, inexpensive test bed implemented using a PC and inexpensive graphics cards. To demonstrate the effectiveness of our test bed, we use it to validate novel methods for synthesizing crosstalk equalization filters.

We present practical algorithms for the synthesis of crosstalk cancelling equalizing filters. We examine designs optimized for the traditional l2 metric and introduce an approach based on the l∞ metric. We compare the two approaches for realistic buses with tight wire spacings. We show bandwidth improvements of up to a factor of 2 using crosstalk cancellation when compared with no filtering or independent pre-emphasis for each wire. Using l∞ optimization, we achieve roughly 50% better performance than the l2 methods. We are aware of only one other published description of crosstalk cancellation for high-performance buses [9]. We believe that our work is the first to show the advantages of l∞ optimization and to consider crosstalk cancellation for more than just nearest neighbours for high-speed buses.

In recent years, formal methods have emerged as an alternative approach to ensuring the quality and correctness of hardware designs, overcoming some of the limitations of traditional validation techniques such as simulation and testing. There are two main aspects to the application of formal methods in a design process: the formal framework used to specify desired properties of a design and the verification techniques and tools used to reason about the relationship between a specification and a corresponding implementation. We survey a variety of frameworks and techniques proposed in the literature and applied to actual designs. The specification frameworks we describe include temporal logics, predicate logic, abstraction and refinement, as well as containment between ω-regular languages. The verification techniques presented include model checking, automata-theoretic techniques, automated theorem proving, and approaches that integrate the above methods. In order to provide insight into the scope and limitations of currently available techniques, we present a selection of case studies where formal methods were applied to industrial-scale designs, such as microprocessors, floating-point hardware, protocols, memory subsystems, and communications hardware.

STARI is a high-speed signaling technique that uses both synchronous and self-timed circuits. To demonstrate STARI, a chip has been fabricated using the MOSIS 2/spl mu/ CMOS process. In a simple test fixture, it operates at data rates of 120 Mbits/sec over a pair of wires. Because STARl uses both synchronous and self-timed circuits, it provides an opportunity to compare these two design methods. The synchronous circuits of the STARI chip achieve rates of operation two to three times those of the self-timed circuits. However, the self-timed FIFO in the receiver provides robust compensation for clock skew that could not be achieved with synchronous circuitry alone. Thus, the STARI chip demonstrates advantages of combining these two design techniques.

Given two models of a circuit, Q and Q', we say that Q' as a refinement of Q if every possible behavior of Q' is allowed by Q. We present a unified framework for verifying refinement using both model-checking and symbolic trajectory evaluation techniques. In this framework, the refinement conditions are derived and verified automatically. To demonstrate this approach, we present a design for a synchronizer circuit used in a high-speed synchronous design.>