MARCH-APRIL 2007 (Vol. 24, No. 2) pp. 110-111
0740-7475/07/$31.00 © 2007 IEEE
Published by the IEEE Computer Society
Published by the IEEE Computer Society
Guest Editors' Introduction: Attacking Functional Verification through Hybrid Techniques
PDFs Require Adobe Acrobat
In industrial design environments, verification engineers are typically not required to write formal properties for system correctness, but they are expected to maximize verification coverage. They must do this under the dual constraints of design cost and time to market. In the absence of complete formal-verification solutions for industrial-strength designs, and given that simulation is still the mainstay for real-life verification issues, a new breed of hybrid validation tools and techniques has come to the forefront. The scalability of simulation, along with its universal appeal of being easily applicable to practically any design, makes it useful for all verification tasks. Its drawbacks are being addressed through powerful analysis tools such as formal verification, automatic test-pattern generators, symbolic techniques, satisfiability (SAT) checkers, bounded model checking, and data mining. The problem has become one of efficiently combining the disparate techniques so that they can cooperate with one another in a meaningful way.
Hybrid techniques have proven effective in exploring interesting corner cases, coverage holes, invariant variations, and so forth, in the general area of directed functional validation. Despite the emergence of several demonstrably effective hybrid validation techniques, both industrial and academic, several questions remain: Do hybrid techniques enable fast and improved design validation? Have the supporting methodologies that can maximize the gain from hybrid techniques matured? What major issues are being addressed by teams of engineers working in the area of directed functional validation in industry? To help explain some of the different facets of this area, we present this special issue, which includes five articles.
The issue begins with a survey article on the topic, which we wrote along with our colleague, Sandip Ray. This survey article outlines some of the recent work in this rapidly developing area. Next, in "Hybrid Verification of Protocol Bridges," Praveen Tiwari and Raj Mitra demonstrate that a hybrid framework can find bugs that individual techniques are unable to find alone. They have developed a technique that uses simulation and formal verification to complement scalability and completeness. The application domain is protocol verification.
In "Combining Theorem Proving with Model Checking through Predicate Abstraction," Sandip Ray and Rob Sumners present a procedure for proving invariants of infinite-state reactive systems using a combination of two formal verification techniques: theorem proving and model checking. This method uses term rewriting to reduce an invariant proof of the target system to reachability analysis on a finite predicate abstraction that can be discharged by model checking. The method affords substantial automation in invariant proofs, while preserving the expressiveness and control afforded by theorem proving.
"Hybrid, Incremental Assertion-Based Verification for TLM Design Flows," by Nicola Bombieri et al., addresses problems that arise in refining now-ubiquitous transaction-level models to efficient RTL models. The authors present a hybrid, incremental, assertion-based verification technique to check the correctness of the refinement. Owing to the manual nature of the translation process, this method is an important tool for catching bugs early in the design cycle. The authors also demonstrate the effectiveness of their technique on an industrial-strength design.
Finally, in "Hybrid Approach to Faster Functional Verification with Full Visibility," Chin-Lung Chuang et al. present an interesting technique that combines simulation and emulation to achieve a faster, more efficient front-end debugging environment. Logic simulators provide controllability and observability, and emulators offer speed. To achieve faster debugging, the authors present a platform in which an emulator's internal states are recorded and later played back through a software simulation environment. They demonstrate that the technique provides excellent speedup.
Although a comprehensive verification methodology for arbitrary designs remains an elusive goal, there is an encouraging trend to enhance the capability of verification methodologies through the cross-pollination of hybrid techniques. Some of these hybrid techniques are even supported today by a variety of commercial tools. Perhaps it will be through these cross-pollination efforts that one day we will achieve that elusive goal of a comprehensive verification methodology. Of course, it is impractical to address all hybrid verification within a single issue. However, we hope these five articles can provide a good source for further references and future research. We thank all the authors and referees for their contributions in creating this special issue. We also express our sincere thanks to our colleague and friend Tim Cheng (EIC of IEEE Design & Test) for his support and guidance. We hope that you enjoy this special issue and that it inspires more research to overcome future verification challenges.
Jayanta Bhadra is the technical lead of formal verification and validation at Freescale Semiconductor. He has worked on the verification of several generations of PowerPC microprocessors. His research interests include testing and verification of digital systems, mathematical logic, VLSI algorithms, and multicore verification. Bhadra has a PhD in electrical and computer engineering from the University of Texas at Austin. He is a member of the IEEE.
Magdy S. Abadir is the manager of EDA strategy, EDA vendor relations, and customer collaboration at Freescale Semiconductor. He is also an adjunct faculty member at the University of Texas at Austin, and he is Associate EIC of IEEE Design & Test. His research interests include microprocessor test and verification, test economics, and DFT. Abadir has a BS in computer science from the University of Alexandria, Egypt, an MS in computer science from the University of Saskatchewan, and a PhD in electrical engineering from the University of Southern California. He coedited the IEEE Design & Test special issue on functional verification in 2004. He is an IEEE Fellow.
Li-C. Wang is an associate professor in the Department of Electrical and Computer Engineering of the University of California, Santa Barbara. His research interests include microprocessor test and verification, statistical methods for timing analysis, speed test and performance validation, and applications of data mining and statistical learning in EDA. Wang has an MS in computer science and a PhD in electrical and computer engineering, both from the University of Texas at Austin. He coedited the IEEE Design & Test special issue on functional verification in 2004.