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

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

3天内不再提示

分享一些形式验证(Formal Verification)的经典视频

芯片验证日记 来源:芯片验证日记 作者:芯片验证日记 2023-02-11 13:15 次阅读
加入交流群
微信小助手二维码

扫码添加小助手

加入工程师交流群

0.前言:

前段时间很多朋友在微信群里讨论Formal验证的视频资料问题,今天整理好了,分享给大家。

1.什么是形式验证(Formal Verification)

在计算机硬件(特别是集成电路)和软件系统的设计过程中,形式验证的含义是根据某个或某些形式规范或属性,使用数学的方法证明其正确性或非正确性。形式验证是一个系统性的过程,将使用数学推理来验证设计意图(指标)在实现(RTL)中是否得以贯彻。

由于仿真对于超大规模设计来说太耗费时间,形式验证(Formal Verification)就出现了。FV的主要思想是通过使用形式证明的方式来验证一个设计的功能是否正确。FV主要靠工具自己来完成,无需开发测试向量(断言还是需要写的),这比功能仿真的时间要少很多。

2.分享的Formal Verification视频资料

关注微信公众号《芯片验证日记》,后台回复”formal”,可得本文所有formal视频资料对应的百度链接,目录如下图所示。

poYBAGPnItyABozMAAGCGbwQFvw444.png

2.1 《Formal_Coverage》的内容,如下图所示:

pYYBAGPnIyeAbDQxAAS0HzhqNeE509.png

2.2 《Synopsys_VC-Formal_apps讲解》的内容,如下图所示:

poYBAGPnI1yAEPsaAAMHPNusGqE653.png

2.3 《动态系统的形式化分析与控制-上海交通大学殷翔》的内容,如下图所示:

pYYBAGPnI5aAEcxsAAaYIK655nI229.png

2.4《逻辑与形式化方法-龙星计划》的内容,如下图所示:

poYBAGPnI9GAU9PgAAbREDW8cBw696.png

3.声明

本文所有的视频资料都是来自B站公开的视频,如有侵权请后台联系作者删除。

最后,收集整理资料非常费时,如果觉得对您有帮助,麻烦点个在看,或者赏个鸡腿也行。谢谢!

审核编辑黄宇

声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉
  • 形式验证
    +关注

    关注

    0

    文章

    8

    浏览量

    5849
收藏 人收藏
加入交流群
微信小助手二维码

扫码添加小助手

加入工程师交流群

    评论

    相关推荐
    热点推荐

    如何使用 powerquad 加速器中的一些功能以及 CMSIS 原始实现中的一些功能?

    )。 如何使用 powerquad 加速器中的一些功能以及 CMSIS 原始实现中的一些功能。 Example: I do not want to call arm_mat_trans_q15 powerquad
    发表于 04-03 06:37

    时钟缓冲器的一些主要应用领域介绍

    电子设备和通信系统中都有广泛的应用,以下是一些主要的应用领域介绍:1.计算机与外设接口计算机内部的各种硬件设备需要通过总线相互通信,而这些设备的时钟信号通常是非常不稳
    的头像 发表于 04-02 16:30 8575次阅读
    时钟缓冲器的<b class='flag-5'>一些</b>主要应用领域介绍

    RDMA设计35:基于 SV 的验证平台

    功能的模型。接下来将对验证环境和 RDMA 子系统模型的设计进行详细分析。 B站已给出相关性能的视频,如想进步了解,请搜索B站用户:专注与守望 https://www.bilibili.com
    发表于 02-01 13:14

    爬壁机器人磁铁的一些常见问题

    爬壁机器人近几年比较火,它是类能够在垂直墙面、天花板、倾斜表面上移动和作业的特种机器人,今天我们不聊其它,只聊下关于磁吸附应用中的磁铁,以下是小编整理的关于爬壁机器人中磁铁的一些常见问题。
    的头像 发表于 01-09 10:06 432次阅读
    爬壁机器人磁铁的<b class='flag-5'>一些</b>常见问题

    关于六类网线一些问题的解答

    今天我们就围绕网友一些常见的关于六类网线的问题进行下汇总式解答: 问 六类网线可以当电源用吗? 答 六类网线并不是设计用于传输电力的电缆,因此般不建议将其用于电源传输。 尽管六类网线的线芯可以
    的头像 发表于 12-09 11:13 763次阅读

    贴片电容精度J±5%的一些详细知识

    贴片电容精度J±5%表示电容的实际值与标称值之间的偏差范围在±5%以内 ,以下是关于贴片电容精度J±5%的一些详细知识: 、精度等级含义 J±5% :字母“J”在贴片电容的标识中通常表示标称精度
    的头像 发表于 11-20 14:38 963次阅读
    贴片电容精度J±5%的<b class='flag-5'>一些</b>详细知识

    蜂鸟E203的浮点指令集F的一些实现细节

    蜂鸟E203的浮点指令集F的一些实现细节 既然E203不是多发射,且为了节省面积,一些指令使用FPU内的同个子模块来执行,即FPU同时只能进行种计算,我们只在FPU内部署了11个
    发表于 10-24 08:57

    在Linux ubuntu上使用riscv-formal工具验证蜂鸟E203 SoC的正确性

    内容:在Linux ubuntu上使用riscv-formal工具验证蜂鸟E203 SoC的正确性 步骤: 1、下载和安装riscv-formal工具: bash复制代码 git clone
    发表于 10-24 07:52

    推荐一些可以验证电能质量在线监测装置数据准确性的工具

    验证电能质量在线监测装置数据准确性的工具需覆盖信号模拟、现场测试、数据分析全流程。以下结合行业标准与最新技术,从四大类工具中精选核心产品并说明其应用场景: 、高精度标准源设备:实验室基准校准 1.
    的头像 发表于 09-18 14:28 707次阅读
    推荐<b class='flag-5'>一些</b>可以<b class='flag-5'>验证</b>电能质量在线监测装置数据准确性的工具

    NVMe高速传输之摆脱XDMA设计23:UVM验证平台

    十分复杂,需要使用成熟的验证知识产权(Verification IP,VIP)保证仿真的准确性和效率,这类的 VIP 通常十分昂贵并且复杂;另方面,PCIE 集成块是 Xilinx
    发表于 08-26 09:49

    射频工程师需要知道的一些常见转接头

    ,是由于转接头的损坏造成的,而且有些接头的连接固定的方式不对,每次修好的仪器,过去后客户又按照他们原来的方式去拧紧了。特别是在一些生产型的企业,由于操作人员流动性比较
    的头像 发表于 08-06 17:39 1549次阅读
    射频工程师需要知道的<b class='flag-5'>一些</b>常见转接头

    NVMe高速传输之摆脱XDMA设计18:UVM验证平台

    十分复杂,需要使用成熟的验证知识产权(Verification IP,VIP)保证仿真的准确性和效率,这类的 VIP 通常十分昂贵并且复杂;另方面,PCIE 集成块是 Xilinx
    发表于 07-31 16:39

    适用于SystemC/C++验证形式化解决方案

    虽然 SystemC/C++ 编程风格已使用多年,但最近出现了一些特定使用模式,它们推动工程团队采用共同的设计流程。这包括抽象算法设计代码用作高层次综合 (HLS) 工具的输入,虚拟平台模型用于早期软件测试,可配置的知识产权 (IP) 模块,等等。
    的头像 发表于 06-24 11:07 1411次阅读
    适用于SystemC/C++<b class='flag-5'>验证</b>的<b class='flag-5'>形式</b>化解决方案

    筑牢汽车品质基石:深入剖析 DV 与 PV 验证

    在汽车产业蓬勃发展的当下,消费者对汽车品质的要求愈发严苛。汽车从设计图纸走向千家万户的过程中,DV(Design Verification,设计验证)与 PV(Production
    的头像 发表于 05-13 09:15 2092次阅读
    筑牢汽车品质基石:深入剖析 DV 与 PV <b class='flag-5'>验证</b>

    Debian和Ubuntu哪个好一些

    兼容性对比Debian和Ubuntu哪个好一些,并为您揭示如何通过RAKsmart服务器释放Linux系统的最大潜能。
    的头像 发表于 05-07 10:58 1413次阅读