Synchronous Verilog does not contain the event based constructs of Verilog, such as @(..). However, SMV does support inference of combinational logic and edge-sensitive storage devices in a way that is compatible with logic synthesis tools (see the draft standard IEEE P1364.1/D1.6).
For example here is a simple positive edge-triggered register, with input y and output x:
always @(posedge clk) x <= y;
Here is a positive edge-triggered register with active-low asynchronous reset:
always @(posedge clk or negedge rst)
if(!rst)
x <= 0;
else
x <= y;
Note that even if x is declared as a wire in the above examples, it will be treated as a register.
Here is an example of inferred combinational logic:
always @(x or y or z) a = (x | y) & z;
SMV does not recognize inferred latches. These are treated as combinational logic.
By default, SMV assumes that all inferred registers are triggered on the same edge of the same clock signal. It then "extracts" the clock, meaning that each step of the resulting SMV model corresponds to one full cycle of the clock. For single-clocked designs this generally results in improved verification efficiency, and has the advantage that the "next time" operator X has the interpration "at the next clock edge". A side-effect of clock extraction is that asynchronous resets become synchronous, since all state transitions correspond to clock edges.
For multple clock designs, you must set the environment variable VL2SMV_MULTI_CLOCK. In this case, clock extraction will not occur, and both phases of the clock signal will be apparent in the SMV model. Care should be taken in writing temporal properties in this mode, since the X operator does not mean "at the next clock edge". Also, note that if the clock signals are not explicitly driven, they will be allow to rise and fall nondeterministically (and thus are not guaranteed to toggle).