Ten-million-gate switched fabric needs better verification

Ten-million-gate switched fabric needs better verification
Because Onex is a startup, our design and verification teams require efficient design flows and methodology to be effective. During the design phase of the company's service processor, the Switch Fabric chip, we recognized the need to incorporate formal equivalence checking into our silicon design flow. By guaranteeing equivalence of the register-transfer-level (RTL) description to our physical netlist at various stages of development, our verification engineers could prove functionality without resorting to gate-level simulations. We concluded that equivalence-checking tools were a key technology that would enable us to finish the design on time without sacrificing our product quality.

Basically, the Switch Fabric chip is a comprehensive software and a fully functional reference platform for telecom equipment vendors targeting the optical market. And, delivering a highly integrated silicon solution to the marketplace requires comprehensive verification, EDA tools and methodology. The Switch Fabric chip design is quite complex, on the order of 10 million gates, and has interface speeds greater than 2 GHz.

We evaluated various products for equivalence checking, making our primary criteria accuracy, ease of use and resource efficiency. We ultimately decided on Verplex Systems Inc. and its Conformal Equivalence Checker. The tool's Logical Equivalence Checker (LEC) offered an efficient syntax, with libraries and Verilog files specified in much the same way as NC-Verilog. This allowed a quick conversion from our existing simulation scripts. Also helpful was a straightforward mapping of registers in the RTL to the registers in the gate-level netlist. Register mapping is based on pattern rules, making the process extremely fast. LEC was able to run complete RTL-to-gate-level verification in 90 minutes, faster than we could load and initialize our full-chip gate-level simulation.

When we compared synthesized gates to RTL, we found several types of errors. One common issue was that of mismatched port widths in our top-level interconnect. In some cases, a port on one module was expanded, while the port on a connected module was overlooked. Since we used a bottom-up synthesis approach, certain gates were inferred during synthesis to handle the wider port, but never connected to any logic at the top level. Our synthesized netlist had gates with floating inputs as a result.

This type of problem would not necessarily be an issue during simulation, depending on the specific circuit involved. Without LEC, these problems would have persisted until ASIC vendor design rule checks identified the gates with floating inputs. These gates would then either have to be deleted from the netlist or tied off to ground, costing time and effort toward the end of the project. If only one module were modified, it would be necessary to synthesize only the affected portions of the netlist. If the comparison failed, we knew exactly which additional modules needed synthesis. LEC aided in this task by identifying unmapped points — registers that exist in the RTL but not in the gate netlist or vice versa.

The final problem seen during synthesis was a module-name duplication, which caused functional inconsistency within the netlist when integrated at the top level. This problem might not have been identified until late in the design cycle, perhaps not even until lab work with first-pass silicon. With LEC, it was a trivial edit to the Verilog source code. Once functional errors were fixed and verified against the RTL, we released the gate-level netlist to our vendor with a very high degree of confidence.

At this stage, the vendor modified the netlist during front-end processing. Test insertion added scan connections, RAM built-in self-test functionality and boundary scan. The resulting netlist was returned to us for evaluation. To compare this gate-level netlist with the RTL netlist, we declared test personality pins and ports to be tied to their functional-mode values. LEC propagated these constants throughout the gate-level netlist, ignoring the inserted test structures. While we found no errors introduced during test, it gave us considerable peace of mind to know with certainty that test insertion had not altered our normal functionality.

Clock tree generation was another task performed by the vendor. Our clock structure included several domains and gated clocks for power savings. It was clearly important to verify that creation of these clock trees did not alter the basic functionality of the device. One branch of our clock tree became inverted during various balancing operations. LEC was able to identify this by showing a list of registers that did not match their RTL functionality (nonequivalent points). Logical equivalence checking identifies the various bits of sequential logic that affect the value of the register being examined. We first noticed that the source bits in the RTL and the gate-level netlist were identical.

Next, we scrutinized the actual vectors that caused the error to occur. Knowing that only the clock structure had changed, we changed the clock value in one of the gate-level vectors and saw that it then matched the value seen in the RTL. We went back to the list of nonequivalent registers and identified the common module to which they belonged. To prove that this was the only problem, we edited the gate-level netlist, adding an inverter to the base of the offending branch. This modified netlist proved equivalent to our RTL, and the fix was complete. This became the base netlist for place, route and timing optimization. We were able to prove that the new netlist after all of these additional modifications, including logic restructuring and duplication, was functionally equivalent to our verified RTL.

Several problems were identified by ongoing RTL simulation during the time spent in physical design and optimization. We considered it highly desirable to integrate these changes into our release netlist. It was not feasible to go back to synthesis, discarding weeks of work in optimization, test insertion and clock tree creation. The only way to accomplish the change was by modifying the gate-level netlist directly. Since our functionality was verified in RTL, we needed some way to be certain that the engineering change order (ECO) was an equivalent implementation of the modifications. Since synthesis, scan insertion, buffering, logic restructuring and clock tree insertion had been performed, it was rarely possible to identify the proper gate-level fixes on the first attempt. Even a few lines of modified RTL could easily translate into hundreds of new gates, additional wires, deleted gates and new connections. This level of complexity could not be handled through manual review, and gate-level simulation was prohibitively expensive. Unmapped and nonequivalent points were early indicators of problems, and these often contained enough information for the ECO to be modified.

Other problems were not as easy, including the creation of a new configuration register along with associated address decoding for system bus access. For any nonequivalent point, we were able to generate two views of the logic. RTL was represented as functional gates created by the equivalence tool, while the gate-level netlist was displayed accurately by function. These views were specifically of the full cone of logic with fan-in to the nonequivalent point. By pruning out any unrelated gates, this was much more efficient than trying to view the full gate-level netlist in available network viewers.

In future projects we can expect to do less gate-level simulation, possibly eliminating it altogether. With LEC, we will be able to accelerate our development cycle and increase confidence in our released netlist. The reduction in time-to-market alone is worth the investment in tools and training. Our team could not imagine doing another design without formal verification in our tool arsenal.