{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T11:11:11Z","timestamp":1648984271028},"reference-count":37,"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\/bf01383876","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T02:10:10Z","timestamp":1112407810000},"page":"125-148","source":"Crossref","is-referenced-by-count":2,"title":["Translating VHDL into functional symbolic finite-state models"],"prefix":"10.1007","volume":"7","author":[{"given":"Gert","family":"D\ufffdhmen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ronald","family":"Herrmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hergen","family":"Pargmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"C-27","key":"CR1","first-page":"509","volume":"6","author":"S.B. Akers","year":"1978","unstructured":"S.B. Akers, ?Binary Decision Diagrams, Transactions on Computers,?IEEE, 6(C-27):509?516, 1978.","journal-title":"IEEE"},{"key":"CR2","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang, ?Symbolic Model Checking: 1020 States and Beyond,?Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, 1990."},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill, ?Sequential Circuit Verification using Symbolic Model Checking,?ACM IEEE Design Automation Conference, 1990.","DOI":"10.1145\/123186.123223"},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"D. Borrione, H. Eveking, and L. Pierre, ?Formal proofs from HDL description,? Technical Report, 1993.","DOI":"10.1007\/978-94-011-1914-6_5"},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"P.T. Breuer, L. Sanches Fernandes, and C.D. Cloos, ?Clean formal semantics for VHDL,?EDAC, 1994.","DOI":"10.1109\/EDTC.1994.326810"},{"key":"CR6","unstructured":"D. Borrione, L. Pierre, and A. Salem, ?PREVAIL: A proof environment for VHDL environments,?Proceedings of the Advanced Research Workshop on Correct Hardware Design Methodologies, 1991."},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"K.S. Brace, R.L. Rudell, and R.E. Bryant, ?Efficient implementation of a BDD package,?ACM\/IEEE Proceedings 27th Design Automation Conference, Orlando, Florida, pp. 40?45, 1990.","DOI":"10.1145\/123186.123222"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, ?Graph Based Algorithms for Boolean Function Manipulation,?Transaction on Computers, C-35:677?691, 1986.","journal-title":"Transaction on Computers, C"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long, ?Model checking and abstraction,?Proceedings of the 19th ACM Symposium on Principles of Programming Languages, pp. 343?354, 1992.","DOI":"10.1145\/143165.143235"},{"key":"CR10","unstructured":"D. Deharbe and D. Borrione, ?Symbolic model checking of VHDL design entities,? Technical Report RR 9925-I-, Laboratoire ARTEMIS, Grenoble, 1993."},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"D. Dams, G. D\u00f6hmen, R. Gerth, R. Herrmann, P. Kelb, and H. Pargmann, ?Design of a VHDL\/S model checker based on adaptive state and data abstraction,?CAV, 1994.","DOI":"10.1007\/3-540-58179-0_75"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"D. Dams, O. Grumberg, and R. Gerth, ?Generation of reduced models for checking fragments of CTL,? C. Courcoubetis, ed.,Computer Aided Verification, Lecture Notes in Computer Science 697, Springer Verlag, 1993, pp. 479?490.","DOI":"10.1007\/3-540-56922-7_39"},{"key":"CR13","unstructured":"G. D\u00f6hmen, R. Herrmann, and H. Pargmann, ?A Case Study for the Generation of a Symbolic Model from VHDL,? Technical Report, 1994."},{"key":"CR14","unstructured":"W. Damm, B. Josko, and R. Schl\u00f6r, ?Linking VHDL with formal verification tools: How to generate finite-state models out of VHDL designs,? ESPRIT Project No. 6128, OFFIS-1992-1, September 1992."},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"W. Damm, B. Josko, and R. Schl\u00f6r, ?A net-based semantics for VHDL,?Eurodac, 1993.","DOI":"10.1109\/EURDAC.1993.410685"},{"key":"CR16","unstructured":"W. Damm, B. Josko, and R. Schl\u00f6r, ?Specification and Verification of VHDL-based System-Level Hardware Designs,?Specification and Validation Methods for Programming Languages and Systems, Oxford University Press, 1994."},{"key":"CR17","unstructured":"G. D\u00f6hmen, ?Petri nets as intermediate representation between VHDL and symbolic transition systems,?EURO VHDL, 1994."},{"key":"CR18","unstructured":"W. Damm and R. Schl\u00f6r, ?Specification and verification of system-level hardware designs using timing diagrams,?EDAC-EUROASIC, 1993."},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"T. Filkorn, ?Functional Extension of Symbolic Model Checking,?CAV, Aalborg, 1991.","DOI":"10.1007\/3-540-55179-4_22"},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"T. Filkorn, ?A Method for Symbolic Verification of Synchronous Circuits,?Proc. 10th Int. Symp. on Computer Hardware Description Languages and Their Applications, 1992.","DOI":"10.1016\/B978-0-444-89208-9.50020-X"},{"key":"CR21","unstructured":"L.S. Fermandes and C.D. Kloos, ?Functional Description of VHDL,?Segundo Congreso de Programacion Declarativa PRODE'93, Spain, 1993."},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"E. Felt, G. York, R. Brayton, and A. Sangiovanni-Vincentelli, ?Dynamic Variable Reordering for BDD Minimization,?Proceedings of EURO-DAC'93, 1993.","DOI":"10.1109\/EURDAC.1993.410627"},{"key":"CR23","unstructured":"R. Herrmann and H. Pargmann, ?Computing binary decision diagrams for VHDL data types,?EURO VHDL, 1994."},{"key":"CR24","unstructured":"C.N. Ip and D.L. Dill, ?Better verification through symmetry,? D. Agnew, L. Claesen, and R. Camposano, ed.,CHDL 93, pp. 87?100, 1993."},{"key":"CR25","unstructured":"IEEE, IEEE Standard 1076?1987,VHDL Reference Manual, 1987."},{"key":"CR26","unstructured":"B. Josko, ?Modular Specification and Verification of Reactive Systems?,Habilitationsschrift, University of Oldenburg, 1993."},{"key":"CR27","unstructured":"R. Lipset, C. Schaefer, and C. Ussery,VHDL: Hardware Description and Design, Kluwer Academic Publisher, 1991."},{"key":"CR28","volume-title":"Symbolic Model Checking: An approach to the state explosion problem?","author":"K.L. McMillan","year":"1992","unstructured":"K.L. McMillan, ?Symbolic Model Checking: An approach to the state explosion problem?, PhD thesis, Carnegie Mellon University, Pittsburgh, 1992."},{"key":"CR29","doi-asserted-by":"crossref","unstructured":"J. M\u00fcller and H. Kr\u00e4mer, ?Analysis of Multi-Process VHDL specification with a Petri net model?,Proceedings EURO-VHDL, 1993.","DOI":"10.1109\/EURDAC.1993.410679"},{"key":"CR30","unstructured":"S. Olcoz and J.M. Colon, ?Petri net based analysis of VHDL programs?, Technical Report, TGI, Madrid 1991."},{"key":"CR31","unstructured":"S. Olcoz and J.M. Colon, ?Towards a formal semantics of IEEE VHDL 1076,?Proceedings EURO-VHDL, 1993."},{"key":"CR32","unstructured":"H. Pargmann and R. Herrmann, ?Efficient symbolic transition systems for VHDL?, Technical Report, 1994."},{"key":"CR33","unstructured":"R. Rudell, ?Dynamic Variable Ordering for ordered Binary Decision Diagrams?,IEEE\/ACM International Conference on CAD, pp. 42?47, 1993."},{"key":"CR34","doi-asserted-by":"crossref","unstructured":"G. Umbreit, ?Providing a VHDL interface for proof systems?,EDAC, 1992.","DOI":"10.1109\/EURDAC.1992.246187"},{"key":"CR35","unstructured":"J.P. van Tassel, ?The semantics of VHDL with VAL and HOL: Towards Practical Verification Tools?, M.Sc. Thesis, Dept. of Computer Science and Engineering, Wright University, 1989."},{"key":"CR36","doi-asserted-by":"crossref","unstructured":"J.P. van Tassel, ?A formalisation of the VHDL simulation cycle?, Technical Report 249, University of Cambridge, Computer Laboratory, 1992.","DOI":"10.1016\/B978-0-444-89880-7.50029-2"},{"key":"CR37","unstructured":"J.P. van Tassel, ?Femto-VHDL: The Semantics of a subset of VHDL and its Embedding in the HOL Theorem Prover?, PhD thesis, University of Cambridge, 1993."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383876.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01383876\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383876","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T16:22:59Z","timestamp":1586190179000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01383876"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,8]]},"references-count":37,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1995,8]]}},"alternative-id":["BF01383876"],"URL":"https:\/\/doi.org\/10.1007\/bf01383876","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,8]]}}}