| |||||||||||||||||||||||||||||||
|
"Without Formality in the design process, we estimate that we would have spent at least a further 4-6 weeks on each ASIC in simulation and verification. Formality has been a critical part of our rigorous approach to the verification process for these three complex, high-performance ASIC’s."
Solution
Benefits
ECI Telecom is a world leader in integrated network solutions. Built on a solid foundation of customer commitment and technological excellence, ECI Telecom provides leading-edge digital telecommunications and data transmission systems to Network Service Providers around the globe. By deploying ECI Telecom’s "Do More" products in their telecommunications infrastructure, Service Providers can make their networks more competitive-offering everything from cost-effective expanded capacity and boosted performance to new profit-generating subscriber services. Assaf Sagir is a formal verification specialist in the ASIC Research and Development Network Systems Group at ECI Telecom. Here, he describes the critical role that Synopsys’ Formality played in tackling the design of multiple ASIC’s for a complex SDH system. The ASIC R&D team specializes in IC design for network equipment, in particular SDH products such as add-drop multiplexers and cross-connect switches. The customer for our most recent ASIC project was our own internal system design team, engaged on developing a new SDH product. The project required the design of a chipset for this application that consisted of three complex ASIC’s-with even the smallest design in excess of 2-million gates. All the designs had clock speeds of well over 100MHz and featured multiple clocks, including high-speed clock recovery schemes. We were targeting Lucent Microelectronics’ 0.18-micron process technology.
Complexity and Schedules Each ASIC design was started at a different time, with the aim of synchronizing delivery to the system engineers for integration into the final product. With a project duration of some 18 months and with scheduled tape-out dates all falling within three weeks of each other, the critical issue became keeping all the designs to the project timescale. Failure of any of the devices would set the whole project back by at least two months. Needless to say, we really wanted these devices to work to specification first time round. This was one of the most compelling reasons for considering the use of formal verification on the project. Adopting any new methodology on a large project represents a risk. In order to minimize this risk and the time associated with the change in methodology, we structured the project teams so that we had a mixture of dedicated designers on each project backed up by a number of methodology specialists floating between projects to provide specialist services. On average, over the life of the project we had around five dedicated designers per chip, with a total of five specialists overall in back-up roles. This turned out to be a successful strategy, demonstrated by the efficient use of Formality within the project on all three designs. After spending limited time learning the tool through experimentation on some of the ASIC modules and gaining a thorough understanding of the design flow issues, I tackled the formal verification of the first ASIC. I estimate we spent approximately five to six weeks in developing scripts to automate the verification process and actually running verification on the chip. For the second ASIC, this time fell to around four weeks and for the third to less than three weeks. This really demonstrated the value of gaining experience with the tool and new methodology.
Verification Process Elimination of functional errors is so critical that we take a very thorough approach to simulation. Once the RTL for a module has been developed and simulated, it is handed off to another member of the design team who will take their own interpretation of the specification and run independent simulations on the block to ensure conformance to specification. Once all blocks have been integrated, we establish conformance of the reference design by running extensive simulations on the top-level RTL. Some 60-70 percent of the entire project is spent running simulations and verification. In adopting Formality, we have replaced most-but not all-of our gate-level simulations. In adopting a new tool, it is very important to build confidence gradually. For this reason, and because formal verification supports such a critical part of our design process, we continued to run some gate-level simulations during the verification stages. In the future, as we gain more confidence in the tool and our ability to use it, we see gate-level simulation reducing further. Formality was used for both RTL-gate and gate-gate comparison as shown in Figure 1. Early in the design we used formal verification to validate the synthesis process. This was a quick process-we didn’t expect to find any problems, and in fact found none. Nevertheless, verification of the synthesis process was very important in building confidence as the development progressed. We found that the real value of using Formality in the design flow was during the back-end stages of design. In order to meet the timing requirements, in the later design stages our own designers made manual changes to the netlist and our vendor, Lucent, performed layout-based optimizations. Formality proved to be of major benefit in verification of these changes.
Figure 1 - Formality in the verification process
Back-end Bug Alert At least one bug was discovered, introduced into a design when two sets of signals were disconnected and inadvertently switched before reconnection. Formality alerted us to this soon after the change was made so that we were able to correct it without any significant penalty. This particular error would have taken a long time to discover using conventional simulation: it is quite possible we may not have discovered it until we tested the first samples.. It is not overstating the case to say that letting this error through would have been a catastrophic disaster, setting the project back at least two months, with significant cost implications. Using scripts enabled us to develop an automated approach to verifying the netlist at very regular intervals during the backend design stages-such as after test insertion, and after timing optimizations performed either by the ECI design team or by Lucent. The TCL scripts were structured so that verification could be initiated at any point in the hierarchy- from standalone verification of lower-level blocks to complete verification from the top level.
Best Practice Although much of the work with Formality was done at the shell level through scripts, we used the graphical user interface (GUI) to pinpoint any problems we found. Using scripts offers the best performance-in both speed and memory-enabling automation of repetitive tasks and providing control of overnight verification runs. The Formality GUI offers an excellent way of pinpointing problems. For example, it shows a comparison of two sub-cones up to the failing point-and the patterns, or vectors, generated in the verification process that caused the comparison to fail. Use of the GUI really assisted our working practices. For example, when I discovered an inconsistency, I could sit with the designer in front of the GUI and we could interactively isolate the problem very efficiently. Some switch designs, although complex, contain elements of replicated functionality and so allow a modular approach to be taken to both design and verification. One design consisted of four instances of a block, each with a further three levels of hierarchy-consisting of 30 or 40 modules in total. Full verification of this design at the top level took in excess of 13 hours, and used a lot of memory. Once the main block had been verified, we could replace the instances with a "black box" representation. This enabled us to verify the peripheral logic at the top level much more efficiently-reducing the run time to six to seven hours. This is an elegant solution to the verification time, but just add a word of caution here: it is essential to ensure that the black-box representation has identical behavior to the fully functional block that it replaces. We took a lot of care in checking the implementation design against the reference to ensure they were identical in behavior before substituting the black box.
Robust Verification One of our main concerns in adopting Formality was that we were introducing a tool into the design flow that was checking the quality of other Synopsys tools-that is, Design Compiler™ synthesis. We were concerned that, if there was any overlap in the Synopsys development teams, or any code re-use, then there was a danger that Formality could be vulnerable to the same errors that Design Compiler might have introduced. We were reassured to learn from Synopsys that the parsing block used in the Formality front-end was completely new technology, and that the new HDL reader was developed independently from other Synopsys tools, ensuring objective interpretation of HDL constructs. This was also demonstrated to us in a particular block, which a certain VHDL code style was interpreted slightly different by Design Compiler and Formality.
Summary All three ASIC’s are currently being integrated into the system design. So far, all three have produced correct test results and work to specification. Without Formality in the design process, we estimate that we would have spent at least a further 4-6 weeks on each ASIC in simulation and verification. Formality also flagged a critical bug that was introduced as a result of manual optimization, which would probably not have been found using dynamic simulation alone. Formality has been a critical part of our rigorous approach to the verification process for these three complex, high-performance ASIC’s. We are highly likely to increase our usage of Formality on future projects. |
||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||
