next up previous contents
Next: Basic concepts Up: Getting started with SMV Previous: The bakery algorithm   Contents

Synchronous Verilog

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.