I recently joined Real Intent with over 10 years of experience developing and supporting assertion-based methodologies and have seen the technology move from research toward the mainstream. Formal technologies have proven to have a lot of value for functional verification and for coverage, but having to learn evolving assertion languages and techniques has slowed the adoption. I like Real Intent’s approach of automating the verification effort.
In the very early stages of design, linting is a basic step. Lint checkers for HDL have been around for some time, and continue to become more sophisticated. AscentTM Lint runs very fast because the checks are all static. The user can easily configure what checks are desired.
In the next stage, also early in the process but after linting, Real Intent has what is my favorite tool – Implied Intent Verifier (IIV). They have adapted formal verification techniques to automatically detect issues that can result in bugs that might be difficult to trigger and detect in simulation. Think of this as automatically generated assertions. Formal verification without having to write assertions! It is all automatic. IIV goes beyond static linting to detect bugs that require sequential analysis.
An example of a significant IIV check is the one for state machine deadlocks. Deadlocks are the type of symptom that foreshadow bugs that can result in product recalls if not found. Finding them often depends on whether the testbench author thinks to test the scenario. IIV provides detection of deadlock in one FSM and between two FSMs, without the need to write any testbench or assertions. For example,
This is the classic example of two state machines that are waiting on one another. In this case a single-state deadlock (SSD) is reported for both state machines and the deadlocked state is state 00. This is because state machine A is waiting on a signal from state machine B and vice-a-versa.
Many other errors are also reported that have the same root cause. One of the unique features of IIV is that it distinguishes secondary failures. The report focuses your effort on the root cause of a failure, in this case the SSD, and you can ignore the secondary failures.
While this example was very simple for the purpose of illustration, you can imagine a similar scenario in protocols. Take for example, a peer-to-peer handshake where both request to transmit at the same time, causing them to both go to a state where they are waiting for an acknowledge signal from their peer. This would be a fundamental state machine design issue. Simulations would pass unless the corner case where both request simultaneously is tested. As shown in the simple example above, this can also happen as the result of a simple typo.
You can get a fast start in functional verification by exploiting the verification features provided in Real Intent’s tool suite. Common bugs are quickly and automatically weeded out, building a strong foundation for the real work of verifying your specific design intent. Check out Real Intent’s complete product line at www.realintent.com .