时序电路的形式化证明

Formal Verification of Sequential Circuits

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

Formal verification is one method of verified hardware. Verifying a sequential circuit consists in proving that the given implementation of the circuit satisfies its specification. This paper presents that the implementation is given as a formula W, of the equality theory,and the Tempura program segment B capures the specification of the circuit ,goal formula of the form P include B （P imply 13） have been introduced to capture the correctness property of the circuit,where P is the initial states derived from W,. At last an example is given in order to illustrate this method.