Advertisement

Formally embedding existing high level synthesis algorithms

  • Dirk Eisenbiegler
  • Ramayya Kumar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)

Abstract

This paper introduces a general scheme for formally embedding high level synthesis by formulating its basic steps as transformations within higher order logic. A functional representation of a data flow graph is successively refined by means of generic logical transformations. Algorithms that are based on logical transformations guarantee “correctness by design”. They not only construct an implementation but also derive the proof for its formal correctness, on the fly. An extra postsynthesis-verification step becomes obsolete. The logical transformations presented in this paper form a framework for formally embedding existing high-level-synthesis procedures.

Keywords

Communication Scheme Register Binding Auxiliary Variable High Order Logic Synthesis Algorithm 
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.

References

  1. [AHL92]
    AHL. Lambda Reference Manual, 1989.Google Scholar
  2. [CaWo91]
    R. Camposano and W. Wolf. High-Level VLSI Synthesis. Kluwer, Boston, 1991.Google Scholar
  3. [Davi89]
    R. E. Davis. Truth, Deduction, and Computation: Logic and Semantics for Computer Science. Computer Science Press, New York, 1 edition, 1989.Google Scholar
  4. [Day92]
    Nancy Day. A comparison between statecharts and state transition assertions. In Luc Claesen and Michael Gordon, editors, Higher Order Logic Theorem Proving and Its Applications, pages 247–262, Leuven, Belgium, November 1992. North-Holland.Google Scholar
  5. [FoMa90]
    M.P. Fourman and E.M. Mayger. Formally Based System Design — Interactive hardware scheduling. In G. Musgrave and U. Lauter, editors, International Conference on Very Large Scale Integration, pages 101–112. Elsevier Science Publishers (North-Holland), 1990.Google Scholar
  6. [GoMe93]
    M.J.C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.Google Scholar
  7. [Gupt92]
    A. Gupta. Formal hardware verification. Formal Methods in System Design, 1(2/3):151–238, 1992.Google Scholar
  8. [HaLD89]
    F.K. Hanna, M. Longley, and N. Daeche. Formal synthesis of digital systems. In IMEC-IFIP Workshop on Applied Formal Methods for Correct VLSI Design, pages 532–548, Leuven,Belgium, 1989. Elsevier Science Publishers B.V.Google Scholar
  9. [John84]
    S. D. Johnson. Synthesis of Digital Designs from Recursion Equations. MIT Press, 1984.Google Scholar
  10. [JoWB89]
    S.D. Johnson, R.M. Wehrmeister, and Bhaskar Bose. On the interplay of synthesis and verification. In IMEC-IFIP Workshop on Applied Formal Methods for Correct VLSI Design, pages 385–404, Leuven,Belgium, 1989. Elsevier Science Publishers B.V.Google Scholar
  11. [Lars94]
    M. Larsson. An engineering approach to formal system design. In Thomas F. Melham and Juanito Camilleri, editors, Higher Order Logic Theorem Proving and Its Applications, pages 300–315, Valetta, Malta, September 1994. Springer.Google Scholar
  12. [Loew92]
    Paul Loewenstein. A formal theory of simulations between infinite automata. In Luc Claesen and Michael Gordon, editors, Higher Order Logic Theorem Proving and Its Applications, pages 227–246, Leuven, Belgium, November 1992. North-Holland.Google Scholar
  13. [MaFo91]
    E.M. Mayger and M.P. Fourman. Integration of formal methods with system design. In A. Halaas and P.B. Denyer, editors, International Conference on Very Large Scale Integration, pages 59–70, Edinburgh, Scotland, August 1991. IFIP Transactions, North-Holland.Google Scholar
  14. [Melh93]
    T. Melham. Higher Order Logic and Hardware Verification. Cambridge University Press, 1993.Google Scholar
  15. [Paul91]
    P. G. Paulin. Global Scheduling and Allocation Algorithms in the HAL System. In R. Camposano and W. Wolf, editors, High-Level VLSI Synthesis, pages 255–281. Kluwer Academic Publishers, 1991.Google Scholar
  16. [RoKr91]
    W. Rosenstiel and H. KrÄmer. Scheduling and Assignment in High Level Synthesis. In R. Camposano and W. Wolf, editors, High-Level VLSI Synthesis, pages 355–382. Kluwer Academic Publishers, 1991.Google Scholar
  17. [ScKK93]
    K. Schneider, R. Kumar, and Thomas Kropf. Alternative proof procedures for finite-state machines in higher-order logic. In Jeffrey J. Joyce and Carl-Johan H. Seger, editors, Higher Order Logic Theorem Proving and Its Applications, pages 213–226, Vancouver, B.C., Canada, August 1993. Springer.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Dirk Eisenbiegler
    • 1
  • Ramayya Kumar
    • 1
  1. 1.Forschungszentrum InformatikKarlsruheGermany

Personalised recommendations