|
 |
The Design of A Formal Property-Specification Language
Moshe Y. Vardi
Rice University
Thursday, December 5th, 2002, 4:00pm-5:00pm
540AB Cory Hall (DOP Center Classroom)
|
Abstract
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.
Speaker
Moshe Y. Vardi is Karen Ostrum George Professor in Computational Engineering and
Chair of Computer Science at Rice University. His interests focus on applications of logic to computer
science, including database theory, finite-model theory, knowledge in multi-agent
systems, computer-aided verification and reasoning, and teaching logic across the curriculum.
|
