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

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

3天内不再提示

介绍放宽约束的等价性比对sequential equivalence

电子工程师 来源:芯片验证工程师 作者:验证哥布林 2022-07-19 09:53 次阅读

在上一篇文章《等价性比对验证之combinational equivalence》中,我们说过Combinational equivalence比对最严格,但是在很多场景下有限制(不适应于时序单元变化的场景)。

本章我们在时序单元数量或者位置发生变化,但是整体功能不变的场景下对于Combinational equivalence进行一定程度的放松。

SEQUENTIAL EQUIVALENCE

Sequential equivalence被某些EDA工具称之为周期精确等价(cycle-accurate equivalence),名字不重要,关键的是理解它和combinational equivalence的区别。

Sequential equivalence是使用EDA工具形式化地确认是否SPEC模型和IMP模型能否在相同的激励下产生相同的输出(这是最基本的要求)。另外不同于combinational equivalence,它不要求电路中每个时序单元都能够精确地比对,最终只要输出的时序一致即可。

如此,就可能在综合工具进行一些特殊优化使得时序单元数量、位置和流水线深度发生变化时依然能够比对通过。

其实伴随着对于combinational equivalence的要求的放松,

sequential equivalence以及后面即将介绍的transaction-based equivalence.
越来越贴近FPV。



审核编辑:刘清

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

    关注

    4

    文章

    245

    浏览量

    31246
  • SPEC
    +关注

    关注

    0

    文章

    31

    浏览量

    15676
  • IMP
    IMP
    +关注

    关注

    0

    文章

    10

    浏览量

    8316

原文标题:等价性比对验证之sequential equivalence

文章出处:【微信号:芯片验证工程师,微信公众号:芯片验证工程师】欢迎添加关注!文章转载请注明出处。

收藏 人收藏

    评论

    相关推荐

    一文解析最严格的等价比对验证combinational equivalence

    Combinational equivalence是使用EDA工具进行等价比对中最成熟的FEV技术,一般情况下是将RTL和原理图网表进行等价比对
    的头像 发表于 07-19 09:48 1306次阅读

    Xilinx FPGA管脚物理约束介绍

    引言:本文我们简单介绍下Xilinx FPGA管脚物理约束,包括位置(管脚)约束和电气约束
    发表于 07-25 10:13 4108次阅读

    FPGA时序约束之衍生时钟约束和时钟分组约束

    在FPGA设计中,时序约束对于电路性能和可靠性非常重要。在上一篇的文章中,已经详细介绍了FPGA时序约束的主时钟约束
    发表于 06-12 17:29 1265次阅读

    软件测评的等价类设计方法

    主要看文档,不是代码 五、等价类的划分: 1、有效等价类:指符合《需求规格说明书》,输入合理的数据集合 2、无效等价类:指不符合《需求规格说明书》,输入不合理的数据集合 二者概念可以共同记忆 六、
    发表于 12-29 10:22

    基于特征的音频比对技术

    的方式提取出能代表音频主要信息特征的质心、均方根和前12个Mel倒谱系数,并分别计算这3类参数的欧氏距离,根据欧氏距离的值与阀值ε之间的关系,完成音频间的比对任务.经实践证明,这套方案对于音频比对具有较高的准确和较好的实时
    发表于 03-06 21:40

    allegro布局完成后修改线宽约束后如何更新到PCB中

    `图片中高亮部分是GND网络,在首次布线之后,又对GND网络线宽约束进行了修改,修改后不知道在哪里更新,图中较宽的线是删除后重新布线的,有没有方法不删除布线直接更新的?请大神指导,谢谢!`
    发表于 11-13 16:12

    线宽约束规则失效?

    我将DDR的数据地址线设置为4mil线宽,已经画了一部分了。今天临时修改了下约束管理器的设置,结果开始报错了:从第二幅图看出,我明明设置的是4mil。但是第一幅图显示,系统认为我任然用的是默认线宽设置。这是怎么回事呢
    发表于 04-20 17:29

    分享一个FEC RTLvs Netlist等价比对的示例

    中,只要你使用逻辑综合将RTL转换为门级网表,那么你必然需要使用FEC工具进行RTL和门级网表等价比对。下图是一个FEC RTLvs Netlist等价
    发表于 07-22 14:56

    时序逻辑设计原则 (Sequential Logic Des

    时序逻辑设计原则 (Sequential Logic Design principles):A sequential logic circuit is one whose outputs
    发表于 09-26 12:54 33次下载

    时序逻辑设计实践 (Sequential Logic Des

    时序逻辑设计实践 (Sequential Logic Design Practices)The purpose of this chapter is to familiarize you
    发表于 09-26 12:57 13次下载

    动态矩阵/Field Sequential 是什么意思

    动态矩阵/Field Sequential 是什么意思     所谓Field Sequential技术就是透过对红、绿、蓝的影像,进行高速切换来实现彩色显示
    发表于 03-27 11:52 735次阅读

    支持Baseline和Extended Sequential

    支持Baseline和Extended Sequential的JPEG编码IP核 CAST公司宣布提供独有的同时支持Baseline(8位)和Extended Sequential(12位)
    发表于 05-18 09:22 584次阅读

    【新专利介绍】三表位电能表自助比对装置及其比对方法

    今天为大家介绍一项国家发明授权专利——三表位电能表自助比对装置及其比对方法。该专利由贵州长征电器成套有限公司申请,并于2018年2月9日获得授权公告。
    发表于 07-10 15:01 690次阅读

    FPGA约束的详细介绍

    介绍FPGA约束原理,理解约束的目的为设计服务,是为了保证设计满足时序要求,指导FPGA工具进行综合和实现,约束是Vivado等工具努力实现的目标。所以首先要设计合理,才可能满足
    发表于 06-25 09:14 6386次阅读

    介绍3个时序优化的RTL改动及其中Formal SEC的角色

    对于这种pipe个数变化,但是端到端功能不变的修改,同样可以使用sequential FEC来进行等价比对。只不过有所区别的是,需要指定比对是latency差异。
    的头像 发表于 08-09 15:44 1636次阅读
    <b class='flag-5'>介绍</b>3个时序优化的RTL改动及其中Formal SEC的角色