Subject: formal semantics
From: John Havlicek (john.havlicek@motorola.com)
Date: Fri Aug 02 2002 - 09:10:19 PDT
Dear SV-AC:
At yesterday's meeting there was repeated the question, what
is the value of formal (a.k.a., mathematically precise) semantics?
At Motorola, we see important value deriving from increasing the level
of mathematical precision in all aspects of design development,
verification, reuse, and export. Mathematically precise semantics for
a verification property language helps to:
1. Enable mathematically precise reasoning about the properties
written, their satisfaction or failure, the design under test (DUT),
and the testing environment, all in the absence of visibility into
the implementations of the EDA tools.
2. Enable separation of the concern of behavior of EDA tools from
the concerns of correctness of properties written, DUTs, and test
environments.
3. Reduce the variability of verification results from one EDA tool
to another.
We do not think the need for mathematical precision is less for
a property language of assertions embedded within design descriptions
than for a property language written externally to design descriptions.
We believe that our designers and verification engineers both have the
aptitude for mathematical precision. For many years now, we have been
deploying the same internal property writing language to both of these
groups.
We do not want to see from Accellera divergence of the property writing
language standard for designers from that for verification engineers.
We also do not want Accellera to promote a mathematically imprecise
property writing language for designers. We do want to see alignment
between the property writing language of embedded assertions and the
general temporal property writing language.
Best regards,
John Havlicek
This archive was generated by hypermail 2b28 : Fri Aug 02 2002 - 09:12:16 PDT