Skip to main content
SpringerLink
Log in

Combined Formal Post- and Presynthesis Verification in High Level Synthesis

  • Conference paper
  • First Online:
Formal Methods in Computer-Aided Design (FMCAD 1998)

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

Included in the following conference series:

Abstract

We propose a formal framework based on higher order logic theorem proving as a support for high level synthesis. We suppose that the design process starts from a behavioural or functional specification in terms of a VHDL description. It produces a structural description at the register transfer level. We propose a method for proving the correctness of synthesis results combining the advantages of presynthesis and postsynthesis verification. To perform the postsynthesis task automatically and efficiently correctness-implying properties of an intermediate synthesis result are checked.

This work is supported by the Deutsche Forschungsgemeinschaft under project no. GR 1006/21 (FORVERTIS)

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Achatz. SUSAN: System for universal scheduling and allocation. In SASIMI Synthesis and Simulation Meeting and International Interchange, pages 138–44, 1993.

    Google Scholar 

  2. D. A. Basin, G. M. Brown, and M. E. Leeser. Formally verified synthesis of combinational CMOS circuits. In L. Claesen, editor, Applied Formal Methods for Correct VLSI Design, pages 251–260. Oganizing Commitee of the IMEC-IFIP-Workshop, November1989.

    Google Scholar 

  3. A. Bartsch, H. Eveking, H.-J. Faerber, M. Kelelatchew, J. Pinder, and U. Schellin. LOVERT-a logic verifier of register-transfer level description. In L. Claesen, editor, Applied Formal Methods for Correct VLSI Design, pages 522–531. Organizing Commitee of the IMEC-IFIP-Workshop, November 1989.

    Google Scholar 

  4. C. Blumenröhr, D. Eisenbiegler, and R. Kumar. Implementation issues about the embedding of existing high level synthesis algorithms in HOL. In Joakim Wright, editor, Theorem proving in higher order logics, pages 165–172. Springer, August1996. LNCS 1125.

    Google Scholar 

  5. D. Basin and S. Friedrich. Modelling a hardware synthesis methodology in Isabelle. In G. Goos, J. Hartmanis, and J. van Leeuwen, editors, Theorem Proving in Higher Order Logics, pages 33–50. Springer, August 1996. LNCS 1125.

    Google Scholar 

  6. H. Barringer, G. Gough, B. Monahan, and A. Williams. Formal support for the ELLA hardware description language. In Paulo E. Camurati and Hans Eveking, editors, Formal Methods in Computer Aided Design, pages 225–245. Springer, July 1995. LNCS987.

    Google Scholar 

  7. R. J. Boulton. CLaReT user’s manual. Technical report, University of Cambridge, Computer Laboratory, 1995.

    Google Scholar 

  8. R. J. Boulton. A single language for specifying abstract syntax trees, lexical analysis, parsing and pretty printing. Technical report, University of Cambridge, Computer Laboratory, 1996.

    Google Scholar 

  9. D. Borrione and A. Salem. Proving an on-line multiplier with OBJ3 and TACHE: A practical experience. In L. Claesen, editor, Applied Formal Methods for Correct VLSI Design, pages 271–280. Organizing Commitee of the IMEC-IFIP-Workshop, November 1989.

    Google Scholar 

  10. Bhaskar Bose, M. Esen Tunar, and Venkatesh Choppella. A tutorial on digital design derivation using DRS. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer Aided Design, pages 270–274. Springer, September 1996. LNCS 1166.

    Chapter  Google Scholar 

  11. F. J. Cantu, A. Bundy, A. Smaill, and D. Basin. Experiments in automating hardware verification using inductive proof planning. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer Aided Design, pages 94–108. Springer, September1996. LNCS 1166

    Chapter  Google Scholar 

  12. Solange Coupet-Grimal and Line Jakubier. Coq and hardware verification: A case study. In G. Goos, J. Hartmanis, and J. van Leeuwen, editors, Theorem Proving in Higher Order Logics, pages 125–140. Springer, August 1996. LNCS 1125

    Google Scholar 

  13. Sergio R. Ramirez Chavez. Formal proof of the cascading property of a parallel sorting circuit. In L. Claesen, editor, Applied Formal Methods for Correct VLSI Design, pages 338–346. Organizing Commitee of the IMEC-IFIP-Workshop, November 1989.

    Google Scholar 

  14. L. Claesen, F. Proesmans, E. Verlind, and H. DeMan. SFG-tracing: A formal verification methodology. In ACM-SIGDA Workshop, February 1990. Miami.

    Google Scholar 

  15. C. Delgado Kloos and P. T. Breuer, editors. Formal Semantics for VHDL. Kluwer Academic Publishers, 1995.

    Google Scholar 

  16. S. Finn, M. P. Fourman, M. Francis, and R. Harris. Formal system design — interactive synthesis based on computer-assisted formal reasoning. In L. Claesen, editor, Workshop on Applied Formal Methods for Correct VLSI Design, pages 97–110, 1989. North Holland.

    Google Scholar 

  17. D. Gajski, N. Dutt, A Wu, S. Lin, et al. High Level Synthesis: Introduction to Chip and System Design. Kluwer Academic Publishers, 1992.

    Google Scholar 

  18. 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 

  19. W. Grass, M. Mutz, and W.-D. Tiedemann. High level synthesis based on formal methods. In EUROMICRO’ 94, pages 83–91, 1994. Liverpool (Great Britain).

    Google Scholar 

  20. A. A. Jerraya, H. Ding, P. Kission, and M. Rahmouni. Behavioral Synthesis and Component Reuse with VHDL. Kluwer Academic Publishers, 1992.

    Google Scholar 

  21. G. G. de Jong. Generalized Data Flow Graphs — Theory and Applications. PhD thesis, Eindhoven, 1993. Cip-Gegevens Koninklijke Bibliotheek, Den Haag.

    Google Scholar 

  22. R. Kumar, C. Blumenröhr, D. Eisenbiegler, and D. Schmid. Formal synthesis in circuit design— a classification and survey. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer Aided Design, pages 294–309. Springer, September 1996. LNCS 1166

    Chapter  Google Scholar 

  23. M. Larsson. An engineering approach to formal digital system design. The Computer Journal, 38(2):101–10, 1995.

    Article  MathSciNet  Google Scholar 

  24. Th. Lock and M. Mutz. FORVERTIS: Projektbericht. Technical report, UniversitÄt Passau, Lehrstuhl für Rechnerstrukturen, Oktober 1997.

    Google Scholar 

  25. Th. Lock and M. Mendler. Formale Modellierung von kontrollflu\dominierten High-Level-Synthese-Eingabebeschreibungen zur Verifikation von Ergebnissen kontrollflu\gesteuerter Einplanungsverfahren. In F. J. Rammig and W. Müller, editors, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, pages 75–84. GI/ITG/GMM, HNI-Verlagsschriftenreihe, MÄrz 1998. Paderborn.

    Google Scholar 

  26. S. S. Leung and M. A. Shanblatt. ASIC System Design with VHDL: A Paradigm. Kluwer Academic Publishers, 1989.

    Google Scholar 

  27. P. Michel, U. Lauther, and P. Duzy. The Synthesis Approach to Digital System Design. Kluwer Academic Publishers, 1992.

    Google Scholar 

  28. M. Mutz. Presynthesis proof and postsynthesis tactic for pure dataflow descriptions in high level synthesis. http://acrux.fmi.uni-passau.de/~lock/pre-post-proof.html. au][NCS]_The benchmark archives at CBL. http://www.cbl.ncsu.edu/www/benchmarks/

  29. R. De Nicola, A. Fantechi, S. Gnesi, S. Larosa, and G. Ristori. Verifying hardware components with JACK. In Paulo E. Camurati and Hans Eveking, editors, Formal Methods in Computer Aided Design, pages 246–260. Springer, July 1995. LNCS 987

    Google Scholar 

  30. Laurance Pierre. The formal proof of sequential circuits described in CASCADE using the boyer-moore theorem proover. In L. Claesen, editor, Applied Formal Methods for Correct VLSI Design, pages 365–384. Organizing Commitee of the IMEC-IFIP-Workshop, November 1989.

    Google Scholar 

  31. Laurence Pierre. Describing and verifying synchronous circuits with the boyer-moore theorem proover. In Paulo E.Camurati and Hans Eveking, editors, Formal Methods in Computer Aided Design, pages 35–55. Springer, July 1995. LNCS 987.

    Google Scholar 

  32. M. Rahmouni. AMICAL: Interactive behavioral synthesis based on VHDL for control-flow dominated systems. Journal of the Brazilian Computer Society, November 1995.

    Google Scholar 

  33. R. Reetz and T. Kropf. A Flow Graph Semantics of VHDL: A Basis for Hardware Verification with VHDL, pages 205–38. Kluwer Academic Publishers, 1995.

    Google Scholar 

  34. H. Simonis and T. Le Provost. Verification in CHIP: Benchmark results. In L. Claesen, editor, Applied Formal Methods for Correct VLSI Design, pages 570–574. Organizing Commitee of the IMEC-IFIP-Workshop, November 1989.

    Google Scholar 

  35. J. P. Van Tassel. An Operational Semantics for a Subset of VHDL, pages 71–106. Kluwer Academic Publishers, 1995.

    Google Scholar 

  36. S. Tabar and P. Curzon. A comparison of MDG and HOL for hardware-verification. In G. Goos, J. Hartmanis, and J. van Leeuwen, editors, Theorem Proving in Higher Order Logics, pages 415–430. Springer, August 1996. LNCS 1125.

    Google Scholar 

  37. Li-Guo Wang and Michael Mendler. Formal design of a class of computers. In Paulo E. Camurati and Hans Eveking, editors, Formal Methods in Computer Aided Design, pages 84–102. Springer, July 1995. LNCS 987.

    Google Scholar 

  38. L. G. Wang and M. Mendler. Abstraction of hardware construction. In G. Dowek, J. Heering, B. Möller, and K. Meinke, editors, Higher-Order Algebra, Logic, and Term Rewriting, HOA’95, pages 264–287. Springer, 1996. LNCS 1074.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Passau, D-94030, Passau, Germany

    Thomas Lock (Chair for Computer Architectures, Prof. Dr. Ing. W. Grass)

  2. SICAN Braunschweig GmbH, Richard-Wagner-Stra\e 1, D-38106, Braunschweig, Germany

    Michael Mendler (Chair for Computer Architectures, Prof. Dr. Ing. W. Grass) & Matthias Mutz

Authors
  1. Thomas Lock
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Mendler
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Matthias Mutz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Utah, 50 S Central Campus, Salt Lake City, UT, 841112-9205, USA

    Ganesh Gopalakrishnan

  2. Department of Computer Science, Brigham Young University, 3361 TMCB, Provo, UT, 84602-6576, USA

    Phillip Windley

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lock, T., Mendler, M., Mutz, M. (1998). Combined Formal Post- and Presynthesis Verification in High Level Synthesis. In: Gopalakrishnan, G., Windley, P. (eds) Formal Methods in Computer-Aided Design. FMCAD 1998. Lecture Notes in Computer Science, vol 1522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49519-3_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-49519-3_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65191-8

  • Online ISBN: 978-3-540-49519-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation