March 2-5, 2020

DoubleTree Hotel, San Jose, CA

MP Associates, Inc.
TUESDAY March 03, 9:00am - 10:30am | Oak
Formal Verification I
Xiaolin Chen - Synopsys, Inc.
Using formal verification and assertions to strengthen your methodology.

1.1The Importance of Complete Signoff Methodology for Formal Verification
In recent years the use of formal verification has expanded greatly in the industry due to the increased confidence and exhaustive nature of this technology. With the advancement of formal verification, however, comes the need for methodologies to quantify and measure the quality of formal. In this paper, we present a case study of a sub-block to an advanced microprocessor verified with formal and show how the correct methodology can catch otherwise missed RTL bugs. The entire sign-off flow and details of issues found are included.
 Speaker: Iain T. Singleton - Synopsys, Inc.
 Authors: Mahesh Parmar - Synopsys India Pvt. Ltd. & Synopsys, Inc.
Iain T. Singleton - Synopsys, Inc.
Geogy Jacob - Synopsys, Inc.
1.2Formal Verification of Macro-Op Cache Including Coherence Verification, for Cortex A77 and its Successor CPU
For Cortex A77 ARM CPU and its successor core, formal verification was strategically introduced to verify a new design feature, "macro-op cache". In this paper, we describe how formal was applied effectively to find bugs in both bring up phase and late in the project. The paper talks about methods to reduce complexity for formal, along with effective ways to write checkers and constraints to make them more efficient for formal verification. Data on bugs is also presented, along with some details. Finally, collaboration with design and simulation testbench teams that enabled this work is also presented.
 Speaker: Vaibhav Agrawal - Arm, Ltd.
 Author: Vaibhav Agrawal - Arm, Ltd.
1.3Finding the Last Bug in a CNN DMA Unit
Functional formal sign-off of design blocks provides the benefit of finding all bugs, no matter how resistant they are to discovery through traditional methods. The Direct Memory Access unit of a Convolutional Neural Network is a design that has very long memory volume transport latencies, which is a characteristic that would conventionally cause it to be considered incompatible with formal verification. However, we present a methodology that enables the successful application of formal sign-off to such designs. We will show how we were able to find extreme corner case bugs and have confidence that we had found the last bug.
 Speaker: Roger Sabbagh - Oski Technology, Inc.
 Authors: Bruno Lavigueur - Synopsys, Inc.
Dean Ke - Synopsys, Inc.
Eric Rao - Synopsys, Inc.
Fergus Casey - Synopsys, Inc.
Achin Mittal - Oski Technology, Inc.
Pallavi Kumari - Oski Technology, Inc.
Michael Thompson - Oski Technology, Inc.
Roger Sabbagh - Oski Technology, Inc.