{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T06:31:13Z","timestamp":1648794673174},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1994,7,1]],"date-time":"1994-07-01T00:00:00Z","timestamp":773020800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1994,7]]},"DOI":"10.1007\/bf01384234","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T02:09:32Z","timestamp":1112407772000},"page":"61-94","source":"Crossref","is-referenced-by-count":1,"title":["Modeling multi-rate DSP specification semantics for formal transformational design in HOL"],"prefix":"10.1007","volume":"5","author":[{"given":"Catia M.","family":"Angelo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luc","family":"Claesen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hugo","family":"de Man","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"Hilfinger, P.N., ?Silage, a high-level language and silicon compiler for digital signal processing,?Proceedings IEEE CICC-85, Portland, Oregon, May 1985, pp. 213?216."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Hilfinger, P.N.,Silage Reference Manual, December 1987.","DOI":"10.1049\/esn.1987.0025"},{"key":"CR3","unstructured":"Genin, D., Hilfinger, P., Rabaey, J., Sheers, C. and De Man, H., ?DSP specification using the Silage language,?IEEE International Conference on Acoustics, Speech and Signal Processing, April 1990, pp. 1057?1060."},{"key":"CR4","volume-title":"A Silage Tutorial","author":"L. Nachtergaele","year":"1990","unstructured":"Nachtergaele, L.,A Silage Tutorial IMEC, Leuven, Belgium, May, 1990."},{"key":"CR5","volume-title":"User manual for the S2C Silage to C compiler","author":"L. Nachtergaele","year":"1990","unstructured":"Nachtergaele, L.,User manual for the S2C Silage to C compiler, IMEC, Belgium, May, 1990."},{"issue":"No. 6","key":"CR6","first-page":"73","volume":"3","author":"H. Man De","year":"1986","unstructured":"De Man, H., Rabaey, J., Six, P., Claesen, L., ?Cathedral-II: a silicon compiler for digital signal processing,?IEEE Design & Test of Computers, Vol. 3, No. 6, December 1986, pp. 73?85.","journal-title":"IEEE Design & Test of Computers"},{"key":"CR7","series-title":"Internal report","volume-title":"Defining control flow from an applicative specification","author":"P. Lippens","year":"1988","unstructured":"Lippens, P.,Defining control flow from an applicative specification, Internal report, Philips Research Laboratories, Eindhoven, December, 1988."},{"key":"CR8","first-page":"11","volume-title":"CompEuro 92, IEEE International Conference on Computer Systems and Software Engineering","author":"J.G. Samsom","year":"1992","unstructured":"Samsom, J.G., Claesen, L., De Man, H., ?Correctness preserving transformations on the Hough algorithm,?CompEuro 92, IEEE International Conference on Computer Systems and Software Engineering, Patrick Dewilde and Joos Vandewalle (eds.), IEEE Computer Society Press, May 1992. The Hague, The Netherlands, pp. 11?16."},{"key":"CR9","unstructured":"Angelo, C.M.,Transformations in Silage, IMEC report, November 91."},{"key":"CR10","volume-title":"Formal Hardware Verification in a Silicon Compilation Environment by means of Theorem Proving","author":"C.M. Angelo","year":"1994","unstructured":"Angelo, C.M.,Formal Hardware Verification in a Silicon Compilation Environment by means of Theorem Proving, Ph.D. Thesis, IMEC, Leuven, Belgium, February 1994."},{"key":"CR11","volume-title":"VLSI design methodologies for application-specific cryptographic and algebraic systems","author":"I. Verbauwhede","year":"1991","unstructured":"Verbauwhede, I.,VLSI design methodologies for application-specific cryptographic and algebraic systems, Ph.D. Thesis, IMEC, Leuven, Belgium, 1991."},{"key":"CR12","unstructured":"Vanhoof, J.,Multi-rate expansion for CATHEDRAL-II\/III. A tutorial. IMEC internal report, October 1992."},{"key":"CR13","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1109\/VLSISP.1993.404479","volume-title":"1993 IEEE Workshop on VLSI Signal Processing, VI","author":"J. G. Samsom","year":"1993","unstructured":"Samsom, J. G., Claesen, L., De Man, H., ?SynGuide: An Environment for Doing Interactive Correctness Preserving Transformations,? In L.D.J. Eggermont, P. Dewilde, E. Deprettere, and J. Van Meerbergen, editors,1993 IEEE Workshop on VLSI Signal Processing, VI, pages 269?277. Veldhoven, The Netherlands, IEEE Special Publications, October 1993."},{"key":"CR14","unstructured":"Pauwels, M.,Requirements for bit-true synthesis on specification languages and simulation, synthesis and verification tools, IMEC internal report, September, 1990."},{"key":"CR15","series-title":"VLSI Specification, Verification and Synthesis","first-page":"73","volume-title":"HOL: A proof generating system for higher-order logic","author":"M. Gordon","year":"1988","unstructured":"Gordon, M., ?HOL: A proof generating system for higher-order logic,?VLSI Specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyam, (eds.). Academic Press, Boston, 1988, pp. 73?127."},{"key":"CR16","unstructured":"Cousineau, G., Gordon, M., Huet, G., Milner, R., Paulson, L., Wadsworth, C.,The ML Handbook, INRIA, 1986."},{"key":"CR17","unstructured":"Angelo, C.M.,Issues on the signal flow graph semantics of Silage in HOL, IMEC report, October 1991."},{"key":"CR18","unstructured":"Gordon, A.D.,A mechanised definition of Silage in HOL, Technical Report 287, University of Cambridge Computer Laboratory, February 1993."},{"key":"CR19","doi-asserted-by":"crossref","first-page":"531","DOI":"10.1109\/ICCD.1992.276230","volume-title":"ICCD92: 1992 IEEE International Conference on Computer Design: VLSI in Computers & Processors","author":"A. Gordon","year":"1992","unstructured":"Gordon, A., ?The formal definition of a synchronous hardware-description language in higher order logic,?ICCD92: 1992 IEEE International Conference on Computer Design: VLSI in Computers & Processors, IEEE Computer Society Press, Cambridge, Massachusetts, October 1992, pp. 531?534."},{"key":"CR20","unstructured":"Geurts, W., Pauwels, M. Catthoor, F., Goossens, G., Nachtergaele, L.,Proposal for extensions to the Silage language, IMEC internal report, March, 1990."},{"key":"CR21","unstructured":"Philips, L., Bolsens, I., Rabaeijs, A., Vanhoof, B., Vanhoof, J., ?Silicon integration of digital user-end mobile communication systems,? to appear inIEEE International Conference on Communications ICC'93, Geneva, Switzerland, May, 1993."},{"key":"CR22","unstructured":"University of Cambridge Computer Laboratory,The HOL System Description, October 1991."},{"key":"CR23","series-title":"University Mathematical Series","volume-title":"Mathematical Logic and Hilbert's ?-Symbol","author":"A. Leisenring","year":"1969","unstructured":"Leisenring, A.,Mathematical Logic and Hilbert's ?-Symbol, Macdonald & Co. Ltd., London, 1969, University Mathematical Series."},{"key":"CR24","first-page":"145","volume-title":"IFIP Internatonal Workshop on Higher Order Logic Theorem Proving and its Applications, HOL'92","author":"J. Harrison","year":"1992","unstructured":"Harrison, J., ?Constructing the Real Numbers in HOL,? In L. Claesen and M. Gordon, editors,IFIP Internatonal Workshop on Higher Order Logic Theorem Proving and its Applications, HOL'92, pages 145?164. IMEC, Leuven, Belgium, Elsevier Science Publishers B. V. (North-Holland) Amsterdam, September 1992."},{"key":"CR25","unstructured":"Wong., W., ?Modelling Bit Vectors in HOL: the word Library,? InParticipants' Proceedings of the 1993 International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 373?386. Vancouver, Canada, August 1993. To be published inLecture Notes in Computer Science, Springer-Verlag."},{"key":"CR26","unstructured":"Boulton, R., Gordon, A., Gordon, M., Harrison, J., Herbert, J., Van Tassel, J., ?Experience with embedding hardware description languages in HOL,?Proceedings of the Conference on Theorem Provers in Circuit Design, V. Stavridou, T.F. Melham and R. Boute, (eds.), IFIP North Holland, IFIP Transactions A-10, 1992, pp. 129?156."},{"key":"CR27","unstructured":"Boulton, R., Gordon, M., Herbert, J., Van Tassel, J., ?The HOL verification of ELLA designs,?Proceedings of the International Workshop on Formal Methods in VLSI Design, Miami, January 1991."},{"key":"CR28","unstructured":"Boulton, R.,A HOL Semantics for a Subset of ELLA University of Cambridge Computer Laboratory, Technical Report 254, April 1992."},{"key":"CR29","doi-asserted-by":"crossref","unstructured":"Van Tassel, J.,A Formalisation of the VHDL Simulation Cycle, University of Cambridge Computer Laboratory, Technical Report 249, March 1992.","DOI":"10.1016\/B978-0-444-89880-7.50029-2"},{"key":"CR30","first-page":"359","volume-title":"Proceedings of theHOL'92 International Workshop on Higher Order Logic Theorem Proving and its Applications","author":"J. Tassel Van","year":"1992","unstructured":"Van Tassel, J., ?A Formalisation of the VHDL Simulation Cycle,? Proceedings of theHOL'92 International Workshop on Higher Order Logic Theorem Proving and its Applications, Ed. L. Claesen and M. Gordon, Elsevier North Holland, September, 1992, Leuven, Belgium, pp. 359?374."},{"key":"CR31","volume-title":"Algorithms for high level synthesis: resource utilization based approach","author":"M. Potkonjak","year":"1992","unstructured":"Potkonjak, M.,Algorithms for high level synthesis: resource utilization based approach, Ph.D. Thesis, University of California, Berkeley, January 1992."},{"key":"CR32","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1002\/cta.4490150307","volume":"15","author":"F. Catthoor","year":"1987","unstructured":"Catthoor, F., De Man, H., and Vandewalle, J., ?Bit-Serial VLSI implementation for an optimized transmultiplexer design,?International Journal of Circuit Theory and Applications, Vol. 15, 1987, pp. 281?303.","journal-title":"International Journal of Circuit Theory and Applications"},{"key":"CR33","volume-title":"Architecture synthesis for application-specific medium-throughput digital signal processing chips","author":"J. Vanhoof","year":"1992","unstructured":"Vanhoof, J.,Architecture synthesis for application-specific medium-throughput digital signal processing chips, Ph.D. Thesis, K.U.leuven (Belgium), February 1992."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384234.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384234\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384234","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T16:22:59Z","timestamp":1586190179000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384234"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,7]]},"references-count":33,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1994,7]]}},"alternative-id":["BF01384234"],"URL":"https:\/\/doi.org\/10.1007\/bf01384234","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,7]]}}}