Formal verification of hardware correctness: introduction and survey of current research

Abstract

Formal verification techniques are analyzed, focusing on two key points: suitable representation systems and mechanizable proofs. Different approaches to hardware verification are first examined, and formal verification and automated synthesis are compared to show how they cooperate in producing zero-defect designs. The different techniques are evaluated. Cross fertilization with software verification techniques is discussed.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>