Formal Verification of Sequential Circuits
Jian Wen Guo · Modern Electronic Technique · 2005
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_s of the equality theory,and the Tempura program segment B capures the specification of the circuit,goal formula of the form PB(P imply B) have been introduced to capture the correctness property of the circuit,where P is the initial states derived from W_s.At last an example is given in order to illustrate this method.