An HOL based framework for design of correct high level synthesizers

Author

Subraya, B.M. ; Kumar, Anshul ; Kumar, Shashi

Author_Institution

Dept. of Comput. Sci. & Eng., S.J. Coll. of Eng., Mysore, India

fYear

1995

fDate

4-7 Jan 1995

Firstpage

249

Lastpage

254

Abstract

The paper investigates the problem of designing high level synthesizers which would guarantee correctness of the designs produced. No satisfactory solution to this problem had been available so far. The paper presents a formal framework in which the synthesis and verification processes can be modelled in a practical way. It is shown that the complexity of the verification process can be reduced by following the modularity usually present in a synthesizer design. To simplify the correctness proof of the individual synthesis steps, some easily verifiable templates are defined, in which the algorithms can be expressed. The methodology is embedded in HOL (Higher Order Logic) system

Keywords

formal logic; formal verification; high level synthesis; HOL based framework; design correctness guarantee; formal framework; high level synthesizer design; higher order logic; modularity; synthesis module correctness; verifiable templates; verification process; Circuit synthesis; Educational institutions; Hardware; Logic circuits; Logic design; Scheduling; Synthesizers; Very large scale integration;

fLanguage

English

Publisher

ieee

Conference_Titel

VLSI Design, 1995., Proceedings of the 8th International Conference on

Conference_Location

New Delhi

ISSN

1063-9667

Print_ISBN

0-8186-6905-5

Type

conf

DOI

10.1109/ICVD.1995.512118

Filename

512118