Example - traffic light controller

This example is a controller that operates the traffic lights at an intersection where two-way street running north and south intersects a one-way street running east. The goal is to design the controller so that collisions are avoided, and no traffic waits at a red light forever.

The controller has three traffic sensor inputs, N_Sense, S_Sense and E_Sense, indicating when a car is present at the intersection traveling in the north, south and east directions respectively. There are three outputs, N_Go, S_Go and E_Go, indicating that a green light should be given to traffic in each of the three directions.

module main(N_SENSE,S_SENSE,E_SENSE,N_GO,S_GO,E_GO);

  input  N_SENSE, S_SENSE, E_SENSE;
  output N_GO, S_GO, E_GO;

  wire   N_SENSE, S_SENSE, E_SENSE;
  reg    N_GO, S_GO, E_GO;

In addition, there are five internal registers. The register NS_Lock is set when traffic is enabled in the north or south directions, and prevents east-going traffic from being enabled. Similarly EW_LOCK is set when traffic is enabled in the east direction, and prevents north or south-going traffic from being enabled. The three bits N_Req, S_Req, E_Req are used to latch the traffic sensor inputs.

  reg    NS_LOCK, EW_LOCK, N_REQ, S_REQ, E_REQ;

The registers are initialized as follows:

  initial begin
    N_REQ = 0; S_REQ = 0; E_REQ = 0;
    N_GO = 0; S_GO = 0; E_GO = 0;
    NS_LOCK = 0; EW_LOCK = 0;
  end

Always, if any of the sense bits are true, we set the corresponding request bit:

  always begin if (!N_REQ & N_SENSE) N_REQ = 1; end
  always begin if (!S_REQ & S_SENSE) S_REQ = 1; end
  always begin if (!E_REQ & E_SENSE) E_REQ = 1; end

The code to operate the north-going light is then as follows:

  always begin
    if (N_REQ)
      begin
        wait (!EW_LOCK);
        NS_LOCK = 1;
        N_GO = 1;
        wait (!N_SENSE);
        if (!S_GO) NS_LOCK = 0;
        N_GO = 0;
        N_REQ = 0;
      end
  end

That is, when a north request is detected, we wait for the EW lock to be cleared, then set the NS lock, and switch on the north light. Note, these last two assignments occur simultaneously, since they execute in zero time. Then we wait for the north sensor to be off, indicating there is no more traffic in the north direction. We then clear the NS lock, but only if the south light is currently off. Otherwise, we might cause a collision of south and east traffic. Finally, we switch off the north light and clear the north request flag. Note, the last two actions occur simultaneously with switching off the lock, so there is no danger of having the lock off but the light on.

The code for the south light is similar.

  always begin
    if (S_REQ)
      begin
        wait (!EW_LOCK);
        NS_LOCK = 1; S_GO = 1;
        wait (!S_SENSE);
        if (!N_GO) NS_LOCK = 0;
        S_GO = 0; S_REQ = 0;
      end
  end

Finally, here is the code for the east light:

  always begin
    if (E_REQ) 
      begin
        EW_LOCK = 1;
        wait (!NS_LOCK);
        E_GO = 1;
        wait (!E_SENSE);
        EW_LOCK = 0; E_GO = 0; E_REQ = 0;
      end
  end

This differs slightly from the north and south cases. When an east request is detected, we set the EW lock, and then wait for the NS lock to be cleared, turn on the light, wait for the traffic sensor to clear, and finally, clear lock, light and request.

There are two kinds of specification we would like to make about the traffic light controller. The first is called ``mutex'', and states that lights in cross directions are never on at the same time:

always begin
  assert mutex: !(E_GO & (S_GO | N_GO));
end

This assert statement executes at every time unit, and fails if the east light is on at the same time as either the north or the south lights.

Second, we have ``liveness'' specifications. For each direction, we specify that if the traffic sensor is on for a given direction, then the corresponding light is eventually on, thus no traffic waits forever at a red light:

always begin
  if (E_SENSE) assert E_live: eventually E_GO;
  if (S_SENSE) assert S_live: eventually S_GO;
  if (N_SENSE) assert N_live: eventually N_GO;
end

Notice that since assert statements execute in zero time, each of these statements executes once every time unit. Further, this shows the use if the ``eventually'' operator in an assertion. This is equivalent to the temporal logic operator F. For example, if at any time the assertion E_live executes, then E_GO must eventually be true.

Our traffic light controller is designed so that it depends on drivers not waiting forever at a green light. We want to verify the above properties given that this assumption holds. To do this, we write some ``fairness constraints'', as follows:

always begin
  assert E_fair: eventually !(E_GO & E_SENSE);
  assert S_fair: eventually !(S_GO & S_SENSE);
  assert N_fair: eventually !(N_GO & N_SENSE);
end

Each of these assertions states that, always eventually, it is not the case that a car is at a green light. To tell SMV to assume these ``fairness'' properties when proving the ``liveness'' properties, we say:

  using N_fair, S_fair, E_fair prove N_live, S_live, E_live;
  assume E_fair, S_fair, N_fair;

endmodule

In effect, we are telling SMV to ignore any execution traces where one of these assumptions is false. The fairness constraints themselves will simply be left unproved. Now, open this file and try to verify the property mutex. The result should be ``false'', and in the ``Trace'' panel, you should see a counterexample trace in which the north light goes off exactly at the time when the south light goes on. In this case, the north light controller is trying to set the NS lock bit at exactly the same time that the south light is trying to clear it. The result of this is undefined, hence SMV attempts to verify both cases. It reports the case where the NS lock bit is cleared, which allows the east light to go on, violating the mutex property.

To fix this problem, let's insure that this situation doesn't arise by making the south light wait to go on if the north light is currently going off. Change the code for the north light controller to the following (and make the corresponding change in the south light controller):

  always begin
    if (N_REQ)
      begin
        wait (!EW_LOCK & !(S_GO & !S_SENSE));
        NS_LOCK = 1;
        N_GO = 1;
        wait (!N_SENSE);
        if (!S_GO) NS_LOCK = 0;
        N_GO = 0;
        N_REQ = 0;
      end
  end

Open this new version and verify the property mutex. It should be true. Now try to verify N_live. It should come up false, with a counterexample showing a case where both the north and south lights are going off at exactly the same time. In this case neither the north code nor the south code clears the lock, because each thinks that the other light is still on. As a result, the lock remains on, which prevents an east request from being served. This leaves the EW lock set forever, hence the controller is deadlocked, and remains in the same state indefinitely (note the ``repeat signs'' on the last state).

To fix this problem, we'll have the north controller switch off the lock when the south light is either off, or going off (and make the corresponding change to the south light controller). Here is the new code for the north controller:

  always begin
    if (N_REQ)
      begin
        wait (!EW_LOCK & !(S_GO & !S_SENSE));
        NS_LOCK = 1; N_GO = 1;
        wait (!N_SENSE);
        if (!S_GO | !S_SENSE) NS_LOCK = 0;
        N_GO = 0; N_REQ = 0;
      end
  end

Open this new version and verify the properties mutex, N_live, S_live and E_live. They should all be true. Note that if you try to verify the fairness constraints N_fair, S_fair and E_fair, they will come up false. These are unprovable assumptions that we made in designing the controller. However, if we used the controller module in a larger circuit, we could (and should) verify that the environment we put the controller into actually satisfies these properties. In general, it's best to avoid unproved assumptions if possible, since if any of these assumptions is actually false, all the properties we ``proved'' are invalid.