Advertisement
Published in:
2007 | OriginalPaper | Chapter
Verification of Data Paths Using Unbounded Integers: Automata Strike Back
Authors : Tobias Schuele, Klaus Schneider
Published in: Hardware and Software, Verification and Testing
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We present a decision procedure for quantifier-free Presburger arithmetic that is based on a polynomial time translation of Presburger formulas to alternating finite automata (AFAs). Moreover, our approach leverages the advances in SAT solving by reducing the emptiness problem of AFAs to satisfiability problems of propositional logic. In order to obtain a complete decision procedure, we use an inductive style of reasoning as originally proposed for proving safety properties in bounded model checking. Besides linear arithmetic constraints, our decision procedure can deal with bitvector operations that frequently occur in hardware design. Thus, it is well-suited for the verification of data paths at a high level of abstraction.