© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Bit-Precise Reasoning with Affine Functions
Neil Kettle and Andy King
Electronic Notes in Theoretical Computer Science, pages 182-196, July 2008 Revised, Selected papers from the Bit-Precise Reasoning (BPR'08) workshop in Princetown.Abstract
The class of affine Boolean functions is rich enough to express constant bits and dependencies between different bits of different words. For example, the function $(x_0)\wedge(\neg y_1)\wedge(x_4\iff y_7)\wedge(x_5\iff\neg y_9)$ is affine and expresses the invariant that the low bit (bit $0$) of the variable (unknown variable x)$ is true, that bit $1$ of (unknown variable y)$ is false, that the bits $4$ and $7$ of (unknown variable x)$ and (unknown variable y)$ coincide whereas bits $5$ and $9$ of (unknown variable x)$ and (unknown variable y)$ differ. This class of Boolean function is amenable to bit-precise reasoning since it satisfies strong chain properties which bound the number of times a system of semantic fixpoint equations need to be reapplied when reasoning about loops. This paper address the key problem of abstracting an arbitrary Boolean function to either a general affine function or a so-called affine function of width 2, when the function is represented as an ROBDD. Novel algorithms are presented for this task: one that manipulates Boolean vectors and another which is inspired by anti-unification. The speed and precision of both algorithms are compared on benchmark circuits, to draw conclusions on the tractability of affine abstraction.
Download publication 193 kbytes (PDF)Bibtex Record
@article{2776,
author = {Neil Kettle and Andy King},
title = {Bit-{P}recise {R}easoning with {A}ffine {F}unctions},
month = {July},
year = {2008},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Revised, Selected papers from the Bit-Precise Reasoning (BPR'08) workshop in Princetown.},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2008/2776},
publication_type = {article},
submission_id = {4099_1212653065},
ISSN = {1571-0661},
journal = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
}