{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:18:03Z","timestamp":1755217083411,"version":"3.43.0"},"reference-count":87,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1998,9,1]],"date-time":"1998-09-01T00:00:00Z","timestamp":904608000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,9,1]],"date-time":"1998-09-01T00:00:00Z","timestamp":904608000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[1998,9]]},"DOI":"10.1023\/a:1008622002590","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T10:12:40Z","timestamp":1040551960000},"page":"159-225","source":"Crossref","is-referenced-by-count":6,"title":["A Practical Methodology for the Formal Verification of RISC Processors"],"prefix":"10.1007","volume":"13","author":[{"given":"Sofi\u00e9ne","family":"Tahar","sequence":"first","affiliation":[]},{"given":"Ramayya","family":"Kumar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"180577_CR1","first-page":"15","volume-title":"Proc. Theorem Provers in Circuit Design","author":"M. Aagaard","year":"1994","unstructured":"M. Aagaard and M. Leeser, \u201cReasoning about pipelines with structural hazards,\u201d in Proc. Theorem Provers in Circuit Design, Bad Herrenalb, Germany, Sept. 1994, pp. 15\u201334."},{"key":"180577_CR2","unstructured":"Abstract Hardware Limited, LAMBDA\u2014Logic and Mathematics behind Design Automation: User and Reference Manuals, Version 3.1, 1990."},{"key":"180577_CR3","unstructured":"F. Anceau, The Architecture of Microprocessors, Addison-Wesley Publishing Company, 1986."},{"key":"180577_CR4","unstructured":"P. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth though Proof, Academic Press, 1986."},{"key":"180577_CR5","volume-title":"The formal verification of the VIPER microprocessor: EBM to phase, phase to microcode level","author":"T. Arora","year":"1990","unstructured":"T. Arora, \u201cThe formal verification of the VIPER microprocessor: EBM to phase, phase to microcode level,\u201d Master's thesis, University of California, Davis, 1990."},{"key":"180577_CR6","volume-title":"DLX VHDL model","author":"P. Ashenden","year":"1993","unstructured":"P. Ashenden, \u201cDLX VHDL model,\u201d Department of Computer Science, University of Adelaide, Australia, Nov. 1993."},{"key":"180577_CR7","doi-asserted-by":"crossref","unstructured":"T. Baker, \u201cHeadroom and legroom in the 80960 architecture,\u201d in Proc. 35th IEEE Computer Society International Conference (COMPCON'90), San Francisco, CA, Feb. 1990, pp. 299\u2013306.","DOI":"10.1109\/CMPCON.1990.63691"},{"key":"180577_CR8","unstructured":"A. Berenbaum, \u201cFunctional simulation for the CRISP microprocessor,\u201d in Proc. International Conference on Very Large Scale Integration (VLSI'87), Vancouver, Canada, Aug. 1987, pp. 323\u2013334."},{"key":"180577_CR9","unstructured":"A. Berenbaum, D. Ditzel, and H. McLellan, \u201cIntroduction to the CRISP microprocessor,\u201d in Proc. 32th IEEE Computer Society International Conference (COMPCON'87), San Francisco, CA, Feb. 1987, pp. 86\u201390."},{"key":"180577_CR10","doi-asserted-by":"crossref","unstructured":"D. Borrione, P. Camurati, J. Paillet, and P. Prinetto, \u201cA functional approach to formal hardware verification: The MTI experience,\u201d in Proc. IEEE International Conference on Computer Design (ICCD'88), Rye Brook, New York, Oct. 1988, IEEE Computer Society Press, pp. 592\u2013595.","DOI":"10.1109\/ICCD.1988.25769"},{"key":"180577_CR11","doi-asserted-by":"crossref","unstructured":"V. Bhagwati and S. Devadas, \u201cAutomatic verification of pipelined microprocessors,\u201d in Proc. ACM\/IEEE 31st Design Automation Conference (DAC'94), San Diego, CA, June 1994, pp. 603\u2013608.","DOI":"10.1145\/196244.196577"},{"key":"180577_CR12","volume-title":"AVLSI implementation of the DLX microprocessor","author":"M. Blomkvist","year":"1992","unstructured":"M. Blomkvist, J. Nilsson, and W. Sagefalk, \u201cAVLSI implementation of the DLX microprocessor,\u201d Department of Computer Engineering, Lund University, Sweden, Sept. 1992."},{"key":"180577_CR13","unstructured":"A. Bode, RISC-Architekturen, BI-Wiss, Verlag, 1990."},{"key":"180577_CR14","doi-asserted-by":"crossref","unstructured":"S. Bose and A. Fisher, \u201cVerifying pipelined hardware using symbolic logic simulation,\u201d in Proc. IEEE International Conference on Computer Design (ICCD'89), Cambridge, MA, Sept. 1989, IEEE Computer Society Press, pp. 217\u2013221.","DOI":"10.1109\/ICCD.1989.63359"},{"key":"180577_CR15","first-page":"349","volume-title":"Formal VLSI Correctness Verification, VLSI Design Methods II","author":"A. Bronstein","year":"1990","unstructured":"A. Bronstein and C. Talcott, \u201cFormal verification of pipelines based on string-functional semantics,\u201d in L. Claesen (Ed.), Formal VLSI Correctness Verification, VLSI Design Methods II, Elsevier Science Publishers B.V. (North-Holland), 1990, pp. 349\u2013367."},{"issue":"8","key":"180577_CR16","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"R. Bryant, \u201cGraph-based algorithms for Boolean function manipulation,\u201d; IEEE Transactions on Computers, Vol. C-35, No. 8, pp. 677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"180577_CR17","volume-title":"Formale spezifikation und (teil-) verifikation eines SPARC-kompatiblen prozessors mit LAMBDA","author":"O. Buckow","year":"1992","unstructured":"O. Buckow, \u201cFormale spezifikation und (teil-) verifikation eines SPARC-kompatiblen prozessors mit LAMBDA,\u201d; Diplomarbeit, Fachbereich Mathematik-Informatik, Universit\u00e4t-Gesamthochschule Paderborn, Germany, Oct. 1992."},{"key":"180577_CR18","doi-asserted-by":"crossref","unstructured":"J. Burch, \u201cTechniques for verifying superscalar microprocessors,\u201d in Proc. 33rd ACM IEEE Design Automation Conference, Las Vegas, June 1996, ACM Press, pp. 552\u2013557.","DOI":"10.1109\/DAC.1996.545637"},{"key":"180577_CR19","doi-asserted-by":"crossref","unstructured":"J. Burch and D. Dill, \u201cAutomatic verification of pipelined microprocessor control,\u201d in D. Dill (Ed.), Computer Aided Verification, Lecture Notes in Computer Science 818, Springer-Verlag, 1994, pp. 68\u201380.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"180577_CR20","unstructured":"Cadence Design Systems Inc., CADENCE User Manuals, Cadence Design Systems Inc., Oct. 1991."},{"key":"180577_CR21","unstructured":"A. Camilleri, \u201cSimulation as an aid to verification using the HOL theorem prover,\u201d Technical Report No. 150, Computer Laboratory, Cambridge University, Oct. 1988."},{"key":"180577_CR22","doi-asserted-by":"crossref","unstructured":"P. Camurati and P. Prinetto, \u201cFormal verification of hardware correctness: Introduction and survey of current research,\u201d IEEE Computer, pp. 8\u201319, July 1988.","DOI":"10.1109\/2.65"},{"key":"180577_CR23","volume-title":"Implementation of DLX in ALLIANCE","author":"CAO-VLSI Team","year":"1993","unstructured":"CAO-VLSI Team, \u201cImplementation of DLX in ALLIANCE,\u201d MASI Laboratory, University Pierre et Marie Curie, Jussieu, Paris, France, March 1993."},{"key":"180577_CR24","doi-asserted-by":"crossref","unstructured":"R. Cloutier and D. Thomas, \u201cSynthesis of pipelined instruction set processors,\u201d in Proc. ACM\/IEEE 30th Design Automation Conference (DAC'93), Dallas, Texas, June 1993, pp. 583\u2013588.","DOI":"10.1145\/157485.165053"},{"key":"180577_CR25","unstructured":"M. Coe, \u201cResults from verifying a pipelined microprocessor,\u201d Master thesis, Laboratory for Applied Logic, University of Idaho, Oct. 1994."},{"key":"180577_CR26","doi-asserted-by":"crossref","unstructured":"A. Cohn, \u201cA proof of the viper microprocessor: The first level,\u201d in G. Birtwistle and P. Subrahmanyam (Eds.), VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"180577_CR27","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/BF00243000","volume":"5","author":"A. Cohn","year":"1989","unstructured":"A. Cohn, \u201cThe notion of proof in hardware verification,\u201d Journal of Automated Reasoning, Vol. 5, pp. 127\u2013139, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"180577_CR28","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. Constable","year":"1986","unstructured":"R. Constable et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, Englewood Cliffs, NJ, 1986."},{"key":"180577_CR29","first-page":"20","volume-title":"Proc. 13th National Computer Security Conference","author":"J. Cook","year":"1990","unstructured":"J. Cook, \u201cVerification of the C\/30 microcode using the state delta verification system (SDVS),\u201d in Proc. 13th National Computer Security Conference, Washington, DC, National Bureau of Standards\/National Computer Security Centre, Oct. 1990, pp. 20\u201331."},{"key":"180577_CR30","unstructured":"D. Cyrluk, \u201cMicroprocessor verification in PVS: A methodology and simple example,\u201d Technical Report SRI-CSL-92-12, SRI Computer Science Laboratory, Dec. 1993."},{"key":"180577_CR31","volume-title":"Formale spezifikation und verifikation des DLX-RISC-prozessors","author":"M. Dehof","year":"1994","unstructured":"M. Dehof, \u201cFormale spezifikation und verifikation des DLX-RISC-prozessors,\u201d; Diplomarbeit, Institut f\u00fcr Technik der Informationsverarbeitung, Universit\u00e4t Karlsruhe, Germany, Aug. 1994."},{"key":"180577_CR32","series-title":"Technical Report","volume-title":"Implementierung des DLX RISC-processors in einer standardzellenentwufsumgebung","author":"M. Dehof","year":"1994","unstructured":"M. Dehof and S. Tahar, \u201cImplementierung des DLX RISC-processors in einer standardzellenentwufsumgebung,\u201d; Technical Report No. SFB 358-C2-1\/94, Institute for Computer Design and Fault Tolerance, University of Karlsruhe, Germany, March 1994."},{"key":"180577_CR33","volume-title":"Alpha Architecture Handbook","author":"Digital Equipment Corp.","year":"1992","unstructured":"Digital Equipment Corp., Alpha Architecture Handbook, Digital Equipment Corp., Maynard, MA, Order No. EC-H1689-10, 1992."},{"issue":"10","key":"180577_CR34","doi-asserted-by":"publisher","first-page":"1159","DOI":"10.1109\/12.93749","volume":"40","author":"P. Dubey","year":"1991","unstructured":"P. Dubey and M. Flynn, \u201cBranch strategies: Modelling and optimization,\u201d IEEE Transactions on Computer, Vol. 40, No. 10, pp. 1159\u20131167, 1991.","journal-title":"IEEE Transactions on Computer"},{"key":"180577_CR35","unstructured":"Electronic Design Interchange Format, Version 200: EIA Interim Standard No. 44, EDIF Steering Committee, Electronic Industries Association, May 1987."},{"key":"180577_CR36","volume-title":"Electrical Engineering and Electronics","author":"S. Furber","year":"1989","unstructured":"S. Furber, \u201cVLSI RISC architecture and organization,\u201d Electrical Engineering and Electronics, Marcel Dekker, New York, 1989."},{"key":"180577_CR37","first-page":"117","volume-title":"Computer Hardware Description Language and their Applications (CHDL'89)","author":"G. Gopalakrishnan","year":"1989","unstructured":"G. Gopalakrishnan, \u201cSpecification and verification of pipelined hardware in HOP,\u201d in J. Darringer and J. Rammig (Eds.), Computer Hardware Description Language and their Applications (CHDL'89), Elsevier Science Publishers B.V. (North-Holland), 1989, pp. 117\u2013131."},{"key":"180577_CR38","doi-asserted-by":"crossref","unstructured":"G. Gopalakrishnan, R. Fujimoto, V. Akella, N. Mani, and K. Smith, \u201cSpecification-driven design of custom hardware in HOP,\u201d in G. Birtwistle and P. Subrahmanyam (Eds.), Current Trends in Hardware Verification and Automated Theorem Proving, Springer-Verlag, 1989, pp. 128\u2013170.","DOI":"10.1007\/978-1-4612-3658-0_3"},{"key":"180577_CR39","unstructured":"A. Van De Goor, Computer Architecture and Design, Addison-Wesley, 1989."},{"key":"180577_CR40","unstructured":"M. Gordon, \u201cProving a computer correct using the LCF LSM hardware verification system,\u201d Technical Report No. 42, Computer Laboratory, University of Cambridge, Sept. 1983."},{"key":"180577_CR41","unstructured":"M. Gordon and T. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993."},{"key":"180577_CR42","doi-asserted-by":"crossref","unstructured":"B. Graham, The SECD Microprocessor: A Verification Case Study, Kluwer Academic Publishers, 1992.","DOI":"10.1007\/978-1-4615-3576-8"},{"issue":"2\/3","key":"180577_CR43","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BF00121125","volume":"1","author":"A. Gupta","year":"1992","unstructured":"A. Gupta, \u201cFormal hardware verification methods: A survey,\u201d Journal of Formal Methods in System Design, Vol. 1, Nos. 2\/3, pp. 151\u2013238, 1992.","journal-title":"Journal of Formal Methods in System Design"},{"key":"180577_CR44","volume-title":"VHDL design and analysis of DLX","author":"A. Gupta","year":"1991","unstructured":"A. Gupta and P. Stephan, \u201cVHDL design and analysis of DLX,\u201d CS252 Semester Project, University of California, Berkeley, May 1991."},{"issue":"3","key":"180577_CR45","first-page":"242","volume":"133","author":"F. Hanna","year":"1986","unstructured":"F. Hanna and N. Daeche, \u201cSpecification and verification of digital systems using higher-order predicate logic,\u201d IEE Proc. Pt. E, Vol. 133, No. 3, pp. 242\u2013254, Sept. 1986.","journal-title":"IEE Proc. Pt. E"},{"key":"180577_CR46","first-page":"532","volume-title":"Applied Formal Methods for Correct VLSI Design","author":"F. Hanna","year":"1989","unstructured":"F. Hanna, M. Longley, and N. Daeche, \u201cFormal synthesis of digital systems,\u201d in L. Claesen (Ed.), Applied Formal Methods for Correct VLSI Design, Elsevier Science Publishers B.V. (North-Holland), 1989, pp. 532\u2013548."},{"key":"180577_CR47","volume-title":"Computer Architecture: A Quantitative Approach","author":"J. Hennessy","year":"1996","unstructured":"J. Hennessy and D. Patterson, Computer Architecture: A Quantitative Approach, Morgan Kaufmann Publishers, San Mateo, CA, 1996."},{"key":"180577_CR48","first-page":"89","volume-title":"From HDL Description to Guaranteed Correct Circuit Designs","author":"W. Hunt","year":"1987","unstructured":"W. Hunt, \u201cThe mechanical verification of a microprocessor design,\u201d in D. Borrione (Ed.), From HDL Description to Guaranteed Correct Circuit Designs, Elsevier Science Publishers B.V. (North-Holland), 1987, pp. 89\u2013129."},{"issue":"4","key":"180577_CR49","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"W. Hunt","year":"1989","unstructured":"W. Hunt, \u201cMicroprocessor design verification,\u201d Journal of Automated Reasoning, Vol. 5, No. 4, pp. 429\u2013460, 1989.","journal-title":"Journal of Automated Reasoning"},{"issue":"12","key":"180577_CR50","doi-asserted-by":"publisher","first-page":"1537","DOI":"10.1109\/12.214662","volume":"41","author":"W. Hwu","year":"1992","unstructured":"W. Hwu and P. Chang, \u201cEfficient instruction sequencing with inline target insertion,\u201d IEEE Transactions on Computer, Vol. 41, No. 12, pp. 1537\u20131551, 1992.","journal-title":"IEEE Transactions on Computer"},{"key":"180577_CR51","volume-title":"IEEE Standard VHDL Language Reference Manual","author":"Institute of ElectricalElectronics Engineers","year":"1993","unstructured":"Institute of Electrical and Electronics Engineers, IEEE Standard VHDL Language Reference Manual, IEEE Press, New York, June 1993."},{"key":"180577_CR52","volume-title":"i860 64-Bit Microprocessor Programmer's Reference Manual","author":"Intel Corporation","year":"1989","unstructured":"Intel Corporation, i860 64-Bit Microprocessor Programmer's Reference Manual, Intel Corporation, Santa Clara, California, 1989."},{"key":"180577_CR53","unstructured":"J. Joyce, \u201cMulti-level verification of microprocessor-based systems,\u201d Ph.D. Thesis, Computer Laboratory, Cambridge University, Dec. 1989."},{"key":"180577_CR54","unstructured":"P. Kogge, The Architecture of Pipelined Computers, McGraw-Hill, 1981."},{"key":"180577_CR55","unstructured":"T. Kropf, R. Kumar, and K. Schneider, \u201cEmbedding hardware verification within a commercial design framework,\u201d Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'93), Lecture Notes in Computer Science, Springer-Verlag, 1993."},{"issue":"2","key":"180577_CR56","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/BF01383880","volume":"2","author":"R. Kumar","year":"1993","unstructured":"R. Kumar, K. Schneider, and T. Kropf, \u201cStructuring and automating hardware proofs in a higher-order theorem-proving environment,\u201d Journal of Formal Methods in System Design, Vol. 2, No. 2, pp. 165\u2013230, 1993.","journal-title":"Journal of Formal Methods in System Design"},{"key":"180577_CR57","unstructured":"L. Marcus, SDVS 10 Users' Manual, Technical Report ATR-91(6778)-10, The Aerospace Corporation, 1991."},{"key":"180577_CR58","doi-asserted-by":"crossref","unstructured":"S. McFarling and J. Hennessy, \u201cReducing the cost of branches,\u201d in Proc. 13th Annual International Symposium on Computer Architecture, Tokyo, Japan, June 1986.","DOI":"10.21236\/ADA177638"},{"key":"180577_CR59","doi-asserted-by":"crossref","unstructured":"T. Melham, \u201cAbstraction mechanisms for hardware verification,\u201d in G. Birtwistle and P. Subrahmanyam (Eds.), VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, 1988, pp. 129\u2013157.","DOI":"10.1007\/978-1-4613-2007-4_9"},{"key":"180577_CR60","unstructured":"Mentor Graphics Inc., GENESIL Designer Manuals, Mentor Graphics Inc., Sept. 1989."},{"key":"180577_CR61","unstructured":"V. Milutinovic, High Level Language Computer Architecture, Computer Science Press, 1989."},{"key":"180577_CR62","volume-title":"MC88100 RISC Microprocessor User's Manual","author":"Motorola, Inc.","year":"1988","unstructured":"Motorola, Inc., MC88100 RISC Microprocessor User's Manual, Prince-Hall, Englewood Cliffs, NJ, 1988."},{"key":"180577_CR63","volume-title":"User Guide for the PVS Specification and Verification System, Language, and Proof Checker","author":"S. Owre","year":"1993","unstructured":"S. Owre, N. Shankar, and J. Rushby, User Guide for the PVS Specification and Verification System, Language, and Proof Checker, Computer Science Laboratory, SRI International, Melno Park, CA, Feb. 1993."},{"key":"180577_CR64","doi-asserted-by":"crossref","unstructured":"P. Patel and D. Douglass, \u201cArchitecture feature of the i860\u2014Microprocessor RISC core and on-chip caches,\u201d in Proc. IEEE International Conference on Computer Design (ICCD'89), Cambridge, MA, Sept. 1989, IEEE Computer Society Press, pp. 385\u2013390.","DOI":"10.1109\/ICCD.1989.63393"},{"key":"180577_CR65","unstructured":"L. Paulson, ML for the Working Programmer, Cambridge University Press, 1991."},{"key":"180577_CR66","doi-asserted-by":"crossref","unstructured":"L. Paulson, Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science 828, Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"issue":"1652","key":"180577_CR67","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1098\/rsta.1992.0030","volume":"339","author":"A. Roscoe","year":"1992","unstructured":"A. Roscoe, \u201cOccam in the specification and verification of microprocessors,\u201d Philosophical Transactions of the Royal Society of London, Series A: Physical Sciences and Engineering, Vol. 339, No. 1652, pp. 137\u2013151, April 1992.","journal-title":"Philosophical Transactions of the Royal Society of London, Series A: Physical Sciences and Engineering"},{"key":"180577_CR68","doi-asserted-by":"crossref","unstructured":"R. Sekar and M. Srivas, \u201cFormal verification of a microprocessor using equational techniques,\u201d in G. Birtwistle and P. Subrahmanyam (Eds.), Current Trends in Hardware Verification and Automated Theorem Proving, Springer-Verlag, 1989, pp. 171\u2013217.","DOI":"10.1007\/978-1-4612-3658-0_4"},{"key":"180577_CR69","doi-asserted-by":"crossref","unstructured":"J. Saxe, S. Garland, J. Guttag, and J. Horning, \u201cUsing transformations and verification in circuit design,\u201d in Proc. 2nd Workshop on Designing Correct Circuits, Lyngby, Danmark, Jan. 1992.","DOI":"10.1007\/978-1-4471-3558-6_12"},{"issue":"5","key":"180577_CR70","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1109\/52.57892","volume":"7","author":"M. Srivas","year":"1990","unstructured":"M. Srivas and M. Bickford, \u201cFormal verification of a pipelined microprocessor,\u201d IEEE Software, Vol. 7, No. 5, pp. 52\u201364, Sept. 1990.","journal-title":"IEEE Software"},{"key":"180577_CR71","doi-asserted-by":"crossref","unstructured":"M. Srivas and S. Miller, \u201cApplying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods,\u201d Formal Methods in System Design, Kluwer Academic Publishers, Vol. 8, pp. 153\u2013188.","DOI":"10.1007\/BF00122419"},{"key":"180577_CR72","unstructured":"H. Stone: High-Performance Computer Architecture; Addison-Wesley Publishing Company, 1990."},{"key":"180577_CR73","volume-title":"The SPARC Architecture Manual","author":"Sun Microsystems, Inc.","year":"1989","unstructured":"Sun Microsystems, Inc., The SPARC Architecture Manual, Sun Microsystems, Inc., USA, Version 8, Part No. 800-1399-09, Aug. 1989."},{"key":"180577_CR74","doi-asserted-by":"crossref","unstructured":"E. Talkhan, A. Ahmed, and A. Salama, \u201cMicroprocessors functional testing,\u201d IEEE Transactions on Computer Aided Design, Vol. 8, No. 3, March 1989.","DOI":"10.1109\/43.21850"},{"key":"180577_CR75","doi-asserted-by":"crossref","unstructured":"S. Tahar and R. Kumar, \u201cTowards a methodology for the formal hierarchical verification of RISC processors,\u201d in Proc. IEEE International Conference on Computer Design (ICCD'93), Cambridge, MA, Oct. 1993, IEEE Computer Society Press, pp. 58\u201362.","DOI":"10.1109\/ICCD.1993.393405"},{"key":"180577_CR76","doi-asserted-by":"crossref","unstructured":"S. Tahar and R. Kumar, \u201cImplementing a methodology for formally verifying RISC processors in HOL,\u201d in J. Joyce and C. Seger (Eds.), Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science 780, Springer-Verlag, 1994, pp. 281\u2013294.","DOI":"10.1007\/3-540-57826-9_142"},{"key":"180577_CR77","unstructured":"S. Tahar and R. Kumar, \u201cFormal verification of pipeline conflicts in RISC processors,\u201d in Proc. European Design Automation Conference (EURO-DAC'94), Grenoble, France, Sept. 1994, IEEE Computer Society Press, pp. 285\u2013289."},{"key":"180577_CR78","doi-asserted-by":"crossref","unstructured":"S. Tahar and R. Kumar, \u201cImplementational issues for verifying RISC-pipeline conflicts in HOL,\u201d in T. Melham and J. Camilleri (Eds.), Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science 854, Springer-Verlag, 1994, pp. 424\u2013439.","DOI":"10.1007\/3-540-58450-1_58"},{"issue":"1","key":"180577_CR79","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/0141-9331(93)90091-K","volume":"17","author":"M. Thomas","year":"1993","unstructured":"M. Thomas, \u201cThe industrial use of formal methods,\u201d Microprocessor and Microsystems, Vol. 17, No. 1, pp. 31\u201336, 1993.","journal-title":"Microprocessor and Microsystems"},{"key":"180577_CR80","doi-asserted-by":"crossref","unstructured":"N. Tredemick, \u201cExperiences in commercial VLSI microprocessor design,\u201d Microprocessors and Microsystems, Vol. 12, No. 8, Oct. 1988.","DOI":"10.1016\/0141-9331(88)90134-2"},{"key":"180577_CR81","doi-asserted-by":"crossref","unstructured":"P. Villarrubia, G. Nusbaum, R. Masleid, and P. Patel, \u201cIBM RISC chip design methodology,\u201d in Proc. IEEE International Conference on Computer Design (ICCD'89), Cambridge, MA, Sept. 1989, IEEE Computer Society Press, pp. 143\u2013147.","DOI":"10.1109\/ICCD.1989.63345"},{"key":"180577_CR82","doi-asserted-by":"crossref","unstructured":"P. Windley, \u201cFormal modeling and verification of microprocessors,\u201d IEEE Transactions on Computers, Vol. 44, No. 1, 1995.","DOI":"10.1109\/12.368009"},{"key":"180577_CR83","doi-asserted-by":"crossref","unstructured":"P. Windley, \u201cVerifying pipelined microprocessors,\u201d in Proc. Conference on Hardware Description Languages (CHDL'95), Chiba, Japan, Aug. 1995, pp. 503\u2013511.","DOI":"10.1109\/ASPDAC.1995.486362"},{"key":"180577_CR84","doi-asserted-by":"crossref","unstructured":"P. Windley and J. Burch, \u201cMechanically checking a lemma used in an automatic verification tool,\u201d in M. Srivas and A. Camilleri (Eds.), Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science 1166, Springer-Verlag, 1996, pp. 262\u2013276.","DOI":"10.1007\/BFb0031821"},{"key":"180577_CR85","doi-asserted-by":"crossref","unstructured":"P. Windley and M.L. Coe, \u201cA correctness model for pipelined microprocessors,\u201d in R. Kumar and T. Kropf (Eds.), in Proc. Theorem Provers in Circuit Design, Lecture Notes in Computer Science 901, Springer-Verlag, 1995, pp. 33\u201351.","DOI":"10.1007\/3-540-59047-1_41"},{"key":"180577_CR86","volume-title":"ASIC design experience: MDLX","author":"K. Winters","year":"1992","unstructured":"K. Winters, \u201cASIC design experience: MDLX,\u201d Department of Electrical Engineering, Montana State University, USA, April 1992."},{"key":"180577_CR87","doi-asserted-by":"crossref","unstructured":"W. Wong, \u201cModelling bit vectors in HOL: The word library,\u201d in J. Joyce and C. Seger (Eds.), Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science 780, Springer-Verlag, 1994, pp. 371\u2013384.","DOI":"10.1007\/3-540-57826-9_149"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008622002590.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008622002590\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008622002590.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:31:21Z","timestamp":1754368281000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008622002590"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,9]]},"references-count":87,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1998,9]]}},"alternative-id":["180577"],"URL":"https:\/\/doi.org\/10.1023\/a:1008622002590","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1998,9]]}}}