Bit-precise reasoning with affine functions
Bit-precise reasoning with affine functions
复制标题
使用仿射函数进行位精确推理
DOI：
10.1145/1512464.1512474
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Kettle N
中科院分区：
文献类型：
--
作者：
Kettle N
仿射布尔函数类足够丰富，可以表达常数位以及不同字的不同位之间的依赖关系。例如，函数 (x0) ∧ (Øy1) ∧ (x4⇔y7) ∧ (x5⇔ Øy9) 是仿射的，表示变量 x 的低位（位 0）为真，y 的位 1 为假，xandy 的位 4 和 7 一致，而 xandy 的位 5 和 9 不同的不变式。此类布尔函数适合位精确推理，因为它满足强链属性，这些属性限制了在推理循环时需要重新应用语义不动点方程系统的次数。本文解决了当函数表示为 ROBDD 时，将任意布尔函数抽象为一般仿射函数或宽度为 2 的仿射函数的关键问题。为此任务提出了新颖的算法：一种是操纵布尔向量的算法，另一种是受反统一启发的算法。在基准电路上比较两种算法的速度和精度，得出仿射抽象的易处理性结论。
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 (x0) ∧ (¬y1) ∧ (x4⇔y7) ∧ (x5⇔ ¬y9) is affine and expresses the invariant that the low bit (bit 0) of the variablexis true, that bit 1 ofyis false, that the bits 4 and 7 ofxandycoincide whereas bits 5 and 9 ofxandydiffer. 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.
登录
查看更多内容
PRISC：可编程精简指令集计算机
DOI：
--
发表时间：
1994
期刊：
影响因子：
--
作者：
R. Razdan
通讯作者：
R. Razdan
DOI：
--
发表时间：
2002
期刊：
European Conference on Artificial Intelligence
影响因子：
--
作者：
B. Zanuttini
通讯作者：
B. Zanuttini
用于多媒体 PC 的英特尔 MMX
影响因子：
22.7
作者：
A. Peleg;Sam Wilkie;U. Weiser
通讯作者：
U. Weiser
用素蕴涵拓宽 ROBDD
DOI：
--
发表时间：
2006
期刊：
International Conference on Tools and Algorithms for Construction and Analysis of Systems
影响因子：
--
作者：
N. Kettle;A. King;Tadeusz Strzemecki
通讯作者：
Tadeusz Strzemecki
DOI：
--
发表时间：
2000
期刊：
European Conference on Parallel Processing
影响因子：
--
作者：
M. Budiu;M. Sakr;Kip Walker;S. Goldstein
通讯作者：
S. Goldstein