Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Methods in Computer-Aided Design

FMCAD 1996: Formal Methods in Computer-Aided Design pp 294–309Cite as

Formal synthesis in circuit design — A classification and survey

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1166))

Abstract

This article gives a survey on different methods of formal synthesis. We define what we mean by the term formal synthesis and delimit it from the other formal methods that can also be used to guarantee the correctness of an implementation. A possible classification scheme for formal synthesis methods is then introduced, based on which some significant research activities are classified and summarized. We also briefly introduce our own approach towards the formal synthesis of hardware. Finally, we compare these approaches from different points of view.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

General

  1. R.K. Brayton, C. McMullen, “Decomposition and factorization of boolean expressions”, Proc. International Symposium on Circuits and Systems, IEEE Computer Society, 1982

    Google Scholar 

  2. H. Eveking, “Verification, Synthesis and Correctness-Preserving Transformations — Cooperative Approaches to Correct Hardware Design”, From HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione (Ed.), Elsevier Science Publishers North-Holland, 1987

    Google Scholar 

  3. M. Gordon, T. Melham, “Introduction to HOL: A Theorem Proving Environment for Higher Order Logic”, Cambridge University Press, 1993

    Google Scholar 

  4. A. Gupta, “Formal Hardware Verification Methods: A Survey”, Formal Methods in System Design, Kluwer Academic Publishers, Vol. 1, 1992, pp.151–238

    Google Scholar 

  5. M. Leeser, “Using Nuprl for the verification and synthesis of hardware”, Phil. Trans. R. Soc. Lond., Vol. 339, 1992, pp. 49–68

    Google Scholar 

  6. M. Leeser, M. Aagaard, M. Linderman, “The BEDROC High Level Synthesis System”, Proc. ASIC'91, IEEE, 1991

    Google Scholar 

  7. M. Leeser, R. Chapman, M. Aagaard, M. Linderman, S. Meier, “High level Synthesis and Generating FPGAs with the BEDROC System”, Journal of VLSI Signal Processing, Kluwer Academic Publishers, Vol. 6, No.2, Aug. 1993, pp.191–214

    Google Scholar 

  8. M. C. McFarland, A.C. Parker, R. Camposano, “The high-level Synthesis of Digital Systems”, Proc. of IEEE, Vol. 78, 1990, pp. 301–318

    Google Scholar 

Pre-Synthesis Verification

  1. M. Aagaard, M. Leeser, “A Formally verified system for logic synthesis”, Proc. ICCD-91, IEEE, Oct. 1991

    Google Scholar 

  2. M. Aagaard, M. Leeser, “PBS: Proven Boolean Simplification”, IEEE Trans. on Computer Aided Design, Vol. 13, No.4, Apr. 1994

    Google Scholar 

  3. M. Aagaard, M. Leeser, “Verifying a logic synthesis algorithm and implementation: A case study in software verification”, IEEE Trans. on Software Engineering, Oct. 1995

    Google Scholar 

Synthesis Step Specific Verification

  1. C.A.J. van Eijk, J.A.G. Jess, “Exploiting Functional Dependencies in Finite State Machine Verification”, Proc. European Design & Test Conference 1996, Paris, pp. 9–14, IEEE Computer Society Press

    Google Scholar 

  2. Huang, Cheng, Chen, “On Verifying the Correctness of Retimed Circuits”, Great Lakes Symposium on VLSI 1996, Ames, USA

    Google Scholar 

hardware-specific calculus DDD

  1. S.D. Johnson, “Synthesis of Digital Designs from Recursion Equations”, MIT Press, Cambridge, 1984

    Google Scholar 

  2. S.D. Johnson, B. Bose, C.D. Boyer, “A Tactical Framework for Digital Design”, VLSI Specification, Verification and Synthesis, G. Birtwistle and P. Subrahmanyam, Eds., Kluwer Academic Publishers, Boston, 1988, pp. 349–383

    Google Scholar 

  3. S.D. Johnson, “Manipulation logical organization with system factorizations”, Hardware Specification, Verification and Synthesis: Mathematical Aspects, Leeser and Brown (Eds.), LNCS, Vol. 408, Springer, 1989

    Google Scholar 

  4. S.D. Johnson, R. Wehrmeister, B. Bose, “On the Interplay of Synthesis and Verification”, Proc. IMEC-IFIP Intl. Workshop on Applied Formal Methods in Correct VLSI Design, L. Claesen (Ed.), North Holland, 1989, pp. 385–404

    Google Scholar 

  5. S.D. Johnson, B. Bose, “DDD — A System for Mechanized Digital Design Derivation”, ACM/SIGDA Workshop on Formal Methods in VLSI Design, Miami, Florida, Jan. 1991. (Unfortunately, the proceedings of the workshop have not been officially published)

    Google Scholar 

  6. B. Bose, S.D. Johnson, “DDD-FM9001: Derivation of a verified microprocessor. An exercise in integrating verification with formal derivation”, Proc. IFIP Conf. on Correct Hardware Design and Verification Methods, LNCS, Vol., Springer, 1993

    Google Scholar 

  7. K.Rath, B. Bose, S.D. Johnson, “Derivation of a DRAM Memory Interface by Sequential Decomposition, Proc. Intl. Conf. on Computer Design — ICCD, IEEE, Oct. 1993, pp.438–441

    Google Scholar 

  8. K. Rath, M.E. Tuna, S.D. Johnson, “An Introduction to Behaviour Tables”, Tech. Rep. No. 392, Indiana University, Computer Science Department, December, 1993

    Google Scholar 

  9. Z. Zhu, S.D. Johnson, “An Example of Interactive Hardware Transformation”, Tech. Rep. No. 383, Indiana University, Computer Science Department, May, 1993

    Google Scholar 

Rlext

  1. D.W. Knapp, M. Winslett, “A Formalization of Correctness for Linked Representations of Datapath Hardware”, Proc. IMEC-IFIP Intl. Workshop on Applied Formal Methods in Correct VLSI Design, L. Claesen (Ed.), North Holland, 1989, pp. 1–20

    Google Scholar 

  2. D.W. Knapp, M. Winslett, “A Prescriptive Model for Data-path Hardware”, IEEE Trans. on Computer Aided Design, Vol. 11, No.2, Feb. 1992

    Google Scholar 

Ruby

  1. M. Sheeran, “Retiming and slowdown in Ruby”, The fusion of hardware design and verification, G.J. Milne (Ed.), North-Holland, 1988, pp. 245–259

    Google Scholar 

  2. G. Jones, M. Sheeran, “Circuit design in Ruby”, Formal Methods for VLSI design, J. Staunstrup (Ed.), North-Holland, 1990, pp. 13–70

    Google Scholar 

  3. L. Rossen, “Formal Ruby”, Formal Methods for VLSI design, J. Staunstrup (Ed.), North-Holland, 1990, pp. 179–190

    Google Scholar 

  4. L. Rossen, “Ruby Algebra”, Designing Correct Circuits, Oxford, G. Jones and M. Sheeran (Eds.), Springer, 1990, pp. 297–312

    Google Scholar 

  5. G. Jones, M. Sheeran, “Deriving bit-serial circuits in Ruby”, Proc. VLSI-91, Edinburgh, A. Halaas and P.B. Denyer (Eds.), Aug. 1991

    Google Scholar 

  6. G. Jones, M. Sheeran, “Relations and refinements in circuit design”, proc. 3rd Refinement Workshop, C.C. Morgan and J.C.P. Woodcock (Eds.), Springer, 1991, pp. 133–152

    Google Scholar 

  7. R. Sharp, O. Rasmussen, “Transformational Rewriting with Ruby”, Proc. CHDL-93, D. Agnew, L. Claesen and R. Camposano (Eds.), Elsevier Science Publishers, 1993, pp.243–260

    Google Scholar 

  8. R. Sharp, O. Rasmussen, “The T-Ruby Design System”, Computer Hardware Description Languages and their Applications (CHDL'95), pp. 587–596, 1995

    Google Scholar 

Miscellaneous

  1. T. Kropf, K. Schneider, R. Kumar, “A Formal Framework for High Level Synthesis”, in TPCD-94, Bad Herrenalb, Germany, R. Kumar and T. Kropf (Eds.), LNCS, Springer, Vol. 901, 1995, pp. 223–238

    Google Scholar 

  2. G.C. Gopalakrishnan, M.K. Srivas, D.R. Smith, “From Algebraic Specifications to Correct VLSI Circuits”, From HDL Descriptions to guaranteed Correct Design, D. Borrione (Ed.), Elsevier Science Publishers, North-Holland, 1987

    Google Scholar 

  3. W. Grass, R. Rauscher, “CAMILOD — A Program System for Designing Digital hardware with Proven Correctness”, From HDL Descriptions to guaranteed Correct Design, D. Borrione (Ed.), Elsevier Science Publishers, North-Holland, 1987

    Google Scholar 

  4. T. Uehara, “Proofs and Synthesis are Cooperative Approaches for Correct Circuit Designs”, From HDL Descriptions to guaranteed Correct Design, D. Borrione (Ed.), Elsevier Science Publishers, North-Holland, 1987

    Google Scholar 

  5. R. Camposano, “Behaviour-preserving Transformations for High-level Synthesis”, Proc. Workshop on hardware Specification, Verification and Synthesis: Mathematical Aspects, Leeser and Brown (Eds.), LNCS, Vol. 408, Springer, 1989

    Google Scholar 

  6. D. Druinsky, D. Harel, “Using State-Charts for hardware Description and Synthesis” IEEE Trans. on CAD, Vol. 8, No.7, July, 1989, pp. 798–807

    Google Scholar 

  7. W. Grass, M. Mutz, W.D. Tiedemann, “High-level-Synthesis Based on Formal Methods”, Proc. EUROMICRO '94, Liverpool, 1994, 83–91

    Google Scholar 

General Purpose calculus Lambda

  1. S. Finn, M.P. Fourman, M. Francis, R. Harris, “Formal System Design — Interactive Synthesis based on computer-assisted formal reasoning”, Proc. IMEC-IFIP Intl. Workshop on Applied Formal Methods in Correct VLSI Design, L. Claesen (Ed) North Holland, 1989, pp.97–110

    Google Scholar 

  2. M.P. Fourman, E.M. Mayger, “Formally based systems design — Interactive hardware scheduling”, VLSI-89, G. Musgrave and U. Lauther (Eds.), Munich, North Holland, 1989

    Google Scholar 

  3. S. Finn, M.P. Fourman, G. Musgrave, “Interactive Synthesis in higher order logic”, Proc. Intl. Workshop on the HOL Theorem Prover and its applications, Davis, Calif., IEEE Press, 1991

    Google Scholar 

  4. E.M. Mayger, M.P. Fourman, “Integration of Formal Methods with System Design”, Proc. VLSI-91, Edinburgh, A. Halaas and P.B. Denyer (Eds.), Aug. 1991

    Google Scholar 

  5. M. Bombana, P. Cavalloro, G. Zaza, “Specification and Formal Synthesis of Digital Circuits”, 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–484

    Google Scholar 

  6. R.B. Hughes, M.D. Francis, S.P. Finn, G. Musgrave, “Formal Tools for Tri-State Design in Busses”, 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–474

    Google Scholar 

  7. G. Bezzi, M. Bombana, P. Cavalloro, S. Conigliaro, G. Zaza, “Quantitative evaluation of formal based synthesis in ASIC Design”, Proc. TPCD'94, R. Kumar and T. Kropf (Eds.), Bad Herrenalb, Germany, LNCS, Vol. 901, Springer, 1995, pp. 286–291

    Google Scholar 

Veritas

  1. F.K. Hanna, M. Longley, N. Daeche, “Formal Synthesis of Digital Systems”, Proc. IMEC-IFIP Intl. Workshop on Applied Formal Methods in Correct VLSI Design, L. Claesen (Ed.), North Holland, 1989, pp.532–548

    Google Scholar 

  2. F.K. Hanna, N. Daeche, “Dependent types and formal synthesis”, Phil. Trans. R. Soc. Lond., Vol. 339, 1992, pp. 121–135

    Google Scholar 

Hash

  1. D. Eisenbiegler, R. Kumar “An Automata Theory Dedicated towards Formal Circuit Synthesis”, Higher Order Logic Theorem Proving and Its Applications HUG'95, Aspen Grove, Utah, USA, September 11–14, 1995

    Google Scholar 

  2. D. Eisenbiegler, R. Kumar, “Formally embedding existing high level synthesis algorithms”, Proc. CHARME'95, Springer, LNCS, Vol. 987, pp. 71–83

    Google Scholar 

  3. D. Eisenbiegler, C. Blumenröhr, R. Kumar, “Implementation Issues about the Embedding of Existing High Level Synthesis Algorithms in HOL”, International Conference on Theorem Proving in Higher Order Logics, TPHOL'96, Turku, Finland, August 27–30, 1996

    Google Scholar 

Miscellaneous

  1. D.A. Basin, G.M. Brown, M. Leeser, “Formally Verified Synthesis of Combinational CMOS Circuits”, “Formal Synthesis of Digital Systems”, Proc. IMEC-IFIP Intl. Workshop on Applied Formal Methods in Correct VLSI Design, L. Claesen (Ed.), North Holland, 1989, pp. 251–260

    Google Scholar 

  2. D. Basin, “Extracting circuits from Constructive Proofs”, ACM/SIGDA Workshop on Formal Methods in VLSI Design, Miami, Florida, Jan. 1991. (Unfortunately, the proceedings of the workshop have not been officially published)

    Google Scholar 

  3. H. Busch, “Transformational Design in a Theorem Prover”, Theorem Provers in Circuit Design, V. Stravidou, T.F. Melham and R.T. Boute (Eds.), Elsevier Science Publishers, North-Holland, 1992, pp. 175–196

    Google Scholar 

  4. M. Larsson, “An Engineering Approach to Formal System Design”, in Higher Order Logic Theorem Proving and Its Applications, T.F. Melham and J. Camilleri (Eds.), pp. 300–315, Valetta, Malta, September 1994, Springer

    Google Scholar 

  5. M. Larsson, “An Engineering Approach to Formal Digital System Design”, The Computer Journal, Oxford University Press, Vol. 38, No.2, 1995, pp. 101–110

    Google Scholar 

  6. J.B. Saxe, S.J. Garland, J.V. Guttag, J.J. Horning, “Using Transformations and Verification in Circuit Design”, Designing Correct Circuits, J. Staunstrup and R. Sharp (Eds.), Elsevier Science Publishers, North-Holland, 1992

    Google Scholar 

  7. L. Wang, “Deriving a Correct Computer”, 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–458

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Automation in Circuit Design, Forschungszentrum Informatik, Karlsruhe, Germany

    Ramayya Kumar & Detlef Schmid

  2. Institute of Computer Design and Fault Tolerance, University of Karlsruhe, Germany

    Christian Blumenröhr, Dirk Eisenbiegler & Detlef Schmid

Authors
  1. Ramayya Kumar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christian Blumenröhr
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Dirk Eisenbiegler
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Detlef Schmid
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mandayam Srivas Albert Camilleri

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kumar, R., Blumenröhr, C., Eisenbiegler, D., Schmid, D. (1996). Formal synthesis in circuit design — A classification and survey. In: Srivas, M., Camilleri, A. (eds) Formal Methods in Computer-Aided Design. FMCAD 1996. Lecture Notes in Computer Science, vol 1166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0031817

Download citation

  • DOI: https://doi.org/10.1007/BFb0031817

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61937-6

  • Online ISBN: 978-3-540-49567-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation