The Design of A Formal Property-Specification Language

In recent years, the need for formal specification languages is growing rapidly as the functional validation environment in semiconductor design is changing to include more and more validation engines based on formal verification technologies. In particular, the usage of Formal Equivalence Verification and Formal Property Verification is growing, new symbolic simulation engines are introduced and hybrid environments of scalar and symbolic simulators are developed. To facilitate the use of these new-generation validation engines - properties, checkers and reference models need to be developed in a formal language.

In this talk we describe the design of the ForSpec Temporal Logic (FTL), the new temporal logic of ForSpec, Intel's new formal property-specification language, which is today part of Synopsis OpenVera hardware verification language (www.open-vera.com). The key features of FTL are: it is a linear temporal logic, based on Pnueli's LTL, it enables the user to define temporal connectives over time windows, it enables the user to define regular events, which are regular sequences of Boolean events, and then relate such events via special connectives, and it contains constructs that enable the user to model multiple clock and reset signals, which is useful in the verification of globally asynchronous and locally synchronous hardware designs.

The focus of the talk is on design rationale, rather than a detailed language description.