This section contains a number of examples of Verilog and VHDL FSMs. All are synthesisable, but the precise synthesis results will depend on the coding style, and on any recoding of the FSM which may be carried out by the synthesiser. The source code contains no synthesiser directives to select a specific coding style, since these are vendor-specific.

All the examples implement this simple FSM:

The FSM has three inputs (SRST, LOAD and TC), and two outputs (BUSY and SCK). SRST is a synchronous reset; the FSM resets to state 3.

Testbench

A single testbench is used for all the examples (both VHDL and Verilog). This FSM is so simple that it can be tested simply by cycling through all the states from a reset. In general, however, a test for a more complex FSM would need to preload specific states (using the .P directive), and then test the state space around that state.

A significant issue with FSM verification is that the synthesiser may change the state coding, or the number of bits in the state register. If the testbench explicitly tests the state register, or makes any assumptions about the contents of the state register, then that testbench will only work for the original RTL code. A testbench might, for example, check that an FSM is in state ST0; if the synthesiser has recoded ST0 from 00 to 1000, then the testbench will fail with the post-synthesis netlist.

It is not generally practical to construct different testbenches for the RTL code and the netlist, as the synthesis output will change as different coding algorithms are tried (XST, for example, has 8 different algorithms). If the synthesiser is set to auto-encoding, it might also later change the algorithm if an external factor changes. This testbench avoids the problem by checking only the signals at the module interface, and not the state register itself (it may appear that the testbench does actually test the state register, but S0, S1, S2, and S3 are defined as combinations of the two output signals, rather than as specific values of a state register).

fsm.tv

#define S0 0,0
#define S1 0,1
#define S2 1,1
#define S3 1,0

DUT {
   module FSM(
      input  CLK, SRST, LOAD, TC,
      output SCK, BUSY)
   [CLK, SRST, LOAD, TC] -> [SCK, BUSY]
   create_clock CLK       // ';' termination optional in DUT section
}

[.C, 1, .X, .X] -> [S3]
[.C, 0,   ,   ] -> [S1]   // leave blank inputs unchanged at .X
[.C, 0,   ,   ] -> [S2]
[.C, 0,   ,  0] -> [S1]
[.C, 0,   , .X] -> [S2]
[.C, 0,   ,  1] -> [S0]
[.C, 0,  0, .X] -> [S0]
[.C, 0,  1, .X] -> [S1]
[.C, 1, .X, .X] -> [S3]   // reset

The expected testbench output is:

# (Log)        (90 ns) 9 vectors executed (18 passes, 0 fails)