Sphinx

The tool was developed at the USC Asynchronous CAD Group by Vida Vakilotojar as part of her Ph.D. dissertation under the guidance of Dr. Peter A. Beerel. This project has been funded by the Semiconductor Research Corporation, SRC and a gift from the Intel corporation. Vida graduated in August 2000.

Tool Capabilities

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.

Dissertation: Induced Hierarchical Verification of Asynchronous Circutis Using a Partial Order Technique

Getting SPHINX-1.1 Solaris executables

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.

Some Example Circuits

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.

Getting SPHINX-1.1 Source Code

Questions or comments?

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,

Acknowledgements

SPHINX uses the Generic Utilities package of VIS, and in particular the CU Decision Diagram package