SV is a synchronous language. This means that all statements in SV (except the wait statement) execute in exactly zero time. For example, consider the following simple program:
module main(); wire x,y,z; always begin x = y; end always begin y = z; end endmoduleIn SV, the two always blocks execute exactly simultaneously, in zero time. As a result, the assignments x = y and y = z can be viewed as simultaneous equations. Therefore, it is true at all times that x = z. Because values on wires propagate in exactly zero time, there is no need for a notion of a triggering ``event''. That is, we need not (and may not) write
always @(y) begin x = y; endIn SV, any change in y is always reflected instantaneously in x.
As in other synchronous languages, the instantaneous propagation of signals can lead to ``paradoxes''. For example, if we write
wire x,y; always begin x = y; end always begin y = !x; endthen we have two simultaneous equations with no solution. On the other hand, in this case:
wire x,y; always begin x = y; end always begin y = x; endwe have simultaneous equations with two solutions: x = 0, y = 0 and x = 1, y = 1. In a hardware implementation, these cases would correspond to combinational cycles in the logic. There are a number of ways of dealing with such cycles. However, we will leave the behavior in such cases undefined. The SMV system simply disallows combinational cycles.