Automatic Formal Derivation Applied to High-Level Synthesis

  • José Manuel Mendías
  • Román Hermida


Since the early 80’s, when first high-level synthesis (HLS) algorithms appeared, behavioral synthesis tools have had to evolve quickly. From day to day new fields of application are being discovered that require to review the old techniques. Continuously, the market is requiring new algorithms able to perform more efficient search of solutions. Everyday more abstract specification methods are required, which enlarge the semantic gap between specification and circuit. And all this development has got a price to be paid: the complexity of algorithms grows and the supporting data structures become more sophisticated. As a consequence, the bugs in the tools (or even in the algorithms) proliferate. The effect is that reliance in synthesis tools decreases and nowadays no sensible designer takes the risk to accept a circuit automatically generated without a later validation step; either using simulation or verification techniques. This means, in practice, that the well-known paradigm of correctness by construction, widely publicized formerly, has to be handled very carefully.


Output Port Input Port Schedule Length Operation Symbol Hardware Module 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [B1Ei97]
    C. Blumenröhr and D. Eisenbiegler. An efficient representation for formal synthesis, Proc. International symposium on system synthesis, ISSS’97, 1997.Google Scholar
  2. [De1g87]
    C. Delgado. Sematics of digital circuits, LNCS-285, Springer Verlag, 1987.CrossRefGoogle Scholar
  3. [EhMa85]
    H. Ehrig and B. Mahr. Fundamentals of algebraic specification l: equations and initial semantics, EATCS Monographs on theoretical computer science, n°6, Springer-Verlag, 1985.Google Scholar
  4. [FiFM91]
    S. Finn, M.P. Fourman and G. Musgrave. Interactive synthesis in higher order logic, Proc. Workshop on the HOL theorem prover and its applications, 1991.Google Scholar
  5. [JoBo91]
    S.D. Johnson and B. Bose. DDD - A system for mechanized digital design derivation, Proc. International Workshop on Formal Methods in VLSI Design, 1991.Google Scholar
  6. [John89]
    S.D. Johnson. Manipulating logical organization with system factorizations, Hardware specification, verification and synthesis: mathematical aspects, LNCS-408, Springer-Verlag, 1989.Google Scholar
  7. [JoSh90]
    G. Jones and M. Sheeran. Circuit design in Ruby, Formal Methods for VLSI Design, ed. J. Staunstrup, North Holland, 1990.Google Scholar
  8. [Kuma96]
    R. Kumar et al. Formal synthesis in circuit design - A classification and survey, Proc. Formal methods in CAD, FMCAD’96, 1996.Google Scholar
  9. [MeHF96]
    J.M. Mendfas, R. Hermida and M. Fernandez. Algebraic support for transformational hardware allocation, Proc. European Design & Test Conference, EDTC’96, 1996.Google Scholar
  10. [MeHF97]
    J.M. Mendfas, R. Hermida and M. Fernandez. Formal techniques for hardware allocation, Proc. International conference on VLSI design, VLSI’97, 1997.Google Scholar
  11. [Pada88]
    P. Padawitz. Computing in Horn Clause Theories, EATCS Monographs on theoretical computer science, 16, Springer-Verlag, 1988.Google Scholar
  12. [ShRa95]
    R. Sharp and O. Rasmussen. The T-Ruby design system, Proc. Computer hardware description languages and their applications, CHDL’95, 1995.Google Scholar
  13. [Stoy77]
    J.E. Stoy. Denotational semantics: The Scott-Strachey approach to programming languaje theory, The MIT Press Series in Computer Science, 1, MIT Press, 1977.Google Scholar
  14. [WaAs85]
    W.W. Wadge and E.A. Ashcroft. Lucid, the dataflow programming language, APIC Studies in data processing, 22, Academic Press, 1985.Google Scholar

Copyright information

© Springer Science+Business Media Dordrecht 1998

Authors and Affiliations

  • José Manuel Mendías
  • Román Hermida

There are no affiliations available

Personalised recommendations