DocumentCode :
3420382
Title :
Guided synthesis and formal verification techniques for parameterized hardware modules
Author :
Claesen, L. ; Johannes, P. ; Verkest, D. ; Man, H. De
Author_Institution :
Interuniv. Micro Electron. Center, Leuven, Belgium
fYear :
1988
fDate :
11-14 Apr 1988
Firstpage :
90
Lastpage :
99
Abstract :
A method is proposed for either guided synthesis or formal correctness verification of parameterized digital hardware modules. It starts from a high-level parameterized description of the module, which is used as the specification. The method is based on the concept of correctness-preserving transformations. These transformations are described in a formal way by means of transformation descriptions. It ends at a lower-level parameterized structure description of the implementation. Direct manipulations are done using an existing hardware description language that emphasizes a strict separation between parameterized structure description and behavior description. The concepts have been applied to real VLSI design vehicles such as a pipelined and parameterized multiplier accumulator module and systolic implementation of an FIR filter. The methods presented here are easily adaptable to use in CAD
Keywords :
VLSI; circuit layout CAD; integrated circuit testing; CAD; FIR filter; VLSI design vehicles; behavior description; correctness-preserving transformations; finite impulse response; formal correctness verification; formal verification techniques; guided synthesis; hardware description language; parameterized digital hardware modules; parameterized multiplier accumulator module; parameterized structure description; pipelined; specification; systolic implementation; transformation descriptions; Circuit synthesis; Design automation; Design methodology; Formal verification; Hardware design languages; Signal design; Signal synthesis; Silicon; Vehicles; Very large scale integration;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
CompEuro '88. 'Design: Concepts, Methods and Tools'
Conference_Location :
Brussels
Print_ISBN :
0-8186-0834-X
Type :
conf
DOI :
10.1109/CMPEUR.1988.4938
Filename :
4938
Link To Document :
بازگشت