6

State machines are a pattern that is used very often in writing synchronous designs. They serve as the controllers in the design. So, is there a standard way to verify them if they are written using VHDL or Verilog/SystemVerilog? Or is it better to use some GUI to draw them and then generate code from the GUI instead?

By standard way I mean a pattern of code used to verify them. There are always different ways to "skin the cat" but perhaps there is a method that is very popular.

The thing is that state machines can be quite big and one would have to write code to verify each branch in the state machine which leads to a lot of code in the testbench.

Edit: I am only taking about verification of the fsm itself on its own, to verify that it matches the fsm state diagram and no errors in rtl coding exist.

Shashank V M
  • 2,279
  • 13
  • 47
quantum231
  • 11,218
  • 24
  • 99
  • 192
  • 5
    I'm curious to see what others say about this. I've written a lot of state machines, but no, I don't have a standard verification process. For me, writing HDL to *implement* a given state machine design is not really the hard part -- the hard part is making sure that the *design* of the state machine itself has the *behavior* that the application requires under all possible input combinations. – Dave Tweed Dec 09 '16 at 00:26
  • 2
    I have thought that if a specific GUI tool exists for this and we use it, we can take it for granted that the code is correct as long as the state machine diagram is correct. Like you pointed out, writing all that testbench code to verify all possible routes that the state machine must take, this is annoying even for simple state machines. The main problem is if I realize that the state machine needs to be changed and then the code has to be rewritten or changed. It is tedious. – quantum231 Dec 09 '16 at 00:53
  • 2
    Now basically, some time ago I did a course in Comprehensive VHDL from Doulos in UK. It was a fantastic course. In it they also taught how to write state machine in VHDL, the idea was to seperate the synchronous processes that assigns next state to current state from the asynchronous (not clock) process that generates value for the next state from the current state and current inputs. That was a very interesting as it gets rid of many pitfalls in state machine design. However, while they covered state machine design exclusively, this is not so for state machine verification. – quantum231 Dec 09 '16 at 08:44
  • 2
    Stateflow by MathWorks is a GUI tool to code FSMs. – Shashank V M Sep 22 '20 at 06:09
  • 1
    @quantum231 Mentor Graphics' ModelSim also defines Finite State Machine coverage which is used for State and state transition coverage. See my answer for more details. – Shashank V M Oct 27 '20 at 06:08
  • 2
    Yes, a unified approach to verify FSM's can be found in this link :https://verificationacademy.com/verification-horizons/november-2020-volume-16-issue-3/unified-approach-to-verify-fsm – Shashank V M Nov 12 '20 at 08:44
  • 2
    The better way is to do formal verification! I updated my answer after trying it out myself. No more worrying about that corner case anymore! – Shashank V M Dec 29 '22 at 07:59
  • 2
    Alright Shashank bhai. I tried to read about how to actually do formal verification. I came across the concept of using property and assertion (SVA or PSL). I found mention of Logic Equivalence Check. I found mention of model checking as well. I came across name of program called Jasper. However, in all of this, I could not find anything that tells me how I me myself, can do formal verification on my design. I wish formal was taught at university level too. – quantum231 Dec 31 '22 at 00:26

2 Answers2

6

Verification is a huge part of the design process; in a complex design, it would not be unusual to spend as much time, or even more time on verification than you do on the actual design. That being the case, a question which is essentially 'how do you verify complex designs' is quite broad.

In overview, if the design copes with a large number of scenarios, as indicated by there being very many states in your state machine, a good starting point for the test suite would be to have separate tests that stimulate the design so as to replicate all theses scenarios. You can then use code coverage tools to see which state transitions have been covered, and add new tests until everything is being covered. You can manage different test cases using the configuration construct in VHDL

It might commonly be the case that there are scenarios that are variations on a theme, for example receiving a packet of some kind, but with different packet lengths, lengths that are out of bounds, etc. In these cases you can write tests that generate a number of random length packets; you would then need to make sure that all your edge cases are met, for example the minimum and maximum lengths, the minimum plus one, the maximum minus one, etc, and that your design does the correct thing in every case. You might also need to test combinations of inputs to the design, and again these combinations could be generated by a test case, as opposed to writing them out manually one by one.

There are a number of methodologies that attempt to help manage the process of generating stimulus and recording the results. I use OSVVM, which I learned about through a course a couple of years ago. I like it because it uses the same VHDL language that I am used to, along with a bit of TCL scripting, and does not require any 'extras' in order to work with my simulator. There are many alternatives, which I won't try to list here, but a quick Google search for 'fpga verification' brings up a lot of resources.

scary_jeff
  • 1,977
  • 8
  • 11
  • 1
    I only meant testing the state machine on its own, that its behaviour matches the state fsm diagram – quantum231 Dec 12 '16 at 12:58
  • 1
    The best way to test it is as part of the system that it controls. If you test it in isolation, you risk not providing it with the same stimulus it gets in the real system. You need to create a test bench for the system as a whole *anyway*, so you may as well make one test bench that does it all. – scary_jeff Dec 12 '16 at 13:15
3

I recommend using formal verification techniques to prove the complete behaviour of the state machine is as intended.

Write 2 sets of assertions:

  1. Assertions to verify each state transition occurs on the right condition.
  2. Assertions to verify each output transitions only in the state intended.

Then run the formal tool to prove these assertions.

Sometimes, you can write a single assertion to verify the entire FSM functionality, like I did here: https://electronics.stackexchange.com/a/505842/238188

Formal tools are capable of proving infinite length properties, something that is not possible in simulation.

Shashank V M
  • 2,279
  • 13
  • 47