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)
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
H. Achatz. SUSAN: System for universal scheduling and allocation. In SASIMI Synthesis and Simulation Meeting and International Interchange, pages 138–44, 1993.
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.
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.
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.
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.
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.
R. J. Boulton. CLaReT user’s manual. Technical report, University of Cambridge, Computer Laboratory, 1995.
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.
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.
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.
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
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
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.
L. Claesen, F. Proesmans, E. Verlind, and H. DeMan. SFG-tracing: A formal verification methodology. In ACM-SIGDA Workshop, February 1990. Miami.
C. Delgado Kloos and P. T. Breuer, editors. Formal Semantics for VHDL. Kluwer Academic Publishers, 1995.
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.
D. Gajski, N. Dutt, A Wu, S. Lin, et al. High Level Synthesis: Introduction to Chip and System Design. Kluwer Academic Publishers, 1992.
M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
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).
A. A. Jerraya, H. Ding, P. Kission, and M. Rahmouni. Behavioral Synthesis and Component Reuse with VHDL. Kluwer Academic Publishers, 1992.
G. G. de Jong. Generalized Data Flow Graphs — Theory and Applications. PhD thesis, Eindhoven, 1993. Cip-Gegevens Koninklijke Bibliotheek, Den Haag.
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
M. Larsson. An engineering approach to formal digital system design. The Computer Journal, 38(2):101–10, 1995.
Th. Lock and M. Mutz. FORVERTIS: Projektbericht. Technical report, UniversitÄt Passau, Lehrstuhl für Rechnerstrukturen, Oktober 1997.
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.
S. S. Leung and M. A. Shanblatt. ASIC System Design with VHDL: A Paradigm. Kluwer Academic Publishers, 1989.
P. Michel, U. Lauther, and P. Duzy. The Synthesis Approach to Digital System Design. Kluwer Academic Publishers, 1992.
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/
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
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.
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.
M. Rahmouni. AMICAL: Interactive behavioral synthesis based on VHDL for control-flow dominated systems. Journal of the Brazilian Computer Society, November 1995.
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.
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.
J. P. Van Tassel. An Operational Semantics for a Subset of VHDL, pages 71–106. Kluwer Academic Publishers, 1995.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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