| A novel verification technique to uncover out-of-order DUV behaviors |
| Full text |
 Pdf
(159 KB)
|
| Source
|
Annual ACM IEEE Design Automation Conference
archive
Proceedings of the 46th Annual Design Automation Conference
table of contents
San Francisco, California
SESSION: Jumping the high-level verification hurdle
table of contents
Pages 448-453
Year of Publication: 2009
ISBN:978-1-60558-497-3
|
|
Authors
|
|
Gabriel Marcilio
|
Federal University of Santa Catarina, UFSC, Florianopolis, Brazil
|
|
Luiz C. V. Santos
|
Federal University of Santa Catarina, UFSC, Florianopolis, Brazil
|
|
Bruno Albertini
|
University of Campinas, UNICAMP, Campinas, Brazil
|
|
Sandro Rigo
|
University of Campinas, UNICAMP, Campinas, Brazil
|
|
| Sponsors |
|
| Publisher |
|
| Bibliometrics |
Downloads (6 Weeks): 17, Downloads (12 Months): 17, Citation Count: 0
|
|
|
 ABSTRACT
Post-partitioning verification has to deal with abstract data, implementation artifacts, and the order of events may not be preserved in the DUV due to the concurrency treatment in the golden model. Existing techniques are limited either by the use of greedy heuristics (jeopardizing verification guarantees) or by black-box approaches (impairing observability). This work proposes a novel white-box technique that overcomes those limitations by casting the problem as an extended bipartite graph matching. By relying on proven properties, solid verification guarantees are provided. Experimental validation was performed upon platforms built around contemporary real-life applications.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
B. Albertini, S. Rigo, G. Araujo, C. Araujo, E. Barros, and W. Azevedo. A Computational Reflection Mechanism to Support Platform Debugging in SystemC. In Proc. of the International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), pages 81--86, 2007.
|
| |
2
|
B. Bailey. The Functional Verification of Electronic Systems: An Overview from Various Points of View. International Engineering Consortium, 2005.
|
| |
3
|
F. Ghenassia. Transaction-Level Modeling with SystemC: TLM Concepts and Applications for Embedded Systems. Springer, 2005.
|
| |
4
|
M. Hall. An Algorithm for Distinct Representatives. American Mathematical Monthly, No. 10, 63:716--717, 1956.
|
| |
5
|
ISO IEC 11172-3 Standard Implementation. ftp://ftp.tnt.uni-hanover.de/pub/mpeg/audio/mpeg2/software.
|
| |
6
|
C. Jacobi. Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving. Lecture Notes in Computer Science, 2404:211--226, 2002.
|
| |
7
|
G. Martin, B. Bailey, and A. Piziali. ESL Design and Verification: A Prescription for Electronic System Level Methodology. Morgan Kaufmann, 2007.
|
| |
8
|
Mibench suite. http://www.eecs.umich.edu/mibench.
|
| |
9
|
D. A. Patterson and J. L. Hennessy. Computer Organization and Design: The Hardware/Software Interface. Morgan Kaufmann, 2007.
|
| |
10
|
J. U. Skakkebaek, R. B. Jones, and D. L. Dill. Formal Verification of Out-of-Order Execution with Incremental Flushing. Lecture Notes in Computer Science, 1427:98--109, 1998.
|
| |
11
|
B. Wile, J. Goss, and W. Roesner. Comprehensive Functional Verification: The Complete Industry Cycle. Morgan Kaufmann, 2003.
|
| |
12
|
J.-S. Yim, C.-J. Park, W.-S. Yang, H.-S. Oh, H.-C. Lee, H. Choi, T.-H. Kim, S.-J. Lee, N. Won, Y.-H. Lee, I.-C. Park, and C.-M. Kyun. Verification Methodology of Compatible Microprocessors. In Proc. of the Asia and South Pacific Desing Automation Conference, pages 173--180, 1997.
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
B.5