@inproceedings{b910a5e07bcd46fd947679a4aa044bcf,
title = "Towards a provably correct hardware implementation of Occam",
abstract = "This paper shows how to compile a program written in a subset of occam into a normal form suitable for further processing into a netlist of components which may be loaded into a Field-Programmable Gate Array (FPGA). A simple state-machine model is adopted for specifying the behaviour of a synchronous circuit where the observable includes the state of the control path and the data path of the circuit. We identify the behaviour of a circuit with a program consisting of a very restricted subset of occam. Algebraic laws are used to facilitate the transformation from a program into a normal form. The compiling specification is presented as a set of theorems that must be proved correct with respect to these laws. A rapid prototype compiler in the form of a logic program may be implemented from these theorems.",
author = "He Jifeng and Ian Page and Jonathan Bowen",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1993.; Advanced Research Working Conference on Correct HARdware Design MEthodologies, CHARME 1993 ; Conference date: 24-05-1993 Through 26-05-1993",
year = "1993",
doi = "10.1007/bfb0021726",
language = "英语",
isbn = "9783540567783",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "214--225",
editor = "Milne, \{George J.\} and Laurence Pierre",
booktitle = "Correct Hardware Design and Verification Methods - IFIP WG 10.2 Advanced Research Working Conference CHARME 1993, Proceedings",
address = "德国",
}