Fast Three-Valued Abstract Bit-Vector Arithmetic
Fast Three-Valued Abstract Bit-Vector Arithmetic
复制标题
快速三值抽象位向量算法
DOI：
10.1007/978-3-030-94583-1_12
复制
发表时间：
2022
期刊：
影响因子：
5.6
通讯作者：
Stefan Ratschan
中科院分区：
文献类型：
--
作者：
Jan Onderka;Stefan Ratschan
抽象是形式化验证中减少状态数的重要方法之一。一个重要的抽象技术是使用三值逻辑，可扩展到位向量。可以快速计算出运动和逻辑运算的最佳抽象位向量结果。然而，对于广泛使用的算术运算，有效的算法计算的最佳可能的输出还没有到现在为止，在本文中，我们提出了新的有效的多项式时间算法的抽象加法和乘法与三值位向量的输入。这些算法产生最好的可能的三值位向量的输出，并保持快速，即使与32位inputs.To获得的算法，我们设计了一种新的模块极值通过使用伪布尔模不等式的问题的重新制定的技术。使用所介绍的技术，我们构造了一个算法的抽象加法，计算其结果在线性时间，以及最坏情况下的二次时间算法的抽象乘法。最后，我们通过实验评估了算法的性能，证实了它们的实际效率。
Abstraction is one of the most important approaches for reducing the number of states in formal verification. An important abstraction technique is the usage of three-valued logic, extensible to bit-vectors. The best abstract bit-vector results for movement and logical operations can be computed quickly. However, for widely-used arithmetic operations, efficient algorithms for computation of the best possible output have not been known up to now.In this paper, we present new efficient polynomial-time algorithms for abstract addition and multiplication with three-valued bit-vector inputs. These algorithms produce the best possible three-valued bit-vector output and remain fast even with 32-bit inputs.To obtain the algorithms, we devise a novel modular extreme-finding technique via reformulation of the problem using pseudo-Boolean modular inequalities. Using the introduced technique, we construct an algorithm for abstract addition that computes its result in linear time, as well as a worst-case quadratic-time algorithm for abstract multiplication. Finally, we experimentally evaluate the performance of the algorithms, confirming their practical efficiency.