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
endmodule
In 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;
end
In 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;
end
then 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;
end
we 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.