Formal Techniques

A simulation testbench consists of an instance of a device-under-test (DUT) and stimulus generators that feed input signals and data to the DUT. A checker may also be present that yields a pass/fail observable output. A testbench for a formal proof of correctness will likewise contain an instance of the DUT and a checker, but instead of stimulus generation and simulation, a proof is made that the property to be checked will hold under all possible input sequences. Such input sequences may be potentially infinite.

For a formal proof to be made, the DUT must be expressed in a language that has a precise formal semantics that is understood by the proof system. Likewise, the property to be checked, known as the \textit{verification condition} must be expressed in either the same language or another language whose formal semantics are understood by the proof system. All input languages will be converted to a unified internal representation format in which the proofs are actually made. Although there is no precise definition of the term `formal semantics', it can be taken to denote a description of precisely how the system will or should behave in a machine-readable form. Normally the formal language is declarative and, like standard mathematics, respects substitution and associativity rules.

Using formal techniques in hardware design has become mainstream. Formal semantics of the synthesisable subsets of both Verilog and VHDL exist and languages such as PSL (property specification language) are widely used to define the allowable transactions on standard busses.

Individual formal proof engines are either automatic or manual. An automatic tool requires no input from the engineer to prove the result or generate a counter-example. Manual tools require the engineer to dictate the steps of the proof, but the proof engine ensures that each step is valid. In practice, the manual tools embody a lot of automation and manual intervention is often needed for the so-called automatic tools.