loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
8th International Conference on VLSI Design
An HOL based framework for design of correct high level synthesizers
New Delhi, India
January 04-January 07
ISBN: 0-8186-6905-5
ASCII Text
x 
 
B.M. Subraya, A. Kumar, S. Kumar, "An HOL based framework for design of correct high level synthesizers," VLSI Design, International Conference on, pp. 249, 8th International Conference on VLSI Design, 1995.
 
 
BibTex
x
 
@article{ 10.1109/ICVD.1995.512118,
author = {B.M. Subraya and A. Kumar and S. Kumar},
title = {An HOL based framework for design of correct high level synthesizers},
journal ={VLSI Design, International Conference on},
volume = {0},
year = {1995},
isbn = {0-8186-6905-5},
pages = {249},
doi = {http://doi.ieeecomputersociety.org/10.1109/ICVD.1995.512118},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - VLSI Design, International Conference on
TI - An HOL based framework for design of correct high level synthesizers
SN - 0-8186-6905-5
SP
EP
A1 - B.M. Subraya,
A1 - A. Kumar,
A1 - S. Kumar,
PY - 1995
KW - high level synthesis; formal verification; formal logic; HOL based framework; high level synthesizer design; design correctness guarantee; formal framework; verification process; modularity; verifiable templates; higher order logic; synthesis module correctness
VL - 0
JA - VLSI Design, International Conference on
ER -
 
B.M. Subraya, Dept. of Comput. Sci. & Eng., S.J. Coll. of Eng., Mysore, India
A. Kumar, Dept. of Comput. Sci. & Eng., S.J. Coll. of Eng., Mysore, India
S. Kumar, Dept. of Comput. Sci. & Eng., S.J. Coll. of Eng., Mysore, India
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.
Index Terms:
high level synthesis; formal verification; formal logic; HOL based framework; high level synthesizer design; design correctness guarantee; formal framework; verification process; modularity; verifiable templates; higher order logic; synthesis module correctness
Citation:
B.M. Subraya, A. Kumar, S. Kumar, "An HOL based framework for design of correct high level synthesizers," vlsid, pp.249, 8th International Conference on VLSI Design, 1995
Usage of this product signifies your acceptance of the Terms of Use.