Integrating Formal Verification into Synthesis

Formal verification can be used for many things, but one is to ensure that synthesis performs correctly and that the behavior of the output netlist is the same as the behavior of the input RTL. But designs are getting very large and formal verification is a complex tool to use, especially if the design is too large for the formal tool to take in a single run. This is an especially severe problem for Oasys RealTime Designer because its capacity is so much larger than other synthesis tools. Using formal verification typically requires complex scripting and manual intervention to get results with reasonable runtimes.

Oasys and OneSpin Solutions have just announced an OEM agreement. Now, in EDA, OEM agreements really only work when the product being sold is integrated inside another (such as Concept Engineering’s schematic generator). Otherwise customers always prefer to buy the two products from their respective companies. This OEM is a tight integration. OneSpin is licensing a portion of its OneSpin 360 EC technology, automated functional equivalence checking software, to Oasys to integrate with RealTime Designer.

The integrated product allows RealTime Designer to drive the formal verification process automatically, dividing the design up into portions that can then be verified in parallel using multiple licenses. For example, a nearly 5 million instance design (so perhaps 30 or 40 million gates) can be verified in just over 2 hours using 10 licenses. The integration is fully compatible with the low power and DFT flows in RealTime Designer, correctly handling clock gating and scan chain insertion.

OneSpin EC equivalence checking ensures that the RTL design and the output gate-level netlist will produce the same results for the same inputs under all circumstances. It doesn’t use simulation-type approaches but is based on mathematically proving that this is so. In the event that this isn’t so (which would be a bug in RealTime Designer unless any manual intervention has taken place) it will produce a counter example.