Field-Programmable Gate Arrays (Fig’s) have been around since the early 1980s and have now achieved relatively wide-spread use. For example, FPGAs are routinely used for high-performance computing, financial applications, seismic modelling, DNA sequence alignment, software defined networking and, occasionally, are even found in smartphones. And yet, despite their success, there still remains something of a gap between programming languages and circuit designs for an FPGA. We consider the compilation of an imperative programming language, Whiley, to VHDL for use on an FPGA. Whiley supports compile-time verification of function pre- and post-conditions. Hence, our motivation is to adapt this technology for verifying properties of hardware designs.