{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T00:40:09Z","timestamp":1750984809833,"version":"3.41.0"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319703886"},{"type":"electronic","value":"9783319703893"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-70389-3_1","type":"book-chapter","created":{"date-parts":[[2017,11,11]],"date-time":"2017-11-11T14:42:30Z","timestamp":1510411350000},"page":"3-18","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Framework for Asynchronous Circuit Modeling and Verification in ACL2"],"prefix":"10.1007","author":[{"given":"Cuong","family":"Chau","sequence":"first","affiliation":[]},{"suffix":"Jr.","given":"Warren A.","family":"Hunt","sequence":"additional","affiliation":[]},{"given":"Marly","family":"Roncken","sequence":"additional","affiliation":[]},{"given":"Ivan","family":"Sutherland","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,12]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Chau, C.: Extended abstract: formal specification and verification of the FM9001 microprocessor using the DE system. In: Proceedings of the Fourteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2017), pp. 112\u2013114 (2017)","DOI":"10.4204\/EPTCS.249.8"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-12896-4_358","volume-title":"Logics of Programs","author":"E Clarke","year":"1984","unstructured":"Clarke, E., Mishra, B.: Automatic verification of asynchronous circuits. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 101\u2013115. Springer, Heidelberg (1984). https:\/\/doi.org\/10.1007\/3-540-12896-4_358"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Hunt, W.: The DE language. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, chapter 10, pp. 151\u2013166. Springer, US (2000)","DOI":"10.1007\/978-1-4757-3188-0_10"},{"key":"1_CR4","unstructured":"Hunt, W., Reeber, E.: Applications of the DE2 language. In: Proceedings of the Sixth International Workshop on Designing Correct Circuits (DCC-2006) (2006)"},{"key":"1_CR5","unstructured":"Hunt, W., Swords, S.: Use of the E language. In: Hardware Design and Functional Languages (2009)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-11512-7_17","volume-title":"Concurrency, Compositionality, and Correctness","author":"P Joshi","year":"2010","unstructured":"Joshi, P., Beerel, P.A., Roncken, M., Sutherland, I.: Timing verification of GasP asynchronous circuits: predicted delay variations observed by experiment. In: Dams, D., Hannemann, U., Steffen, M. (eds.) Concurrency, Compositionality, and Correctness. LNCS, vol. 5930, pp. 260\u2013276. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11512-7_17"},{"key":"1_CR7","unstructured":"Kaufmann, M., Moore, J.: ACL2 Home Page (2017). http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Kim, H., Beerel, P., Stevens, K.: Relative timing based verification of timed circuits and systems. In: Proceedings of the Eighth International Symposium on Asynchronous Circuits and Systems (ASYNC-2002), pp. 115\u2013124 (2002)","DOI":"10.1109\/ASYNC.2002.1000302"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Kondratyev, A., Neukom, L., Roig, O., Taubin, A., Fant, K.: Checking delay-insensitivity: $$10^4$$ gates and beyond. In: Proceedings of the Eighth International Symposium on Asynchronous Circuits and Systems (ASYNC-2002), pp. 149\u2013157 (2002)","DOI":"10.1109\/ASYNC.2002.1000305"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Myers, C.: Asynchronous Circuit Design. Wiley (2001)","DOI":"10.1002\/0471224146"},{"issue":"1","key":"1_CR11","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s11390-016-1613-y","volume":"31","author":"H Park","year":"2016","unstructured":"Park, H., He, A., Roncken, M., Song, X., Sutherland, I.: Modular Timing Constraints for Delay-Insensitive Systems. Journal of Computer Science and Technology 31(1), 77\u2013106 (2016)","journal-title":"Journal of Computer Science and Technology"},{"key":"1_CR12","unstructured":"Roncken, M., Cowan, C., Massey, B., Gilla, S., Park, H., Daasch, R., He, A., Hei, Y., Hunt, W., Song, X., Sutherland, I.: Beyond carrying coal to newcastle: dual citizen circuits. In: Mokhov, A. (ed.) This Asynchronous World: Essays dedicated to Alex Yakovlev on the Occasion of his 60th Birthday, pp. 241\u2013261. Newcastle University (2016)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Roncken, M., Gilla, S., Park, H., Jamadagni, N., Cowan, C., Sutherland, I.: Naturalized communication and testing. In: Proceedings of the Twenty First IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC-2015), pp. 77\u201384 (2015)","DOI":"10.1109\/ASYNC.2015.20"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Slobodova, A., Davis, J., Swords, S., Hunt, W.: A flexible formal verification framework for industrial scale validation. In: Proceedings of the Ninth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE-2011), pp. 89\u201397 (2011)","DOI":"10.1109\/MEMCOD.2011.5970515"},{"key":"1_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3385-3","volume-title":"Principles of Asynchronous Circuit Design - A Systems Perspective","author":"J Sparso","year":"2001","unstructured":"Sparso, J., Furber, S.: Principles of Asynchronous Circuit Design - A Systems Perspective. Springer, US (2001)"},{"key":"1_CR16","unstructured":"Srinivasan, S., Katti, R.: Desynchronization: design for verification. In: Proceedings of the Eleventh International Conference on Formal Methods in Computer-Aided Design (FMCAD-2011), pp. 215\u2013222 (2011)"},{"key":"1_CR17","unstructured":"Verbeek, F., Schmaltz, J.: Verification of building blocks for asynchronous circuits. In: Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2013), pp. 70\u201384 (2013)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Wijayasekara, V., Srinivasan, S., Smith, S.: Equivalence verification for NULL convention logic (NCL) circuits. In: Proceedings of the Thirty Second IEEE International Conference on Computer Design (ICCD-2014), pp. 195\u2013201 (2014)","DOI":"10.1109\/ICCD.2014.6974681"}],"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-319-70389-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T00:06:15Z","timestamp":1750982775000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70389-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319703886","9783319703893"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70389-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"12 November 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"HVC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa Verification Conference","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"hvc2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.research.ibm.com\/haifa\/conferences\/hvc2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}