{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T03:40:10Z","timestamp":1735530010182,"version":"3.32.0"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1995,8,1]],"date-time":"1995-08-01T00:00:00Z","timestamp":807235200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1995,8]]},"DOI":"10.1007\/bf01383874","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T02:10:10Z","timestamp":1112407810000},"page":"73-99","source":"Crossref","is-referenced-by-count":1,"title":["A flowgraph semantics of VHDL: Toward a VHDL verification workbench in HOL"],"prefix":"10.1007","volume":"7","author":[{"given":"Ralf","family":"Reetz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Kropf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"B. Levy, I. Filippenko, L. Marcus, and T. Menas. Using the state delta verification system (SDVS) for hardware verification. InProc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 337?360, Nijmegen, June 1992. IFIP TC10\/WG 10.2, North-Holland."},{"key":"CR2","unstructured":"B.C. Brock, W.A. Hunt, and W.D. Young. Introduction to a formally defined hardware description language. InProc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 3?35, Nijmegen, June 1992. IFIP TC10\/WG 10.2, North-Holland."},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"R. Camposano. Behavior-preserving transformations for high-level synthesis. In M. Leeser and G. Brown, editors,Proc. of Mathematical Sciences Institute Workshop: Specification, Verification and Synthesis: Mathematical Aspects, pages 106?128, July 1989.","DOI":"10.1007\/0-387-97226-9_26"},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"D. Borrione, L.V.Pierre, and A.M. Salem. Formal verification of VHDL descriptions in the Prevail environment.IEEE Design & Test of Computers, pages 42?55, June 1992.","DOI":"10.1109\/54.143145"},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"D. Boussebha, N. Giambiasi, and H. Magnier. Temporal verification of behavioral descriptions in VHDL. InEuropean Design Automation Conference, pages 692?697, Hamburg, Germany, 1992. IEEE.","DOI":"10.1109\/EURDAC.1992.246188"},{"key":"CR6","unstructured":"D. Eisenbiegler, K. Schneider, and r. Kumar. A functional approach for formalizing regular hardware structures. In J. J. Joyce and C-J. H. Seger, editors,Proc. of the International Workshop on Higher Order Logic Theorem Proving and its Applications, Vancouver, Canada, August, 11?13 1993. University of British Columbia, Springer, Lecture Notes in Computer Science No. 780."},{"key":"CR7","unstructured":"G. de Jong. verification of data flow graphs using temporal logic. InInternational Workshop on Applied Formal Methods for Correct VLSI Design, pages 169?178. IFIP WG 10.2\/WG 10.5, North-Holland, 1990, 1989."},{"key":"CR8","first-page":"263","volume":"1","author":"D.E. Knuth","year":"1970","unstructured":"D.E. Knuth and P.B. Bendix. Simple word problems in universal algebra.Computational algebra, 1:263?297, 1970.","journal-title":"Computational algebra"},{"key":"CR9","unstructured":"D.J. Kinniment and A.M. Koelmans. Modelling and verification of timing conditions with the Boyer Moore prover. InProc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 111?127, Nijmegen, June 1992. IFIP TC10\/WG 10.2, North-Holland."},{"key":"CR10","unstructured":"G. D\u00f6hmen. Petri nets as intermediate representation beween VHDL and symbolic transition systems. InEURO-VHDL'94, Grenoble, France, September 1994."},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"H. Eveking. Experience in designing formally verifiable HDL's. In D. Borrione and R. Waxman, editors,Computer Hardware Description Languages and their Applications, pages 321?334, Marseille, April 1991. IFIP WG 10.2, North-Holland.","DOI":"10.1016\/B978-0-444-89208-9.50024-7"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"F. Feldbusch and R. Kumar. Verification of synthesized circuits at register transfer level. InProc. of 2nd European Design Automation Conference, pages 22?26, Amsterdam, Februar 1991.","DOI":"10.1109\/EDAC.1991.206351"},{"key":"CR13","unstructured":"K.G.W. Goossens. Embedding a CHDDL in a proof system. LFCS Report Series ECS-LFC-91-155, University of Edinburgh, May 1991."},{"key":"CR14","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BF00121125","volume":"1","author":"A. Gupta","year":"1992","unstructured":"A. Gupta. Formal hardware verification methods: A survey.Journal of Formal Methods in System Design, 1:151?238, 1992.","journal-title":"Journal of Formal Methods in System Design"},{"key":"CR15","doi-asserted-by":"crossref","first-page":"571","DOI":"10.1016\/0165-6074(93)90197-S","volume":"38","author":"J. Helbig","year":"1993","unstructured":"J. Helbig, R. Schl\u00f6r, W. Damm, G. D\u00f6hmen, and P. Kelb. VHDL\/S ? integrating statecharts, timing diagrams, and VHDL.Microprocessing and Microprogramming, 38:571?580, 1993.","journal-title":"Microprocessing and Microprogramming"},{"key":"CR16","unstructured":"J. Van Tassel and D. Hemmendinger. Toward formal verification of VHDL specifications. InInternational Workshop on Applied Formal Methods for Correct VLSI Design, pages 409?418. IFIP WG 10.2\/WG 10.5, North-Holland, 1990, 1989."},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors.Stepwise Refinement of Distributed Systems, volume 430 ofLecture Notes in Computer Science. Springer, REX Workshop, Mook, May\/June 1989.","DOI":"10.1007\/3-540-52559-9"},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"K. Schneider, R. Kumar, and Th. Kropf. Alternative proof procedures for finite-state machines in a higherorder environment. In J. J. Joyce and C-J. H. Seger, editors,International Workshop on Higher-Order Logic Theorem Proving and its Applications, Vancouver, Canada, August, 11?13, 1993 1994.","DOI":"10.1007\/3-540-57826-9_137"},{"key":"CR19","unstructured":"L. Lamport and M. Abadi. Composing specifications. Technical report, Digital Equipment Cooperation, 1990."},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"L.M. Augustin, B.A. Gennart, Y.Huh, D.C. Luckham, and A.G. Stanculescu. Verification of VHDL designs using VAL. InProc. of the 25th Design Automation Conference, pages 48?53. ACM\/IEEE, 1988.","DOI":"10.1109\/DAC.1988.14733"},{"key":"CR21","series-title":"Technical report","volume-title":"da Vinci V1.3 user manual","author":"M. Fr\u00f6hlich","year":"1994","unstructured":"M. Fr\u00f6hlich and M. Werner. da Vinci V1.3 user manual. Technical report. University of Bremen, Bremen, Germany, March 1994."},{"key":"CR22","unstructured":"T. Margaria. Hierachical mixed-mode verification of complex FSMs described at the RT level. InProc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 129?156, Nijmegen, June 1992. IFIP TC10\/WG 10.2, North-Holland."},{"key":"CR23","unstructured":"M.C. McFarland, A.C. Parker, and R. Camposano. Tutorial on high-level synthesis. In25th Design Automation Conference, pages 330?336, 1988."},{"key":"CR24","doi-asserted-by":"crossref","unstructured":"T.F. Melham. Abstraction mechanisms for hardware verification. In G. Birtwistle and P.A. Subrahmanyam, editors,VLSI Specification, Verification, and Synthesis, pages 129?157. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_9"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"L. Pierre. From a HDL description to formal proof systems: Principles and mechanization. In D. Borrione and R. Waxman, editors,Computer Hardware Description Languages and their Applications, pages 21?41. North-Holland, Marseille, April 1991.","DOI":"10.1016\/B978-0-444-89208-9.50006-5"},{"key":"CR26","unstructured":"P.T. Breuer, L. S\u00e1nchez, and C.D. Kloos. Proof theory and a validation condition generator for VHDL. InProc. of the EURO-VHDL, Grenoble, France, September 1994. IEEE Press."},{"key":"CR27","unstructured":"R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. Van Tassel. Experience with embedding hardware description languages in HOL. InProc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 129?156, Nijmegen, June 1992. IFIP TC10\/WG 10.2, North-Holland."},{"key":"CR28","unstructured":"R. Boulton, M. Gordon, J. Herbert, and J. Van Tassel. The HOL verification of ELLA designs. InProc. of the International Workshop on Formal Methods in VLSI Design, Miami, 1991."},{"key":"CR29","doi-asserted-by":"crossref","unstructured":"R. Lipsett, C. Schaefer, and C. Ussery.VHDL: Hardware Description and Design. Kluwer Academic Publishers, 1989.","DOI":"10.1007\/978-1-4613-1631-2"},{"key":"CR30","doi-asserted-by":"crossref","unstructured":"R. Reetz and Th. Kropf. Hardwarebeschreibungssprachen und formale Verifikation. Technischer Bericht 358-C2-4\/93, Sonderforschungsbereich 358, September 1993.","DOI":"10.1021\/cr00017a906"},{"key":"CR31","doi-asserted-by":"crossref","unstructured":"R. Reetz and Th. Kropf. Simplifying deep embedding: A formalised code generator. InProc. of the International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 378?390, Malta, September 1994. Lecture Notes in Computer Science No. 859, Springer.","DOI":"10.1007\/3-540-58450-1_55"},{"key":"CR32","volume-title":"Speicification and Validation Methods","author":"D.M. Russinoff","year":"1994","unstructured":"D.M. Russinoff. Specifcation and verification of gate-level VHDL models of synchronous and asynchronous circuits. In E. B\u00f6rger, editor,Speicification and Validation Methods, Oxford University Press. Oxford, 1994."},{"key":"CR33","doi-asserted-by":"crossref","unstructured":"S. Olcoz and J.M. Colom. Toward a formal semantics of IEEE std. VHDL-1076. InEuro VHDL'93, pages 526?531, Hamburg, Germany, 1993.","DOI":"10.1109\/EURDAC.1993.410687"},{"key":"CR34","doi-asserted-by":"crossref","unstructured":"S. Rajgopal, K. Hedlund, and D. Reeves. Integrating hardware verification with CHDLs. In D. Borrione and R. Waxman, editors,Computer Hardware Description Languages and their Applications, pages 153?163. North-Holland, Marseille, April 1991.","DOI":"10.1016\/B978-0-444-89208-9.50014-4"},{"key":"CR35","unstructured":"J.P. Van Tassel. A formalisation of the VHDL simulation cycle. InProc. of the International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 213?228. IFIP WG 10.2, September 1992."},{"key":"CR36","unstructured":"V. Stavridou, J.A. Goguen, A. Stevens, S.M. Eker, S.N. Aloneftis, and K.M. Hobley. FUNNEL and 2OBJ: Towards an integrated hardware design environment. InProc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 197?223, Nijmegen, June 1992. IFIP TC10\/WG 10.2, North-Holland."},{"key":"CR37","unstructured":"IEEE standard VHDL language reference manual. Std 1076, IEEE, 1987."},{"key":"CR38","doi-asserted-by":"crossref","unstructured":"W. Damm, G. D\u00f6hmen, V. Gerstner, and B. Josko. Modular verification of petri nets. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors,Stepwise Refinement of Distributed Systems, volume 430 ofLecture Notes in Computer Science, pages 180?207, REX Workshop, Mook, May\/June 1989. Springer.","DOI":"10.1007\/3-540-52559-9_65"},{"key":"CR39","unstructured":"X. Wang and E.P. Stabler. Formalization of VHDL synthesis procedure in higher-order logic. InProc. of the International Workshop on the HOL Theorem Proving System And Its Applications, pages 106?120, August 1991."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383874.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01383874\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383874","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T02:38:51Z","timestamp":1735526331000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01383874"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,8]]},"references-count":39,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1995,8]]}},"alternative-id":["BF01383874"],"URL":"https:\/\/doi.org\/10.1007\/bf01383874","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1995,8]]}}}