{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T02:04:07Z","timestamp":1725501847865},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540779643"},{"type":"electronic","value":"9783540779667"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-77966-7_1","type":"book-chapter","created":{"date-parts":[[2008,2,1]],"date-time":"2008-02-01T08:59:24Z","timestamp":1201856364000},"page":"1-7","source":"Crossref","is-referenced-by-count":5,"title":["Simulation vs. Formal: Absorb What Is Useful; Reject What Is Useless"],"prefix":"10.1007","author":[{"given":"Alan J.","family":"Hu","sequence":"first","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Aharon, A., Goodman, D., Levinger, M., Lichtenstein, Y., Malka, Y., Metzger, C., Molcho, M., Shurek, G.: Test program generation for functional verification of PowerPC processors in IBM. In: 32nd Design Automation Conference, pp. 279\u2013285. ACM\/IEEE (1995)","key":"1_CR1","DOI":"10.1145\/217474.217542"},{"doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Sierawski, B.D., Sakallah, K.A.: Satometer: How much have we searched. In: 39th Design Automation Conference, pp. 737\u2013742. ACM\/IEEE (2002)","key":"1_CR2","DOI":"10.1145\/513918.514103"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2002","unstructured":"Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M., Zbar, Y.: The ForSpec temporal logic: A new temporal property-specification language. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 296\u2013311. Springer, Heidelberg (2002)"},{"unstructured":"Ball, T.: A theory of predicate-complete test coverage and generation. Technical Report MSR-TR-2004-28, Microsoft Research, (April 2004)","key":"1_CR4"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 363\u2013367. Springer, Heidelberg (2001)"},{"key":"1_CR6","volume-title":"Principles of Verifiable RTL Design: A Functional Coding Style Supporting Verification Processes in Verilog","author":"L. Bening","year":"2001","unstructured":"Bening, L., Foster, H.: Principles of Verifiable RTL Design: A Functional Coding Style Supporting Verification Processes in Verilog, 2nd edn. Kluwer Academic Publishers, Dordrecht (2001)","edition":"2"},{"key":"1_CR7","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1109\/HLDVT.2002.1224424","volume-title":"International Workshop on High-Level Design, Validation, and Test","author":"B. Bentley","year":"2002","unstructured":"Bentley, B.: High level validation of next generation microprocessors. In: International Workshop on High-Level Design, Validation, and Test, pp. 31\u201335. IEEE, Los Alamitos (2002)"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/3-540-45657-0_21","volume-title":"Computer Aided Verification","author":"J.D. Bingham","year":"2002","unstructured":"Bingham, J.D., Hu, A.J.: Semi-formal bounded model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 280\u2013294. Springer, Heidelberg (2002)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","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.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"key":"1_CR10","first-page":"488","volume-title":"International Conference on Computer Design","author":"F.S.-H. Chang","year":"2001","unstructured":"Chang, F.S.-H., Hu, A.J.: Fast specification of cycle-accurate processor models. In: International Conference on Computer Design, pp. 488\u2013492. IEEE, Los Alamitos (2001)"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/3-540-45319-9_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for temporal logic model checking. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 528\u2013542. Springer, Heidelberg (2001)"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/11817963_27","volume-title":"Computer Aided Verification","author":"F.M. Paula de","year":"2006","unstructured":"de Paula, F.M., Hu, A.J.: EverLost: A flexible platform for industrial-strength abstraction-guided simulation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 282\u2013285. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"de Paula, F.M., Hu, A.J.: An effective guidance strategy for abstraction-guided simulation. In: 44th Design Automation Conference, pp. 63\u201368. ACM\/IEEE (2007)","key":"1_CR13","DOI":"10.1109\/DAC.2007.375126"},{"unstructured":"Edelkamp, S., Lluch-Lafuente, A.: Abstraction in directed model checking. In: Workshop on Connecting Planning Theory and Practice, pp. 7\u201313 (2004)","key":"1_CR14"},{"doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Zhang, L., Ashar, P., Gupta, A., Malik, S.: Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. In: 39th Design Automation Conference, pp. 747\u2013750. ACM\/IEEE (2002)","key":"1_CR15","DOI":"10.1145\/514100.514105"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/BFb0031805","volume-title":"Formal Methods in Computer-Aided Design","author":"D. Geist","year":"1996","unstructured":"Geist, D., Farkas, M., Landver, A., Lichtenstein, Y., Ur, S., Wolfsthal, Y.: Coverage-directed test generation using symbolic techniques. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 143\u2013158. Springer, Heidelberg (1996)"},{"key":"1_CR17","first-page":"524","volume-title":"VLSID","author":"A. Gupta","year":"2002","unstructured":"Gupta, A., Casavant, A.E., Ashar, P. Liu, X.G. (Sean), Mukaiyama, A., Wakabayashi, K.: Property-specific testbench generation for guided simulation. In: 7th Asia and South Pacific Design Automation Conference and 15th International Conference on VLSI Design (VLSID), pp. 524\u2013531. IEEE, Los Alamitos (2002)"},{"unstructured":"Ho, P.-H., Shiple, T., Harer, K., Kukula, J., Damiano, R., Bertacco, V., Taylor, J., Long, J.: Smart simulation using collaborative formal and simulation engines. In: International Conference on Computer-Aided Design, pp. 120\u2013126. IEEE\/ACM (2000)","key":"1_CR18"},{"doi-asserted-by":"crossref","unstructured":"Ho, R.C., Yang, C.H., Horowitz, M.A., Dill, D.L.: Architecture validation for processors. In: International Symposium on Computer Architecture (1995)","key":"1_CR19","DOI":"10.1145\/223982.224450"},{"key":"1_CR20","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1109\/FMCAD.2007.4401979","volume-title":"Formal Methods in Computer-Aided Design","author":"F. Hutter","year":"2007","unstructured":"Hutter, F., Babi\u0107, D., Hoos, H.H., Hu, A.J.: Boosting verification by automatic tuning of decision procedures. In: Formal Methods in Computer-Aided Design, pp. 27\u201334. IEEE Computer Society Press, Los Alamitos (2007)"},{"doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., McMillan, K.L., Brayton, R.K.: Probabilistic state space search. In: International Conference on Computer-Aided Design, pp. 574\u2013579. IEEE\/ACM (1999)","key":"1_CR21","DOI":"10.1109\/ICCAD.1999.810713"},{"doi-asserted-by":"crossref","unstructured":"Nanshi, K., Somenzi, F.: Guiding simulation with increasingly refined abstract traces. In: 43rd Design Automation Conference, pp. 737\u2013742. ACM\/IEEE (2006)","key":"1_CR22","DOI":"10.1145\/1146909.1147097"},{"key":"1_CR23","first-page":"409","volume-title":"International Conference on Computer Design","author":"K. Ng","year":"2004","unstructured":"Ng, K., Hu, A.J., Yang, J.: Generating monitor circuits for simulation-friendly GSTE assertion graphs. In: International Conference on Computer Design, pp. 409\u2013416. IEEE Computer Society Press, Los Alamitos (2004)"},{"doi-asserted-by":"crossref","unstructured":"Oliveira, M.T., Hu, A.J.: High-level specification and automatic generation of IP interface monitors. In: 39th Design Automation Conference, pp. 129\u2013134. ACM\/IEEE (2002)","key":"1_CR24","DOI":"10.1145\/513950.513952"},{"doi-asserted-by":"crossref","unstructured":"Ravi, K., Somenzi, F.: High-density reachability analysis. In: International Conference on Computer-Aided Design, pp. 154\u2013158. IEEE\/ACM (1995)","key":"1_CR25","DOI":"10.1109\/ICCAD.1995.480006"},{"doi-asserted-by":"crossref","unstructured":"Shyam, S., Bertacco, V.: Distance-guided hybrid verification with GUIDO. In: Design Automation and Test in Europe, pp. 1211\u20131216 (2006)","key":"1_CR26","DOI":"10.1109\/DATE.2006.244050"},{"unstructured":"Yang, C.H., Dill, D.L.: SpotLight: Best-first search of FSM state space. In: IEEE International High-Level Design Validation and Test Workshops (HLDVT) (1996)","key":"1_CR27"},{"doi-asserted-by":"crossref","unstructured":"Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: 35th Design Automation Conference, pp. 599\u2013604. ACM\/IEEE (1998)","key":"1_CR28","DOI":"10.1145\/277044.277201"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1007\/3-540-63166-6_37","volume-title":"Computer Aided Verification","author":"J. Yuan","year":"1997","unstructured":"Yuan, J., Shen, J., Abraham, J., Aziz, A.: On combining formal and informal verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 376\u2013387. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77966-7_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:57:21Z","timestamp":1619521041000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77966-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540779643","9783540779667"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77966-7_1","relation":{},"subject":[]}}