Towards provably-correct hardware compilation tools based on pass separation techniques

Abstract

This paper presents a framework for verifying compilation tools based on parametrised hardware libraries expressed in Pebble, a simple declarative language. Anapproach 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. © 2001 Springer-Verlag Berlin Heidelberg.