Implicit Reachability Techniques for Presburger EFSMs

Abstract

Symbolic model checking algorithms based on BDDs grow rapidly more expensive as design sizes grow. A major contributor to the size of many designs is the datapath component of the system. In many cases the results of datapath computations influence the behavior of the controller, so an accurate datapath model is required to verify correct system function. Arithmetic datapaths can often be modelled using Presburger arithmetic, for which decision procedures exist that can be used to perform implicit state enumeration. We discuss one such decision procedure, based on automata, and its relation to the conventional BDD approach. The Presburger approach lets a single image computation give results for all possible datapath bit-widths, whereas BDD computations grow more expensive for larger bit-widths. However, Presburger models involve an infinite state space, so convergence to fixed points is not guaranteed. Experimental results demonstrate the usefulness and the limits of the Presburger approach.

This talk describes work done with Tom Shiple, Adnan Aziz, Olivier Coudert, and Rajeev Ranjan.

Transparencies

Relevant Papers