Introduction

Finite State Machines are used in verification everyday and can serve following purposes: 

1. As the system grows, it becomes increasingly complex and you might end up into the state from which transitions to other state is not possible, or you are in a loop and can never exit a system. If you don't understand it yet, no worries. Try understanding how FSM works and it would be easier to understand the benefits. 

​

Design of the FSM:

States: 

Ideally with 3 inputs there can be 6 possible outputs as below: (Remember to exclude repeatations if you are using premutations/combinations)

[red]

[green]

[yellow]

[red,green]

[red,yellow]

['red', 'green', 'yellow']
['red', 'yellow', 'green']
['green', 'red', 'yellow']
['green', 'yellow', 'red']
['yellow', 'red', 'green']
['yellow', 'green', 'red']
Now, most of this scenarios are invalid because, red and green cannot be ON at the same time. 

Also yellow, and green cannot be on at same time. 
Hence, the only valid ones are: 
1. Red
2. RedYellow
3. Green
4. Yellow

This reduces our problem and code complexity. 

Inputs:
- start (to initiate the traffic light system)
- timer (to simulate the passage of time)

Outputs:
- redLight
- yellowLight
- greenLight

Transitions and State Actions:

State: Red
- On start: Transition to state RedYellow
- On timer: No action (stays in Red state)

State: RedYellow
- On start: No action (stays in RedYellow state)
- On timer: Transition to state Green

State: Green
- On start: No action (stays in Green state)
- On timer: Transition to state Yellow

State: Yellow
- On start: No action (stays in Yellow state)
- On timer: Transition to state Red

​

Following are some rules for our FSM: 

1. Completeness: FSMs should be designed to handle all possible inputs and state combinations. There should be a defined transition for every possible input condition to avoid unintended behavior or undefined states. Every state should have atleast one transaction going out.  Reason: if you are in a RED and you can never turn to yellow or green then you are in a locked state. 

2. Determinism: FSMs are deterministic, meaning that given the current state and input, the next state and output are uniquely defined. There should be no ambiguity in the behavior of the FSM. 

   1. Reason: System can not be confused whether after RED, it needs to turn a GREEN or YELLOW. ​

3. Initial State: System should know what to do as it starts. 

4. Default or Else Transitions: FSMs may include default or "else" transitions to handle unexpected or unhandled conditions. These transitions define what happens if none of the defined conditions are met.

5. Mealy and Moore Machines: FSMs can be categorized as Mealy machines or Moore machines. In a Mealy machine, the outputs depend on both the current state and inputs, while in a Moore machine, the outputs depend only on the current state.

6. Timing and Clocking: FSMs can be synchronous or asynchronous. Synchronous FSMs are clock-driven, where state transitions occur on specific clock edges. Asynchronous FSMs, on the other hand, do not rely on a clock and can transition based on combinational logic or event-driven triggers.

7. Completeness: FSMs should be designed to handle all possible inputs and state combinations. There should be a defined transition for every possible input condition to avoid unintended behavior or undefined states.

​

Now that we understand the rules let's go ahead and code: