Formal Synthesis at the Algorithmic Level

  • Christian Blumenröhr
  • Viktor Sabelfeld
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


In our terminology, the term “formal synthesis” stands for a synthesis process where the implementation is derived from the specification by applying elementary mathematical rules within a theorem prover. As a result the implementation is guaranteed to be correct. In this paper we introduce a new methodology to formally derive register-transfer structures from descriptions at the algorithmic level via program transformations. Some experimental results at the end of the paper show how the run-time complexity of the synthesis process in our approach could be.


Synthesis Process Basic Block Program Transformation Design Space Exploration Algorithmic Level 
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.


  1. 1.
    A. Gupta. Formal hardware verification methods: A survey. Formal Methods in System Design, 1(2/3):151–238, 1992.CrossRefGoogle Scholar
  2. 2.
    P. Middelhoek. Transformational Design. PhD thesis, Univ. Twente,NL, 1997.Google Scholar
  3. 3.
    M. McFarland. Formal analysis of correctness of behavioral transformations. Formal Methods in System Design, 2(3), 1993.Google Scholar
  4. 4.
    Z. Peng, K. Kuchcinski. Automated transformation of algorithms into register-transfer implementations. IEEE Transactions on CAD, 13(2):150–166, 1994.Google Scholar
  5. 5.
    R. Camposano. Behavior-preserving transformations for high-level synthesis. In Hardware Specification, Verification and Synthesis: Mathematical Aspects, number 408 in LNCS, pp. 106–128, Ithaca, New York, 1989. Springer.Google Scholar
  6. 6.
    S. D. Johnson, B. Bose. DDD: A system for mechanized digital design derivation. In Int. Workshop on Formal Methods in VLSI Design, Miami, Florida, 1991. Available via “” (rev. 1997).
  7. 7.
    M. J. C. Gordon, T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.Google Scholar
  8. 8.
    R. Sharp, O. Rasmussen. The T-Ruby design system. In IFIP Conference on Hardware Description Languages and their Applications, pp. 587–596, 1995.Google Scholar
  9. 9.
    E. M. Mayger, M. P. Fourman. Integration of formal methods with system design. In Int. Conf. on VLSI,pp. 59–70, Edinburgh,Scotland, 1991. North-Holland.Google Scholar
  10. 10.
    R. Kumar et al. Formal synthesis in circuit design-A classification and survey. In FMCAD’96, number 1166 in LNCS, pp. 294–309, Palo Alto, CA, 1996. Springer.Google Scholar
  11. 11.
    F. K. Hanna et al. Formal synthesis of digital systems. In Applied Formal Methods For Correct VLSI Design, volume 2, pp. 532–548. Elsevier, 1989.Google Scholar
  12. 12.
    M. Larsson. An engineering approach to formal digital system design. The Computer Journal, 38( 2):101–110, 1995.CrossRefMathSciNetGoogle Scholar
  13. 13.
    D. Gajski et al. High-Level Synthesis, Introduction to Chip and System Design. Kluwer, 1992.Google Scholar
  14. 14.
    H.P. Barendregt. Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, chapter 7: Functional Programming and Lambda Calculus, pp. 321–364. Elsevier, 1992.Google Scholar
  15. 15.
    A. Aho et al. Compilers: Principles, Techniques and Tools. Addison Wesley, 1986.Google Scholar
  16. 16.
    P. G. Paulin, J. P. Knight. Force-directed scheduling for the behavioral synthesis of ASIC’s. IEEE Transactions on CAD, 8(6):661–679, 1989.Google Scholar
  17. 17.
    C. Blumenröhr. A formal approach to specify and synthesize at the system level. In GI Workshop Modellierung und Verifikation von Systemen, pp. 11–20,Braunschweig, Germany, 1999. Shaker-Verlag.Google Scholar
  18. 18.
    D. Eisenbiegler, R. Kumar. An automata theory dedicated towards formal circuit synthesis.In TPHOL’95,number 971 in LNCS,pp. 154–169, Aspen Grove, Utah, 1995. Springer.Google Scholar
  19. 19.
    D. Eisenbiegler et al. Implementation issues about the embedding of existing high level synthesis algorithms in HOL. In TPHOLs’96, number 1125 in LNCS, pp. 154–169, Turku, Finland, 1996. Springer.Google Scholar
  20. 20.
    J. Gerlach, W. Rosenstiel. A Scalable Methodology for Cost Estimation in a Transformational High-Level Design Space Exploration Environment. In DATE’98, pp. 226–231,Paris, France, 1998. IEEE Computer Society.Google Scholar
  21. 21.
  22. 22.
    C. Blumenröhr et al. On the efficiency of formal synthesis —experimental results. IEEE Transactions on CAD, 18(1):25–32, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Christian Blumenröhr
    • 1
  • Viktor Sabelfeld
    • 1
  1. 1.Institute for Circuit Design and Fault ToleranceUniversity of KarlsruheGermany

Personalised recommendations