{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:39:59Z","timestamp":1725457199168},"publisher-location":"Berlin, Heidelberg","reference-count":58,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540619376"},{"type":"electronic","value":"9783540495673"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0031817","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:59:01Z","timestamp":1134284341000},"page":"294-309","source":"Crossref","is-referenced-by-count":18,"title":["Formal synthesis in circuit design \u2014 A classification and survey"],"prefix":"10.1007","author":[{"given":"Ramayya","family":"Kumar","sequence":"first","affiliation":[]},{"given":"Christian","family":"Blumenr\u00f6hr","sequence":"additional","affiliation":[]},{"given":"Dirk","family":"Eisenbiegler","sequence":"additional","affiliation":[]},{"given":"Detlef","family":"Schmid","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"22_CR1","unstructured":"R.K. Brayton, C. McMullen, \u201cDecomposition and factorization of boolean expressions\u201d, Proc. International Symposium on Circuits and Systems, IEEE Computer Society, 1982"},{"key":"22_CR2","volume-title":"From HDL Descriptions to Guaranteed Correct Circuit Designs","author":"H. Eveking","year":"1987","unstructured":"H. Eveking, \u201cVerification, Synthesis and Correctness-Preserving Transformations \u2014 Cooperative Approaches to Correct Hardware Design\u201d, From HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione (Ed.), Elsevier Science Publishers North-Holland, 1987"},{"key":"22_CR3","unstructured":"M. Gordon, T. Melham, \u201cIntroduction to HOL: A Theorem Proving Environment for Higher Order Logic\u201d, Cambridge University Press, 1993"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"A. Gupta, \u201cFormal Hardware Verification Methods: A Survey\u201d, Formal Methods in System Design, Kluwer Academic Publishers, Vol. 1, 1992, pp.151\u2013238","DOI":"10.1007\/BF00121125"},{"key":"22_CR5","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1098\/rsta.1992.0025","volume":"339","author":"M. Leeser","year":"1992","unstructured":"M. Leeser, \u201cUsing Nuprl for the verification and synthesis of hardware\u201d, Phil. Trans. R. Soc. Lond., Vol. 339, 1992, pp. 49\u201368","journal-title":"Phil. Trans. R. Soc. Lond."},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"M. Leeser, M. Aagaard, M. Linderman, \u201cThe BEDROC High Level Synthesis System\u201d, Proc. ASIC'91, IEEE, 1991","DOI":"10.1109\/ASIC.1991.242955"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"M. Leeser, R. Chapman, M. Aagaard, M. Linderman, S. Meier, \u201cHigh level Synthesis and Generating FPGAs with the BEDROC System\u201d, Journal of VLSI Signal Processing, Kluwer Academic Publishers, Vol. 6, No.2, Aug. 1993, pp.191\u2013214","DOI":"10.1007\/BF01607881"},{"key":"22_CR8","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1109\/5.52214","volume":"78","author":"M. C. McFarland","year":"1990","unstructured":"M. C. McFarland, A.C. Parker, R. Camposano, \u201cThe high-level Synthesis of Digital Systems\u201d, Proc. of IEEE, Vol. 78, 1990, pp. 301\u2013318","journal-title":"Proc. of IEEE"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"M. Aagaard, M. Leeser, \u201cA Formally verified system for logic synthesis\u201d, Proc. ICCD-91, IEEE, Oct. 1991","DOI":"10.1109\/ICCD.1991.139915"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"M. Aagaard, M. Leeser, \u201cPBS: Proven Boolean Simplification\u201d, IEEE Trans. on Computer Aided Design, Vol. 13, No.4, Apr. 1994","DOI":"10.1109\/43.275356"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"M. Aagaard, M. Leeser, \u201cVerifying a logic synthesis algorithm and implementation: A case study in software verification\u201d, IEEE Trans. on Software Engineering, Oct. 1995","DOI":"10.1109\/32.469458"},{"key":"22_CR12","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1109\/EDTC.1996.494119","volume-title":"Proc. European Design & Test Conference","author":"C.A.J. Eijk van","year":"1996","unstructured":"C.A.J. van Eijk, J.A.G. Jess, \u201cExploiting Functional Dependencies in Finite State Machine Verification\u201d, Proc. European Design & Test Conference 1996, Paris, pp. 9\u201314, IEEE Computer Society Press"},{"key":"22_CR13","unstructured":"Huang, Cheng, Chen, \u201cOn Verifying the Correctness of Retimed Circuits\u201d, Great Lakes Symposium on VLSI 1996, Ames, USA"},{"key":"22_CR14","volume-title":"Synthesis of Digital Designs from Recursion Equations","author":"S.D. Johnson","year":"1984","unstructured":"S.D. Johnson, \u201cSynthesis of Digital Designs from Recursion Equations\u201d, MIT Press, Cambridge, 1984"},{"key":"22_CR15","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/978-1-4613-2007-4_12","volume-title":"VLSI Specification, Verification and Synthesis","author":"S.D. Johnson","year":"1988","unstructured":"S.D. Johnson, B. Bose, C.D. Boyer, \u201cA Tactical Framework for Digital Design\u201d, VLSI Specification, Verification and Synthesis, G. Birtwistle and P. Subrahmanyam, Eds., Kluwer Academic Publishers, Boston, 1988, pp. 349\u2013383"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"S.D. Johnson, \u201cManipulation logical organization with system factorizations\u201d, Hardware Specification, Verification and Synthesis: Mathematical Aspects, Leeser and Brown (Eds.), LNCS, Vol. 408, Springer, 1989","DOI":"10.1007\/0-387-97226-9_33"},{"key":"22_CR17","unstructured":"S.D. Johnson, R. Wehrmeister, B. Bose, \u201cOn the Interplay of Synthesis and Verification\u201d, Proc. IMEC-IFIP Intl. Workshop on Applied Formal Methods in Correct VLSI Design, L. Claesen (Ed.), North Holland, 1989, pp. 385\u2013404"},{"key":"22_CR18","unstructured":"S.D. Johnson, B. Bose, \u201cDDD \u2014 A System for Mechanized Digital Design Derivation\u201d, ACM\/SIGDA Workshop on Formal Methods in VLSI Design, Miami, Florida, Jan. 1991. (Unfortunately, the proceedings of the workshop have not been officially published)"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"B. Bose, S.D. Johnson, \u201cDDD-FM9001: Derivation of a verified microprocessor. An exercise in integrating verification with formal derivation\u201d, Proc. IFIP Conf. on Correct Hardware Design and Verification Methods, LNCS, Vol., Springer, 1993","DOI":"10.1007\/BFb0021724"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"K.Rath, B. Bose, S.D. Johnson, \u201cDerivation of a DRAM Memory Interface by Sequential Decomposition, Proc. Intl. Conf. on Computer Design \u2014 ICCD, IEEE, Oct. 1993, pp.438\u2013441","DOI":"10.1109\/ICCD.1993.393338"},{"key":"22_CR21","unstructured":"K. Rath, M.E. Tuna, S.D. Johnson, \u201cAn Introduction to Behaviour Tables\u201d, Tech. Rep. No. 392, Indiana University, Computer Science Department, December, 1993"},{"key":"22_CR22","unstructured":"Z. Zhu, S.D. Johnson, \u201cAn Example of Interactive Hardware Transformation\u201d, Tech. Rep. No. 383, Indiana University, Computer Science Department, May, 1993"},{"key":"22_CR23","unstructured":"D.W. Knapp, M. Winslett, \u201cA Formalization of Correctness for Linked Representations of Datapath Hardware\u201d, Proc. IMEC-IFIP Intl. Workshop on Applied Formal Methods in Correct VLSI Design, L. Claesen (Ed.), North Holland, 1989, pp. 1\u201320"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"D.W. Knapp, M. Winslett, \u201cA Prescriptive Model for Data-path Hardware\u201d, IEEE Trans. on Computer Aided Design, Vol. 11, No.2, Feb. 1992","DOI":"10.1109\/43.124396"},{"key":"22_CR25","unstructured":"M. Sheeran, \u201cRetiming and slowdown in Ruby\u201d, The fusion of hardware design and verification, G.J. Milne (Ed.), North-Holland, 1988, pp. 245\u2013259"},{"key":"22_CR26","unstructured":"G. Jones, M. Sheeran, \u201cCircuit design in Ruby\u201d, Formal Methods for VLSI design, J. Staunstrup (Ed.), North-Holland, 1990, pp. 13\u201370"},{"key":"22_CR27","unstructured":"L. Rossen, \u201cFormal Ruby\u201d, Formal Methods for VLSI design, J. Staunstrup (Ed.), North-Holland, 1990, pp. 179\u2013190"},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"L. Rossen, \u201cRuby Algebra\u201d, Designing Correct Circuits, Oxford, G. Jones and M. Sheeran (Eds.), Springer, 1990, pp. 297\u2013312","DOI":"10.1007\/978-1-4471-3544-9_16"},{"key":"22_CR29","unstructured":"G. Jones, M. Sheeran, \u201cDeriving bit-serial circuits in Ruby\u201d, Proc. VLSI-91, Edinburgh, A. Halaas and P.B. Denyer (Eds.), Aug. 1991"},{"key":"22_CR30","unstructured":"G. Jones, M. Sheeran, \u201cRelations and refinements in circuit design\u201d, proc. 3rd Refinement Workshop, C.C. Morgan and J.C.P. Woodcock (Eds.), Springer, 1991, pp. 133\u2013152"},{"key":"22_CR31","doi-asserted-by":"crossref","unstructured":"R. Sharp, O. Rasmussen, \u201cTransformational Rewriting with Ruby\u201d, Proc. CHDL-93, D. Agnew, L. Claesen and R. Camposano (Eds.), Elsevier Science Publishers, 1993, pp.243\u2013260","DOI":"10.1016\/B978-0-444-81641-2.50024-1"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"R. Sharp, O. Rasmussen, \u201cThe T-Ruby Design System\u201d, Computer Hardware Description Languages and their Applications (CHDL'95), pp. 587\u2013596, 1995","DOI":"10.1109\/ASPDAC.1995.486374"},{"key":"22_CR33","doi-asserted-by":"crossref","unstructured":"T. Kropf, K. Schneider, R. Kumar, \u201cA Formal Framework for High Level Synthesis\u201d, in TPCD-94, Bad Herrenalb, Germany, R. Kumar and T. Kropf (Eds.), LNCS, Springer, Vol. 901, 1995, pp. 223\u2013238","DOI":"10.1007\/3-540-59047-1_51"},{"key":"22_CR34","volume-title":"From HDL Descriptions to guaranteed Correct Design","author":"G.C. Gopalakrishnan","year":"1987","unstructured":"G.C. Gopalakrishnan, M.K. Srivas, D.R. Smith, \u201cFrom Algebraic Specifications to Correct VLSI Circuits\u201d, From HDL Descriptions to guaranteed Correct Design, D. Borrione (Ed.), Elsevier Science Publishers, North-Holland, 1987"},{"key":"22_CR35","volume-title":"From HDL Descriptions to guaranteed Correct Design","author":"W. Grass","year":"1987","unstructured":"W. Grass, R. Rauscher, \u201cCAMILOD \u2014 A Program System for Designing Digital hardware with Proven Correctness\u201d, From HDL Descriptions to guaranteed Correct Design, D. Borrione (Ed.), Elsevier Science Publishers, North-Holland, 1987"},{"key":"22_CR36","volume-title":"From HDL Descriptions to guaranteed Correct Design","author":"T. Uehara","year":"1987","unstructured":"T. Uehara, \u201cProofs and Synthesis are Cooperative Approaches for Correct Circuit Designs\u201d, From HDL Descriptions to guaranteed Correct Design, D. Borrione (Ed.), Elsevier Science Publishers, North-Holland, 1987"},{"key":"22_CR37","doi-asserted-by":"crossref","unstructured":"R. Camposano, \u201cBehaviour-preserving Transformations for High-level Synthesis\u201d, Proc. Workshop on hardware Specification, Verification and Synthesis: Mathematical Aspects, Leeser and Brown (Eds.), LNCS, Vol. 408, Springer, 1989","DOI":"10.1007\/0-387-97226-9_26"},{"issue":"No.7","key":"22_CR38","doi-asserted-by":"crossref","first-page":"798","DOI":"10.1109\/43.31537","volume":"8","author":"D. Druinsky","year":"1989","unstructured":"D. Druinsky, D. Harel, \u201cUsing State-Charts for hardware Description and Synthesis\u201d IEEE Trans. on CAD, Vol. 8, No.7, July, 1989, pp. 798\u2013807","journal-title":"IEEE Trans. on CAD"},{"key":"22_CR39","doi-asserted-by":"crossref","unstructured":"W. Grass, M. Mutz, W.D. Tiedemann, \u201cHigh-level-Synthesis Based on Formal Methods\u201d, Proc. EUROMICRO '94, Liverpool, 1994, 83\u201391","DOI":"10.1109\/EURMIC.1994.390403"},{"key":"22_CR40","unstructured":"S. Finn, M.P. Fourman, M. Francis, R. Harris, \u201cFormal System Design \u2014 Interactive Synthesis based on computer-assisted formal reasoning\u201d, Proc. IMEC-IFIP Intl. Workshop on Applied Formal Methods in Correct VLSI Design, L. Claesen (Ed) North Holland, 1989, pp.97\u2013110"},{"key":"22_CR41","volume-title":"VLSI-89","author":"M.P. Fourman","year":"1989","unstructured":"M.P. Fourman, E.M. Mayger, \u201cFormally based systems design \u2014 Interactive hardware scheduling\u201d, VLSI-89, G. Musgrave and U. Lauther (Eds.), Munich, North Holland, 1989"},{"key":"22_CR42","volume-title":"Interactive Synthesis in higher order logic","author":"S. Finn","year":"1991","unstructured":"S. Finn, M.P. Fourman, G. Musgrave, \u201cInteractive Synthesis in higher order logic\u201d, Proc. Intl. Workshop on the HOL Theorem Prover and its applications, Davis, Calif., IEEE Press, 1991"},{"key":"22_CR43","unstructured":"E.M. Mayger, M.P. Fourman, \u201cIntegration of Formal Methods with System Design\u201d, Proc. VLSI-91, Edinburgh, A. Halaas and P.B. Denyer (Eds.), Aug. 1991"},{"key":"22_CR44","doi-asserted-by":"crossref","unstructured":"M. Bombana, P. Cavalloro, G. Zaza, \u201cSpecification and Formal Synthesis of Digital Circuits\u201d, Proc. Higher Order logic Theorem Proving and its Applications, L.J.M. Claesen and M.J.C. Gordon (Eds.), Elsevier Publishers, Vol. A-20, 1993, pp.475\u2013484","DOI":"10.1016\/B978-0-444-89880-7.50036-X"},{"key":"22_CR45","doi-asserted-by":"crossref","unstructured":"R.B. Hughes, M.D. Francis, S.P. Finn, G. Musgrave, \u201cFormal Tools for Tri-State Design in Busses\u201d, Proc. Higher Order logic Theorem Proving and its Applications, L.J.M. Claesen and M.J.C. Gordon (Eds.), Elsevier Publishers, Vol. A-20, 1993, pp.459\u2013474","DOI":"10.1016\/B978-0-444-89880-7.50035-8"},{"key":"22_CR46","series-title":"LNCS, Vol. 901","first-page":"286","volume-title":"Proc. TPCD'94","author":"G. Bezzi","year":"1995","unstructured":"G. Bezzi, M. Bombana, P. Cavalloro, S. Conigliaro, G. Zaza, \u201cQuantitative evaluation of formal based synthesis in ASIC Design\u201d, Proc. TPCD'94, R. Kumar and T. Kropf (Eds.), Bad Herrenalb, Germany, LNCS, Vol. 901, Springer, 1995, pp. 286\u2013291"},{"key":"22_CR47","unstructured":"F.K. Hanna, M. Longley, N. Daeche, \u201cFormal Synthesis of Digital Systems\u201d, Proc. IMEC-IFIP Intl. Workshop on Applied Formal Methods in Correct VLSI Design, L. Claesen (Ed.), North Holland, 1989, pp.532\u2013548"},{"key":"22_CR48","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1098\/rsta.1992.0029","volume":"339","author":"F.K. Hanna","year":"1992","unstructured":"F.K. Hanna, N. Daeche, \u201cDependent types and formal synthesis\u201d, Phil. Trans. R. Soc. Lond., Vol. 339, 1992, pp. 121\u2013135","journal-title":"Phil. Trans. R. Soc. Lond."},{"key":"22_CR49","doi-asserted-by":"crossref","unstructured":"D. Eisenbiegler, R. Kumar \u201cAn Automata Theory Dedicated towards Formal Circuit Synthesis\u201d, Higher Order Logic Theorem Proving and Its Applications HUG'95, Aspen Grove, Utah, USA, September 11\u201314, 1995","DOI":"10.1007\/3-540-60275-5_63"},{"key":"22_CR50","doi-asserted-by":"crossref","unstructured":"D. Eisenbiegler, R. Kumar, \u201cFormally embedding existing high level synthesis algorithms\u201d, Proc. CHARME'95, Springer, LNCS, Vol. 987, pp. 71\u201383","DOI":"10.1007\/3-540-60385-9_5"},{"key":"22_CR51","doi-asserted-by":"crossref","unstructured":"D. Eisenbiegler, C. Blumenr\u00f6hr, R. Kumar, \u201cImplementation Issues about the Embedding of Existing High Level Synthesis Algorithms in HOL\u201d, International Conference on Theorem Proving in Higher Order Logics, TPHOL'96, Turku, Finland, August 27\u201330, 1996","DOI":"10.1007\/BFb0105403"},{"key":"22_CR52","unstructured":"D.A. Basin, G.M. Brown, M. Leeser, \u201cFormally Verified Synthesis of Combinational CMOS Circuits\u201d, \u201cFormal Synthesis of Digital Systems\u201d, Proc. IMEC-IFIP Intl. Workshop on Applied Formal Methods in Correct VLSI Design, L. Claesen (Ed.), North Holland, 1989, pp. 251\u2013260"},{"key":"22_CR53","unstructured":"D. Basin, \u201cExtracting circuits from Constructive Proofs\u201d, ACM\/SIGDA Workshop on Formal Methods in VLSI Design, Miami, Florida, Jan. 1991. (Unfortunately, the proceedings of the workshop have not been officially published)"},{"key":"22_CR54","first-page":"175","volume-title":"Theorem Provers in Circuit Design","author":"H. Busch","year":"1992","unstructured":"H. Busch, \u201cTransformational Design in a Theorem Prover\u201d, Theorem Provers in Circuit Design, V. Stravidou, T.F. Melham and R.T. Boute (Eds.), Elsevier Science Publishers, North-Holland, 1992, pp. 175\u2013196"},{"key":"22_CR55","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/3-540-58450-1_50","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"M. Larsson","year":"1994","unstructured":"M. Larsson, \u201cAn Engineering Approach to Formal System Design\u201d, in Higher Order Logic Theorem Proving and Its Applications, T.F. Melham and J. Camilleri (Eds.), pp. 300\u2013315, Valetta, Malta, September 1994, Springer"},{"key":"22_CR56","doi-asserted-by":"crossref","unstructured":"M. Larsson, \u201cAn Engineering Approach to Formal Digital System Design\u201d, The Computer Journal, Oxford University Press, Vol. 38, No.2, 1995, pp. 101\u2013110","DOI":"10.1093\/comjnl\/38.2.101"},{"key":"22_CR57","volume-title":"Designing Correct Circuits","author":"J.B. Saxe","year":"1992","unstructured":"J.B. Saxe, S.J. Garland, J.V. Guttag, J.J. Horning, \u201cUsing Transformations and Verification in Circuit Design\u201d, Designing Correct Circuits, J. Staunstrup and R. Sharp (Eds.), Elsevier Science Publishers, North-Holland, 1992"},{"key":"22_CR58","doi-asserted-by":"crossref","unstructured":"L. Wang, \u201cDeriving a Correct Computer\u201d, Proc. Higher Order logic Theorem Proving and its Applications, L.J.M. Claesen and M.J.C. Gordon (Eds.), Elsevier Publishers, Vol. A-20, 1992, pp. 449\u2013458","DOI":"10.1016\/B978-0-444-89880-7.50034-6"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0031817","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:50:24Z","timestamp":1586613024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031817"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540619376","9783540495673"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/bfb0031817","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}