11.7 Formal Methods and Verification: Core Technologies and Applications

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 Yu¹, Daniel Holcomb¹ and Maciej Ciesielski² ¹University of Massachusetts, Amherst, US; ²University 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 Siddique¹, Khaza Anuarul Hoque² and Taylor T Johnson³ ¹McMaster University, CA; ²University of Oxford, GB; ³University 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 Coffee Break 10:30 - 11:30 Coffee Break 16:00 - 17:00 Wednesday, March 29, 2017 Coffee Break 10:00 - 11:00 Coffee Break 16:00 - 17:00 Thursday, March 30, 2017 Coffee Break 10:00 - 11:00 Coffee Break 15:30 - 16:00

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 Yu¹, Daniel Holcomb¹ and Maciej Ciesielski²
¹University of Massachusetts, Amherst, US; ²University 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 Siddique¹, Khaza Anuarul Hoque² and Taylor T Johnson³
¹McMaster University, CA; ²University of Oxford, GB; ³University 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