Real Intent’s Ascent family of front-end RTL verification tools serves multiple functions in the verification flow. The most important is that Ascent automatically finds functional bugs that are difficult to catch in simulation. While finding bugs early on is very important in itself, Ascent is much more than a bug hunter. Ascent also improves code coverage, saves simulation cycles, and reveals logic optimization potential. Some of these benefits are discussed here.
Code coverage is an important metric for simulation sign-off. Verification teams try to get as close to 100% coverage as possible. It is common for projects to struggle to achieve the 100% coverage due to a combination of reasons:
- A logic bug prevents a code block from being exercised
- A hole in the simulation test plan prevents a block of code from being exercised
The typical hard-to-detect unreachability bug is caused by unintended correlation between deeply nested control statements. This is very hard to detect in simulation since the test plan must exhaust all combinations of control values to determine that the nested block is unreachable. In other words, deeply nested unreachable blocks waste many simulation cycles, result in less than desired coverage, and, at the end of the simulation, one may still not be sure whether the block is truly unreachable.
Finding such unreachable blocks or demonstrating that hard-to-reach blocks are in fact reachable is relatively easy for Ascent’s formal engines. By using Ascent early on, the verification team can determine and fix unreachability issues before simulation is begun so that simulation cycles are not wasted trying to obtain unachievable coverage. On the flip side, Ascent can also help determine that a block not yet reached in simulation is in fact reachable, thereby indicating to the verification team that the test plan needs to be enhanced. Even better, Ascent can be used to find simulation traces to reach the difficult blocks.
Ascent also reveals optimization potential for simplifying designs.
For example, Ascent uses its deep-sequential formal engines to check for constant nets, constant expressions, unreachable states and unused state bits within a design. Because of the deep sequential analysis required to arrive at these results, the reported constant nets or expressions are often not easily identified manually. Those constants could be design bugs or opportunities for design simplification. A common reason for the presence of such constants is the interaction between new constraints and legacy RTL code, or the effect of system-level constraints on deeply embedded blocks. An original fragment from a real design where Ascent detected a constant expression is shown in Figure 1(a). Due to a programming requirement, the following constraint was imposed post facto on the inputs:
assume property @(posedge clk) disable iff (rst) (B==1’b0) |-> (A==1’b0) && (C==1’b0)
As a result, Ascent reported Y as a constant, meaning that the logic can be simply replaced by Figure 1(b). This change, of course, also results in further simplification in downstream logic.
In summary, Ascent can play a key role in achieving very high coverage with a much smaller amount of simulation as well as find optimization potential in your design – it does much more than just find bugs.