Equivalence Checking学习笔记
基本步骤Setup输入包括经过验证的参考设计、库元素和修改后的设计。在此步骤中,将读入输入信息并创建数据结构,以方便后续步骤。
Mapping对设计的关键点进行映射和比较。逻辑锥通常用于组织比较点,是驱动比较点的组合逻辑块。逻辑锥的输入包括寄存器输出引脚、主输入端口和黑盒输出引脚。比较点包括寄存器、主输出端口和黑盒输入引脚。
Compare在比较过程中,将对关键映射点进行检查,以确定它们是等价、非等价还是反向等价。对于无法得出结论的设计部分,可以通过更高的难度重新运行来解决。
等价性检查的优势
效率更高:减少对较慢的门级仿真的依赖。
更有信心:更少担心工具链或 ECO 带来的细微错误。
质量更高:该技术可突出设计中不良的 RTL 编码。
更高的可预测性:减少遗漏错误的机会。
Logic & Sequence逻辑等价检查(LEC)通过观察设计的组合结构来确定两个替代实现的结构是否表现出相同的行为。序列等价性检查(SEC)将时序考虑在内,检查两个设计表示法在多个时钟周期内的等价性。
组合逻辑比较直白,核心就是关于布尔逻辑函数的化简并基于BDD进行结构上的等价性验证或者添加异或逻辑 ...
IEEE 754 二进制浮点数算术标准
什么是IEEE 754标准IEEE二进制浮点数算术标准(IEEE 754)是20世纪80年代以来最广泛使用的浮点数运算标准,为许多CPU与浮点运算器所采用。这个标准定义了表示浮点数的格式(包括负零-0)与反常值(denormal number),一些特殊数值(无穷∞与非数值NaN),以及这些数值的“浮点数运算符”。 常见的四种浮点数值表示方式:单精确度(32位)、双精确度(64位)、延伸单精确度(43比特以上,很少使用)与延伸双精确度(79比特以上,通常以80位实现)。C语言的float通常是指IEEE单精确度,而double是指双精确度。
标准的IEEE 754格式由三部分组成,符号位sign,指数项expoent,以及尾数部分mantissa,尾数对应的值为Fraction。
Exponent:32 位的情况下阶码 E 的取值范围为 8 bit,对应 32 位中的 2-9 位;64 位的情况下阶码E 的取值范围为 11bit,对应 64 位中的 2-12 位。以单精度浮点数为例,它的指数域为 8 bit,固定偏移值为 2^{8-1} - 1 = 127,IEEE754 约 ...
Hello World
Welcome to Hexo! This is your very first post. Check documentation for more info. If you get any problems when using Hexo, you can find the answer in troubleshooting or you can ask me on GitHub.
Quick StartCreate a new post1$ hexo new "My New Post"
More info: Writing
Run server1$ hexo server
More info: Server
Generate static files1$ hexo generate
More info: Generating
Deploy to remote sites1$ hexo deploy
More info: Deployment