OVL assertion checker

news2024/12/26 4:34:39

目录

单周期断言:

1、ovl_always:

功能描述:

ovl和assert_always例子:​编辑​编辑

详细介绍: 

2、ovl_implication:

功能描述:

例子:

详细介绍: 

3、ovl_never:

功能描述:

例子:

详细介绍:

4、ovl_never_unknown:

功能描述:

例子:

详细介绍:

5、ovl_one_hot:

功能描述:

例子:

详细介绍:

6、ovl_range:

功能描述:

例子:

详细介绍:

7、ovl_zero_one_hot:

功能描述:

例子:

详细介绍:

多周期断言:  

8、ovl_cycle_sequence:

功能描述:

例子:

详细介绍:

9、ovl_next:

功能描述:

例子:

详细介绍:


单周期断言:

1、ovl_always:

  • 功能描述:
  • ovl_always断言检查器在时钟的每个活动边缘(时钟上升沿还是下降沿由clock_edge字段决定)检查单比特表达式test_expr。如果test_expr不是TRUE,就会发生always check冲突。

  • 重要字段:五个端口:test_expr,clock,reset,enable,fire;还有Patameters重点前三个,severtity_level和property_type一般选择默认,msg(断言错误时打印输出的消息,有默认VIOLTATION),clock_edge等
  • ovl和assert_always例子:
  • 详细介绍: 

2、ovl_implication:

  • 功能描述:
  • 是一种用于定义蕴含关系的宏,用于基于断言的验证。蕴含关系表示当某个条件成立时,另一个条件也必须成立。
  • ovl_implication断言检查器在时钟的每个活动边缘检查单个位表达式antecedent_expr。如果antecedent_expr为TRUE,则检查器验证consequent_expr的值也为TRUE。如果antecedent_expr不是TRUE,那么无论consequent_expr的值如何,断言都是有效的。
  • 前TRUE,后TRUE,则断言成功;前FALSE,后无所谓,断言都成功(就是成功)
  • 例子:
    `ovl_implication(CheckNonZero, a != 0, b != 0)
    
    //这个例子表示如果变量 a 的值不等于零,则变量 b 的值也必须不等于零。
    如果在仿真中发现 a != 0 为真而 b != 0 为假,
    那么将触发错误并报告 CheckNonZero 标签指定的问题。

 

  • 详细介绍: 

 

3、ovl_never:

  • 功能描述:
  • ovl_never断言检查器在时钟的每个活动边缘检查单比特表达式test_expr,以验证表达式的计算结果不是TRUE。

  • 例子:

  • 详细介绍:

 

 

4、ovl_never_unknown:

  • 功能描述:
  • ovl_never_unknown断言检查器检查时钟每个活动边缘的表达式限定符,以确定是否应该检查test_expr。如果qualifier的采样值为TRUE,则检查器计算test_expr,如果test_expr的值包含一个不是0或1的位,则断言失败。

  • 检查器用于确保某些数据在重置序列之后只有已知值。当必要时它也可以用来验证三状态输入端口驱动和三状态输出端口驱动已知值时。

  • 例子:

 

  • 详细介绍:

5、ovl_one_hot:

  • 功能描述:
  • ovl_one_hot断言检查器在时钟的每个活动边缘检查表达式test_expr,以验证表达式的计算结果为一个单热值(指只有一个位的值为1,其他都为0)。一个单热值恰好有一个位被设置为1。检查器用于验证控制电路,例如,它可以确保具有单热编码的有限状态机正常运行,并且恰好有一个位断言高。在数据路径电路中,检查器可以确保总线的使能条件不会导致总线竞争。

  • 例子:

 

  • 详细介绍:

 

6、ovl_range:

  • 功能描述:
  • ovl_range断言检查器在时钟的每个活动边缘检查表达式test_expr,以验证表达式落在从min到max(包括最大值)的范围内。如果test_expr < min或max <test_expr,断言失败。

  • 检查器对于确保某些控制结构值(如计数器和有限机器值)在其适当范围内是有用的。检查器对于确保数据路径变量和表达式在合法范围内也很有用。

  • 例子:

  • 详细介绍:

 

7、ovl_zero_one_hot:

  • 功能描述:
  • ovl_zero_one_hot断言检查器在时钟的每个活动边缘检查表达式test_expr,以验证表达式的计算结果是一个one-hot值还是为零。一个one-hot单热值恰好有一个位被设置为1。

  • 该检查器可用于验证控制电路、电路使能逻辑和仲裁逻辑。例如,它可以确保具有0 - 1冷编码的有限状态机正常运行,并且只有一个位被断言为高电平,否则为零。在数据路径电路中,检查器可以确保总线的使能条件不会导致总线争用。

  • 例子:

  • 详细介绍:

 

多周期断言:  

8、ovl_cycle_sequence:

  • 功能描述:
  • ovl_cycle_sequence断言检查器在时钟的活动边缘检查表达式event_sequence,以确定event_sequence中的位是否在时钟的连续活动边缘上依次断言。

  • 例如,以下4位值序列(其中b是任意位值)是一个有效序列:1BBB -> BBB -> BBLB -> BBB1;此系列对应于时钟连续活动边缘上的以下一系列事件:

周期1event_sequence [3] = = 1

周期2event_sequence [2] = = 1

周期3event_sequence [1] = = 1

周期4event_sequence [0] = = 1

  • 例子:

 

 

  • 详细介绍:

 

 

 

9、ovl_next:

  • 功能描述:
  • ovl_next断言检查器在时钟的每个活动边缘检查表达式start_event。如果start_event为TRUE,则发起检查。该检查将等待num_cks个时钟周期(即num_cks额外的活动时钟边),并计算test_expr。如果test_expr不为TRUE,断言失败。这些检查是流水线的,也就是说,每个周期都会启动一个检查start_event为TRUE(即使开启了重叠检查,并且发生了重叠违规)。

  • 如果关闭重叠检查(check_overlap为1),则在等待当前检查时可以启动其他检查。如果开启了重叠检查,如果start_event被采样为TRUE,则断言失败(上一个时钟的情况除外)。

  • 如果缺失开始检查是关闭的(check_missing_start为O),则test_expr在任何时候都可以为TRUE。如果开启了missing-start检查,那么如果test_expr为TRUE且没有对应的start事件(num_cks之前循环了),则断言失败。但如果test_expris为TRUE,在重置后的num_cks-1个周期内,没有对应的start事件,则结果是不确定的(即,在初始化结束后,test_expris为TRUE)。,缺失启动检查可能会失败,也可能不会失败)。

  • 例子:

 

  • 详细介绍:

  

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.coloradmin.cn/o/1413130.html

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈,一经查实,立即删除!

相关文章

JDWP原理分析与漏洞利用

JDWP(Java DEbugger Wire Protocol):即Java调试线协议,是一个为Java调试而设计的通讯交互协议,它定义了调试器和被调试程序之间传递的信息的格式。说白了就是JVM或者类JVM的虚拟机都支持一种协议,通过该协议,Debugger 端可以和 target VM 通信,可以获取目标 VM的包括类…

Sphinx的原理详解和使用

一、Sphinx介绍 1.1 简介 Sphinx是由俄罗斯人Andrew Aksyonoff开发的一个全文检索引擎。意图为其他应用提供高速、低空间占用、高结果 相关度的全文搜索功能。Sphinx可以非常容易的与SQL数据库和脚本语言集成。当前系统内置MySQL和PostgreSQL 数据库数据源的支持&#xff0c;也…

455. 分发饼干 - 力扣(LeetCode)

题目描述 假设你是一位很棒的家长&#xff0c;想要给你的孩子们一些小饼干。但是&#xff0c;每个孩子最多只能给一块饼干。 对每个孩子 i&#xff0c;都有一个胃口值 g[i]&#xff0c;这是能让孩子们满足胃口的饼干的最小尺寸&#xff1b;并且每块饼干 j&#xff0c;都有一个尺…

作者推荐 | 【深入浅出MySQL】「底层原理」探秘缓冲池的核心奥秘,揭示终极洞察

探秘缓冲池的核心奥秘&#xff0c;揭示终极洞察 缓存池BufferPool机制MySQL缓冲池缓冲池缓冲池的问题 缓冲池的原理数据预读程序的局部性原则&#xff08;集中读写原理&#xff09;时间局部性空间局部性 innodb的数据页查询InnoDB的数据页InnoDB缓冲池缓存数据页InnoDB缓存数据…

区间dp/线性dp,HDU 4293 Groups

一、题目 1、题目描述 After the regional contest, all the ACMers are walking alone a very long avenue to the dining hall in groups. Groups can vary in size for kinds of reasons, which means, several players could walk together, forming a group.   As the …

RuoYi-Vue前后端分离后台开发框架运行详细教程

一、官网下载代码 RuoYi-Vue是一款基于SpringBootVue的前后端分离极速后台开发框架。 若依官网&#xff1a;http://ruoyi.vip演示地址&#xff1a;http://vue.ruoyi.vip代码下载&#xff1a;https://gitee.com/y_project/RuoYi-Vue 下载之后解压&#xff0c;ruoyi-ui是前端代…

【JavaWeb】过滤器 Filter

文章目录 过滤器是什么&#xff1f;一、过滤器概述二、过滤器工作位置图解三、Filter接口API四、过滤器使用4.1 定义一个过滤器类,编写功能代码&#xff1a;4.2 xml配置&#xff1a;4.3 定义 servletG 目标资源 模拟测试 :4.4 过滤图解 五、过滤器生命周期六、过滤器链的使用6.…

香港服务器IP段4c和8c的区别及SEO选择建议

随着互联网的快速发展&#xff0c;服务器IP段的选择对于网站SEO优化至关重要。香港服务器IP段4C和8C是两种常见的IP段&#xff0c;它们在SEO优化中具有不同的特点和优势。本文将详细介绍这两种IP段的区别&#xff0c;并给出相应的SEO选择建议。 一、香港服务器IP段4C和8C的区别…

每日coding 2846. 边权重均等查询 236. 二叉树的最近公共祖先 35. 搜索插入位置 215. 数组中的第K个最大元素 2. 两数相加

2846. 边权重均等查询 xs&#xff0c;已放弃&#xff0c;考到直接寄 236. 二叉树的最近公共祖先 236. 二叉树的最近公共祖先 给定一个二叉树, 找到该树中两个指定节点的最近公共祖先。 百度百科中最近公共祖先的定义为&#xff1a;“对于有根树 T 的两个节点 p、q&…

向量表示在自然语言、知识图谱和图像视觉中的应用

目录 前言1 不同应用的向量表示1.1 自然语言中的向量表示1.2 知识图谱中的向量表示1.3 图像视觉中的向量表示 2 词的向量表示2.1 One-hot encoding的限制2.2 Bag-of-Words模型的不足2.3 Word Embedding的引入2.4. 词的分布式表示与语境关系 3 词向量模型3.1 CBoW&#xff08;Co…

swagger2 和 knife4j 整合

swagger整合knife4j 导入依赖 <dependency><groupId>com.github.xiaoymin</groupId><artifactId>knife4j-spring-boot-starter</artifactId><version>3.0.2</version></dependency>引入配置 我们自己写一个配置类也好,我这里写…

乐观锁的底层实现以及如何解决ABA问题

什么是乐观锁&#xff1f;乐观锁底层是如何实现的&#xff1f; 乐观锁是一种并发控制的策略。在操作数据的时候&#xff0c;线程读取数据的时候不会进行加锁&#xff0c;先去查询原值&#xff0c;操作的时候比较原来的值&#xff0c;看一下是都被其他线程修改&#xff0c;如果…

OpenHarmony—TypeScript到ArkTS约束说明

对象的属性名必须是合法的标识符 规则&#xff1a;arkts-identifiers-as-prop-names 级别&#xff1a;错误 在ArkTS中&#xff0c;对象的属性名不能为数字或字符串。通过属性名访问类的属性&#xff0c;通过数值索引访问数组元素。 TypeScript var x { name: x, 2: 3 };c…

STM32标准库开发—W25Q64详细介绍

W25Q64简介 Flash编程原理都是只能将1写为0&#xff0c;而不能将0写成1.所以在Flash编程之前&#xff0c;必须将对应的块擦除&#xff0c;而擦除的过程就是将所有位都写为1的过程&#xff0c;块内的所有字节变为0xFF.因此可以说&#xff0c;编程是将相应位写0的过程&#xff0c…

Ubuntu 22.04 安装tomcat

tomcat是常用的Java服务容器,这篇文章我们就来讲讲如何安装它。 更新软件包 首先是更新软件包,这是最常规的操作 sudo apt update 然后是开始安装,不多一会就可以安装好了 sudo apt install tomcat9 然后看一下状态 sudo systemctl status tomcat9 发现虽然启动了,但…

IS-IS:03 ISIS链路状态数据库

一个 OSPF 链路状态数据库是若干条 LSA 的集合。与此相似&#xff0c;一个 IS-IS 链路状态数据库是若干条 LSP 的集合。与 OSPF 链路状态数据库不同&#xff0c; IS-IS 链路状态数据库有 level-1 和 level-2 之分。 在IS-IS 协议中&#xff0c;每一条 LSP 都有一个剩余生存时间…

自学Java的第48,49,50,51天

IO流 应用场景 IO流的分类 文件字节输入流 写法 读取一个字节 读取多个字节 优化&#xff1a; 注意&#xff1a; 读取全部字节 写法 注意&#xff1a; 文件字节输出流 写法 案例&#xff1a; 写法 释放资源的方法 try-catch-finally 写法 try-with-resource 写法 字符流 …

linux内网搭建NFS网络文件系统(rpm)

linux 内网搭建nfs网络文件系统&#xff08;rpm包&#xff09; 前言&#xff1a;一、上传安装包到服务器二、NFS服务端配置三、建立共享目录(服务器端和客户端)四、添加配置共享目录&#xff08;服务器端&#xff09;五、NFS客户端配置六、测试共享服务 前言&#xff1a; 用自…

Type-C平板接口协议芯片介绍,实现单C口充放电功能

在现代平板电脑中&#xff0c;Type-C接口已经成为了一个非常常见的接口类型。相比于传统的USB接口&#xff0c;Type-C接口具有更小的体积、更快的传输速度和更方便的插拔体验。但是&#xff0c;在使用Type-C接口的平板电脑上&#xff0c;如何实现单C口充电、放电和USB2.0数据传…

【iOS ARKit】同时开启前后摄像头BlendShapes

在上一节中已经了解了 iOS ARkit 进行BlendShapes的基本操作&#xff0c;这一小节继续实践同时开启前后摄像头进行人脸捕捉和世界追踪。 iOS设备配备了前后两个摄像头&#xff0c;在运行AR 应用时&#xff0c;需要选择使用哪个摄像头作为图像输人。最常见的AR 体验使用设备后置…