Browse Prior Art Database

A PARTIAL SOLUTION TO THE STE SPECIFICATION COMPLETENESS PROBLEM

IP.com Disclosure Number: IPCOM000008155D
Original Publication Date: 1997-Jun-01
Included in the Prior Art Database: 2002-May-22
Document File: 4 page(s) / 253K

Publishing Venue

Motorola

Related People

Manish Pandey: AUTHOR [+2]

Abstract

Since arrays are critical components of processors, it is necessary to verify them rigorously. simulation falls short of this requirement because of the huge number of simulation patterns required for adequate coverage. The formal verification tech- nique of Symbolic Trajectory Evaluation (STE) [3,1] has shown considerable promise in solving the array verification problem. The technique of STE, given user specifications for a hardware unit, veri- fies that the unit satisfies the specifications. The specification consists of a set of assertions. Each assertion specifies an aspect of the behavior of the system being verified. While using STE, a concern often faced by the user is whether the set of assertions constituting the system specification adequately describe the functionality of the unit, and if there are aspects of the system behavior which have not been covered by any assertion. We term this problem, the STE speczjkztion complete- ness problem, and in this document we have outlined a solution to it.

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 24% of the total text.

Page 1 of 4

0 M

MOTOROLA Technical Developments

A PARTIAL SOLUTION TO THE STE SPECIFICATION COMPLETENESS PROBLEM

by Manish Pandey and Randal E. Bryant

1 INTRODUCTION

  Since arrays are critical components of processors, it is necessary to verify them rigorously. simulation falls short of this requirement because of the huge number of simulation patterns required for adequate coverage. The formal verification tech- nique of Symbolic Trajectory Evaluation (STE) [3,1] has shown considerable promise in solving the array verification problem. The technique of STE, given user specifications for a hardware unit, veri- fies that the unit satisfies the specifications. The specification consists of a set of assertions. Each assertion specifies an aspect of the behavior of the system being verified. While using STE, a concern often faced by the user is whether the set of assertions constituting the system specification adequately describe the functionality of the unit, and if there are aspects of the system behavior which have not been covered by any assertion. We term this problem, the STE speczjkztion complete- ness problem, and in this document we have outlined a solution to it.

2 BACKGROUND

2.1 STE AND A METHODOLOGY FOR ITS APPLICATION

  STE [3], which is based on symbolic ternary simulation, allows us to verify the desired behavior of the system over time. Specifications amasser- tions of the form [Antecedent => Consequent], where Antecedent and Consequent are trajectory formulas. The basic element of a trajectory formula (TF) is a simple predicate like (node-i is O), which states that node-i of a circuit contains the value Cl in the present time step.Using conjunction, case restriction and a next-time operator, trajectory formulas can be constructed from the simple predicates. If T, T-1 and T-2 are TFs, and E is a Boolean expression, then T-1 A T-2, E -> T and

N T are TFs, where N is a next-time temporal operator. Details are included in [3].

  In the methodology we use to apply STE [2], the desired system behavior is specified as a set of abstract assertions, which express system transi- tions over an abstracted system space (Example in section 2). Each assertion is written as [A =>C], which means that if A is the present state of the system, then in the next time step the state of the system is C. The syntax of A and C is similar to that of TF's, except that they do not contain N. Given implementation details such as the corre- spondence of the abstract state to the node values and their timing in the implementation, the, abstract specification is mapped into a set of STE assertions, and the implementation is verified against these. Details are in [I].

2.2 EXAMPLE

Fig. 1 4-bit memory example

  Consider the 4-bit memory unit with control, address and data lines in Figure 1. In order to verify the read operation, we write the abstract assertion shown in equation (1). This assertion states that when the read signal is asserted, the P memory location contai...