Practical FSM analysis for Verilog

The ability to analyze a finite state machine (fsm) has always been desired by hardware designers, since an un-analyzed fsm is clearly prone to design bugs. Unfortunately there are too many ways to represent (code) an fsm. It is almost impossible for a tool to identify all possible fsm coding styles. In our department, at Cisco, we have a standardized fsm coding style. The standard fsm coding style allows us to easily extract an fsm. The extracted fsm is then fed to various tools for analysis: fsm reachability property, fsm coverage, and automatic fsm bubble diagram drawing. We show our standard fsm coding style, how fsms are extracted, and a well known algorithm that is used to study the reachability property. Then we show how to monitor the fsm transition coverage and also introduce a tool to automatically draw an fsm bubble diagram from the extracted fsm