Date: Thursday 30 March 2017
Time: 14:00 - 15:30
Location / Room: 3B
Chair:
Barbara Jobstmann, EPFL / Cadence, CH
Co-Chair:
Christoph Scholl, University of Freiburg, DE
The session consists of three papers on formal verification and its applications. The first paper presents the use of grammar-based techniques for the analysis of high-end processor designs at the netlist level. The second paper considers a computer algebra-based technique to reverse engineer the irreducible polynomial used in the implementation of multipliers in finite fields. The third paper applies probabilistic model checking in a case study analyzing the dependability of optical communication networks with double-ring topologies (which have been proposed for multicast traffic in metropolitan areas).
| Time | Label | Presentation Title Authors |
|---|---|---|
| 14:00 | 11.7.1 | STATIC NETLIST VERIFICATION FOR IBM HIGH-FREQUENCY PROCESSORS USING A TREE-GRAMMAR Speaker: Christoph Jaeschke, IBM Deutschland Research & Development GmbH, DE Authors: Christoph Jaeschke, Ulla Herter, Claudia Wolkober, Carsten Schmitt and Christian Zoellin, IBM Deutschland Research & Development GmbH, DE 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. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 14:30 | 11.7.2 | REVERSE ENGINEERING OF IRREDUCIBLE POLYNOMIALS IN GF(2^M) ARITHMETIC Speaker: Cunxi Yu, University of Massachusetts, Amherst, US Authors: Cunxi Yu1, Daniel Holcomb1 and Maciej Ciesielski2 1University of Massachusetts, Amherst, US; 2University of Massachusetts Amherst, US Abstract Current techniques for formally verifying circuits implemented in Galois field (GF) arithmetic are limited to those with a known irreducible polynomial P (x). This paper presents a computer algebra based technique that extracts the irreducible polynomial P(x) used in the implementation of a multiplier in GF(2^m). The method is based on first extracting a unique polynomial in Galois field of each output bit independently. P(x) is then obtained by analyzing the algebraic expression in GF(2^m) of each output bit. We demonstrate that this method is able to reverse engineer the irreducible polynomial of an n-bit GF multiplier in n threads. Experiments were performed on Mastrovito and Montgomery multipliers with different P(x), including NIST-recommended polynomials and optimal polynomials for different microprocessor architectures. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 15:00 | 11.7.3 | FORMAL SPECIFICATION AND DEPENDABILITY ANALYSIS OF OPTICAL COMMUNICATION NETWORKS Speaker: Khaza Anuarul Hoque, University of Oxford, GB Authors: Umair Siddique1, Khaza Anuarul Hoque2 and Taylor T Johnson3 1McMaster University, CA; 2University of Oxford, GB; 3University of Texas at Arlington, US Abstract Network dependability reflects the ability to deliver continuous services even after failures, such as man-made or natural disturbances, e.g., storms, hurricanes, and floods, etc. In the last decade, optical networks have been increasingly deployed to provide multicast traffic in metropolitan areas. In this paper, we provide a formal specification of double-rings with dual attachments (DRDA) topologies of optical networks using Continuous-Time Markov Chains. Our formal modeling includes the concept of pre-configured protection cycles (p-cycles), which provide effective fault tolerance against link-failures in optical networks. Our approach is generic enough to handle networks of any size that are prone to any combinations of link failures. We formally specify several dependability properties using Continuous Stochastic Logic (CSL). We then provide a quantitative evaluation of these properties using the PRISM model checker. We observe that such formal analysis can provide critical information at early design stages to network operators for designing highly-dependable optical networks in metropolitan areas (e.g., availability on the order of 99.99% or 99.999%). Download Paper (PDF; Only available from the DATE venue WiFi) |
| 15:30 | End of session Coffee Break in Exhibition Area On all conference days (Tuesday to Thursday), coffee and tea will be served during the coffee breaks at the below-mentioned times in the exhibition area. Tuesday, March 28, 2017
Wednesday, March 29, 2017
Thursday, March 30, 2017
|