{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T05:57:14Z","timestamp":1742795834866,"version":"3.32.0"},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"5-6","license":[{"start":{"date-parts":[[1997,9,1]],"date-time":"1997-09-01T00:00:00Z","timestamp":873072000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1997,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We have previously developed a verified algorithm for compiling programs written in an occam-like language into delay-insensitive circuits. In this paper we show how to retarget our compiler for clocked circuits. Since verifying a hardware compiler is a huge effort, it is significant that we are able to retarget our compiler proof without recreating that effort.<\/jats:p><jats:p>The chief contribution of this paper is the methodology used for retargeting our compiler which is based upon a new model for systems with both synchronous and asynchronous behaviour. The retargeting proof utilizes both theorems proved algebraically by hand and theorems proved automatically by state exploration. The technique of protocol conversion is used extensively in modularizing the proof of the clocked implementation.<\/jats:p>","DOI":"10.1007\/bf01211459","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T19:44:01Z","timestamp":1109360641000},"page":"537-559","source":"Crossref","is-referenced-by-count":3,"title":["Verified compilation of communicating processes into clocked circuits"],"prefix":"10.1145","volume":"9","author":[{"given":"John","family":"O'Leary","sequence":"first","affiliation":[{"name":"School of Electrical Engineering, Cornell University, Ithaca, New York, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geoffrey","family":"Brown","sequence":"additional","affiliation":[{"name":"School of Electrical Engineering, Cornell University, Ithaca, New York, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wayne","family":"Luk","sequence":"additional","affiliation":[{"name":"Department of Computing, Imperial College of Science, Technology and Medicine, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01214557"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Brown G. M.: Towards Truly Delay-Insensitive Circuit Realizations of Process Algebras. Designing Correct Circuits Jones G. and Sheeran M. (editors) pp. 120\u2013131. Springer-Verlag 1991.","DOI":"10.1007\/978-1-4471-3544-9_7"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Burch J. R.: Modeling Timing Assumptions with Trace Theory. International Conference on Computer Design pp. 208\u2013211 1989.","DOI":"10.1109\/ICCD.1989.63357"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Dill D. L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits . MIT Press 1989.","DOI":"10.7551\/mitpress\/6874.001.0001"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01887207"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"He J. Brown G. Luk W. and O'Leary J.W.: Deriving Two-Phase Modules for a Multi-Target Hardware Compiler. Designing Correct Circuits Springer Electronic Workshop in Computing series 1996.","DOI":"10.14236\/ewic\/DCC1996.3"},{"key":"e_1_2_1_2_7_2","unstructured":"Hoare C. A. R.: Communicating Sequential Processes . Prentice-Hall International 1985."},{"key":"e_1_2_1_2_8_2","unstructured":"He J. Page I. and Bowen J.: Towards a Provably Correct Hardware Implementation of Occam. Correct Hardware Design and Verification Methods volume 683 of Lecture Notes in Computer Science pp. 214\u2013225 Springer-Verlag 1993."},{"key":"e_1_2_1_2_9_2","unstructured":"Jones G. Programming in occam . Prentice-Hall International 1987."},{"key":"e_1_2_1_2_10_2","unstructured":"O'Leary J. and Brown G.: A Model for Verifying Digital Circuits. Acta Informatica in press 1997."},{"key":"e_1_2_1_2_11_2","unstructured":"O'Leary J. W.: A Model and Proof Technique for Verifying Hardware Compilers for Communicating Processes . Ph.D. thesis Cornell University 1995."},{"key":"e_1_2_1_2_12_2","first-page":"271","volume-title":"FPGAs","author":"Page I.","year":"1991"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"van Berkel K.: Handshake Circuits: An Asynchronous Architecture for VLSI Programming . Cambridge University Press 1993.","DOI":"10.1017\/CBO9780511585777"},{"key":"e_1_2_1_2_14_2","unstructured":"Verhoeff T.: A Theory of Delay-Insensitive Systems . Ph.D. thesis Eindhoven University of Technology 1994."},{"key":"e_1_2_1_2_15_2","unstructured":"Weber S. Bloom B. and Brown G. M.: Compiling Joy into Silicon. Advanced Research in VLSI and Parallel Systems: Proceedings of the 1992 Brown\/MIT Conference pp. 79\u201398 1992."},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.247651"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211459.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211459\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211459","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,24]],"date-time":"2024-12-24T01:16:29Z","timestamp":1735002989000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211459"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,9]]},"references-count":16,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[1997,9]]}},"alternative-id":["10.1007\/BF01211459"],"URL":"https:\/\/doi.org\/10.1007\/bf01211459","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[1997,9]]}}}