Verification of regular architectures using ALPHA: a case study

Author

Bezan, C. ; Quinton, P.

Author_Institution

Dept. d´´Inf., URF Sci. et Tech., Brest, France

fYear

1994

fDate

22-24 Aug 1994

Firstpage

164

Lastpage

175

Abstract

We present a formal method for the verification of regular VLSI architectures. In our method, the behavioral specification of the chip and its implementation are first expressed in ALPHA, a language for the design of regular synchronous architectures. The behavioral specification as refined down to an abstract architecture description, while the implementation is simplified by induction techniques up to the same abstract architecture level. Verification is then done by matching both descriptions. This method has been successfully applied to check the correctness of a 300.000 transistor VLSI systolic chip named API69 for sequence comparison

Keywords

VLSI; formal specification; formal verification; network analysis; specification languages; systolic arrays; transistor circuits; ALPHA; API69; VLSI architecture verification; abstract architecture; abstract architecture level; behavioral specification; case study; correctness; induction technique; sequence comparison; synchronous architecture design language; transistor VLSI systolic chip; Circuit faults; Circuit synthesis; Computer aided software engineering; Convolution; Design optimization; Difference equations; Formal verification; Hardware; Reactive power; Very large scale integration;

fLanguage

English

Publisher

ieee

Conference_Titel

Application Specific Array Processors, 1994. Proceedings. International Conference on

Conference_Location

San Francisco, CA

ISSN

1063-6862

Print_ISBN

0-8186-6517-3

Type

conf

DOI

10.1109/ASAP.1994.331806

Filename

331806