Page 33

EETE JAN 2016

Circuit analysis & debug Continuing the momentum of formal verification By VChi-Ping Hsu erification solution providers seem to agree that it takes a family of engine technologies to efficiently cope with verification complexity. One of the critical members of that family is formal technology. Long known for the completeness and finality of its analysis, where applicable, formal has nonetheless been difficult to harness. There has been a shortage of expert users who understand the strengths and weaknesses of the underlying engines, along with the ultimate task at hand— the verification of a production SoC. However, encapsulation of formal technology use cases into “apps,” along with methodologies that contribute high verification value without requiring formal proofs to complete, have opened the door for “every man’s” formal technology. In 2015, formal verification is already a mission-critical technology for customers. In 2016, we can expect formal engines to continue growing in popularity with verification teams. Verification has always involved a family of technologies that need to be used together: simulation, emulation, FPGA prototyping, formal approaches, software-based verification. But historically, formal verification has been a difficult technique to adopt, since it has largely consisted of the formal engines requiring a lot of user expertise that hasn’t been broadly available. The reputation that it took a PhD in formal verification to be able to use the tool was not that far-fetched. However, formal tools have been democratized by two relatively recent developments: first, the emergence of apps that handle specific use cases that are very accessible to any verification engineer; and second, the emergence of methodologies, such as formal bug-hunting flows and the use of “bounded proofs,” which do not require formal proofs to actually complete in order to add substantial value to today’s verification flows. As a general rule, simulation is good at verifying the normal use cases of a block or an SoC, but formal finds the corner cases that nobody even thinks about. The apps make formal easy to use for straightforward cases by automating both the creation and proving of properties, also known as assertions, to fully verify these cases. Meanwhile, for more involved cases, bug-hunting flows and automated analysis of the verification achieved with incomplete (bounded) proofs have made it much easier for non-experts to derive huge verification value from incomplete exploration of assertions. Both of these recent developments have helped drive the use of formal verification forward. Most formal verification companies have switched to apps to get away from the “must have a PhD” stigma. Apps can make it easier to do the easy things and also provide functionality for more difficult tasks. For example, there are “boring” things like making sure that the microprocessor communicates correctly with the peripherals at the correct register addresses. This task requires a lot of simulation, but formal approaches can handle this fairly easily. There are now apps available for an array of targeted use cases. As an example, consider sequential equivalence checking. Power reduction has meant that netlists are not updated with a full preservation of register equivalence. They may be negated or even delayed if they do not need to be updated. The basic idea is that if a change to a register will never be noticed, then you can save power by not updating it. As a result, it will have the wrong value, which throws off traditional logical equivalence checking (LEC). A sequential equivalence checking app can input two RTL files and quickly verify their sequential behavioral equivalence. There are many other examples of useful formal apps. A security app can check that your keys cannot be leaked, or changed, by code that is not meant to have access to them. That is something that you probably really want to prove, rather than simply rely on a good choice of simulation vectors. A lowpower verification app can help you verify low-power designs with multiple power domains, voltage islands, power shutoff, clock shutoff, and all the other techniques used for reducing power. Of course, power is the main driver of SoC design these days, whether it is for mobile chips (in which extending battery life is paramount) or high-performance chips (where power limits how fast the design can be clocked). Very few designs are lucky enough not to require aggressive power management. In fact, it’s hard to believe that any major SoC doesn’t have power as a major constraint. So verifying the entire power architecture is an important step. Bug hunting and bounded proofs As mentioned earlier, formal is great at finding corner cases that the verification engineer doesn’t think about. We make great use of this capability in bug hunting. Here, rather than creating a test-bench that attempts to cover all eventualities, the verifica- Chi-Ping Hsu is senior vice president and chief strategy officer for electronic design automation (EDA) products and technologies at Cadence – www.cadence.com www.electronics-eetimes.com Electronic Engineering Times Europe January 2016 33


EETE JAN 2016
To see the actual publication please follow the link above