基于时态逻辑的硬件设计形式化验证技术——模型检验  

HARDWARE DESIGN'S FORMAL VERIFICATION BASED ON TEMPORAL LOGIC——MODEL CHECKING

作　　者：郭建[1] 杜惠敏[2] 韩俊刚[1] 郝克刚[3] 

机构地区：[1]西安邮电学院ASIC中心,陕西西安710069 [2]西北工业大学计算机科学系,陕西西安710072 [3]西北大学计算机科学系,陕西西安710072

出　　处：《小型微型计算机系统》2001年第5期521-524,共4页Journal of Chinese Computer Systems

基　　金：国家自然科学基金资助! (NO69473 0 17)

摘　　要：通过对时态逻辑的研究来探讨时态逻辑在硬件设计形式化验证上的应用 ,同时对布尔函数在计算机内的表示二叉判定图 (BDD)进行了进一步地分析 。This article discusses the temporal logical application on the hardware verification, and analyzes the boolean function's expression -BDD in the computer. At last an example about hardware verification is given.

关 键 词：时态逻辑 模型检验 布尔函数 硬件设计 形式化验证 计算机 

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