{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:07:07Z","timestamp":1761620827372,"version":"3.30.2"},"reference-count":87,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":3819,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[2003,2]]},"DOI":"10.1016\/s0747-7171(02)00091-3","type":"journal-article","created":{"date-parts":[[2003,2,12]],"date-time":"2003-02-12T07:46:23Z","timestamp":1045035983000},"page":"73-106","source":"Crossref","is-referenced-by-count":58,"title":["Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors"],"prefix":"10.1016","volume":"35","author":[{"given":"Miroslav N","family":"Velev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Randal E","family":"Bryant","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"year":"1954","series-title":"Solvable Cases of the Decision Problem","author":"Ackermann","key":"10.1016\/S0747-7171(02)00091-3_B1"},{"key":"10.1016\/S0747-7171(02)00091-3_B2","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Markov, I.L., Sakallah, K.A., 2001. Faster SAT and smaller BDDs via common function structure. International Conference on Computer-aided Design (ICCAD\u201901). pp. 443\u2013448","DOI":"10.1109\/ICCAD.2001.968669"},{"key":"10.1016\/S0747-7171(02)00091-3_B3","doi-asserted-by":"crossref","unstructured":"Baptista, L., Marques-Silva, J.P., 2000. Using randomization and learning to solve hard real-world instances of satisfiability. Principles and Practice of Constraint Programming (CP\u201900). Available from: http:\/\/sat.inesc.pt\/~jpms","DOI":"10.1007\/3-540-45349-0_36"},{"key":"10.1016\/S0747-7171(02)00091-3_B4","unstructured":"Bayardo, R.J., Schrag, R., 1997. Using CSP look-back techniques to solve real world SAT instances. 14th National Conference on Artificial Intelligence (AAAI\u201997). pp. 203\u2013208"},{"key":"10.1016\/S0747-7171(02)00091-3_B5","doi-asserted-by":"crossref","unstructured":"Bentley, B., 2001. Validating the Intel\u00ae Pentium\u00ae 4 microprocessor. 38th Design Automation Conference (DAC\u201901). pp. 244\u2013248","DOI":"10.1145\/378239.378473"},{"key":"10.1016\/S0747-7171(02)00091-3_B6","first-page":"454","article-title":"Finding bugs in an alpha microprocessor using satisfiability solvers","volume":"vol. 2102","author":"Bjesse","year":"2001"},{"key":"10.1016\/S0747-7171(02)00091-3_B7","unstructured":"Brafman, R.I., 2001. A simplifier for propositional formulas with many binary clauses. International Joint Conference on Artificial Intelligence (IJCAI\u201901). pp. 515\u2013520"},{"key":"10.1016\/S0747-7171(02)00091-3_B8","doi-asserted-by":"crossref","unstructured":"Brglez, F., Bryan, D., Kozminski, K., 1989. Combinational profiles of sequential benchmark circuits. International Symposium on Circuits and Systems (ISCAS\u201989). Available from: http:\/\/cb1.ncsu.edu\/benchmarks","DOI":"10.1109\/ISCAS.1989.100747"},{"key":"10.1016\/S0747-7171(02)00091-3_B9","unstructured":"Brglez, F., Fujiwara, H., 1985. A neutral netlist of 10 combinational benchmark circuits. International Symposium on Circuits and Systems (ISCAS\u201985). Available from: http:\/\/cb1.ncsu.edu\/benchmarks"},{"key":"10.1016\/S0747-7171(02)00091-3_B10","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for Boolean function manipulation","volume":"C-35","author":"Bryant","year":"1986","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/S0747-7171(02)00091-3_B11","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","article-title":"Symbolic Boolean manipulation with ordered binary-decision diagrams","volume":"24","author":"Bryant","year":"1992","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/S0747-7171(02)00091-3_B12","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/371282.371364","article-title":"Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic","volume":"2","author":"Bryant","year":"2001","journal-title":"ACM Trans. Comput. Logic (TOCL)"},{"key":"10.1016\/S0747-7171(02)00091-3_B13","doi-asserted-by":"crossref","DOI":"10.1145\/566385.566390","article-title":"Boolean satisfiability with transitivity constraints","volume":"3","author":"Bryant","year":"2002","journal-title":"ACM Trans. Comput. Logic (TOCL)"},{"key":"10.1016\/S0747-7171(02)00091-3_B14","doi-asserted-by":"crossref","unstructured":"Burch, J.R., 1996. Techniques for verifying superscalar microprocessor. 33rd Design Automation Conference (DAC\u201996). pp. 552\u2013557","DOI":"10.1145\/240518.240623"},{"key":"10.1016\/S0747-7171(02)00091-3_B15","first-page":"68","article-title":"Automated verification of pipelined microprocessor control","volume":"vol. 818","author":"Burch","year":"1994"},{"key":"10.1016\/S0747-7171(02)00091-3_B16","doi-asserted-by":"crossref","unstructured":"Chatalic, P., Simon, L., 2000. Multi-resolution on compressed sets of clauses. 12th International Conference on Tools with Artificial Intelligence (ICTAI\u201900). pp. 2\u201310","DOI":"10.1109\/TAI.2000.889839"},{"key":"10.1016\/S0747-7171(02)00091-3_B17","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","article-title":"Bounded model checking using satisfiability solving","volume":"19","author":"Clarke","year":"2001","journal-title":"J. Formal Methods Syst. Design (FMSD)"},{"key":"10.1016\/S0747-7171(02)00091-3_B18","first-page":"436","article-title":"Benefits of bounded model checking at an industrial setting","volume":"vol. 2102","author":"Copty","year":"2001"},{"key":"10.1016\/S0747-7171(02)00091-3_B19","doi-asserted-by":"crossref","unstructured":"Crawford, J.M., Auton, L.D., 1996. Experimental results on the crossover point in random 3SAT, In: Hogg T., Huberman B.A., Williams C. (Eds.), Frontiers in Problem Solving: Phase Transitions and Complexity, Artificial Intelligence 81, pp. 31\u201357","DOI":"10.1016\/0004-3702(95)00046-1"},{"key":"10.1016\/S0747-7171(02)00091-3_B20","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem proving","volume":"5","author":"Davis","year":"1962","journal-title":"Commun. ACM"},{"key":"10.1016\/S0747-7171(02)00091-3_B21","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","article-title":"A computing procedure for quantification theory","volume":"7","author":"Davis","year":"1960","journal-title":"J. ACM"},{"key":"10.1016\/S0747-7171(02)00091-3_B22","unstructured":"Dubois, O., Andre, P., Boufkhad, Y., Carlier, J., 1993. Can a very simple algorithm be efficient for SAT? In: Johnson D.S., Trick M.A. (Eds.), The Second DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science. Available from: ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/satisfiability\/contributed\/dubois"},{"key":"10.1016\/S0747-7171(02)00091-3_B23","unstructured":"Freeman, J.W., 1995. Improvements to Propositional Satisfiability Search Algorithms, Ph.D. Thesis, Department of Computer and Information Science, University of Pennsylvania"},{"key":"10.1016\/S0747-7171(02)00091-3_B24","first-page":"244","article-title":"BDD based procedures for a theory of equality with uninterpreted functions","volume":"vol. 1427","author":"Goel","year":"1998"},{"key":"10.1016\/S0747-7171(02)00091-3_B25","unstructured":"Goldberg, E., 2002. Personal communication"},{"key":"10.1016\/S0747-7171(02)00091-3_B26","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y., 2002. BerkMin: a fast and robust sat-solver. Design, Automation, and Test in Europe (DATE\u201902). pp. 142\u2013149","DOI":"10.1109\/DATE.2002.998262"},{"key":"10.1016\/S0747-7171(02)00091-3_B27","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1023\/A:1006314320276","article-title":"Heavy-tailed phenomena in satisfiability and constraint satisfaction problems","volume":"24","author":"Gomes","year":"2000","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/S0747-7171(02)00091-3_B28","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1023\/A:1006366304347","article-title":"The propositional formula checker Heer-Hugo","volume":"24","author":"Groote","year":"2000","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/S0747-7171(02)00091-3_B29","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1023\/A:1008355411566","article-title":"New techniques for deterministic test pattern generation","volume":"15","author":"Hamzaoglu","year":"1999","journal-title":"J. Electron. Test., Theory Appl."},{"key":"10.1016\/S0747-7171(02)00091-3_B30","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/s100090100052","article-title":"Design of experiments and evaluation of BDD ordering heuristics","volume":"3","author":"Harlow","year":"2001","journal-title":"Int. J. Softw. Tools Technology Transfer (STTT)"},{"year":"2002","series-title":"Computer Architecture: A Quantitative Approach","author":"Hennessy","key":"10.1016\/S0747-7171(02)00091-3_B31"},{"key":"10.1016\/S0747-7171(02)00091-3_B32","doi-asserted-by":"crossref","unstructured":"Hirsch, E.A., Kojevnikov, A., 2001. Solving Boolean satisfiability using local search guided by unit clause elimination. Principles and Practice of Constraint Programming (CP\u201901). pp. 605\u2013609","DOI":"10.1007\/3-540-45578-7_48"},{"key":"10.1016\/S0747-7171(02)00091-3_B33","unstructured":"Hoos, H.H., 1999. SAT-encodings, search space structure, and local search performance. International Joint Conference on Artificial Intelligence (IJCAI\u201999). pp. 296\u2013302"},{"key":"10.1016\/S0747-7171(02)00091-3_B34","unstructured":"Intel Corporation, 1999. IA-64 application developer\u2019s architecture guide. Available from: http:\/\/developer.intel.com\/design\/ia-64\/architecture.htm"},{"key":"10.1016\/S0747-7171(02)00091-3_B35","series-title":"Information Processing 92, vol. 1, Algorithms, Software, Architecture","first-page":"322","article-title":"Random generation of satisfiable and unsatisfiable CNF predicates","author":"Iwama","year":"1992"},{"key":"10.1016\/S0747-7171(02)00091-3_B36","doi-asserted-by":"crossref","unstructured":"Iwama, K., Hino, K., 1994. Random generation of test instances for logic optimizers. 31st Design Automation Conference (DAC\u201994) pp. 430\u2013434","DOI":"10.1145\/196244.196452"},{"key":"10.1016\/S0747-7171(02)00091-3_B37","unstructured":"Janssen, G., 2001. Design of a pointerless BDD package. 10th International Workshop on Logic & Synthesis (IWLS\u201901)"},{"journal-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","year":"1993","key":"10.1016\/S0747-7171(02)00091-3_B38"},{"year":"2002","series-title":"Symbolic Simulation Methods for Industrial Formal Verification","author":"Jones","key":"10.1016\/S0747-7171(02)00091-3_B39"},{"key":"10.1016\/S0747-7171(02)00091-3_B40","doi-asserted-by":"crossref","unstructured":"Kalla, P., Zeng, Z., Ciesielski, M.J., Huang, C., 2000. A BDD-based satisfiability infrastructure using the unate recursive paradigm. Design, Automation and Test in Europe (DATE\u201900). pp. 232\u2013236","DOI":"10.1109\/DATE.2000.840044"},{"key":"10.1016\/S0747-7171(02)00091-3_B41","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1109\/43.108614","article-title":"Test pattern generation using Boolean satisfiability","volume":"11","author":"Larrabee","year":"1992","journal-title":"IEEE Trans. Comput.-aided Des. Integr. Circuits Syst."},{"key":"10.1016\/S0747-7171(02)00091-3_B42","unstructured":"Li, C.M., 2000. Integrating equivalency reasoning into Davis\u2013Putnam procedure. 17th National Conference on Artificial Intelligence (AAAI\u201900). pp. 291\u2013296"},{"key":"10.1016\/S0747-7171(02)00091-3_B43","unstructured":"Li, C.M., Anbulagan, 1997. Heuristics based on unit propagation for satisfiability problems. International Joint Conference on Artificial Intelligence (IJCAI\u201997). pp. 366\u2013371"},{"key":"10.1016\/S0747-7171(02)00091-3_B44","doi-asserted-by":"crossref","unstructured":"Lynce, I., Baptista, L., Marques-Silva, J.P., 2001. Stochastic systematic search algorithms for satisfiability. LICS Workshop on Theory and Applications of Satisfiability Testing (LICS-SAT)","DOI":"10.1016\/S1571-0653(04)00322-1"},{"key":"10.1016\/S0747-7171(02)00091-3_B45","doi-asserted-by":"crossref","unstructured":"Malik, S., Wang, A.R., Brayton, R.K., Sangiovani-Vincentelli, A., 1988. Logic verification using binary decision diagrams in a logic synthesis environment. International Conference on Computer-aided Design (ICCAD\u201988). pp. 6\u20139","DOI":"10.1109\/ICCAD.1988.122451"},{"key":"10.1016\/S0747-7171(02)00091-3_B46","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., 1999. The impact of branching heuristics in propositional satisfiability algorithms. 9th Portuguese Conference on Artificial Intelligence (EPIA). Available from: http:\/\/sat.inesc.pt\/~jpms","DOI":"10.1007\/3-540-48159-1_5"},{"key":"10.1016\/S0747-7171(02)00091-3_B47","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., 2000. Algebraic simplification techniques for propositional satisfiability. Principles and Practice of Constraint Programming (CP\u201900). pp. 537\u2013542. Available from: http:\/\/sat.inesc.pt\/~jpms","DOI":"10.1007\/3-540-45349-0_45"},{"key":"10.1016\/S0747-7171(02)00091-3_B48","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., e Silva, L.G., 1999. Algorithms for satisfiability in combinational circuits based on backtrack search and recursive learning. 12th Symposium on Integrated Circuits and Systems Design (SBCCI\u201999). pp. 192\u2013195. Available from: http:\/\/sat.inesc.pt\/~jpms","DOI":"10.1109\/SBCCI.1999.803118"},{"key":"10.1016\/S0747-7171(02)00091-3_B49","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","article-title":"GRASP: a search algorithm for propositional satisfiability","volume":"48","author":"Marques-Silva","year":"1999","journal-title":"IEEE Trans. Comput."},{"year":"1996","series-title":"Binary Decision Diagrams and Applications for VLSI CAD","author":"Minato","key":"10.1016\/S0747-7171(02)00091-3_B50"},{"key":"10.1016\/S0747-7171(02)00091-3_B51","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/s100090100038","article-title":"Zero-suppressed BDDs and their applications","volume":"3","author":"Minato","year":"2001","journal-title":"Int. J. Softw. Tools Technology Transfer (STTT)"},{"key":"10.1016\/S0747-7171(02)00091-3_B52","unstructured":"Mitchell, D., Selman, B., Levesque, H., 1992. Hard and easy distributions of SAT problems. 10th National Conference on Artificial Intelligence (AAAI\u201992). pp. 459\u2013465"},{"key":"10.1016\/S0747-7171(02)00091-3_B53","unstructured":"Moskewicz, M.W., 2001. Personal communication"},{"key":"10.1016\/S0747-7171(02)00091-3_B54","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S., 2001. Engineering a highly efficient SAT solver. 38th Design Automation Conference (DAC\u201901). pp. 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"10.1016\/S0747-7171(02)00091-3_B55","doi-asserted-by":"crossref","unstructured":"Pilarski, S., Hu, G., 2002. SAT with partial clauses and back-leaps. 39th Design Automation Conference (DAC\u201902). pp. 743\u2013746","DOI":"10.1145\/513918.514104"},{"key":"10.1016\/S0747-7171(02)00091-3_B56","unstructured":"Plaisted, D.A., Biere, A., Zhu, Y., 2002. A satisfiability procedure for quantified Boolean formulae, In: Hammer P. (Ed.), Discrete Applied Mathematics, Renesse Special Issue Devoted to the International Symposium on Theory and Applications of Satisfiability Testing (SAT\u201900)"},{"key":"10.1016\/S0747-7171(02)00091-3_B57","first-page":"455","article-title":"Deciding equality formulas by small-domain instantiations","volume":"vol. 1633","author":"Pnueli","year":"1999"},{"key":"10.1016\/S0747-7171(02)00091-3_B58","unstructured":"Prestwich, S.D., 2000. Stochastic local search in constrained spaces. Practical Application of Constraint Technology and Logic Programming (PACLP\u201900). pp. 27\u201339"},{"key":"10.1016\/S0747-7171(02)00091-3_B59","unstructured":"Rintanen, J., 1999. Improvements to the evaluation of quantified Boolean formulae. International Joint Conference on Artificial Intelligence (IJCAI\u201999). pp. 1192\u20131197"},{"key":"10.1016\/S0747-7171(02)00091-3_B60","doi-asserted-by":"crossref","unstructured":"Rudell, R., 1993. Dynamic variable ordering for ordered binary decision diagrams. International Conference on Computer-aided Design (ICCAD\u201993). pp. 42\u201347","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"10.1016\/S0747-7171(02)00091-3_B61","unstructured":"Selman, B., Kautz, H., 1993. Domain-independent extensions to GSAT: solving large structured satisfiability problems. International Joint Conference on Artificial Intelligence (IJCAI\u201993). pp. 290\u2013295"},{"key":"10.1016\/S0747-7171(02)00091-3_B62","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1090\/dimacs\/026\/25","article-title":"Local search strategies for satisfiability testing","volume":"26","author":"Selman","year":"1996","journal-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science"},{"key":"10.1016\/S0747-7171(02)00091-3_B63","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1023\/A:1008287028851","article-title":"A discrete Lagrangian-based global-search method for solving satisfiability problems","volume":"12","author":"Shang","year":"1998","journal-title":"J. Global Optimization"},{"issue":"5","key":"10.1016\/S0747-7171(02)00091-3_B64","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1109\/40.877948","article-title":"Itanium processor microarchitecture","volume":"20","author":"Sharangpani","year":"2000","journal-title":"IEEE Micro"},{"key":"10.1016\/S0747-7171(02)00091-3_B65","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/s100090100042","article-title":"Efficient manipulation of decision diagrams","volume":"3","author":"Somenzi","year":"2001","journal-title":"Int. J. Softw. Tools Technology Transfer (STTT)"},{"key":"10.1016\/S0747-7171(02)00091-3_B66","unstructured":"St\u00e5lmarck, G., 1989. A System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula, Swedish Patent No. 467076 (approved 1992), U.S. Patent No. 5276897 (1994), European Patent No. 0403454 (1995)"},{"key":"10.1016\/S0747-7171(02)00091-3_B67","doi-asserted-by":"crossref","first-page":"907","DOI":"10.1109\/43.856977","article-title":"GRAINE\u2014an implication GRaph-bAsed engINE for fast implication, justification and propagation","volume":"19","author":"Tafertshofer","year":"2000","journal-title":"IEEE Trans. CAD"},{"key":"10.1016\/S0747-7171(02)00091-3_B68","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/332833.332837","article-title":"Proactive computing","volume":"43","author":"Tennenhouse","year":"2000","journal-title":"Commun. ACM"},{"key":"10.1016\/S0747-7171(02)00091-3_B69","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1145\/296333.296347","article-title":"High-level design verification of microprocessors via error modeling","volume":"3","author":"Van Campenhout","year":"1998","journal-title":"ACM Trans. Des. Autom. Electronic Syst."},{"key":"10.1016\/S0747-7171(02)00091-3_B70","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1109\/54.895006","article-title":"Collection and analysis of microprocessor design errors","volume":"17","author":"Van Campenhout","year":"2000","journal-title":"IEEE Des. Test Comput."},{"key":"10.1016\/S0747-7171(02)00091-3_B71","unstructured":"Velev, M.N., 1999. Benchmark suites, SSS. 1.0, SSS. 1.0a. Available from: http:\/\/www.ece.cmu.edu\/~mvelev"},{"key":"10.1016\/S0747-7171(02)00091-3_B72","doi-asserted-by":"crossref","unstructured":"Velev, M.N., 2000a. Formal verification of VLIW microprocessors with speculative execution. In: Emerson, E.A., Sistla, A.P. (Eds.), Computer-aided Verification (CAV'00), LNCS, vol. 1855. Springer, pp. 296\u2013311. Available from: http:\/\/www.ece.cmu.edu\/~mvelev","DOI":"10.1007\/10722167_24"},{"key":"10.1016\/S0747-7171(02)00091-3_B73","unstructured":"Velev, M.N., 2000b. Benchmark suites SSS-SAT. 1.0, VLIW-SAT. 1.0, FVP-UNSAT. 1.0, and FVP-UNSAT. 2.0. Available from: http:\/\/www.ece.cmu.edu\/~mvelev"},{"key":"10.1016\/S0747-7171(02)00091-3_B74","first-page":"252","article-title":"Automatic abstraction of memories in the formal verification of superscalar microprocessors","volume":"vol. 2031","author":"Velev","year":"2001"},{"key":"10.1016\/S0747-7171(02)00091-3_B75","unstructured":"Velev, M.N., 2002. Benchmark suite NPE-1.0. Available from: http:\/\/www\/ece\/cmu.edu\/~mvelev"},{"key":"10.1016\/S0747-7171(02)00091-3_B76","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E., 1998a. Incorporating timing constraints in the efficient memory model for symbolic ternary simulation. International Conference on Computer Design (ICCD\u201998). pp. 400\u2013406. Available from: http:\/\/www.ece.cmu.edu\/~mvelev","DOI":"10.1109\/ICCD.1998.727081"},{"key":"10.1016\/S0747-7171(02)00091-3_B77","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E., 1998b. Bit-level abstraction in the verification of pipelined microprocessors by correspondence checking. In: Gopalakrishnan, G., Windley, P. (Eds.), Formal Methods in Computer-aided Design (FMCAD\u201998), LNCS, vol. 1522. Springer, pp. 18\u201335. Available from: http:\/\/www.ece.cmu.edu\/~mvelev","DOI":"10.1007\/3-540-49519-3_3"},{"key":"10.1016\/S0747-7171(02)00091-3_B78","first-page":"37","article-title":"Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic","volume":"vol. 1703","author":"Velev","year":"1999"},{"key":"10.1016\/S0747-7171(02)00091-3_B79","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E., 2000. Formal verification of superscalar microprocessors with multicycle functional units, exceptions, and branch prediction. 37th Design Automation Conference (DAC\u201900). pp. 112\u2013117. Available from: http:\/\/www.ece.cmu.edu\/~mvelev","DOI":"10.1145\/337292.337331"},{"key":"10.1016\/S0747-7171(02)00091-3_B80","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E., 2001a. Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. 38th Design Automation Conference (DAC\u201901). pp. 226\u2013231. Available from: http:\/\/www.ece.cmu.edu\/~mvelev","DOI":"10.1145\/378239.378469"},{"key":"10.1016\/S0747-7171(02)00091-3_B81","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E., 2001b. EVC: a validity checker for the logic of equality with uninterpreted functions and memories, exploiting positive equality and conservative transformations. In: Berry, G., Comon, H., Finkel, A. (Eds.), Computer-aided Verification (CAV\u201901), LNCS, vol. 2102. Springer, pp. 235\u2013240. Available from: http:\/\/www.ece.cmu.edu\/~mvelev","DOI":"10.1007\/3-540-44585-4_20"},{"key":"10.1016\/S0747-7171(02)00091-3_B82","doi-asserted-by":"crossref","unstructured":"Wang, D., Clarke, E., Zhu, Y., Kukula, J., 2001. Using cutwidth to improve symbolic simulation and Boolean satisfiability. IEEE International High Level Design Validation and Test Workshop (LDVT\u201901)","DOI":"10.1109\/HLDVT.2001.972824"},{"key":"10.1016\/S0747-7171(02)00091-3_B83","unstructured":"Williams, P.F., 2000. Formal Verification Based on Boolean Expression Diagrams. Ph.D. Thesis. Department of Information Technology, Technical University of Denmark, Lyngby, Denmark. Available from: http:\/\/www.it-c.dk\/research\/bed"},{"key":"10.1016\/S0747-7171(02)00091-3_B84","first-page":"124","article-title":"Combining decision diagrams and SAT procedures for efficient symbolic model checking","volume":"vol. 1855","author":"Williams","year":"2000"},{"key":"10.1016\/S0747-7171(02)00091-3_B85","unstructured":"Wu, Z., Wah, B.W., 1999. Solving hard satisfiability problems: a unified algorithm based on discrete Lagrange multipliers. 11th IEEE International Conference on Tools with Artificial Intelligence (ICTAI\u201999). pp. 210\u2013217. Available from: http:\/\/manip.crhc.uiuc.edu"},{"key":"10.1016\/S0747-7171(02)00091-3_B86","first-page":"272","article-title":"SATO: an efficient propositional prover","volume":"vol. 1249","author":"Zhang","year":"1997"},{"key":"10.1016\/S0747-7171(02)00091-3_B87","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S., 2001. Efficient conflict driven learning in a Boolean satisfiability solver. International Conference on Computer-aided Design (ICCAD\u201901). pp. 279\u2013285"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717102000913?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717102000913?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,11]],"date-time":"2024-12-11T18:19:34Z","timestamp":1733941174000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717102000913"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,2]]},"references-count":87,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,2]]}},"alternative-id":["S0747717102000913"],"URL":"https:\/\/doi.org\/10.1016\/s0747-7171(02)00091-3","relation":{},"ISSN":["0747-7171"],"issn-type":[{"type":"print","value":"0747-7171"}],"subject":[],"published":{"date-parts":[[2003,2]]}}}