Sequential equivalence checking for RTL models

 
In this paper, we examine the need for formal sequential equivalence checking across pairs of RTL models. We present scenarios that call for modifying the sequential behavior of RTL models while preserving functionality. These primarily have to do with reliably achieving aggressive timing and power goals typical of high performance design.

The advantages of verifying such sequential modifications using formal methods at the block level are identified. Some attention to front end design methodology can vastly improve the efficiency of sequential equivalence checking tools.

1 Introduction

The ability to formally determine functional equivalence between RTL models is seen as a key enabler in physically aware front-end design methodologies that are being practiced in high performance designs. In this paper, we describe sequential equivalence checking (SEC) technology and the usage of such a tool in various a practical design flows.

Commercially available equivalence checking tools today require states in the designs are tested to have one-to-one functional maps. This implies that every flop in one design must have a functionally identical flop in the partner design. As such, these tools are combinational equivalence checkers. They find maximum utility in proving that a gate level implementation of an RTL design is correct. A secondary application is that a gate level ECO can be proven not to have compromised the original functionality of RTL or gate level design.

Pixley has described the concept of sequential hardware equivalence (SHE) in [1]. We define SEC as the process of formally proving functional equivalence of designs that may in general have sequentially different implementations. Examples of sequential differences span the space from retimed pipelines (thus breaking the maps between registers, and rendering combinational equivalence checkers ineffective), differing latencies and throughputs (allowing for checking re-pipelined designs), and even scheduling and resource allocation differences.

These sequential modifications to a design are ways to robustly meet timing, area and power goals in a reliable manner. Traditionally, such modifications are frowned upon in a simulation based verification flows because of the work involved in gaining confidence in their correctness. However, sequential equivalence checking enables designers to comprehensively verify sequential design changes with trivial effort.

In the remainder of this paper, we describe some motivations for performing sequential changes to RTL designs in Section 2. Section 3 discusses some of the methodological aspects concerned with application of sequential equivalence checking to real designs. We describe technical challenges in performing sequential equivalence checking on RTL designs in section 4.

Click here to read more ...