使用形式化验证方法进行流水线验证  

Formalization Method for Pipeline Verification

作　　者：高妍妍[1] 李曦[1] 熊焰[1] 余洁[1] 

机构地区：[1]中国科学技术大学计算机科学技术系,安徽合肥230027

出　　处：《小型微型计算机系统》2008年第6期1168-1172,共5页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(60273042)资助;高等学校博士学科点专项科研基(20050358040)资助

摘　　要：随着流水线技术的广泛应用,流水线设计的验证问题也越来越受到业界的关注.本文提出的方法作为自上而下验证方法的一部分,可以在指令级对流水线设计的正确性进行检验.本文从控制逻辑的角度对流水线的行为进行分析,通过为控制逻辑建立FSM表示,以及采用NuSMV作为验证工具,达到对流水线的自动验证.这种方法的优势在于是以流水段为单位进行检验,这种局部验证的方法不但可以降低建模和检验的复杂度,还可以极大地缩短验证时间.With the development and application of pipeline technique in processor, the designs of pipeline verification is becoming important in academies and industries. This paper presents a method to check the correctness of pipeline at instruction level. This method is based on the control logic of the pipeline. Through the analysis of the system, an FSM model is extracted from the control logic. The model can be verified automatically by using NuSMV, which is a tool used for model checking. This method verifies the pipeline stages separately. This local verification not only reduces the complication of modeling and verification of the system but also cuts down the time of the verification.

关 键 词：流水线 模型检验 控制逻辑 体系结构描述语言 

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