如何可靠、快速、自动地验证处理器硬件
你是否会遇到以下问题：bug可能比较微妙，不直观，无法手动推断；或者在被观察到之前就被激活很久了，传统的模拟设计需要花很长时间自动；验证工作量随着设计复杂性的增加而增加，人工推理和手动编写属性不再可行，等等。目前验证cpu的主流方法，如 hw testbench,
universal verification methodology (uvm),
sw testbench, property checking,
这些现有方法具有范围受限、仿真较慢、long bug traces、需要手动编写test的特点。
那么，如何可靠、快速、自动地验证处理器硬件，并且生成bug trace？
no.1
形式化验证的开展基于形式化规范和自动推理。其中形式化规范是指通过形式化语言将duv和待证明的属性建模成形式化模型，自动推理是指通过严格的数学方法来推导duv和待证明属性规范之间的逻辑关系，通常是证明duv的形式化模型能满足所有形式化属性规范。
形式化验证的基本步骤：
系统建模：把系统转换为能被模型检测工具所接受的形式。这是模型检测的首要步骤，构建系统模型时为了提高验证过程的效率及可行性需要将和要验证的属性无关的细节抽象掉，仅保留与此相关的细节，这是一个比较简单但通常会比较繁琐的过程。
形式化规范：在对模型进行验证之前以逻辑公式的形式给出待验证的属性。命题时态逻辑能够表达出系统的行为如何随着时间而发生变化，因而通常被用来描述规范。一条规范只是描述了系统某一个属性，一组规范是否覆盖了系统需要满足的所有属性一直是个开放问题。规范开发的人力投入也是长期困扰形式验证的问题。
形式化验证：模型检测工具对输入的模型的状态空间进行搜索来确定输入的规范是否为真，为真表示模型满足规范；为假则表示模型不满足规范，此时会给出一个反例来说明规范为假的原因。
no.2
qed（快速错误检测）是一种识别错误的方法（主要在处理器中，但也可用于其他组件），它将一组原始测试转换为qed检查。这涉及到将寄存器文件分成两部分，其中一半用于原始指令，另一半用于重复的指令序列，原始序列和复制序列都以相同的顺序执行相同的指令，但它们是交错的，在原始指令序列和复制指令序列完成后，寄存器文件的两部分应该匹配。
根据经验，与传统技术相比，这种方法可以将bug trace的长度减少多达6个数量级。
bounded model checking（bmc） 用于验证有限状态模型的正确性。它通过遍历有限长度的路径来检查模型是否满足给定的性质。
sqed基于bmc进行符号运算搜索所有指令序列组合。这为我们提供了一种无需编写测试就可以验证处理器的方法，也不需要提供任何手写属性，只依赖于sqed检查。是对传统的形式验证方法的突破。
no.3
基于sqed的指令集形式验证具有如下特点
全自动验证：symbolic instructions + self-consistency checking，不需要开发属性集。
高覆盖率：bmc工具搜索给定深度的所有指令序列。
最简bug复现：bmc工具自动生成从复位状态到bug site的最短路径。
借助avemc高性能形式验证平台，avemc/sqed组合为芯片设计指令集验证提供了全新的验证解决方案。
no.4
avemc在开源risc-v上的sqed验证过程: 给定risc-v核的rtl实现和isa spec，从isa spec中自动解析生成qed module（一个新的rtl），将原有的risc-v核和qed module连接起来。这里avemc就可以直接进行验证了。
指令集形式验证是芯片设计验证中的新兴方向，在riscv和ai/ml硬件加速芯片的验证中得到越来越广泛的应用。sqed是指令集形式验证领域的新兴工具，它通过完全自测试的特性解决了验证属性开发的低效和覆盖率问题。在上海阿卡思微电子技术有限公司形式验证平台avemc上，sqed得到了成功的实现。与开源形式验证工具相比，avemc/sqed不仅提升了验证速度，还能发现其他工具无法发现的bug。
上海阿卡思微电子技术有限公司由硅谷回国的资深电子设计自动化(eda)专家于2020年在上海张江高科技园区设立，旗下子公司成都奥卡思微电科技有限公司于2018年在成都高新区创立，公司聚集国际知名eda公司和芯片设计公司具有多年研发经验的尖端人才，基于形式化方法为逻辑芯片设计和工控软件等提供验证工具及咨询服务，凭借在形式化方法领域深厚的技术积累及深入的产品实践，公司已推出系列商用性能优异的验证工具，服务于复杂芯片设计及通用设计流程，获得多个标杆客户的采购使用。在研产品及应用包括高阶等价验证、功能安全等，覆盖数字信息、智能硬件、航空航天、人工智能等行业需求。公司将最新的eda技术与本土用户需求相结合，服务于中国集成电路自主可控设计；将产品开发与数字产业趋势相结合，服务于中国技术创新与技术赶超；将技术推广与产品优化相结合，服务于海内外需求市场。致力于成为国内领先的形式化技术开发与服务商。
SynQor电源模块UPS的特征
4项与工业机器人相关的新增国家推荐标准
区块链是一个怎样的安全体系，术语又有哪些
英途4D智能互动情景教学系统优势
物联网农场应用生态系统
如何可靠、快速、自动地验证处理器硬件
怎么设计一种基于RT-Thread和infineon开发板的智能家居系统？
2023最新：国产芯各领域龙头企业！（含传感器芯片）
多种处理器调度过程及调度算法
5G的标准是什么？主要技术实验的进程是怎样的？
简单介绍产品结构中的EMC设计
基于TDA1514的40W音频放大器电路图
中国两家大型智能手机制造商表示反对博通和高通公司的潜在合并交易
变电站接地电阻大小要求、不合格的危害和处理方法
澳柯玛空调故障代码
差压流量计的工作原理
TMS320C61416控制FPGA数据加载设计
振动测量应用实例
eBPF安全可观测性的前景展望
一种用于高能和长循环锂硫电池的极性氧化还原活性中间层新概念
universal verification methodology (uvm),
sw testbench, property checking,
这些现有方法具有范围受限、仿真较慢、long bug traces、需要手动编写test的特点。
那么，如何可靠、快速、自动地验证处理器硬件，并且生成bug trace？
no.1
形式化验证的开展基于形式化规范和自动推理。其中形式化规范是指通过形式化语言将duv和待证明的属性建模成形式化模型，自动推理是指通过严格的数学方法来推导duv和待证明属性规范之间的逻辑关系，通常是证明duv的形式化模型能满足所有形式化属性规范。
形式化验证的基本步骤：
系统建模：把系统转换为能被模型检测工具所接受的形式。这是模型检测的首要步骤，构建系统模型时为了提高验证过程的效率及可行性需要将和要验证的属性无关的细节抽象掉，仅保留与此相关的细节，这是一个比较简单但通常会比较繁琐的过程。
形式化规范：在对模型进行验证之前以逻辑公式的形式给出待验证的属性。命题时态逻辑能够表达出系统的行为如何随着时间而发生变化，因而通常被用来描述规范。一条规范只是描述了系统某一个属性，一组规范是否覆盖了系统需要满足的所有属性一直是个开放问题。规范开发的人力投入也是长期困扰形式验证的问题。
形式化验证：模型检测工具对输入的模型的状态空间进行搜索来确定输入的规范是否为真，为真表示模型满足规范；为假则表示模型不满足规范，此时会给出一个反例来说明规范为假的原因。
no.2
qed（快速错误检测）是一种识别错误的方法（主要在处理器中，但也可用于其他组件），它将一组原始测试转换为qed检查。这涉及到将寄存器文件分成两部分，其中一半用于原始指令，另一半用于重复的指令序列，原始序列和复制序列都以相同的顺序执行相同的指令，但它们是交错的，在原始指令序列和复制指令序列完成后，寄存器文件的两部分应该匹配。
根据经验，与传统技术相比，这种方法可以将bug trace的长度减少多达6个数量级。
bounded model checking（bmc） 用于验证有限状态模型的正确性。它通过遍历有限长度的路径来检查模型是否满足给定的性质。
sqed基于bmc进行符号运算搜索所有指令序列组合。这为我们提供了一种无需编写测试就可以验证处理器的方法，也不需要提供任何手写属性，只依赖于sqed检查。是对传统的形式验证方法的突破。
no.3
基于sqed的指令集形式验证具有如下特点
全自动验证：symbolic instructions + self-consistency checking，不需要开发属性集。
高覆盖率：bmc工具搜索给定深度的所有指令序列。
最简bug复现：bmc工具自动生成从复位状态到bug site的最短路径。
借助avemc高性能形式验证平台，avemc/sqed组合为芯片设计指令集验证提供了全新的验证解决方案。
no.4
avemc在开源risc-v上的sqed验证过程: 给定risc-v核的rtl实现和isa spec，从isa spec中自动解析生成qed module（一个新的rtl），将原有的risc-v核和qed module连接起来。这里avemc就可以直接进行验证了。
指令集形式验证是芯片设计验证中的新兴方向，在riscv和ai/ml硬件加速芯片的验证中得到越来越广泛的应用。sqed是指令集形式验证领域的新兴工具，它通过完全自测试的特性解决了验证属性开发的低效和覆盖率问题。在上海阿卡思微电子技术有限公司形式验证平台avemc上，sqed得到了成功的实现。与开源形式验证工具相比，avemc/sqed不仅提升了验证速度，还能发现其他工具无法发现的bug。
上海阿卡思微电子技术有限公司由硅谷回国的资深电子设计自动化(eda)专家于2020年在上海张江高科技园区设立，旗下子公司成都奥卡思微电科技有限公司于2018年在成都高新区创立，公司聚集国际知名eda公司和芯片设计公司具有多年研发经验的尖端人才，基于形式化方法为逻辑芯片设计和工控软件等提供验证工具及咨询服务，凭借在形式化方法领域深厚的技术积累及深入的产品实践，公司已推出系列商用性能优异的验证工具，服务于复杂芯片设计及通用设计流程，获得多个标杆客户的采购使用。在研产品及应用包括高阶等价验证、功能安全等，覆盖数字信息、智能硬件、航空航天、人工智能等行业需求。公司将最新的eda技术与本土用户需求相结合，服务于中国集成电路自主可控设计；将产品开发与数字产业趋势相结合，服务于中国技术创新与技术赶超；将技术推广与产品优化相结合，服务于海内外需求市场。致力于成为国内领先的形式化技术开发与服务商。
SynQor电源模块UPS的特征
4项与工业机器人相关的新增国家推荐标准
区块链是一个怎样的安全体系，术语又有哪些
英途4D智能互动情景教学系统优势
物联网农场应用生态系统
如何可靠、快速、自动地验证处理器硬件
怎么设计一种基于RT-Thread和infineon开发板的智能家居系统？
2023最新：国产芯各领域龙头企业！（含传感器芯片）
多种处理器调度过程及调度算法
5G的标准是什么？主要技术实验的进程是怎样的？
简单介绍产品结构中的EMC设计
基于TDA1514的40W音频放大器电路图
中国两家大型智能手机制造商表示反对博通和高通公司的潜在合并交易
变电站接地电阻大小要求、不合格的危害和处理方法
澳柯玛空调故障代码
差压流量计的工作原理
TMS320C61416控制FPGA数据加载设计
振动测量应用实例
eBPF安全可观测性的前景展望
一种用于高能和长循环锂硫电池的极性氧化还原活性中间层新概念