Verification languages

Verification is the process of checking whether a given design is correct with respect to its specification. The specification itself can be in different forms - it can be a nontangible entity such as a designer’s intent, or a document written in a natural language, or expressions written in a formal language. In this chapter, we consider a verification language to be a language with a formal syntax, which supports expression of verification-related tasks. It is very useful for a verification language to have a precise unambiguous semantics. However, we also consider languages where ambiguity in semantics is resolved by accepted practices. Broadly speaking, we focus on the support a verification language provides for dynamic verification based on simulation, as well as static verification based on formal techniques. Though we discuss some high-level behavioral modeling languages also, we highlight their verification-related features. Other details on how they are used for representing higher-level models can be found in other recent articles [1,2].