山东大学团队在RISC-V中国峰会分享服务器生态标准化进展‌

7月16日，戴鸿君教授项目组工程师刘振参加RISC-V 中国峰会，并作为参会嘉宾在软件与生态分论坛与阿里达摩院联合做有关RISC-V Firmware 的技术分享。

中国峰会是全球三大RISC-V专业会展之一，也是中国规模最大的RISC-V年度活动，峰会由上海开放处理器产业创新中心（SOPIC）主办，线下举行了为期三天的会议和会展，吸引了一大批RISC-V 产业相关专家参加。

山东大学固件工程师刘振与合作伙伴阿里达摩院Evan Chai共同发布的《The Road to RISC-V Server Standardization:UEFI, Boot and Runtime Services》技术报告，分享了国内固件团队在RISC-V领域取得的进展和突破。

刘振在技术分享中首先做了社区固件现状的展示，主要包括：

·‌ratified标准

ACPI规范v6.6（高级配置与电源管理）新增RISC-V hart 和中断Table相关内容；

RISC-V SBI规范v3.0（特权架构接口）发布；

·‌开发中标准‌

BRS规范v0.9（Boot与Runtime Services）进入public review，即将发布1.0 版本；

Smmttspec 和Server Platform spec 在work inprogress阶段；

同时也展示了山东大学在RISC-V领域取得的进展，主要包括：

·与软件所合作推动BRS spec v1 版本的落地以及搭建BRS test suite；

·与阿里达摩院合作搭建了RISC-VplatformQemu 自动化实现平台；

·搭建了48台RISC-V 服务器的东山集群；

分享了基于UEFI boot 的固件模型及规范化验证模型图：

目前山东大学基于算能SG2042及SG2044服务器平台已经实现UEFI启动（EDK II适配）以及UEFI自认证测试(SCT)测试。在技术分享中，刘振也同步分享了现在山东大学在RISC-V UEFI SCT 测试的结果。并且展示了山东大学基于Qemu 平台的GitHub开源项目，该开源项目可以基于Qemu 环境实现RISC-V 的固件编译，Qemu 环境搭建以及UEFI boot 等等，并公开了开源仓库地址。刘振在第二部分的技术分享中，主要介绍了山东大学戴鸿君教授项目组SBI 形式化验证有关的内容：项目组搭建了全球首个形式化验证SBI固件‌——SeSBI，验证成果包含：

·完成模式切换、PMP、定时器等核心功能的形式化证明；

·建立从规范->代码->验证报告的完整形式化验证链；

‌技术分享中介绍了SBI 形式化验证的需求来源，介绍了形式化验证的数学模型和SBI 形式化验证模型闭环框图：

在技术分享中，刘振也对广大的RISC-V Platform 从业者和爱好者发出邀请，欢迎大家试用山东大学的RISC-V 服务器集群——东山集群，也欢迎大家体验github的开源qemu 平台，并提出宝贵意见。

图文：李冰