{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:40:48Z","timestamp":1725493248047},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651918"},{"type":"electronic","value":"9783540495192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49519-3_16","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T06:37:12Z","timestamp":1192862232000},"page":"222-236","source":"Crossref","is-referenced-by-count":3,"title":["Combined Formal Post- and Presynthesis Verification in High Level Synthesis"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Lock","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Mendler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Mutz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"16_CR1","unstructured":"H. Achatz. SUSAN: System for universal scheduling and allocation. In SASIMI Synthesis and Simulation Meeting and International Interchange, pages 138\u201344, 1993."},{"key":"16_CR2","unstructured":"D. A. Basin, G. M. Brown, and M. E. Leeser. Formally verified synthesis of combinational CMOS circuits. In L. Claesen, editor, Applied Formal Methods for Correct VLSI Design, pages 251\u2013260. Oganizing Commitee of the IMEC-IFIP-Workshop, November1989."},{"key":"16_CR3","unstructured":"A. Bartsch, H. Eveking, H.-J. Faerber, M. Kelelatchew, J. Pinder, and U. Schellin. LOVERT-a logic verifier of register-transfer level description. In L. Claesen, editor, Applied Formal Methods for Correct VLSI Design, pages 522\u2013531. Organizing Commitee of the IMEC-IFIP-Workshop, November 1989."},{"key":"16_CR4","series-title":"Lect Notes Comput Sci","first-page":"165","volume-title":"Theorem proving in higher order logics","author":"C. Blumenr\u00f6hr","year":"1996","unstructured":"C. Blumenr\u00f6hr, D. Eisenbiegler, and R. Kumar. Implementation issues about the embedding of existing high level synthesis algorithms in HOL. In Joakim Wright, editor, Theorem proving in higher order logics, pages 165\u2013172. Springer, August1996. LNCS 1125."},{"key":"16_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BFb0105395","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Basin","year":"1996","unstructured":"D. Basin and S. Friedrich. Modelling a hardware synthesis methodology in Isabelle. In G. Goos, J. Hartmanis, and J. van Leeuwen, editors, Theorem Proving in Higher Order Logics, pages 33\u201350. Springer, August 1996. LNCS 1125."},{"key":"16_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-60385-9_14","volume-title":"Formal Methods in Computer Aided Design","author":"H. Barringer","year":"1995","unstructured":"H. Barringer, G. Gough, B. Monahan, and A. Williams. Formal support for the ELLA hardware description language. In Paulo E. Camurati and Hans Eveking, editors, Formal Methods in Computer Aided Design, pages 225\u2013245. Springer, July 1995. LNCS987."},{"key":"16_CR7","unstructured":"R. J. Boulton. CLaReT user\u2019s manual. Technical report, University of Cambridge, Computer Laboratory, 1995."},{"key":"16_CR8","unstructured":"R. J. Boulton. A single language for specifying abstract syntax trees, lexical analysis, parsing and pretty printing. Technical report, University of Cambridge, Computer Laboratory, 1996."},{"key":"16_CR9","unstructured":"D. Borrione and A. Salem. Proving an on-line multiplier with OBJ3 and TACHE: A practical experience. In L. Claesen, editor, Applied Formal Methods for Correct VLSI Design, pages 271\u2013280. Organizing Commitee of the IMEC-IFIP-Workshop, November 1989."},{"key":"16_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/BFb0031815","volume-title":"Formal Methods in Computer Aided Design","author":"B. Bose","year":"1996","unstructured":"Bhaskar Bose, M. Esen Tunar, and Venkatesh Choppella. A tutorial on digital design derivation using DRS. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer Aided Design, pages 270\u2013274. Springer, September 1996. LNCS 1166."},{"key":"16_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/BFb0031802","volume-title":"Formal Methods in Computer Aided Design","author":"F. J. Cantu","year":"1996","unstructured":"F. J. Cantu, A. Bundy, A. Smaill, and D. Basin. Experiments in automating hardware verification using inductive proof planning. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer Aided Design, pages 94\u2013108. Springer, September1996. LNCS 1166"},{"key":"16_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/BFb0105401","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Coupet-Grimal","year":"1996","unstructured":"Solange Coupet-Grimal and Line Jakubier. Coq and hardware verification: A case study. In G. Goos, J. Hartmanis, and J. van Leeuwen, editors, Theorem Proving in Higher Order Logics, pages 125\u2013140. Springer, August 1996. LNCS 1125"},{"key":"16_CR13","unstructured":"Sergio R. Ramirez Chavez. Formal proof of the cascading property of a parallel sorting circuit. In L. Claesen, editor, Applied Formal Methods for Correct VLSI Design, pages 338\u2013346. Organizing Commitee of the IMEC-IFIP-Workshop, November 1989."},{"key":"16_CR14","unstructured":"L. Claesen, F. Proesmans, E. Verlind, and H. DeMan. SFG-tracing: A formal verification methodology. In ACM-SIGDA Workshop, February 1990. Miami."},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"C. Delgado Kloos and P. T. Breuer, editors. Formal Semantics for VHDL. Kluwer Academic Publishers, 1995.","DOI":"10.1007\/978-1-4615-2237-9"},{"key":"16_CR16","unstructured":"S. Finn, M. P. Fourman, M. Francis, and R. Harris. Formal system design \u2014 interactive synthesis based on computer-assisted formal reasoning. In L. Claesen, editor, Workshop on Applied Formal Methods for Correct VLSI Design, pages 97\u2013110, 1989. North Holland."},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"D. Gajski, N. Dutt, A Wu, S. Lin, et al. High Level Synthesis: Introduction to Chip and System Design. Kluwer Academic Publishers, 1992.","DOI":"10.1007\/978-1-4615-3636-9"},{"key":"16_CR18","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"W. Grass, M. Mutz, and W.-D. Tiedemann. High level synthesis based on formal methods. In EUROMICRO\u2019 94, pages 83\u201391, 1994. Liverpool (Great Britain).","DOI":"10.1109\/EURMIC.1994.390403"},{"key":"16_CR20","unstructured":"A. A. Jerraya, H. Ding, P. Kission, and M. Rahmouni. Behavioral Synthesis and Component Reuse with VHDL. Kluwer Academic Publishers, 1992."},{"key":"16_CR21","unstructured":"G. G. de Jong. Generalized Data Flow Graphs \u2014 Theory and Applications. PhD thesis, Eindhoven, 1993. Cip-Gegevens Koninklijke Bibliotheek, Den Haag."},{"key":"16_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/BFb0031817","volume-title":"Formal Methods in Computer Aided Design","author":"R. Kumar","year":"1996","unstructured":"R. Kumar, C. Blumenr\u00f6hr, D. Eisenbiegler, and D. Schmid. Formal synthesis in circuit design\u2014 a classification and survey. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer Aided Design, pages 294\u2013309. Springer, September 1996. LNCS 1166"},{"issue":"2","key":"16_CR23","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1093\/comjnl\/38.2.101","volume":"38","author":"M. Larsson","year":"1995","unstructured":"M. Larsson. An engineering approach to formal digital system design. The Computer Journal, 38(2):101\u201310, 1995.","journal-title":"The Computer Journal"},{"key":"16_CR24","unstructured":"Th. Lock and M. Mutz. FORVERTIS: Projektbericht. Technical report, Universit\u00c4t Passau, Lehrstuhl f\u00fcr Rechnerstrukturen, Oktober 1997."},{"key":"16_CR25","unstructured":"Th. Lock and M. Mendler. Formale Modellierung von kontrollflu\\dominierten High-Level-Synthese-Eingabebeschreibungen zur Verifikation von Ergebnissen kontrollflu\\gesteuerter Einplanungsverfahren. In F. J. Rammig and W. M\u00fcller, editors, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, pages 75\u201384. GI\/ITG\/GMM, HNI-Verlagsschriftenreihe, M\u00c4rz 1998. Paderborn."},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"S. S. Leung and M. A. Shanblatt. ASIC System Design with VHDL: A Paradigm. Kluwer Academic Publishers, 1989.","DOI":"10.1007\/978-1-4615-6473-7"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"P. Michel, U. Lauther, and P. Duzy. The Synthesis Approach to Digital System Design. Kluwer Academic Publishers, 1992.","DOI":"10.1007\/978-1-4615-3632-1"},{"key":"16_CR28","unstructured":"M. Mutz. Presynthesis proof and postsynthesis tactic for pure dataflow descriptions in high level synthesis. http:\/\/acrux.fmi.uni-passau.de\/~lock\/pre-post-proof.html . au][NCS]_The benchmark archives at CBL. http:\/\/www.cbl.ncsu.edu\/www\/benchmarks\/"},{"key":"16_CR29","series-title":"Lect Notes Comput Sci","first-page":"246","volume-title":"Formal Methods in Computer Aided Design","author":"N.F.G.+.9.5._.R. Nicola De","year":"1995","unstructured":"R. De Nicola, A. Fantechi, S. Gnesi, S. Larosa, and G. Ristori. Verifying hardware components with JACK. In Paulo E. Camurati and Hans Eveking, editors, Formal Methods in Computer Aided Design, pages 246\u2013260. Springer, July 1995. LNCS 987"},{"key":"16_CR30","unstructured":"Laurance Pierre. The formal proof of sequential circuits described in CASCADE using the boyer-moore theorem proover. In L. Claesen, editor, Applied Formal Methods for Correct VLSI Design, pages 365\u2013384. Organizing Commitee of the IMEC-IFIP-Workshop, November 1989."},{"key":"16_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/3-540-60385-9_3","volume-title":"Formal Methods in Computer Aided Design","author":"L. Pierre","year":"1995","unstructured":"Laurence Pierre. Describing and verifying synchronous circuits with the boyer-moore theorem proover. In Paulo E.Camurati and Hans Eveking, editors, Formal Methods in Computer Aided Design, pages 35\u201355. Springer, July 1995. LNCS 987."},{"key":"16_CR32","unstructured":"M. Rahmouni. AMICAL: Interactive behavioral synthesis based on VHDL for control-flow dominated systems. Journal of the Brazilian Computer Society, November 1995."},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"R. Reetz and T. Kropf. A Flow Graph Semantics of VHDL: A Basis for Hardware Verification with VHDL, pages 205\u201338. Kluwer Academic Publishers, 1995.","DOI":"10.1007\/978-1-4615-2237-9_8"},{"key":"16_CR34","unstructured":"H. Simonis and T. Le Provost. Verification in CHIP: Benchmark results. In L. Claesen, editor, Applied Formal Methods for Correct VLSI Design, pages 570\u2013574. Organizing Commitee of the IMEC-IFIP-Workshop, November 1989."},{"key":"16_CR35","doi-asserted-by":"crossref","unstructured":"J. P. Van Tassel. An Operational Semantics for a Subset of VHDL, pages 71\u2013106. Kluwer Academic Publishers, 1995.","DOI":"10.1007\/978-1-4615-2237-9_4"},{"key":"16_CR36","series-title":"Lect Notes Comput Sci","first-page":"415","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Tabar","year":"1996","unstructured":"S. Tabar and P. Curzon. A comparison of MDG and HOL for hardware-verification. In G. Goos, J. Hartmanis, and J. van Leeuwen, editors, Theorem Proving in Higher Order Logics, pages 415\u2013430. Springer, August 1996. LNCS 1125."},{"key":"16_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60385-9_6","volume-title":"Formal Methods in Computer Aided Design","author":"L.-G. Wang","year":"1995","unstructured":"Li-Guo Wang and Michael Mendler. Formal design of a class of computers. In Paulo E. Camurati and Hans Eveking, editors, Formal Methods in Computer Aided Design, pages 84\u2013102. Springer, July 1995. LNCS 987."},{"key":"16_CR38","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/3-540-61254-8_30","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting, HOA\u201995","author":"L. G. Wang","year":"1996","unstructured":"L. G. Wang and M. Mendler. Abstraction of hardware construction. In G. Dowek, J. Heering, B. M\u00f6ller, and K. Meinke, editors, Higher-Order Algebra, Logic, and Term Rewriting, HOA\u201995, pages 264\u2013287. Springer, 1996. LNCS 1074."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49519-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T17:59:18Z","timestamp":1556906358000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49519-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651918","9783540495192"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-49519-3_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}