Operations of Presburger Arithmetic Using BDD-like Data Structures and Circuits Verification with them

摘要

We have proposed a formal design verification method for logic circuits and have implemented a verification support system for our method. Our verification support system divides the decision problem for design correctness of the implementation circuit into some decision problems written in Presburger arithmetic, and decides each problem with a decision procedure for Presburger arithmetic. In this paper, we propose new data structures for Presburger arithmetic, and implement the algorithms for the data operations over the proposed data structures. We describe the results of some experiments of high level design verification using our methods.