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

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

来源：评论

学校读者我要写书评

暂无评论

Word-level symbolic simulation in processor verification

引用

IEE PROCEEDINGS-COMPUTERS AND DIGITAL TECHNIQUES 2004年第5期151卷 356-366页

作者： Alizadeh, B Navabi, Z Univ Tehran Dept Elect & Comp Engn Tehran 14399 Iran

Formal verification of RT-level digital systems has attracted attention due to its efficiency over traditional simulation methods. This technology is still at its infancy and faces problems of property checking efficiency, memory explosion, and simultaneously the handling of data and control modules of hardware to be verified. Various methods of representing hardware and/or algorithms for property checking have been proposed to overcome these problems. One such method is symbolic simulation, which is attracting increasing interest in the area of digital circuit validation. It allows the verification engineer to explore all, or a major portion, of the circuit's state space without the need for designing time-consuming test stimuli. However, the complexity and unpredictable run-time behaviour of symbolic simulation have limited its scope to small-to-medium size circuits. A proposed solution for formal verification of digital systems is the use of symbolic simulation of a word-level representation. For this purpose a high-level model is described for digital circuits in the form of a distributed table-based representation that is suitable for application of formal verification property checking. The distributed table-based representation means that the next-state, output and intermediate signals are represented in a table that retains hierarchy of signal assignments without flattening them. In the model a design is represented by an hierarchical structure of integer equations, instead of a binary decision diagram. A subset of PSL (property specification language) can be directly applied to circuits described in the proposed representation. In addition, a set of integer equations are symbolically. simulated based on the specified property in a predictable time. The word-level representation is a canonical form of the linear Taylor expansion diagram.

关键词： microprocessor chips digital circuit validation integer programming signal assignment hierarchy linear Taylor expansion diagram File organisation hierarchical structure property checking efficiency Microprocessor chips distributed table-based representation processor verification logic simulation high-level model RT-level digital systems data structures property specification language PSL word-level representation Computer-aided logic design specification languages integer equations memory explosion Formal methods formal verification word-level symbolic simulation data flow graphs

来源：评论

学校读者我要写书评

暂无评论

Efficient Cross-Level processor verification using Coverage-guided Fuzzing 22

Efficient Cross-Level Processor Verification using Coverage-...

引用

32nd Great Lakes Symposium on VLSI (GLSVLSI)

作者： Bruns, Niklas Herdt, Vladimir Grosse, Daniel Drechsler, Rolf Univ Bremen Inst Comp Sci Bremen Germany Univ Bremen DFKI GmbH Cyber Phys Syst Inst Comp Sci Bremen Germany Johannes Kepler Univ Linz Inst Complex Syst Linz Austria DFKI GmbH CyberPhys Syst Bremen Germany

ISBN: (纸本)9781450393225

In this paper, we propose a novel simulation-based cross-level approach for processor verification at the Register-Transfer Level (RTL). We leverage state-of-the-art coverage-guided fuzzing techniques from the software domain to generate processor-level input stimuli. An Instruction Set Simulator (ISS) is utilized as a reference model for the RTL processor under test in an efficient co-simulation setting. To further boost the fuzzing effectiveness, we devised custom mutation procedures tailored for the processor verification domain. Our experiments using the popular open-source RISC-V based VexRiscv processor demonstrate the effectiveness of our approach in finding intricate bugs at the processor level.

关键词： Cross-Level verification processor verification Fuzzing

来源：评论

学校读者我要写书评

暂无评论

Industrial experience with test generation languages for processor verification

Industrial experience with test generation languages for pro...

引用

41st Design Automation Conference

作者： Behm, M Ludden, J Lichtenstein, Y Rimon, M Vinov, M IBM Dev Ctr Austin TX USA

ISBN: (纸本)1581138288

We report on our experience with a new test generation language for processor verification. The verification of two superscalar multiprocessors is described and we show the ease of expressing complex verification tasks. The cost and benefit are demonstrated: training takes up to six months;the simulation time required for a desired level of coverage has decreased by a factor of twenty;the number of escape bugs has been reduced.

关键词： functional verification processor verification test generation

来源：评论

学校读者我要写书评

暂无评论

Efficient Cross-Level Testing for processor verification: A RISC-V Case-Study

Efficient Cross-Level Testing for Processor Verification: A ...

引用

Forum for Specification and Design Languages (FDL)

作者： Herdt, Vladimir Grosse, Daniel Jentzsch, Eyck Drechsler, Rolf DFKI GmbH Cyber Phys Syst Bremen Germany Johannes Kepler Univ Linz Chair Complex Syst Linz Austria MINRES Technol GmbH Munich Germany Univ Bremen Inst Comp Sci Bremen Germany

ISBN: (纸本)9781728189284

Extensive processor verification at the Register-Transfer Level (RTL) is crucial to avoid bugs. Therefore, simulation-based approaches are prevalent but they require efficient test generation methods to achieve a thorough verification. In this paper we propose an efficient cross-level testing approach for processor verification targeting the RISC-V Instruction Set Architecture (ISA). We generate an endless instruction stream without restrictions on the generated instructions by evolving the instruction stream on-the-fly during simulation. An Instruction Set Simulator (ISS) is leveraged as reference model for the RTL core under test in a tightly coupled cross-level co-simulation setting. This enables a very efficient and comprehensive testing process. As a case-study we present results on the verification of the 32 bit pipelined RISC-V core of MINRES The Good Folk (TGF) Series Our approach has been very effective in finding several serious bugs.

关键词： RISC-V Cross-Level processor verification Instruction Stream Co-Simulation

来源：评论

学校读者我要写书评

暂无评论

Formal verification of a complex pipelined processor

引用

FORMAL METHODS IN SYSTEM DESIGN 2003年第2期23卷 171-213页

作者： Hosabettu, R Gopalakrishnan, G Srivas, M Sun Microsyst Inc Sunnyvale CA USA Univ Utah Salt Lake City UT USA RealChip Inc Sunnyvale CA USA

This paper addresses the problem of formally verifying the correctness of a complex pipelined microprocessor at the micro-architectural level of abstraction. The design verified is an example out-of-order execution processor with a reorder buffer, a store buffer, branch prediction, speculative execution and exceptions. We propose a systematic approach called the Completion Functions Approach to decompose and incrementally build its proof of correctness. The central idea is to construct the abstraction function using completion functions, one per unfinished instruction, each of which specifies the effect on the programmer visible state components of completing the instruction. This construction of the abstraction function leads to a very natural decomposition of the proof into proving a series of verification conditions. The approach prescribes a systematic way to generate these verification conditions which can then be discharged with a high degree of automation using techniques based on decision procedures and rewriting. The verification was completed in 34 person days, which we believe, is a modest investment in return for the significant benefits of formal verification.

关键词： formal verification processor verification completion functions PVS

来源：评论

学校读者我要写书评

暂无评论

Functional verification of Arithmetic Logic Unit and Instruction Fetch Unit of a 32-bit RV321M ISA based RISC-V processor 10

Functional Verification of Arithmetic Logic Unit and Instruc...

引用

10th IEEE International Conference on Electronics, Computing and Communication Technologies (IEEE CONECCT)

作者： Verma, Reshma Hrishikesh, C. S. Shrinivasan, Lakshmi Ramaiah Inst Technol Dept Elect & Comminicat Bengaluru Karnataka India

ISBN: (纸本)9798350385939;9798350385922

verification is a pivotal process in the design life cycle of integrated circuits, ensuring the functionality aligns with the chosen architecture. This paper focuses on the verification of the Arithmetic Logic Unit (ALU) and Instruction Fetch Unit (IFU) of a processor using Universal verification Methodology (UVM). By adopting a simulation-based approach, this project aims to enhance confidence in the conformance of the ALU and IFU design to their specifications. Through this project, we aim to establish a robust verification methodology using UVM for validating the ALU and IFU components in a processor design. The adoption of UVM promises to enhance verification quality, scalability, and reusability while ensuring adherence to processor specifications.

关键词： processor verification ALU verification IFU verification Universal verification Methodology (UVM) RISC-V processor Functional verification Simulation - Based Approach VLSI Design Conformance Testing Design under Test (DUT)

来源：评论

学校读者我要写书评

暂无评论

Improve the verification Productivity: Some Best Practices from SoC and processor Projects 15

Improve the Verification Productivity: Some Best Practices f...

引用

15th International Microprocessor Test and verification Workshop (MTV)

作者： Han, Weihua Synopsys Inc Austin TX 78746 USA

ISBN: (纸本)9781467368582

Challenges of a complex chip verification come from every aspect, such as network file system (NFS) access, coding style etc. This paper presents some best practices from several sytem-on-chip (SoC) and processor projects we completed recently. It includes: improve NFS access during regression, save and restore technologies for simulation and interactive debug, compilation technologies based on design partitioning and pre-compiled design units, a mixed-signal co-simulation environment involving both UPF based low power RTL simulation and transistor level simulation, etc. These best practices improved the verification productivity and helped us to complete the projects successfully on schedule.

关键词： SoC verification processor verification Simulation Program Relocation Partition Compilation Pre-Compiled Design Mixed-signal Low Power co-simulation

来源：评论

学校读者我要写书评

暂无评论

A framework for the validation of processor architecture compliance

A framework for the validation of processor architecture com...

引用

44th ACM/IEEE Design Automation Conference

作者： Adir, Allon Asaf, Sigal Fournier, Laurent Jaeger, Itai Peled, Ofer IBM Res Lab Haifa Mt Carmel IL-31905 Haifa Israel

ISBN: (纸本)9781595937711

We present a framework for validating the compliance of a design with a given architecture. Our approach is centered on the concept of misinterpretations. These include missing behavior, wrong understanding of a behavior, or confusion with similar behavior described in the architecture or elsewhere. We formally capture the architecture behavior in the form of flowcharts and automatically derive a list of architecture misinterpretations from these flowcharts. These misinterpretations constitute the backbone of coverage models targeted by a suite of tests. The suite is automatically generated by a model-based test case generator. A compliance validation System based on these principles has been developed and used in two actual industrial processes of checking compliance with the PowerPC architecture.

关键词： compliance suite conformance processor verification

来源：评论

学校读者我要写书评

暂无评论

Using field-repairable control logic to correct design errors in microprocessors

引用

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS 2008年第2期27卷 380-393页

作者： Wagner, Ilya Bertacco, Valeria Austin, Todd Univ Michigan Dept Elect Engn & Comp Sci Ann Arbor MI 48109 USA

Functional correctness is a vital attribute of any hardware design. Unfortunately, due to extremely complex architectures, widespread components, such as microprocessors, are often released with latent bugs. The inability of modern verification tools to handle the fast growth of design complexity exacerbates the problem even further. In this paper, we propose a novel hardware-patching mechanism, called the field-repairable control logic (FRCL), that is designed for in-the-field correction of errors in the design's control logic-the most common type of defects, as our analysis demonstrates. Our solution introduces an additional component in the processor's hardware, a state matcher, that can be programmed to identify erroneous configurations using signals in the critical control state of the processor. Once a flawed configuration is "matched," the processor switches into a degraded mode, a mode of operation which excludes most features of the system and is simple enough to be formally verified, yet still capable to execute the full instruction-set architecture at one instruction at a time. Once the program segment exposing the design flaw has been executed in a degraded mode, we can switch the processor back to its full-performance mode. In this paper, we analyze a range of approaches to selecting signals comprising the processor's critical control state and evaluate their effectiveness in representing a variety of design errors. We also introduce a new metric (average specificity per. signal) that encodes the bug-detection capability and amount of control state of a particular critical signal set. We demonstrate that the FRCL can support the detection and correction of multiple design errors with a performance impact of less than 5% as long as the incidence of the flawed configurations is below 1% of dynamic instructions. In addition, the area impact of our solution is less than 2% for the two microprocessor designs that we investigated in our experiments.

关键词： hardware patching processor verification

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：