loading...
Formal synthesis of circuits with a simple handshake protocol
New Delhi, India January 04-January 07
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICVD.1995.5121198th International Conference on VLSI ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
R. Kumar, T. Kropf, K. Schneider, "Formal synthesis of circuits with a simple handshake protocol," VLSI Design, International Conference on, pp. 255, 8th International Conference on VLSI Design, 1995.
 
 
BibTex
x
 
@article{ 10.1109/ICVD.1995.512119,
author = {R. Kumar and T. Kropf and K. Schneider},
title = {Formal synthesis of circuits with a simple handshake protocol},
journal ={VLSI Design, International Conference on},
volume = {0},
year = {1995},
isbn = {0-8186-6905-5},
pages = {255},
doi = {http://doi.ieeecomputersociety.org/10.1109/ICVD.1995.512119},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - VLSI Design, International Conference on
TI - Formal synthesis of circuits with a simple handshake protocol
SN - 0-8186-6905-5
SP
EP
A1 - R. Kumar,
A1 - T. Kropf,
A1 - K. Schneider,
PY - 1995
KW - formal logic; logic design; protocols; high level synthesis; formal circuit synthesis; handshake protocol; preproven building blocks; template; operator semantics; correctness proofs; higher-order temporal operators; parametrized data signals; HOL theorem prover; sequentially composed modules; parallel module composition; synchronous circuits
VL - 0
JA - VLSI Design, International Conference on
ER -
 
R. Kumar, Forschungszentrum Inf. Karlsruhe, Germany
T. Kropf, Forschungszentrum Inf. Karlsruhe, Germany
K. Schneider, Forschungszentrum Inf. Karlsruhe, Germany
Our approach towards the formal synthesis of circuits can be compared to that of constructing using LEGO bricks. Given a set of pre-proven building blocks they can be composed using certain operators, such that the overall composed circuit meets its specifications. Each of these building blocks obeys a simple handshake protocol and the composition takes place by plugging these building blocks into a predefined template which reflects the semantics of the operator. The correctness proofs between the templates and the operators are performed a priori. The specification of the overall circuit is given using certain higher-order temporal operators and parametrized data signals. This entire approach has been formally embedded in the HOL theorem prover.
Index Terms:
formal logic; logic design; protocols; high level synthesis; formal circuit synthesis; handshake protocol; preproven building blocks; template; operator semantics; correctness proofs; higher-order temporal operators; parametrized data signals; HOL theorem prover; sequentially composed modules; parallel module composition; synchronous circuits
Citation:
R. Kumar, T. Kropf, K. Schneider, "Formal synthesis of circuits with a simple handshake protocol," vlsid, pp.255, 8th International Conference on VLSI Design, 1995
Usage of this product signifies your acceptance of the Terms of Use.


Suggestions