High-Speed Equivalence Checking

Following on product introductions for simulation and prototyping, physical verification and implementation earlier in the year, Anirudh Devgan (Exec VP and GM at Cadence), the king of speed and parallelism has done it again, this time with logic equivalence checking (LEC). Cadence recently announced an advance to their well-known conformal LEC with a new Smart LEC.

First, some background on LEC for those who started design relatively recently. Back in the mists of time when logic synthesis was becoming popular, a question asked by many design team was how they could trust that synthesis didn’t make mistakes in translating from RTL to gate-level design. Back then one answer was to repeat RTL verification regressions at the gate level. But of course that was very slow and might still miss bugs that weren’t exposed in those regression suites. Today some amount of gate-level testing is making a comeback for other reasons but would be laughably ineffective for comprehensive RTL to gate equivalence checking.

Back in 2003 Cadence acquired a private company called Verplex who had built a tool to answer this problem (then called Conformal LEC, now Conformal EC), approaching the problem of checking equivalence between RTL and synthesized gate-level netlist in a different way, through formal verification. A formal equivalence check promised complete verification of logic equivalence, unlike simulation and could complete proving in relatively modest time, again unlike simulation. It took a little work to setup but quickly became popular and a de-facto part of the implementation flow where it was also used at ties to verify the logical correctness of implementation ECOs.

Synopsys had similar technology in Formality, but users raised a common concern – if I want to check the output of a tool from company X, do I really want to use a tool also from that same company or would I rather use a tool from a competing company? Fair or not, this thinking was widespread, contributing to Conformal leadership in this domain and arguably the first real commercial success for formal technology in production design flows.

As the technology became more embedded and more proven in flows, designers felt more comfortable using more aggressive synthesis options where before it would have been very challenging to validate the equivalence of before and after synthesis behavior in any comprehensive way.

Of course it wasn’t all plain sailing for formal-based proofs either. This was especially true around datapath components and optimizations. Validating multipliers, carry-save transformations and even more tricky blended operations (multiply-accumulate for example) can’t just be thrown at standard LEC algorithms. These required specialized approaches, and specialized user-directed scripting where needed.

All such problems were conquered one way or another, but over time the setup recipes and thus scripting to run LEC became more complex and required more expert guidance both within companies and from tool providers. A natural progression perhaps, but as designs get bigger, there was a natural desire to be able to parallelize verification, yet making that truly streamlined was hampered by all these complex user-defined recipes with multiple proof strategies.

Enter Conformal Smart LEC. This will now automatically partition a design with what Cadence calls adaptive proof technology which will assign appropriate proof strategies to different parts of the design, then launch those partitions across multiple machines/CPUs for parallel proving. The platform still supports scripting but notably, according to Kam Kittrell (Product management group director, Digital & Signoff Group at Cadence), Smart LEC has been able to run large designs with the default script rather than previous complex scripts (making setup much easier). And even using that default script it has been able to complete proofs 4X faster than the previous approach on a cited customer example. Cadence asserts that the tool can transparently scale up to run on 100s of CPUs (no script changes required) and that 20X+ improvements in runtime are possible.

You can learn more about Conformal Smart LEC HERE.