It is difficult to verify that the components of programmable systems will behave correctly with respect to either high level specifications or the intent of the designers that have implemented them. To focus on a concrete example, microprocessors traditionally use the notion of an instruction set (IS), specified at a high level, to form a boundary between the hardware designers and the compiler authors. While there are many variations on this theme, it has proved a long-lived approach to the complexities of programming and designing microprocessors. However, it is still difficult to verify that a particular implementation of a microprocessor implements a given IS, and the more hardware details the IS hides, the more difficult is it to use the IS as the sole input for an optimizing compiler. Thus, compiler authors must often be familiar with all of the low-level hardware details of a processor, and then carefully construct code using the hidden semantics of the IS with respect to a given processor or processor class to give good performance.
VLIW style instruction sets are an attempt to reduce this semantic gap by exposing more of the behavior of the processor to the compiler. The research question posed here is: "What is required to completely close the semantic gap between the hardware level description of a programmable component and the exported semantics of the same component?" The tentative answer is that as a first step it requires a more formal description of the device, its programability, and its concurrency than is offered by traditional HDLs. Furthermore, given this new description, it is necessary to reformulate much of the abstraction/mapping tool chain from the hardware description to the high-level programmer's model of the device. One way to explore this issue is to attempt to build such a system. The current approach combines a function hardware description language (sharing properties with other concurrent constraint languages such as Oz and Mercury) with the power of complex propositional reasoning (using high performance SAT solvers), and additional theories (a la CVC) including Presburger arithmetic, and any other ones that look cool or necessary. Currently, work is underway to develop a high performance SAT+Presburger solver while pushing the design of simply controlled (similar to a horizontal VLIW) heterogeneous processors to the level of automatic compiler generation. It is expected that the solver will be useful for the implementation of an efficient retargetable compiler, due to the fact that Presburger arithmetic can encode the semantics of the current constraint language that is used to model both the hardware and intermediate forms (at the compiler IR level) of the software.