{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:24:51Z","timestamp":1740122691467,"version":"3.37.3"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,12,15]],"date-time":"2022-12-15T00:00:00Z","timestamp":1671062400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,12,15]],"date-time":"2022-12-15T00:00:00Z","timestamp":1671062400000},"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":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2023,3]]},"DOI":"10.1007\/s10626-022-00371-7","type":"journal-article","created":{"date-parts":[[2022,12,15]],"date-time":"2022-12-15T09:03:54Z","timestamp":1671095034000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Design and verification of pipelined circuits with Timed Petri Nets"],"prefix":"10.1007","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1943-8171","authenticated-orcid":false,"given":"R\u00e9mi","family":"Parrot","sequence":"first","affiliation":[]},{"given":"Mika\u00ebl","family":"Briday","sequence":"additional","affiliation":[]},{"given":"Olivier H.","family":"Roux","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,15]]},"reference":[{"issue":"4","key":"371_CR1","first-page":"419","volume":"89","author":"PA Abdulla","year":"2008","unstructured":"Abdulla PA, Deneux J, Ouaknine J, Quaas K, Worrell J (2008) Universality analysis for one-clock timed automata Fundam. Informaticae 89(4):419\u2013450","journal-title":"Informaticae"},{"issue":"1","key":"371_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur R, Courcoubetis C, Dill D (1993) Model-checking in dense real-time. Inf Comput 104(1):2\u201334","journal-title":"Inf Comput"},{"issue":"6","key":"371_CR3","doi-asserted-by":"publisher","first-page":"1509","DOI":"10.1093\/logcom\/exp036","volume":"19","author":"H Boucheneb","year":"2009","unstructured":"Boucheneb H, Gardey G, Roux OH (2009) TCTL model checking of time Petri nets. J Log Comput 19(6):1509\u20131540","journal-title":"J Log Comput"},{"key":"371_CR4","doi-asserted-by":"crossref","unstructured":"Bouyer P, Larsen KG, Nicolas M (2008) Model checking one-clock priced timed automata. Logical Methods in Computer Science 4(2)","DOI":"10.2168\/LMCS-4(2:9)2008"},{"key":"371_CR5","unstructured":"Brayton RK (2020) Berkeley logic synthesis and verification group. ABC: a system for sequential synthesis and verification, release 70930"},{"key":"371_CR6","doi-asserted-by":"crossref","unstructured":"Bufistov D., Cortadella J., Kishinevsky M., Sapatnekar S. (2007) A general model for performance optimization of sequential systems. In: 2007 IEEE\/ACM international conference on computer-aided design","DOI":"10.1109\/ICCAD.2007.4397291"},{"issue":"5","key":"371_CR7","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1109\/81.139289","volume":"39","author":"J Campos","year":"1992","unstructured":"Campos J., Chiola G., Colom J. M., Silva M. (1992) Properties and performance bounds for timed marked graphs. IEEE Transactions on Circuits and Systems I: Fundamental Theory and Applications 39(5):386\u2013401","journal-title":"IEEE Transactions on Circuits and Systems I: Fundamental Theory and Applications"},{"issue":"4","key":"371_CR8","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/MDT.2011.44","volume":"28","author":"F de Dinechin","year":"2011","unstructured":"de Dinechin F, Pasca B (2011) Designing custom arithmetic data paths with FloPoCo. IEEE Design & Test of Computers 28(4):18\u201327","journal-title":"IEEE Design & Test of Computers"},{"key":"371_CR9","doi-asserted-by":"crossref","unstructured":"Hilaire T, Volkova A (2017) Error analysis methods for the fixed-point implementation of linear systems. In: 2017 IEEE international workshop on signal processing systems (siPS), pp 1\u20136","DOI":"10.1109\/SiPS.2017.8109991"},{"key":"371_CR10","doi-asserted-by":"crossref","unstructured":"Hurst A. P., Mishchenko A., Brayton R. K. (2007) Fast minimum-register retiming via binary maximum-flow. In: Formal methods in computer aided design (FMCAD\u201907), pp 181\u2013187","DOI":"10.1109\/FAMCAD.2007.31"},{"key":"371_CR11","doi-asserted-by":"crossref","unstructured":"Istoan M, de Dinechin F (2017) Automating the pipeline of arithmetic datapaths. In: Design, automation & test in europe conference & exhibition (DATE 2017). Lausanne, Switzerland, pp 704\u2013709","DOI":"10.23919\/DATE.2017.7927080"},{"key":"371_CR12","doi-asserted-by":"crossref","unstructured":"Josipovi\u0107 L, Sheikhha S, Guerrieri A, Ienne P, Cortadella J (2020) Buffer placement and sizing for high-performance dataflow circuits. In: Proceedings of the 2020 ACM\/SIGDA Int. Symposium on Field-Programmable Gate Arrays, FPGA \u201920. Association for Computing Machinery, New York, pp 186\u2013196","DOI":"10.1145\/3373087.3375314"},{"key":"371_CR13","doi-asserted-by":"crossref","unstructured":"Kern C, Greenstreet MR (1999) Formal verification in hardware design A survey. ACM Trans Des Autom Electron Syst 4","DOI":"10.1145\/307988.307989"},{"issue":"10","key":"371_CR14","doi-asserted-by":"publisher","first-page":"1990","DOI":"10.1109\/TCAD.2006.873887","volume":"25","author":"DU Lee","year":"2006","unstructured":"Lee D. U., Gaffar A. A., Cheung R. C. C., Mencer O., Luk W., Constantinides GA (2006) Accuracy-guaranteed bit-width optimization. Trans Comp-Aided Des Integ Cir Sys 25(10):1990\u20132000","journal-title":"Trans Comp-Aided Des Integ Cir Sys"},{"issue":"1-6","key":"371_CR15","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF01759032","volume":"6","author":"CE Leiserson","year":"1991","unstructured":"Leiserson CE, Saxe JB (1991) Retiming synchronous circuitry. Algorithmica 6(1-6):5\u201335","journal-title":"Algorithmica"},{"key":"371_CR16","doi-asserted-by":"crossref","unstructured":"Najibi M, Beerel PA (2013) Slack matching mode-based asynchronous circuits for average-case performance. In: Proceedings of the international conference on computer-aided design, ICCAD \u201913. IEEE Press, pp 219\u2013225","DOI":"10.1109\/ICCAD.2013.6691122"},{"key":"371_CR17","doi-asserted-by":"crossref","unstructured":"Ouaknine J, Worrell J (2004) On the language inclusion problem for timed automata: closing a decidability gap. In: Proceedings of the 19th annual IEEE symposium on logic in computer science, 2004, pp 54\u201363","DOI":"10.1109\/LICS.2004.1319600"},{"key":"371_CR18","doi-asserted-by":"crossref","unstructured":"Parrot R, Briday M, Roux OH (2021) Pipeline Optimization using a Cost Extension of Timed Petri Nets. In: The 28th IEEE international symposium on computer arithmetic (ARITH 2021). IEEE","DOI":"10.1109\/ARITH51176.2021.00018"},{"key":"371_CR19","doi-asserted-by":"crossref","unstructured":"Parrot R, Briday M, Roux OH (2021) Timed petri nets with reset for pipelined synchronous circuit design. In: The 42th international conference on application and theory of petri nets and concurrency (petri nets 2021), vol 12734 of lecture notes in computer science. Springer","DOI":"10.1007\/978-3-030-76983-3_4"},{"key":"371_CR20","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, providence. IEEE Computer Society, Rhode Island, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"371_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41115-1","volume-title":"Time and petri nets","author":"L Popova-Zeugmann","year":"2013","unstructured":"Popova-Zeugmann L (2013) Time and petri nets. Springer, Berlin"},{"key":"371_CR22","unstructured":"Ramchandani C (1974) Analysis of asynchronous concurrent systems by timed Petri nets. PhD thesis, Massachusetts Institute of Technology. Cambridge, MA"},{"issue":"3","key":"371_CR23","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1109\/TCAD.2005.853689","volume":"25","author":"S Kim","year":"2006","unstructured":"Kim S, Beerel PA (2006) Pipeline optimization for asynchronous circuits: complexity analysis and an efficient optimal algorithm. IEEE Trans Comput Aided Des Integr Circuits Syst 25(3):389\u2013402","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"371_CR24","doi-asserted-by":"crossref","unstructured":"Sittel P., Fiege N., Kumm M., Zipf P. (2019) Isomorphic subgraph-based problem reduction for resource minimal modulo scheduling. In: 2019 international conference on reconfigurable computing and FPGAs (reconfig), pp 1\u20138","DOI":"10.1109\/ReConFig48160.2019.8994768"},{"key":"371_CR25","doi-asserted-by":"crossref","unstructured":"Sittel P, Kumm M, Oppermann J, M\u00f6ller K, Zipf P, Koch A (2018) Ilp-based modulo scheduling and binding for register minimization. In: 2018 28th international conference on field programmable logic and applications (FPL), pp 265\u20132656","DOI":"10.1109\/FPL.2018.00053"},{"key":"371_CR26","doi-asserted-by":"crossref","unstructured":"Sittel P, M\u00f6ller K, Kumm M, Zipf P, Pasca B, Jervis M (2017) Model-based hardware design based on compatible sets of isomorphic subgraphs. 12","DOI":"10.1109\/FPT.2017.8280140"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-022-00371-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10626-022-00371-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-022-00371-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,3]],"date-time":"2023-03-03T11:19:25Z","timestamp":1677842365000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10626-022-00371-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,15]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3]]}},"alternative-id":["371"],"URL":"https:\/\/doi.org\/10.1007\/s10626-022-00371-7","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"type":"print","value":"0924-6703"},{"type":"electronic","value":"1573-7594"}],"subject":[],"published":{"date-parts":[[2022,12,15]]},"assertion":[{"value":"16 March 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 November 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 December 2022","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 that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Conflict of Interests"}}]}}