{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,4]],"date-time":"2024-12-04T02:10:15Z","timestamp":1733278215807,"version":"3.30.1"},"reference-count":26,"publisher":"Elsevier BV","issue":"12","license":[{"start":{"date-parts":[[2000,10,1]],"date-time":"2000-10-01T00:00:00Z","timestamp":970358400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Systems Architecture"],"published-print":{"date-parts":[[2000,10]]},"DOI":"10.1016\/s1383-7621(00)00014-x","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T18:33:56Z","timestamp":1049740436000},"page":"1137-1158","source":"Crossref","is-referenced-by-count":3,"title":["Symbolic forward\/backward traversals of large finite state machines"],"prefix":"10.1016","volume":"46","author":[{"given":"Gianpiero","family":"Cabodi","sequence":"first","affiliation":[]},{"given":"Paolo","family":"Camurati","sequence":"additional","affiliation":[]},{"given":"Stefano","family":"Quer","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1383-7621(00)00014-X_BIB1","doi-asserted-by":"crossref","unstructured":"H. Touati, H. Savoj, B. Lin, R.K. Brayton, A. Sangiovanni-Vincentelli, Implicit enumeration of finite state machines using BDDs, in: Proceedings of the IEEE ICCAD'90, San Jose, CA, USA, November 1990, pp. 130\u2013133","DOI":"10.1109\/ICCAD.1990.129860"},{"issue":"4","key":"10.1016\/S1383-7621(00)00014-X_BIB2","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/43.275352","article-title":"Symbolic model checking for sequential circuit verification","volume":"13","author":"Burch","year":"1994","journal-title":"IEEE Transactions on CAD"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB3","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, J.C. Madre, Verification of sequential machines based on symbolic execution, in: Lecture Notes in Computer Science, vol. 407, Springer, Berlin, 1989, pp. 365\u2013373","DOI":"10.1007\/3-540-52148-8_30"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB4","doi-asserted-by":"crossref","unstructured":"H. Cho, G.D. Hatchel, E. Macii, B. Plessier, F. Somenzi, Algorithms for approximate FSM traversal, in: Proceedings of the ACM\/IEEE DAC'93, Dallas, TX, USA, June 1993, pp. 25\u201330","DOI":"10.1145\/157485.164555"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB5","unstructured":"H. Cho, G.D. Hatchel, E. Macii, M. Poncino, K. Ravi, F. Somenzi, Approximate finite state machine traversal: extensions and new results, in: IWLS'95 \u2013 IEEE International Workshop on Logic Synthesis, Lake Tahoe, CA, USA, May 1995"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB6","doi-asserted-by":"crossref","unstructured":"F. Brglez, D. Bryan, K. Ko\u017ami\u0144ski, Combinatorial profiles of sequential benchmark circuits, in: Proceedings of the IEEE ISCAS'89, May 1989, pp. 1929\u20131934","DOI":"10.1109\/ISCAS.1989.100747"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB7","unstructured":"S. Yang, Logic Synthesis and Optimization Benchmarks User Guide Version 3.0, in: MCNC Report, Research Triangle Park, NC, USA, January 1991"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB8","unstructured":"G. Cabodi, P. Camurati, S. Quer, Symbolic exploration of large circuits with enhanced forward\/backward traversals, in: Proceedings of the IEEE EURO-DAC'94, Grenoble, France, September 1994, pp. 22\u201327"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB9","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, S. Quer, Full symbolic ATPG for large circuit, in: Proceedings of the IEEE ITC'94, Washington DC, USA, October 1994, pp. 980\u2013988","DOI":"10.1109\/TEST.1994.528047"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB10","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, S. Quer, Efficient state space pruning in symbolic backward traversal, in: Proceedings of the IEEE ICCD'94, Cambridge, MA, USA, October 1994, pp. 230\u2013235","DOI":"10.1109\/ICCD.1994.331895"},{"issue":"8","key":"10.1016\/S1383-7621(00)00014-X_BIB11","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for Boolean function manipulation","volume":"C\u201335","author":"Bryant","year":"1986","journal-title":"IEEE Transactions on Computers"},{"issue":"3","key":"10.1016\/S1383-7621(00)00014-X_BIB12","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","article-title":"Symbolic Boolean manipulation with ordered binary-decision diagrams","volume":"24","author":"Bryant","year":"1992","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB13","doi-asserted-by":"crossref","unstructured":"K.S. Brace, R.L. Rudell, R.E. Bryant. Efficient implementation of a BDD package, in: Proceedings of the ACM\/IEEE DAC'90, June 1990, pp. 40\u201345","DOI":"10.1145\/123186.123222"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB14","unstructured":"O. Coudert, C. Berthet, J.C. Madre, Verification of sequential machines using Boolean function vectors, in: Proceedings of the IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, 1989, pp. 111\u2013128"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB15","doi-asserted-by":"crossref","unstructured":"H. Cho, G. Hachtel, S.W. Jeong, B. Plessier, E. Schwarz, F. Somenzi, ATPG aspects of FSM verification, in: Proceedings of the IEEE ICCAD'90, San Jose, CA, USA, November 1990, pp. 134\u2013137","DOI":"10.1109\/ICCAD.1990.129861"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB16","unstructured":"O. Coudert, J.C. Madre, Symbolic computation of the valid states of the sequential machine: algorithms and discussion, in: Proceedings of the 1991 International Workshop on Formal Methods in VLSI Design, January 1991"},{"issue":"5","key":"10.1016\/S1383-7621(00)00014-X_BIB17","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1109\/43.631208","article-title":"Symbolic FSM traversals based on the transition relation","volume":"16","author":"Cabodi","year":"1997","journal-title":"IEEE Transactions on CAD"},{"issue":"9","key":"10.1016\/S1383-7621(00)00014-X_BIB18","doi-asserted-by":"crossref","first-page":"1179","DOI":"10.1109\/43.310907","article-title":"Boolean division and factorization using binary decision diagrams","volume":"13","author":"Stanion","year":"1994","journal-title":"IEEE Transactions on CAD"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB19","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, S. Quer, Detecting hard faults with combined approximate forward\/backward symbolic techniques, in: Proceedings of the IEEE ISCAS'94, London, UK, May 1994, pp. 25\u201330","DOI":"10.1109\/ISCAS.1994.408814"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB20","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1090\/dimacs\/003\/07","article-title":"Verifing temporal properties of sequential machines without building their state diagrams","volume":"3","author":"Coudert","year":"1991","journal-title":"AMS\/DIMACS Series in Discrete Mathematics and Theoretical Computer Science"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB21","doi-asserted-by":"crossref","unstructured":"C. Pixley, S.W. Jeong, G.D. Hachtel, Exact calculation of synchronization sequences based on binary decision diagrams, in: Proceedings of the ACM\/IEEE DAC'92, June 1992, pp. 614\u2013619","DOI":"10.1109\/DAC.1992.227811"},{"issue":"7","key":"10.1016\/S1383-7621(00)00014-X_BIB22","doi-asserted-by":"crossref","first-page":"935","DOI":"10.1109\/43.238030","article-title":"Redundancy identification\/removal and test generation for sequential circuits using implicit state enumeration","volume":"12","author":"Cho","year":"1993","journal-title":"IEEE Transactions on CAD"},{"issue":"5","key":"10.1016\/S1383-7621(00)00014-X_BIB23","doi-asserted-by":"crossref","first-page":"652","DOI":"10.1109\/43.79502","article-title":"Test generation and verification for highly sequential circuits","volume":"10","author":"Ghosh","year":"1991","journal-title":"IEEE Transactions on CAD"},{"issue":"4","key":"10.1016\/S1383-7621(00)00014-X_BIB24","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1109\/2.25381","article-title":"Gentest: an automatic test-generation system for sequential circuits","volume":"22","author":"Chakraborty","year":"1989","journal-title":"IEEE Computer"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB25","doi-asserted-by":"crossref","unstructured":"J.H. Patel, T. Niermann, HITEC: a test generation package for sequential circuits, in: Proceedings of the IEEE EDAC'91, February 1991, pp. 214\u2013218","DOI":"10.1109\/EDAC.1991.206393"},{"key":"10.1016\/S1383-7621(00)00014-X_BIB26","doi-asserted-by":"crossref","unstructured":"K. Hatayama, K. Hikone, M. Ikeda, T. Hayashi, Sequential test generation based on real-valued logic simulation, in: Proceedings of the IEEE ITC'92, September 1992, pp. 41\u201348","DOI":"10.1109\/TEST.1992.527802"}],"container-title":["Journal of Systems Architecture"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S138376210000014X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S138376210000014X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,4]],"date-time":"2024-12-04T01:34:32Z","timestamp":1733276072000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S138376210000014X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,10]]},"references-count":26,"journal-issue":{"issue":"12","published-print":{"date-parts":[[2000,10]]}},"alternative-id":["S138376210000014X"],"URL":"https:\/\/doi.org\/10.1016\/s1383-7621(00)00014-x","relation":{},"ISSN":["1383-7621"],"issn-type":[{"type":"print","value":"1383-7621"}],"subject":[],"published":{"date-parts":[[2000,10]]}}}