[PRL] Fwd: Talk, Friday July 23, 2-3pm

[David A. Herman]

I just went to a talk by Moshe Vardi on the hardware verification language
he helped design at Intel. It was an interesting talk about the trade-offs
and design decisions that went into using temporal logics and model
checking for an industrial system.

Highlights:

- While CTL and LTL are incomparable in terms of the specifications they
can express, Moshe claimed that in practice LTL is more useful. I don't
think he really got into a justification of this claim.
- Their language is based on LTL, but wait, there's more...
- They have ASSUME and ASSERT primitives that allow an assume-guarantee
model of compositional verification.
- They have a regular-expression-like language for combining propositions,
whose composability has allowed people to write big libraries of reusable
propositions.
- They have a couple of extra primitives not present in LTL that
apparently cover the vast majority of use cases for the hardware domain.

Matthias: Moshe says hi.
Mitch: I helped him plug LMCS. :)

Dave

---------- Forwarded message ----------
Date: Fri, 23 Jul 2004 15:36:23 -0700 (PDT)
From: David Herman <dherman at email.arc.nasa.gov>
To: dherman at ccs.neu.edu
Subject: Talk, Friday July 23, 2-3pm (fwd)



---------- Forwarded message ----------
Date: Wed, 21 Jul 2004 17:14:33 -0700
From: Klaus Havelund <havelund at email.arc.nasa.gov>
To: seminars at email.arc.nasa.gov
Subject: Talk, Friday July 23, 2-3pm


TALK!

Title: The Design of A Formal Property-Specification Language
Speaker: Moshe Y. Vardi
Rice University
http://www.cs.rice.edu/~vardi

Time: Friday July 23, 2-3pm
Place: room 100, building 262

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.

--