Synchrony

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.