Static netlist verification for IBM high-frequency processors using a tree-grammar
Abstract
This paper introduces a new static verification technique using tree-grammars. The core contribution is the combination of a structural netlist traversal with parser generation techniques for tree-grammars. Today's commercial static analysis tools offer a rich set of parameterized connectivity checks, but their predefined nature prevents effective checks on the highly customized structures found in high-end processor designs. The method presented here allows to formulate the required connectivity using a tree-grammar, thus combining high checking flexibility with convenient specification. Unlike other grammar based structural verification approaches, this method does not require the complete netlist to be matched against the production rules, which allows short runtimes even on large multi-core chip netlists. Results are presented for the most recent 22nm high-end processor designs.
References
[1]
Atrenta Inc. An automated approach to RTL memory BIST insertion and verification. http://www.atrenta.com/resources/white-papers.htm5. Accessed November 25, 2014.
[2]
Atrenta Inc. Atrenta SpyGlass. http://www.atrenta.com/products/spyglass.htm5. Accessed November 25, 2014.
[3]
Mentor Graphics. Questa clock-domain crossing (CDC) verification. http://www.mentor.com/products/fv/questa-cdc/. Accessed November 25, 2014.
[4]
PCRE - Perl Compatible Regular Expressions. http://www.pcre.org. Accessed November 25, 2014.
[5]
Synopsys Inc. Next-generation CDC static checking. http://www.synopsys.com/tools/verification/static-formal-verification/pages/vc-cdc-ds.aspx. Accessed November 25, 2014.
[6]
R. D. Adams, R. Abbott, X. Bai, D. Burek, and E. MacDonald. An integrated memory self test and EDA solution. In 12th IEEE International Workshop on Memory Technology, Design, and Testing (MTDT 2004), 9--10 August 2004, San Jose, CA, USA, pages 92--95, 2004.
[7]
Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques and Tools. Addison Wesley, 1986.
[8]
T. Asaka, M. Yoshida, S. Bhattacharya, and S. Dey. H-SCAN+: A practical low-overhead RTL design-for-testability technique for industrial designs. In Proceedings IEEE International Test Conference 1997, Washington, DC, USA, November 3--5, 1997, pages 265--274, 1997.
[9]
C. Bamji and J. Allen. Grasp: A grammar-based schematic parser. In DAC, pages 448--453, 1989.
[10]
G. H. Chisholm, S. T. Eckmann, C. M. Lain, and R. Veroff. Understanding integrated circuits. IEEE Design & Test of Computers, 16(2):26--37, 1999.
[11]
E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.
[12]
E. J. Fluhr et al. POWER8™: A 12-core server-class processor in 22nm soi with 7.6tb/s off-chip bandwidth. In Solid-State Circuits Conference Digest of Technical Papers (ISSCC), 2014 IEEE International, pages 96--97, 2014.
[13]
J. Warnock et al. POWER7™ local clocking and clocked storage elements. In IEEE International Solid State Circuits Conference, 2010. Paper 9.3.
[14]
J. Warnock et al. 22nm Next Generation IBM System Z Microprocessor. In Solid-State Circuits Conference Digest of Technical Papers (ISSCC), 2015 IEEE International, pages 70--71, 2015.
[15]
H. D. Man, I. Bolsens, E. V. Meersch, and J. V. Cleynenbreugel. DIALOG: An expert debugging system for MOSVLSI design. IEEE Trans. on CAD of Integrated Circuits and Systems, 4(3):303--311, 1985.
[16]
T. Parr. The Definitive ANTLR Reference: Building Domain-Specific Languages. Pragmatic Programmers. The Pragmatic Bookshelf, Raley, May 2007.
[17]
G. Pelz. An interpreter for general netlist design rule checking. In DAC, pages 305--310, 1992.
[18]
G. Rozenberg, editor. Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations. World Scientific, 1997.
[19]
Spickelmier, R.L. and Newton, A.R. Critic: A knowledge-based program for critiquing circuit designs. In VLSI in Computers and Processors, pages 324--327, 1988.
[20]
T. Webel, T. Pflueger, R. Ludewig, C. Lichtenau, W. Niklaus, and R. Schaufler. Scalable and modular pervasive logic/firmware design. IBM J. Res. Dev., 56(1):54--63, January 2012.
[21]
L. Yang and C.-J. R. Shi. FROSTY: A fast hierarchy extractor for industrial CMOS circuits. In ICCAD, pages 741--747, 2003.
Recommendations
Tree insertion grammar: a cubic-time, parsable formalism that lexicalizes context-free grammar without changing the trees produced
Tree insertion grammar (TIG) is a tree-based formalism that makes use of tree substitution and tree adjunction. TIG is related to tree adjoining grammar. However, the adjunction permitted in TIG is sufficiently restricted that TIGs only derive context-...
Tree insertion grammar: a cubic-time, parsable formalism that lexicalizes context-free grammar without changing the trees produced
Tree insertion grammar (TIG) is a tree-based formalism that makes use of tree substitution and tree adjunction. TIG is related to tree adjoining grammar. However, the adjunction permitted in TIG is sufficiently restricted that TIGs only derive context-...
Zero-Change Netlist Transformations: A New Technique for Placement Benchmarking
In this paper, the authors introduce the concept of zero-change netlist transformations (ZCNTs) to: 1) quantify the suboptimality of existing placers on artificially constructed instances and 2) "partially" quantify the suboptimality of placers on ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
March 2017
1814 pages
Publisher
European Design and Automation Association
Leuven, Belgium
Publication History
Published: 27 March 2017
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 58Total Downloads
- Downloads (Last 12 months)34
- Downloads (Last 6 weeks)9
Reflects downloads up to 15 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in