{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:25:24Z","timestamp":1740122724808,"version":"3.37.3"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2019,11,5]],"date-time":"2019-11-05T00:00:00Z","timestamp":1572912000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,11,5]],"date-time":"2019-11-05T00:00:00Z","timestamp":1572912000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Des Autom Embed Syst"],"published-print":{"date-parts":[[2019,12]]},"DOI":"10.1007\/s10617-019-09226-1","type":"journal-article","created":{"date-parts":[[2019,11,5]],"date-time":"2019-11-05T11:07:48Z","timestamp":1572952068000},"page":"123-151","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["On embedding a hardware description language in Isabelle\/HOL"],"prefix":"10.1007","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0993-5964","authenticated-orcid":false,"given":"Wilayat","family":"Khan","sequence":"first","affiliation":[]},{"given":"David","family":"Sanan","sequence":"additional","affiliation":[]},{"given":"Zhe","family":"Hou","sequence":"additional","affiliation":[]},{"given":"Liu","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,5]]},"reference":[{"key":"9226_CR1","unstructured":"HOL Interactive Theorem Prover. \nhttps:\/\/hol-theorem-prover.org\/\n\n. Accessed 8th Jan 2018"},{"key":"9226_CR2","unstructured":"VeryPCC project. \nhttp:\/\/isabelle.in.tum.de\/verypcc\/\n\n. Accessed 22nd Nov 2017"},{"key":"9226_CR3","volume-title":"Compilers: principles, techniques, and tools","author":"AV Aho","year":"2007","unstructured":"Aho AV, Sethi R, Ullman JD (2007) Compilers: principles, techniques, and tools, vol 2. Addison-Wesley Reading, Boston"},{"key":"9226_CR4","volume-title":"The designer\u2019s guide to VHDL","author":"PJ Ashenden","year":"2010","unstructured":"Ashenden PJ (2010) The designer\u2019s guide to VHDL, vol 3. Morgan Kaufmann, Burlington"},{"key":"9226_CR5","unstructured":"Association IS et\u00a0al (2005) IEEE Standard for Verilog Hardware Description Language. Design Automation Standards Committee. IEEE Std 1364TM-2005"},{"key":"9226_CR6","doi-asserted-by":"crossref","unstructured":"Bachrach J, Vo H, Richards B, Lee Y, Waterman A, Avi\u017eienis R, Wawrzynek J, Asanovi\u0107 K (2012) Chisel: constructing hardware in a scala embedded language. In: Proceedings of the 49th annual design automation conference. ACM, pp 1216\u20131225","DOI":"10.1145\/2228360.2228584"},{"key":"9226_CR7","unstructured":"Barras B, Boutin S, Cornes C, Courant J, Filliatre JC, Gimenez E, Herbelin H, Huet G, Munoz C, Murthy C et al (1997) The Coq proof assistant reference manual: Version 6.1. Ph.D. thesis, Inria"},{"key":"9226_CR8","doi-asserted-by":"crossref","unstructured":"Barthe G, Forest J, Pichardie D, Rusu V (2006) Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In: International symposium on functional and logic programming. Springer, pp 114\u2013129","DOI":"10.1007\/11737414_9"},{"key":"9226_CR9","volume-title":"Foundations of web script security","author":"A Bohannon","year":"2012","unstructured":"Bohannon A (2012) Foundations of web script security. University of Pennsylvania, Philadelphia"},{"key":"9226_CR10","first-page":"129","volume":"10","author":"RJ Boulton","year":"1992","unstructured":"Boulton RJ, Gordon AD, Gordon MJ, Harrison J, Herbert J, Van Tassel J (1992) Experience with embedding hardware description languages in HOL. TPCD 10:129\u2013156","journal-title":"TPCD"},{"issue":"5\u20136","key":"9226_CR11","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0950-5849(95)99362-Q","volume":"37","author":"J Bowen","year":"1995","unstructured":"Bowen J, Gordon M (1995) A shallow embedding of Z in HOL. Inf Softw Technol 37(5\u20136):269\u2013276","journal-title":"Inf Softw Technol"},{"key":"9226_CR12","unstructured":"Boyer RS, Hunt\u00a0Jr WA (2007) The e language. In: Proceedings of the international workshop on hardware design and functional languages, March"},{"key":"9226_CR13","doi-asserted-by":"crossref","unstructured":"Braibant T, Chlipala A (2013) Formal verification of hardware synthesis. In: computer aided verification. Springer, pp 213\u2013228","DOI":"10.1007\/978-3-642-39799-8_14"},{"issue":"4","key":"9226_CR14","doi-asserted-by":"publisher","first-page":"509","DOI":"10.3233\/JCS-150529","volume":"23","author":"M Bugliesi","year":"2015","unstructured":"Bugliesi M, Calzavara S, Focardi R, Khan W (2015) CookiExt: patching the browser against session hijacking attacks. J Comput Secur 23(4):509\u2013537","journal-title":"J Comput Secur"},{"issue":"ICFP","key":"9226_CR15","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/3110268","volume":"1","author":"J Choi","year":"2017","unstructured":"Choi J, Vijayaraghavan M, Sherman B, Chlipala A et al (2017) Kami: a platform for high-level parametric hardware specification and its modular verification. Proc ACM Program Lang 1(ICFP):24","journal-title":"Proc ACM Program Lang"},{"key":"9226_CR16","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge"},{"key":"9226_CR17","doi-asserted-by":"crossref","unstructured":"Clavel M, Dur\u00e1n F, Hendrix J, Lucas S, Meseguer J, \u00d6lveczky P (2007) The Maude formal tool environment. In: Algebra and coalgebra in computer science. Springer, pp 173\u2013178","DOI":"10.1007\/978-3-540-73859-6_12"},{"key":"9226_CR18","unstructured":"Compiler\u00a0II F (1999) FPGA express Verilog reference manual, synopsys. Inc.-Ver"},{"key":"9226_CR19","unstructured":"Compiler\u00a0II F (1999) FPGA express VHDL reference manual, synopsys. Inc.-Ver"},{"key":"9226_CR20","doi-asserted-by":"crossref","unstructured":"Cuadrado JS, Izquierdo JLC, Molina JG (2013) Comparison between internal and external DSLs via RubyTL and Gra2MoL. In: Formal and practical aspects of domain-specific languages: recent developments. IGI Global, pp 109\u2013131","DOI":"10.4018\/978-1-4666-2092-6.ch005"},{"issue":"1","key":"9226_CR21","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.entcs.2009.08.005","volume":"250","author":"J Dawson","year":"2009","unstructured":"Dawson J (2009) Isabelle theories for machine words. Electron Notes Theor Comput Sci 250(1):55\u201370","journal-title":"Electron Notes Theor Comput Sci"},{"issue":"127","key":"9226_CR22","first-page":"5","volume":"2004","author":"J Decaluwe","year":"2004","unstructured":"Decaluwe J (2004) MyHDL: a python-based hardware description language. Linux J 2004(127):5","journal-title":"Linux J"},{"key":"9226_CR23","volume-title":"Domain-specific languages","author":"M Fowler","year":"2010","unstructured":"Fowler M (2010) Domain-specific languages. Pearson Education, London"},{"issue":"7","key":"9226_CR24","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/1965724.1965740","volume":"54","author":"D Ghosh","year":"2011","unstructured":"Ghosh D (2011) DSL for the uninitiated. Commun ACM 54(7):44\u201350","journal-title":"Commun ACM"},{"key":"9226_CR25","unstructured":"Gibbons J (2013) Functional programming for domain-specific languages. In: Central European Functional Programming School. Springer, pp 1\u201328"},{"key":"9226_CR26","doi-asserted-by":"crossref","unstructured":"Gibbons J, Wu N (2014) Folding domain-specific languages: deep and shallow embeddings (functional pearl). In: ACM SIGPLAN Notices, vol.\u00a049. ACM, pp 339\u2013347","DOI":"10.1145\/2692915.2628138"},{"key":"9226_CR27","doi-asserted-by":"crossref","unstructured":"Gordon M (1995) The semantic challenge of Verilog HDL. In: Proceedings of tenth annual IEEE symposium on logic in computer science, 1995. LICS\u201995. IEEE, pp 136\u2013145","DOI":"10.1109\/LICS.1995.523251"},{"issue":"6","key":"9226_CR28","doi-asserted-by":"publisher","first-page":"81","DOI":"10.3390\/electronics7060081","volume":"7","author":"T Grimm","year":"2018","unstructured":"Grimm T, Lettnin D, H\u00fcbner M (2018) A survey on formal verification techniques for safety-critical systems-on-chip. Electronics 7(6):81","journal-title":"Electronics"},{"key":"9226_CR29","doi-asserted-by":"crossref","unstructured":"Haftmann F, Nipkow T (2010) Code generation via higher-order rewrite systems. In: International symposium on functional and logic programming. Springer, pp 103\u2013117","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"9226_CR30","unstructured":"Hanna K, Daeche N (1985) Specification and verification using higher-order logic. Computer hardware description languages and their applications pp 418\u2013433"},{"issue":"4es","key":"9226_CR31","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/242224.242477","volume":"28","author":"P Hudak","year":"1996","unstructured":"Hudak P (1996) Building domain-specific embedded languages. ACM Comput Surv (CSUR) 28(4es):196","journal-title":"ACM Comput Surv (CSUR)"},{"key":"9226_CR32","unstructured":"Hunt\u00a0Jr WA (1987) The mechanical verification of a microprocessor design. HDL descriptions to guaranteed correct circuit designs, pp 89\u2013129"},{"key":"9226_CR33","doi-asserted-by":"crossref","unstructured":"Hupel L, Nipkow T (2018) A verified compiler from Isabelle\/HOL to CakeML. In: European symposium on programming. Springer, pp 999\u20131026","DOI":"10.1007\/978-3-319-89884-1_35"},{"key":"9226_CR34","volume-title":"Lint, a C program checker","author":"SC Johnson","year":"1977","unstructured":"Johnson SC (1977) Lint, a C program checker. Bell Telephone Laboratories, Murray Hill"},{"key":"9226_CR35","doi-asserted-by":"crossref","unstructured":"Khan W, Azam B, Shahid N, Moeed Khan A, Shaheen A (2019) Formal verification of digital circuits using simulator with mathematical foundation. In: Applied mechanics and materials, vol 892. Trans Tech Publications Ltd., pp 134\u2013142","DOI":"10.4028\/www.scientific.net\/AMM.892.134"},{"key":"9226_CR36","unstructured":"Khan W, Tiu A, San\u00e1n D (2017) VeriFormal: an executable formal model of a hardware description language. In: SG-CRC, pp 19\u201336"},{"key":"9226_CR37","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.infsof.2015.11.001","volume":"71","author":"T Kosar","year":"2016","unstructured":"Kosar T, Bohra S, Mernik M (2016) Domain-specific languages: a systematic mapping study. Inf Softw Technol 71:77\u201391","journal-title":"Inf Softw Technol"},{"key":"9226_CR38","unstructured":"Krauss A (2008) Defining recursive functions in Isabelle\/HOL"},{"issue":"4","key":"9226_CR39","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/s10817-009-9157-2","volume":"44","author":"A Krauss","year":"2010","unstructured":"Krauss A (2010) Partial and nested recursive function definitions in higher-order logic. J Autom Reason 44(4):303\u2013336","journal-title":"J Autom Reason"},{"key":"9226_CR40","volume-title":"Hardware design verification: simulation and formal method-based approaches (Prentice Hall Modern semiconductor design series)","author":"WK Lam","year":"2005","unstructured":"Lam WK (2005) Hardware design verification: simulation and formal method-based approaches (Prentice Hall Modern semiconductor design series). Prentice Hall PTR, Upper Saddle River"},{"key":"9226_CR41","doi-asserted-by":"crossref","unstructured":"Lockhart D, Zibrat G, Batten C (2014) PyMTL: a unified framework for vertically integrated computer architecture research. In: 2014 47th annual IEEE\/ACM international symposium on microarchitecture (MICRO). IEEE, pp 280\u2013292","DOI":"10.1109\/MICRO.2014.50"},{"issue":"1","key":"9226_CR42","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1109\/TIFS.2011.2160627","volume":"7","author":"E Love","year":"2012","unstructured":"Love E, Jin Y, Makris Y (2012) Proof-carrying hardware intellectual property: a pathway to trusted module acquisition. IEEE Trans Inf Forensics Secur 7(1):25\u201340","journal-title":"IEEE Trans Inf Forensics Secur"},{"key":"9226_CR43","unstructured":"Melham TF et al (1988) Using recursive types to reason about hardware in higher order logic, vol 135. University of Cambridge, Computer Laboratory"},{"key":"9226_CR44","doi-asserted-by":"crossref","unstructured":"Meredith P, Katelman M, Meseguer J, Rosu G (2010) A formal executable semantics of Verilog. In: 2010 8th IEEE\/ACM international conference on formal methods and models for codesign (MEMOCODE). IEEE, pp 179\u2013188","DOI":"10.1109\/MEMCOD.2010.5558634"},{"issue":"4","key":"9226_CR45","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1145\/1118890.1118892","volume":"37","author":"M Mernik","year":"2005","unstructured":"Mernik M, Heering J, Sloane AM (2005) When and how to develop domain-specific languages. ACM Comput Surv (CSUR) 37(4):316\u2013344","journal-title":"ACM Comput Surv (CSUR)"},{"key":"9226_CR46","doi-asserted-by":"crossref","unstructured":"Nikhil RS (2008) Bluespec: a general-purpose approach to high-level synthesis based on parallel atomic transactions. In: High-level synthesis. Springer, pp 129\u2013146","DOI":"10.1007\/978-1-4020-8588-8_8"},{"key":"9226_CR47","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: a proof assistant for higher-order logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL: a proof assistant for higher-order logic, vol 2283. Springer, Berlin"},{"key":"9226_CR48","unstructured":"Odersky M, Altherr P, Cremet V, Emir B, Maneth S, Micheloud S, Mihaylov N, Schinz M, Stenman E, Zenger M (2004) An overview of the Scala programming language. Technical Report"},{"key":"9226_CR49","unstructured":"Pace GJ, He J (1998) Formal reasoning with Verilog HDL. In: Workshop on formal techniques for hardware and hardware-like systems"},{"key":"9226_CR50","doi-asserted-by":"crossref","unstructured":"Reetz R (1995) Deep embedding VHDL. In: International conference on theorem proving in higher order logics. Springer, pp 277\u2013292","DOI":"10.1007\/3-540-60275-5_71"},{"key":"9226_CR51","unstructured":"Shelley G, Forrest S, ACL2 Theorem Prover"},{"key":"9226_CR52","unstructured":"Sloane T (2008) Experiences with domain-specific language embedding in Scala. In: Domain-specific program development, p\u00a07"},{"key":"9226_CR53","unstructured":"Svenningsson J, Axelsson E (2012) Combining deep and shallow embedding for EDSL. In: International symposium on trends in functional programming. Springer, pp 21\u201336"},{"key":"9226_CR54","volume-title":"The Verilog\u00aehardware description language","author":"D Thomas","year":"2008","unstructured":"Thomas D, Moorby P (2008) The Verilog\u00aehardware description language. Springer, Berlin"},{"key":"9226_CR55","doi-asserted-by":"crossref","unstructured":"Wildmoser M, Nipkow T (2004) Certifying machine code safety: shallow versus deep embedding. Theorem proving in higher order logics, pp 133\u2013142","DOI":"10.1007\/978-3-540-30142-4_22"}],"container-title":["Design Automation for Embedded Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10617-019-09226-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10617-019-09226-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10617-019-09226-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,4]],"date-time":"2020-11-04T00:32:39Z","timestamp":1604449959000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10617-019-09226-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,5]]},"references-count":55,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["9226"],"URL":"https:\/\/doi.org\/10.1007\/s10617-019-09226-1","relation":{},"ISSN":["0929-5585","1572-8080"],"issn-type":[{"type":"print","value":"0929-5585"},{"type":"electronic","value":"1572-8080"}],"subject":[],"published":{"date-parts":[[2019,11,5]]},"assertion":[{"value":"24 September 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 October 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 November 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}