{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:34:20Z","timestamp":1761597260928,"version":"3.38.0"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,3,29]],"date-time":"2011-03-29T00:00:00Z","timestamp":1301356800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Electron Test"],"published-print":{"date-parts":[[2011,4]]},"DOI":"10.1007\/s10836-011-5209-8","type":"journal-article","created":{"date-parts":[[2011,3,28]],"date-time":"2011-03-28T12:02:45Z","timestamp":1301313765000},"page":"137-162","source":"Crossref","is-referenced-by-count":9,"title":["Efficient Generation of Stimuli for Functional Verification by Backjumping Across Extended FSMs"],"prefix":"10.1007","volume":"27","author":[{"given":"Giuseppe Di","family":"Guglielmo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi Di","family":"Guglielmo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franco","family":"Fummi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Graziano","family":"Pravadelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,3,29]]},"reference":[{"issue":"1","key":"5209_CR1","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1145\/225871.225880","volume":"1","author":"K Cheng","year":"1996","unstructured":"Cheng K, Krishnakumar A (1996) Automatic generation of functional vectors using the extended finite state machine model. ACM Transact Des Automat Electron Syst 1(1):57\u201379","journal-title":"ACM Transact Des Automat Electron Syst"},{"key":"5209_CR2","unstructured":"Chipounov V, Georgescu V, Zamfir C, Candea G (2009) Selective symbolic execution. In: Proc. of workshop on hot topics dependable systems"},{"key":"5209_CR3","doi-asserted-by":"crossref","unstructured":"Corno F, Cumani G, Sonza Reorda M, Squillero G (2001) Effective Techniques for High-Level ATPG. In: Proc of IEEE ATS, pp 225\u2013230","DOI":"10.1109\/ATS.2001.990286"},{"issue":"4","key":"5209_CR4","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron R, Ferrante J, Rosen B, Wegman M, Zadeck F (1991) Efficiently computing static single assignment form and the control dependence graph. ACM Trans Program Lang Syst (TOPLAS) 13(4):451\u2013490","journal-title":"ACM Trans Program Lang Syst (TOPLAS)"},{"key":"5209_CR5","unstructured":"Di Guglielmo G, Fummi F, Marconcini C, Pravadelli G (2006) Improving Gate-Level ATPG by Traversing Concurrent EFSMs. In: Proc of IEEE VTS"},{"key":"5209_CR6","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/BF01386390","volume":"1","author":"E Dijkstra","year":"1959","unstructured":"Dijkstra E (1959) A note on two problems in connexion with graphs. Numer Math 1:269\u2013271","journal-title":"Numer Math"},{"issue":"5","key":"5209_CR7","doi-asserted-by":"crossref","first-page":"614","DOI":"10.1109\/TC.2004.1275300","volume":"53","author":"A Duale","year":"2004","unstructured":"Duale A, Uyar U (2004) A method enabling feasible conformance test sequence generation for EFSM models. IEEE Trans Comput 53(5):614\u2013627","journal-title":"IEEE Trans Comput"},{"key":"5209_CR8","doi-asserted-by":"crossref","unstructured":"Ferrandi F, Fummi F, Sciuto D (1998) Implicit test generation for behavioral vhdl models. In: Proc of IEEE ITC, pp 436\u2013441","DOI":"10.1109\/TEST.1998.743202"},{"key":"5209_CR9","doi-asserted-by":"crossref","unstructured":"Fin A, Fummi F (2003) Genetic algorithms: the philosopher\u2019s stone or an effective solution for high-level TPG? In: Proc of IEEE HLDVT, pp 163\u2013168","DOI":"10.1109\/HLDVT.2003.1252491"},{"key":"5209_CR10","doi-asserted-by":"crossref","unstructured":"Fummi F, Marconcini C, Pravadelli G (2004) Functional verification based on the EFSM model. In: Proc of IEEE HLDVT, pp 69\u201374","DOI":"10.1109\/HLDVT.2004.1431240"},{"key":"5209_CR11","doi-asserted-by":"crossref","unstructured":"Gajski D, Zhu J, Domer R (1997) Essential issue in codesign. Thecnical report ICS-97-26, University of California, Irvine","DOI":"10.1007\/978-1-4757-2649-7_1"},{"key":"5209_CR12","doi-asserted-by":"crossref","unstructured":"Gajski D, Dutt N, Allen S, Wu C, Lin Y (1992) High-level synthesis: introduction to chip and system design, 1st edn. Kluwer Academic Publishers","DOI":"10.1007\/978-1-4615-3636-9_1"},{"key":"5209_CR13","unstructured":"Gaschnig J (1979) Performance measurement and analysis of certain search algorithms. PhD thesis, Department of Computer Science, CarnegieMellon University, Pittsburgh"},{"issue":"3","key":"5209_CR14","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1109\/43.913758","volume":"20","author":"I Ghosh","year":"2001","unstructured":"Ghosh I, Fujita M (2001) Automatic test pattern generation for functional register-transfer level circuits using assignment decision diagrams. IEEE Trans Comput-Aided Des Integr Circuits Syst 20(3):402\u2013415","journal-title":"IEEE Trans Comput-Aided Des Integr Circuits Syst"},{"key":"5209_CR15","doi-asserted-by":"crossref","unstructured":"Giomi J (1995) Finite state machine extraction from hardware description languages. In: ASIC conference and exhibit, 1995. Proceedings of the eighth annual IEEE international, pp 353\u2013357","DOI":"10.1109\/ASIC.1995.580747"},{"key":"5209_CR16","doi-asserted-by":"crossref","unstructured":"Hansen T, Schachte P, S\u00f8ndergaard H (2009) State Joining and Splitting for the Symbolic Execution of Binaries. In: Runtime Verification. Springer, pp 76\u201392","DOI":"10.1007\/978-3-642-04694-0_6"},{"key":"5209_CR17","doi-asserted-by":"crossref","unstructured":"Hierons R, Kim T-H, Ural H (2002) Expanding an extended finite state machine to aid testability. In: Proc of IEEE COMPSAC, pp 334\u2013339","DOI":"10.1109\/CMPSAC.2002.1045023"},{"key":"5209_CR18","unstructured":"IEEE Computer Society (2008) IEEE standard for the functional language e. IEEE Computer Society"},{"key":"5209_CR19","doi-asserted-by":"crossref","unstructured":"Iyer M, Parthasarathy G, Cheng K-T (2005) Efficient conflict-based learning in an RTL circuit constraint solver. In: Proc of IEEE DATE, pp 666\u2013671","DOI":"10.1109\/DATE.2005.127"},{"key":"5209_CR20","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19","author":"J Jaffar","year":"1994","unstructured":"Jaffar J, Maher M (1994) Constraint logic programming: a survey. J Log Program 19:503\u2013581","journal-title":"J Log Program"},{"issue":"7","key":"5209_CR21","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J King","year":"1976","unstructured":"King J (1976) Symbolic execution and program testing. Commun ACM 19(7):385\u2013394","journal-title":"Commun ACM"},{"key":"5209_CR22","volume-title":"Decision procedures: an algorithmic point of view","author":"D Kroening","year":"2008","unstructured":"Kroening D, Strichman O (2008) Decision procedures: an algorithmic point of view. Springer, New York"},{"key":"5209_CR23","unstructured":"Lee D, Yannakakis M (1992) Online minimization of transition systems. In: Proc of ACM symposium on the theory of computing, pp 264\u2013274"},{"key":"5209_CR24","unstructured":"Lin X, Pomeranz I, Reddy S (1999) Techniques for improving the efficiency of sequential circuit test generation. In: Proc of IEEE\/ACM ICCAD, pp 147\u2013151"},{"key":"5209_CR25","doi-asserted-by":"crossref","unstructured":"Lingappan L, Ravi S, Jha N (2003) Test generation for non-separable RTL controller-datapath circuits using a satisfiability based approach. In: Proc of IEEE ICCD, pp 187\u2013193","DOI":"10.1109\/ICCD.2003.1240893"},{"key":"5209_CR26","unstructured":"Mentor Graphics inFact. http:\/\/www.mentor.com\/products\/fv\/infact\/"},{"key":"5209_CR27","unstructured":"Mentor Graphics Questa MVC. http:\/\/www.mentor.com\/products\/fv\/questa-mvc\/"},{"key":"5209_CR28","doi-asserted-by":"crossref","unstructured":"Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient sat solver. In: Proc of ACM\/IEEE DAC, 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"5209_CR29","volume-title":"The art of software testing","author":"G Myers","year":"1979","unstructured":"Myers G (1979) The art of software testing. Wiley-Interscience, New York"},{"key":"5209_CR30","unstructured":"Navabi Z (1993) VHDL: analysis and modeling of digital systems. McGraw-Hill"},{"key":"5209_CR31","doi-asserted-by":"crossref","unstructured":"Padmanabhuni S (1999) Extended analysis of intelligent backtracking algorithms for the maximal constraint satisfaction problem. In: Proc of IEEE CCECE, pp 1710\u20131715","DOI":"10.1109\/CCECE.1999.804975"},{"issue":"1","key":"5209_CR32","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1146\/annurev.cs.02.060187.002315","volume":"2","author":"J Pearl","year":"1987","unstructured":"Pearl J, Korf R (1987) Search techniques. Annu Rev Comput Sci 2(1):451\u2013467","journal-title":"Annu Rev Comput Sci"},{"key":"5209_CR33","unstructured":"Politecnico di Torino (1999) ITC-99 Benchmarks. In: http:\/\/www.cad.polito.it\/tools\/itc99.html"},{"key":"5209_CR34","doi-asserted-by":"crossref","unstructured":"Regimbal S, Lemire J-F, Savaria Y, Bois G, Aboulhamid E, Baron A (2003) Automating functional coverage analysis based on an executable specification. In: Proc of IEEE international workshop on system-on-chip for real-time applications, pp 228\u2013234","DOI":"10.1109\/IWSOC.2003.1213040"},{"key":"5209_CR35","doi-asserted-by":"crossref","unstructured":"Roy S, Ramesh S, Chakraborty S, Nakata T, Rajan S (2002) Functional verification of system on chips-practices, issues and challenges. In: Proc of IEEE ASP-DAC, pp 11\u201313","DOI":"10.1109\/ASPDAC.2002.994873"},{"key":"5209_CR36","unstructured":"Russel S, Norvig P (2002) Artificial intelligence: a modern approach. Prentice Hall"},{"key":"5209_CR37","unstructured":"Sallay B, Petri A, Tilly K, Pataricza A, Sziray J (1996) High level test pattern generation for vhdl circuits. In: Proc of IEEE ETW, pp 201\u2013205"},{"key":"5209_CR38","doi-asserted-by":"crossref","unstructured":"Tao Y (2009) An introduction to assertion-based verification. In: Proc of IEEE international conference on ASIC, pp 1318\u20131323","DOI":"10.1109\/ASICON.2009.5351246"},{"key":"5209_CR39","unstructured":"Uyar U, Duale A (1997) Modeling VHDL specifications as consistent EFSMs. In: Proc of IEEE MILCOM, pp 740\u2013744"},{"key":"5209_CR40","doi-asserted-by":"crossref","unstructured":"Uyar U, Duale A (1999) Resolving inconsistencies in EFSM-modeled specifications. In: Proc of IEEE MILCOM, pp 135\u2013139","DOI":"10.1109\/MILCOM.1999.822658"},{"key":"5209_CR41","unstructured":"Uyar U, Duale A (2000) Test generation form EFSM models of complex army protocols with inconsistencies. In: Proc of IEEE MILCOM, pp 340\u2013346"},{"key":"5209_CR42","unstructured":"Wallace M, Veron A (1994) Two problems-two solutions: one system-ECLiPSe. In: IEE Colloquium on advanced software technologies for scheduling, pp 1\u20133"},{"key":"5209_CR43","unstructured":"Wu Q, Hsiao M (2004) Efficient ATPG for design validation based on partitioned state exploration histories. In: Proc of IEEE VTS, pp 389\u2013394"},{"key":"5209_CR44","unstructured":"Xin F, Ciesielski M, Harris I (2005) Design validation of behavioral vhdl descriptions for arbitrary fault models. In: Proc of IEEE ETS, pp 156\u2013161"},{"key":"5209_CR45","doi-asserted-by":"crossref","unstructured":"Zhang L, Ghosh I, Hsiao M (2003) Efficient Sequential ATPG for Functional RTL Circuits. In: Proc of IEEE ITC, pp 290\u2013298","DOI":"10.1109\/TEST.2003.1270851"}],"container-title":["Journal of Electronic Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-011-5209-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10836-011-5209-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-011-5209-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,4]],"date-time":"2025-03-04T18:29:28Z","timestamp":1741112968000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10836-011-5209-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3,29]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,4]]}},"alternative-id":["5209"],"URL":"https:\/\/doi.org\/10.1007\/s10836-011-5209-8","relation":{},"ISSN":["0923-8174","1573-0727"],"issn-type":[{"type":"print","value":"0923-8174"},{"type":"electronic","value":"1573-0727"}],"subject":[],"published":{"date-parts":[[2011,3,29]]}}}