| 基于Mealy机精化关系的验证算法 |
| |
| 引用本文： | 梁虹,金乃咏.基于Mealy机精化关系的验证算法[J].计算机应用与软件,2012,29(8):169-172. |
| |
| 作者姓名： | 梁虹 金乃咏 |
| |
| 作者单位： | 1. 中国科学院软件研究所 北京100080
2. 新思科技有限公司验证组 上海200050 |
| |
| 摘 要： | 与传统验证方法相比,形式验证技术因其完备性,已在数字电路设计领域中得到越来越多的关注。通过对形式验证技术和状态机的研究,在LTL公式的可实现策略基础上,提出一个基于Mealy机精化关系的验证算法,实现了一个搜索工具原型:支持算术表达式的LTL性质描述,在设计空间中搜索满足给定规范的输入输出信号。该技术可应用于定位电路设计中满足给定功能性质的代码片段。
|
| 关 键 词： | 形式验证 性质验证 精化 Mealy机 |
A VERIFICATION METHOD BASED ON REFINEMENT OF MEALY MACHINE |
| |
| Liang Hong
,
Jin Naiyong.A VERIFICATION METHOD BASED ON REFINEMENT OF MEALY MACHINE[J].Computer Applications and Software,2012,29(8):169-172. |
| |
| Authors: | Liang Hong Jin Naiyong |
| |
| Affiliation: | 1(Institute of Software,Chinese Academy of Sciences,Beijing 100080,China) 2(Verification Group,Synopsys Company,Shanghai 200050,China) |
| |
| Abstract: | |
| |
| Keywords: | Formal verification Property verification Refinement Mealy machine |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
