Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

A formal framework for high level synthesis

  • Research Papers
  • Conference paper
  • First Online:

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

Included in the following conference series:

Abstract

In this paper, we propose a new approach to formal synthesis which focuses on the generation of verification-friendly circuits. Starting from a high-level implementation description, which may result from the application of usual scheduling and allocation algorithms, hardware is automatically synthesized. The target architecture is based onhandshake processes, modules which communicate by a simple synchronizing handshake protocol. The circuits result from the application of only a few basic operations like synchronization, sequential execution or iteration of base handshake processes. Each process is guided by an abstract theorem that is used to derive proof obligations, to be justified after synthesis. Automation has been achieved to the extend that only those “relevant” proof obligations remain to be proven manually, e.g. theorems for data-dependent loops and lemmata about the used data types. The process-oriented implementation language is enriched by loop invariants. If those are given prior to the synthesis process and the underlying data types are only Booleans, i.e. finite-length bitvectors, then the complete synthesis and verification process runs automatically.

Similar content being viewed by others

Keywords

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. M.C. McFarland, A.C. Parker, and R. Camposano. Tutorial on high-level synthesis. In25th Design Automation Conference, pages 330–336, 1988.

    Google Scholar 

  2. J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Sequential circuit verification using symbolic model checking.27rd ACM/IEEE Design Automation Conference. IEEE, 1990, pages 46–51.

    Google Scholar 

  3. A. Gupta. Formal hardware verification methods: A survey.Journal of Formal Methods in System Design, pages 151–238, 1992.

    Google Scholar 

  4. K. Schneider, R. Kumar, and T. Kropf. Automating verification by functional abstraction at the system level. In T. Melham and J. Camilleri, editors,International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 391–406, Malta, September 1994. Lecture Notes on Computer Science No. 859, Springer.

    Google Scholar 

  5. K. Schneider, R. Kumar, and T. Kropf. Modelling generic hardware structures by abstract datatypes. In L. Claesen and M. Gordon, editors,International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 419–429, Leuven, Belgium, September 1992. IFIP TC10/WG10.2, Elsevier Science Publishers.

    Google Scholar 

  6. M. Mutz. Using the HOL theorem proving environment for proving the correctness of term rewriting rules reducing terms of sequential behavior. In K.G. Larsen and A. Skou.International Workshop on Computer Aided Verification, volume 575 ofLecture Notes in Computer Science. Springer, Aalborg, July 1991, pages 355–366.

    Google Scholar 

  7. E. Mayger and M. P. Fourman. Integration of formal methods with system design. In A. Halaas and P.B. Denyer.International Conference on Very Large Scale Integration, pages 59–70, 1991. Edinburgh, North-Holland.

    Google Scholar 

  8. M. Fujita and H. Fujisawa. Specification, verification and synthesis of control circuits with propositional temporal logic. J.A. Darringer and F.J. Rammig, editors.Computer Hardware Description Languages and their Applications, Washington, June 1989. IFIP WG 10.2, North-Holland, pages 265–279.

    Google Scholar 

  9. S.M. Burns and A.J. Martin. Synthesis of self-timed circuits by program transformation. In G. Milne, editor,The Fusion of Hardware Design and Verification, pages 99–116, Glasgow, Scotland, July 1988. IFIP WG 10.2, North-Holland.

    Google Scholar 

  10. M.J.C. Gordon and T. Melham.Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

    Google Scholar 

  11. F.K. Hanna and N. Daeche. Specification and verification using high-order logic. In C.J. Koomen and T. Moto-oka, editors,Computer Hardware Description Languages, pages 418–433. Elsevier Science Publishers, North-Holland, 1985.

    Google Scholar 

  12. E. A. Emerson.Temporal and Modal Logics, chapter 16, pages 996–1072. Elsevier Science Publishers, 1990.

    Google Scholar 

  13. F. Kröger.Temporal Logic of Programs, volume 8 ofEATCS Monographs on Theoretical Computer Science. Springer Verlag, 1987.

    Google Scholar 

  14. K. Schneider, T. Kropf, and R. Kumar. Control-path oriented verification of sequential generic circuits with control and data path. In4th European Design Automation Conference, pages 648–652, Paris, France, March 1994. IEEE Computer Society Press.

    Google Scholar 

  15. T. Melham. Abstraction mechanisms for hardware verification. In G. Birtwistle and P.A. Subrahmanyam, editors,VLSI Specification, Verification and Synthesis, pages 267–291. Kluwer Academic Press, 1988.

    Google Scholar 

  16. K. Schneider, T. Kropf, and R. Kumar. Why hardware verification needs more than model checking. InInternational Workshop on Higher Order Logic Theorem Proving and its Applications, Malta, 1994, Short Paper.

    Google Scholar 

  17. R. Kumar, K. Schneider, and T. Kropf. Structuring and automating hardware proofs in a higher-order theorem-proving environment.International Journal of Formal System Design, pages 165–230, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Rechnerentwurf und Fehlertoleranz, Universität Karlsruhe, Kaiserstr. 12, 76128, Karlsruhe, Germany

    Thomas Kropf & Klaus Schneider

  2. FZI, Haid-und-Neu-Str.10-14, 76131, Karlsruhe, Germany

    Ramayya Kumar

Authors
  1. Thomas Kropf

    You can also search for this author inPubMed Google Scholar

  2. Klaus Schneider

    You can also search for this author inPubMed Google Scholar

  3. Ramayya Kumar

    You can also search for this author inPubMed Google Scholar

Editor information

Ramayya Kumar Thomas Kropf

Rights and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kropf, T., Schneider, K., Kumar, R. (1995). A formal framework for high level synthesis. In: Kumar, R., Kropf, T. (eds) Theorem Provers in Circuit Design. TPCD 1994. Lecture Notes in Computer Science, vol 901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59047-1_51

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp