{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T11:12:09Z","timestamp":1760613129197,"version":"build-2065373602"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,5,16]],"date-time":"2025-05-16T00:00:00Z","timestamp":1747353600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,5,16]],"date-time":"2025-05-16T00:00:00Z","timestamp":1747353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,10]]},"DOI":"10.1007\/s10703-025-00478-1","type":"journal-article","created":{"date-parts":[[2025,5,16]],"date-time":"2025-05-16T13:22:49Z","timestamp":1747401769000},"page":"3-26","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Timed causal fanin analysis for symbolic simulation"],"prefix":"10.1007","volume":"67","author":[{"given":"Roope","family":"Kaivola","sequence":"first","affiliation":[]},{"given":"Neta Bar","family":"Kama","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,16]]},"reference":[{"key":"478_CR1","doi-asserted-by":"crossref","unstructured":"Aagaard MD, Jones RB, Seger CJH (1999) Formal verification using parametric representations of Boolean constraints. In: Proceedings of the of 36th ACM\/IEEE design automation conference, pp 402\u2013407","DOI":"10.1145\/309847.309968"},{"key":"478_CR2","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 et al (1999) Symbolic model checking without BDDS. In: Cleaveland WR (ed) Tools and algorithms for the construction and analysis of systems. Springer, Berlin Heidelberg, pp 193\u2013207"},{"key":"478_CR3","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-48683-6_8","volume-title":"Computer aided verification","author":"A Biere","year":"1999","unstructured":"Biere A, Clarke E, Raimi R et al (1999) Verifying safety properties of a powerpc microprocessor using symbolic model checking without BDDS. In: Halbwachs N, Peled D (eds) Computer aided verification. Springer, Berlin Heidelberg, pp 60\u201371"},{"issue":"8","key":"478_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput C 35(8):677\u2013691","journal-title":"IEEE Trans Comput C"},{"key":"478_CR5","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 et al (2000) Counterexample-guided abstraction refinement. In: Emerson EA, Sistla AP (eds) computer aided verification. Springer, Berlin Heidelberg, pp 154\u2013169"},{"key":"478_CR6","doi-asserted-by":"publisher","unstructured":"Clarke EM, Kurshan RP, Veith H (2010) The localization reduction and counterexample-guided abstraction refinement. Springer, Berlin Heidelberg, pp 61\u201371. https:\/\/doi.org\/10.1007\/978-3-642-13754-9_4","DOI":"10.1007\/978-3-642-13754-9_4"},{"key":"478_CR7","doi-asserted-by":"crossref","unstructured":"Gupta A, KiranKumar MVA, Ghughal R (2014) Formally verifying graphics FPU. In: Jones C, Pihlajasaari P, Sun J (eds) FM 2014: formal methods. Springer International Publishing, Berlin, pp 673\u2013687","DOI":"10.1007\/978-3-319-06410-9_45"},{"key":"478_CR8","unstructured":"IEEE (1985) IEEE standard for binary floating-point arithmetic. Institute of Electrical and Electronics Engineers, note: Standard 754\u20131985"},{"key":"478_CR9","unstructured":"Intel (2021) Intel AVX512-FP16 Architecture Specification, June 2021, Revision 1.0. https:\/\/software.intel.com\/content\/www\/us\/en\/develop\/download\/intel-avx512-fp16-architecture-specification.html"},{"key":"478_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-1101-4","volume-title":"Symbolic simulation methods for industrial formal verification","author":"RB Jones","year":"2002","unstructured":"Jones RB (2002) Symbolic simulation methods for industrial formal verification. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-1-4615-1101-4"},{"key":"478_CR11","volume-title":"Handbook of computer architecture","author":"R Kaivola","year":"2022","unstructured":"Kaivola R, O\u2019Leary J (2022) Verification of arithmetic and datapath circuits with symbolic simulation. In: Chattopadhyay A (ed) Handbook of computer architecture. Springer, Berlin"},{"key":"478_CR12","doi-asserted-by":"crossref","unstructured":"Kaivola R, Ghughal R, Narasimhan N et\u00a0al (2009) Replacing testing with formal verification in Intel Core i7 processor execution engine validation. In: Bouajjani A, Maler O (eds) Computer aided verification. Springer, pp 414\u2013429","DOI":"10.1007\/978-3-642-02658-4_32"},{"key":"478_CR13","doi-asserted-by":"publisher","unstructured":"Melham T (2018) Symbolic trajectory evaluation. In: Clarke EM, Henzinger TA, Veith H, et\u00a0al (eds) Handbook of model checking. Springer International Publishing, chap\u00a025, pp 831\u2013870, https:\/\/doi.org\/10.1007\/978-3-319-10575-8_25","DOI":"10.1007\/978-3-319-10575-8_25"},{"key":"478_CR14","doi-asserted-by":"publisher","unstructured":"O\u2019Leary J, Kaivola R, Melham T (2013) Relational STE and theorem proving for formal verification of industrial circuit designs. In: 2013 formal methods in computer-aided design, pp 97\u2013104, https:\/\/doi.org\/10.1109\/FMCAD.2013.6679397","DOI":"10.1109\/FMCAD.2013.6679397"},{"issue":"2","key":"478_CR15","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"CH Seger","year":"1995","unstructured":"Seger CH, Bryant RE (1995) Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods Syst Des 6(2):147\u2013189. https:\/\/doi.org\/10.1007\/BF01383966","journal-title":"Formal Methods Syst Des"},{"issue":"9","key":"478_CR16","doi-asserted-by":"publisher","first-page":"1381","DOI":"10.1109\/TCAD.2005.850814","volume":"24","author":"CJ Seger","year":"2005","unstructured":"Seger CJ, Jones R, O\u2019Leary J et al (2005) An industrially effective environment for formal hardware verification. IEEE Trans Computer-Aided Des Integr Circuits Syst 24(9):1381\u20131405. https:\/\/doi.org\/10.1109\/TCAD.2005.850814","journal-title":"IEEE Trans Computer-Aided Des Integr Circuits Syst"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00478-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-025-00478-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00478-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T10:33:32Z","timestamp":1760610812000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-025-00478-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,16]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,10]]}},"alternative-id":["478"],"URL":"https:\/\/doi.org\/10.1007\/s10703-025-00478-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2025,5,16]]},"assertion":[{"value":"29 February 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 April 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 May 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no Conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}