{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T12:04:03Z","timestamp":1759147443178,"version":"3.37.3"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2017,2,14]],"date-time":"2017-02-14T00:00:00Z","timestamp":1487030400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100002418","name":"Intel Corporation","doi-asserted-by":"publisher","award":["Sponsored Projecti Number 05IU019"],"award-info":[{"award-number":["Sponsored Projecti Number 05IU019"]}],"id":[{"id":"10.13039\/100002418","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10703-017-0268-9","type":"journal-article","created":{"date-parts":[[2017,2,14]],"date-time":"2017-02-14T02:18:04Z","timestamp":1487038684000},"page":"317-352","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Symbolic trajectory evaluation for word-level verification: theory and implementation"],"prefix":"10.1007","volume":"50","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7527-7675","authenticated-orcid":false,"given":"Supratik","family":"Chakraborty","sequence":"first","affiliation":[]},{"given":"Zurab","family":"Khasidashvili","sequence":"additional","affiliation":[]},{"given":"Carl-Johan H.","family":"Seger","sequence":"additional","affiliation":[]},{"given":"Rajkumar","family":"Gajavelly","sequence":"additional","affiliation":[]},{"given":"Tanmay","family":"Haldankar","sequence":"additional","affiliation":[]},{"given":"Dinesh","family":"Chhatani","sequence":"additional","affiliation":[]},{"given":"Rakesh","family":"Mistry","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,2,14]]},"reference":[{"key":"268_CR1","doi-asserted-by":"publisher","unstructured":"Barrett C, Conway CL, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C (2011) CVC4. In: Proceedings of the 23rd international conference on computer aided verification, CAV 2011, Snowbird, UT, USA, 14\u201320 July 2011, pp 171\u2013177","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"268_CR2","doi-asserted-by":"publisher","unstructured":"Brayton R, Mishchenko A (2010) ABC: an academic industrial-strength verification tool. In: Proceedings of the 22nd international conference on computer aided verification, CAV\u201910. Springer, Berlin, pp 24\u201340","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"268_CR3","doi-asserted-by":"publisher","unstructured":"Brummayer R, Biere A (2009) Boolector: an efficient SMT solver for bit-vectors and arrays. In: TACAS, pp 174\u2013177","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"268_CR4","unstructured":"Bryant RE, Seger C-JH (1990) Formal verification of digital circuits using symbolic ternary system models. In: CAV, pp 33\u201343"},{"issue":"8","key":"268_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"Randal E Bryant","year":"1986","unstructured":"Bryant Randal E (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"key":"268_CR6","doi-asserted-by":"publisher","unstructured":"Chakraborty S, Gupta A, Jain R (2017) Matching multiplications in bit-vector formulas. In: Verification, model checking and abstract interpretation (VMCAI). Springer, Berlin, pp 131\u2013150","DOI":"10.1007\/978-3-319-52234-0_8"},{"key":"268_CR7","doi-asserted-by":"publisher","unstructured":"Chakraborty S, Khasidashvili Z, Seger C-JH, Gajavelly R, Haldankar T, Chhatani D, Mistry R (2015) Word-level symbolic trajectory evaluation. In: Computer-aided verification (CAV). Springer, Berlin, pp 128\u2013143","DOI":"10.1007\/978-3-319-21668-3_8"},{"key":"268_CR8","doi-asserted-by":"publisher","unstructured":"Cimatti A, Griggio A, Schaafsma B, Sebastiani R (2013) The MathSAT5 SMT solver. In: Piterman N, Smolka S (eds) Proceedings of TACAS, volume 7795 of LNCS. Springer, Berlin","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"268_CR9","doi-asserted-by":"publisher","unstructured":"Cimatti A, Griggio A, Schaafsma B, Sebastiani R (2013) The MathSAT5 SMT solver. In: Piterman N, Smolka S (eds) Proceedings of TACAS, volume 7795 of LNCS. Springer, Berlin","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"268_CR10","doi-asserted-by":"crossref","unstructured":"Dutertre B (2014) Yices 2.2. In: Biere A, Bloem R (eds) Computer-aided verification (CAV\u20192014), volume 8559 of Lecture notes in computer science, pp 737\u2013744. Springer, Berlin","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"268_CR11","unstructured":"Dutertre B, De Moura L (2006) The yices SMT solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf , 2(2)"},{"key":"268_CR12","unstructured":"E\u00e9n N, S\u00f6rensson N (2012) The minisat page"},{"key":"268_CR13","doi-asserted-by":"crossref","unstructured":"Emerson EA (1995) Temporal and modal logic. In: Hanbook of theoretical computer science, pp 995\u20131072. Elsevier, Amsterdam","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"268_CR14","unstructured":"IEEE standard for SystemVerilog\u2014unified hardware design, specification, and verification language. IEEE Std 1800-2012 (Revision of IEEE Std 1800-2009), pp 1\u20131315 (2013)"},{"key":"268_CR15","doi-asserted-by":"publisher","unstructured":"Jha S, Limaye R, Seshia SA (2009) Beaver: engineering an efficient SMT solver for bit-vector arithmetic. In: Proceedings of the 21st international conference on computer aided verification, CAV 2009, Grenoble, France, June 26\u2013July 2, 2009, pp 668\u2013674","DOI":"10.1007\/978-3-642-02658-4_53"},{"key":"268_CR16","doi-asserted-by":"publisher","unstructured":"Johannsen P (2001) Reducing bitvector satisfiability problems to scale down design sizes for RTL property checking. In: HLDVT, pp 123\u2013128","DOI":"10.1109\/HLDVT.2001.972818"},{"issue":"4","key":"268_CR17","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1109\/54.936245","volume":"18","author":"RB Jones","year":"2001","unstructured":"Jones RB, O\u2019Leary JW, Seger C-JH, Aagaard M, Melham TF (2001) Practical formal verification in microprocessor design. IEEE Des Test Comput 18(4):16\u201325","journal-title":"IEEE Des Test Comput"},{"key":"268_CR18","unstructured":"Kaivola R, Ghughal R, Narasimhan N, Telfer A, Whittemore J, Pandav S, Slobodov\u00e1 A, Taylor C, Frolov V, Reeber E, Naik A (2009) Replacing testing with formal verification in intel $$\\text{Core}^\\text{ TM }$$ Core TM i7 processor execution engine validation. In: CAV, pp 414\u2013429"},{"key":"268_CR19","unstructured":"KiranKumar VMA, Gupta A, Ghughal R (2012) Symbolic trajectory evaluation: the primary validation vehicle for next generation intel $$^{\\textregistered }$$ \u00ae processor graphics fpu. In: FMCAD, pp 149\u2013156"},{"key":"268_CR20","unstructured":"Kroening D, Strichman O (2008) Decision procedures: an algorithmic point of view. Texts in theoretical computer science. An EATCS series. Springer, Berlin"},{"key":"268_CR21","unstructured":"Malvar HS, Li-Wei H, Cutler R (2004) High-quality linearinterpolation for demosaicing of Bayer-patterned color images. In: ICASSP, vol 3, pp 485\u2013488"},{"key":"268_CR22","doi-asserted-by":"publisher","unstructured":"Roorda J-W, Claessen K (2005) A new SAT-based algorithm for symbolic trajectory evaluation. In: CHARME, pp 238\u2013253","DOI":"10.1007\/11560548_19"},{"issue":"2","key":"268_CR23","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C-JH Seger","year":"1995","unstructured":"Seger C-JH, Bryant RE (1995) Formal verification by symbolic evaluation of partially-ordered trajectories. Form Methods Syst Des 6(2):147\u2013189","journal-title":"Form Methods Syst Des"},{"issue":"9","key":"268_CR24","doi-asserted-by":"publisher","first-page":"1381","DOI":"10.1109\/TCAD.2005.850814","volume":"24","author":"C-JH Seger","year":"2005","unstructured":"Seger C-JH, Jones RB, O\u2019Leary JW, Melham TF, Aagaard M, Barrett C, Syme D (2005) An industrially effective environment for formal hardware verification. IEEE Trans CAD Integr Circuits Syst 24(9):1381\u20131405","journal-title":"IEEE Trans CAD Integr Circuits Syst"},{"key":"268_CR25","unstructured":"Somenzi F (2012) CUDD: CU decision diagram package-release 2.5.0. University of Colorado at Boulder"},{"key":"268_CR26","doi-asserted-by":"publisher","unstructured":"Stump A, Barrett CW, Dill DL (2001) A decision procedure for an extensional theory of arrays. In: Logic in computer science (LICS). IEEE Computer Society, pp 29\u201337","DOI":"10.1109\/LICS.2001.932480"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0268-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0268-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0268-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,18]],"date-time":"2019-09-18T12:57:11Z","timestamp":1568811431000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0268-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,14]]},"references-count":26,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["268"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0268-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2017,2,14]]}}}