使用局部建模的微处理器测试程序自动生成方法  

Test Program Generation for Microprocessor Verification Using Local Modeling Strategy

作　　者：张良[1] 易江芳[2] 佟冬[1] 程旭[1] 王克义[1] 

机构地区：[1]北京大学深圳研究生院,广东深圳518055 [2]北京大学微处理器研究开发中心,北京100871

出　　处：《电子学报》2011年第7期1639-1644,共6页Acta Electronica Sinica

基　　金：国家"863"高技术研究发展计划重点项目(No.2006AA010202)

摘　　要：模拟仿真方法是当前微处理器功能验证的主要方法,然而在验证工作后期需要耗费大量的时间来检验余下复杂的功能点,验证收敛速度缓慢.针对该问题,本文在覆盖率增长缓慢时,引入结合模型检验引擎的测试程序生成方法.该方法首先采用局部建模策略为处理器构建抽象设计模型,然后使用模型检验引擎读入该模型并产生测试生成指导规则,最后,随机测试生成器依据指导规则产生大量测试程序作为模拟器输入,完成功能验证工作.以北大众志UniCore32定点处理器核的功能验证为例评估本文方法,结果表明,使用该方法可以快速完成对未覆盖功能点的验证,加速验证收敛.Simulation is the major technique used for processor verification.In the late of the verification process,simulation requires a lot of expert time and computer resources to verify residual complicated functional points,which slows down the verification progress.This paper introduces a test generation method based on model checking engine to address this problem.First,an abstract microprocessor model focuses on these uncovered functional points is constructed using local modeling strategy.Second,model checker reads this abstract model and automatically produces test generator directives.Finally,these directives guide random test generator to generate test programs that cover the specified functional points.Experiments on verifying PKUnity UniCore32 microprocessor demonstrated that this method spent little time to cover these uncovered coverage tasks and increased the verification efficiency.

关 键 词：功能验证 模型检验 局部建模 测试程序生成 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]