Title :
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
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;
Conference_Titel :
VLSI Design, 1995., Proceedings of the 8th International Conference on
Conference_Location :
New Delhi
Print_ISBN :
0-8186-6905-5
DOI :
10.1109/ICVD.1995.512118
