程序员经验分享-hwhale

CPU系统级验证——概览索引

2023-11-19

1. RISC-V CPU核指令集验证分析

1 wujian100

（1）SoC核分析

无剑100实际上是一款低功耗SoC，采用的CPU核是E902。

core通过AHB总线与Icache相连

（2）验证环境分析

通过 $readmemh("test.pat", temp_mem)将二进制文件读进工程。

通过Srec2vmem.py将某文件转化为某文件，为何转化尚未搞清。（判断S[1-9]是否跟某线程或某核有关？即某核只处理某类型的指令。）初步判断测试集为riscv-tests测试集。

2 bottlerocket

通过$readmemh({image,".hex"}, imem.mem)和$readmemh({image,".hex"}, dmem.mem)将bin文件读进工程

测试用例为riscv-tests中RV32ui和RV32mi测试集

3 rv32cpu

通过axi总线接入TEXT和DATA ram，但axi数据来源未知。

测试激励为src文件夹中的汇编文件，为指明测试激励集。

4 clarvi

在dual_port_bram模块中通过$readmemh(INIT_FILE, memory)将mem.hex读进工程。

测试用例为riscv-tests中RV32ui和RV32mi测试集

5 RI5CY

苏黎世联邦理工大学和波罗尼亚大学联合设计的一款小巧的4级流水线开源处理器，实现了RV32IC，以及RV32M中乘法指令mul，其目标是作为并行超低功耗处理器项目PULP（Parallel Ultra Low Power）的处理器核，所以RI5CY在RISC-V的基础上增加了许多扩展，包括硬件循环、乘累加、高级算术指令等。采用UMC的65nm工艺进行流片，RI5CY主频可以达到654MHz，动态功耗是17.5uW/MHz。采用SystemVerilog编写。

测试集有三种：

  1. RISCV tests   即riscv-tests。
  2. RISCV compliance tests  即指令集兼容性测试，共56个汇编文件，测试指令包括整数计算指令、存储器操作指令、控制跳转指令等。（该部分会做详细分析）
  3. firmware tests   固件测试。一个独立的测试用C代码。

6. openHW core-v系列

cv32e40p核分析：CPU设计——CPU核解析——cv32e40p_KGback的博客-CSDN博客

验证环境分析具体参见：CPU系统级验证——验证环境——OpenHW core-v验证环境及文件分析_riscv el2验证环境_KGback的博客-CSDN博客

7. LowRISC Ibex

参考链接：

2. 指令集验证（compliance test）

指令集验证主要是验证CPU对指令集的兼容性，即该CPU是否能准确无误的执行每条目标指令。

1 DUT仿真验证（simulation verification）

目前指令集验证均是编写测试激励对DUT和参考模型进行simulation，后对比结果。

  • 指令集验证的需求
  1. 能够使用操作数产生合法的基本整数运算指令
  2. 在指令执行完成后能够检查通用寄存器的状态
  3. 指令执行完成后能检查副效应，例如溢出等。
  • 指令集验证内容

指令集的验证需要验证工程师思考该指令需要测试的特征是什么，为了确保指令的正确执行需要检查的内容是什么，为了确保该特征被测试需要进行哪些激励和配置等。验证的充不充分取决于验证人员对CPU微架构的理解和风险应对能力。

（1）RISCV基本指令定向测试
设计出来的CPU首先需要兼容RISCV基本指令，即需要满足RISCV基本整数指令及相关标准指令集。

即risc-v兼容性测试，riscv-compliance工程主要由imperas公司维护，详细介绍见：RISC-V及RISC-V core compliance test简析 - 知乎

主要测试的内容有：

  1. 溢出检测及相关标志位
  2. 下溢检测及相关标志位
  3. 无指令执行的副效应，比如异常的通用处理寄存器变化，异常的条件代码
  4. 使用x0-x31作为rs1/rs2
  5. 使用x0-x31作为rd
  6. x0寄存器的值始终为0
  7. set/clear所有立即数的比特位
  8. set/clear源寄存器rs1/rs2的比特位
  9. 根据7/8两条set/clear目的寄存器rd的比特位

（2）自定义扩展指令定向测试

对于自定义扩展指令集的验证，该验证需要修改相关的工具链并通过相关测试验证工具链的修改成功，再进行（1）中的测试。

（3）随机约束测试

对进行大量的随机指令测试

  • 指令集验证激励的种类

指令集验证testcase基本分为以下几种：

  1. self check
  2. signature comparison (extension of self check)
  3. trace log comparison
  4. step and compare

代码执行模式主要有以下两种：

  1. 自检测试激励运行时按照源文件中指令顺序依次，并同时将指令执行结果和参考值作检查，若出错则程序跳转到fail，打断正常执行顺序，立即执行完成。类似的测试集有riscv-tests、riscv-compilance-tests等
  2. 预存测试激励运行时不会打断执行顺序，执行的结果会和指令集模拟器（ISS）的结果作对比，最终统计对比的结果。类似的测试集有riscv-dv等
  • 指令集验证pass/fail的标志

测试的pass/fail与上述激励的种类有关

  1. self checking：自检性质的测试激励在每条指令执行时就会同时将结果和参考值作对比，若失败则跳转到fail
  2. signature check：特征检查，相对自检来说更加复杂深入。测试的结果将被用来计算该指令的某个特征，这将会和预先确定好的较标准特征作对比。采用该检查的为riscv-complience-tests。
  3. check against ISS：与指令集模拟器对比检查。该情况下，testcase并不知道测试的参考值，仅仅给DUT提供激励，testbench会对比DUT和ISS的输出结果确定测试的pass/fail。该检查较被经常使用，因为它是的testcase更加简单。采用该检查的如riscv-dv
  4. check against RM：与参考模型对比检查，该检查方式与第三点类似，但相对ISS更加通用。通常用作ISS检测的补充。
  5. assertion check：通过断言判断是否执行出错。

2 形式化验证（Formal verification）

系统级验证中的形式化验证是近期较流行的一种验证方式，它是可以在simulation之前做的验证，在芯片设计流程通常处于CPU的RTL代码尚未设计好的阶段，此外，在simulation进行的同时，同样可以采用形式化验证并行工作，两种验证方法的feature做互补。

  • 指令集描述语言——sail

sail是REMS构建的一种描述指令集的语言，可以认为是一种机器可读的形式化ISA模型。REMS是英国的一家学术组织，该组织已构建出RV32IMAC和RV64IMAC指令集的sail model，链接见上。

riscv基金会有意用其来描述RISCV指令集。

初步来看，sail可以用来形式化testbench断言的参考模型，这些assertion可以根据sail spec来验证基于RISCV ISA的某微架构。目前该领域OneSpin GapFree已经在sail model和RTL代码间做了可比性的check，该公司仍在探索如何充分使用sail model

SAIL模型的优点在于它可以与RISC-V ISA相同的方式进行扩展。然后对core执行formal验证，以创建一组SystemVerilog断言，然后将其用于对RTL进行formal验证。通过比较RTL的断言进行formal验证的工具是专有工具，并且用于执行此操作的技术将是每个供应商专有的。

该语言将持续关注。

3. 系统功能验证

很明显，单单的compliance测试是远远不够的，compliance测试只是在验证指令执行的正确性，但是CPU中的debug功能，interrupt功能，异常检测等却没有验证。

此时应该做的是：

  1. 分析验证计划，扩充testcase

4. 验证生态

1 验证工具

  • Risc-v verification APP (Onespin)

该解决方案的核心是使用OneSpin的断言设置方法将risc-v指令集形式化位一种systemverilog断言，该方法可以产生一种高性能、非重叠的断言，从而以一种纯粹优雅的方式来捕捉端到端的转换和需求，具体是：

  1. 将功能需求转换位一种形式化的可仿真执行的形式
  2. 捕捉完整的电路信号变化，类似于时序图
  3. 通过高级的易于复查的断言来获取100%的功能覆盖率
  4. 将特定于实现的支持验证代码与可重用规范级代码清晰地分离开来
  5. 使用OneSpin的GapFreeVerification进一步利用断言集用于自动检测规范遗漏和错误、验证计划中的漏洞和未验证的RTL函数

2. 测试用例

  • benchmark测试

1. IO测试

Benchmark测试——fio_KGback的博客-CSDN博客

Benchmark测试——IOzone_iozone测试结果分析_KGback的博客-CSDN博客

Benchmark测试——Unixbench 2D测试和x11perf_KGback的博客-CSDN博客

网卡netperf测试：https://www.cnblogs.com/xieshengsen/p/6493277.html

https://www.cnblogs.com/davidesun/p/12726006.html

2. CPU性能测试

UnixBench：UnixBench的实现介绍-阿里云开发者社区

CPU2006: 测试工具（spec2006及Lmbench）讲解及数据分析_specint2006_GLL_的博客-CSDN博客

常见CPU benchmark的测试报告：实测一些CPU得到的原始测试报告

3. 验证相关文章

  1. semiconductor Engineering: Components For Open-Source Verification
    链接：Components For Open-Source Verification

本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

CPU系统级验证

CPU系统级验证——概览索引 的相关文章

  • （手工）【sqli-labs32-38】宽字节注入、报错回显、字符/数字型注入

    目录 一 推荐 二 手工 SQL注入基本步骤 三 Less32 GET Bypass custom filter adding slashes to dangerous chars 3 1 简介 宽字节注入 报错回显 字符型注入 3 2 第

  • JVM简介说明

    转自 JVM简介说明 下文笔者讲述JVM的简介说明 如下所示 JVM简介 JVM的功能是Java应用程序的运行环境 它是Java虚拟机 JVM用于运行java的字节码文件 JVM可以将字节码转换为硬件 操作系统指令 JVM用于同操作系统内层

  • 【HJ31】 单词倒排

    题目描述 对字符串中的所有单词进行倒排 说明 1 构成单词的字符只有26个大写或小写英文字母 2 非构成单词的字符均视为单词间隔符 3 要求倒排后的单词间隔符以一个空格表示 如果原字符串中相邻单词间有多个间隔符时 倒排转换后也只允许出现一个

  • ubuntu 串口助手通信收发数据不一致

    文章目录 问题背景 一 解决方案 1 直接更换硬件 靠这个解决的 2 其他参考 总结 问题背景 主机1 win10笔记本电脑 主机2 ubuntu16 04的宸曜工控机 主机3 ubuntu14 04的一个小盒子 串口助手 cutecom

  • pmd java规则_静态代码扫描 (一)——PMD 自定义规则入门

    阅读该文章前 最好已经对 PMD 有了初步的认识和了解 可参考静态分析工具 PMD 使用说明 准备工作 首先在PMD 官网下载最新版本的文件 目前最新版本是 5 4 1 下载 pmd bin 5 4 1 zip 和 pmd src 5 4

  • QT串口助手的实现

    serial c include serial h include ui serial h serial serial QWidget parent QWidget parent ui new Ui serial ui gt setupUi

  • 【数据库】MySQL三大日志：binlog、redo log和undo log

    MySQL三大日志 binlog redo log和undo log 日志是mysql数据库的重要组成部分 记录着数据库运行期间各种状态信息 mysql日志主要包括错误日志 查询日志 慢查询日志 事务日志 二进制日志几大类 作为开发 我们重

  • 土壤含水量仪的监测方法

    土壤含水量监测仪对土壤内部水分含量情况进行监测 可实现对灾害隐患点土壤含水量的长期实时监测 仪器主机采用低功耗设计 工作功耗可达毫瓦级 根据滑坡隐患点的特点 仪器主机采用多通道设计 可根据实际情况接驳1 4路土壤含水量传感器对监测点不同深度

  • Python安全攻防之第二章Python语言基础

    2 3 Python模块的安装与使用 python模块的安装 pip3 install 模块名称 py 3 m pip install 模块名称 python模块的导入与使用 1 Import模块名称 采用 Import模块名称 方式时 需

  • Shell中的算术运算

    let expr bc都是在Bash shell环境中进行数学运算时我们会用到的工具 一 整数运算 let 当使用let时 变量名之前不能再添加 用法 var1 2 var2 3 let result var1 var2 echo resu

  • 一文搞懂积分不等式证明(积分证明题总结笔记3/3)

    积分证明题是考研中难度较大的板块 很多学弟学妹们希望我出一篇总结文章 故作本文 希望对大家有所帮助 本文所涉及题目 均是来自市面上常见题册 李林880 张宇1000题 汤家凤1800等 由于内容较多 故分为三部分 等式证明 点击进入 由积分

  • Qt 绘图设备，QPixmap 和QImage 相互转化

    Qt的绘图系统允许使用相同的API在屏幕和其他打印设备上进行绘制 整个绘图系统基于 QPainter QPainterDevice 和 QPaintEngine三个类 QPainter用来执行绘制的操作 QPaintDevice是一个二维空

  • ospf和mgre的综合应用

    1 R6为ISP只能配置IP地址 R1 R5的环回为私有网段 首先划分好IP地址 如下图所示 然后对各个环回和接口进行IP配置 如下面所示 对r1 r1 int l0 r1 LoopBack0 ip add 192 168 1 1 24 r

  • Mybatis-plus查看完整执行sql

    Mybatis plus查看完整执行sql application properties 文件 mybatis plus configuration log impl org apache ibatis logging stdout Std

  • Redis-Sentinel（哨兵模式），看这篇就够了哦

    文章目录 简介 启动并初始化Sentinel 初始化Sentinel服务器 替换普通Redis代码为Sentinel的专用代码 初始化 Sentinel 状态 初始化Sentinel监视的主服务器列表 创建连向主服务器的网络连接 获取主服务

  • 二进制兼容与Qt的D指针

    二进制兼容的定义 一个连接到旧版本的动态库的应用程序 无需重新编译就可以用新版本的动态库运行 则这个库被认为是二进制兼容的 一个连接到旧版本的动态库的应用程序 无需修改源码单需要重新编译后可以用新版本的动态库运行 则这个库被认为是源码兼容的

  • java版spring cloud+spring boot 直播电商 社交电子商务平台

    涉及平台 平台管理 包含自营店面 商家端 PC端 手机端 买家平台 PC端 H5 公众号 小程序 APP端 IOS Android 微服务 核心思想 分布式 微服务 云架构 模块化 原子化 持续集成 集群部署 开发模式 代码生成工具 驱动式

  • 【Java 数据结构】单链表与OJ题

    篮球哥温馨提示 编程的同时不要忘记锻炼哦 暮色降临 冲一杯咖啡 目录 1 什么是链表 2 实现一个单向非循环链表 2 1 实现前的约定 2 2 addFirst 方法 2 3 addList 方法 2 4 addIndex 方法 2 5 c

  • SpringBoot 集成积木报表

    前言 积木报表是jeecg的一款开源但代码不开源的一款自定义报表 可以基于 网页灵活调整报表的布局 样式等内容 无需编程 专为企业数据分析 报表制作而设计 降低管理人员汇总制作报表的门槛 解决各类日常管理和 汇报的难题 但是因为代码不开源所

随机推荐

  • SQL 入门的必读好书

    点击蓝色 有关SQL 关注我哟 加个 星标 天天与10000人一起快乐成长 最近 很多朋友来问我 有没有入门 SQL 的好书 与这些朋友聊天发现 大部分人都没有系统学过计算机专业的专修课 有从物流转行的 有从会计专业扩展的 还有从运维行业转

  • 出现“java.sql.SQLException: 无法转换为内部表示”解决方法

    现在 java sql SQLException 无法转换为内部表示 很可能是因为数据库某字段的类型出错了 比如程序将某字段当做Integer类型 而数据库存储又使用另外一种类型 不如String 建议出现这样问题的同行们认真检查一下代码

  • 软件配置管理

    第一章 1 软件配置管理用于控制变化 2 软件配置管理 Software Configuration Management SCM 是指一套管理软件开发和维护过程中所产生的各种中间软件产品的方法和规则 它是控制软件系统演变的学科 3 软件配

  • java8之lambda表达式

    java8 近期 在一个不完全的统计中 java8的普及率已经到达了近80 图 1 相比之前的java版本 下面两个是java8出现带来最大的影响 其一是极大地简化了代码的复杂度尤其是在处理集合以及接口这两个方面 除此之外 java8引入了

  • Linux系统FTP传输协议

    目录 一 FTP传输协议 什么是FTP传输协议 FTP数据连接的两种方式 二 如何使用FTP传输协议 三 设置黑白名单 设置黑名单 设置白名单 一 FTP传输协议 什么是FTP传输协议 FTP协议 文件传输协议 网络上控制文件传输的双向性

  • 中国央行数字货币或比Libra更早发行，考虑让非政府机构参与试点

    中国官员和专家们表示 中国正在测试推出中国首款央行数字货币 CBDC 的多种方式 他们预计私营机构将更多地参与创造政府支持的货币 基于一些领域正在进行的试验 引入 CBDC 的时机已经接近成熟 但与中国央行关系密切的专家们周一表示 Face

  • 区块链教育应用案例_区块链技术在教育领域中的应用研究

    来源 廊坊云报 廊坊日报讯教育对一个国家来说意味着希望 教育行业数字的应用是各行各业发展的基础 只有通过完善的教育体系 才能培育出更加优秀的人才来输送到各个行业 所以说教育领域是一个重要领域 其他重要领域的未来 包括科学 医学 农业 工业和

  • 华为hilens 系统制作

    恢复出厂设置 https support huawei com enterprise zh doc EDOC1100112066 9b0a1fba 长按RST按钮2 3秒 在这个过程中 短按电源按钮后松开 当前面板健康指示灯出现橙色 常亮

  • Debian 12 发布，迄今为止最佳 Linux 版本

    Debian 项目今天发布了 Debian 12 Bookworm 操作系统的最终版本 这是一个重大发布 带来了几个新功能 更新的组件和许多改进 凭借其长期稳定和安全的历史 Debian 12 备受全球开源爱好者的热切期待 这个新版本带来了

  • 图书馆管理系统开发(C# && Sql Server)

    图书馆管理系统 C S架构软件 开发 主要步骤 遇见问题 1 主要步骤 1 1 学习主干知识 大概懂得数据库相关sql语法 大概懂得C 语法 C 菜鸟教程 把基础篇看看 大概掌握 Net开发窗口界面 Net教程 然后可以实战一下项目 VS2

  • 将嘉立创中元件导出为AD封装库使用

    AD封装库的选择和元件的查找实在让人头大 我们不妨使用好嘉立创提供的丰富元器件库 如果想要找到想要的元件 可以直接去嘉立创EDA 标准版 的元件库中寻找 在符号类型中可以找到原理图文件 很奇怪 在嘉立创商城中直接搜索的话元器件会比在嘉立创E

  • python列表输出去掉引号_如何从导出的python列表中删除逗号、引号和圆括号？

    你们帮了我最后一个新手的忙 所以我想我会再问一次 现在 我的Python 3代码从CSV文件中获取数据 将数据存储为列表 创建该数据的排列 并以列格式将其导出回新的CSV文件 不幸的是 导出列表的格式不适合我的需要 我的问题是 如何在pyt

  • vue3.0项目报错：删除node包重新装报错

    前言 vue3 0的项目删除node包以后重新装项目 会报错 vue loader v16 找不到 安装以后下次再删包 再装会报错webpack的问题 解决办法 在新建项目后 打开pack json文件 找到 devDependencies

  • 【积累】Element-ui，el-dialog里面嵌入el-form，resetFields失效问题

    记一次element ui el dialog里面嵌入el form 使用resetFields方法初始化表单失效 问题记录 前提 当el form在一个el dialog中 dialog显示与否绑定变量 showDialog ref 为

  • 用DC-DC 升压降压以及产生负电压的原理及应用

    文章目录 前言 一 Boost和Buck电路 二 实际使用 1 DC DC芯片 2 DC DC芯片产生负电压 前言 在设计电源电路时经常会用到升压降压和负电压等电路 博主结合理论知识和实际应用加上自己理解 分享这篇文章 一 Boost和Bu

  • 设置无线路由器与有线网络在同一网段

    公司有两台路由器 一台连接internet的大路由器 一台无线路由器 两台路由器不在同一网段 所以无法实现互联互通 在一个局域网中很不方便 原设置 无线路由器的WAN口连接到大路由器上 插网线 无线路由器的WAN IP设置与大路由器一个网段

  • 【微信小程序】wx.request出现undefined

    偶现 天啦噜 一直困惑了很久的bug终于找到原因了 示例代码如下 wx request sucess function res if res statusCode 200 res data status 200 do something e

  • csdn中使用KaTeX给公式编号

    说明 csdn用的公式编辑器是Katex 并不是LaTeX 两者语法有些区别 比如LaTeX中的公式编号 begin equation 在KateX中就会解析错误 katex中 给公式编号用 tag 1 的形式 例如 E mc 2 tag

  • 【Threejs效果：挖空几何体】ThreeBSP实现墙体挖洞

    1 效果如下 2 代码如下 基本思路 1 创建两个mesh 一个墙体 一个窗户 2 然后取墙体和窗户的差集 将差集转换成几何体 3 根据几何体新建mesh 并贴纹理 依赖库有三个 import as THREE from three imp

  • CPU系统级验证——概览索引

    1 RISC V CPU核指令集验证分析 1 wujian100 1 SoC核分析 无剑100实际上是一款低功耗SoC 采用的CPU核是E902 core通过AHB总线与Icache相连 2 验证环境分析 通过 readmemh test

热门标签