Due to the complexity of any hardware design in use today (eg: industrial-scale designs, such as microprocessors, floating-point hardware, protocols, memory subsystems, and communications hardware), the use of formal methods has been generalized for ensuring quality and correctness.
There are two main aspects to the application of formal methods in a design process:
- the formal framework that is used to specify the desired properties of a design.
These include temporal logics, predicate logic, abstraction and refinement.
- the verification techniques and tools used to reason about the relationship between a specification and a corresponding implementation. These include model checking, automata-theoretic techniques, automated theorem proving, and approaches that integrate the above methods.