Verification of streaming hardware and software codesigns

We present an approach to verifying the codesign of software and hardware. Our approach verifies that a reference design, perhaps a straightforward software implementation, is equivalent to a design combining software and reconfigurable hardware, possibly using runtime reconfiguration. Our approach combines symbolic simulation with equivalence checking to compare symbolic output expressions. Whilst our implementation uses C-style software and streaming hardware based on Maxeler designs, our approach is modular and could generalize to other software or hardware inputs. We evaluate our approach by applying it to several kernels, including one used for geoengineering.