面向处理器功能验证的硬件化SystemVerilog断言设计

张子卿; 石侃; 徐烁翔; 王梁辉; 包云岗

doi:10.7544/issn1000-1239.202331003

面向处理器功能验证的硬件化SystemVerilog断言设计

张子卿^{1, 2,},
石侃^{1, 2, ,},
徐烁翔³,
王梁辉⁴,
包云岗^{1, 2}

1.
处理器芯片全国重点实验室（中国科学院计算技术研究所）　北京　100190
2.
中国科学院大学计算机科学与技术学院　北京　100049
3.
上海科技大学信息科学与技术学院　上海　201210
4.
中国科学技术大学计算机科学与技术学院　合肥　230027

基金项目: 国家重点研发计划项目（2023YFB4405105）；中国科学院计算技术研究所创新项目（E261100）；国家自然科学基金重大项目（62090023）

详细信息

作者简介:
张子卿: 2002年生. 博士研究生. 主要研究方向为FPGA、芯片验证、计算机体系结构

石侃: 1988年生，博士，副研究员，主要研究方向为处理器芯片敏捷设计与验证，FPGA、计算机体系结构

徐烁翔: 1999年生. 硕士研究生. 主要研究方向为FPGA、敏捷芯片设计与验证

王梁辉: 2000年生. 硕士研究生. 主要研究方向为FPGA、芯片设计与验证

包云岗: 1980 年生. 博士，研究员. 主要研究方向为数据中心体系结构、处理器芯片敏捷设计方法论、开源处理器芯片生态

通讯作者:
石侃（shikan@ict.ac.cn）

中图分类号: TP391
计量
- 文章访问数: 335
- HTML全文浏览量: 120
- PDF下载量: 92
出版历程
- 收稿日期: 2023-12-13
- 修回日期: 2024-03-21
- 网络出版日期: 2024-04-14
- 刊出日期: 2024-05-31

Design of SystemVerilog Assertions Hardware Towards Efficient Processor Functional Verification

Zhang Ziqing^{1, 2,},
Shi Kan^{1, 2, ,},
Xu Shuoxiang³,
Wang Lianghui⁴,
Bao Yungang^{1, 2}

1.
State Key Lab of Processors (Institute of Computing Technology, Chinese Academy of Sciences), Beijing 100190
2.
School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing 100049
3.
School of Information Science and Technology, Shanghaitech University, Shanghai 201210
4.
School of Computer Science and Technology, University of Science and Technology of China, Hefei 230027

Funds: This work was supported by the National Key Research and development Program of China (2023YFB4405105), the Innovation Project of Institute of Computing Technology, Chinese Academy of Sciences (E261100), and the Major Program of the National Natural Science Foundation of China (62090023).

More Information

Author Bio:
Zhang Ziqing: born in 2002. PhD candidate. His main research interests include FPGA, chip verification, and computer architecture

Shi Kan: born in 1988. PhD, associate professor. His main research interests include agile chip design and verification, FPGA, and computer architecture

Xu Shuoxiang: born in 1999. Master candidate. His main research interests include FPGA, and agile chip design and verification

Wang Lianghui: born in 2000. Master candidate. His main research interests include FPGA, and chip design and verification

Bao Yungang: born in 1980. PhD, professor. His main research interests include data-center architecture, agile design methodology of processor chips, and ecosystem of open-source processor chips

摘要

摘要:
功能验证在处理器芯片开发流程中所占用的时间超过70%，因此优化提升功能验证环节的效率非常必要. 软件仿真等传统验证方法提供了包括断言等多种验证机制，以提升验证的细粒度可见性和自检查能力，但是软件仿真运行速度较慢，在高效性方面有明显不足. 基于FPGA的硬件原型验证方法能极大地加速验证性能，但其调试能力较弱，虽能快速发现漏洞，但难以定位漏洞出现的具体位置和根本原因，存在有效性不足难题. 为同时解决上述功能验证有效性与高效性的问题，提出一种将不可综合的断言语言SVA（SystemVerilog Assertion）自动转换成逻辑等效但可综合的RTL电路的方法，聚焦于断言这一类对设计进行非全局建模、纵向贯穿各抽象层级的验证方式，对基于全局指令集架构（instruction set architecture, ISA）模型的验证能力进行补足. 同时，结合FPGA细粒度并行化、高度可扩展的优势，对处理器的验证过程进行硬件加速，提升了处理器的开发效率. 实现了一个端到端的硬件断言平台，集成对SVA进行硬件化的完整工具链，并统计运行在FPGA上的硬件化断言的触发和覆盖率情况. 实验表明，和软件仿真相比，所提方法能取得超过2万倍的验证效率提升.
- 断言 /
- 处理器验证 /
- 硬件仿真 /
- 现场可编程逻辑门阵列 /
- 原型验证
Abstract:
Processor verification occupies more than 70% of the time in the processor development flow, so it is necessary to optimize the efficiency of the processor verification process. Traditional verification methods such as software simulation provide various verification mechanisms including assertions to improve the fine-grained visibility and self-checking capability of verification, but software simulation runs slowly and lacks in efficiency. FPGA-based hardware simulation acceleration methods can greatly improve the verification performance, but debugging ability is weak, and it is difficult to locate the specific location and cause of vulnerabilities. In order to solve the above problems of verification efficiency and effectiveness, we propose a method to automatically convert non-synthesizable SystemVerilog Assertion (SVA) into logically equivalent but synthesizable RTL circuits, focusing on assertions, which is a type of non-global modeling of the design, and vertically penetrates through the various levels of abstraction, and complements the verification capability of the global ISA-based model, which can be used to verify the design. Our method complements the global ISA model-based verification capability. At the same time, combined with the advantages of FPGA fine-grained parallelization and high scalability, the verification process of the processor is hardware-accelerated, which improves the development efficiency of the processor. In this paper, we implement an end-to-end hardware assertion platform, integrate a complete toolchain for hardware-enabling SVAs, and count the triggering and coverage of hardware-enabled assertions running on FPGAs. Experiments show that the proposed method achieves more than 20000 times verification efficiency improvement compared with software simulation.
- assertion /
- processor verification /
- hardware simulation /
- FPGA /
- prototyping

HTML全文

传统联盟链通过PBFT^[1]，RAFT^[2]，DIEM^[3]等拜占庭容错协议保证共识正常进行， $n\ge 3f+ 1$ 是保证共识协议能够正常运行的必要条件^[4-5]. 若异常节点f数量较多，采用轮换机制选举leader的方法会使视图更替变得频繁，为了改善其性能，RE-PBFT^[6]，PROOF-OF-REPUTATION^[7]，WRBFT^[8]等共识算法引入了节点信誉计算机制^[9]作为节点的性能指标，信誉越高的节点会获得更高当选leader的机会. 虽然这些评判机制可以避免异常节点多次当选leader节点，但异常节点依然存在于共识群组当中，若此时f因为不可控因素变为 $f+1$ ，节点总数 $n=3f+1$ ，将无法满足拜占庭容错的最低条件，共识的进程无法得到保障. 如所示，目前的解决方案需要人为更换异常节点，将异常节点从共识群组中剔除，以消除 $f > \dfrac{n-1}{3}$ 的可能性.

图 1 传统区块链管理模式

Figure 1. Management mode of traditional blockchain

下载: 全尺寸图片幻灯片

如图2所示，随着区块链规模增大，出现了多链系统^[10]以处理不同的业务^[11-12]，节点规模动辄成百上千，节点来源也从封闭式的单位局域网变成更加开放的云环境，信誉值共识算法在面对异常节点出现的情况时，封闭式的手动替换节点需要终止共识、同步区块状态等，会消耗大量时间，相比于节点可以随意加入或离开的公有链，其开放能力还有差距^[13]. 另一方面，基于信誉的共识算法，其共识节点数量相对比较固定，并未考虑根据交易量进行调整，存在极大的浪费，难以达到最优化的区块链性能.

图 2 大规模许可区块链多链管理模式

Figure 2. Multi-chain management mode of large-scale permissioned blockchain

下载: 全尺寸图片幻灯片

本文改善现有的信誉值机制，提出了新的多链共识机制MC-RHotStuff. 其不仅能够选择性能最佳的节点当选leader，还能标记异常节点，随后用自动的节点替换机制将异常节点替换掉；并且，共识群组的规模是可以根据交易量变化的，使区块链系统始终保持最佳的状态. 为了实现上述功能，每个节点都应被赋予不同的角色，节点根据不同的角色被划分为共识节点和备选节点，当共识节点异常时，备选节点可以替换异常节点成为新的共识节点，且不干扰正常的共识进程，不会因为节点的替换而导致系统重启.

本文的主要贡献包括3个方面：

1）引入多角色节点概念，不同角色的节点负责不同区块链上的不同任务，增强对大规模多链联盟链管理的能力.

2）引入适用于大规模多链联盟链环境下节点自动替换功能的信誉机制，解决共识群组存在异常节点的问题，保证节点的活性，避免因为存在拜占庭节点而导致效率低下.

3）引入节点动态调整方法，可以灵活地根据交易量改变共识群组的成员及节点数量，避免计算资源的浪费.

1. 相关工作

1.1 信誉值无关的共识算法

信誉值无关的共识算法多指通过轮转或其他特殊选择方法选择节点当选leader节点的共识算法，主要代表有PBFT，Sbft^[14]，HotStuff^[15]等部分同步共识算法^[16]，只有在GST^[17]之后，才能确保同步.

即使只计算数字签名或消息验证码^[18]，在PBFT中传递一个新的区块也有 $O({n}^{2})$ 的通信开销， $n$ 为工作链节点数量. 如果在决定达成之前发生视图更改，则传输开销变为 $O({n}^{3})$ . SBFT引入门限签名^[19]后，可以将视图更改的开销降为 $O({n}^{2})$ . 尽管如此，在多链环境下，交易需要通过协作链分流到不同的工作链中处理^[20]，此部分的通信开销为 $O\left(n\right)$ ，完成交易共识后，工作链节点会向协作链节点广播新区块，此时的通信开销为 $O\left(nm\right)$ ， $m$ 为协作链节点数量，则完成1笔交易总的通信开销为 $O(n+{n}^{2}+nm)$ ，若采用PBFT的最差情况下出现视图更替，总体的开销将达到立方数量级.

HotStuff引入门限签名技术，将节点广播投票改成leader节点来收集投票然后再广播，从而将通信的复杂度从 $O({n}^{2})$ 降低为 $O\left(n\right)$ ，即使出现视图更改的情况，其最大通信开销也仅为 $O({n}^{2})$ . 因此，在正常情况下，多链共识的通信开销仅为 $O(2n+nm)$ ，若能合理地控制 $m$ 的数量，使得 $m \ll n$ ，多链共识的通信成本可控制在常量级.

Boneh等人^[21]在2004年提出的BLS12加密算法是一种可以实现签名聚合和密钥聚合的算法，它不需要随机数生成器，可以将区块中的所有签名聚合成1个，容易实现 $m-n$ 多重签名^[22]，也可以避免签名者之间的多余通信，从而进一步降低通信成本.

即便如此，拜占庭节点带来的代价仍需进一步降低，大量研究者开始考虑基于信誉值的共识算法.

1.2 信誉值共识算法

信誉值共识算法是通过信誉值来衡量一个节点性能的指标，可以选举信誉值高的节点作为leader节点，用来降低共识成本，提升共识性能.

在RE-PBFT共识算法中，节点在共识的过程中记录其他节点的行为，共识结束后，节点将行为记录表发送到智能合约，智能合约根据每个节点的行为修改每个节点的信誉值，并将该信誉值发送给每个节点，节点根据更新后的信誉值选择信誉值最高的节点当选新的leader节点.

PROOF-OF-REPUTATION的信誉值计算过程与RE-PBFT类似，也是通过共识过程中节点的交互进行信誉值的计算，但与此不同的是，leader的选举不再以最高信誉值为准，而是为每个节点分配1个权重，该权重为该节点信誉值占整体信誉值的比重，随后采用随机算法，随机挑选一个节点作为leader节点.

WRBFT引入了不同角色的节点，共识群组中节点分为高信誉节点和低信誉节点，尽管每个节点都参与共识，但只要高信誉节点中超过阈值的节点对提议达成共识，共识就算成功，这使得共识群组具有可以容纳超过f个拜占庭节点的能力.

尽管有很多的节点信誉评判机制来衡量节点的行为，但它们都是针对当前共识群组而设的，异常节点还是存在于共识群组当中，这使得异常节点仍然可以参与共识，增加了共识失败的风险.

如何安全替换异常节点以确保共识正常运行，是亟需解决的问题，本文提出面向多链基于信誉的共识机制MC-RHotStuff，解决共识群组存在异常节点的问题，保证节点的活性，避免因为存在拜占庭节点而导致的效率低下. 同时支持动态调整共识节点数量：一方面是为了在吞吐量需求大的情况下提升共识性能，避免计算资源的浪费；另一方面，在吞吐量需求不大的情况下，适当增加节点的数量，在不影响交易正常执行的情况下，提高筛选异常节点的速度，使共识群组的网络环境更加安全，不会因为存在过多异常节点而导致共识的失败.

1.3 节点多角色划分

目前已经有许多研究将区块链的节点划分为多种不同的角色，并执行不同的任务. 例如Hyperledger Fabric支持多类节点角色，Orderers节点负责提供共识服务，Peers负责担任背书或记账服务，Comitters负责检查交易的合法性，最终将交易提交到区块链中. Hyperledger Fabric的角色划分目的是为了更好地推进共识，但是，如果某类节点发生了较多的故障，共识可能会因此收到很大的影响. 而本文的角色划分则更注重于解决此类问题，MC-RHotStuff将节点划分为备选节点和共识节点，若将 MC-RHotStuff的思想运用到Hyperledger Fabric中，将体现为处于共识的节点和处于备选的节点，MC-RHotStuff将实时监控正在共识的节点，一旦其性能与正常节点不匹配，就会启用处于后备队列的节点顶替它执行共识任务.

WRBFT也引入了备选节点的概念用于解决共识节点性能低的问题，但与本文思路不同的是，WRBFT的备选节点和共识节点都是存在于共识群组当中的，一旦创建其网络结构就不会发生改变，节点没有动态地加入和删除过程，节点群组不会发生变化，每轮共识根据其性能的反馈来选择部分节点作为共识节点使用，但不论如何选择，节点池的构成并没有发生变化. 而本文实现了节点的动态加入和删除，一旦共识节点的性能达不到要求，就会被备选节点所替代，并且被替代的节点将会被踢出节点池，而备选节点组中会源源不断地有新的节点加入，这保证了共识节点不是在原有的节点池中选择相对较好的节点，而是在不断更新的节点池中选择最优性能的节点，性能提升相比WRBFT会更多.

2. MC-RHotStuff系统框架

本节将详细介绍MC-RHotStuff的系统构成以及事务处理、节点准入、节点动态调整MC-Schedule流程，并阐述节点信誉值计算及筛选算法MC-Scan、节点状态同步算法MC-Syn是如何实现的.

2.1 节点角色划分

如图3所示，本文将节点划分为待准入节点、工作链备选节点、工作链共识节点、协作链共识节点4类节点. 待准入节点为某个云服务器中尚未加入区块链的节点^[23]，它无法参与共识；若待准入节点通过协作链共识节点审核^[24]并获得相应证书后^[25]，其身份会变为工作链备选节点，并隶属于某个工作链当中. 本文规定，每个工作链上的备选节点个数 $M= \dfrac{N-1}{3}$ ，N为当前共识节点的个数，当该链上备选节点个数超过M时则停止为该链分配备选节点，若每个链都具备M个备选节点时，则停止节点的准入. 工作链共识节点为参与当前区块链共识的节点，它可以产生区块、处理交易、评判其他共识节点，当其信誉值过低时，会被备选节点替换. 协作链共识节点不具备信誉值，采用传统的共识算法进行共识.

图 3 节点角色划分

Figure 3. Node role division

下载: 全尺寸图片幻灯片

为了更好地区分，本文将节点的身份用符号来表示：

${C}_{i}$ 表示当前节点为待准入节点， $i$ 为当前第 $i$ 待准入节点；

${N}_{i}$ 表示当前节点为协作链共识节点， $i$ 为当前第 $i$ 协作链共识节点，注意协作链不存在备选节点；

${W}_{j}. {A}_{i}$ 表示当前第 $j$ 工作链上第 $i$ 备选节点；

${W}_{j}. {N}_{i}$ 表示当前第 $j$ 工作链上第 $i$ 共识节点.

2.2 系统概述

如图4所示，本文的多链架构分为工作链和协作链的形式，协作链分流客户端发来的交易，将不同的事务划分到不同的工作链进行处理.

图 4 MC-RHotStuff系统框架

Figure 4. MC-RHotStuff system framework

下载: 全尺寸图片幻灯片

协作链上的共识节点负责监视每条工作链的瞬时交易量，若发现交易量较之前改变较大，就会在协作链上发起新一轮共识，这与工作链的交易共识不同，其目的是改变当前工作链上的节点数量来满足吞吐量的需求. 当有新的待准入节点申请准入时，协作链节点也会发起一轮新的共识，目的是审核待准入节点，当共识达成后，待准入节点将会获得准入证书并被分配到工作链的节点池中，协作链节点会将该准入节点加入到自身维护的节点列表中，列表记录了所有工作链节点，包括它们属于哪个工作链、目前属于什么角色，此外，协作链节点会将新节点的状态同步给相应的工作链节点，目的是当新节点加入后，保证协作链和工作链节点状态一致.

工作链共识节点将新交易打包成新区块，随后进行交易共识，当共识完成后，工作链节点首先会更新本地区块链状态，其次会发送该区块到协作链，协作链通过区块可以同步该工作链上节点和区块链的最新状态，当发生节点替换时，协作链没法通过产生的新区块获得最新的工作链节点状态，这时，工作链会采用节点状态同步算法MC-Syn将节点状态同步给协作链.

协作链采用基本的HotStuff算法运行，为了更好地提升工作链性能，区别于传统的信誉激励机制，本文通过信誉机制的评判实现2个目标：一方面将信誉值最高的工作链共识节点作为leader发起新一轮的共识；另一方面，将信誉值作为离群因素，通过聚类算法筛选出信誉值低（离群因素过大）的工作链节点，并将其判定为异常的共识节点，然后该异常节点与备选节点交换，使备选节点成为新的共识节点，从而动态配置共识节点群.

此外，备选节点可向外部提供查询接口，返回当前工作链状态的最新值，此步骤交由备选节点完成，共识节点无需负责，可以减少共识节点的网络带宽占用. 并且，备选节点采用区块卸载机制，通过LRU^[26]算法，将过时的区块由链上卸载到链下^[27-28]，这也同样减少了共识节点的网络带宽.

3. MC-RHotStuff流程及算法

3.1 基本交易事务

基本交易事务由工作链负责共识. 基本交易事务流程如图5所示. 基本交易事务流程分为5个步骤：

图 5 基本交易事务流程

Figure 5. Basic transaction process

下载: 全尺寸图片幻灯片

1）客户端发送一笔交易TX到协作链，该交易TX为某个工作链应处理的交易；

2）协作链节点 ${N}_{i}$ 收到交易TX后，会将该交易转播给目标工作链中的当前所有的共识节点 ${W}_{j}. {N}_{1}$ ， ${W}_{j}. {N}_{2}$ ，…， ${W}_{j}. {N}_{n}$ ；

3）目标工作链的节点 ${W}_{j}. {N}_{\mathrm{l}\mathrm{e}\mathrm{a}\mathrm{d}\mathrm{e}\mathrm{r}}$ 收到交易后，如果该交易不是过期交易且通过节点选举算法得知自己是主节点后，就将该笔交易放入自己构造的区块中进行共识；

4）当共识成功后，各个工作链节点 ${W}_{j}. {N}_{1}$ ， ${W}_{j}. {N}_{2}$ ，…， ${W}_{j}. {N}_{n}$ ，和 ${W}_{j}. {A}_{1}$ ， ${W}_{j}. {A}_{2}$ ，…， ${W}_{j}. {A}_{m}$ （该工作链所有的节点）会更新自己本地的区块链， ${W}_{j}. {N}_{1}$ ， ${W}_{j}. {N}_{2}$ ，…， ${W}_{j}. {N}_{n}$ 将产生的新区块广播回协作链；

5）当协作链节点收到足够阈值的消息后，就会将区块Hash链接到协作链保存的工作链区块头中，并会根据区块中的参与者更新自己的节点列表，例如， ${W}_{j}. {N}_{i}$ 为异常节点，则更新后的共识节点变为 ${W}_{j}. {N}_{1}$ ， ${W}_{j}. {N}_{2}$ ，…， ${W}_{j}. {N}_{i-1}$ ， ${W}_{j}. {A}_{1}$ ， ${W}_{j}. {N}_{i+1}$ ， ${W}_{j}. {N}_{i+2}$ ，…， ${W}_{j}. {N}_{n}$ ，备选节点变为 ${W}_{j}. {A}_{2}$ ， ${W}_{j}. {A}_{3}$ ，…， ${W}_{j}. {A}_{m}$ .

3.2 节点准入

节点准入由协作链负责共识. 如图6所示，节点准入流程由4个步骤构成：

图 6 节点准入流程

Figure 6. Node admission process

下载: 全尺寸图片幻灯片

1）协作链的节点 ${N}_{i}$ 收到足够数量的准入节点请求后，将这些请求封装到一个新的区块中作为新一轮共识，这些待准入节点都拥有期望加入的工作链ID；

2）一旦共识达成，说明多数的协作链节点认可新的待准入节点，待准入节点一定是按照协作链所制定的安全规则接入网络的，其身份是可认证的，由协作链共识保证其安全性. 协作链节点 ${N}_{1}$ ， ${N}_{2}$ ，… $，{N}_{n}$ 会更新自己的工作链节点列表，将新的待准入节点加入进去；

3）待准入节点 ${C}_{i}$ 的身份将变成备选节点 ${W}_{j}. {A}_{i}$ ， ${C}_{i}$ 将获得准入证书，并被放到相应的工作链节点池中；

4）协作链节点 ${N}_{1}$ ， ${N}_{2}$ ，…， ${N}_{n}$ 将相应工作链 ${W}_{j}$ 最新的节点信息发送给对应工作链的节点 ${W}_{j}. {N}_{1}$ ， ${W}_{j}. {N}_{2}$ ，…， ${W}_{j}. {N}_{n}$ 和 ${W}_{j}. {A}_{1}$ ， ${W}_{j}. {A}_{2}$ ，…， ${W}_{j}. {A}_{m}$ ，等收取到超过阈值的协作链发送的信息后，这些工作链节点更新自己的本地节点列表，将 ${W}_{j}. {A}_{i}$ 加入到备选节点组中.

3.3 MC-Schedule节点调度

节点调度由协作链负责共识. 如图7所示，节点调度流程由4个步骤构成：

图 7 MC-Schedule节点调度流程

Figure 7. MC-Schedule node scheduling process

下载: 全尺寸图片幻灯片

1）协作链节点负责监视每个工作链上的最近一个区块的平均交易量大小，如果改变幅度超过20%时，将会根据式（1）改变当前工作链 ${W}_{j}$ 共识节点的数量.

$N'=N\times （2-X）.$

(1)

注意，改变的共识节点数量应符合共识机制的数量要求，如4,7,10等.

2）MC-Schedule节点调度算法的实现要根据具体情况，例如，以C为交易量起始值的阈值，共识节点数量为N，最新的交易量 $C'$ 为例，计算它们的比值 $X=C'/C$ .

当X>1.2时，说明交易量变多，要减少共识群组中的节点数量 $N$ 来快速达成共识.

当X<0.8时，说明交易量变少，本文要增加共识群组中的节点数量 $N$ 来保证更高的安全性，同时可以加速替换共识群组中的异常节点（因为有更多的正确节点，异常节点会显得更离群）.

3）协作链节点 ${N}_{1}$ ， ${N}_{2}$ ，…， ${N}_{n}$ 将该工作链最新的节点数量要求发送给对应的工作链节点 ${W}_{j}. {N}_{1}$ ， ${W}_{j}. {N}_{2}$ ，…， ${W}_{j}. {N}_{n}$ ，等收取到超过阈值的协作链节点发送的信息后，这些工作链节点更新自己的本地节点列表，如果共识节点增加，将从备选节点中选取新的节点 ${W}_{j}. {A}_{1}$ ， ${W}_{j}. {A}_{2}$ ，…， ${W}_{j}. {A}_{m}$ （m为需要的节点数量）加入到共识群组中；如果节点减少，优先将信誉值低的共识节点 ${W}_{j}. {N}_{\mathrm{l}\mathrm{o}\mathrm{w}1}$ ， ${W}_{j}. {N}_{\mathrm{l}\mathrm{o}\mathrm{w}2},$ …， ${W}_{j}. {N}_{\mathrm{l}\mathrm{o}\mathrm{w}m}$ 放入到备选节点中. 最终，由新的共识节点向协作链发送回复.

4）当协作链节点收到超过阈值的回复后会更新自己的节点列表.

3.4 节点信誉评判以及节点自动替换MC-Scan

在讲述MC-Scan算法前，需要注意2点：

1）在选举新的leader时，会根据最新已经提交的区块来计算最新的信誉值，然后选举最高信誉值的节点作为leader.

2）仅仅把信誉值最高的节点作为leader会产生很多弊端. 例如：当该节点成为信誉值最高的节点后，即使做出异常的行为，也会因为节点信誉值高而霸占多个共识阶段，因此需要一个节点信誉值扣除机制，来保证异常的高信誉值节点能够快速地被剔除. 另外，需要防止节点的信誉值无限制的增长，以至于高信誉值节点和新加入的节点之间信誉值差距过大导致没有成为leader的机会.

因此，本文通过此轮共识下节点的2种不同表现来计算信誉值：

1）当前共识下产生了新的区块

如图8所示，如果当前共识下产生了新的区块，那么一定会存在一个新的QC，这标志着其祖父区块会被确认提交，并且，根据BLS-12门限签名机制，可以获得该祖父区块的签名参与者，因此，在选举下一轮共识的leader时，就可以根据最新被提交的区块来计算每个节点的信誉值，为了防止其信誉值无限增长，需要采用特定的方法使一直诚实的签名参与者的信誉累计增加量趋近收敛，信誉值的增加幅度也应当以签名参与者累计成功参与次数、是否被选拔为leader等因素综合度量.

图 8 当前共识下产生了新的区块

Figure 8. A new block has been generated under the current consensus

下载: 全尺寸图片幻灯片

为此，节点 ${W}_{j}. {N}_{i}$ 的第n次成功参与投票后的信誉值 ${R}_{n}^{i}$ 按照式（2）的方式增加.

${R}_{n}^{i}={R}_{n-1}^{i}+B\left(\frac{\sum {S}_{\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}}^{i}}{{\mathrm{e}}^{{R}_{n-1}^{i}}}+a\frac{\sum {R}^{j}}{N}\right) \text{，}$

(2)

其中 ${R}_{n-1}^{i}$ 为上一次投票后的信誉值， ${S}_{\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}}^{i}$ 是节点i成功参与区块构建投票的次数， $\dfrac{\sum {R}^{j}}{N}$ 为共识节点的信誉均值，N是共识节点的个数，其不包括备选节点个数，当共识节点参与了区块的投票时，B=1，否则B=0，a是信誉调节因子，当节点 ${W}_{j}. {N}_{i}$ 被选为leader时，a=–0.3，否则a=0.

信誉调节因子a的作用在于提升共识节点群组的整体公平性和积极性，使得诚实节点被当选为leader的概率是相近的，同一节点不能连续被选中，从而避免了共识节点群组的中心化问题，即纵使从始至终是诚实节点也不应该一直被选中为leader.因为leader节点为信誉值最高的节点，为保证其信誉值不能无限增长，并且不能长期处于最高信誉的状态，在leader每次当选后，就减少其信誉值，将a值设为–0.3保证了其每次削弱后不会被其他节点判定为异常节点，其信誉值处于正常共识节点信誉值的中游. 非leader节点且做出正常行为的节点的a=0，这保证了其余节点的活性，意味着只要持续做出正常行为，就一定会当选为leader节点.

算法1. MC-Scan正确区块产生时信誉值的计算.

输入：第View轮共识；

输出：Null or “View过旧”.

① block $\leftarrow$ getCommittedBlock()；/*获得最新提交的区块*/

② if block.view > View–chainLength()

③ 　return “View过旧”；

④ end if

⑤ voters $\leftarrow$ block.QC().signature().participant；/*获得最新提交的区块的参与者*/

⑥ for each voters containing v

⑦　if prevCommitHeadView() < block.view

⑧　　if v.id in currentConsensusNode /*这个节点　　还在共识组中*/

⑨　　　 v.prereputation $\leftarrow$ v.reputation；

⑩　　　 v.reputation $\leftarrow$ 式（2）；

⑪ 　　　v.timeout $\leftarrow$ false；

⑫　　end if

⑬　end if

⑭ end for

⑮ if prevCommitHead.View() < block.view

⑯　prevCommitHead $\leftarrow$ block；

⑰ end if

⑱ updateCurrentReplicasReputation(). /*将已经标记为超时的节点信誉值继续减半*/

2）当前共识下没有产生正确的区块

如图9所示，如果当前共识下没有产生正确的区块，将无法通过新的QC来寻找其祖父区块来计算新的信誉值. 为了保证信誉值计算能够正常进行，本文将根据与QC产生原理相似但意义不同的TC作为信誉评判的标准. TC的产生是因为当前共识下没有对leader提出的区块产生正确的响应，从而导致此次共识超时，根据所有节点对本次共识超时达成共识以后而产生的门限签名本文就可以成功地过渡到下一轮共识，进行新一轮共识，TC的作用相当于在该共识中产生了一个空区块为流水线填充，从而保证流水线不会中断，若因为连续超时等原因导致多个空白区块及TC连接在一起，则会形成一个连续的空流水线，但最终提交到区块链中的内容都为经过3阶段共识成功的QC，所以实际的区块链中并不存在TC. 因此，本文就可以利用TC来对此次共识下的leader的行为进行评判.

图 9 当前共识下没有产生正确的区块

Figure 9. The correct block has not been generated under the current consensus

下载: 全尺寸图片幻灯片

当选举下一轮共识的leader时，会检查最新的TC，如果TC是当前第View轮共识产生的话，则断定此轮共识的leader发生了异常. 但是，异常的可能性有很多种，其中一种可能是因为当前的交易量无法满足一个区块的打包，导致leader无法提出新区块造成的超时，该行为并不是因为leader节点自身的原因造成的，而是该节点不能因为做出了正确的行为而扣除了错误的信誉值. 因此，本文采取一个缓和措施，如式（3）所示，当共识第1次产生了TC，本文不对当前节点采取信誉值扣除，而只是标注其发生了异常行为，其节点还是信誉值最高的节点，但无论其是否存在自身的问题，都不应选举该节点当选下一轮共识的leader节点，因此，本文顺延至信誉值排名第2的节点来当作新的leader发起共识.

当此异常leader再次当选leader并且做出正确行为时，或者参与下一轮投票时，本文会取消上一次异常行为的标注，但如果该节点还是产生异常行为，本文就会扣除该节点的信誉值，扣除的信誉值为当前所有节点信誉值平均值的一半，这对该节点的信誉积累是致命的，所有节点的平均信誉值代表大部分正常节点的信誉值，即便此时的异常节点为信誉值最高的节点，经过1~2轮的异常判定后，其信誉值会被减少到远离平均值，这意味着该节点很快就会被踢出共识组，这保证了节点不能因为信誉值高而不作为，而是等到信誉值降低到一定程度后再恢复正常行为.

${R}_{n}^{i}=\left\{\begin{array}{*{20}{c}}{R}_{n-1}^{i}\text{，}& label={\mathrm{false}};\\ {R}_{n-1}^{i}-\frac{\sum {R}^{j}}{N}\text{，}& label={\mathrm{true}}.\end{array}\right.$

(3)

算法2. MC-Scan没有正确区块产生时信誉值的计算.

输入：第View轮共识.

① block $\leftarrow$ getCommittedBlock()；/*获得最新提交的区块*/

② if block.view > View–chainLength()

③　return “View过旧”；

④ end if

⑤ if preTimeOutQC[View–1]==false&&highTCview() ==View–1&&highTCview()> highQCview() /*此轮共识还未访问过TC，并且产生的新的TC比QC的view还高*/

⑥　leader $\leftarrow$ getLeader(View–1)；

⑦　if leader.timeout==false /*第1次仅标记*/

⑧　　leader.timeout $\leftarrow$ true；

⑨　else /*第2次扣除信誉值*/

⑪　　leader.preReputation=leader.Reputation；

⑫　　leader.Reputation= 式（3）；

⑬　end if

⑭　prevTimeOutQC[View–1] = true；

⑮ end if

当本轮共识的节点信誉值更新完成后，本文引入聚类算法DBSCAN^[29-30]，以节点的上一次信誉值作为x轴，新的信誉值作为y轴，平均信誉值为半径来对异常节点进行筛选，通过扫描，本文将平均信誉值范围内存在的节点数量小于阈值的节点判定为异常节点，随后与备选节点进行替换.

为了保持一致性，替换时要保证从节点ID最小的备选节点替换，当备选节点不足时，本文需要暂停替换，直到新的备选节点加入；当备选节点充足但替换失败时，表明备选节点存在异常节点，本文维持当前共识组，并更新备选节点，当更新完成时进行新一轮的替换.

本文使用BLS12加密算法来保证当节点被替换或者加入新的节点不会影响门限签名的生成，从而不影响共识的流程，解决方案是对此让每个节点都记录当前共识组节点的公钥，当节点变化时则更新这个节点的记录表.

算法3. MC-Scan选举leader节点并替换异常节点.

输入：第View轮共识；

输出：leader Node.

① 执行算法 1；

② 执行算法2；/*执行算法1或算法2计算节点的信誉值*/

③ cluster $\leftarrow$ dbscan(nodelist,quorumSize(numReplicas),getAverageReputation())；/*通过DBSCAN聚类算法，以节点平均信誉值为半径，2/3节点为阈值进行聚类，寻找异常节点*/

④ alterNodes $\leftarrow$ currentConsensusNode–cluster；/*在簇外的节点为异常节点*/

⑤ if len(alterNodes)≠0

⑥　alterReplica $\leftarrow$ updateCRepl(alterNodes)；　/*先从本地替换，返回被替换的节点（有　可能会因为备选节点不足或备选节点异　常导致没有节点被替换）*/

⑦ end if

⑧ isChange $\leftarrow$ MC-Syn(alterReplicas)；/*算法4*/

⑨ if isChange ==false

⑩　return “节点更新失败”；

⑪ end if

⑫ leader $\leftarrow$ getHighestReputationReplicas()；

⑬ return leader.

MC-RHotStuff中提出的信誉值计算和异常节点替换机制不仅适用于多链环境中，其核心思想也适用于大多数共识算法和不同类型的区块链，具有很强的通用性.

3.5 节点状态同步

节点调度流程如图10所示. 当一轮共识中未发生节点替换时，共识组中的节点和备选节点所保存的每个节点信誉值是一样的，而且它们都会更新自己的区块链，因此，在未替换的情况下，当前进到下一轮共识时，其状态都是同步的.

图 10 节点状态同步流程

Figure 10. Node status synchronization process

下载: 全尺寸图片幻灯片

当一轮共识中发生了视图异常更替时，首先，备选节点由于身份的限制无法参与共识，所以接收不到TC，因此无法在异常情况下更新节点的最新状态. 简言之，备选节点可以同步区块链的区块信息，而无法同步每个节点的信誉状态. 这时就需要一个同步的过程来保证全局状态的一致. 该过程只能由共识节点发起，因为大多数节点为诚实节点，因此当共识组在本轮共识中发现了需要替换的节点时，由于替换节点首选ID最小原则，假设 ${W}_{j}. {A}_{1}$ 为ID最小的备选节点，多数共识节点都会将 ${W}_{j}. {A}_{1}$ 和异常节点 ${W}_{j}. {N}_{i}$ 进行替换. ${W}_{j}. {N}_{1}$ ， ${W}_{j}. {N}_{2}$ ，…， ${W}_{j}. {N}_{i-1}$ ， ${W}_{j}. {N}_{i+1}$ ，…， ${W}_{j}. {N}_{n}$ 会发送节点替换信息. 当所有节点收到超过共识节点阈值的消息后会进行转发；当收到超过所有节点阈值的消息，并且这些消息中存在 ${W}_{j}. {A}_{1}$ 的消息，则表明大多数节点已经对最新的节点信誉达成了共识，并且 ${W}_{j}. {A}_{1}$ 是活跃的节点，这时所有节点认可 ${W}_{j}. {A}_{1}$ 是新的共识节点，并更新自己的列表，将 ${W}_{j}. {A}_{1}$ 转变为 ${W}_{j}. {N}_{\mathrm{n}\mathrm{e}\mathrm{w}}$ . 当下一轮共识开始时， ${W}_{j}. {N}_{\mathrm{n}\mathrm{e}\mathrm{w}}$ 将参与新的共识，工作链共识节点会将最新同步的节点状态广播给协作链，使协作链和工作链节点状态一致.

这个过程是在一轮共识中发生的，由于半同步性质，大多数的诚实节点都处于本轮共识中，因此当发生节点替换时，每个共识节点都延长了本轮共识的时间来保证替换的成功完成，延长的时间由当前共识组正常推进一轮共识所需要的时间来决定，由于每个节点都会维护一个最近几轮共识所需要的时间，通过计算这几轮共识的方差，并采用随机数算法添加一定的时间后来作为下一轮的共识最长时间. 每个节点的超时时间都是不同的，但都不会超过最大超时时间，即GST.因此，从理论结果表明，当发生替换后，延长的时间一定要超过GST，本文设定延长的时间为GST的2倍. 当替换完成后，会推进下一轮共识继续进行新的共识，从宏观角度来看，节点的替换行为并没有影响共识的进行，区块链的状态仍保持一致. 从算法4，5和结果来看，节点替换虽然会延长此轮共识的时间，影响区块链的整体性能，但与因节点故障而导致的性能下降相比可忽略不计.

算法4. MC-Syn实现节点状态同步.

输入：alterReplicas；

输出：ture or false.

① if len(alterReplicas)≠0/*真的发生了节点替换*/

②　synchronizer.restTimer()；　/*延长本轮共识的超时时间，以完成节　点同步*/

③　synchronizer.cancelView()；　/*取消本轮共识下的相关工作*/

④　sendNodeInfoToOtherNodes(alterReplicas)；

⑤　until get quorumSize(allNodes) replys；　/*收到了该工作链上多数节点对该消息　的响应*/

⑥　if alterReplicas.hash==replys.hash

⑦　　return true；

⑧　else

⑨　　return false；

⑩　end if

⑪ end if

⑫ return true.

算法5. UpdateNodeInfo接收MC-Syn信息更新节点信息.

输入：alterReplicas.

① wait quorumSize(consensusNodes)；

② alter Replicasrequests；/*更新节点由共识节点　发起，因此到达共识节点阈值就表明更　新有效*/

③ update CurrentReplicas(alterReplicasrequset) ；

④ send NodeInfoToOtherNodes(quorumrequset). /*转发给共识节点，当共识节点收到超过阈值的消息后，表明该工作链已经完成同步*/

4. 性能分析

本文使用GO语言来编写了大约5000行代码实现了实验算法，本文在4台Intel Xeon^® Gold 6240C CPU @ 2.60 GHz × 72，256 GB运行内存的服务器上进行实验，本文将该服务器虚拟化成32台可视化的Ubuntu22虚拟机，每台虚拟机拥有8核2.60 GHz的CPU和16 GB的运行内存，它们直接的网络通信延迟少于1 ms，平均网络带宽10000 Mbps.

本文算法主要和原生HotStuff算法进行比较，本文设定一笔交易中拥有128 B的负载，批处理大小为400，主要观察其吞吐量和交易延迟的差异. 另外，本文对节点行为评判机制进行实验来观察本文算法的表现.

1）实验1. 该实验在多链环境下进行，将0.16 MTPS作为基准交易吞吐量，并布置了10个协作链节点，首先，该实验让每个协作链节点达到负载均衡，通过不断增加工作链条数来观察工作链平均吞吐量. 通过实验发现，当工作链条数增加到9时，平均吞吐量下降，这说明协作链节点条数达到了性能瓶颈. 另外，该实验改变协作链节点的负载均衡，100%将交易平均分配给所有协作链节点，1%使1个协作链节点负责处理交易，通过实验发现，当负载均衡率越低时，平均吞吐量将显著下降. 通过实验可以得出，若协作链节点数量较多且性能较好时即可发挥出每条工作链的最大性能，实验结果如图11所示.

图 11 多链平均吞吐量

Figure 11. Average throughput of multiple chains

下载: 全尺寸图片幻灯片

2）实验2. 该实验在一条工作链上进行，引入节点调度与原生算法进行比较，将0.16 MTPS作为基准交易吞吐量，32个节点作为基准共识节点. 根据实验结果可以看到，在吞吐量小于基准交易吞吐量时，由于MC-Schedule会增加共识节点的数量，节点之间通信的开销增大，交易的延迟会小幅度增长，但随着吞吐量的增加，共识节点数量减少，其交易延迟要优于原生算法. 本文认为，为了在吞吐量高的情况下保持良好的性能，在吞吐量较少的情况下牺牲一部分的性能，来加快对异常节点的替换是值得的，因为节点数量越多，异常节点的异常行为暴露得就越快，实验结果如图12所示.

图 12 动态共识节点与原共识模式对比

Figure 12. Comparison between dynamic consensus node and original consensus mode

下载: 全尺寸图片幻灯片

3）实验3. 在该实验中，本文设置了32个共识节点，其中，有10个异常节点，本文设定每100轮共识时产生1个异常节点，随后通过MC-Scan算法将其替换，本文记录每100轮共识的平均交易延迟和吞吐量，并采用不具备节点替换机制的原生HotStuff算法与其比较.

可以看到，如图13所示在前200轮共识中交易时延有小幅度增长，这是因为节点替换导致共识的持续时间变长而造成的，引入节点替换机制后，会在替换初期产生较原生HotStuff更高的交易时延. 但在随后的共识中，随着异常节点的数量慢慢减少，时延整体是优于原生算法的. 另外，本文可以看到，随着异常节点的减少，交易吞吐量也慢慢增加，实验结果如图14所示.

图 13 引入节点替换机制后交易吞吐量对比

Figure 13. Comparison of transaction throughput after introducing node replacement mechanism

下载: 全尺寸图片幻灯片

图 14 引入节点替换机制后交易时延对比

Figure 14. Comparison of transaction latency after introducing node replacement mechanism

下载: 全尺寸图片幻灯片

4）实验4. 为了检验MC-Scan寻找异常节点的精确度，本文设置了2个对比实验，在本实验中，为了方便观察，仅设置4个共识节点，其中，节点1为异常节点，并且持续做出异常行为，本文设置每个节点的初始信誉值为50，图15中的虚线部分是所有节点的平均信誉度，而阴影部分表示节点1以平均信誉度为半径的扫描范围，最新信誉值代表本轮节点信誉值，上一轮信誉值代表上一轮节点信誉值. 可以看到，随着共识进程的进行，节点1的信誉值持续下降，最终在MC-Scan算法的扫描下被判定为异常节点，随后被替换为节点5，节点5获得其余3个节点的平均信誉值，其信誉值范围为阴影部分. 与其他信誉值评判算法相比，MC-Scan算法具有自动检测异常节点并进行替换的功能，并且，在大规模节点情况下该算法同样有效，实验结果如图15所示.

图 15 异常节点持续异常

Figure 15. Exception node persistent exception

下载: 全尺寸图片幻灯片

5）实验5. 在本实验中设置4个共识节点，其中，节点1为异常节点，在其做出1次异常行为后转为正常节点，本文设置每个节点的初始信誉值为50，图中的虚线部分是所有节点的平均信誉度，而阴影部分表示节点1以平均信誉度为半径的扫描范围. 可以看到，随着共识进程的进行，节点1的信誉值产生了下降，但随后转为正常节点后，其信誉值不断上升，最终在收敛的节点信誉值计算下，其信誉度逐渐恢复成和正常节点同一个水平，并不会作为异常节点而被替换，实验结果如图16所示.

图 16 异常节点非持续异常

Figure 16. Exception node nonpersistent exception

下载: 全尺寸图片幻灯片

5. 结　　论

本文提出了一种新型多链联盟链共识机制，通过引入节点身份机制来为不同节点划分不同职能，本文使用节点信誉值及基于信誉值的节点聚类和替换算法寻找共识节点中的异常节点并清除来实现更高的系统效率，同时引入了动态共识节点调整机制，进一步优化系统资源使性能得到提升.

未来的工作包括2个方面：1）继续优化资源池调度算法来对共识算法进行改进；2）实现分层机制划分不同的工作链，使更高层次的工作链作为协作链管理低层次工作链.

作者贡献声明：路宇轩提出了算法思路和实验方案；孔兰菊提出指导意见并修改论文；路宇轩、张宝晨、闵新平负责完成实验并撰写论文.

图 1 硬件化断言自动化编译器工作流与平台结构

Figure 1. Workflow and platform structure of the hardware assertion automatic complier

下载: 全尺寸图片幻灯片

图 2 硬件化断言编译器结构

Figure 2. Structure of the hardware assertion complier

下载: 全尺寸图片幻灯片

图 3 断言表达式语法树示例

Figure 3. An example of assertion expression syntax tree

下载: 全尺寸图片幻灯片

图 4 内部结点例化示例

Figure 4. An example of inner node instantiation

下载: 全尺寸图片幻灯片

图 5 断言数据区域结构

Figure 5. Structure of assertion data region

下载: 全尺寸图片幻灯片

图 6 断言数据平台数据流结构

Figure 6. Dataflow structure of assertion data platform

下载: 全尺寸图片幻灯片

图 7 硬件化断言平台版图

Figure 7. Floorplan of hardware assertion platform

下载: 全尺寸图片幻灯片

图 8 FPGA仿真相对于软件仿真加速比

Figure 8. Acceleration ratio of FPGA simulation compared with software simulation

下载: 全尺寸图片幻灯片

表 1 已支持的硬件化断言算子

Table 1 Supported Hardware Assertion Operators

硬件算子类型	硬件算子名称	算子使用示例
采样函数	$rose $fell $stable $past	$rose(a) $fell(a) $stable(a) $past(a)
序列操作符	and or intersect first_match	a and b a or b a intersect b first_match(a)
属性操作符	\|=> \|-> if … else	a \|=> b a \|-> b if (a) b else c
延迟与重复	## [*]	a ## 1 b / a ##[1:2]b a[2]/a[1:2]b

下载: 导出CSV

表 2 断言数据地址分配

Table 2 Address Mapping of Assertion Data

地址	地址段功能	寄存器宽度
0x0000-0x0fff	触发计数器	16
0x1000	断言失败记录	32
0x1004	性能计数器低位	32
0x1006	性能计数器高位	32

下载: 导出CSV

表 3 断言类型与数量

Table 3 Type and Amount of Assertions

断言类型	断言子类型	数量	属性来源
AXI Assertion	KEEP STABLE	29	Standard
	INVALID WHEN RESET	10	Standard
	TIME_OUT	1	Standard
	RESERVE SIGNAL	2	Standard
CSR Assertion	TRAP	5	Standard
	RET	6	Standard
	EXCEPTION PIRORITY	4	Standard
BPU Assertion		4	Design Spec
Cache Assertion		3	Design Spec
Regfile		1	Standard

下载: 导出CSV

表 4 软件仿真Nutshell运行各基准测试结果

Table 4 Testing Results of Each Benchmark Run by Software Simulation Nutshell

基准测试	运行时间/s	周期数	仿真频率/kHz
coremark	371.42	1858853	5.005
dhrystone	437.63	2143378	4.898
microbench-qsort	463.21	2369069	5.114
microbench-queen	360.46	1821639	5.054
microbench-bf	448.01	1967435	4.392
microbench-fib	390.40	2639506	6.761
microbench-sieve	485.60	3174664	6.538
microbench-15pz	457.99	2585612	5.646
microbench-dinic	539.19	3412524	6.329
microbench-lzip	510.03	3796330	7.443
microbench-ssort	495.73	3109954	6.273
microbench-md5	514.30	4066747	7.907

下载: 导出CSV

表 5 硬件断言与ILA的资源占用量和资源占用比

Table 5 Resource Usage and Resource Usage Ratio of Hardware Assertions and ILA

资源类型	硬件断言	ILA（配置1）	ILA(配置2)	果壳处理器
LUTs	1223 (0.23%)	2266 (0.43%)	3749 (0.72%)	41537 (7.95%)
Registers	933 (0.09%)	3833 (0.37%)	4243 (0.41%)	53273 (5.1%)
BRAMs	0 (0%)	8 (0.81%)	512 (52.03%)	56 (5.69%)
DSPs	0 (0%)	0 (0%)	0 (0%)	16 (0.81%)
注：括号内部的资源占用比表示该类型资源用量与FPGA片上资源总量的比值.

下载: 导出CSV

参考文献(24)

[1]	Witharana H, Lyu Y, Charles S, et al. A survey on assertion-based hardware verification[J]. ACM Computing Surveys, 2022, 54(11s): 1−33
[2]	Xu Yin’an, Yu Zihao, Tang Dan, et al. Towards developing high performance RISC-V processors using Agile methodology[C]//Proc of the 55th IEEE/ACM Int Symp on Microarchitecture (MICRO). Piscataway, NJ: IEEE, 2022: 1178−1199
[3]	GRAPHICS M. The 2020 Wilson research group functional verification study[EB/OL]. (2020-10-10)[2023-12-08]. https://blogs.sw.siemens.com/verificationhorizons/2022/10/10/prologue-the-2022-wilson-research-group-functional-verification-study/
[4]	Shi Kan, Xu Shuaxiang, Diao Yuhan, et al. ENCORE: Efficient architecture verification framework with FPGA acceleration[C]//Proc of the ACM/SIGDA Int Symp on Field Programmable Gate Arrays. New York: ACM, 2023: 209–219
[5]	Xilinx. Vivado Design Suite User Guide: Synthesis (UG901) [EB/OL]. [2023-04-17]. https://docs.xilinx.com/r/en-US/ug901-vivado-synthesis
[6]	Cerny E, Dudani S, Havlicek J, et al. SVA: The Power of Assertions in SystemVerilog[M]. Berlin: Springer, 2015
[7]	Design Automation Standards Committee. IEEE1800-2017 IEEE Standard for SystemVerilog Unified Hardware Design, Specification, and Verification Language Standard IEEE 1800[S].[2023-12-03]. http://www.edastds.org/sv/
[8]	Zhou Zhili, Xie Zheng, Wang Xin’an. Development of verification envioronment for SPI master interface using SystemVerilog[C]//Proc of the 11th Int Conf on Signal Processing. Piscataway, NJ: IEEE, 2012: 2188−2192
[9]	Gurha P, Khandelwal R R. Systemverilog assertion based verification of amba-ahb[C]//Proc of 2016 Int Conf on Micro-Electronics and Telecommunication Engineering (ICMETE). Piscataway, NJ: IEEE, 2016: 641−645
[10]	Tan Zhangxi, Andrew W, Henry C, et al. A case for FAME: FPGA architecture model execution[C]//Proc of the 37th Annual Int Symp on Computer Architecture. New York: ACM, 2010: 290–301
[11]	Krupnova H, Saucier G. FPGA-based emulation: Industrial and custom prototyping solutions[C]//Proc of Int Workshop on Field Programmable Logic and Applications. Berlin: Springer, 2000: 68–77
[12]	Veneris A, Keng B, Safarpour S. From RTL to silicon: The case for automated debug[C]//Proc of the 16th Asia and South Pacific Design Automation Conf (ASP-DAC 2011). Piscataway, NJ: IEEE, 2011: 306−310
[13]	Ma Jiacheng, Zuo Gefei, Loughlin K, et al. Debugging in the brave new world of reconfigurable hardware[C]//Proc of the 27th ACM Int Conf on Architectural Support for Programming Languages and Operating Systems. New York: ACM, 2022: 946−962
[14]	Kim D, Celio C, Karandikar S, et al. DESSERT: Debugging RTL effectively with state snapshotting for error replays across trillions of cycles[C]//Proc of the 28th Int Conf on Field Programmable Logic and Applications (FPL). Piscataway, NJ: IEEE, 2018: 76−764
[15]	Attia S, Betz V. StateMover: Combining simulation and hardware execution for efficient FPGA debugging[C]//Proc of the 2020 ACM/SIGDA Int Symp on Field-Programmable Gate Arrays. New York: ACM, 2020: 175−185
[16]	Pellauer M, Lis M, Baltus D, et al. Synthesis of synchronous assertions with guarded atomic actions[C]//Proc of the 2nd ACM and IEEE Int Conf on Formal Methods and Models for Co-Design (MEMOCODE’05). Piscataway, NJ: IEEE, 2005: 15−24
[17]	Das S, Mohanty R, Dasgupta P, et al. Synthesis of system verilog assertions[C]//Proc of the Design Automation & Test in Europe Conf. Piscataway, NJ: IEEE, 2006, 2: 1−6
[18]	Kastelan I, Krajacevic Z. Synthesizable SystemVerilog assertions as a methodology for SoC[C]//Proc of the 1st IEEE Eastern European Conf on the Engineering of Computer Based Systems. Piscataway, NJ: IEEE, 2009: 120−127
[19]	Slang-SystemVerilog Language Services [EB/OL]. (2015) [2023-12-01]. https://github.com /MikePopoloski/slang
[20]	OSCPU Nutshell(果壳)处理器核 [EB/OL]. [2023-04-17]. https://oscpu. gitbook.io/nutshell/jie-shao/introduction OSCPU. Nutshell processor core[EB/OL]. [2023-04-17]. https://oscpu. gitbook.io/nutshell/jie-shao/introduction (in chinese
[21]	Bachrach J, Vo H, Richards B, et al. Chisel: Constructing hardware in a scala embedded language[C]//Proc of the 49th Annual Design Automation Conf. San Francisco, CA: DAC, 2012: 1216−1225
[22]	Gal-on S, Levy M. Exploring coremark a benchmark maximizing simplicity and efficacy[R]. The Embedded Microprocessor Benchmark Consortium.2012[2023-12-01].https://www.eembc.org/techlit/articles/coremark—whitepaper.pdf
[23]	Weicker R P. Dhrystone: A synthetic systems programming benchmark[J]. Communications of the ACM, 1984, 27(10): 1013−1030 doi: 10.1145/358274.358283
[24]	Yu Zihao, Jiang Yanyan. Benchmarks for CPU correctness and performance testing[EB/OL]. 2021 [2023-12-01]. https://github.com/NJU-ProjectN/am-kernels/tree/master /benchmarks/ microbench