Formal synthesis of circuits with a simple handshake protocol

Author

Kumar, Ramayya ; Kropf, Thomas ; Schneider, Klaus

Author_Institution

Forschungszentrum Inf. Karlsruhe, Germany

fYear

1995

fDate

4-7 Jan 1995

Firstpage

255

Lastpage

259

Abstract

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

Keywords

formal logic; high level synthesis; logic design; protocols; HOL theorem prover; correctness proofs; formal circuit synthesis; handshake protocol; higher-order temporal operators; operator semantics; parallel module composition; parametrized data signals; preproven building blocks; sequentially composed modules; synchronous circuits; template; Circuit simulation; Circuit synthesis; Control system synthesis; Fault tolerance; Hardware; Logic; Pipelines; Protocols; Signal synthesis; Software tools;

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.512119

Filename

512119