检索结果-内蒙古大学图书馆

BDD based procedures for a theory of equality with uninterpreted functions

FORMAL METHODS IN SYSTEM DESIGN 2003年第3期22卷 205-224页

作者： Goel, A Sajid, K Univ Texas Dept ECE Austin TX 78712 USA Northwestern Univ Dept ECE Evanston IL 60208 USA Intel Corp Santa Clara CA 95051 USA Tempus Fugit Inc Albany CA USA

The logic of equality with uninterpreted functions has been proposed for verifying abstract hardware designs. The ability to perform fast satisfiability checking over this logic is imperative for such verification paradigms to be successful. We present symbolic methods for satisfiability checking for this logic. The first procedure is based on restricting analysis to finite instantiations of the variables. The second procedure directly reasons about equality by introducing Boolean-valued indicator variables for equality. Theoretical and experimental evidence shows the superiority of the second approach.

关键词： uninterpreted functions logic of equality BDDs

来源：评论

学校读者我要写书评

暂无评论

Processor Verification Using Efficient Reductions of the Logic of uninterpreted functions to Propositional Logic

引用

ACM Transactions on Computational Logic 2001年第1期2卷 93-134页

作者： Bryant, Randal E. German, Steven Velev, Miroslav N. Computer Science Department Carnegie Mellon University Pittsburgh PA 15213 United States IBM Watson Research Center NY P.O. Box 218 Yorktown Heights 10598 United States Electrical Engineering Department Carnegie Mellon University Pittsburgh PA 15213 United States

The logic of Equality with uninterpreted functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic. By reducing formulas in this logic to propositional formulas, we can apply Boolean methods such as ordered Binary Decision Diagrams (BDDs) and Boolean satisfiability checkers to perform the verification. We can exploit characteristics of the formulas describing the verification conditions to greatly simplify the propositional formulas generated. We identify a class of terms we call “p-terms” for which equality comparisons can only be used in monotonically positive formulas. By applying suitable abstractions to the hardware model, we can express the functionality of data values and instruction addresses flowing through an instruction pipeline with p-terms. A decision procedure can exploit the restricted uses of p-terms by considering only “maximally diverse” interpretations of the associated function symbols, where every function application yields a different value except when constrained by functional *** present two methods to translate formulas in EUF into propositional logic. The first interprets the formula over a domain of fixed-length bit vectors and uses vectors of propositional variables to encode domain variables. The second generates formulas encoding the conditions under which pairs of terms have equal valuations, introducing propositional variables to encode the equality relations between pairs of terms. Both of these approaches can exploit maximal diversity to greatly reduce the number of propositional variables that need to be introduced and to reduce the overall formula *** present experimental results demonstrating the efficiency of this approach when verifying pipelined processors using the method proposed by Burch and Dill. Exploiting positive equality allows us to overcome the exponential blow-up experienced previously when verifying microprocessors wi

关键词： Algorithms Decision procedures Processor verification uninterpreted functions Verification

来源：评论

学校读者我要写书评

暂无评论

NuMDG:A New Tool for Multiway Decision Graphs Construction

引用

Journal of Computer Science & Technology 2011年第1期26卷 139-152页

作者： Sa'ed Abed Yassine Mokhtari Otmane Ait-Mohamed Sofiene Tahar Department of Computer Engineering Hashemite UniversityZarqaJordan Department of Electrical and Computer Engineering Concordia UniversityMontrealCanada

Multiway Decision Graphs （MDGs） are a canonical representation of a subset of many-sorted first-order logic. This subset generalizes the logic of equality with abstract types and uninterpreted function symbols. The distinction between abstract and concrete sorts mirrors the hardware distinction between data path and control. Here we consider ways to improve MDGs construction. Efficiency is achieved through the use of the Generalized-If-Then-Else （GITE） commonly operator in Binary Decision Diagram packages. Consequently, we review the main algorithms used for MDGs verification techniques. In particular, Relational Product and Pruning by Subsumption are algorithms defined uniformly through this single CITE operator which will lead to a more efficient implementation. Moreover, we provide their correctness proof. This work can be viewed as a way to accommodate the ROBBD algorithms to the realm of abstract sorts and uninterpreted functions. The new tool, called NuMDG, accepts an extended SMV language, supporting abstract data sorts. Finally, we present experimental results demonstrating the efficiency of the NuMDG tool and evaluating its performance using a set of benchmarks from the SMV package.

关键词： infinite state model checking multiway decision graphs uninterpreted functions

来源：评论

学校读者我要写书评

暂无评论

A methodology for hardware verification using compositional model checking

引用

SCIENCE OF COMPUTER PROGRAMMING 2000年第1-3期37卷 279-309页

作者： McMillan, KL 2001 Addison St. Berkeley CA 94704-1103 USA

A methodology for system-level hardware verification based on compositional model checking is described. This methodology relies on a simple set of proof techniques, and a domain specific strategy for applying them. The goal of this strategy is to reduce the verification of a large system to finite state subgoals that are tractable in both size and number. These subgoals are then discharged by model checking. The proof strategy uses proof techniques for design refinement, temporal case splitting, data-type reduction and the exploitation of symmetry. uninterpreted functions can be used to abstract operations on data. A proof system supporting this approach generates verification subgoals to be discharged by the SMV symbolic model checker. Application of the methodology is illustrated using an implementation of Tomasulo's algorithm, a packet buffering device and a cache coherence protocol as examples. (C) 2000 Published by Elsevier Science B.V. All rights reserved.

关键词： hardware verification design refinement compositional model checking symbolic model checking data type reduction symmetry uninterpreted functions SMV Tomasulo's algorithm cache coherence protocol

来源：评论

学校读者我要写书评

暂无评论

A polynomial-time algorithm for global value numbering

引用

SCIENCE OF COMPUTER PROGRAMMING 2007年第1期64卷 97-114页

作者： Gulwani, Sumit Necula, George C. Microsoft Corp Redmond WA 98052 USA Univ Calif Berkeley Dept Comp Sci Berkeley CA 94720 USA

We describe a polynomial-time algorithm for global value numbering, which is the problem of discovering equivalences among program sub-expressions. We treat all conditionals as non-deterministic and all program operators as uninterpreted. We show that there are programs for which the set of all equivalences contains terms whose value graph representation requires exponential size. Our algorithm discovers all equivalences among terms of size at most s in time that grows linearly with s. For global value numbering, it suffices to choose s to be the size of the program. Earlier deterministic algorithms for the same problem are either incomplete or take exponential time. We provide a detailed analytical comparison of some of these algorithms. (c) 2006 Elsevier B.V. All rights reserved.

关键词： global value numbering uninterpreted functions abstract interpretation Herbrand equivalence

来源：评论

学校读者我要写书评

暂无评论

Polyhedral Specification and Code Generation of Sparse Tensor Contraction with Co-iteration

引用

ACM TRANSACTIONS ON ARCHITECTURE AND CODE OPTIMIZATION 2022年第1期20卷 1-26页

作者： Zhao, Tuowen Popoola, Tobi Hall, Mary Olschanowsky, Catherine Strout, Michelle Univ Utah Salt Lake City UT 84112 USA Boise State Univ Boise ID 83725 USA Univ Arizona Tucson AZ USA Sch Comp 50 S Cent Campus Dr Salt Lake City UT 84112 USA Comp Sci Dept 777 W Main St 364 Boise ID 83702 USA Dept Comp Sci POB 210077 Tucson AZ 85721 USA

This article presents a code generator for sparse tensor contraction computations. It leverages a mathematical representation of loop nest computations in the sparse polyhedral framework (SPF), which extends the polyhedral model to support non-affine computations, such as those that arise in sparse tensors. SPF is extended to perform layout specification, optimization, and code generation of sparse tensor code: (1) We develop a polyhedral layout specification that decouples iteration spaces for layout and computation;and (2) we develop efficient co-iteration of sparse tensors by combining polyhedra scanning over the layout of one sparse tensor with the synthesis of code to find corresponding elements in other tensors through an SMT solver. We compare the generated code with that produced by a state-of-the-art tensor compiler, TACO. We achieve on average 1.63x faster parallel performance than TACO on sparse-sparse co-iteration and describe how to improve that to 2.72x average speedup by switching the find algorithms. We also demonstrate that decoupling iteration spaces of layout and computation enables additional layout and computation combinations to be supported.

关键词： Data layout sparse tensor contraction polyhedral compilation code synthesis uninterpreted functions index array properties

来源：评论

学校读者我要写书评

暂无评论

The small model property: How small can it be?

引用

INFORMATION AND COMPUTATION 2002年第1期178卷 279-293页

作者： Pnueli, A Rodeh, Y Strichman, O Siegel, M Weizmann Inst Sci Dept Appl Math & Comp Sci IL-76100 Rehovot Israel

Efficient decision procedures for equality logic (quantifier-free predicate calculus+the equality sign) are of major importance when proving logical equivalence between systems. We introduce an efficient decision procedure for the theory of equality based on finite instantiations. The main idea is to analyze the structure of the formula and compute accordingly a small domain to each variable such that the formula is satisfiable iff it can be satisfied over these domains. We show how the problem of finding these small domains can be reduced to an interesting graph theoretic problem. This method enabled us to verify formulas containing hundreds of integer and floating point variables that could not be efficiently handled with previously known techniques. (C) 2002 Elsevier Science (USA).

关键词： finite instantiation equality logic uninterpreted functions compiler verification translation validation range allocation

来源：评论

学校读者我要写书评

暂无评论

Global value numbering using random interpretation 04

Global value numbering using random interpretation

引用

31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

作者： Gulwani, S Necula, GC Univ Calif Berkeley Dept Elect Engn & Comp Sci Berkeley CA 94720 USA

ISBN: (纸本)9781581137293

We present a polynomial time randomized algorithm for global value numbering. Our algorithm is complete when conditionals are treated as non-deterministic and all operators are treated as uninterpreted functions. We are not aware of any complete polynomial-time deterministic algorithm for the same problem. The algorithm does not require symbolic manipulations and hence is simpler to implement than the deterministic symbolic algorithms. The price for these benefits is that there is a probability that the algorithm can report a false equality. We prove that this probability can be made arbitrarily small by controlling various parameters of the algorithm. Our algorithm is based on the idea of random interpretation, which relies on executing a program on a number of random inputs and discovering relationships from the computed values. The computations are done by giving random linear interpretations to the operators in the program. Both branches of a conditional are executed. At join points, the program states are combined using a random affine combination. We discuss ways in which this algorithm can be made more precise by using more accurate interpretations for the linear arithmetic operators and other language constructs.

关键词： global value numbering Herbrand equivalences random interpretation randomized algorithm uninterpreted functions

来源：评论

学校读者我要写书评

暂无评论

Code Synthesis for Sparse Tensor Format Conversion and Optimization 2023

Code Synthesis for Sparse Tensor Format Conversion and Optim...

引用

21st ACM/IEEE International Symposium on Code Generation and Optimization (CGO)

作者： Popoola, Tobi Zhao, Tuowen St George, Aaron Bhetwal, Kalyan Strout, Michelle Mills Hall, Mary Olschanowsky, Catherine Boise State Univ Comp Sci Boise ID 83725 USA Univ Utah Comp Sci Salt Lake City UT 84112 USA Univ Arizona Comp Sci Tucson AZ 85721 USA Univ Utah Sch Comp Salt Lake City UT 84112 USA

ISBN: (纸本)9798400701016

Many scientific applications compute using sparse data and store that data in a variety of sparse formats because each format has unique space and performance benefits. Optimizing applications that use sparse data involves translating the sparse data into the chosen format and transforming the computation to iterate over that format. This paper presents a formal definition of sparse tensor formats and an automated approach to synthesize the transformation between formats. This approach is unique in that it supports ordering constraints not supported by other approaches and synthesizes the transformation code in a high-level intermediate representation suitable for applying composable transformations such as loop fusion and temporary storage reduction. We demonstrate that the synthesized code for COO to CSR with optimizations is 2.85x faster than TACO, Intel MKL, and SPARSKIT while the more complex COO to DIA is 1.4x slower than TACO but faster than SPARSKIT and Intel MKL using the geometric average of execution time.

关键词： Sparse Format Conversion Sparser Format Descriptors Polyhedral compilation Code synthesis uninterpreted functions Index array properties Transformations

来源：评论

学校读者我要写书评

暂无评论

Precise interprocedural analysis using random interpretation

Precise interprocedural analysis using random interpretation

引用

32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

作者： Gulwani, S Necula, GC Univ Calif Berkeley Dept Elect Engn & Comp Sci Berkeley CA 94720 USA

We describe a unified framework for random interpretation that generalizes previous randomized intraprocedural analyses, and also extends naturally to efficient interprocedural analyses. There is no such natural extension known for deterministic algorithms. We present a general technique for extending any intraprocedural random interpreter to perform a context-sensitive interprocedural analysis with only polynomial increase in running time. This technique involves computing random summaries of procedures, which are complete and probabilistically sound. As an instantiation of this general technique, we obtain the first polynomial-time randomized algorithm that discovers all linear relationships interprocedurally in a linear program. We also obtain the first polynomial-time randomized algorithm for precise interprocedural value numbering over a program with unary uninterpreted functions. We present experimental evidence that quantifies the precision and relative speed of the analysis for discovering linear relationships along two dimensions: intraprocedural vs. interprocedural, and deterministic vs. randomized. We also present results that show the variation of the error probability in the randomized analysis with changes in algorithm parameters. These results suggest that the error probability is much lower than the existing conservative theoretical bounds.

关键词： algorithms theory verification interprocedural analysis random interpretation randomized algorithm linear relationships uninterpreted functions interprocedural value numbering

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：