Reasoning about hardware designs written in Verilog is problematic, in large part because of the lack of a formal semantics for the language. The behavioral aspects of many constructs within the language are unclear, even with the existence now of an official language standard. As a result, a program may contain many subtleties which can be overlooked without careful analysis, and which may not even appear, depending on the implementation of the simulator that is used. In this thesis, we present a formal description of a large subset of behavioral Verilog, based on axiomatic semantics. Our primary contribution is an explicit formalization of the Verilog simulation cycle. In addition, we discuss some of the constructs that pose particular challenges to formal description, and offer axiomatic descriptions of these constructs that appear to match the behavior of the leading simulation packages.