It's an increasingly complex world in which we live and that seems to be doubly true of state-machine design.
With protocols such as USB3, PCI Express and a growing number of cache coherent multiprocessor on-chip buses and networks, the designer has been greeted with a state-space explosion. USB3 has, for example, added an entire link layer and, with it, the Link Training and Status State Machine. This is, in itself, a complex entity, which although it has only 12 states in total can move between them using a variety of different arcs.
Within the SoC itself, to maximize bandwidth, we are seeing highly complex processor-to-memory interconnect schemes that allow transactions to be split into smaller entities, with the ability for each master or slave on the interconnect to respond out of order. Not only that, to maintain cache coherency, data may need to be reflected to other nodes as it is returned. State machines that can control this level of activity are, by nature, highly complex. Because of the way that transactions can be split, prioritized and reordered, FSMs are potentially prone to design-killing problems such as deadlock and livelock.
Although it is technically possible to write assertions that can hunt for deadlock conditions or unreachable states, it is generally clear that avoiding these situations are the intent of every designer. Furthermore, writing detailed, comprehensive assertions is not something that a domain expert in cache coherency or bus interface design has a lot of time to perform. It makes far more sense to use a tool that can parse and understand state machines to infer these common intents from the RTL source code, leaving the designer and verification teams to concentrate on writing test code to ensure that states are connected by the right transition arcs.
Automated checking makes it possible to deploy verification tools across a wider group of engineers, in both design and verification, so that they can erase bugs in their designs faster and earlier. The technology also improves their ability to harden IP before it is released to other SoC groups that need to use these complex controllers.
A potential hazard of automated intent checking is that the tool may not prioritize the errors that really matter. An problem in one condition in part of the RTL may trigger a number of ancillary errors that the tool dutifully reports, but which obscure the root cause that, if fixed, will also solve many of the secondary problems. This is where smart reporting will play an important role.
Smart reporting looks one level deeper at the design and assembles the errors that really matter so that the designer is not forced to wade through a series of reports that, in reality, are simply shadows of the root cause. This smart reporting is a key component of the latest release of the Ascent Implied Intent Verification (IIV) automatic formal tool.
In a project at a major customer, Ascent IIV found some 3000 failures in a block of 130,000 gates. But, more importantly, rather than forcing the designer to look at each one in detail, narrowed down the causes of those errors to fewer than 200 – cutting out 94 per of the reporting noise that the design team would have seen from a tool without such smart analysis and reporting technology.
To ease debugging once the errors have been flagged up, Ascent IIV lets the user trace back to state-transition assignments, making it easier and faster to make changes to the RTL. To support the latest design and verification flows, Ascent IIV adds support for SystemVerilog 1800-2009. The result is that, even as state machines become ever more complex, verification tools are more than keeping pace.