Case Study: Can you afford to ignore formal analysis?

Joachim Knäblein and Hans Sahm, Alcatel-Lucent
11/30/2010 10:15 PM EST

Introduction

This article is about our experience in applying formal verification techniques to an ASIC design in a large communication system.

When we, in the Alcatel-Lucent IC design group in Nürnberg, Germany, first encountered formal verification methods three years ago, our goal was to assess whether formal analysis has the potential to become an effective part of our standard functional verification flow. During our assessment, we had a lot of surprises. We found bugs in both legacy code and recent RTL code, and we learned a lot about specification gaps. Later on, we tried to leverage the complementary strengths of simulation-based verification and formal analysis, but discovered that this is more difficult than we expected. In this article, we share our experiences and best practices.

Formal verification techniques have been in industrial use for more than a decade now, but were considered as "emerging" methods for most of that time. They were viewed as an approach requiring high levels of expertise, and with limited applicability to industrial designs. This was the estimation of many IC design departments and also of the design team at Alcatel-Lucent in Nürnberg until 2007. This view significantly changed with our participation in the HERKULES project [1], supported by the German government.

Over the past three years, this project teamed chip-design engineers at leading system providers and research institutes with developers of commercial formal verification tools. Our goal was to develop a right-first-time formal verification approach for digital and mixed-signal designs – and to ensure that it is widely applicable to the development of automotive and telecommunication IP, which must comply with very high quality standards. Alcatel-Lucent participated as an application partner, using newly developed techniques and methodologies in normal design work, and cooperating very closely with the tool developers in order to evaluate and improve usability and concepts.

This article is structured as follows. First, we give a brief description of the ASIC’s functionality. In the next section, we talk about the design aspects that we tackled with formal verification. Then, we compare simulation and formal verification with respect to effort, capabilities and required skills based on the experience from the application project. And finally, we describe how simulation-based and formal verification methods can be brought together in a combined verification flow using SystemVerilog Assertions (SVA) [3].

Click here to read more ...