{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T08:31:50Z","timestamp":1672302710731},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2005,1,25]],"date-time":"2005-01-25T00:00:00Z","timestamp":1106611200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2005,4]]},"DOI":"10.1007\/s10009-004-0170-9","type":"journal-article","created":{"date-parts":[[2005,1,24]],"date-time":"2005-01-24T15:01:13Z","timestamp":1106578873000},"page":"102-117","source":"Crossref","is-referenced-by-count":7,"title":["A BMC-based formulation for the scheduling problem of hardware systems"],"prefix":"10.1007","volume":"7","author":[{"given":"Gianpiero","family":"Cabodi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alex","family":"Kondratyev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luciano","family":"Lavagno","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Nocco","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Quer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yosinori","family":"Watanabe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,1,25]]},"reference":[{"key":"170_CR1","doi-asserted-by":"crossref","unstructured":"Cabodi G, Kondratiev A, Lavagno L, Nocco S, Quer S, Watanabe Y (2003) A BMC-Formulation for the Scheduling Problem in Highly Constrained Hardware Systems. In: BMC\u201903: First International Workshop on Bounded Model Checking, Boulder, Colorado, July","DOI":"10.1016\/S1571-0661(05)82547-2"},{"key":"170_CR2","doi-asserted-by":"crossref","unstructured":"Cabodi G, Kondratiev A, Lavagno L, Nocco S, Quer S, Watanabe Y (2004) A BMC-Formulation for the Scheduling Problem in Highly Constrained Hardware Systems. In: Strichman O, Biere A (eds) Electronic Notes in Theoretical Computer Science, vol 89. Elsevier","DOI":"10.1016\/S1571-0661(05)82547-2"},{"key":"170_CR3","doi-asserted-by":"crossref","unstructured":"Cabodi G, Nocco S, Quer S (2003) Improving SAT-based bounded model checking by means of BDD-based approximate traversals. In: Proc. conference on design automation and test in Europe, Munich, Germany, March 2003, pp 898\u2013903","DOI":"10.1109\/DATE.2003.1253720"},{"key":"170_CR4","unstructured":"Cabodi G, Quer S (2004) URL: http:\/\/staff.polito.it\/{gianpiero.cabodi,stefano.quer}\/"},{"key":"170_CR5","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1109\/92.238439","volume":"1","author":"Gebotys","year":"1993","unstructured":"Gebotys C (1993) Throughput optimized architectural synthesis. IEEE Trans VLSI Syst 1(3):254\u2013261","journal-title":"IEEE Trans VLSI Syst"},{"key":"170_CR6","doi-asserted-by":"crossref","unstructured":"Goldberg E, Novikov Y (2002) BerkMin: a fast and robust SAT-solver. In: Proc. conference on design automation and test in Europe, Paris, February 2002, pp 142\u2013149","DOI":"10.1109\/DATE.2002.998262"},{"key":"170_CR7","doi-asserted-by":"crossref","unstructured":"Goldberg E, Prasad M, Brayton R (2002) Using problem symmetry in search based satisfiability algorithms. In: Proc. conference on design automation and test in Europe, Paris, February 2002, pp 134\u2013141","DOI":"10.1109\/DATE.2002.998261"},{"key":"170_CR8","doi-asserted-by":"crossref","unstructured":"Gupta S, Dutt N, Gupta R, Nicolau A (2003) SPARK: A high-level synthesis framework for applying parallelizing COMPILER TRANSFORMATIONS. In: Proc. international conference on VLSI","DOI":"10.1109\/ICVD.2003.1183177"},{"key":"170_CR9","unstructured":"Haynal S (2000) Automata-based symbolic scheduling. PhD thesis, University of California at Santa Barbara, December 2000"},{"key":"170_CR10","doi-asserted-by":"crossref","unstructured":"Haynal S, Brewer F (1998) Efficient encoding for exact symbolic automata-based scheduling. In: Proc. international conference on computer-aided design, San Jose, CA, November 1998, pp 477\u2013481","DOI":"10.1145\/288548.289074"},{"key":"170_CR11","unstructured":"Haynal S, Brewer F (1999) Automata-based scheduling for looping DFGs. Technical report, University of California at Santa Barbara, October 1999"},{"key":"170_CR12","doi-asserted-by":"crossref","unstructured":"Hwang C-T, Lee J-H, Hsu Y-C (1991) A formal approach to the scheduling problem in high-level synthesis. IEEE Trans Comput-Aided Des 10:464\u2013475","DOI":"10.1109\/43.75629"},{"key":"170_CR13","doi-asserted-by":"crossref","unstructured":"Khouri KS, Lakkshminarayana G, Jha NK (1999) High-level synthesis of low-power control-flow intensive circuits. IEEE Trans Comput-Aided Des 18(12):1715\u20131729","DOI":"10.1109\/43.811321"},{"key":"170_CR14","doi-asserted-by":"crossref","unstructured":"Lakshminarayana G, Khouri KS, Jha NK (1999) Wavesched: a novel scheduling technique for control-flow intensive design. IEEE Trans Comput-Aided Des 18:505\u2013523","DOI":"10.1109\/43.759064"},{"key":"170_CR15","doi-asserted-by":"crossref","unstructured":"Paulin PG, Knight JP (1989) Force-directed scheduling for the behavioral synthesis of ASICs. IEEE Trans Comput-Aided Des 8:661\u2013679","DOI":"10.1109\/43.31522"},{"key":"170_CR16","doi-asserted-by":"crossref","unstructured":"Radivojevic I, Brewer F (1996) A new symbolic technique for control-dependent scheduling. IEEE Trans Comput-Aided Des 15(1):45\u201347","DOI":"10.1109\/43.486271"},{"key":"170_CR17","doi-asserted-by":"crossref","unstructured":"Wakabayashi K, Tanaka H (1992) Global scheduling independent of control dependencies based on condition vectors. In: Proc. 29th conference on design automation, Anaheim, CA, June 1992, pp 112\u2013115","DOI":"10.1109\/DAC.1992.227852"},{"key":"170_CR18","doi-asserted-by":"crossref","unstructured":"Wang CY, Parhi K (1995) High-level DSP synthesis using concurrent transformations, scheduling, and allocation. IEEE Trans Comput-Aided Des 14:274\u2013295","DOI":"10.1109\/43.365120"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0170-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0170-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0170-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T12:09:16Z","timestamp":1586088556000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0170-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1,25]]},"references-count":18,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,4]]}},"alternative-id":["170"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0170-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,1,25]]}}}