FPGA Formal Verification: A Local Logic Correctness Approach

Hardware verification is the proof that a circuit or a system (its implementation) behaves according to a given set of requirements (its specification). Design faults may result from an erroneous transformation of a design specification into the layout description, the latter being the basis of fabrication. A formal specification is a concise description of the behavior and properties of a system written in a mathematically based language. It will state what a system is supposed to do in the context it is supposed to operate as abstractly as possible, thereby eliminating distracting detail and providing a general description resistant to future system modifications. Suppose logic is used to formalize both the specification and the implementation. In that case, the verification procedure will lead to proof of logical equivalence that the two formalisms are the same or an implication that the implementation covers the specification. Verification is only a correct proposition concerning a formal specification. If the specification or the modeling is wrong, then even a positive result of a correctness proof is meaningless. This article will glue the implementation and specification in one formalism, a.k.a local logic, to avoid the inherent discrepancy between the two formalisms. This article proposes that an FPGA is correct if its local logic is sound and complete.