Trustworthy Codesign by Verifiable Transformations

This paper proposes a novel approach to trustworthy algorithm-hardware codesign based on the Ruby language and the Coq theorem prover. An algorithm is captured as a functional description in Ruby, which can then be optimised by transformations to become relational descriptions that support efficient hardware design involving multi-directional dataflow and systolic implementations. This approach enables rapid verification of instance-specific designs by numerical and symbolic simulations, while parametric transformations can be verified using Coq based on Ruby’s relational algebra. Case studies based on the 1D convolver designs are used to illustrate the proposed approach.