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

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

通过对时态逻辑的研究来探讨时态逻辑在硬件设计形式化验证上的应用 ,同时对布尔函数在计算机内的表示二叉判定图 (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.