时序电路的形式化证明

• 作者: 郭建
• 来源期刊: 现代电子技术
• 关键词: 形式化验证 时序电路的验证 Tempura语言 逻辑公式
• 年，卷（期）: 2005,（20）
• 所属期刊栏目: 测试·封装·材料
• 页码范围: 57-60
• 页数: 4页
• 分类号: TN79+.1
• 语种: 中文
• DOI: 10.3969/j.issn.1004-373X.2005.20.028

摘要

对硬件的形式化验证是硬件验证的一个发展方向,形式化验证一个时序电路就是证明电路的实现是否满足他的规格描述.本文提出了用等式逻辑ε的一个公式Ws来表示电路的实现,用Tempura的程序B表示对该电路的特性描述.公式P(C)B引入来证明电路的正确性,这里P是电路的初始状态,是从Ws中抽取的,另外还要从Ws提取输出等式.这样,一旦证明了P(C)B,就能证明实现满足规格描述.最后,给出了一个例子来说明此证明方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭建		9	48	4.0	6.0