Hi Chao
I don't know what books you have on assertions, but some good ones to start with are:
- Assertion-Based Design by Foster, Krolnik, Lacey
- SystemVerilog Assertions Handbook by Cohen, Venkataramanan, Kumari
- A Practical Guide for Systemverilog Assertions by Vijayaraghavan, Ramanathan
There's some useful papers kicking around, such as Stuart Sutherland's Introduction to Assertions from DesignCon 2006:
http://www.sutherland-hdl.com/papers/2006-DesignCon_Getting_Started_with_SVA_presentation.pdf
Anyway, back to the question.
You are correct to notice that it is not desirable to duplicate the RTL code. There's not much point in that. We need to think about *what* we're trying to verify in the FSM. We might like to verify some or all of the following:
- reset behaviour
- state encoding, e.g. one hot, grey code
- only legal states occur
- only legal transitions occur
- assumptions on inputs are correct
- etc.
In your small example the next state logic is simple, so it didn't show there was much value to the assertion; however that's not always the case. If the next state logic is complicated, there can be lots of ways a transition can go wrong, or an illegal state can be entered. Looking only at the state transitions, values, and encoding, we can pick up lots of potential errors. We don't need to specify the details of the next state logic in the assertion.
A lot of FSM errors are to do with communication with other FSMs, or the rest of the environment. Sometimes this can be crossing clock domains, other times it's simply that a different protocol was expected. These are good places for assertions, as they protect the FSM against unexpected behaviour, misinterpretations, or changes.
Also remember that we like to apply functional coverage to state machines. This can be done using SVA pretty effectively. Functional coverage lets us see the areas of design functionality that have been reached during simulation. It doesn't check correctness (although you can highlight illegal transitions and states), but it does let you know how comprehensive your stimulus is.
You might like to check out these presentations for an idea of what I'm talking about:
- http://www.verilab.com/downloads/dac2005_mal_sva_cov_presentation_a4.pdf
- http://www.verilab.com/downloads/snug2005-europe-litterick-slides.pdf
Hope this helps
Jason
--
Verilab Ltd (www.verilab.com)
jason.sprott@verilab.com |