Automatic verification of safety and liveness for XScale-like processor models using WEB refinements
Automatic verification of safety and liveness for XScale-like processor models using WEB refinements
复制标题
使用 WEB 改进自动验证类似 XScale 的处理器模型的安全性和活性
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
S. Srinivasan
中科院分区：
文献类型：
--
作者：
P. Manolios;S. Srinivasan
我们展示了如何通过使用结构良好的等效性分配（Web）改进的概念来展示如何自动验证该复杂的类似XScale的管道式机器模型与相应的指令集体系结构模型满足相同的安全性和livess属性。自动化是通过将Web进行证明义务减少到具有Lambda表达式和未解释功能（CLU）的逻辑中的公式中实现的。我们使用UCLID工具将所得的CLU公式转换为布尔公式，然后将其与SAT求解器进行检查。我们验证的模型包括诸如OUT OUT OUT OUT OUT OUTION完成，精确异常，分支预测和中断之类的功能。我们使用两种类型的改进图。在一个中，冲洗用于将管道的机器状态映射到指令集架构状态；另一方面，我们使用承诺方法，这是冲洗双重的，因为部分完成的说明是无效的。我们为所有建模的机器提供了实验结果，包括验证时间。对于我们的申请，我们发现花费的时间证明了易感的时间约占整个验证时间的5％。
We show how to automatically verify that complex XScale-like pipelined machine models satisfy the same safety and liveness properties as their corresponding instruction set architecture models, by using the notion of well-founded equivalence bisimulation (WEB) refinement. Automation is achieved by reducing the WEB-refinement proof obligation to a formula in the logic of counter arithmetic with lambda expressions and uninterpreted functions (CLU). We use the tool UCLID to transform the resulting CLU formula into a Boolean formula, which is then checked with a SAT solver. The models we verify include features such as out of order completion, precise exceptions, branch prediction, and interrupts. We use two types of refinement maps. In one, flushing is used to map pipelined machine states to instruction set architecture states; in the other, we use the commitment approach, which is the dual of flushing, since partially completed instructions are invalidated. We present experimental results for all the machines modelled, including verification times. For our application, we found that the time spent proving liveness accounts for about 5% of the over-all verification time.