Formal reasoning with Verilog HDL
Gordon J. Pace, Jifeng He · OAR@UM (University of Malta) · 1998
Abstract. Most hardware verification techniques tend to fall under one of two broad, yet separate caps: simulation or formal verification. This paper briefly presents a framework in which formal verification plays a crucial role within the standard approach currently used by the hardware industry. As a basis for this, the formal semantics of Verilog HDL are defined, and properties about synchronization and mutual exclusion algorithms are proved. 1