{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:01:06Z","timestamp":1760043666562,"version":"3.33.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2007,8,1]],"date-time":"2007-08-01T00:00:00Z","timestamp":1185926400000},"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":[[2007,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A compiler from a synthesisable subset of higher order logic to clocked synchronous hardware is described. It is being used to create coprocessors for cryptographic and arithmetic applications. The compiler automatically translates a function<jats:italic>f<\/jats:italic>defined in higher order logic (typically using recursion) into a device that computes<jats:italic>f<\/jats:italic>via a four-phase handshake circuit. Compilation is by fully automatic proof in the HOL4 system, and generates a correctness theorem for each compiled function. Synthesised circuits can be directly translated to Verilog, and then input to design automation tools. A fully-expansive \u2018LCF methodology\u2019 allows users to safely modify and extend the compiler\u2019s theorem proving scripts to add optimisations or to enlarge the synthesisable subset of higher order logic.<\/jats:p>","DOI":"10.1007\/s00165-007-0028-5","type":"journal-article","created":{"date-parts":[[2007,5,29]],"date-time":"2007-05-29T11:22:39Z","timestamp":1180437759000},"page":"343-362","source":"Crossref","is-referenced-by-count":13,"title":["Proof producing synthesis of arithmetic and cryptographic hardware"],"prefix":"10.1145","volume":"19","author":[{"given":"Konrad","family":"Slind","sequence":"first","affiliation":[{"name":"School of Computing, University of Utah, 50 South Central Campus Drive, UT84112, Salt Lake City, Utah, USA"}]},{"given":"Scott","family":"Owens","sequence":"additional","affiliation":[{"name":"School of Computing, University of Utah, 50 South Central Campus Drive, UT84112, Salt Lake City, Utah, USA"}]},{"given":"Juliano","family":"Iyoda","sequence":"additional","affiliation":[{"name":"University of Cambridge Computer Laboratory, William Gates Building, 15 JJ Thomson Avenue, CB3 0FD, Cambridge, UK"}]},{"given":"Mike","family":"Gordon","sequence":"additional","affiliation":[{"name":"University of Cambridge Computer Laboratory, William Gates Building, 15 JJ Thomson Avenue, CB3 0FD, Cambridge, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1145\/291251.289440"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Blumenr\u00f6hr C Eisenbiegler D (1998) Performing high-level synthesis via program transformations within a theorem prover. In: Proceedings of the Digital System Design Workshop at the Euromicro 98 Conference V\u00e4steras Sweden pp 34\u201337 Universit\u00e4t Karlsruhe Institut f\u00fcr Rechnerentwurf und Fehlertoleranz","DOI":"10.1109\/EURMIC.1998.711771"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011184310224"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008685826293"},{"key":"e_1_2_1_2_5_2","unstructured":"Blumenr\u00f6hr C (1999) A formal approach to specify and synthesize at the system level. In: GI Workshop Modellierung und Verifikation von Systemen. Shaker-Verlag Braunschweig Germany pp 11\u201320"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/43.180266"},{"key":"e_1_2_1_2_7_2","unstructured":"Common criteria for information security evaluation 2004. Part 3: Security Assurance Requirements http:\/\/niap.nist.gov\/ cc-scheme\/cc_docs\/cc_v22_part3.pdf."},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Duan J Hurd J Li G Owens S Slind K Zhang J (2005) Functional correctness proofs of encryption algorithms. In: Proceedings of 12th conference on logic for programming artificial intelligence and reasoning (LPAR 2005) number 3835 in LNAI Springer Heidelberg pp 519\u2013533","DOI":"10.1007\/11591191_36"},{"key":"#cr-split#-e_1_2_1_2_9_2.1","unstructured":"Finn S Fourman MP Francis M Harris R (1989) Formal system design-interactive synthesis based on computer-assisted formal reasoning. In: Luc Claesen"},{"key":"#cr-split#-e_1_2_1_2_9_2.2","unstructured":"(ed) IMEC-IFIP international workshop on applied formal methods for correct VLSI Design Vol 1 pp 97-110 Houthalen Belgium November 1989. Elsevier Science Publishers B.V. North-Holland Amsterdam"},{"key":"e_1_2_1_2_10_2","unstructured":"Fox A Verifying ARM6 multiplication. http:\/\/www.cl.cam.ac.uk\/users\/acjf3."},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.362752"},{"key":"e_1_2_1_2_12_2","unstructured":"Herbert JMJ (1988) Temporal abstraction of digital designs. In: George J. Milne (ed) The fusion of hardware design and verification: proceedings of the IFIP WG 10.2 Working conference on the fusion of hardware design and verification: Glasgow Scotland North-Holland pp 4\u20136"},{"key":"e_1_2_1_2_13_2","unstructured":"Hanna FK Longley M Daeche N (1989) Formal synthesis of digital systems. In: Claesen L. (ed) Applied formal methods for correct VLSI Design North-Holland pp 153\u2013170"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/573164"},{"key":"e_1_2_1_2_15_2","unstructured":"Johnson SD Bose B (1990) DDD\u2014A system for mechanized digital design derivation. Technical Report TR323 Indiana University IU Computer Science Department"},{"key":"e_1_2_1_2_16_2","first-page":"13","volume-title":"Formal methods for VLSI design","author":"Jones G","year":"1990"},{"key":"e_1_2_1_2_17_2","unstructured":"Jones G Sheeran M (1990) Circuit design in Ruby. Lecture notes on Ruby from a summer school in Lyngby Denmark. September"},{"volume-title":"BCS FACS Workshop on Refinement","year":"1991","author":"Jones G","key":"e_1_2_1_2_18_2"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Melham TF (1993) Higher order logic and hardware verification. Cambridge University Press Cambridge England 1993. Cambridge Tracts in Theoretical Computer Science 31","DOI":"10.1017\/CBO9780511569845"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Mycroft A Sharp R (2001) Hardware synthesis using SAFL and application to processor design. In: Proceedings of the 11th advanced research working conference on correct hardware design and verification methods (CHARME\u201901) Livingston Scotland September 2001. Springer Heidelberg. Invited Talk. LNCS Vol 2144","DOI":"10.1007\/3-540-44798-9_2"},{"key":"e_1_2_1_2_21_2","unstructured":"Norrish M Slind K (project administrators). The HOL4 System. SourceForge website. http:\/\/hol.sourceforge.net\/."},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"O\u2019Donnell J (2002) Overview of Hydra: A concurrent language for synchronous digital circuit design. In: Proceedings of the 16th international parallel and distributed processing symposium. IEEE Computer Society Press","DOI":"10.1109\/IPDPS.2002.1016653"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00936948"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Pnueli A Siegel M Singerman E (1998) Translation validation. In: Proceedings of TACAS\u201998 Vol 1384 of Lecture Notes in Computer Science Springer Heidelberg pp 151\u2013166","DOI":"10.1007\/BFb0054170"},{"key":"e_1_2_1_2_25_2","first-page":"294","volume-title":"First international conference on formal methods in computer-aided design, Vol 1166","author":"Kumar R","year":"1996"},{"key":"e_1_2_1_2_26_2","unstructured":"Rivest R Robshae M Sidney R Yin YL(1998) The RC6 block cipher. Available at http:\/\/www.rsasecurity.com\/rsalabs\/rc6 August"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Sheeran M (1984)\u00a0\u03bcFP A language for VLSI design. In: Proceedings of the ACM symposium on LISP and functional programming ACM Press Austin Texas pp 104\u2013112","DOI":"10.1145\/800055.802026"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Sheeran M (1984) muFP A language for VLSI design. In: Conference record of the 1984 ACM symposium on lisp and functional programming ACM New York pp 104\u2013112","DOI":"10.1145\/800055.802026"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Slind K (1996) Function definition in higher order logic. In: Theorem proving in higher order logics number 1125 in lecture notes in computer science Springer Heidelberg pp 381\u2013398 Turku Finland","DOI":"10.1007\/BFb0105417"},{"key":"#cr-split#-e_1_2_1_2_30_2.1","doi-asserted-by":"crossref","unstructured":"Slind K (2000) Wellfounded schematic definitions. In: David McAllester","DOI":"10.1007\/10721959_4"},{"key":"#cr-split#-e_1_2_1_2_30_2.2","unstructured":"(ed) In: Proceedings of the seventeenth international conference on automated deduction CADE-17 Vol 1831 of Lecture Notes in Computer Science. Springer Heidelberg pp 45-63 Pittsburgh Pennsylvania"},{"volume-title":"Handshake circuits: an asynchronous architecture for VLSI programming","year":"1993","author":"van Berkel K","key":"e_1_2_1_2_31_2"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Wheeler D Needham R (1999) TEA a tiny encryption algorithm. In Fast Software Encryption: Second International Workshop Vol 1008 of LNCS. Springer Heidelberg pp 363\u2013366","DOI":"10.1007\/3-540-60590-8_29"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-007-0028-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-007-0028-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-007-0028-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T18:52:59Z","timestamp":1737053579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-007-0028-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,8]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,8]]}},"alternative-id":["10.1007\/s00165-007-0028-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-007-0028-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2007,8]]}}}