{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,15]],"date-time":"2025-07-15T00:02:28Z","timestamp":1752537748526,"version":"3.41.2"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Design Automation for Embedded Systems"],"published-print":{"date-parts":[[2002,7]]},"DOI":"10.1023\/a:1016507527035","type":"journal-article","created":{"date-parts":[[2002,12,28]],"date-time":"2002-12-28T22:32:49Z","timestamp":1041114769000},"page":"367-399","source":"Crossref","is-referenced-by-count":2,"title":["A Compositional Framework for Hardware\/Software Co-Design"],"prefix":"10.1007","volume":"6","author":[{"given":"A.","family":"Cau","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Hale","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Dimitrov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Zedan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B.","family":"Moszkowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Manjunathaiah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Spivey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Allara, A., C. Brandolese, W. Fornaciari, F. Salice, and D. Sciuto System-Level Performance Estimation Strategy for Sw and Hw. In Proceedings of the International Conference on Computer Design 1998, 1998.","key":"5091182_CR1"},{"doi-asserted-by":"crossref","unstructured":"Balarin, F., M. Chiodo, P. Giusto, H. Hsieh, A. Jurecska, L. Lavagno, C. Passerone, A. Sangiovanni-Vincentelli, E. Sentovich, K. Suzuki, and B. Tabbara. Hardware-Software Co-Design of Embedded Systems: The Polis Approach. Kluwer Academic Publishers, 1997.","key":"5091182_CR2","DOI":"10.1007\/978-1-4615-6127-9"},{"unstructured":"Barringer, H., M. Fisher, G. Gough, D. Gabbay, and R. Owens. 1995, Metatem: A Framework for Programming in Temporal Logic. In Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, 1995.","key":"5091182_CR3"},{"doi-asserted-by":"crossref","unstructured":"Beer, I., S. Ben-David, C. Eisner, D. Fisman, A. Gringauze, and Y. Rodeh. The Temporal Logic Sugar. In Proceedings of CAV 2001, 2001.","key":"5091182_CR4","DOI":"10.1007\/3-540-44585-4_33"},{"doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., and G. D. Castillo. A Formal Method for Provably Correct Composition of a Real-Life Processor Out of Basic Components. In Proceedings of the 1st ICECCS'95. 1995, pp. 145-148.","key":"5091182_CR5","DOI":"10.1109\/ICECCS.1995.479320"},{"doi-asserted-by":"crossref","unstructured":"Bowen, J., H. Jifeng, and X. Qiwen. An Animatable Operational Semantics of the VERILOG Hardware Description Language. In Proc. of ICFEM2000: 3rd Int. Conf. on Formal Engineering Methods, 2000, pp. 199-207.","key":"5091182_CR6","DOI":"10.1109\/ICFEM.2000.873820"},{"doi-asserted-by":"crossref","unstructured":"Cau, A., C. Czarnecki, and H. Zedan. Designing a Provably Correct Robot Control System using a \u2018Lean\u2019 Formal Method. In: A. P. Ravn and H. Rischel (eds.): Proceedings 5th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'98), vol. 1486 of LNCS. 1998, pp. 123-132.","key":"5091182_CR7","DOI":"10.1007\/BFb0055342"},{"doi-asserted-by":"crossref","unstructured":"Cau, A., and H. Zedan. Refining Interval Temporal Logic Specifications. In: M. Bertran and T. Rus (eds.): Transformation-Based Reactive Systems Development, vol. 1231 of LNCS, 1997, pp. 79-94.","key":"5091182_CR8","DOI":"10.1007\/3-540-63010-4_6"},{"unstructured":"Celoxica Ltd., Handel-C Language Reference Manual.","key":"5091182_CR9"},{"issue":"9","key":"5091182_CR10","doi-asserted-by":"crossref","first-page":"1004","DOI":"10.1109\/TCOM.1977.1093941","volume":"25","author":"W.-H. Chen","year":"1977","unstructured":"Chen, W.-H., C. H. Smith, and S. C. Fralick. A Fast Computational Algorithm for the Discrete Cosine Transform. IEEE Transaction on Communications, vol. 25,no. 9, pp. 1004-1009, 1977.","journal-title":"IEEE Transaction on Communications"},{"doi-asserted-by":"crossref","unstructured":"Clarke, E. M., E. Emerson, and A. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM TOPLAS, vol. 8,no. 2, 1986.","key":"5091182_CR11","DOI":"10.1145\/5397.5399"},{"doi-asserted-by":"crossref","unstructured":"Borrione, D., P. Camurati, J. Piallet, and P. Prinetto. A Functional Approach to Formal Hardware Verification. In Proc. of ICCD-88, 1988, pp. 592-595.","key":"5091182_CR12","DOI":"10.1109\/ICCD.1988.25769"},{"unstructured":"de Roever, W.-P., F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, 2001.","key":"5091182_CR13"},{"doi-asserted-by":"crossref","unstructured":"Dimitrov, J. Interval Temporal Logic (ITL) Semantics for Verilog. Proc. of IEE event on Hardware-Software Co-Design, 2000.","key":"5091182_CR14","DOI":"10.1049\/ic:20000597"},{"unstructured":"Dimitrov, J. Operational Semantics for Verilog. In Proceedings of APSEC'2001, 2001.","key":"5091182_CR15"},{"unstructured":"Dreike, P., and J. McCoy. Cosimulating Hardware and Software in Embedded Systems. In Proceedings Embedded Systems Programming Europe, 1997, pp. 12-27.","key":"5091182_CR16"},{"doi-asserted-by":"crossref","unstructured":"Ernst, R. Codesign of Embedded Systems: Status and Trends. IEEE Design & Test of Computers pp. 45-54, 1998.","key":"5091182_CR17","DOI":"10.1109\/54.679207"},{"doi-asserted-by":"crossref","unstructured":"Gajski, D. D., J. Zhu, and R. Domer. Essential Issues in Codesign. Technical Report ICS-TR-97-26, University of California, Irvine, Department of Information and Computer Science, 1997.","key":"5091182_CR18","DOI":"10.1007\/978-1-4757-2649-7_1"},{"doi-asserted-by":"crossref","unstructured":"Gordon, M., The Semantic Challenge of Verilog HDL. In Proc. 10th Annual IEEE Symposium on Logic in Computer Science, 1995, pp. 136-145.","key":"5091182_CR19","DOI":"10.1109\/LICS.1995.523251"},{"unstructured":"Gordon, M.J.C., and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.","key":"5091182_CR20"},{"unstructured":"Grundy, J. Window Inference in the HOL System. In: P. J. Windley, M. Archer, K. N. Levitt, and J. J. Joyce (eds.): The Proceedings of the International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications, 1991.","key":"5091182_CR21"},{"unstructured":"Gupta, R. K. (ed.): Special Issue on Hardware\/Software Partitioning of Design Automation for Embedded Systems Journal, Kluwer Academic Publishers, vol. 2, 1997.","key":"5091182_CR22"},{"unstructured":"Hale, R. Using ITL for Co-Design. In Proc. of the Verification Workshop VERIFY'01, 2001.","key":"5091182_CR23"},{"key":"5091182_CR24","series-title":"Appeared as technical report","volume-title":"Programming in Temporal Logic","author":"R. W. S. Hale","year":"1988","unstructured":"Hale, R. W. S. Programming in Temporal Logic. Ph.D. thesis, Computer Laboratory, Cambridge University, Cambridge, England, 1988, Appeared as technical report 173 in year 1989."},{"doi-asserted-by":"crossref","unstructured":"Hale, R. W. S., and H. Jifeng. A Real-Time Programming Language. In: J. Bowen (ed.): Towards Verified Systems. Elsevie, pp. 115-130, 1994.","key":"5091182_CR25","DOI":"10.1016\/B978-0-444-89901-9.50015-X"},{"unstructured":"Hollander, Y., M. Morley, and A. Noy. The e Language: A Fresh Separation of Concerns. In: Proceedings of TOOLS Europe 2001, 2001.","key":"5091182_CR26"},{"unstructured":"Holzmann, G. Design and Validation of Computer Protocols. Prentice-Hall, 1990.","key":"5091182_CR27"},{"doi-asserted-by":"crossref","unstructured":"Huibiao, Z., J. Bowen, and H. Jifeng. From Operational Semantics to Denotational Semantics for Verilog. In Proc. of CHARME2001; the 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 2001.","key":"5091182_CR28","DOI":"10.1007\/3-540-44798-9_34"},{"unstructured":"Huibiao, Z., and H. Jifeng. A Semantics of Verilog Using Duration Calculus. In Proc. Intl. Conf. on Software: Theory and Practice. 2000, pp. 421-432.","key":"5091182_CR29"},{"unstructured":"Hunt, W., FM8501: A Verified Microprocessor. In Proc of IFIP WG 10.2 Workshop: From HDL To Guaranteed Correct Circuit Designs. 1986, pp. 85-114.","key":"5091182_CR30"},{"unstructured":"IEEE: IEEE Standard Hardware Description Language Based on the Verilog(\u00a9) Hardware Description Language'. IEEE Standard 1364-1995, 1995.","key":"5091182_CR31"},{"unstructured":"ITL homepage, http:\/\/www.cse.dmu.ac.uk\/~cau\/itlhomepage\/.","key":"5091182_CR32"},{"unstructured":"Jifeng, H., and Z. Huibiao. Formalising Verilog. In Proc. IEEE Intl. Conf. on Electronics, Circuits and Systems. 2000, pp. 412-415.","key":"5091182_CR33"},{"doi-asserted-by":"crossref","unstructured":"Kurshan, R. P., Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.","key":"5091182_CR34","DOI":"10.1515\/9781400864041"},{"unstructured":"Lavenier, D., P. Quinton, and S. Rajopadhye. Chapter 5, Digital Signal Processing for MultiMedia Systems. In Parhi and Hishitani (eds.): Advanced Systolic Design, 1999.","key":"5091182_CR35"},{"issue":"2","key":"5091182_CR36","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1023\/A:1008884219274","volume":"2","author":"J. Madsen","year":"1997","unstructured":"Madsen, J., J. Grode, P. Knudsen, M. Petersen, and A. Haxthausen. LYCOS: The Lyngby Co-Synthesis System. Design Automation for Embedded Systems, vol. 2,no. 2, pp. 195-235, 1997.","journal-title":"Design Automation for Embedded Systems"},{"key":"5091182_CR37","series-title":"Technical Report","volume-title":"Design of Multi-Phase Regular Arrays","author":"M. Manjunathaiah","year":"1999","unstructured":"Manjunathaiah, M., and G. Megson. Design of Multi-Phase Regular Arrays. Technical Report RUCS\/1999\/TR\/016\/A, Computer Science, The University of Reading, U.K., 1999."},{"key":"5091182_CR38","volume-title":"Proceedings of 2001 International Conference on Parallel Processing (30th ICPP'01)","author":"M. Manjunathaiah","year":"2001","unstructured":"Manjunathaiah, M., G. Megson, S. Rajopadhaye, and T. Risset. Uniformization of Affine Dependance Programs for Parallel Embedded System Design. In Proceedings of 2001 International Conference on Parallel Processing (30th ICPP'01). U. Politec. de Valencia, Spain, 2001."},{"unstructured":"Megson, G. An Introduction to Systolic Algorithm Design. Oxford University Press, 1992.","key":"5091182_CR39"},{"key":"5091182_CR40","volume-title":"Executing Temporal Logic Programs","author":"B. Moszkowski","year":"1986","unstructured":"Moszkowski, B., Executing Temporal Logic Programs. Cambridge, England: Cambridge University Press, 1986."},{"unstructured":"Moszkowski, B.: Some Very Compositional Temporal Properties. In: E.-R. Olderog (ed.): Programming Concepts, Methods and Calculi, vol. A-56 of IFIP Transactions. 1994, pp. 307-326.","key":"5091182_CR41"},{"doi-asserted-by":"crossref","unstructured":"Nielson, F., H. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.","key":"5091182_CR42","DOI":"10.1007\/978-3-662-03811-6"},{"key":"5091182_CR43","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/BF00936948","volume":"12","author":"I. Page","year":"1996","unstructured":"Page, I. Constructing Hardware-Software Systems From a Single Description. Journal of VLSI Signal Processing, vol. 12, pp. 87-107, 1996.","journal-title":"Journal of VLSI Signal Processing"},{"unstructured":"Sagdeo, V. The Complete Verilog Book. Kluwer Academic Publishers, 1998.","key":"5091182_CR44"},{"unstructured":"Soininen, J.-P., T. Huttunen, K. Tiensyrja, and H. Heusala. Cosimulation of Real-Time Control Systems. In Proceedings of the European Design Automation Conference with EURO-VHDL'95, 1996.","key":"5091182_CR45"},{"unstructured":"Spivey, J. Deriving a Hardware Compiler From Operational Semantics. Technical report, Oxford University Computing Laboratory, 1997.","key":"5091182_CR46"},{"doi-asserted-by":"crossref","unstructured":"Thomas, D., and P. Moorby. The Verilog Hardware Description Language. Kluwer Academic Publishers, 1998.","key":"5091182_CR47","DOI":"10.1007\/978-1-4757-2896-5"},{"doi-asserted-by":"crossref","unstructured":"Zhou, S., H. Zedan, and A. Cau. A Framework For Analysing The Effect of \u2018Change\u2019 In Legacy Code. In IEEE Proc. of ICSM'99, 1999.","key":"5091182_CR48","DOI":"10.1109\/ICSM.1999.792639"}],"container-title":["Design Automation for Embedded Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1016507527035.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1016507527035\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1016507527035.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,14]],"date-time":"2025-07-14T02:37:05Z","timestamp":1752460625000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1016507527035"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,7]]},"references-count":48,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2002,7]]}},"alternative-id":["5091182"],"URL":"https:\/\/doi.org\/10.1023\/a:1016507527035","relation":{},"ISSN":["0929-5585","1572-8080"],"issn-type":[{"type":"print","value":"0929-5585"},{"type":"electronic","value":"1572-8080"}],"subject":[],"published":{"date-parts":[[2002,7]]}}}