Verification of SoC Designs with Integrated Analog/Mixed-Signal Components

Background, Motivation, and Goals

Most modern SoC designs contain analog and mixed signal (AMS) elements integrated with digital components. AMS elements currently consume about 40% of the design effort, and an estimated 50% of errors in recent chips that require a redesign are due to bugs in the AMS portion of the design. Analysis of AMS elements is thus a crucial component of in the verification of an SoC design. The key problem in the applicability of formal analysis to AMS verification arises from the need to handle continuous quantities. Note that unlike digital artifacts, AMS elements are characterized in terms of continuous time, as they deal with factors like voltage level, signal noise, and current leakage. On the other hand, formal methods are typically applied to models based on discrete events, which can be effectively described as state machines. Thus, while the capacity of verification of digital designs has increased dramatically over the last decade, AMS verification has remained largely the same, with the designers relying on simulation traces to validate specific properties of a circuit. The current bottlenecks in applying formal analysis for industrial AMS elements are summarized in the Needs Document of the Semiconductor Research Corporation as follows. “In the past, analog verification has taken one of two well-understood tracks — (a) using detailed differential equations from solid state physics or (b) very high level abstract modeling of analog elements. The latter has found limited use in the industry, the former is hard to use in industrial design practice.”

Our approach to solve this issue is to develop behavioral abstractions, which permit formalization of circuit behavior as an interactive composition of state machines. The approach is motivated by the observation that the AMS elements used in an SoC block are designed not as an ad-hoc transistor network but by interconnecting small, cohesive, logical units each designed to operate over a limited set of operating conditions. The transitions and timing constraints of the unit within the operating conditions are well-understood and validated by extensive analog SPICE simulation. The behavior of each unit under the operating constraints can be formalized as a parameterized state machine, using guarded transitions to encode its operating constraints; the state machine can be viewed as providing a logical semantics of the transitions of the unit. The behavior of an entire AMS element is modeled as an interacting composition of the individual state machines. Note that focusing on the behavior of a unit within the operating constraints enables us to circumvent the complex problem of abstracting inherently continuous quantities with a discrete algebra. Finally, the specification is extracted from the interface used to black-box the circuit during functional verification of its surrounding SoC block, and the verification problem is to show that the behavioral model is a refinement of this specification.

We have successfully used behavioral abstractions to reason about flash memory designs. Flash memory designs make use of analog characteristics of special “floating-gate” and “split-gate” transistors which cannot be handled by traditional memory verification techniques. Our approach has been applied to a number of industrial flash designs involving both floating-gate and split-gate technologies. We are currently applying the same approach to verify other AMS components such as phase-locked loops.

Funding, Personnel, and Organizations

The research has been funded by the Semiconductor Research Corporation under Grant 08-TJ-1849, and by the Defense Advanced Research Projects Agency and the National Science Foundation under Grant CNS-0429591.[1] We closely collaborate with the industry (e.g., researchers from Freescale Semiconductor Inc. and Advanced Micro Devices Inc.), to ensure that our formalization and reasoning tools meet the industry needs.

Here are the people who have been involved in this research so far in various capacities.

We're looking for more help, so if you're interested in the work feel free to talk to us.

Publications

The publications below are posted roughly in reverse chronological order. The FMCAD 2007 paper presents our initial thinking of the problem, and discusses how the approach can handle custom memories in general, including both SRAM and flash memories. The flash formalization presented in this paper is a basic NOR configuration. The exposition in the NVMTS 2008 paper is targeted primarily at flash memory designers. It presents the verification problem for flash memories to this audience, and includes a formalization of a NAND flash in addition to the NOR configuration. Both papers are superceded by the ISQED 2010 paper which discusses the general techniques and presents the application of the approach to industrial flash memory implementations.

[1] Any opinions, findings and conclusions or recomendations expressed in this material are those of the authors and do not necessarily reflect the views of the Defense Advanced Research Projects Agency, the National Science Foundation, or the Semiconductor Research Corporation.