Title :
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
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;
Conference_Titel :
Application Specific Array Processors, 1994. Proceedings. International Conference on
Conference_Location :
San Francisco, CA
Print_ISBN :
0-8186-6517-3
DOI :
10.1109/ASAP.1994.331806
