资料介绍
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!
- 网络变压器HR911105A原理图及PCB封装下载 152次下载
- 普中51-单核-A3&A4开发板原理图下载 16次下载
- 语音芯片WT588E02A-8S产品说明书 13次下载
- 爱华无线电收音机FR-A120/FR-A125维修手册 2次下载
- 爱华无线电收音机FR-A270/FR-A275维修手册 5次下载
- 三菱A系列PLC解密软件下载 11次下载
- 高效高功率同步整流升压DC-DC芯片AMT6802 19次下载
- 爱华磁带随身听FR-A530/A532规格说明书 0次下载
- 1.2MHz低噪DC-DC升压开关电容倍压器PW5410A 2次下载
- 1.5A高效同步低电压电源变频器芯片HM6350A 8次下载
- Optimization of Extraction Technology and Property Analysis of CORTEX 5次下载
- LabVIEW Scripting 编程指南
- 功能验证覆盖测量与分析 0次下载
- Functional Verification Coverage Measurement and Analysis 0次下载
- 路线图正式产权核查 0次下载
- a17芯片提升多少 a17芯片与a16芯片的比较 5946次阅读
- Formal Verification的基础知识 2106次阅读
- 谈谈Formal验证中的Equivalence Checking 3581次阅读
- SOC V2.0的Formal是什么? 1130次阅读
- chiplet和SoC、SiP及其IP核等有什么关系呢? 1403次阅读
- 形式验证工具对系统功能的设计 1316次阅读
- 宽禁带器件和仿真环境介绍 1457次阅读
- 分析clock tree的小工具——CCOPT Clock Tree Debugger(二) 8893次阅读
- NoC技术的应用优势、关键技术难点及发展趋势分析 6281次阅读
- 在贴片加工厂中有哪些安全防护需要了解 1306次阅读
- 复合放大器实现高精度的高输出驱动能力 获得最佳的性能 1600次阅读
- 用降压型稳压器或线性稳压器电源时值来会为负载供电 984次阅读
- 锂电池并联充电时保护板均衡原理 3w次阅读
- 更小更智能的电机控制器推进HEV/EV市场 1105次阅读
- xilinx公司的代理商有哪些_十大xilinx公司的代理商推荐 3.9w次阅读
下载排行
本周
- 1电子电路原理第七版PDF电子教材免费下载
- 0.00 MB | 1490次下载 | 免费
- 2单片机典型实例介绍
- 18.19 MB | 92次下载 | 1 积分
- 3S7-200PLC编程实例详细资料
- 1.17 MB | 27次下载 | 1 积分
- 4笔记本电脑主板的元件识别和讲解说明
- 4.28 MB | 18次下载 | 4 积分
- 5开关电源原理及各功能电路详解
- 0.38 MB | 10次下载 | 免费
- 6基于AT89C2051/4051单片机编程器的实验
- 0.11 MB | 4次下载 | 免费
- 7蓝牙设备在嵌入式领域的广泛应用
- 0.63 MB | 3次下载 | 免费
- 89天练会电子电路识图
- 5.91 MB | 3次下载 | 免费
本月
- 1OrCAD10.5下载OrCAD10.5中文版软件
- 0.00 MB | 234313次下载 | 免费
- 2PADS 9.0 2009最新版 -下载
- 0.00 MB | 66304次下载 | 免费
- 3protel99下载protel99软件下载(中文版)
- 0.00 MB | 51209次下载 | 免费
- 4LabView 8.0 专业版下载 (3CD完整版)
- 0.00 MB | 51043次下载 | 免费
- 5555集成电路应用800例(新编版)
- 0.00 MB | 33562次下载 | 免费
- 6接口电路图大全
- 未知 | 30320次下载 | 免费
- 7Multisim 10下载Multisim 10 中文版
- 0.00 MB | 28588次下载 | 免费
- 8开关电源设计实例指南
- 未知 | 21539次下载 | 免费
总榜
- 1matlab软件下载入口
- 未知 | 935053次下载 | 免费
- 2protel99se软件下载(可英文版转中文版)
- 78.1 MB | 537791次下载 | 免费
- 3MATLAB 7.1 下载 (含软件介绍)
- 未知 | 420026次下载 | 免费
- 4OrCAD10.5下载OrCAD10.5中文版软件
- 0.00 MB | 234313次下载 | 免费
- 5Altium DXP2002下载入口
- 未知 | 233045次下载 | 免费
- 6电路仿真软件multisim 10.0免费下载
- 340992 | 191183次下载 | 免费
- 7十天学会AVR单片机与C语言视频教程 下载
- 158M | 183277次下载 | 免费
- 8proe5.0野火版下载(中文版免费下载)
- 未知 | 138039次下载 | 免费
评论
查看更多