Abstract
This paper presents a framework for verifying compilation tools based on parametrised hardware libraries expressed in Pebble, a simple declarative language. An approach based on pass separation techniques is described for specifying and verifying Pebble abstraction mechanisms, such as the loop statement. We show how this approach can be used to verify the correctness of the flattening procedure in the Pebble compiler, which also results in a more efficient implementation than a non-verified version. The approach is useful for guiding compiler implementations for Pebble and related languages such as VHDL; it may also form the basis for automating the generation of provably-correct tools for hardware development.
Chapter PDF
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
I. Attali, J. Chazarain and S. Gilette, “Incremental evaluation of natural semantics specifications”, Proc. 4th Int. Symp. on Programming Language Implementation and Logic Programming, LNCS 631, Springer, 1992.
L.A. Dennis et. al., “The PROSPER toolkit”, Proc. 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1785, Springer, 2000.
T. Despeyroux, “Executable specification of static semantics”, Semantics of Data Types, LNCS 173, Springer, 1984.
D. Eisenbiegler, C. Blumenroehr and R. Kumar, “Implementation issues about the embedding of existing high level synthesis algorithms in HOL”, Theorem Proving in Higher Order Logics, LNCS 1125, Springer, 1996.
C. Hankin, Lambda Calculus, A guide for Computer Scientists, Oxford University Press, 1994.
J. He, G. Brown, W. Luk and J.W. O’Leary, “Deriving two-phase modules for a multi-target hardware compiler”, Designing Correct Circuits, Springer Electronic Workshop in Computing, 1996.
J. He, I. Page and J.P. Bowen, “Towards a provably correct hardware implementation of occam”, Correct Hardware Design and Verification Methods, LNCS 683, Springer, 1993.
C.A.R. Hoare, J. He and A. Sampaio, “Normal form approach to compiler design”, Acta Informatica, Vol. 30, pp. 701–739, 1993.
G. Jones and M. Sheeran, “Timeless truths about sequential circuits”, Concurrent Computations: Algorithms, Architectures and Technology, S.K. Tewksbury et. al. (eds.), Plenum Press, 1988.
G. Jones and M. Sheeran, “ircuit design in Ruby”, Formal Methods for VLSI Design, J. Staunstrup (ed.), North-Holland, 1990.
U. Jørring and W. Scherlis, “Compilers and staging transformations”, Proc. ACM Symp. on Principles of Programming Languages, ACM Press, 1986.
W. Luk and S.W. McKeever, “Pebble: a language for parametrised and reconfigurable hardware design”, Field-Programmable Logic and Applications, LNCS 1482, Springer, 1998.
W. Luk et. al., “A framework for developing parametrised FPGA libraries”, Field-Programmable Logic and Applications, LNCS 1142, Springer, 1996.
W. Luk et. al., “econfigurable computing for augmented reality”, Proc. IEEE Symp. on Field-Programmable Custom Computing Machines, IEEE Computer Society Press, 1999.
N. Mansouri and R. Vemuri, “Amethodology for completely automated verification of synthesized RTL designs and its integration with a high-level synthesis tool”, Formal Methods in Computer-Aided Design, LNCS 1522, Springer, 1998.
H.R. Nielson and F. Nielson, Semantics with Applications, John Wiley and Sons, 1992.
F. Pfenning and C. Schrmann, “System description: Twelf-a meta-logical framework for deductive systems”, Proc. Int. Conf. on Automated Deduction, LNAI1632, Springer, 1999.
M. Sheeran, S. Singh and G. Stalmarck, “Checking safety properties using induction and a SAT-solver”, Proc. Int. Conf. on Formal Methods in CAD, LNCS 1954, Springer, 2000.
M. Weinhardt and W Luk, “Pipeline vectorization”, IEEE Trans. CAD, Vol. 20, No. 2, 2001, pp. 234–248.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McKeever, S., Luk, W. (2001). Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques. In: Margaria, T., Melham, T. (eds) Correct Hardware Design and Verification Methods. CHARME 2001. Lecture Notes in Computer Science, vol 2144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44798-9_19
Download citation
DOI: https://doi.org/10.1007/3-540-44798-9_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42541-0
Online ISBN: 978-3-540-44798-6
eBook Packages: Springer Book Archive