{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:58:16Z","timestamp":1725569896126},"publisher-location":"Berlin, Heidelberg","reference-count":49,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642169007"},{"type":"electronic","value":"9783642169014"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16901-4_24","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T12:40:06Z","timestamp":1289220006000},"page":"355-370","source":"Crossref","is-referenced-by-count":4,"title":["Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors"],"prefix":"10.1007","author":[{"given":"Miroslav N.","family":"Velev","sequence":"first","affiliation":[]},{"given":"Ping","family":"Gao","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_8","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":"24_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":"24_CR3","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland, Amsterdam (1954)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-642-12133-3_45","volume-title":"Reconfigurable Computing: Architectures, Tools and Applications","author":"B. Alizadeh","year":"2010","unstructured":"Alizadeh, B., Gharehbaghi, A.M., Fujita, M.: Pipelined Microprocessors Optimization and Debugging. In: Sirisuk, P., Morgan, F., El-Ghazawi, T., Amano, H. (eds.) Reconfigurable Computing: Architectures, Tools and Applications. LNCS, vol.\u00a05992, pp. 435\u2013444. Springer, Heidelberg (2010)"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Blaauw, D., Das, S.: CPU, Heal Thyself: A Fault-Monitoring Microprocessor Design Can Save Power or Allow Overclocking. IEEE Spectrum (August 2009), http:\/\/spectrum.ieee.org\/semiconductors\/processors\/cpu-heal-thyself\/0","DOI":"10.1109\/MSPEC.2009.5186555"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Bouajila, A., Zeppenfeld, J., Stechele, W., Herkersdorf, A., Bernauer, A., Bringmann, O., Rosenstiel, W.: Organic Computing at the System on Chip Level. In: IFIP International Conference on Very Large Scale Integration (VLSI-SoC 2006), pp. 338\u2013341 (2006)","DOI":"10.1109\/VLSISOC.2006.313257"},{"key":"24_CR7","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\u00a02(1) (2001)","DOI":"10.1145\/371282.371364"},{"issue":"4","key":"24_CR8","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":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58179-0_44","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":"24_CR10","doi-asserted-by":"crossref","unstructured":"Burch, J.R.: Techniques for Verifying Superscalar Microprocessors. In: Design Automation Conference (June 1996)","DOI":"10.1145\/240518.240623"},{"key":"24_CR11","unstructured":"Burcin, A.: RAD750, BAE Systems (December 2002), http:\/\/www.aero.org\/conferences\/mrqw\/2002-papers\/A_Burcin.pdf"},{"issue":"1","key":"24_CR12","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1109\/JSSC.2008.2007145","volume":"44","author":"S. Das","year":"2009","unstructured":"Das, S., Tokunaga, C., Pant, S., Ma, W.-H., Kalaiselvan, S., Lai, K., Bull, D.M., Blaauw, D.T.: RazorII: In Situ Error Detection and Correction for PVT and SER Tolerance. IEEE Journal of Solid-State Circuits\u00a044(1), 32\u201348 (2009)","journal-title":"IEEE Journal of Solid-State Circuits"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. Springer, Heidelberg (1998)"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A Fast and Robust Sat-Solver. In: Design, Automation, and Test in Europe (DATE 2002), pp. 142\u2013149 (March 2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"24_CR15","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 Publishers, San Francisco (2002)","edition":"3"},{"key":"24_CR16","unstructured":"Intel Corporation: IA-64 Application Developer\u2019s Architecture Guide (May 1999), http:\/\/developer.intel.com\/design\/ia-64\/architecture.htm"},{"key":"24_CR17","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) (2001)"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11527695_25","volume-title":"Theory and Applications of Satisfiability Testing","author":"D. Berre Le","year":"2005","unstructured":"Le Berre, D., Simon, L.: Results from the SAT 2004 SAT Solver Competition. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 321\u2013344. Springer, Heidelberg (2005)"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: 38th Design Automation Conference (DAC 2001) (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-72788-0_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"K. Pipatsrisawat","year":"2007","unstructured":"Pipatsrisawat, K., Darwiche, A.: A Lightweight Component Caching Scheme for Satisfiability Solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 294\u2013299. Springer, Heidelberg (2007)"},{"key":"24_CR21","unstructured":"Pipatsrisawat, K., Darwiche, A.: A New Clause Learning Scheme for Efficient Unsatisfiability Proofs. In: Twenty-Third AAAI Conference on Artificial Intelligence, pp. 1481\u20131484 (July 2008)"},{"key":"24_CR22","doi-asserted-by":"crossref","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) (2002)","DOI":"10.1016\/S0890-5401(02)93175-5"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Rotenberg, E.: AR-SMT: A Microarchitectural Approach to Fault Tolerance in Microprocessors. In: Annual International Symposium on Fault-Tolerant Computing (June 1999)","DOI":"10.1109\/FTCS.1999.781037"},{"key":"24_CR24","unstructured":"Ryan, L.: Siege SAT Solver v.4, http:\/\/www.cs.sfu.ca\/~loryan\/personal\/"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Su, Y.-S., Chang, P.-H., Chang, S.-C., Hwang, T.: Synthesis of a Novel Timing-Error Detection Architecture. Transactions on Design Automation of Electronic Systems (TODAES)\u00a013(1) (January 2008)","DOI":"10.1145\/1297666.1297680"},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"Subramanian, V., Bezdek, M., Avirneni, N.D., Somani, A.: Superscalar Processor Performance Enhancement Through Reliable Dynamic Clock Frequency Tuning. In: Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (2007)","DOI":"10.1109\/DSN.2007.90"},{"issue":"5","key":"24_CR27","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/40.877948","volume":"20","author":"H. Sharangpani","year":"2000","unstructured":"Sharangpani, H., Arora, K.: Itanium processor microarchitecture. IEEE Micro\u00a020(5), 24\u201343 (2000)","journal-title":"IEEE Micro"},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"Tschanz, J., Kim, N.S., Dighe, S., Howard, J., Ruhl, G., Vanga, S., Narendra, S., Hoskote, Y., Wilson, H., Lam, C., Shuman, M., Tokunaga, C., Somasekhar, D., Tang, S., Finan, D., Karnik, T., Borkar, N., Kurd, N., De, V.: Adaptive Frequency and Biasing Techniques for Tolerance to Dynamic Temperature-Voltage Variations and Aging. In: IEEE International Solid-State Circuits Conference (ISSCC 2007), pp. 292\u2013604 (February 2007)","DOI":"10.1109\/ISSCC.2007.373409"},{"issue":"7","key":"24_CR29","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1109\/TC.1986.1676803","volume":"C-35","author":"W.J. Gils Van","year":"1986","unstructured":"Van Gils, W.J.: A Triple Modular Redundancy Technique Providing Multiple-Bit Error Protection Without Using Extra Redundancy. IEEE Trans. Computers\u00a0C-35(7), 623\u2013631 (1986)","journal-title":"IEEE Trans. Computers"},{"key":"24_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-49519-3_3","volume-title":"Formal Methods in Computer-Aided Design","author":"M.N. Velev","year":"1998","unstructured":"Velev, M.N., Bryant, R.E.: Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 18\u201335. Springer, Heidelberg (1998)"},{"key":"24_CR31","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), pp. 397\u2013401 (June 1999)","DOI":"10.1145\/309847.309967"},{"key":"24_CR32","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":"24_CR33","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: 37 th Design Automation Conference (DAC 2000), pp. 112\u2013117 (June 2000)","DOI":"10.1145\/337292.337331"},{"key":"24_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","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, pp. 296\u2013311. Springer, Heidelberg (2000)"},{"key":"24_CR35","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)"},{"issue":"2","key":"24_CR36","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/S0747-7171(02)00091-3","volume":"35","author":"M.N. Velev","year":"2003","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), 73\u2013106 (2003)","journal-title":"Journal of Symbolic Computation (JSC)"},{"key":"24_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","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(LNAI), vol.\u00a02796, pp. 196\u2013213. Springer, Heidelberg (2003)"},{"key":"24_CR38","unstructured":"Velev, M.N.: Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-Solver When Formally Verifying Out-of-Order Processors. In: Artificial Intelligence and Mathematics (AI&MATH 2004), pp. 242\u2013254 (January 2004)"},{"key":"24_CR39","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), pp. 310\u2013315 (January 2004)","DOI":"10.1109\/ASPDAC.2004.1337587"},{"key":"24_CR40","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":"24_CR41","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 (2004)","DOI":"10.1109\/DATE.2004.1268859"},{"key":"24_CR42","unstructured":"Velev, M.N.: Encoding Global Unobservability for Efficient Translation to SAT. In: International Conference on Theory and Applications of Satisfiability Testing (May 2004)"},{"key":"24_CR43","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)","DOI":"10.1109\/ICCD.2004.1347910"},{"key":"24_CR44","doi-asserted-by":"crossref","unstructured":"Velev, M.N.: Comparison of Schemes for Encoding Unobservability in Translation to SAT. In: Asia & South Pacific Design Automation Conference (ASP-DAC 2005) (January 2005)","DOI":"10.1145\/1120725.1120823"},{"key":"24_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/11560548_10","volume-title":"Correct Hardware Design and Verification Methods","author":"M.N. Velev","year":"2005","unstructured":"Velev, M.N.: Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 97\u2013113. Springer, Heidelberg (2005)"},{"key":"24_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\u00a01(1\/2) (2005)","DOI":"10.1504\/IJES.2005.008815"},{"key":"24_CR47","doi-asserted-by":"crossref","unstructured":"Velev, M.N.: Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction. In: 7th International Symposium on Quality Electronic Design (ISQED 2006), pp. 51\u201356 (March 2006)","DOI":"10.1109\/ISQED.2006.142"},{"key":"24_CR48","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Gao, P.: Exploiting Hierarchical Encodings of Equality to Design Independent Strategies in Parallel SMT Decision Procedures for a Logic of Equality. In: IEEE High Level Design Validation and Test Workshop (HLDVT 2009) (November 2009)","DOI":"10.1109\/HLDVT.2009.5340184"},{"key":"24_CR49","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Gao, P.: A Method for Debugging of Pipelined Processors in Formal Verification by Correspondence Checking. In: 15th Asia and South Pacific Design Automation Conference (ASP-DAC 2010), pp. 619\u2013624 (January 2010)","DOI":"10.1109\/ASPDAC.2010.5419811"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16901-4_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T00:12:45Z","timestamp":1559779965000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}