符号模型验证器 SMV 的更多图像计算

【文件属性】：
文件名称：符号模型验证器 SMV 的更多图像计算
文件大小：128KB
文件格式：PDF
更新时间：2021-06-29 19:44:31
学术 论文 符号模型验证器 SMV 的更多图像计算 符号模型验证器 SMV 的更多图像计算 Hiromi Hiraishi 工程学院，京都产业大学，京都，日本 603-8555 摘要 本文描述了一系列提高效率的技术作为符号模型验证器 (SMV) 的核心的图像前和图像后计算，用于形式逻辑设计验证。 所提出的技术主要旨在提高异步过程验证的效率。 改进主要体现在（1）后期图像计算中过程变量的早期消除，（2）联合分区技术在异步过程验证中的应用，（3）稳定状态变量的早期替代, (4) 原像计算的非确定性替代方法。 实验测量表明，所提出的技术非常有效，与原始 SMV 相比，速度提高了 50 倍。 :copyright: 2000 Scripta Technica, Syst Comp Jpn, 31(9): 1 9, 2000 关键词：形式设计验证； 符号模型检查； 图像计算； 异步进程； SMV。 1. 引言 随着要设计的逻辑系统变得越来越大和越来越复杂，设计人员更容易犯设计错误。 逻辑模拟已被广泛用于发现设计错误。 然而，由于仿真不能涵盖所有情况，很难通过仿真来保证逻辑设计的正确性。 因此，形式化设计验证