The high security requirements of cyber-physical systems and the critical tasks they carry out make it necessary to guarantee the absence of any vulnerability to security attacks and that they have no unexpected behaviour. The size and complexity of the underlying hardware in cyber-physical systems are increasing and so is the risk of failures and vulnerability to security threats. Checking for errors and security holes in the early phases of hardware production is generally considered an effective approach. To ease the process of designing and testing in the early stage, hardware description languages such as Verilog are used to design hardware. Hardware designs in such description languages, however, do not correspond to mathematical models. Hence we cannot reason about hardware designs and formally verify their correctness and security related properties. In this paper, we develop a formal model of Verilog in the theorem prover Isabelle/HOL. Our model covers most constructs used in hardware designs. With our model, one can analyse Verilog designs and execute them for simulation. More importantly, our model enables formal reasoning about interesting properties for Verilog designs. To complete our tool chain, we build a translator which automatically translates an existing Verilog design to equivalent design in our formal model.