( ESNUG 430 Item 2 ) --------------------------------------------- [06/16/04]
From: Steve Lamb <steve.lamb=user domain=synopsys got calm>
Subject: A False Equivalence Warning for Formality 2003.06 and 2004.03
Hi, John,
The Formality product team recently discovered two situations Formality
users may be interested in and we would like your help getting the word out.
1.) We have found that a potential false equivalence could occur due to
recent changes in our solver algorithms. Our testing shows this is a
corner-case situation (we have validated that this issue affects none
of the more than 5,000 designs in Formality's regression suite).
The problem is in Formality releases between 2003.06 and 2004.03. It
has been fixed in the 2004.06 release, which is currently available
for download from SolvNet. We recommend customers migrate to this
release.
2.) Beginning in 2004.06, we have changed the default behavior regarding
Finite State Machine (FSM) encoding information in the automated
setup file (SVF file). The verification of re-encoded (or sequentially
optimized) FSMs may introduce "don't-care" logic for the unused FSM
states. When a user provides Formality the FSM state and encoding
information, by definition, they are telling it that the provided
legal state space is complete and accurate.
Our concern is that unless the user reviews the text file when using
the automated setup flow, they may be unaware that FSM state info is
being provided. Beginning in 2004.06, Formality will by default
ignore information in the automated setup file pertaining to FSMs.
Important note: All remaining content within the setup script is
validated and can continue to be used, by default, without impacting
results.
Because FSM setup information is necessary to avoid false differences,
we recommend that customers review the FSM information within the
setup file. Once determined accurate, they can tell Formality to use
this info by entering a mode controlled by setting this variable:
set svf_ignore_unqualified_fsm_information false
In 2004.06, new transcript messages clearly indicate in which mode
Formality is operating.
The release notes contain additional info concerning this change in behavior
(as well as information on many user-requested enhancements that have been
implemented in this release).
- Steve Lamb
Synopsys, Inc. Marlboro, MA
|
|
