Verifying Hardware Optimizations for Efficient Acceleration

Verifying the correctness of optimizations is a key challenge in hardware acceleration. Incorrect optimizations can produce designs unfit for purpose. This paper presents a novel approach, Covoh, which captures families of hardware designs as parametric block descriptions, such that the behaviour of design instances can be verified by numerical and symbolic simulation. In this work, hardware optimizations are expressed as transformations of parametric descriptions, and their parametric verification based on the Coq proof assistant is guided by verification strategies. Repositories of design descriptions and verification strategies have been developed to facilitate design development in Covoh. Its use in verifying two optimizations illustrates the capability of Covoh. The first, a variation of Horner's Rule, maps an O(n2) design to an O(n) design. The second, used in optimizing avionics monitoring, maps an O(2n) design to an O(n) design. The effectiveness of such optimizations is demonstrated with FPGA implementations: varying the value of a single parameter that controls pipelining would, for example, lead to a family of functionally-verified designs with different trade-offs, from ones with low throughput, low resource usage and low power consumption to ones with high throughput, high resource usage and high power consumption.