Towards verifying parametrised hardware libraries with relative placement information [parametrised read parameterised]

This paper presents a framework for verifying compilation tools for parameterised hardware libraries with placement information. Such libraries are captured in Pebble, a simple declarative language based on structural VHDL, and can contain placement information to guide circuit layout. Relative placement information enables control of circuit layout at a higher level of abstraction than placement information in the form of explicit coordinates. We provide a functional specification of a procedure for compiling Pebble programs with relative placement information into Pebble programs with explicit placement coordinate information. We present an overview of the steps for verifying this procedure based on pass separation techniques. The compilation procedure can be used in conjunction with partial evaluation to optimise the size and speed of circuits described using relative placement. Our approach has been used for optimising a pattern matcher design, which results in a 33% reduction in resource usage.