"Faced with the tight deadlines, we decided to enhance our conventional simulation-based methodology by adding Formality’s equivalence checker."
Mr. Kazumasa Doi,
Fujitsu Digital Technology
Fujitsu Digital Technology (FDT) is engaged in a broad spectrum of design and development activity centered primarily on development of core systems for data communication networks ranging from system LSI development to network operation systems. FDT provides total solutions consisting of consulting for data communication systems and operations. VLSI Design Department, Osaka, New Business Division of FDT, develops RTL to netlist designs specializing in high-performance complex chips. For their customers thorough verification is a must, and down time can be catastrophic. Relying on traditional simulation technology alone for gate-level regression testing increases risk by delaying bug discoveries and leads to a longer design iteration. Both of which negatively impact tape-out schedules. To survive in a highly competitive networking market, the risk is too large to ignore.
With this in mind, FDT has developed a best-in-class verification environment for SoC designs that includes the Synopsys’ Formality® equivalence checker to guarantee RTL-to-Gate equivalence. FDT partnered with Formality three years ago to deliver best in quality, multimillion-gate chips. Formality continually enables FDT to deal with increasing complexity and to provide higher quality results on schedule. With Formality, FDT has successfully taped out approximately 60 chips.
Formality Maintains QoR and Shortens TAT
"It became obvious that we needed a methodology to reduce the design TAT (turn around time) and prevent risk in order to meet our severe customer requirements," says Mr. Kazumasa Doi at FDT. "At that time we were engaged in RTL to netlist designs of 1-million gates. We would simulate our chip at the register transfer level (RTL) to ensure that the behavior matched specification. Once we confirmed/guaranteed the timing after synthesis and layout, we would perform a gate-level simulation to ensure functional integrity was not lost during the implementation. However, this approach is problematic because implementation bugs are found too late. Another problem was that the gate-level simulation took too long. The quality of gate-level simulation and design schedule is always a trade-off, but it is impossible to keep the same verification exhaustiveness found in an RTL simulation at the gate level. Moreover, we had a risk of missing bugs because you can’t obtain complete coverage with the simulation methodology. Additionally, we did not have a methodology to efficiently guarantee the integrity between the golden RTL model and the final net list."
Mr. Doi thought formal verification techniques were necessary to solve these problems. Future projects would require larger designs, with more functionality, while trying to achieve the same quality within a shorter design cycle.
"Faced with the tight deadlines, we decided to enhance our conventional simulation-based methodology by adding Formality’s equivalence checker," says Mr. Doi. "Using Formality we were able to guarantee the quality of the ASICs and shorten the turn around time (TAT)."
Formality determines functional equivalence by comparing different stages of a design. Formality uses mathematical verification methods, requiring no simulation vectors, allowing designers to rapidly detect implementation errors. Formality’s multi-solver architecture permits RTL-to-gate verification of complex, multi-million-gate, SoC designs. Formality runs in a matter of minutes or hours, instead of the weeks and months typically required by gate-level simulation.
Formality Contributes to FDT’s On-going Success
"Formality enables us to meet the customer’s various requirements," said Mr. Hatakeyama. "For example, we occasionally reuse chip designs by porting them to the latest process technology. In other cases, we may integrate several tested chips into a new system, but we’ll only have access to the tape-out data. To illustrate my point, we integrated four chips into a single package of 1-million gates. We defined the netlist of the proven original design as the golden model. We then used Formality to compare the equivalency of the logic, excluding test circuitry, between the golden model and the new netlist that had been redesigned for the targeted technology. Using Formality we were able to verify designs of different process technologies as well as different scan methodologies. Without the need for test vectors, Formality quickly verified large SoC designs that had been created by the merging of several existing chips. Formality enabled us to maintain a short design cycle and reduce development cost while meeting our customer requirements," says Mr. Yoshiyuki Hatakeyama at FDT.
"Formality requires minimal setup at the chip level, so we can eliminate the extra effort that would be required if we had to verify hierarchically. It also removes the extra process of creating a new netlist for hierarchical verification, eliminating the risk of introducing mistakes during that process. Thus, Formality’s capacity extends the advantage and quality of the formal verification methodology itself."
Fujitsu Digital Technology
"When we redesign a chip for a technology requiring another test style, we use 'translate' in Design Compiler."Formality handles the different hierarchical structure and the different instance names caused during the ‘translate’ process. Nevertheless, we create the model for ‘translate’ so that the instance names are as close as possible. We also use ‘ungroup -simple_name’ to match the hierarchical structure before and after the technology transfer. Designers keep formal verification in mind during the design flow so that we can get optimal results from the tool," says Mr. Hatakeyama.
A recent FDT design was a system control LSI for high-speed digital telecommunication. The design was roughly 1.5-million gates, and it included a configurable processor and a hard macro made by Fujitsu. It was designed using VHDL and C. The design period was approximately five months from coding to tape out. This System-on-a-chip was designed as follows:
"Once the design spec was approved, we began developing a C-level functional model. We then performed the functional evaluation using ISS. After we partitioned the design into the hardware and software components, we designed the hardware in cycle-based C", says the design engineer. "We then performed hardware and software co-verification in C and ran RTL verification".
The team’s front-end design environment is based on Design Compiler from Synopsys Inc., and they use an in-house tool for the back end.
"We first use Formality after synthesis to ensure integrity between the RTL and the netlist. The objective is to not only transfer the golden design from the RTL to gate level but also to reduce the verification iteration between the RTL and gate level." explains Mr. Hatakeyama. "We insert test circuitry for full scan and use Formality to ensure equivalency between the pre- and post-insertion implementations. If we change the netlist in the backend, we use Formality to check the equivalency of the design before and after the change. We also check equivalency before and after a timing adjustment. Lastly, we check and guarantee the functional equivalency between the original golden RTL and the final netlist. Formality flexibly deals with each verification checkpoint and continues to provide the highest quality as design size and functionality increase. Formality enables us to find problems during implementation and minimize the amount of gate-level simulation."
Formality’s New Solvers and Hier-IQ™ Technology Increase Capacity
"The solvers added to Formality 2000.11 and the Hier-IQ technology introduced in 2001.08 significantly improved Formality’s memory usage and run time", says Mr. Hatakeyama.
"With Formality 2000.11, we were able to verify a 3-million gate design that earlier versions could not handle due to memory limitations. With the new solvers in 2000.11 the design took about 6.5 hours to verify after the first mapping and about 4.2 hours after scan insertion and timing adjustment. The minor releases, 2000.11-FM1 and FM2-SP1, improved runtime another 28 percent after the initial mapping and 8 percent after scan insertion and timing adjustment. On the same design, Hier-IQ technology introduced in 2001.08 reduced the run time after the first mapping to just 3.8 hours and runtime after scan insertion and timing adjustment to 3.0 hours. This is an improvement of 40 percent and 30 percent between Formality 2000.11, FM1.0, and Formality 2001.08 respectively."
Mr. Hatakeyama explains the significance of these improvements. "The fact that Formality handles large designs is very significant. Formality requires minimal setup at the chip level, so we can eliminate the extra effort that would be required if we had to verify hierarchically. It also removes the extra process of creating a new netlist for hierarchical verification, eliminating the risk of introducing mistakes during that process. Thus, Formality’s capacity extends the advantage and quality of the formal verification methodology itself. Currently FDT is using Formality on a 5-million gate design.
FDT Expands its Quality of ASIC to FPGA
"FPGA technology has dramatically improved in terms of density, speed and cost effectiveness. It is not unusual to integrate an FPGA in the final system. FPGA requires the same quality of ASIC. Therefore, the same level of thorough verification is necessary, including static timing analysis and logic equivalency checking. In the past, if we were to use an FPGA as an ASIC prototype, there was no methodology to prove the equivalency between FPGA and the ASICs designed by different tools with different synthesisable subsets", says Mr. Hatakeyama. "However, since Formality started supporting FPGA we are now able to verify the logic equivalency between a FPGA and ASIC design. We take the RTL verified by logic simulation and define it as the golden model. We then use Formality to check between the Golden RTL and the FPGA, as well as the Golden RTL and ASIC. By using Formality effectively we can achieve FPGA quality that is consistent with that of our ASICs."
Advantage of Formal Verification and Future Perspective
"Since adopting Formality almost three years ago, we have not had a single chip failure due to implementation errors. Formality enables us to find problems quickly and easily. We are able to deliver products early to the market while maintaining the highest level of product quality. With Formality in our flow, we have successfully taped out roughly 60 telecom chips of increasing complexity," says Mr. Doi.
"However, the possibility of introducing mistakes during implementation is not zero. We cannot know whether potential mistakes will be caused by manual work or tool failure. We cannot know when, in what process, and how the mistakes will be introduced. Unless we use a formal verification methodology, designers can only find problems during gate-level simulation, at the last stage of the design process. With this is mind, a formal verification tool that can verify the correctness of an implementation at each stage of the design, independent from the implementation tools, provides the best quality to FDT and our customers," says Mr. Doi.
"We believe Formality will continue to be the de-facto standard equivalence checker for our multi-million-gate SoC designs and a strong partner of FDT as we target 100 percent quality. By integrating Formality in the design flow, FDT is meeting our goal of delivering chips of various complexity early to the market," concludes Mr. Doi.
As the data shows, Formality continues to improve. Formality 2002 delivers a new GUI, improved reader, various reporting and debug functions, as well as run time and memory usage reduction.