Formal Behavioural Synthesis of Handel-C Parallel Hardware Implementations from Functional Specifications