Kettle, N. and King, A.M.
(2008)
Bit-Precise Reasoning with Affine Functions.
Electronic Notes in Theoretical Computer Science
.
ISSN 1571-0661.
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 <span class='mathrm'>(x<sub>0</sub>)∧(neg y<sub>1</sub>)∧(x<sub>4</sub>ıff y<sub>7</sub>)∧(x<sub>5</sub>ıffneg y<sub>9</sub>)</span> is affine and expresses the invariant that the low bit (bit <span class='mathrm'>0</span>) of the variable <span class='mathrm'>x</span> is true, that bit <span class='mathrm'>1</span> of <span class='mathrm'>y</span> is false, that the bits <span class='mathrm'>4</span> and <span class='mathrm'>7</span> of <span class='mathrm'>x</span> and <span class='mathrm'>y</span> coincide whereas bits <span class='mathrm'>5</span> and <span class='mathrm'>9</span> of <span class='mathrm'>x</span> and <span class='mathrm'>y</span> 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.
- Depositors only (login required):
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_pdf.png)
