Formal verification technology has advanced significantly in recent years, yet it seems to have no noticeable acceptance as a mainstream verification methodology within the industry. This paper discusses the issues involved with deploying formal verification on a production mode, and the strategies that may need to be adopted to make this deployment successful. It analyses the real benefits and risks of using formal verification in the overall verification process, and how to integrate this new technology with traditional technologies like simulation. The lessons described in this paper have been learnt from several years of experience with using commercial formal verification tools in industrial projects.

For multimedia SOCs supporting real time, high throughput and data intensive applications, performance validation of memory subsystems is needed to uncover the bottlenecks in the RTL implementation. Traditional validation techniques are either too slow, non-exhaustive (like performance simulations or running pseudo applications on FPGA platforms), or are not accurate enough to guarantee conformance (like abstract interpretation and analysis). In this paper we present an approach for performance validation which uses (a) semi-formal techniques rather than pure simulation for providing a wider coverage, (b) actual RTL implementations wherever available for more accurate analysis, and (c) sequential equivalence checking for validating the abstract models for IP's whose RTL is either not present or from which datapath has been abstracted out. We illustrate this approach using two case studies from video signal processing platforms. In the first study, performance Issues found in silicon were detected using the proposed approach, and in the second study a number of performance bottlenecks were detected much before the RTL was frozen.

Architectural decisions for DSP modules are often analyzed using high level C models. Such high-level explorations allow early examination of the algorithms and the architectural trade-offs that must be made for a practical implementation. The same models can be reused during the verification of the RTL subsequently developed, provided that various "hooks " which are desirable during the verification process are considered while creating these high level models. In addition, consideration must be given to the qualitative content of these high level models to permit an optimal verification flow allowing for compromise between features of the model and the completeness of the verification. Thus, high quality design and verification are achieved by the use of valid models and the valid use of models. In this paper, we describe our approach and show examples from a typical image processing application.

Robust verification of protocol conversion and arbitration schemes of SoC bridges forms a significant component of the overall SoC verification. Formal verification provides a way to achieve this, but a naive approach often leads to explosion of the state space, and is impractical for most of today's protocols and bridges. This problem is further complicated in the presence of serial protocols, where control and data are mixed together and transactions continue for very great depths. White-box verification is not a feasible solution, since these bridges are often imported or generated from other sources, and internal information is not readily available. In this paper, we propose a black-box and hybrid approach to this problem, by judiciously mixing simulation and formal verification. We illustrate our approach by applying it to two dual stage bridges that perform serial to parallel protocol conversion and vice versa.

This paper presents the knowledge representation schemes adopted in MICKEY, a knowledge based system for designing microprocessor based systems. MICKEY is essentially a hybrid expert system, using rules and procedures for achieving the different design tasks. We briefly describe the hierarchy of tasks in this problem domain, and emphasize on the refinement paradigm, constraint propagation, conflict resolution and task management strategies adopted in MICKEY. Next, we dwell upon the different knowledge sources and their functions, with respect to the particular design domain. Finally, we present an industrial design, achieved by MICKEY, to demonstrate its applicability.

In CAD systems, it is often required to implement desired behaviors by some available device. The selection of the device that can implement the behavior, and the required interfacing, is usually done by human experts. The interface consists of transformations that may have to be performed on the inputs and outputs of the device. This paper describes an approach to automatically derive the specifications of the device's interface. For sequential circuits, the behaviors are often represented as FSMs, and hence the task is to determine whether the FSM of the desired function can be contained in the FSM of the device, subject to the transformations of the interface. A related objective, addressed in this paper, is to model the behaviors of complex devices in a way that facilitates the analysis.

In order to design microprocessor-based application systems, several cooperating tasks have to be performed, such as the design of the skeletal process, hardware-software partitioning, design of the hardware configuration, interface design for the selected I/O devices, and generation of application specific software code. This paper presents an integrated CAD framework for automatically designing such hardware configurations and software code, to achieve the functionalities of the desired application. The design of an ECG monitoring system has been presented to illustrate the efficacy of the system.