协同形式验证环境Co-Formal的建立与应用  

Setup and Applications of the Co-Formal Verification Environment Co-Formal

作　　者：王彬[1] 林争辉[1] 

机构地区：[1]上海交通大学电子工程系,上海200030

出　　处：《上海交通大学学报》2003年第z1期143-146,151,共5页Journal of Shanghai Jiaotong University

基　　金：美国国家科学基金(5978EastAsiaandPacificProgram-9602485);教育部博士点基金资助项目

摘　　要：形式验证存在状态爆炸的问题,特别是软硬件的协同验证难以解决.为此研究了片上系统的协同形式验证问题,给出了一种高效的协同形式验证环境Co-Formal,用于从行为级到具体实现级的软硬件协同形式验证.以一个实际的硬件系统验证了该环境的可用性.Formal verification has attracted great interests in recent years. But the real world system is too complex to be verified directly by symbolic model checking because of state explosion. Another difficulty in validation of system on chip (SoC) is how to coverify of HW/SW. This paper is focused on the coformal verification for SoC. It presented an effective formal coverification environment CoFormal. In this environment, we can coverify a system at behavior level and implementation level. A real circuit system was verified to illustrate the usage of this environment.

关 键 词：协同形式验证环境 模型检查 片上系统 

分 类 号：TN407[电子电信—微电子学与固体电子学]