Conformal Smart LEC

Design sizes and complexity are increasing with rapidly growing functionality at advanced nodes. Designers must apply more functions for synthesis optimization to achieve their PPA goals, especially in datapath-intensive designs. These advances in size and complexity in designs are challenging current equivalence-checking proof methods, resulting in long runtimes and inconclusive results. Equivalence checking, as a critical component in tapeout flows, must keep up. Conformal Smart LEC addresses these challenges with a suite of new “smart” technologies.

As Figure 1 shows, Conformal Smart LEC is a superset of the existing Conformal L and Conformal XL configurations. Conformal L offers core equivalence-checking technology; Conformal XL adds automated checking of complex datapaths and equivalence checking of the final place-and-route netlist. In addition to capabilities provided by the L and XL configurations, Conformal Smart LEC delivers next-generation equivalence checking with smart instance selection, adaptive proof, and massive parallelization technologies.

Smart instance selection identifies modules and detects aborts accurately for hierarchical comparison. This feature minimizes dynamic flattening, and thus improves overall performance.

Conformal Smart LEC has an extensive portfolio of formal solvers that can handle all conceivable design syntheses and implementations. Adaptive proof technology orchestrates the solvers, so users do not have to iterate over their verification strategies. With a single command, Conformal Smart LEC analyzes the characteristics of both the golden and revised designs, such as datapath type and logic complexity. Based on the analysis results, the command automatically applies the most appropriate strategy to complete the comparison. See Figure 2.

The strategies are different for different parts of the design and the result is effectively a fine-grain strategy customization that is very difficult or nearly impossible to replicate manually. With adaptive proof technology and scalable massive parallelism, designers can achieve runtime improvement of up to 20X.

Conformal Smart LEC introduces a massively parallel architecture that can utilize multiple hosts and cores to maximize computation results. Designers can use this new architecture to run module comparisons in hierarchical equivalence checking across multiple CPUs and hosts. In addition, the parallel hierarchical comparison uses smart scheduling to reduce runtime and improve resource efficiency. For a design with an evenly distributed module complexity, parallelizing the hierarchical comparison can significantly reduce the turnaround time. To achieve parallel efficiency, Conformal Smart LEC uses continuous workers— processes containing the entire design—to run the module comparisons. See Figure 3. Workers can be invoked on the local host or remote machines.

During the run, workers collaborate to compare the modules in parallel. When switching between different modules, workers can quickly set up the target module and perform verification without reloading the design data. Workers can use all Conformal Smart LEC multithreading features— including comparison, module datapath analysis (MDP), bit-level datapath analysis, non-exact synthesis module and abort analysis—thereby, achieving massive parallelization.