{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T00:57:35Z","timestamp":1648861055597},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,9,30]],"date-time":"2020-09-30T00:00:00Z","timestamp":1601424000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,9,30]],"date-time":"2020-09-30T00:00:00Z","timestamp":1601424000000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,2]]},"DOI":"10.1007\/s10009-020-00591-y","type":"journal-article","created":{"date-parts":[[2020,9,30]],"date-time":"2020-09-30T08:05:14Z","timestamp":1601453114000},"page":"1-28","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Utilizing parametric systems for detection of pipeline hazards"],"prefix":"10.1007","volume":"24","author":[{"given":"Luk\u00e1\u0161","family":"Charv\u00e1t","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ale\u0161","family":"Smr\u010dka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,9,30]]},"reference":[{"key":"591_CR1","doi-asserted-by":"crossref","unstructured":"Aagaard, M.D.: A hazards-based correctness statement for pipelined circuits. In: Proceedings of Correct Hardware Design and Verification Methods (CHARME\u201903), LNCS, vol. 2860, pp. 66\u201368. Springer (2003)","DOI":"10.1007\/978-3-540-39724-3_8"},{"key":"591_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: All for the price of few (parameterized verification through view abstraction). In: Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI\u201913), LNCS, vol. 7737, pp .476\u2013495. Springer (2013)","DOI":"10.1007\/978-3-642-35873-9_28"},{"key":"591_CR3","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u2019c, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911), LNCS, vol. 6806, pp. 171\u2013177. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"591_CR4","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Proceedings of 16th International Conference on Computer Aided Verification (CAV\u201904). LNCS, vol. 3114, pp. 197\u2013202. Springer (2004)"},{"key":"591_CR5","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201909). LNCS, vol. 5505, pp. 174\u2013177. Springer (2009)","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"591_CR6","unstructured":"Bryant, R.E.: Formal verification of pipelined Y86-64 microprocessors with UCLID5. Technical Report CMU-CS-18-122 (2018)"},{"key":"591_CR7","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Proceedings of Computer Aided Verification (CAV\u201994), LNCS, vol. 818, pp. 68\u201380. Springer (1994)","DOI":"10.1007\/3-540-58179-0_44"},{"key":"591_CR8","unstructured":"Cadence: Tensilica Software Development Toolkit (SDK) (2014)"},{"key":"591_CR9","doi-asserted-by":"crossref","unstructured":"Charv\u00e1t, L., Smr\u010dka, A., Vojnar, T.: Automatic formal correspondence checking of ISA and RTL microprocessor description. In: Proceedings of Microprocessor Test and Verification (MTV\u201912), pp. 6\u201312. IEEE (2012)","DOI":"10.1109\/MTV.2012.19"},{"key":"591_CR10","unstructured":"Charv\u00e1t, L., Smr\u010dka, A., Vojnar, T.: Hades Hades Hardware Verification Tool. www.fit.vutbr.cz\/research\/groups\/verifit\/tools\/hades\/ (2014)"},{"key":"591_CR11","doi-asserted-by":"crossref","unstructured":"Charv\u00e1t, L., Smr\u010dka, A., Vojnar, T.: Using formal verification of parameterized systems in RAW hazard analysis in microprocessors. In: Proceedings of Microprocessor Test and Verification (MTV\u201914), pp. 83\u201389. IEEE (2014)","DOI":"10.1109\/MTV.2014.21"},{"key":"591_CR12","doi-asserted-by":"crossref","unstructured":"Charv\u00e1t, L., Smr\u010dka, A., Vojnar, T.: Hades: microprocessor hazard analysis via formal verification of parameterized systems. In: Proceedings of 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS\u201916), vol. 233, pp. 87\u201393. EPTCS (2016)","DOI":"10.4204\/EPTCS.233.9"},{"key":"591_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E. Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI\u201906). LNCS, vol. 3855, pp. 126\u2013141. Springer (2006)","DOI":"10.1007\/11609773_9"},{"key":"591_CR14","unstructured":"CodAL architecture description language. www.codasip.com\/custom-processor (2019)"},{"key":"591_CR15","unstructured":"Codasip Studio for rapid processor development. www.codasip.com (2019)"},{"key":"591_CR16","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bjorner, N.: Z3: an efficient SMT solver. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908). LNCS, vol. 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"591_CR17","unstructured":"Hao, K., Ray, S., Xie, F.: Equivalence checking for function pipelining in behavioral synthesis. In: Proceedings of Design, Automation and Test in Europe (DATE\u201914)"},{"key":"591_CR18","doi-asserted-by":"crossref","unstructured":"Jones, R.B., Seger, C.H., Dill, D.L.: Self-consistency checking. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD\u201996). LNCS, vol. 1166, pp. 159\u2013171. Springer (1996)","DOI":"10.1007\/BFb0031806"},{"key":"591_CR19","doi-asserted-by":"crossref","unstructured":"Koelbl, A., Jacoby, R., Jain, H., Pixley, C.: Solver technology for system-level to RTL equivalence checking. In: Proceedings of Design, Automation and Test in Europe (DATE\u201909), pp. 196\u2013201. IEEE (2009)","DOI":"10.1109\/DATE.2009.5090657"},{"key":"591_CR20","unstructured":"Kuhne, U., Beyer, S., Bormann, J., Barstow, J.: Automated formal verification of processors based on architectural models. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD\u201910), pp. 129\u2013136. IEEE (2010)"},{"key":"591_CR21","unstructured":"Mishra, P., Tomiyama, H., Dutt, N., Nicolau, A.: Automatic verification of in-order execution in microprocessors with fragmented pipelines and multicycle functional units. In: Proceedings of Design, Automation and Test in Europe (DATE\u201902), pp. 36\u201343. IEEE (2002)"},{"key":"591_CR22","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S.: Symmetry and completeness in the analysis of parameterized systems. In: Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI\u201907). LNCS, vol. 4349, pp. 299\u2013313. Springer (2007)","DOI":"10.1007\/978-3-540-69738-1_22"},{"key":"591_CR23","doi-asserted-by":"crossref","unstructured":"Ngyuen, M., Thalmaier, M., Wedler, M., Bormann, J., Stoffel, D., Kunz, W.: Unbounded protocol compliance verification using interval property checking with invariants. IEEE Trans. Comput. Aided Des. Integr. Circuits 27(11), 2068\u20132082 (2008). https:\/\/ieeexplore.ieee.org\/document\/4655556","DOI":"10.1109\/TCAD.2008.2006092"},{"key":"591_CR24","volume-title":"Computer Organization and Design: The Hardware\/Software Interface","author":"DA Patterson","year":"2012","unstructured":"Patterson, D.A., Hennessy, J.L.: Computer Organization and Design: The Hardware\/Software Interface, fourth edn. Morgan Kaufmann, Boston (2012)","edition":"fourth"},{"key":"591_CR25","first-page":"65","volume-title":"nML: A Structural Processor Modeling Language for Retargetable Compilation and ASIP Design. Systems on Silicon","author":"J Van Praet","year":"2008","unstructured":"Van Praet, J., Lanneer, D., Geurts, W., Goossens, G.: nML: A Structural Processor Modeling Language for Retargetable Compilation and ASIP Design. Systems on Silicon, vol. 1, pp. 65\u201393. Morgan Kaufmannvol, Burlington (2008)"},{"key":"591_CR26","unstructured":"Synopsys: ASIP designer: design tool for application specific instruction-set processors, designer datasheet (2018)"},{"key":"591_CR27","doi-asserted-by":"crossref","unstructured":"Velev, M.N, Gao, P.: Automatic formal verification of multithreaded pipelined microprocessors. In: Proceedings of International Conference on Computer Aided Design (ICCAD\u201911), pp. 679\u2013686. IEEE (2011)","DOI":"10.1109\/ICCAD.2011.6105403"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00591-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00591-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00591-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,15]],"date-time":"2022-03-15T16:15:51Z","timestamp":1647360951000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00591-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,30]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["591"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00591-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,9,30]]},"assertion":[{"value":"14 September 2020","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 September 2020","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}