Those familiar with the Verilog modeling language may find it easier to write models for SMV in Synchronous Verilog (SV). This language is syntactically only a slight variation of the Verilog language. However its semantics is not based on an event queue model, as in Verilog. Rather, SV is a synchronous language, in the same family as Esterel, Lustre, and SMV. Because SV provides a functional description of a design rather than an operational description of how to simulate it, SV is better suited than Verilog to such applications as hardware synthesis, cycle-based (functional) simulation and model checking. Nonetheless, the meaning of most SV programs should be readily apparent to one familiar with modeling in Verilog.