时序电路的形式化证明

摘要：

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

关键词：形式化验证、时序电路的验证、Tempura语言、逻辑公式

所属期刊栏目：28

分类号：TN79+.1(基本电子电路)

资助基金：国家自然科学基金90207015

在线出版日期：2005-11-17（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：57-60