Browse Prior Art Database

An Iterative Method to Reduce State Space for Efficient Formal Verification

IP.com Disclosure Number: IPCOM000122984D
Original Publication Date: 1998-Mar-01
Included in the Prior Art Database: 2005-Apr-04
Document File: 2 page(s) / 91K

Publishing Venue

IBM

Related People

Baumgartner, J: AUTHOR [+2]

Abstract

A method for reducing state space in a formal verification environment is disclosed. First, an exact copy of the model under test is created, and the environment (used to irritate the model) is redefined as a function of this copy. Then, network analysis is performed to remove logic from the original model not in the fanin path of the formula signals. Finally, the copy of the model is removed, and the inputs are redefined as a function of the remaining model signals (i.e., the input function is projected down to the remaining model signals). In this way, we attain a higher degree of reduction than is possible using traditional approaches.

This text was extracted from an ASCII text file.
This is the abbreviated version, containing approximately 52% of the total text.

An Iterative Method to Reduce State Space for Efficient Formal Verification

      A method for reducing state space in a formal verification
environment is disclosed.  First, an exact copy of the model under
test is created, and the environment (used to irritate the model) is
redefined as a function of this copy.  Then, network analysis is
performed to remove logic from the original model not in the fanin
path of the formula signals.  Finally, the copy of the model is
removed, and  the inputs are redefined as a function of the remaining
model signals (i.e., the input function is projected down to the
remaining model signals).  In this way, we attain a higher degree of
reduction than is  possible using traditional approaches.

      The traditional model checking approach involves creating an
environment which drives the input to the model.  The environment is
essentially a state machine design that is driven by the outputs of
the actual design to provide a legal set of values as an input to the
actual design for the model checking process.  On invariant/fanin
reduction, since the environment/model composite state bits are
dependent on each  other, even if a rule to be checked doesn't
require certain state bits  of the design, they may not be removed
due to a dependency of those bits  by the environment (i.e., the
state bits fan out to an output of the model, which is used as an
input to the environment).

      The optimization invention disclosed here achieves the
additional optimization by replacing the input dependency of the
environment upon the outputs of the actual design with a dependency
upon an exact copy of the design under test.  While this will make
the total  number of states bits initially more than the traditional
approach, the  actual design under test will be substantially reduced
when the fanin/invariant optimization is performed.  It is important
to note that  this fanin/invariant optimization can be performed by
network analysis  alone; state space does not need to be searched.
Therefore, the increased state space size in this step is not a
consideration factor.

      The copy of the design in the environment can now be removed
and the environment input can be redefined to be a function of the
state bits that actually take part in the evaluation of the rule in
the reduced model.  This iterative process thus yields an overall
composite model of the environment/des...