SystemVerilog Assertions应用指南 Chapter1.20“ $past”构造

2023-10-21 03:52

本文主要是介绍SystemVerilog Assertions应用指南 Chapter1.20“ $past”构造,希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

 1.20“ $past”构造

        SVA提供了一个内嵌的系统任务“$past”,它可以得到信号在几个时钟周期之前的值。在默认情况下,它提供信号在前一个时钟周期的值。结构的基本语法如下

$past (signal_name ,number of clock cycles)

        这个任务能够有效地验证设计到达当前时钟周期的状态所采用的通路是正确的。属性p19检验的是在给定的时钟上升沿,如果表达式(c&&d)为真,那么两个周期前,表达式(a&&b)为真。

property p19;@(posedge clk) (c && d) |-> ($past ((a  && b),2)==1'b1);
endpropertya19: assert property(p19);

        图1-22显示了属性p19在模拟中的响应。表1-12总结了断言a19的状态和相关信号的采样值。断言在时钟周期1失败。在时钟周期1,信号“c”和信号“d”都为高,断言有一个有效的开始。于是检验器的后续算子需要比较两个周期前的表达式(a&&b)的值。但是由于不可能得到两个信号在时钟周期1之前两个周期的历史,信号的值被当作“x”,因此检验器在时钟周期1失败。

        检验在时钟周期5有一个真正的成功。在时钟周期5,由于信号“a”和信号“b”都为高,断言有一个成功的开始。后续算子检查在时钟周期3时表达式(a&&b)是否为真。正如期望的那样,在时钟周期3,信号“a”和信号“b”都被检测为高,因此检验成功。
        检验在时钟周期16失败。在时钟周期16,由于信号“a”和信号“b”都为高,断言也有一个成功的开始。后续算子检查在时钟周期3时表达式(a&&b)是否为真。信号“a”如期望的那样为高,但是信号“b”为低。这使得表达式(a&&b)为假,检验失败。


带时钟门控的$past构造

        $past构造可以由一个门控信号 (gating singal)控制。比如,在个给定的时钟沿,只有当门控信号的值为真时才检查后续算子的状况。使用门控信号的$past构造的基本语法如下

$past (signal_name, number of clock cycles ,gating signal);

        属性p20与属性p19相似。但是只有当门控信号“e”在任意给定的时钟上升沿有效时检验才被激活。

property p20;@(posedge clk) (c && d) |-> ($past ((a && b ),2,e)==1'b1);
endpropertya20: assert property(p20);

这篇关于SystemVerilog Assertions应用指南 Chapter1.20“ $past”构造的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/251740

相关文章

SpringBoot实现RSA+AES自动接口解密的实战指南

《SpringBoot实现RSA+AES自动接口解密的实战指南》在当今数据泄露频发的网络环境中,接口安全已成为开发者不可忽视的核心议题,RSA+AES混合加密方案因其安全性高、性能优越而被广泛采用,本... 目录一、项目依赖与环境准备1.1 Maven依赖配置1.2 密钥生成与配置二、加密工具类实现2.1

Oracle迁移PostgreSQL隐式类型转换配置指南

《Oracle迁移PostgreSQL隐式类型转换配置指南》Oracle迁移PostgreSQL时因类型差异易引发错误,需通过显式/隐式类型转换、转换关系管理及冲突处理解决,并配合验证测试确保数据一致... 目录一、问题背景二、解决方案1. 显式类型转换2. 隐式转换配置三、维护操作1. 转换关系管理2.

Nginx进行平滑升级的实战指南(不中断服务版本更新)

《Nginx进行平滑升级的实战指南(不中断服务版本更新)》Nginx的平滑升级(也称为热升级)是一种在不停止服务的情况下更新Nginx版本或添加模块的方法,这种升级方式确保了服务的高可用性,避免了因升... 目录一.下载并编译新版Nginx1.下载解压2.编译二.替换可执行文件,并平滑升级1.替换可执行文件

Python调用LibreOffice处理自动化文档的完整指南

《Python调用LibreOffice处理自动化文档的完整指南》在数字化转型的浪潮中,文档处理自动化已成为提升效率的关键,LibreOffice作为开源办公软件的佼佼者,其命令行功能结合Python... 目录引言一、环境搭建:三步构建自动化基石1. 安装LibreOffice与python2. 验证安装

分布式锁在Spring Boot应用中的实现过程

《分布式锁在SpringBoot应用中的实现过程》文章介绍在SpringBoot中通过自定义Lock注解、LockAspect切面和RedisLockUtils工具类实现分布式锁,确保多实例并发操作... 目录Lock注解LockASPect切面RedisLockUtils工具类总结在现代微服务架构中,分布

破茧 JDBC:MyBatis 在 Spring Boot 中的轻量实践指南

《破茧JDBC:MyBatis在SpringBoot中的轻量实践指南》MyBatis是持久层框架,简化JDBC开发,通过接口+XML/注解实现数据访问,动态代理生成实现类,支持增删改查及参数... 目录一、什么是 MyBATis二、 MyBatis 入门2.1、创建项目2.2、配置数据库连接字符串2.3、入

Apache Ignite 与 Spring Boot 集成详细指南

《ApacheIgnite与SpringBoot集成详细指南》ApacheIgnite官方指南详解如何通过SpringBootStarter扩展实现自动配置,支持厚/轻客户端模式,简化Ign... 目录 一、背景:为什么需要这个集成? 二、两种集成方式(对应两种客户端模型) 三、方式一:自动配置 Thick

Python标准库之数据压缩和存档的应用详解

《Python标准库之数据压缩和存档的应用详解》在数据处理与存储领域,压缩和存档是提升效率的关键技术,Python标准库提供了一套完整的工具链,下面小编就来和大家简单介绍一下吧... 目录一、核心模块架构与设计哲学二、关键模块深度解析1.tarfile:专业级归档工具2.zipfile:跨平台归档首选3.

SQL Server跟踪自动统计信息更新实战指南

《SQLServer跟踪自动统计信息更新实战指南》本文详解SQLServer自动统计信息更新的跟踪方法,推荐使用扩展事件实时捕获更新操作及详细信息,同时结合系统视图快速检查统计信息状态,重点强调修... 目录SQL Server 如何跟踪自动统计信息更新:深入解析与实战指南 核心跟踪方法1️⃣ 利用系统目录

使用IDEA部署Docker应用指南分享

《使用IDEA部署Docker应用指南分享》本文介绍了使用IDEA部署Docker应用的四步流程:创建Dockerfile、配置IDEADocker连接、设置运行调试环境、构建运行镜像,并强调需准备本... 目录一、创建 dockerfile 配置文件二、配置 IDEA 的 Docker 连接三、配置 Do