With rapidly growing chip functionality, design sizes are increasing. In addition, with the latest advances in logic synthesis at advanced nodes, designers make aggressive pushes in synthesis to achieve power, performance, and area (PPA) goals. These advances in both design size and complexity stress today’s equivalence checking proof methods and can result in long RTL-to-gate runtimes and, sometimes, inconclusive results. Equivalence checking is a critical step in digital tapeout flows, and the Conformal Smart Logic Equivalence Checker (LEC) solution addresses these issues.
Key Features
Massively parallel architecture automatically partitions designs, distributes formal proof strategies across multiple machines and CPUs, and can scale seamlessly to 100s of CPUs for improved runtime. This process is fully transparent to the user and does not require manual configuration.
Adaptive-proof technology finds the fastest solution to a conclusive proof with minimal user effort. It analyzes each partition and determines the optimal formal algorithm to minimize runtime and avoid proof timeouts—especially on designs with complex behavioral datapath components.
With the adaptive-proof technology and scalable, massively parallel architecture, designers can potentially improve their runtime by more than 20X.
