IP Verification : Plugging the verification time sink

Marvell engineers recently designed three concurrent ASICs for the mass storage market. Each was a high-density SoC that included a memory block, MPU, and analog blocks. The size of the design teams ranged from six to 15 engineers per project, who found that 50 percent of their time was spent on verification. Projects normally last between four and nine months, so it is within reason to speculate that nearly an entire year of Marvell design time was allotted to verification.

These designs typically required five or more clocks with rates in the range of 100Mhz t o greater than 200 MHz. Design sizes were at least 300K gates for the digital portion. A custom ASIC flow was used for front-end design entry. A mixture of IP from customers and internal designs was used. The types of IP were a combination of hard macros and RTL soft macros.

Both hand written code in Verilog, as well as VisulaHDL from Innoveda were used to describe the designs. Innoveda's HDCScore was used for coverage while Verisity's SureLint was chosen for linting. Synopsys' VCS was selected for the simulation and Design Compiler for the logic synthesis.

An equivalence checker from Verplex (Conformal Logic Equivalence Checker) verified the netlists produced by the design implementation process back to the golden RTL. Verification of post-synthesis, pre-scan versus post-scan, post-layout, and engineering change orders were performed using logic equivalence checking throughout the design process.

Verplex Conformal LEC uses a correlation learning technique to compare designs and simplify the proof process, which enables comparisons of RTL to flattened netlists.

Since the IP was of all varieties — hard, gray and soft macros — making sure the interface timing was met was difficult because not every macro had timing library information. If the design contains an MPU, then co-simulation was involved.

It was found that most of the bugs showed up during system-level simulation, since corner cases were not always included in block-level verification. For example, the module/block designer may have made assumptions that didn't always work when added together. Depending on the test, some ran for hours in gate level with timing.

Equivalence checking offered significant cost and time savings. RTL simulation was run to verify the functionality and then the logic equivalence checker was used to make sure the functionality wasn't changed by synthesis. Static timing analysis insured the timing budget was met. This methodology significantly reduced e ngineering time, gate-level simulation runs, and shortened the schedule.

The logic equivalence checker isolated design differences and displayed them graphically back to the original source code. Counter examples of patterns were generated, viewed on a table-like format, and displayed on the schematic viewer.

The logic equivalence checker supported changes to specification-generated ECOs, and enabled the team to verify pre- and post-ECO netlists to ensure hand modifications to the netlist were done properly. This allowed the staff to redesign the functionality in RTL and compare it to the hand-edited netlist, assuring that the final netlist was correct without repeatedly taking the design through design implementation.

One particular project had a number of wafers on hold at the base layer because new cells could not be added, bringing intense pressure to engineering because the financial impact of placing manufacturing on hold indefinitely was significant. As a result, most of t he ECOs were done using spare cells and verifying ECO functionality became critically important.

The back end process flow, to better solve integration issues, was vastly improved by the addition of a formal verification strategy. In reviewing the overall experience, we realized that verification must be independent from the design flow. The logic equivalence checker chosen in this example does not rely on synthesis or other verification tools.

See related chart