Browse Prior Art Database

Automatic Generation of Design Constraints in Verifying High Performance Embedded Dynamic Circuits

IP.com Disclosure Number: IPCOM000009237D
Original Publication Date: 2002-Aug-13
Included in the Prior Art Database: 2002-Aug-13

Publishing Venue

Motorola

Related People

Jayanta Bhadra: AUTHOR [+2]

Abstract

Design constraints are artifacts that model an environment of a design under verification by restricting input stimuli to plausible valuations. Judicious usage of design constraints can be effective in eliminating false verification results. Given a particular verification problem, however, it is a difficult proposition to write down all the necessary constraints. We present a technique for automatic generation of design constraints from simple user-provided information about potential design environments. Our method generates a set of design constraints representing varying degrees of assumptions about potential environments of a dynamic circuit. We also present experimental results on verification of custom designed embedded dynamic circuits taken from the Motorola MPC7455 microprocessor that is compatible with the PowerPC instruction set architecture.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 7% of the total text.

Page 1 of 13

Automatic Generation of Design Constraints in Verifying High Performance Embedded Dynamic Circuits

Jayanta Bhadra and Narayanan Krishnamurthy Motorola Inc.

Abstract

  Design constraints are artifacts that model an environment of a design under verification by restricting input stimuli to plausible valuations. Judicious usage of design constraints can be e[ff]ective in eliminating false verification results. Given a particular verification problem, however, it is a di[ffi]cult proposition to write down all the necessary constraints. We present a technique for automatic generation of design constraints from simple user-provided information about potential design environments. Our method generates a set of design constraints representing varying degrees of assumptions about potential environments of a dynamic circuit. We also present experimental results on verification of custom designed embedded dynamic circuits taken from the Motorola MPC7455 microprocessor that is compatible with the PowerPC instruction set architecture.

1 Introduction

At Motorola's High Performance Design Center, Symbolic Trajectory Evaluation (STE) [7] is routinely used to perform equivalence checking between Register Transfer Level (RTL) and transistor level descriptions of embedded custom circuits [1, 2, 3]. The transistor level description is custom designed with respect to an RTL specification. Equivalence checking is necessary as the RTL description is required to be predictive of silicon behavior. In our verification methodology, a switch level model is extracted from the transistor level implementation [5], and assertions (or, properties) are automatically generated from the RTL description [2, 4]. The assertions are then automatically proved to hold on the transistor level model by symbolic simulation under an STE framework.

  Traditionally, the state space of a system where STE can be performed consists of assignments to primary inputs, primary outputs as well as state holding elements. In order to model a hardware design for STE one has to construct a closed system where one combines the system with its encapsulating environment. However, construction of the entire environment for this purpose is a wasteful exercise. Construction of the most accurate environment needs one to make it non-deterministic such that the environment can assign any value to any primary input signal at any clock synchronous point of execution. Fortunately, most circuits are constructed under a certain set of assumptions on their environments. Thus, for practical verification purposes one needs to abstract the environment in such a way that it embodies the actual behavior of the environment under which the design is meant to operate. We term such abstractions as constraints on the behavior of the environment.

  Automatic verification is an exercise where the state space of an implementation is systematically searched - a failure occurs when a state that is inconsistent with a spec...