Correct hardware compilation with Verilog HDL
Gordon J. Pace · OAR@UM (University of Malta) · 1999
. Hardware description languages usually include features which do not have a direct hardware interpretation. Recently, synthesis algorithms allowing some of these features to be compiled into circuits have been developed and implemented. Using a formal semantics of Verilog based on Relational Duration Calculus, we give a number of algebraic laws which Verilog programs obey, using which, we then prove the correctness of a hardware compilation procedure. 1