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

Efficient debugging in a formal verification environment

International Journal on Software Tools for technology Transfer 2003年第3期4卷 335-348页

作者： Copty, Fady Irron, Amitai Weissberg, Osnat Kropp, Nathan Kamhi, Gila Logic and Validation Technology Intel Corporation Haifa Israel Microprocessor Group Intel Corporation United States

In this paper, we emphasize the importance of efficient debugging in formal verification and present capabilities that we have developed in order to aid debugging in Intel's Formal Verification Environment. We have given the name "Counter-Example Wizard" to the bundle of capabilities that we have developed to address the needs of the verification engineer in the context of counter-example diagnosis and rectification. The novel features of the Counter-Example Wizard are the multi-value counter-example annotation, constraint-based debugging, and multiple counter-example generation mechanisms. Our experience with the verification of real-life Intel designs shows that these capabilities complement one another and can help the verification engineer diagnose and fix a reported failure. We use real-life verification cases to illustrate how our system solution can significantly reduce the time spent in the loop of model checking, specification, and design modification. © 2003 Springer-Verlag.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

SAT-based methods for sequential hardware equivalence verification without synchronization

SAT-based methods for sequential hardware equivalence verifi...

引用

BMC'2003, First International Workshop on Bounded Model Checking

作者： Khasidashvili, Zurab Hanna, Ziyad Logic and Validation Technology Design Technology Division Intel Development Center Haifa Israel

The BDD- and SAT-based model checking and verification methods normally require an initial state. Here we are concerned with sequential hardware verification, where an initial state must be one of the reset states. In practice, a reset state is not always given by the designer, and computing a reset state of a circuit is a hard problem. In this paper we propose a method allowing usage of SAT-based verification methods without a need for a user-given or a computed initial state. The idea is to employ a binary encoding of 3-valued modeling of circuits, and use the undefined state X as a reset state. © 2003 Published by Elsevier Science B.V.

关键词： Synchronization

来源：评论

学校读者我要写书评

暂无评论

Evaluating semi-exhaustive verification techniques for bug hunting

Evaluating semi-exhaustive verification techniques for bug h...

引用

SMC'99, First International Workshop on Symbolic Model Checking (Associated to FLoC'99, the 1999 Federated logic Conference)

作者： Fraer, Ranan Kamhi, Gila Fix, Limor Vardi, Moshe Y. Logic and Validation Technology Intel Corp. Haifa Israel Dept of Computer Science Rice University

We propose a methodology to evaluate a rich set of BDD subsetting heuristics with respect to bug hunting and apply it to a set of real-life Intel designs. Our results illustrate that the evaluation metrics used to rate these heuristics in previous work were not tuned for bug-finding efficiency, which we believe is the major criterion that the heuristics need to meet. ©1999 Published by Elesevier Science B. V.

关键词： Program debugging

来源：评论

学校读者我要写书评

暂无评论

Pattern search in hierarchical high-level designs

Pattern search in hierarchical high-level designs

引用

11th IEEE International Conference on Electronics, Circuits and Systems, ICECS 2004

作者： Terem, Zvi Kamhi, Gila Vardi, Moshe Y. Irron, Amitai Logic Validation Technology Intel Corp. Haifa Israel Rice Universiy Houston United States

ISBN: (纸本)0780387155

The main focus of this paper is on using algorithms for design pattern matching to address the challenges of designs at RT and higher abstraction levels. The crux of our approach is modeling designs and patterns as graphs, which lets us express design pattern matching as subgraph isomorphism. We apply a constraint-satisfaction approach and address the problem of both exact and generalized matching. Our experimental results confirm the applicability of our approach on industrial test cases. © 2004 IEEE.

关键词： Pattern recognition

来源：评论

学校读者我要写书评

暂无评论

Efficient debugging in a formal verification environment 11th

引用

11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2001 held jointly with the 14th International Conference on Theorem Proving in Higher Order logics, TPHOLs 2009

作者： Copty, Fady Irron, Amitai Weissberg, Osnat Kropp, Nathan Kamhi, Gila Logic and Validation Technology Intel Corporation Haifa Israel Microprocessor Group Intel Corporation United States

ISBN: (纸本)3540425411

In this paper, we emphasize the importance of efficient debugging in formal verification and present capabilities that we have developed in order to augment debugging in Intel’s Formal Verification Environment. We have given the name the "counter-example wizard" to the bundle of capabilities that we have developed to address the needs of the verification engineer in context of counter-example diagnosis and rectification. The novel features of the counterexample wizard are the "multi-value counter-example annotation," "multiple root cause detection," and "constraint-based debugging" mechanisms. Our experience with the verification of real-life Intel designs shows that these capabilities complement one another and can considerably help the verification engineer diagnose and fix a reported failure. We use real-life verification cases to illustrate how our system solution can significantly reduce the time spent in the loop of model checking, specification and design modification. © Springer-Verlag Berlin Heidelberg 2001.

关键词： Formal verification

来源：评论

学校读者我要写书评

暂无评论

Prioritized traversal: Efficient reachability analysis for verification and falsification 12th

Prioritized traversal: Efficient reachability analysis for v...

引用

12th International Conference on Computer Aided Verification, CAV 2000

作者： Fraer, Ranan Kamhi, Gila Ziv, Barukh Vardi, Moshe Y. Fix, Limor Logic and Validation Technology Intel Corporation Haifa Israel Dept. of Computer Science Rice University United States

ISBN: (纸本)3540677704

Our experience with semi-exhaustive verification shows a severe degradation in usability for the corner-case bugs, where the tuning effort becomes much higher and recovery from dead-ends is more and more difficult. Moreover, when there are no bugs at all, shifting semi-exhaustive traversal to exhaustive traversal is very expensive, if not impossible. This makes the output of semi-exhaustive verification on non-buggy designs very ambiguous. Furthermore, since after the design fixes each falsification task needs to converge to full verification, there is a strong need for an algorithm that can handle efficiently both verification and falsification. We address these shortcomings with an enhanced reachability algorithm that is more robust in detecting corner-case bugs and that can potentially converge to exhaustive reachability. Our approach is similar to that of Cabodi et al. in partitioning the frontiers during the traversal, but differs in two respects. First, our partitioning algorithm trades quality for time resulting in a significantly faster traversal. Second, the subfrontiers are processed according to some priority function resulting in a mixed BFS/DFS traversal. It is this last feature that makes our algorithm suitable for both falsification and verification. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Edge detection

来源：评论

学校读者我要写书评

暂无评论

SAT-Based Methods for Sequential Hardware Equivalence Verification without Synchronization

引用

Electronic Notes in Theoretical Computer Science 2003年第4期89卷 593-607页

作者： Zurab Khasidashvili Ziyad Hanna Logic and Validation Technology Design Technology Division Intel Development Center Haifa Israel

关键词：

来源：评论

学校读者我要写书评

暂无评论

Alignability equivalence of synchronous sequential circuits

Alignability equivalence of synchronous sequential circuits

引用

IEEE International High-Level Design validation and Test Workshop

作者： A. Rosenmann Z. Hanna Design Technology Division Logic and Validation Technology Haifa Israel

Sequential verification is a well known research framework that has attracted many researchers in the aca demic and industrial worlds during the last few decades. In this framework, initialization of synchronous models is one of the fundamental and challenging research topics that is difficult to solve, especially when talking about large industrial strengths hardware models. Many researchers in this domain such as Pomeranz and Reddy (1994), Pixley and Beihl (1991), and Pixley, Jeong and Hachtel (1994), and others tried to analyze and propose solutions to this problem, however the majority of the approaches used were based on BDDs and classical reachability analysis methods, which by nature suffer from capacity and complexity limits. When talking about hardware formal equivalence verification, the Initialization issue becomes even more complex especially when trying to verify the logic equivalence of two large industrial circuits. In this note we propose a new adaptive and iterative approach that combines various symbolic simulation techniques and bounded model checking algorithms to initialize sequential circuits for the alignability equivalence verification. The novelty of our method has been employed on complex real life sequential models from Intel lead Pentium processor designs. These methods are already implemented in Intel's sequential verification engine, Insight.

关键词： Sequential circuits Hardware Data structures Boolean functions Reachability analysis logic circuits Iterative methods Circuit simulation Iterative algorithms Process design

来源：评论

学校读者我要写书评

暂无评论

An abstract concept of optimal implementation

An abstract concept of optimal implementation

引用

WRS 2003, 3rd International Workshop on Reduction Strategies in Rewriting and Programming - Final Proceedings

作者： Khasidashvili, Zurab Glauert, John Logic and Validation Technology Intel IDC Haifa Israel School of Computing Sciences UEA Norwich NR4 7TJ United Kingdom

In previous works, we introduced Stable Deterministic Residual Structures (SDRSs), Abstract Reduction Systems with an axiomatized residual relation which model orthogonal term and graph rewriting systems, and Deterministic Family Structures (DFSs), which add an axiomatized notion of redex-family to capture known sharing concepts in the lambda-calculus and other orthogonal rewrite systems. In this paper, we introduce and study a concept of implementation of DFSs. We show that for any DFS F, its implementation FI is a non-duplicating DFSs with zig-zag as the family relation, where zig-zag is simply the symmetric and transitive closure of the residual relation on redexes with histories. Further, we show that sharing is compositional: the sharing in a DFS F can be decomposed into a weaker sharing F' (such as zig-zag) and a sharing in the implementation F'I of F' stronger than zig-zag. These results require study of the family relation in non-duplicating SDRSs. We show that zig-zag forms a family-relation in every non-duplicating SDRS, and that it is the only separable family relation in such SDRSs. © 2003 Published by Elsevier Science B.V.

关键词： Computer science

来源：评论

学校读者我要写书评

暂无评论

Evaluating Semi-Exhaustive Verification Techniques for Bug Hunting

引用

Electronic Notes in Theoretical Computer Science 2001年第2期23卷 11-22页

作者： Ranan Fraer Gila Kamhi Limor Fix Moshe Y. Vardi Logic and Validation Technology Intel Corp. Haifa Israel Dept. of Computer Science Rice University

关键词：

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：