电子发烧友App

硬声App

0
  • 聊天消息
  • 系统消息
  • 评论与回复
登录后你可以
  • 下载海量资料
  • 学习在线课程
  • 观看技术视频
  • 写文章/发帖/加入社区
会员中心
创作中心

完善资料让更多小伙伴认识你,还能领取20积分哦,立即完善>

3天内不再提示
电子发烧友网>电子资料下载>电子书籍>A Roadmap for Formal Property

A Roadmap for Formal Property

2009-07-18 | rar | 2150 | 次下载 | 免费

资料介绍

What is formal property verification? A natural language such as English allows
us to interpret the term formal property verification in two ways, namely:
• Verification of formal properties, or
• Formal methods for property verification
This inherent ambiguity in natural languages has been the source of many
logical bugs in chip designs. Design specifications are sometimes interpreted
in different ways by different designers with the result that the design’s architectural
intent is not implemented correctly. In an era where bugs are more
costly than transistors, the industry is beginning to realize the value of using
formal specifications.
In practice there are indeed two ways in which property verification is
done today. These are static Assertion-based Verification (ABV) and dynamic
Assertion-based Verification (ABV). In both forms, formal properties specify
the correctness requirements of the design, and the goal is to check whether a
given implementation satisfies the properties. Static ABV techniques formally
verify whether all possible behaviors of the design satisfy the given properties.
Dynamic ABV is a simulation-based approach, where the properties are
checked over a simulation run – the verification is thereby confined to only
those behaviors that are encountered during the simulation. In this book, we
shall refer to static ABV as formal property verification (FPV), and continue
to use dynamic ABV to refer to the simulation based property verification
approach.
The main tasks for a practitioner of property verification are as follows:
1. Development of the formal property specification. The main challenge here
is to express key features of the design intent in terms of formal properties.
2. Verifying the consistency and completeness of the specification. This is a
necessary step, because the first task is a non-trivial one and subject to
errors and oversights.
3. Verifying the implementation against the formal property specification. In
order to perform this task effectively, a verification engineer must be aware
of the limitations of the verification tool and must know the best way to
use the tool under various types of constraints.
All the above tasks are replete with open issues – the focus of this book is to
consider some of these issues and attempt to forecast the roadmap for FPV
and dynamic ABV within the existing design verification flows of chip design
companies. This chapter will summarize some of the major challenges. Let us
use the following case as a running example for our discussion.
Example 1.1. Let us consider the specification of a 2-way priority arbiter having
the following interface:
mem-arbiter( input r1, r2, clk, output g1, g2 )
r1 and r2 are the request lines, g1 and g2 are the corresponding grant lines,
and clk is the clock on which the arbiter samples its inputs and performs the
arbitration.We assume that the arbitration decision for the inputs at one cycle
is reflected by the status of the grant lines in the next cycle. Let us suppose
that the specification of the arbiter contains the following requirements:
1. Request line r1 has higher priority than request line r2. Whenever r1 goes
high, the grant line g1 must be asserted for the next two cycles.
2. When none of the request lines are high, the arbiter parks the grant on
g2 in the next cycle.
3. The grant lines, g1 and g2, are mutually exclusive.
It is difficult to locate a book on formal verification that does not have an
arbiter example - we hereby follow the tradition!

下载该资料的人也在下载 下载该资料的人还在阅读
更多 >

评论

查看更多

下载排行

本周

  1. 1电子电路原理第七版PDF电子教材免费下载
  2. 0.00 MB  |  1490次下载  |  免费
  3. 2单片机典型实例介绍
  4. 18.19 MB  |  92次下载  |  1 积分
  5. 3S7-200PLC编程实例详细资料
  6. 1.17 MB  |  27次下载  |  1 积分
  7. 4笔记本电脑主板的元件识别和讲解说明
  8. 4.28 MB  |  18次下载  |  4 积分
  9. 5开关电源原理及各功能电路详解
  10. 0.38 MB  |  10次下载  |  免费
  11. 6基于AT89C2051/4051单片机编程器的实验
  12. 0.11 MB  |  4次下载  |  免费
  13. 7蓝牙设备在嵌入式领域的广泛应用
  14. 0.63 MB  |  3次下载  |  免费
  15. 89天练会电子电路识图
  16. 5.91 MB  |  3次下载  |  免费

本月

  1. 1OrCAD10.5下载OrCAD10.5中文版软件
  2. 0.00 MB  |  234313次下载  |  免费
  3. 2PADS 9.0 2009最新版 -下载
  4. 0.00 MB  |  66304次下载  |  免费
  5. 3protel99下载protel99软件下载(中文版)
  6. 0.00 MB  |  51209次下载  |  免费
  7. 4LabView 8.0 专业版下载 (3CD完整版)
  8. 0.00 MB  |  51043次下载  |  免费
  9. 5555集成电路应用800例(新编版)
  10. 0.00 MB  |  33562次下载  |  免费
  11. 6接口电路图大全
  12. 未知  |  30320次下载  |  免费
  13. 7Multisim 10下载Multisim 10 中文版
  14. 0.00 MB  |  28588次下载  |  免费
  15. 8开关电源设计实例指南
  16. 未知  |  21539次下载  |  免费

总榜

  1. 1matlab软件下载入口
  2. 未知  |  935053次下载  |  免费
  3. 2protel99se软件下载(可英文版转中文版)
  4. 78.1 MB  |  537791次下载  |  免费
  5. 3MATLAB 7.1 下载 (含软件介绍)
  6. 未知  |  420026次下载  |  免费
  7. 4OrCAD10.5下载OrCAD10.5中文版软件
  8. 0.00 MB  |  234313次下载  |  免费
  9. 5Altium DXP2002下载入口
  10. 未知  |  233045次下载  |  免费
  11. 6电路仿真软件multisim 10.0免费下载
  12. 340992  |  191183次下载  |  免费
  13. 7十天学会AVR单片机与C语言视频教程 下载
  14. 158M  |  183277次下载  |  免费
  15. 8proe5.0野火版下载(中文版免费下载)
  16. 未知  |  138039次下载  |  免费