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

J4 ›› 2014, Vol. 36 ›› Issue (05): 821-827.

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

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

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

收稿日期:2013-08-10 修回日期:2013-11-16 出版日期:2014-05-25 发布日期:2014-05-25
基金资助:
国家自然科学基金资助项目（61133007）

Multi-core transaction level modeling and
multi-view co-verification environment

WANG Jun，LIU Lei，ZHANG Long，LI Sikun

（State Key Laboratory of High Performance Computing,National University of Defense Technology,Changsha 410073,China）

Received:2013-08-10 Revised:2013-11-16 Online:2014-05-25 Published:2014-05-25

摘要/Abstract

摘要：

随着集成电路工艺持续高速发展，片上处理器核数目呈现指数增长规律，设计复杂程度不断增长，对处理器验证提出了严峻的挑战，至今仍缺乏有效的工具手段。提出了一种多核处理器事务级模型的多视图协同验证方法，将模拟验证、形式验证、应用验证三种不同验证视图，采用统一平台集成为一体化验证环境。从而可在一体化验证环境中，充分发挥多种验证方法综合应用的优势，协同高效完成多核处理器事务级模型验证任务。基于SoCLib事务级建模仿真平台实现了一个具有良好可扩展性的多视图协同验证环境MVIE。初步应用实验结果表明，多视图协同验证和传统单一视图验证方法相比，在模型验证的方便性、完备性、高效性以及模型数据一致性维护等方面，具有明显的优势。

关键词: 多核处理器, 事务级模型, 多视图, 协同验证, SoCLib平台

Abstract:

With the continuous rapid development of integrated circuit technology, the exponential growing of the number of onchip processor cores, the growing complexity of the design, the processor verification faces challenges. However, so far effective tools are still lacked. The paper proposes a multiview coverification method regarding transactionlevel modeling of multicore processors. Using a unified platform, the multiview coverification environment contains simulation verification, formal verification and application verification as three different views. Hence, multicore processors transactionlevel model validation task can be done in this integrated verification environment, owning multiple methods advantages of three different views. Based on a transactionlevel modeling and simulation platform, named SoCLib, we implement a good scalable multiview coverification environment called MVIE. Experimental results show that, compared with traditional single view verification, the proposed multiview coverification method has obvious advantages in transaction verification, especially in terms of convenience, completeness, efficiency, and model data consistency maintenance, etc.

Key words: multi-core processor;transaction level modeling;multi-view;co-verification;SoCLib platform

王俊，刘磊，张龙，李思昆. 多核处理器事务级模型多视图协同验证环境[J]. J4, 2014, 36(05): 821-827.

WANG Jun，LIU Lei，ZHANG Long，LI Sikun. Multi-core transaction level modeling and
multi-view co-verification environment [J]. J4, 2014, 36(05): 821-827.

参考文献

［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 engineTM processor［C］∥Proc of the 43rd Design Automation Conference, 2006:1.
［4］Schubert KD. POWER7—Verification challenge of a multicore 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 SPARCTM CMT 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.

[1]	张翼飞, 邓秀勤, 王卓薇. 特征直连与结构化约束的多视图子空间聚类[J]. 计算机工程与科学, 2022, 44(04): 753-760.
[2]	欧琦媛, 祝恩. 基于压缩子空间对齐的多核聚类算法[J]. 计算机工程与科学, 2021, 43(10): 1730-1735.
[3]	罗莉, 周宏伟, 周理, 潘国腾, 周海亮, 刘彬. 一种多核处理器直连接口QoS的设计与验证[J]. 计算机工程与科学, 2021, 43(04): 620-627.
[4]	陈倩,刘云,高钰莹. 并行动态位向量频繁闭合序列模式挖掘算法[J]. 计算机工程与科学, 2018, 40(10): 1717-1725.
[5]	杨胜哲，于俊清,唐九飞. 数据流程序动态调度与优化[J]. 计算机工程与科学, 2017, 39(07): 1201-1210.
[6]	魏朝磊1，闫民2，赵方1. OpenMP多核技术在颗粒流体力学方法GHM中的应用[J]. 计算机工程与科学, 2017, 39(07): 1234-1240.
[7]	姚文军,陈俊仕,苏志超,余洋,廖陈志,安虹. 基于神威太湖之光的NAMD软件的移植与优化[J]. 计算机工程与科学, 2017, 39(06): 1022-1030.
[8]	唐秋虎，张志毅. 基于多视图像的摄像机自标定方法[J]. 计算机工程与科学, 2017, 39(04): 748-755.
[9]	杜琦，姜浩，李宽，彭林，杨灿群. 面向ARMv8 64位多核处理器QTRSM的实现[J]. 计算机工程与科学, 2017, 39(03): 451-457.
[10]	朱峰军1，武继刚1, 2，史雯隽1，姜桂圆3. 多选择软硬件划分问题的计算模型与动态规划算法[J]. J4, 2015, 37(04): 641-648.
[11]	温浩宇,刘芬芳,刘燕燕. 多视图下的生产线建模与仿真[J]. J4, 2014, 36(09): 1823-1828.
[12]	毛席龙，杨安，吕高锋，林琦，程辉. 基于可变步长的访存延迟测量模型的研究与实现[J]. J4, 2014, 36(01): 12-18.
[13]	孙连山，王今雨. 一种面向特征的软件产品线非功能需求建模方法[J]. J4, 2013, 35(5): 67-76.
[14]	李艳华，张悠慧，王为，郑纬民. 延时敏感的推测多线程调度策略[J]. J4, 2013, 35(11): 14-21.
[15]	徐远超1,2,谭旭2,3,范灵俊2,3,孙卫真1，张志敏2. 性能不对称多核处理器负载均衡调度研究[J]. J4, 2013, 35(11): 80-86.