Title :
Formal synthesis of circuits with a simple handshake protocol
Author :
Kumar, Ramayya ; Kropf, Thomas ; Schneider, Klaus
Author_Institution :
Forschungszentrum Inf. Karlsruhe, Germany
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;
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.512119
