SPHINX is a design verification tool for asynchronous circuits
and systems which has the capability of verifying speed
independence and conformance of asynchronous circuits
to their specifications. The verification is performed in a
hierarchical (pyramidal) fashion, to reduce the complexity
associated with the state explosion problem. The verification
problem is decomposed into the verification of a number of
circuit blocks, where each circuit block can be
hierarchically and recursively verified in the same manner. For
a given circuit block (e.g., the original circuit at the highest
level of hierarchy), a selected set of circuit signals, called
external signals, is used to partition the circuit
into circuit blocks of a lower level. A safe abstraction
of the behavior of the external signals is found by a partial
order analysis of the behavior of all the signals of the
current circuit. A safe abstraction, by definition, is a
behavior over the set of external signals which is guaranteed to
exactly resemble the behavior of those signals if the circuit is
in fact failure-free, and which otherwise will never
over-estimate that behavior. A safe abstraction is then used to
derive specifications for each of the corresponding
circuit blocks. Each derived specification is mirrored to create
an environment element for the corresponding circuit
block. Next step of hierarchical verification will then consist
of verifying whether each circuit block conforms to its
derived specification. This is performed by verifying whether
the closed subcircuit obtained by the composition of a
circuit block with its derived environment element is
failure-free. Such a closed circuit is failure-free
if it is hazard-free and there is no input-chokes
at the inputs of its environment element.
Theory:
Hiding Memory Elements in Hierarchical Verification of
Speed-Independent Circuits
A previous method for the verification of speed-independent
circuits [Roig et al.] computed the behavior of the
corresponding complex gate circuit, and then verified the
failure-freedom of each complex gate using the derived safe
abstraction. The limitation of such complex-gate approaches is
that no internal signal of a complex gate can be the output of a
memory-element (e.g., a C-element). In other words,
previous methods could not hide the outputs of memory elements
when finding safe abstractions of circuit behaviors. In
contrast, we have shown that by using an observationally
sufficient set of external signals, and appropriate partial
order analysis techniques, the outputs of memory elements can be
hidden in finding the safe abstraction of the behavior of such
external signals. Since most asynchronous circuits are dominated
by memory-elements, we expect greater speed-ups for the
verification of such circuits. The following paper
IWLS'98
paper outlines the theory in more detail. The theory, in a
more visual setting can be found in a set of
TECHCON'98 slides.
Possible future improvements to SPHINX are
listed in a
README
file, along with the options to run the code. A list of the new
features and the latest bug fixes can be found in
UPGRADE.
Comments and bug reports are very welcome and appreciated.
An input file of SPHINX contains the circuit
structure, pointers to the specification files (e.g., an STG
specification), the BDD ordering information, and the set of
external signals of the highest level of hierarchy. The circuit
components can be either gates, or modules which
are specified in separate files. The input files have an easy to
understand syntax. Information on the format of input files can
be found in the
EX_README.
I graduated in 2000, and I am not really
maintaining SPHINX anymore. Yet, you can reach me at vida .
vakil at alumni . usc . edu for questions or comments, or if you
can provide me with any interesting circuit examples, or to
report any instance of SPHINX crashing.
Acknowledgements
SPHINX uses the Generic Utilities
package of
VIS,
and in particular the CU Decision Diagram package.
Tool Capabilities