{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T04:13:58Z","timestamp":1742789638164,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642287558"},{"type":"electronic","value":"9783642287565"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28756-5_26","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:57:15Z","timestamp":1332449835000},"page":"377-391","source":"Crossref","is-referenced-by-count":5,"title":["QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification"],"prefix":"10.1007","author":[{"given":"Hu-Hsi","family":"Yeh","sequence":"first","affiliation":[]},{"given":"Cheng-Yin","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Chung-Yang","family":"Huang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"SIS, http:\/\/embedded.eecs.berkeley.edu\/pubs\/downloads\/sis\/index.html"},{"key":"26_CR2","unstructured":"VIS, http:\/\/vlsi.colorado.edu\/~vis\/"},{"key":"26_CR3","unstructured":"MVSIS, http:\/\/embedded.eecs.berkeley.edu\/Respep\/Research\/mvsis\/"},{"key":"26_CR4","unstructured":"Berkeley ABC, http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"26_CR5","unstructured":"Icarus Verilog, http:\/\/iverilog.icarus.com\/"},{"key":"26_CR6","unstructured":"MiniSAT, http:\/\/minisat.se\/"},{"key":"26_CR7","unstructured":"Boolector, http:\/\/fmv.jku.at\/boolector\/"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Yeh, H.-H., Huang, C.-Y.: Automatic Constraint Generation for Guided Random Simulation. In: Asia and South Pacific Design Automation Conference, pp. 613\u2013618 (2010)","DOI":"10.1109\/ASPDAC.2010.5419814"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Kitchen, N., Kuehlmann, A.: Stimulus generation forconstrained random simulation. In: International Conference on Computer-Aided Design, pp. 258\u2013265 (2007)","DOI":"10.1109\/ICCAD.2007.4397275"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Wu, B.-H., Yang, C.-J., Tso, C.-C., Huang, C.-Y.: Toward an Extremely-High-Throughput and Even-Distribution Pattern Generator for the Constrained Random Simulation Techniques. In: International Conference on Computer-Aided Design, pp. 602\u2013607 (2011)","DOI":"10.1109\/ICCAD.2011.6105392"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Yeh, H.-H., Wu, C.-Y., Huang, C.-Y.: Property-Specific Sequential Invariant Extraction for SAT-based Unbounded Model Checking. In: International Conference on Computer-Aided Design, pp. 674\u2013678 (2011)","DOI":"10.1109\/ICCAD.2011.6105402"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Thalmaier, M., Nguyen, M.D., Wedler, M., Stoffel, D., Bormann, J., Kunz, W.: Analyzing k-step induction to compute invariants for SAT-based property checking. In: Design Automation Conference, pp. 176\u2013181 (2010)","DOI":"10.1145\/1837274.1837319"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Vizel, Y., Grumberg, O.: Interpolation-Sequence Based Model Checking. In: Formal Methods in Computer Aided Design, pp. 1\u20138 (2009)","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"26_CR15","unstructured":"Een, N., Mishchenko, A., Brayton, R.: Efficient Implementation of Property Directed Reachability. In: Formal Methods in Computer Aided Design, pp. 125\u2013134 (2011)"},{"key":"26_CR16","unstructured":"Liu, C.-N., Jou, J.-Y.: A FSM Extractor from HDL Description at RTL Level. In: Asia Pacific Conference on Hardware Description Languages, pp. 33\u201338 (1998)"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Touati, H., Savoj, H., Lin, B., Brayton, R.K., Sangiovanni-Vincentelli, A.: Implicit State Enumeration of Finite State Machines using BDDs. In: International Conference on Computer-Aided Design, pp. 130\u2013133 (1990)","DOI":"10.1109\/ICCAD.1990.129860"},{"key":"26_CR18","unstructured":"OpenCores, http:\/\/www.opencores.org"},{"key":"26_CR19","unstructured":"Cadence Conformal LEC, http:\/\/www.cadence.com\/products\/"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28756-5_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T18:53:44Z","timestamp":1742756024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28756-5_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287558","9783642287565"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28756-5_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}