Static Netlist Verification for IBM High-Frequency Processors using a Tree-Grammar

Christoph Jäschkea, Ulla Herterb, Claudia Wolkoberc, Carsten Schmittd and Christian Zoelline
IBM Deutschland Research & Development GmbH, Schönaicherstr. 220, 71032 Böblingen, Germany.


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 treegrammars. 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 treegrammar, 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.

Full Text (PDF)