{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:30:23Z","timestamp":1725456623230},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540567783"},{"type":"electronic","value":"9783540706557"}],"license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/bfb0021718","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T09:47:42Z","timestamp":1132739262000},"page":"109-121","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Combining symbolic evaluation and object oriented approach for verifying processor-like architectures at the RT-level"],"prefix":"10.1007","author":[{"given":"Jacques","family":"Chazarain","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H\u00e9lne","family":"Collavizza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,13]]},"reference":[{"key":"9_CR1","unstructured":"D. BORRIONE, P. CAMURATI, P. PRINETTO, J.L PAILLET: \u201cA functional approach to formal hardware verification: The MTI experience\u201d, Proc. IEEE International Conference on Computer Design ICCD'88, New York, Oct. 88."},{"key":"9_CR2","unstructured":"D. BORRIONE, C. LE FAOU: \u201cOverwview of the CASCADE Multi-level Hardware Description Language and its Mixed-Mode Simulation Mechanism\u201d, Proc. IFIP WG 10.2 Int. Conf. CHDL 85, Tokyo, Japan, Aug 85"},{"key":"9_CR3","unstructured":"M BICKFORD, M.SRIVAS: \u201cVerification of a Pipelined Microprocessor using CLIO\u201d, Proc Work. on \u201cHardware Specification, Verification and Synthesis: Mathematical Aspects\u201d, Ithaca, Jul 89, LNCS 408."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"P. CAMURATI, P. PRINETTO: \u201cFormal verification of hardware correctness: an introduction\u201d, Proc. 8th IFIP int. Conf CHDL 87, Armsterdam, April 1987 (also in computer 88)","DOI":"10.1109\/2.65"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"W.J. CARTER, W.H.JOYNER. D. BRAND: \u201cSymbolic Simulation for Correct Machine Design\u201d, ACM IEEE 16th Design Automation Conference, June 1979, pp 280\u2013286.","DOI":"10.1109\/DAC.1979.1600119"},{"key":"9_CR6","volume-title":"proc. workshop \u201cVLSI Specification, Specification and Synthesis\u201d","author":"A. Cohn","year":"1987","unstructured":"A. COHN: \u201cA Proof of Correctness of the Viper Microprocessor\u201d, in proc. workshop \u201cVLSI Specification, Specification and Synthesis\u201d, ed. G Birtwistle and P.A Subrahmanyam, Kaigary, KWA 1987."},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"P. CAMURATI, P. PRINETTO: \u201cFormal verification of hardware correctness: an introduction\u201d, Proc. 8th IFIP int. Conf CHDL 87, Armsterdam, April 1987 (also in computer 88)","DOI":"10.1109\/2.65"},{"key":"9_CR8","unstructured":"J. CHAZARAIN, H. COLLAVIZZA: \u201cAn Object Oriented Approach for Specifying and Proving Processor Like Architectures at the RT-Level\u201d Research Rapport RR-92-69 CNRS URA 1376 Sophia Antipolis, 1992."},{"key":"9_CR9","unstructured":"L. CLAESEN, D. BORRIONE, H. EVEKING, G.J. MILNE, J.L. PAILLET, P. PRINETTO: \u201cCHARME: towards formal design and verification for provably correct VLSI hardware\u201d, in proc. of the advanced work. on Correct Hardware Design Methodology, Turin,12\u201314 June 1991."},{"key":"9_CR10","unstructured":"H.COLLAVIZZA: \u201cFunctional Semantics of Microprocessors at the Microprogram Level and Correspondence with the Machine Instruction Level\u201d. Proc. EDAC. March 1990."},{"key":"9_CR11","unstructured":"H.COLLAVIZZA: \u201cSemantique Fonctionnelle des Microprocesseurs: L'environnement de Sp\u00e9cication et de preuve \u201d\u03bcSPEED\u201d Thesis University of Aix Marseille I 1991."},{"key":"9_CR12","unstructured":"D. VERKEST, L.CLAESEN: \u201cSpecial Benchmark Session on Tautology Checking\u201d, Proc. IFIP WG 10.2\/10.5 Work. on \u201cApplied Formal Methods for Correct VLSI Design\u201d, Houthalen, Belgium, 13\u201316 Nov. 1989 (Ed. by L. Claesen, North Holland)"},{"key":"9_CR13","volume-title":"Thesis 1935, reprinted in \u201cThe collected papers of Gerhard Gentzen\u201d","author":"G. Gentzen","year":"1969","unstructured":"G. GENTZEN: \u201cInvestigation into Logical Deduction\u201d Thesis 1935, reprinted in \u201cThe collected papers of Gerhard Gentzen\u201d E. Szabo, North Holland, Amsterdam 1969"},{"key":"9_CR14","volume-title":"\u201cLCF-LSM\u201d, TR 41","author":"M. Gordon","year":"1983","unstructured":"M. GORDON: \u201cLCF-LSM\u201d, TR 41, Computer Laboratory, University if Cambridge, England, 1983"},{"key":"9_CR15","unstructured":"W.A. HUNT: \u201cFM8501: A Verified Microprocessor\u201d, Technical Report 47, Institute for Computing Science, University of Texas at Austin, Feb 1986."},{"key":"9_CR16","volume-title":"Proc. Work. on Designing Correct Circuits","author":"J. Joyce","year":"1990","unstructured":"J. JOYCE: \u201cGeneric Specification of Digital Hardware\u201d, Proc. Work. on Designing Correct Circuits, 26\u201328 Sept 1990, Glasgow (Springer Verlag)"},{"key":"9_CR17","unstructured":"G. KAHN: \u201cNatural Semantics\u201d, Proc of Symp on Theoretical Aspects of Computer Science, Passau, Germany, LNCS 247,1987."},{"key":"9_CR18","unstructured":"M. LANGEVIN, E. CERNY: \u201cVerification of processor-like circuits\u201d, in proc. of the advanced work. on Correct Hardware Design Methodology, Turin 12\u201314 June 1991."},{"key":"9_CR19","unstructured":"G.J. MILNE: \u201cDesign for Verifiability\u201d, Proc. Work on \u201cHardware Specification, Verification and Synthesis: Mathematical Aspects\u201d, Ithaca, Jul 89, LNCS 408."},{"key":"9_CR20","unstructured":"J.L.PAILLET: \u201cFunctional Semantics of Microprocessors at the Machine Instruction Level\u201d, Proc 9th IFIP WG 10.2 Conf CHDL,Washington, June 89."},{"key":"9_CR21","volume-title":"Report DAIMI FN-19","author":"G. Plotkin","year":"1981","unstructured":"G. PLOTKIN: \u201cA structural approach to operational semantics\u201d Report DAIMI FN-19, Computer Science DPt Aarhus Univ, Danemark, 1981."},{"key":"9_CR22","unstructured":"G. L. STEELE Jr.: \u201cCommon LISP The Language\u201d Second Edition Digital Presss, 1990."},{"key":"9_CR23","unstructured":"WINDLEY: \u201cThe formal Verification of Generic Interpreters\u201d, Phd Thesis, University of California, Division of Computer Science, 1990."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0021718","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:19:40Z","timestamp":1558271980000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0021718"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540567783","9783540706557"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0021718","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]},"assertion":[{"value":"13 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}