In this paper, experiments with a useable C frontend for the CCC behavioural synthesis tools are presented and analysed. This tool combination is able to rapidly deliver provably-correct hardware implementations at the RTL ...