Verification using uninterpreted functions and finite instantiations
Verification using uninterpreted functions and finite instantiations
复制标题
DOI：
10.1007/bfb0031810
复制
发表时间：
1996-01-01
期刊：
影响因子：
--
通讯作者：
Brayton, RK
中科院分区：
文献类型：
--
作者：
Hojati, R;Isles, A;Brayton, RK
在具有宽数据路径的微处理器验证中，解决状态爆炸问题的一种方法是将变量建模为整数，将数据路径函数建模为未解释的变量。然后，验证要么以符号方式模拟这个抽象模型，要么创建一个包含所有可能行为的小的有限实例化。在这篇文章中，我们首先证明了模型的可达性问题是不可判定的，其中x和y都是整数变量。然而，这样的谓词通常只在被检查的属性中需要，而不是在模型中。对于包含x=Term和n=y形式的谓词的性质，我们分别使用有限实例化提供了完全和部分验证技术。给出了这些结果在超标量微处理器控制电路验证中的应用，其中人们可以使用具有一个或几个位整数的模型来验证各种正确性性质。
One approach to address the state explosion problem in verification of microprocessors with wide datapaths is to model variables as integers and datapath functions as uninterpreted ones. Verification then proceeds by either symbolically simulating this abstract model, or creating a small finite instantiation which contains all possible behaviors. In this paper, we first prove that the reachability problem for models with uninterpreted functions and predicates only of the form x = y, where both x and y are integer variables, is undecidable. However, such predicates are generally only needed in the property being checked and not in the model. For properties involving predicates of the forms x = term and n = y, we provide complete and partial verification techniques using finite instantiations respectively. Applications of these result to the verification of the control circuitry of superscalar microprocessors are provided, where one can verify various correctness properties using models with one or a few bit integers.