作者：郭建形式化验证时序电路的验证tempura语言逻辑公式时序电路证明方法硬件验证表示电路初始状态公式等式规格
摘要：对硬件的形式化验证是硬件验证的一个发展方向,形式化验证一个时序电路就是证明电路的实现是否满足他的规格描述.本文提出了用等式逻辑ε的一个公式Ws来表示电路的实现,用Tempura的程序B表示对该电路的特性描述.公式P(C)B引入来证明电路的正确性,这里P是电路的初始状态,是从Ws中抽取的,另外还要从Ws提取输出等式.这样,一旦证明了P(C)B,就能证明实现满足规格描述.最后,给出了一个例子来说明此证明方法.
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
