[资料]

展示一个FPV执行空间的例子

2022-10-27 16:55:25 2359 FPV RTL 寄存器

0 1、展示一个FPV执行空间的例子　　简单来讲，FPV是用来数学方法来证明，RTL符合用户指定的一堆property（一般是SVA书写）。FPV工具，基于输入的约束，用数学方法分析RTL逻辑执行的所有可能的空间。与Simulation不同，FPV会同时check当前约束所有合法的值。　　FPV的输入一般有：　　RTL 　　待证明的property：assertions， cover points 　　约束：assumptions， clock ， reset 　　FPV输出一般有：　　证明了的property：proven assertion， unreachable cover points. 　　对于fail的assertion，或者reachable cover point ，都有一个对应的波形来显示failure或者reachbility 　　bounded or inconclusive proofs：不确定证明的一些assertion和coverpooint 原作者：木马哥验证工程师的自我修养 1 Formal property verification.pdf 649.44 KB , 下载次数: 0
举报淘帖0 只看该作者相关推荐 • FPV设计的状态空间主要由什么因素决定的 2348 • 双FPV摄像头板的资料分享 1296 • 分析FPV与EDA仿真（simulation）有何不同 2323 • 一、什么是FPV？ 26452 • 搭建FPV验证环境之创建assert与执行FPV简析 2641 • 什么是FPV？怎样去搭建FPV验证环境呢？ 2851 • 通过IDA调试一个函数进而展示栈空间的操作过程 6665 • 如何去制作一个低成本、有保护圈的FPV 863 • “坦克大战”基于WIFI网络的FPV遥控坦克 2862 • labview的一个小例子使用 4315