{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T17:46:21Z","timestamp":1729619181569,"version":"3.28.0"},"reference-count":73,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/date.2004.1268859","type":"proceedings-article","created":{"date-parts":[[2004,5,25]],"date-time":"2004-05-25T20:11:16Z","timestamp":1085515876000},"page":"266-271","source":"Crossref","is-referenced-by-count":19,"title":["Exploiting signal unobservability for efficient translation to CNF in formal verification of microprocessors"],"prefix":"10.1109","author":[{"given":"M.N.","family":"Velev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"35","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2002.1012603"},{"key":"36","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378470"},{"key":"33","article-title":"Towards and efficient tableau method for boolean circuit satisfiability checking","author":"junttila","year":"0","journal-title":"1st International Conference on Computational Logic (CL ' 00)"},{"key":"34","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1145\/37888.37940","article-title":"dagon: technology binding and local optimization by dag matching","author":"keutzer","year":"1987","journal-title":"24th ACM\/IEEE Design Automation Conference"},{"key":"39","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-45069-6_33","article-title":"Deductive verification of advanced out-of-order microprocessors","author":"lahiri","year":"2003","journal-title":"Computer-Aided Verification (CAV ' 02"},{"journal-title":"Experience with Term Level Modeling and Verification of the MCORE Microprocessor Core","year":"2001","author":"lahiri","key":"37"},{"key":"38","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36126-X_9","article-title":"Modeling and verification of out-of-order microprocessors in uclid","author":"lahiri","year":"2002","journal-title":"Formal Methods in Computer-Aided Design (FMCAD ' 02)"},{"key":"43","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1997.643402"},{"key":"42","article-title":"Results from the sat'03 solver competition","volume":"3","author":"le berre","year":"2003","journal-title":"6th int'L Conference on Theory and Applications of Satisfiability Testing (SAT ' 03"},{"key":"41","volume":"9","author":"le berre","year":"2001","journal-title":"Exploiting the Real Power of Unit Propagation Lookahead \" Workshop on Theory and Applications of Satisfiability Testing (SAT '01)"},{"key":"40","doi-asserted-by":"publisher","DOI":"10.1109\/43.108614"},{"key":"67","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44585-4_20","article-title":"EVC: A validity checker for the logic of equality with uninterpreted functions and memories, exploiting positive equality and conservative transformations","author":"velev","year":"2001","journal-title":"Computer-Aided Verification (CAV ' 01)"},{"key":"66","first-page":"252","article-title":"Automatic abstraction of memories in the formal verification of superscalar microprocessors","author":"velev","year":"2001","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS '01)"},{"key":"69","first-page":"189","article-title":"Automatic abstraction of equations in a logic of equality","author":"velev","year":"2003","journal-title":"Automated Reasoning with Analytic Tableaux and Related Methods"},{"key":"68","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(02)00091-3"},{"journal-title":"On the Practical Value of Different Definitional Translations to Normal Form \" 13th International Conference on Automated Deduction (CADE '96)","year":"1996","author":"egly","key":"22"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_30"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2002.1012722"},{"key":"25","first-page":"244","article-title":"Bdd based procedures for a theory of equality with uninterpreted functions","author":"goel","year":"1998","journal-title":"Proc Computer-Aided Verification (CAV 98)"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2002.998262"},{"journal-title":"Personal communication","year":"2003","author":"goldberg","key":"27"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156197"},{"journal-title":"Personal communication","year":"1999","author":"hasteer","key":"29"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2002.1181983"},{"journal-title":"Solvable Cases of the Decision Problem","year":"1954","author":"ackermann","key":"2"},{"journal-title":"Digital Systems Testing and Testable Design","year":"1990","author":"abramovici","key":"1"},{"key":"7","first-page":"17","volume":"4","author":"bauer","year":"1973","journal-title":"A Note on Disjunctive Form Tautologies"},{"journal-title":"Computer Architecture A Quantitative Approach","year":"2002","author":"hennessy","key":"30"},{"key":"6","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","article-title":"Checking satisfiability of first-order formulas by incremental translation to sat","author":"barrett","year":"2002","journal-title":"Computer Aided Verification (CAV)"},{"key":"5","article-title":"Effective preprocessing with hyper-resolution and equality reduction","author":"bacchus","year":"2003","journal-title":"6th International Conference on Theory and Applications of Satisfiability Testing (SAT'03)"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2001.968669"},{"journal-title":"Second DIMACS Implementation Challenge","year":"0","author":"johnson","key":"31"},{"key":"70","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2004.1337587"},{"key":"71","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2001.972824"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90009-S"},{"key":"72","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80661-3"},{"key":"8","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45657-0_21","article-title":"Semi-formal bounded model checking","author":"bingham","year":"2002","journal-title":"Computer-Aided Verification (CAV ' 02"},{"key":"73","article-title":"Cache performance of sat solvers: A case study for efficient implementation of algorithms","volume":"3","author":"zhang","year":"2003","journal-title":"6th int'L Conference on Theory and Applications of Satisfiability Testing (SAT ' 03"},{"key":"59","article-title":"Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation","author":"velev","year":"1998","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS '98)"},{"journal-title":"A Proof System and A Decision Procedure for Equality Logic","year":"2003","author":"tveretina","key":"58"},{"journal-title":"On the Complexity of Derivation in Propositional Calculus \" in Studies in Constructive Mathematics and Mathematical Logic","year":"1983","author":"tseitin","key":"57"},{"key":"56","doi-asserted-by":"publisher","DOI":"10.1109\/MTV.2003.1250266"},{"key":"19","first-page":"21","article-title":"Experimental results on the crossover point in satisfiability problems","author":"crawford","year":"1993","journal-title":"10th National Conference on Artificial Intelligence"},{"key":"55","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775945"},{"journal-title":"Propositional Logic Deduction and Algorithms","year":"1999","author":"bu?ning","key":"17"},{"key":"18","article-title":"A failed attempt to optimize variable ordering with tools for constraints solving","volume":"2","author":"clarke","year":"2002","journal-title":"Workshop on Constraints in Formal Verification"},{"key":"15","article-title":"Automated verification of pipelined microprocessor control","author":"burch","year":"1994","journal-title":"Computer-aided Verification (CAV '94)"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1145\/240518.240623"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/371282.371364"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1145\/566385.566390"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_13"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"21","article-title":"An implementation of a theorem prover based on the connection method","volume":"84","author":"eder","year":"1985","journal-title":"Artificial Intelligence Methodology Systems Applications"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1990.129965"},{"key":"64","doi-asserted-by":"publisher","DOI":"10.1145\/337292.337331"},{"key":"65","doi-asserted-by":"crossref","DOI":"10.1007\/10722167_24","article-title":"Formal verification of vliw microprocessors with speculative execution","author":"velev","year":"0","journal-title":"Computer-Aided Verification (CAV ' 00)"},{"key":"62","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781348"},{"key":"63","first-page":"37","article-title":"Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic","author":"velev","year":"1999","journal-title":"Correct Hardware Design and Verification Methods (CHARME 99)"},{"key":"60","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1998.727081"},{"key":"61","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/3-540-49519-3_3","article-title":"Bit-level abstraction in the verification of pipelined microprocessors by correspondence checking","author":"velev","year":"1998","journal-title":"Formal Methods in Computed Aided Design (FMCAD)"},{"key":"49","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"journal-title":"Algebraic Simplification Techniques for Propositional Satisfiability \" Principles and Practice of Constraint Programming (CP '00)","year":"0","author":"marques-silva","key":"48"},{"key":"45","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775947"},{"key":"44","first-page":"342","article-title":"Look-Ahead versus look-back for satisfiability problems","author":"li","year":"1997","journal-title":"3rd International Conference on Principles and Practice of Constraint Programming (CP ' 97)"},{"key":"47","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1988.122451"},{"key":"46","doi-asserted-by":"crossref","DOI":"10.1109\/TAI.2003.1250177","article-title":"Probing-based preprocessing techniques for propositional satisfiability","author":"lynce","year":"2003","journal-title":"15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI '03"},{"key":"10","article-title":"A simplifier for propositional formulas with many binary clauses","volume":"1","author":"brafman","year":"2001","journal-title":"International Joint Conference on Artificial Intelligence (IJCAI)"},{"key":"51","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"52","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(02)93175-5"},{"key":"53","volume":"3","author":"ryan","year":"0","journal-title":"Siege SAT Solver"},{"key":"54","article-title":"The use of abservability and external don't cares for the simplification of multi-level networks","volume":"0","author":"savoj","year":"1990","journal-title":"Proc of Design Automation Conference (DAC)"},{"key":"50","first-page":"185","author":"ostrowski","year":"2002","journal-title":"Recovering and exploiting structural knowledge from cnf formulas \" principles and practice of constraint programming (cp '02)"}],"event":{"name":"Design, Automation and Test in Europe Conference and Exhibition","acronym":"DATE-04","location":"Paris, France"},"container-title":["Proceedings. Design, Automation and Test in Europe Conference and Exhibition"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8959\/28390\/01268859.pdf?arnumber=1268859","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,5,23]],"date-time":"2018-05-23T06:09:16Z","timestamp":1527055756000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1268859\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":73,"URL":"https:\/\/doi.org\/10.1109\/date.2004.1268859","relation":{},"subject":[]}}