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.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com