{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:36:54Z","timestamp":1725550614683},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291053"},{"type":"electronic","value":"9783540320302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560548_10","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T09:38:22Z","timestamp":1128591502000},"page":"97-113","source":"Crossref","is-referenced-by-count":9,"title":["Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units"],"prefix":"10.1007","author":[{"given":"Miroslav N.","family":"Velev","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X","volume-title":"Formal Methods in Computer-Aided Design","author":"M.D. Aagaard","year":"2002","unstructured":"Aagaard, M.D., Day, N.A., Lou, M.: Relating multi-step and single-step microprocessor correctness statements. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517. Springer, Heidelberg (2002)"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Aagaard, M.D., Cook, B., Day, N.A., Jones, R.B.: A framework for superscalar microprocessor correctness statements. Software Tools for Technology Transfer (STTT)\u00a04(3) (May 2003)","DOI":"10.1007\/s10009-002-0087-0"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science\u00a066 (2002)","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. International Journal on Software Tools for Technology Transfer (STTT)\u00a05(2\u20133) (March 2004)","DOI":"10.1007\/s10009-003-0121-x"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., German, S., Velev, M.N.: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Transactions on Computational Logic (TOCL)\u00a02(1) (2001)","DOI":"10.1145\/371282.371364"},{"issue":"4","key":"10_CR6","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1145\/566385.566390","volume":"3","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. ACM Transactions on Computational Logic (TOCL)\u00a03(4), 604\u2013627 (2002)","journal-title":"ACM Transactions on Computational Logic (TOCL)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automated verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818. Springer, Heidelberg (1994)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Burch, J.R.: Techniques for verifying superscalar microprocessors. In: 33rd Design Automation Conference (DAC 1996) (June 1996)","DOI":"10.1109\/DAC.1996.545637"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/BFb0055616","volume-title":"CONCUR \u201988 Concurrency Theory","author":"W. Damm","year":"1988","unstructured":"Damm, W., Pnueli, A., Ruah, S.: Herbrand Automata for Hardware Verification. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 67\u201383. Springer, Heidelberg (1988)"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/BFb0028749","volume-title":"Computer Aided Verification","author":"A. Goel","year":"1998","unstructured":"Goel, A., Sajid, K., Zhou, H., Aziz, A., Singhal, V.: BDD based procedures for a theory of equality with uninterpreted functions. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 244\u2013255. Springer, Heidelberg (1998)"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A fast and robust sat-solver. In: DATE 2002, March 2002, pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"10_CR12","unstructured":"Goldberg, E., Novikov, Y.: SAT-solver BerkMin621 (June 2003)"},{"key":"10_CR13","volume-title":"Computer Architecture: A Quantitative Approach","author":"J.L. Hennessy","year":"2002","unstructured":"Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach, 3rd edn. Morgan Kaufmann, San Francisco (2002)","edition":"3"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Decomposing refinement proofs using assume-guarantee reasoning. In: International Conference on Computer-Aided Design, ICCAD 2000 (2000)","DOI":"10.1109\/ICCAD.2000.896481"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/3-540-48683-6_7","volume-title":"Computer Aided Verification","author":"R. Hosabettu","year":"1999","unstructured":"Hosabettu, R., Srivas, M., Gopalakrishnan, G.: Proof of correctness of a processor with reorder buffer using the completion functions approach. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 47\u201359. Springer, Heidelberg (1999)"},{"key":"10_CR16","volume-title":"30. Jahrestagung der Gesellshaft f\u00fcr Informatik","author":"C. Jacobi","year":"2000","unstructured":"Jacobi, C., Kr\u00f6ning, D.: Proving the correctness of a complete microprocessor. In: 30. Jahrestagung der Gesellshaft f\u00fcr Informatik. Springer, Heidelberg (2000)"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Kr\u00f6ning, D., Paul, W.J.: Automated pipeline design. In: Design Automation Conference (DAC 2001) (June 2001)","DOI":"10.1145\/378239.379071"},{"key":"10_CR18","unstructured":"Lahiri, S., Pixley, C., Albin, K.: Experience with term level modeling and verification of the M\u2219CORETM microprocessor core. In: International Workshop on High Level Design, Validation and Test (HLDVT 2001) (November 2001)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_9","volume-title":"Formal Methods in Computer-Aided Design","author":"S.K. Lahiri","year":"2002","unstructured":"Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517. Springer, Heidelberg (2002)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. on Software Engineering\u00a03(2) (1977)","DOI":"10.1109\/TSE.1977.229904"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"D. Berre Le","year":"2004","unstructured":"Le Berre, D., Simon, L.: Results from the SAT\u201903 solver competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919. Springer, Heidelberg (2004), http:\/\/www.lri.fr\/~simon\/contest03\/results\/"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Malik, S., Wang, A.R., Brayton, R.K., Sangiovani-Vincentelli, A.: Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment. In: International Conference on Computer-Aided Design (November 1988)","DOI":"10.1109\/ICCAD.1988.122451"},{"key":"10_CR23","unstructured":"Manolios, P.: Mechanical verification of reactive systems. Ph.D. Thesis, Computer Sciences, Univ. of Texas at Austin (2001)"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.K.: Automatic verification of safety and liveness for XScale-like processor models using WEB refinements. In: Design, Automation and Test in Europe (DATE 2004), February 2004, vol.\u00a01 (2004)","DOI":"10.1109\/DATE.2004.1268844"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/3-540-48683-6_26","volume-title":"Computer Aided Verification","author":"J. Matthews","year":"1999","unstructured":"Matthews, J., Launchbury, J.: Elementary microarchitecture algebra. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 288\u2013300. Springer, Heidelberg (1999)"},{"key":"10_CR26","unstructured":"Matthews, J.R.: Algebraic specification and verification of processor microarchitectures. Ph.D. Thesis, Department of Computer Science and Engineering, Oregon Graduate Institute of Science and Technology (October 2000)"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Circular compositional reasoning about liveness. Technical Report, Cadence Berkeley Labs (1999)","DOI":"10.1007\/3-540-48153-2_30"},{"key":"10_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04267-0","volume-title":"Computer Architecture: Complexity and Correctness","author":"S.M. M\u00fcller","year":"2000","unstructured":"M\u00fcller, S.M., Paul, W.J.: Computer Architecture: Complexity and Correctness. Springer, Heidelberg (2000)"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1, infinity)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 107. Springer, Heidelberg (2002)"},{"issue":"1","key":"10_CR30","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/S0890-5401(02)93175-5","volume":"178","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Rodeh, Y., Strichman, O., Siegel, M.: The small model property: how small can it be? Journal of Information and Computation\u00a0178(1), 279\u2013293 (2002)","journal-title":"Journal of Information and Computation"},{"key":"10_CR31","unstructured":"Ryan, L.: Siege SAT Solver v.4, http:\/\/www.cs.sfu.ca\/~loryan\/personal\/"},{"key":"10_CR32","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"J. Sawada","year":"2000","unstructured":"Sawada, J.: Verification of a simple pipelined machine model. In: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Boston (2000)"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Sharangpani, H., Arora, K.: Itanium processor microarchitecture. IEEE Micro\u00a020(5) (2000)","DOI":"10.1109\/40.877948"},{"key":"10_CR34","unstructured":"Srivas, M.K., Miller, S.P.: Formal verification of an avionics microprocessor. Tech. Report CSL-95-4, SRI International (1995)"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E.: Exploiting positive equality and partial non-consistency in the formal verification of pipelined microprocessors. In: 36th Design Automation Conference (DAC 1999) (June 1999)","DOI":"10.1145\/309847.309967"},{"key":"10_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-48153-2_5","volume-title":"Correct Hardware Design and Verification Methods","author":"M.N. Velev","year":"1999","unstructured":"Velev, M.N., Bryant, R.E.: Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 37\u201353. Springer, Heidelberg (1999)"},{"key":"10_CR37","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E.: Formal verification of superscalar microprocessors with multicycle functional units, exceptions, and branch prediction. In: 37th Design Automation Conference (DAC 2000) (June 2000)","DOI":"10.1145\/337292.337331"},{"key":"10_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_24","volume-title":"Computer Aided Verification","author":"M.N. Velev","year":"2000","unstructured":"Velev, M.N.: Formal verification of VLIW microprocessors with speculative execution. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"10_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-45319-9_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.N. Velev","year":"2001","unstructured":"Velev, M.N.: Automatic abstraction of memories in the formal verification of superscalar microprocessors. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 252\u2013267. Springer, Heidelberg (2001)"},{"key":"10_CR40","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. Journal of Symbolic Computation (JSC)\u00a035(2) (February 2003)","DOI":"10.1016\/S0747-7171(02)00091-3"},{"key":"10_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45206-5_16","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M.N. Velev","year":"2003","unstructured":"Velev, M.N.: Automatic abstraction of equations in a logic of equality. In: Cialdea Mayer, M., Pirri, F. (eds.) TABLEAUX 2003. LNCS, vol.\u00a02796. Springer, Heidelberg (2003)"},{"key":"10_CR42","doi-asserted-by":"crossref","unstructured":"Velev, M.N.: Using positive equality to prove liveness for pipelined microprocessors. In: Asia and South Pacific Design Automation Conference (ASP-DAC 2004) (January 2004)","DOI":"10.1109\/ASPDAC.2004.1337588"},{"key":"10_CR43","doi-asserted-by":"crossref","unstructured":"Velev, M.N.: Efficient translation of Boolean formulas to CNF in formal verification of microprocessors. In: Asia and South Pacific Design Automation Conference (ASP-DAC 2004) (January 2004)","DOI":"10.1109\/ASPDAC.2004.1337587"},{"key":"10_CR44","doi-asserted-by":"crossref","unstructured":"Velev, M.N.: Exploiting signal unobservability for efficient translation to CNF in formal verification of microprocessors. In: Design, Automation and Test in Europe (DATE 2004) (February 2004)","DOI":"10.1109\/DATE.2004.1268859"},{"key":"10_CR45","doi-asserted-by":"crossref","unstructured":"Velev, M.N.: Comparative Study of Strategies for Formal Verification of High-Level Processors. In: 22nd International Conference on Computer Design (ICCD 2004), October 2004, pp. 119\u2013124.","DOI":"10.1109\/ICCD.2004.1347910"},{"key":"10_CR46","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E.: TLSim and EVC: A term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories. International Journal of Embedded Systems (IJES), Special Issue on Hardware-Software Codesign for Systems-on-Chip (2004)","DOI":"10.1504\/IJES.2005.008815"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560548_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:50:23Z","timestamp":1605642623000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/11560548_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}