This talk gives a set of primitive recursive functions or rules that act on the parse tree for a section of Verilog and return a finite state machine or circuit netlist representation of the section. The rules embody the notions of hardware equivalence normally used by compilers such as Synopsys and CV2. The motivation for providing primitive recursive functions is that they may be easy to reason with and thus help our Verilog Formal Equivalence project.