{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T19:32:05Z","timestamp":1725910325626},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319671031"},{"type":"electronic","value":"9783319671048"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/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-67104-8_6","type":"book-chapter","created":{"date-parts":[[2017,8,31]],"date-time":"2017-08-31T07:14:14Z","timestamp":1504163654000},"page":"108-129","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Improving the Efficiency of Formal Verification: The Case of Clock-Domain Crossings"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Plassan","sequence":"first","affiliation":[]},{"given":"Hans-J\u00f6rg","family":"Peter","sequence":"additional","affiliation":[]},{"given":"Katell","family":"Morin-Allory","sequence":"additional","affiliation":[]},{"given":"Shaker","family":"Sarwary","sequence":"additional","affiliation":[]},{"given":"Dominique","family":"Borrione","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,1]]},"reference":[{"key":"6_CR1","series-title":"IFIP \u2013 The International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-0-387-09661-2_6","volume-title":"Distributed Embedded Systems: Design, Middleware and Resources","author":"E Alkassar","year":"2008","unstructured":"Alkassar, E., B\u00f6hm, P., Knapp, S.: Formal correctness of an automotive bus controller implementation at gate-level. In: Kleinjohann, B., Wolf, W., Kleinjohann, L. (eds.) DIPES 2008. ITIFIP, vol. 271, pp. 57\u201367. Springer, Boston, MA (2008). doi:10.1007\/978-0-387-09661-2_6"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: Refinement strategies for verification methods based on datapath abstraction. In: ASP-DAC, pp. 19\u201324 (2006)","DOI":"10.1145\/1118299.1118306"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Andraus, Z.S., Sakallah, K.A.: Automatic abstraction and verification of Verilog models. In: Design Automation Conference (DAC), pp. 218\u2013223 (2004)","DOI":"10.1145\/996566.996629"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). doi:10.1007\/3-540-49059-0_14"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14295-6_5"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Burns, F., Sokolov, D., Yakovlev, A.: GALS synthesis and verification for xMAS models. In: DATE (2015)","DOI":"10.7873\/DATE.2015.0063"},{"issue":"4","key":"6_CR7","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1109\/T-C.1973.223730","volume":"C\u201322","author":"T Chaney","year":"1973","unstructured":"Chaney, T., Molnar, C.: Anomalous behavior of synchronizer and arbiter circuits. IEEE Trans. Comput. C\u201322(4), 421\u2013422 (1973)","journal-title":"IEEE Trans. Comput."},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). doi:10.1007\/10722167_15"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Long, D.E.: Model checking and abstraction. In: ACM (1991)","DOI":"10.1145\/143165.143235"},{"key":"6_CR10","unstructured":"Cummings, C.E.: Clock domain crossing design & verification techniques using systemverilog. In: SNUG, Boston (2008)"},{"key":"6_CR11","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: FMCAD, pp. 125\u2013134 (2011)"},{"key":"6_CR12","unstructured":"Gabara, T.J., Cyr, G.J., Stroud, C.E.: Metastability of CMOS master\/slave flip-flops. In: IEEE Custom Integrated Circuits Conference. pp. 29.4\/1\u201329.4\/6, May 1991"},{"key":"6_CR13","unstructured":"Ginosar, R.: Fourteen ways to fool your synchronizer. In: Asynchronous Circuits and Systems, pp. 89\u201396 (2003)"},{"issue":"5","key":"6_CR14","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1109\/MDT.2011.113","volume":"28","author":"R Ginosar","year":"2011","unstructured":"Ginosar, R.: Metastability and synchronizers: a tutorial. IEEE Des. Test Comput. 28(5), 23\u201335 (2011)","journal-title":"IEEE Des. Test Comput."},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/11560548_31","volume-title":"Correct Hardware Design and Verification Methods","author":"T Kapschitz","year":"2005","unstructured":"Kapschitz, T., Ginosar, R.: Formal verification of synchronizers. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 359\u2013362. Springer, Heidelberg (2005). doi:10.1007\/11560548_31"},{"issue":"9","key":"6_CR16","doi-asserted-by":"publisher","first-page":"1395","DOI":"10.1109\/TCAD.2013.2255127","volume":"32","author":"N Karimi","year":"2013","unstructured":"Karimi, N., Chakrabarty, K.: Detection, diagnosis, and recovery from clock-domain crossing failures in multiclock SoCs. Comput. Aided Des. Integr. Circuits Syst. 32(9), 1395\u20131408 (2013)","journal-title":"Comput. Aided Des. Integr. Circuits Syst."},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Kebaili, M., Brignone, J.C., Morin-Allory, K.: Clock domain crossing formal verification: a meta-model. In: IEEE International High Level Design Validation and Test Workshop (HLDVT), pp. 136\u2013141, October 2016","DOI":"10.1109\/HLDVT.2016.7748267"},{"key":"6_CR18","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"RP Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)"},{"key":"6_CR19","unstructured":"Kwok, C., Gupta, V., Ly, T.: Using assertion-based verification to verify clock domain crossing signals. In: Design and Verification Conference, pp. 654\u2013659 (2003)"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Leong, C., Machado, P., et al.: Built-in clock domain crossing (CDC) test and diagnosis in GALS systems. In: Proceedings of the DDECS 2010, pp. 72\u201377, April 2010","DOI":"10.1109\/DDECS.2010.5491815"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Li, B., Kwok, C.K.: Automatic formal verification of clock domain crossing signals. In: ASP-DAC, pp. 654\u2013659, January 2009","DOI":"10.1109\/ASPDAC.2009.4796554"},{"key":"6_CR22","unstructured":"Litterick, M.: Pragmatic simulation-based verification of clock domain crossing signals and jitter using SystemVerilog Assertions. In: DVCON (2006)"},{"key":"6_CR23","unstructured":"Mentor Graphics: Questa CDC. https:\/\/www.mentor.com\/products\/fv\/questa-cdc\/. Accessed Jan 2017"},{"key":"6_CR24","unstructured":"Real Intent: Meridian CDC. http:\/\/www.realintent.com\/real-intent-products\/meridian-cdc\/. Accessed Jan 2017"},{"key":"6_CR25","first-page":"55","volume":"53","author":"S Sarwary","year":"2008","unstructured":"Sarwary, S., Verma, S.: Critical clock-domain-crossing bugs. Electron. Des. Strateg. News 53, 55\u201364 (2008)","journal-title":"Electron. Des. Strateg. News"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Schmaltz, J.: A formal model of clock domain crossing and automated verification of time-triggered hardware. In: FMCAD. pp. 223\u2013230, November 2007","DOI":"10.1109\/FMCAD.2007.4402004"},{"key":"6_CR27","unstructured":"Synopsys: Spyglass CDC. https:\/\/www.synopsys.com\/verification\/static-and-formal-verification.html. Accessed Jan 2017"}],"container-title":["IFIP Advances in Information and Communication Technology","VLSI-SoC: System-on-Chip in the Nanoscale Era \u2013 Design, Verification and Reliability"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67104-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,31]],"date-time":"2021-08-31T00:04:12Z","timestamp":1630368252000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-67104-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319671031","9783319671048"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67104-8_6","relation":{},"ISSN":["1868-4238","1868-422X"],"issn-type":[{"type":"print","value":"1868-4238"},{"type":"electronic","value":"1868-422X"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"1 September 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VLSI-SoC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"IFIP\/IEEE International Conference on Very Large Scale Integration - System on a Chip","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tallinn","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Estonia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 September 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 September 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vlsi-soc2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ati.ttu.ee\/vlsi-soc2016\/index.php?page=7","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}