数字系统设计中形式验证
2017-08-09 22:54
274 查看
下图给出等价性验证的基本概念。
等价性验证用于验证A与B是否等价,这里的B是由A转换得到的。这里的A与B可以是RTL代码,也可以是门级网表。在进行等价性验证时,A是参考,B称为实现。可以用形式验证来检查综合结果是否正确(将RTL级的设计与门级网表比较)、插扫描链前后的网表是否一致、布局前后网表是否一致、插时钟树前后的网表是否一致、布线前后的网表是否一致。如下图所示。
通常在综合后、在第一次布线完成后以及每次对网表中的错误进行修改(ECO)时均要进行等性验证,等价性验证可以验证EDA工具的结果是否正确,也可以验证网表修改是否正确。例如,在设计布线完成后,设计者发现设计中有错误。这时候,需要在RTL代码与网表中同时作修改。如果RTL与门级修改不一致,
通过形式验证可以很容易发现。在进行RTL级与门级网表进行等价性比较的时候,等价性工具先将RTL代码综合成网表,然后将其与实现进行比较。其原理如下图:
等价性验证工具通过比较设计点中比较点的功耗与状态是否等价,以此来验证两个参考设计与实现是否等价。比较点是等价性验证中的一个重要概念。它包括输出、寄存器、黑盒子的输入等。一般来说形式工具会根据信号的命名来自动选择比较点,对一些特殊的、形式工具难以识别的比较点,设计者也可以手工进行设置。如下图所示:
需要注意的是,等价性验证仅能保证两个设计的一致性,但不能保证两个设计的正确性。因此在IC设计中,仿真仍然是必不可少的步骤。但是有了等价性验证工具之后,我们可以将主要精力放在RTL的仿真上。
下面介绍用formality进行形式验证的流程。
formality是synopsys的形式验证工具,它在进行形式验证的时候,步骤如下:
1)读入链接库:read_db ../../lib/target.db
2)读入参考设计,并设置顶层设计:
read_verilog r rtl/rtl.v
set_top mydesign
3)读入实现,并设置顶层设计:
read_verilog i gate/gate.v
set_top mydesign
4)设置一些与进行等价性验证有关的设置。例如:若设计中的某些模块不需要进行检查,可以将其设置为“黑盒子”;在验证插入扫描链的网表时,需要将测试模式信号与扫描使能信号设置为0等等。
5)进行比较点的匹配。采用match命令即可。一般来说,等价性验证工具会根据相近的信号命令来选取比较点,并给出比较点的报告。如果等价性工具无法识别某些比较点,或者识别有错误,设计者可以手工进行相应的设置。
6)进行验证。采用verif命令即可。
7)给出报告,如果发现错误,则利用图形方式进行调试。
整个流程图可以总结为下图:
<
4000
p>
等价性验证用于验证A与B是否等价,这里的B是由A转换得到的。这里的A与B可以是RTL代码,也可以是门级网表。在进行等价性验证时,A是参考,B称为实现。可以用形式验证来检查综合结果是否正确(将RTL级的设计与门级网表比较)、插扫描链前后的网表是否一致、布局前后网表是否一致、插时钟树前后的网表是否一致、布线前后的网表是否一致。如下图所示。
通常在综合后、在第一次布线完成后以及每次对网表中的错误进行修改(ECO)时均要进行等性验证,等价性验证可以验证EDA工具的结果是否正确,也可以验证网表修改是否正确。例如,在设计布线完成后,设计者发现设计中有错误。这时候,需要在RTL代码与网表中同时作修改。如果RTL与门级修改不一致,
通过形式验证可以很容易发现。在进行RTL级与门级网表进行等价性比较的时候,等价性工具先将RTL代码综合成网表,然后将其与实现进行比较。其原理如下图:
等价性验证工具通过比较设计点中比较点的功耗与状态是否等价,以此来验证两个参考设计与实现是否等价。比较点是等价性验证中的一个重要概念。它包括输出、寄存器、黑盒子的输入等。一般来说形式工具会根据信号的命名来自动选择比较点,对一些特殊的、形式工具难以识别的比较点,设计者也可以手工进行设置。如下图所示:
需要注意的是,等价性验证仅能保证两个设计的一致性,但不能保证两个设计的正确性。因此在IC设计中,仿真仍然是必不可少的步骤。但是有了等价性验证工具之后,我们可以将主要精力放在RTL的仿真上。
下面介绍用formality进行形式验证的流程。
formality是synopsys的形式验证工具,它在进行形式验证的时候,步骤如下:
1)读入链接库:read_db ../../lib/target.db
2)读入参考设计,并设置顶层设计:
read_verilog r rtl/rtl.v
set_top mydesign
3)读入实现,并设置顶层设计:
read_verilog i gate/gate.v
set_top mydesign
4)设置一些与进行等价性验证有关的设置。例如:若设计中的某些模块不需要进行检查,可以将其设置为“黑盒子”;在验证插入扫描链的网表时,需要将测试模式信号与扫描使能信号设置为0等等。
5)进行比较点的匹配。采用match命令即可。一般来说,等价性验证工具会根据相近的信号命令来选取比较点,并给出比较点的报告。如果等价性工具无法识别某些比较点,或者识别有错误,设计者可以手工进行相应的设置。
6)进行验证。采用verif命令即可。
7)给出报告,如果发现错误,则利用图形方式进行调试。
整个流程图可以总结为下图:
<
4000
p>
相关文章推荐
- 基于达芬奇技术的数字视频系统设计与实现
- [转]Verilog数字系统设计教程(大连理工一博士学习笔记)
- USB接口的数字摄像系统设计
- [导入]从架构设计到系统实施——基于.NET 3.0的全新企业应用系列课程(9):设计基于CardSpace的身份验证系统.zip(7.98 MB)
- DE2-70数字系统设计实验(3)--移位寄存器
- DE2-70数字系统设计(4)--基于Nios的LCD显示
- 系统设计中的业务验证设计1
- 系统级芯片设计语言和验证语言的发展
- 基于Quartus II 的FPGA/CPLD数字系统设计与应用(原理图编辑)
- (笔记)电路设计(十二)之高速数字系统滤波电容的设计应用
- [导入]从架构设计到系统实施——基于.NET 3.0的全新企业应用系列课程(9):设计基于CardSpace的身份验证系统.zip(7.98 MB)
- (转)数字电路的设计验证
- 系统设计中的业务验证设计2
- verilog 数字系统设计教程 读书笔记(1)
- 数字电路设计和搭建系统的主要工作
- [毕业设计]手写数字识别系统设计与实现
- 如果系统要使用超大整数(超过long长度范围),请你设计一个数据结构来存储这种超大型数字以及设计一种算法来实现超大整数加法运算
- verilog 数字系统设计教程 读书笔记(2)
- mysql:获取系统当前的数字形式时间值
- 详解HTTPS中数字证书验证系统