多核处理器事务级模型多视图协同验证环境＊

王 俊，刘 磊，张 龙，李思昆

（国防科学技术大学高性能计算国家重点实验室，湖南长沙410073）

1 引言

根据2011年国际半导体技术发展路线图（ITRS）预测［1］，未来10年集成电路仍将按照摩尔定律持续高速发展，2015年将采用15 nm工艺，2020年将采用10 nm工艺，2022年将实现8 nm工艺，片上处理器核数目也呈现出同摩尔定律相似的指数增长规律，设计复杂程度达到前所未有的高度，对处理器验证提出了严峻的挑战。

目前工程应用中，多核处理器体系结构的设计和验证仍然主要集中在寄存器传输级和门级。常用的验证方法仍然是模拟验证。形式验证成为研究热点，硅后验证研究也得到了更多的关注。众多的研究显示，在多核处理器项目中，验证耗费的时间和资源最多，验证已成为片上多核处理器发展的重大障碍。

Mentor Graphics公司CEO WallyRhines认为，目前验证能力需要提高100倍才能满足当前硬件发展需要［2］，而形式验证和高层次的事务级验证将可能带来这100倍的提速。但是，目前支持事务级高层次验证理论与方法的研究仍处于发展阶段，相应的验证工具还比较匮乏。

模拟验证由于具有非完备性，即只能证明有错而不能证明无错，一般适用于在验证初期发现大量和明显的设计错误。基于覆盖率驱动的模拟矢量自动生成是当前多核处理器模拟验证技术的研究热点［3～6］。由于当今片上多核处理器设计的复杂性和庞大的规模，没有一种方法或工具能生成完备的模拟向量。

形式验证对系统具有的性质和最终实现的正确性进行严格的证明，从数学上完备地证明系统是否实现了设计者的意图，较好地弥补了模拟验证的完备性缺陷，已在多个领域得到广泛应用。形式验证主要分为静态形式验证和半形式验证。静态形式验证不需要添加激励，也不需要仿真，常用的是等价性检查（Equivalence Checking）。半形式验证混合了仿真技术和形式验证技术，常用的是等价性验证和模型检验。至今形式验证存在状态空间爆炸问题，验证规模仍较小。Stanford大学和CMU大学在模型检验方面进行了大量卓有成效的研究，Clarke E M提出完全自动化的、反例指导的抽象精化方法——CEGAR（Counter－Example Guide Abstraction Refinement），成为自动分析与验证大规模软硬件系统的一种主要方法［7］。荷兰Rad－boud大学Schmaltz J等［8］在NOC协议交互式推断验证方面做了大量有效工作。

事务级应用验证是在多核处理器系统事务级模型上，编译运行典型应用程序，验证多核处理器系统的功能设计是否正确。既可缩短应用软件开发时间，又可更完备地验证多核处理器事务级模型的设计正确性。已有的多核处理器应用验证大多都是基于硬件仿真器实现，运行效率较高，验证周期长，代价昂贵。对事务级应用验证重视不够，应用较少。

前述的多核处理器验证方法属于单视图验证，在实际验证应用中存在局限性。要将已有的单视图验证联合使用，存在数据共享和数据交换困难、使用不方便等问题。将形式验证和模拟验证结合是目前的研究热点。

本文提出多核处理器的事务级多视图协同验证方法，是通过把已有不同类型的先进验证工具集成应用，充分发挥不同类型验证方法综合应用的优势，协同高效完成验证任务。

2 多核事务级模型多视图协同验证方法

2.1 多核事务级模型多视图协同验证原理

随着电子系统级设计方法的发展，事务级建模与验证技术受到高度重视。事务级模型遵循计算、存储、通信分离的理念进行高层抽象建模，只关注周期精确的系统功能，隐藏了不必要的计算和通信细节。因此，模型的可读性好，模拟效率高，既便于进行系统架构分析和方案探索，又可为早期软件开发提供模拟平台，也可以为RTL设计提供参考模型和验证平台。

多核处理器事务级模型多视图协同验证方法，是把模拟验证、形式验证、应用验证三类验证方法看做三种验证视图，采用统一集成平台，构建一体化验证环境。从而可在一体化验证环境中，充分发挥多种验证方法综合应用的优势，协同高效完成多核处理器的验证任务。其原理示意图如图1所示。

该方法针对多核事务级模型，通过构建统一操作界面，把三个验证视图所需工具集成到一个框架下，使得验证操作便捷高效；进行全局数据管理和一致性维护，有效控制三个视图验证流程，不同验证视图可同时运行，多个验证人员也可并行协同工作；通过构建模型库、验证库、应用程序库，实现多核部件模块、验证模块、应用程序的重用，增强了平台的可扩展性和适用性。

Figure 1 Multi－view co－verification schematic of transaction－level models图1 事务级模型多视图协同验证原理图

2.2 多核事务级模型多视图协同验证流程

由于进行模拟验证和形式验证的工具和方法多样，每种应用都有特定的配置和需求，构建统一界面的集成环境需要充分考虑这些工具软件的特性，理顺操作流程和相互关系。同时，多视图协同验证中的大量数据需要按照协同验证流程合理顺畅地在各视图之间传递。其基本验证流程如图2所示。

为实现时钟精确的模拟，需要首先使用SystemC建立周期精确的多核事务级模型；然后根据多核模型各模块的特点，结合模拟验证和形式验证的各自优势，并行进行。

基于设计IP重用和验证IP重用思想，模拟验证视图采用具有模拟矢量自动生成、覆盖率驱动、基于事务验证的UVM验证技术，或者基于SCV（SystemC Verification Library）库，进行模拟验证。形式验证视图目前主要基于较成熟的模型检测和等价性验证工具，可以对在模拟试图中所设计并经过模拟验证的模块做进一步验证，也可以对所建立的多核事务级模型的其他适合进行形式验证的模块进行同步验证。

基于验证程序重用思想，从基准测试程序库选取基准程序，或自定义应用测试程序，交叉编译为目标平台上的二进制文件，在硬件模拟器上加载运行，结果与标准输出对比，进行应用验证。该视图下也可以实现软硬件协同验证，即在通过验证的正确多核模型上，开发调试适合该多核架构的应用程序。

Figure 2 Multi－view co－verification process of multicore transaction－level models图2 多核事务级模型多视图协同验证流程

3 基于SoCLib的多核事务级多视图协同验证环境实现

3.1 SoCLib仿真平台

SoCLib仿真平台由法国TIMA Lab、Lip6等研究机构与STMicrelectronics等知名企业联合开发，是基于片上多核系统设计的、开源的ESL建模仿真开放平台。该平台的核心是使用SystemC建模的模型库，包括ARM、MIPS、Nios等微处理器、总线及片上网络、Cache、主存、各种外设等，均可以在标准SystemC环境中模拟仿真。使用SystemC建模能够实现功能模块、通信模块、软件模块和硬件模块在各种系统级层次上的抽象，可以快速有效地建立软件算法的精确模型，并对设计进行仿真验证和优化。其仿真速度可达到使用VHDL或Verilog建模的10～100倍，可有效减少设计验证周期，缩短产品开发时间。

SoCLib每种模型有两种类型可供使用：CABA（Cycle Accurate/Bit Accurate）、TLM－DT（Transaction Level Modeling with Distributed Time），均采用VISA组织的IP标准化接口VCI进行封装，可实现时钟周期精确的仿真。SoCLib平台还支持运行DNA/OS、Mutek H、NetBSD等多个嵌入式操作系统，也提供了多个用于系统调试、监控、设计空间探测的工具。SoCLib核心库、多核系统架构、操作系统与应用程序之间的关系如图3所示。

SoCLib平台由一组库文件构成，其所有部件都符合VCI/OCP通讯协议标准，可以方便地根据特定的应用需求添加新的功能，是比较理想的多核事务级建模仿真平台。

Figure 3 Relations among SoCLib libraries，multi－core platforms，operating systems and applications图3 SoCLib库、多核平台、操作系统和应用程序关系

基于SoCLib开发多核处理器事务级多视图验证环境，主要优点在于：（1）SoCLib所有部件都采用SystemC建模，模型封装都符合VCI/OCP通讯协议标准，既可有效利用其模型资源，又易于添加新的部件功能；（2）SoCLib的多核系统架构遵循计算、通信、存储分离的理念进行设计，互联通信模型既可采用总线模型，也可采用片上网络模型，易于重用已有的IP核，提高了构建各种多核处理器体系结构的效率；（3）Soclib对多核体系结构的应用程序编译映射提供了较好的技术支持。因此，本文重点研究基于SoCLib的多核处理器事务级多视图协同验证方法。

3.2 多核事务级模型多视图协同验证环境MVIE架构

基于选择或继承已有的先进模拟平台和程序编译平台的考虑，构建多视图协同验证环境MVIE（Multi－view Verification Integrated Environment）。MVIE是基于SoCLib仿真平台构建的，直接支持SystemC事务级建模和ESL硬件仿真，主要解决模拟验证、形式验证和应用验证多视图协同控制，验证数据管理传递的问题，支持多种验证方法，支持验证代码重用。

该多视图协同验证环境框架基本结构如图4所示，主要分为三个层次。一是环境基础部分，包括基础类库和SoCLib事务级仿真平台、共享模型库及工程模型库。基础类库含SystemC类库、SCV类库、Python库、C＋＋标准库，用以支持整个平台运行。二是人机交互部分，主要包括人机界面及对应三类视图的工具集成。其中公共人机界面提供统一的操作接口，并根据不同验证视图所需工具的集成需要，实现三类验证视图界面。模拟验证视图下集成代码编辑器、应用编译器和波形查看器；形式验证视图下集成Cache一致性验证工具、等价性验证工具、NoC验证工具；应用验证视图下集成硬件编译器、交叉编译器、可视化调试器。三是工程数据管理部分，实现三类视图数据的收集、查询、分析和一致性管理。由于数据信息量不大，为便于在多视图间传递，采用XML描述和存储数据。

3.3 多核事务级模型多视图协同验证环境MVIE软件实现

在Linux下安装设置好SoCLib仿真环境，按照图4所示环境架构，使用Qt设计开发具有良好交互界面的集成软件平台MVIE，着重解决三个视图协同验证的数据传递和管理问题、多个工具软件的集成问题、多视图协同验证集中展现方法，实现软件环境的可用性、高效性和实用性。

Figure 4 Multi－view co－verification environment architecture of multi－core transaction－level models图4 多核事务级模型多视图协同验证环境系统架构

MVIE软件主界面如图5所示，主要分为四个区域：

（1）位于顶部的功能菜单区，可选择软件所有功能，包括工程、建模、视图、命令、帮助等。

（2）位于左侧的功能切换区，包括快捷使用、快速建模、模拟验证、形式验证、应用验证五类视图，可根据使用者的选择显示不同的内容。快捷使用视图，用于快速入门和启动工程，显示于软件启动时，提供软件使用的快速入门提示和快速启动工程的链接；快速建模视图，用于基于已有模块库快速建立多核模型，若模型工程未建立则提示先建立工程，待模型工程建立后或工程已建立则显示当前工程文件，提供代码编辑、编译、调试功能；模拟验证视图和形式验证视图用于使用相关工具对特定模块进行验证，若模块工程未建立则建立模块工程，若模块工程已建立则显示模块工程主文件内容，提供代码编辑、编译、调试和基于工具的验证功能；应用验证视图用于使用自选的应用程序验证多核模型，或者在已验证的多核模型上开发多核应用软件，提供代码编辑、编译、调试和程序运行结果对比功能。

（3）文件列表区，分为工程文件列表和库文件列表。其中，工程文件列表列出当前工程所有文件，便于查看和组织工程源文件；库文件列表列出公用IP模块库和自定义模块库所有模块，方便查看和调用。工程文件列表根据视图选择的不同进行相应的变化，快速建模和应用验证视图下显示模型工程文件列表，模拟验证和形式验证视图下显示模块工程文件列表，并提供导入/导出、添加/删除代码文件的功能；库文件列表根据视图选择的不同进行相应变化，快速建模视图下显示为SoCLib内置IP库和用户自定义IP库，模拟验证和形式验证视图则显示为工具列表，应用验证视图下显示为应用程序库。

（4）显示区，包括代码显示区和编译信息显示区。代码显示区主要提供代码显示、编辑功能；编译信息显示区显示与当前视图相关的编译输出、验证结果等，还提供命令行功能，可使用soclib cc命令执行某些编译操作。

Figure 5 Main interface of software MVIE图5 MVIE软件主界面

MVIE主要信息分为两类：工程文件和验证信息。工程文件分两种：（1）模型，用于构建完整的多核模型，在快速建模和应用验证两类视图下使用；（2）模块，用于自主编写单个模块并据此进行验证，在模拟验证和形式验证两类视图下使用。工程文件的XML信息主要描述相关文件组织结构、进行版本记录等。验证信息也分两种，（1）模型验证信息，用于对整个多核模型的运行和验证情况进行记录，在快速建模和应用验证视图下使用；（2）模块验证信息，用于对特定的模块的运行和验证情况进行记录，在模拟验证和形式验证视图下使用。模型验证信息记录多核模型的主要结构参数和应用验证的结果数据，用于对多核模型的整体评估；模块验证信息记录当前模块主要信息和进行模拟验证、形式验证的结果数据，并进行模块版本记录，用于控制模块验证过程。软件采用XML描述相关信息，各视图之间传递XML文件，软件对所有XML文件统一管理。

4 多视图协同验证环境MVIE的使用

4.1 多视图协同验证环境MVIE的使用流程

根据多核事务级模型的建立方法的不同，多视图协同验证环境MVIE的使用流程分为两种类型：（1）可称为集成建模，即基于现有模块库进行快速建模后，直接进行应用验证，验证模型建模正确性，分析体系结构性能，进行多核应用开发；（2）可称为标准建模，即用户使用SystemC自主开发部分组件模块，使用模拟验证和形式验证验证其正确性后，按照VCI规范，结合IP库中已有模块，构建多核模型，再进行应用验证，进一步验证建模正确性，分析体系结构性能，进行多核应用开发。使用MVIE进行多视图协同验证的基本流程如图6所示，其中图6a为集成建模下多视图协同验证基本流程，图6b为标准建模下多视图协同验证基本流程。

Figure 6 Basic process of multi－view co－verification using MVIE图6 使用MVIE进行多视图协同验证基本流程

4.2 多视图协同验证环境MVIE使用实例

使用MVIE，可使用SystemC进行硬件模块建模，采用VCI规范封装后集成到SoCLib平台进行模拟验证、形式验证、应用验证；也可直接基于SoCLib平台提供的SystemC模型库进行集成建模，分析验证所构建的多核系统。由于多视图协同验证环境MVIE的使用流程中，标准建模验证已包含了集成建模验证的过程，因此进行标准建模验证实验即可完整检验所建立的MVIE环境。

实验自主设计的用SystemC描述的1 KB RAM事务级模型，基于SCV进行模拟验证。用SystemC描述多核Cache一致性协议的事务级模型，使用NuSMV模型检验工具进行形式验证。使用该RAM事务级模型和Cache一致性协议模型，基于SoCLib平台构建双核系统，运行MJPEG解码程序进行应用验证。

在MVIE环境下，首先使用MVIE快速建模功能在模拟验证视图下建立RAM的模块工程，使用SystemC编写事务级模型代码。基于SCV构建自检测验证平台［9］，编写Stimulus模块、BFM/FIFO模块、Write Adaptor模块、Read Adaptor模块、Reference Model模块、Checker模块，使用SCV提供的测试向量生成机制进行模拟验证，输出结果与数学模型［10］结果比较。

在形式化验证视图下，我们使用SystemC构建多核Cache一致性协议事务级模块，并通过基于谓词的自动化抽象和模型转换技术生成Kripke结构，最后调用NuSMV模型检验工具对该模块进行形式验证［11］。在快速建模视图下，建立多核模型工程。对上述建立的两个模块按照VCI规范封装，再从SoCLib共享模型库中选择所需模块，如MIPS处理器、片上网络GMN（Generic Micronetwork）、显示设备VCI＿TTY模块、定时器VCI＿TIMER、文件系统VCI＿FDACCESS、帧缓存VCI＿FRAMEBUFFER、同步锁VCI＿LOCKS，使用顶层描述文件描述双核硬件平台，并调用硬件编译器编译SystemCASS成可执行硬件模拟平台。使用C＋＋编写MJPEG解码程序，调用MIPS交叉编译器编译成二进制文件，在可执行硬件模拟平台上运行，进行应用验证。

5 结束语

本文提出了多核事务级模型多视图协同验证方法，并论述了多视图协同验证环境的架构，最后实现了该环境MVIE。该方法针对高层次事务级建模需要，基于开放的SoCLib事务级仿真平台，将模拟验证、形式验证和应用验证有机结合起来。使用MVIE可基于SoCLib平台快速构建多核事务级模型，大大缩短复杂多核系统事务级模型开发时间，提高建模效率；多个验证视图切换由软件控制，各视图间验证数据使用XML交互，能充分发挥三种不同验证手段的优势，提高验证效率；不同模块可在不同的视图下并行验证，有利于验证人员分工合作，加快验证工作进程。但是，由于多核系统模型的复杂性，多视图下的协同验证的数据收集还比较简单，且目前形式验证技术发展尚不成熟，支持形式验证的工具方法非常有限，下一步将针对细化多视图协同验证数据、丰富形式验证工具、提高多视图验证协同度进行更深入的研究。

［1］ Jiang Shan，Huang Jian，Wang Gui－fang，et al.A brief of the international technology roadmap for semiconductors（ITRS）：Executive summary，2011［J］.Dynamic Monitoring of Science Letters，2012（4）：1－2.（in Chinese）

［2］ Foster H.Ending endless verification with questa formal verification［C］∥Proc of DVCon’08，2008：1.

［3］ Shimizu K，Gupta S，Koyama T，et al.Verification of the cell broadband engineTMprocessor［C］∥Proc of the 43rd Design Automation Conference，2006：1.

［4］ Schubert K－D.POWER7—Verification challenge of a multicore processor［C］∥Proc of the 2009 International Conference on Computer－Aided Design（ICCAD09），2009：809－812.

［5］ Turumella B，Sharma M.Assertion－based verification of a 32 thread SPARCTMCMT microprocessor［C］∥Proc of the 45th Design Automation Conference，2008：256－261.

［6］ Chen Xiao－fang，Yang Yu，Gopalakrishnan G，et al.Reducing verification complexity of a multicore coherence protocol using assume/guarantee［C］∥Proc of FMCAD’06，2006：81－88.

［7］ Borrione D，Helmy A，Pierre L V，et al.A generic model for formally verifying NoC communication architectures：A case study［C］∥Proc of NOCS’07，2007：127－136.

［8］ Chen Xiao－fang，Yang Yu，Gopalakrishnan G，et al.Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols［J］.Formal Methods in System Design，2010，36（1）：37－64.

［9］ Fang Liang，Rong Meng－tian，Liu Wen－jiang，et al.Modeling of transaction－level verification based on systemC verification library［J］.Computer Engineering，2007，33（15）：238－240.（in Chinese）

［10］ Silva D，Araujo M.An automatic testbench generation tool for a systemC functional verification methodology［C］∥Proc of the 17th Symposium on Integrated Circuits and System Design，2004：66－70.

［11］ Zhang Long.Research and implementation of model checking cache coherence protocol for multi－core processor［D］.Changsha：National University of Defence Technology，2012.（in Chinese）

附中文参考文献：

［1］ 姜山，黄健，王桂芳，等.2011版国际半导体技术路线图部分更新内容摘要［J］.科学研究动态监测快报，2012（4）：1－2.

［9］ 方亮，戎蒙恬，刘文江，等.基于SCV的事务级验证建模［J］.计算机工程，2007，33（15）：238－240.

［11］ 张龙.多核处理器Cache一致性协议模型检验研究与实现［D］.长沙：国防科学技术大学，2012.