Word-level Symbolic Trajectory Evaluation

TL;DR

This paper introduces STEWord, the first practical word-level symbolic trajectory evaluation engine, which automatically derives abstract lattices from RTL descriptions to improve scalability over existing bit-level STE methods.

Contribution

It demonstrates how to automatically generate abstract lattices from RTL descriptions and implements a practical word-level STE model checker, enhancing scalability.

Findings

STEWord scales better than bit-level STE and word-level BMC.

It automatically derives abstract lattices from RTL descriptions.

Experiments show improved scalability on industrial-like designs.

Abstract

Symbolic trajectory evaluation (STE) is a model checking technique that has been successfully used to verify industrial designs. Existing implementations of STE, however, reason at the level of bits, allowing signals to take values in {0, 1, X}. This limits the amount of abstraction that can be achieved, and presents inherent limitations to scaling. The main contribution of this paper is to show how much more abstract lattices can be derived automatically from RTL descriptions, and how a model checker for the general theory of STE instantiated with such abstract lattices can be implemented in practice. This gives us the first practical word-level STE engine, called STEWord. Experiments on a set of designs similar to those used in industry show that STEWord scales better than word-level BMC and also bit-level STE.